code/SokobanObjectwise.icl

   1 module SokobanObjectwise
   2
   3 import StdString
   4 import StdFile
   5 import StdTuple
   6 import StdFunc
   7 import StdOrdList
   8 import StdList
   9
  10 from Data.Func import $
  11 from Data.List import intercalate, maximum, permutations
  12 from Text import class Text(concat,join), instance Text String
  13
  14 import Sokoban
  15
  16 :: AnnotatedSokoban :== [(Int, Int, SokobanTile)]
  17
  18 Start :: *World -> *World
  19 Start w
  20 # (io, w) = stdio w
  21 # (puzzle, io) = parseFromFile io
  22 # io = io <<< encode puzzle <<< "\n"
  23 = snd (fclose io w)
  24
  25 encode :: SokobanPuzzle -> String
  26 encode p = join "\n" [
  27         "MODULE main",
  28         "VAR",
  29         encodeAgentVars maxX maxY,
  30         encodeBoxVars (indexList boxes) maxX maxY,
  31         "\tmovement: {left, up, right, down, finished};",
  32         "",
  33         "DEFINE dx := case",
  34         "\t\tmovement = left : -1;",
  35         "\t\tmovement = right: +1;",
  36         "\t\tTRUE:              0;",
  37         "\tesac;",
  38         "\tdy := case",
  39         "\t\tmovement = up  : -1;",
  40         "\t\tmovement = down: +1;",
  41         "\t\tTRUE:             0;",
  42         "\tesac;",
  43         "",
  44         "INIT",
  45         encodeAgentInit agent <+ " &",
  46         encodeBoxInit boxes <+ ";",
  47         "--Agent not on the box",
  48         "INVAR " <+ encodeAgentNotOnBox (indexList boxes) <+ ";",
  49         "--Allowed box positions on the field",
  50         encodeBoxPositions (indexList boxes) legalPos,
  51         "--Box not on box",
  52         encodeBoxOnBoxes (indexList boxes),
  53         "--Allowed agent positions",
  54         "INVAR " <+ encodeAgentPositions legalPos,
  55         "--Goal state",
  56         "INVAR " <+ encodeGoalState (indexList boxes) targetPos <+ ";",
  57         "",
  58         encodeAgentMovement,
  59         encodeBoxMovement (indexList boxes),
  60         "CTLSPEC ! EF (movement = finished);",
  61
  62         ""]
  63         where
  64                 targetPos = getTargets annot
  65                 boxes = getBoxes annot
  66                 agent = hd $ getAgents annot
  67                 legalPos = legalPositions annot
  68                 annot = annotate p
  69                 (maxX, maxY) = getMetrics annot
  70
  71 //THIS IS NAIVE AND SHOULD BE IMPROVED
  72 legalPositions :: AnnotatedSokoban -> [(Int, Int)]
  73 legalPositions p = [(x, y)\\(x, y, t)<-p | case t of Wall=False; _=True]
  74
  75 annotate :: SokobanPuzzle -> AnnotatedSokoban
  76 annotate (Sokoban p) = flatten [[(x, y, t)\\t<-r & x<-[0..]]\\r<-p & y<-[0..]]
  77
  78 getTargets :: AnnotatedSokoban -> [(Int, Int)]
  79 getTargets p = [(x, y)\\(x, y, t)<-p |
  80         case t of Target=True;TargetBox=True;TargetAgent=True;_=False]
  81
  82 getMetrics :: AnnotatedSokoban -> (Int, Int)
  83 getMetrics p = (maximum (map fst3 p),maximum (map snd3 p))
  84
  85 getAgents :: AnnotatedSokoban -> [(Int, Int)]
  86 getAgents p = [(x, y)\\(x, y, Agent)<-p] ++ [(x, y)\\(x, y, TargetAgent)<-p]
  87
  88 getBoxes :: AnnotatedSokoban -> [(Int, Int)]
  89 getBoxes p = [(x, y)\\(x, y, Box)<-p] ++ [(x, y)\\(x, y, TargetBox)<-p]
  90
  91 (<+) infixr 5 :: a b -> String | toString a & toString b
  92 (<+) a b = toString a +++ toString b
  93
  94 encodeGoalState :: [Int] [(Int, Int)] -> String
  95 encodeGoalState boxes targets = "(" <+
  96         join " |\n\t" (map encodeOneGoal boxtargets) <+ ")<->movement=finished"
  97         where
  98                 boxtargets = map (zip2 targets) (permutations boxes)
  99
 100                 encodeOneGoal :: [((Int, Int), Int)] -> String
 101                 encodeOneGoal p = "(" <+ join " & " (encodeOneGoal` p) <+ ")"
 102
 103                 encodeOneGoal` :: [((Int, Int), Int)] -> [String]
 104                 encodeOneGoal` [] = []
 105                 encodeOneGoal` [((x, y), b):xs] = [
 106                         "b" <+ b <+ "x = " <+ x <+ " & " <+
 107                         "b" <+ b <+ "y = " <+ y:encodeOneGoal` xs]
 108
 109 encodeBoxOnBoxes :: [Int] -> String
 110 encodeBoxOnBoxes [] = ""
 111 encodeBoxOnBoxes [b] = ""
 112 encodeBoxOnBoxes [b:bs] = "INVAR " <+ encodeBoxOnBox b bs <+ ";\n" <+
 113         encodeBoxOnBoxes bs
 114         where
 115                 encodeBoxOnBox :: Int [Int] -> String
 116                 encodeBoxOnBox x bs = join " & " ["!(b" <+ x <+ "x=b" <+ b <+ "x &" <+
 117                         "b" <+ x <+ "y=b" <+ b <+ "y)"\\b<-bs]
 118
 119 encodeAgentNotOnBox :: [Int] -> String
 120 encodeAgentNotOnBox bs = join " &\n\t" [
 121         "!(b" <+ i <+ "x = agentx & b" <+ i <+ "y = agenty)"\\i<-bs]
 122
 123 encodeObPosition :: String [(Int, Int)] -> String
 124 encodeObPosition b p = join " | " [
 125         "(" <+ b <+ "x=" <+ x <+ " & " <+
 126         b <+ "y=" <+ y <+ ")"\\ (x, y)<-p]
 127
 128 encodeAgentInit :: (Int, Int) -> String
 129 encodeAgentInit (x, y) = "\tagentx=" <+ x <+ " & " <+ "agenty=" <+ y
 130
 131 encodeAgentVars :: Int Int -> String
 132 encodeAgentVars mx my =
 133         "\tagentx: 0.." <+ mx <+ ";\n\tagenty: 0.." <+ my <+ ";\n"
 134
 135 encodeAgentPositions :: [(Int, Int)] -> String
 136 encodeAgentPositions p = encodeObPosition "agent" p
 137
 138 encodeAgentMovement :: String
 139 encodeAgentMovement = "TRANS next(agentx) = agentx + dx;\n" <+
 140         "TRANS next(agenty) = agenty + dy;"
 141
 142 encodeBoxInit :: [(Int,Int)] -> String
 143 encodeBoxInit bs = join " &\n" [
 144         "\tb" <+ i <+ "x=" <+ x <+ " & " <+
 145         "b" <+ i <+ "y=" <+ y
 146         \\(x, y)<-bs & i<-[0..]]
 147
 148 encodeBoxVars :: [Int] Int Int -> String
 149 encodeBoxVars p mx my = join "\n"
 150         ["\tb" <+ i <+ "x: 0.." <+ mx <+ ";\n" <+
 151         "\tb" <+ i <+ "y: 0.." <+ my <+ ";" \\ i<-p]
 152
 153 encodeBoxPositions :: [Int] [(Int, Int)] -> String
 154 encodeBoxPositions bs ps = join "\n" [
 155         "INVAR " <+ encodeObPosition ("b" <+ b) ps <+ ";"\\b<-bs]
 156
 157 encodeBoxMovement :: [Int] -> String
 158 encodeBoxMovement bs = join "\n" $ map ebm bs
 159         where
 160                 ebm :: Int -> String
 161                 ebm i =
 162                         "TRANS next(b" <+ i <+ "x) = case\n" <+
 163                         "\t\tnext(agentx) = b" <+ i <+ "x & " <+
 164                         "next(agenty) = b" <+ i <+ "y: b" <+ i <+ "x + dx;\n" <+
 165                         "\t\tTRUE: b" <+ i <+ "x;\n" <+
 166                         "\tesac;\n" <+
 167                         "TRANS next(b" <+ i <+ "y) = case\n" <+
 168                         "\t\tnext(agentx) = b" <+ i <+ "x & " <+
 169                         "next(agenty) = b" <+ i <+ "y: b" <+ i <+ "y + dy;\n" <+
 170                         "\t\tTRUE: b" <+ i <+ "y;\n" <+
 171                         "\tesac;"