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 "INVAR " <+ encodeBoxOnBoxes boxnums <+ ";",
46 "INVAR " <+ encodeGoalState boxnums targetPos <+ ";",
48 encodeObMovement "agent",
50 encodeBoxMovement boxnums,
51 "CTLSPEC ! EF (movement = finished);",
55 targetPos = getTargets annot
56 boxes = getBoxes annot
57 boxnums = indexList boxes
58 agent = hd $ getAgents annot
59 legalPos = legalPositions annot
61 (maxX, maxY) = getMetrics annot
63 declareObject :: (Int, Int) -> String
64 declareObject (x, y) = "ob(" <+ x <+ ", " <+ y <+ ");"
67 deltaDefine = join "\n" [
69 "\t\tmovement = left : -1;",
70 "\t\tmovement = right: +1;",
74 "\t\tmovement = up : -1;",
75 "\t\tmovement = down: +1;",
79 //THIS IS NAIVE AND SHOULD BE IMPROVED
80 legalPositions :: AnnotatedSokoban -> [(Int, Int)]
81 legalPositions p = [(x, y)\\(x, y, t)<-p | case t of Wall=False; _=True]
83 annotate :: SokobanPuzzle -> AnnotatedSokoban
84 annotate (Sokoban p) = flatten [[(x, y, t)\\t<-r & x<-[0..]]\\r<-p & y<-[0..]]
86 getTargets :: AnnotatedSokoban -> [(Int, Int)]
87 getTargets p = [(x, y)\\(x, y, t)<-p |
88 case t of Target=True;TargetBox=True;TargetAgent=True;_=False]
90 getMetrics :: AnnotatedSokoban -> (Int, Int)
91 getMetrics p = (maximum (map fst3 p),maximum (map snd3 p))
93 getAgents :: AnnotatedSokoban -> [(Int, Int)]
94 getAgents p = [(x, y)\\(x, y, Agent)<-p] ++ [(x, y)\\(x, y, TargetAgent)<-p]
96 getBoxes :: AnnotatedSokoban -> [(Int, Int)]
97 getBoxes p = [(x, y)\\(x, y, Box)<-p] ++ [(x, y)\\(x, y, TargetBox)<-p]
99 (<+) infixr 5 :: a b -> String | toString a & toString b
100 (<+) a b = toString a +++ toString b
102 encodeGoalState :: [Int] [(Int, Int)] -> String
103 encodeGoalState boxes targets = "(" <+
104 join " |\n\t" (map encodeOneGoal boxtargets) <+ ")<->movement=finished"
106 boxtargets = map (zip2 targets) (permutations boxes)
108 encodeOneGoal :: [((Int, Int), Int)] -> String
109 encodeOneGoal p = "(" <+ join " & " (encodeOneGoal` p) <+ ")"
111 encodeOneGoal` :: [((Int, Int), Int)] -> [String]
112 encodeOneGoal` [] = []
113 encodeOneGoal` [((x, y), b):xs] = [
114 "b" <+ b <+ ".x = " <+ x <+ " & " <+
115 "b" <+ b <+ ".y = " <+ y:encodeOneGoal` xs]
117 encodeBoxOnBoxes :: [Int] -> String
118 encodeBoxOnBoxes [] = ""
119 encodeBoxOnBoxes [b] = "TRUE"
120 encodeBoxOnBoxes [b:bs] = encodeBoxOnBox b bs <+ " &\n\t" <+
123 encodeBoxOnBox :: Int [Int] -> String
124 encodeBoxOnBox x bs = join " & " ["!(b" <+ x <+ ".x=b" <+ b <+ ".x &" <+
125 "b" <+ x <+ ".y=b" <+ b <+ ".y)"\\b<-bs]
127 encodeAgentNotOnBox :: [Int] -> String
128 encodeAgentNotOnBox bs = join " &\n\t" [
129 "!(b" <+ i <+ ".x = agent.x & b" <+ i <+ ".y = agent.y)"\\i<-bs]
131 encodeObMovement :: String -> String
132 encodeObMovement s = "TRANS next(" <+ s <+ ".x) = " <+ s <+ ".x + dx & " <+
133 "next(" <+ s <+ ".y) = " <+ s <+ ".y + dy;"
135 encodeObPosition :: [(Int, Int)] -> String
136 encodeObPosition p = join " |\n\t" [forThisX x p\\x<-removeDup $ map fst p]
138 forThisX :: Int [(Int, Int)] -> String
139 forThisX cx p = "(x=" <+ cx <+ " & (" <+
140 join " | " ["y=" <+ y \\(x, y)<-p | x == cx] <+ "))"
142 encodeBoxMovement :: [Int] -> String
143 encodeBoxMovement bs = join "\n" $ map ebm bs
146 ebm i = "TRANS next(b" <+ i <+ ".x) = case\n" <+
147 "\t\tnext(agent.x) = b" <+ i <+ ".x & " <+
148 "next(agent.y) = b" <+ i <+ ".y: b" <+ i <+ ".x + dx;\n" <+
149 "\t\tTRUE: b" <+ i <+ ".x;\n" <+
151 "TRANS next(b" <+ i <+ ".y) = case\n" <+
152 "\t\tnext(agent.x) = b" <+ i <+ ".x & " <+
153 "next(agent.y) = b" <+ i <+ ".y: b" <+ i <+ ".y + dy;\n" <+
154 "\t\tTRUE: b" <+ i <+ ".y;\n" <+