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" [
27 "MODULE ob(ix, iy, movement)",
29 "\tx: 0 .. " <+ maxX <+ ";",
30 "\ty: 0 .. " <+ maxX <+ ";",
32 "INVAR " <+ encodeObjectPositions legalPos <+ ";",
40 "\tmovement: {left, up, right, down, finished};",
41 "\tagent: " <+ encodeAgent annot,
46 "\t\tmovement = left : -1;",
47 "\t\tmovement = right: +1;",
51 "\t\tmovement = up : -1;",
52 "\t\tmovement = down: +1;",
56 "INVAR (" <+ encodeGoalState (indexList boxes) targetPos <+
57 ") <-> movement = finished;",
58 "INVAR " <+ encodeAgentNotOnBox (indexList boxes) <+ ";",
59 "INVAR " <+ encodeBoxesNotOnBox (indexList boxes),
60 "TRANS next(agent.x) = agent.x + dx;",
61 "TRANS next(agent.y) = agent.y + dy;",
62 encodeBlockMovement (indexList boxes),
63 "CTLSPEC ! EF (movement = finished)",
67 targetPos = getTargets annot
68 boxes = getBoxes annot
69 legalPos = legalPositions annot
71 (maxX, maxY) = getMetrics annot
73 //THIS IS NAIVE AND SHOULD BE IMPROVED
74 legalPositions :: AnnotatedSokoban -> [(Int, Int)]
75 legalPositions p = [(x, y)\\(x, y, t)<-p | case t of Wall=False; _=True]
77 annotate :: SokobanPuzzle -> AnnotatedSokoban
78 annotate (Sokoban p) = flatten [[(x, y, t)\\t<-r & x<-[0..]]\\r<-p & y<-[0..]]
80 getTargets :: AnnotatedSokoban -> [(Int, Int)]
81 getTargets p = [(x, y)\\(x, y, t)<-p |
82 case t of Target=True;TargetBox=True;TargetAgent=True;_=False]
84 getMetrics :: AnnotatedSokoban -> (Int, Int)
85 getMetrics p = (maximum (map fst3 p),maximum (map snd3 p))
87 getBoxes :: AnnotatedSokoban -> [(Int, Int)]
88 getBoxes p = [(x, y)\\(x, y, Box)<-p] ++ [(x, y)\\(x, y, TargetBox)<-p]
90 (<+) infixr 5 :: a b -> String | toString a & toString b
91 (<+) a b = toString a +++ toString b
93 encodeGoalState :: [Int] [(Int, Int)] -> String
94 encodeGoalState boxes targets = join " |\n\t" $ map encodeOneGoal boxtargets
96 boxtargets = map (zip2 targets) (permutations boxes)
98 encodeOneGoal :: [((Int, Int), Int)] -> String
99 encodeOneGoal p = "(" <+ join " & " (encodeOneGoal` p) <+ ")"
101 encodeOneGoal` :: [((Int, Int), Int)] -> [String]
102 encodeOneGoal` [] = []
103 encodeOneGoal` [((x, y), b):xs] = [
104 "b" <+ b <+ ".x = " <+ x <+ " & " <+
105 "b" <+ b <+ ".y = " <+ y:encodeOneGoal` xs]
108 encodeBlockMovement :: [Int] -> String
109 encodeBlockMovement bs = join "\n" $ map ebm bs
113 "TRANS next(b" <+ i <+ ".x) = case\n" <+
114 "\t\tnext(agent.x) != b" <+ i <+ ".x | " <+
115 "next(agent.y) != b" <+ i <+ ".y: b" <+ i <+ ".x;\n" <+
116 "\t\tTRUE: b" <+ i <+ ".x + dx;\n" <+
118 "TRANS next(b" <+ i <+ ".y) = case\n" <+
119 "\t\tnext(agent.x) != b" <+ i <+ ".x | " <+
120 "next(agent.y) != b" <+ i <+ ".y: b" <+ i <+ ".x;\n" <+
121 "\t\tTRUE: b" <+ i <+ ".y + dy;\n" <+
125 encodeBoxesNotOnBox :: [Int] -> String
126 encodeBoxesNotOnBox _ = "TRUE;"
128 encodeAgentNotOnBox :: [Int] -> String
129 encodeAgentNotOnBox bs = join " &\n\t" [
130 "(b" <+ i <+ ".x != agent.x & b" <+ i <+ ".y != agent.y)"\\i<-bs]
132 encodeObjectPositions :: [(Int, Int)] -> String
133 encodeObjectPositions p = join " | " ["x="<+x<+" & "<+"y="<+y\\(x, y)<-p]
135 encodeAgent :: AnnotatedSokoban -> String
136 encodeAgent [x:xs] = case x of
137 (x, y, Agent) = "ob(" <+ x <+ "," <+ y <+ ", movement);"
138 (x, y, TargetAgent) = "ob(" <+ x <+ "," <+ y <+ ", movement);"
141 encodeBoxes :: [(Int, Int)] -> String
142 encodeBoxes p = join "\n"
143 ["\tb" <+ i <+ ": ob(" <+ bx <+ ", " <+ by <+ ", movement);"
144 \\(bx, by)<-p & i<-[0..]]