1 module SokobanObjectwise
10 from Data.Func import $
11 from Data.List import intercalate, maximum, permutations
12 from Text import class Text(concat,join), instance Text String
16 :: AnnotatedSokoban :== [(Int, Int, SokobanTile)]
18 Start :: *World -> *World
21 # (puzzle, io) = parseFromFile io
22 # io = io <<< encode puzzle <<< "\n"
25 encode :: SokobanPuzzle -> String
26 encode p = join "\n" [
29 "\tx: 0.." <+ maxX <+ ";",
30 "\ty: 0.." <+ maxY <+ ";",
32 "INVAR " <+ encodeObPosition legalPos,
36 "\tagent: " <+ declareObject agent,
37 join "\n" ["\tb" <+ i <+ ": " <+ declareObject b\\i<-boxnums & b<-boxes],
38 "\tmovement: {left, up, right, down, finished};",
39 "--Handy variable for deltas",
41 "--Agent not on the box",
42 "INVAR " <+ encodeAgentNotOnBox boxnums <+ ";",
44 encodeBoxOnBoxes (indexList boxes),
46 "INVAR " <+ encodeGoalState boxnums targetPos <+ ";",
48 encodeObMovement "agent",
49 encodeBoxMovement boxnums,
50 "CTLSPEC ! EF (movement = finished);",
54 targetPos = getTargets annot
55 boxes = getBoxes annot
56 boxnums = indexList boxes
57 agent = hd $ getAgents annot
58 legalPos = legalPositions annot
60 (maxX, maxY) = getMetrics annot
62 declareObject :: (Int, Int) -> String
63 declareObject (x, y) = "ob(" <+ x <+ ", " <+ y <+ ");"
66 deltaDefine = join "\n" [
68 "\t\tmovement = left : -1;",
69 "\t\tmovement = right: +1;",
73 "\t\tmovement = up : -1;",
74 "\t\tmovement = down: +1;",
78 //THIS IS NAIVE AND SHOULD BE IMPROVED
79 legalPositions :: AnnotatedSokoban -> [(Int, Int)]
80 legalPositions p = [(x, y)\\(x, y, t)<-p | case t of Wall=False; _=True]
82 annotate :: SokobanPuzzle -> AnnotatedSokoban
83 annotate (Sokoban p) = flatten [[(x, y, t)\\t<-r & x<-[0..]]\\r<-p & y<-[0..]]
85 getTargets :: AnnotatedSokoban -> [(Int, Int)]
86 getTargets p = [(x, y)\\(x, y, t)<-p |
87 case t of Target=True;TargetBox=True;TargetAgent=True;_=False]
89 getMetrics :: AnnotatedSokoban -> (Int, Int)
90 getMetrics p = (maximum (map fst3 p),maximum (map snd3 p))
92 getAgents :: AnnotatedSokoban -> [(Int, Int)]
93 getAgents p = [(x, y)\\(x, y, Agent)<-p] ++ [(x, y)\\(x, y, TargetAgent)<-p]
95 getBoxes :: AnnotatedSokoban -> [(Int, Int)]
96 getBoxes p = [(x, y)\\(x, y, Box)<-p] ++ [(x, y)\\(x, y, TargetBox)<-p]
98 (<+) infixr 5 :: a b -> String | toString a & toString b
99 (<+) a b = toString a +++ toString b
101 encodeGoalState :: [Int] [(Int, Int)] -> String
102 encodeGoalState boxes targets = "(" <+
103 join " |\n\t" (map encodeOneGoal boxtargets) <+ ")<->movement=finished"
105 boxtargets = map (zip2 targets) (permutations boxes)
107 encodeOneGoal :: [((Int, Int), Int)] -> String
108 encodeOneGoal p = "(" <+ join " & " (encodeOneGoal` p) <+ ")"
110 encodeOneGoal` :: [((Int, Int), Int)] -> [String]
111 encodeOneGoal` [] = []
112 encodeOneGoal` [((x, y), b):xs] = [
113 "b" <+ b <+ ".x = " <+ x <+ " & " <+
114 "b" <+ b <+ ".y = " <+ y:encodeOneGoal` xs]
116 encodeBoxOnBoxes :: [Int] -> String
117 encodeBoxOnBoxes [] = ""
118 encodeBoxOnBoxes [b] = ""
119 encodeBoxOnBoxes [b:bs] = "INVAR " <+ encodeBoxOnBox b bs <+ ";\n" <+
122 encodeBoxOnBox :: Int [Int] -> String
123 encodeBoxOnBox x bs = join " & " ["!(b" <+ x <+ ".x=b" <+ b <+ ".x &" <+
124 "b" <+ x <+ ".y=b" <+ b <+ ".y)"\\b<-bs]
126 encodeAgentNotOnBox :: [Int] -> String
127 encodeAgentNotOnBox bs = join " &\n\t" [
128 "!(b" <+ i <+ ".x = agent.x & b" <+ i <+ ".y = agent.y)"\\i<-bs]
130 encodeObMovement :: String -> String
131 encodeObMovement s = "TRANS next(" <+ s <+ ".x) = " <+ s <+ ".x + dx;\n" <+
132 "TRANS next(" <+ s <+ ".y) = " <+ s <+ ".y + dy;"
134 encodeObPosition :: [(Int, Int)] -> String
135 encodeObPosition p = join " |\n\t" [forThisX x p\\x<-removeDup $ map fst p]
137 forThisX :: Int [(Int, Int)] -> String
138 forThisX cx p = "(x=" <+ cx <+ " & (" <+
139 join " | " ["y=" <+ y \\(x, y)<-p | x == cx] <+ "))"
141 encodeBoxMovement :: [Int] -> String
142 encodeBoxMovement bs = join "\n" $ map ebm bs
145 ebm i = "TRANS next(b" <+ i <+ ".x) = case\n" <+
146 "\t\tnext(agent.x) = b" <+ i <+ ".x & " <+
147 "next(agent.y) = b" <+ i <+ ".y: b" <+ i <+ ".x + dx;\n" <+
148 "\t\tTRUE: b" <+ i <+ ".x;\n" <+
150 "TRANS next(b" <+ i <+ ".y) = case\n" <+
151 "\t\tnext(agent.x) = b" <+ i <+ ".x & " <+
152 "next(agent.y) = b" <+ i <+ ".y: b" <+ i <+ ".y + dy;\n" <+
153 "\t\tTRUE: b" <+ i <+ ".y;\n" <+