3 import StdList, StdInt, StdBool, StdChar, StdMisc, StdClass, StdString, StdFile, StdArray, StdTuple, Data.Maybe, Data.Map, Data.Tuple, Data.Void
4 from Text import class Text(concat,join), instance Text String
7 inpath :== "screen.2001"
8 outpath :== "solver.smv"
10 (<+) infixr 5 :: a b -> String | toString a & toString b
11 (<+) a b = toString a +++ toString b
13 checkX :: [[SokobanTile]] Int -> Int
14 checkX p x = if (x > (length p - 1)) (-1) x
16 checkY :: [[SokobanTile]] Int Int -> Int
18 | ((x < 0) || (x > (length p - 1))) = -1
19 | otherwise = if (y > (length (p !! x) - 1)) (-1) y
21 genField :: [[SokobanTile]] Int Int -> String
22 genField p x y = " init(x" <+ x <+ "_" <+ y <+ ") := " <+ fromTile ((p !! x) !! y) <+ ";"
24 genVars :: Int Int -> String
25 genVars x y = " x" <+ x <+ "_" <+ y <+ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};"
27 genCoord :: [[SokobanTile]] Int Int -> [String]
28 genCoord p x y = [" next(x" <+ x <+ "_" <+ y <+ ") := case",
29 " x" <+ x <+ "_" <+ y <+ " = Wall: Wall;",
30 " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Agent | x"
31 <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = AgentOnTarget) & move = Left: Agent;",
32 " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
33 <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & move = Up: Agent;",
34 " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
35 <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & move = Right : Agent;",
36 " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
37 <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & move = Down : Agent;",
39 " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Box | x"
40 <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = BoxOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = Agent | x"
41 <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = AgentOnTarget) & move = Left: Box;",
42 " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Box | x"
43 <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = BoxOnTarget) & (x" <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = Agent | x"
44 <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = AgentOnTarget) & move = Up: Box;",
45 " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Box | x"
46 <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = BoxOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = Agent | x"
47 <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = AgentOnTarget) & move = Right : Box;",
48 " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Box | x"
49 <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = BoxOnTarget) & (x" <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = Agent | x"
50 <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = AgentOnTarget) & move = Down : Box;",
52 " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Target) & move = Right: Free;",
53 " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p x y) <+ " = Target) & move = Down: Free;",
54 " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left : Free;",
55 " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ "= Free | x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Target) & move = Up : Free;",
57 " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Box | x"
58 <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = BoxOnTarget) & (x"
59 <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = Target) & move = Right: Free;",
60 " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p x y) <+ " = Box | x"
61 <+ (checkX p (x+1)) <+ "_" <+ (checkY p x y) <+ " = BoxOnTarget) & (x"
62 <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = Free | x" <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = Target) & move = Down: Free;",
63 " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Box | x"
64 <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = BoxOnTarget) & (x"
65 <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = Target) & move = Left: Free;",
66 " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Box | x"
67 <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = BoxOnTarget) & (x"
68 <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = Free | x" <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = Target) & move = Up: Free;",
70 " x" <+ x <+ "_" <+ y <+ " = Box & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Agent | x"
71 <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left: Agent;",
72 " x" <+ x <+ "_" <+ y <+ " = Box & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
73 <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & (x" <+ (x-1) <+ "_" <+ (checkY p (x-1) y) <+ " = Free | x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Target) & move = Up: Agent;",
74 " x" <+ x <+ "_" <+ y <+ " = Box & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
75 <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Target) & move = Right : Agent;",
76 " x" <+ x <+ "_" <+ y <+ " = Box & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
77 <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p x y) <+ " = Target) & move = Down : Agent;",
79 " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Agent | x"
80 <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = AgentOnTarget) & move = Left: AgentOnTarget;",
81 " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
82 <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & move = Up: AgentOnTarget;",
83 " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
84 <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & move = Right : AgentOnTarget;",
85 " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
86 <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & move = Down : AgentOnTarget;",
88 " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Box | x"
89 <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = BoxOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = Agent | x"
90 <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = AgentOnTarget) & move = Left: BoxOnTarget;",
91 " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Box | x"
92 <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = BoxOnTarget) & (x" <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = Agent | x"
93 <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = AgentOnTarget) & move = Up: BoxOnTarget;",
94 " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Box | x"
95 <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = BoxOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = Agent | x"
96 <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = AgentOnTarget) & move = Right : BoxOnTarget;",
97 " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Box | x"
98 <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = BoxOnTarget) & (x" <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = Agent | x"
99 <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = AgentOnTarget) & move = Down : BoxOnTarget;",
101 " x" <+ x <+ "_" <+ y <+ " = AgentOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Target) & move = Right: Target;",
102 " x" <+ x <+ "_" <+ y <+ " = AgentOnTarget & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Target) & move = Down: Target;",
103 " x" <+ x <+ "_" <+ y <+ " = AgentOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left : Target;",
104 " x" <+ x <+ "_" <+ y <+ " = AgentOnTarget & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Free | x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Target) & move = Up : Target;",
106 " x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Agent | x"
107 <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left: AgentOnTarget;",
108 " x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
109 <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Free | x" <+ (checkX p (x-1)) <+ "_"
110 <+ (checkY p (x-1) y) <+ " = Target) & move = Up: AgentOnTarget;",
111 " x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
112 <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Free | x" <+ x <+ "_" <+ (checkY p x (y+1)) <+ " = Target) & move = Right : AgentOnTarget;",
113 " x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
114 <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_"
115 <+ (checkY p (x+1) y) <+ " = Target) & move = Down : AgentOnTarget;",
117 " TRUE : x" <+ x <+ "_" <+ y <+ ";",
121 instance == SokobanTile
123 (==) Wall Wall = True
124 (==) Free Free = True
126 (==) Agent Agent = True
127 (==) Target Target = True
128 (==) TargetBox TargetBox = True
129 (==) TargetAgent TargetAgent = True
132 fromTile :: SokobanTile -> String
133 fromTile Wall = "Wall"
134 fromTile Free = "Free"
136 fromTile Target = "Target"
137 fromTile Agent = "Agent"
138 fromTile TargetAgent = "AgentOnTarget"
139 fromTile TargetBox = "BoxOnTarget"
141 genCond :: [[SokobanTile]] Int Int -> String
143 | x < 0 || y < 0 || x > (length p) - 1 = ""
145 | y > (length (p !! x) - 1) = ""
146 | otherwise = if ((p !! x) !! y == Target) ("x" <+ x <+ "_" <+ y <+ " = BoxOnTarget") ""
148 addLogic :: [String] -> [String]
151 addLogic [x:xs] = [x <+ " & ": addLogic xs]
153 genAll :: SokobanPuzzle -> String
154 genAll puzzle = let (Sokoban p) = puzzle in
159 , join "\n" [genVars x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
160 ," move : {Up, Down, Left, Right};"
162 ," init(move) := {Up, Down, Left, Right};"
163 ,join "\n" [genField p x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
164 ,join "\n" (flatten [filter (\x -> not (contains '-' x)) (genCoord p x y) \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]])
165 ," next(move) := {Up, Down, Left, Right};"
167 ,join "\n" (addLogic (filter (\x -> x <> "" ) [genCond p x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]))
170 contains :: Char String -> Bool
171 contains char str = not (isEmpty [c\\c<-:str | char == c])
173 readLines :: File -> [String]
176 # (line, file) = sfreadline file
177 | otherwise = [line: readLines file]
179 writeLines :: [String] *File -> *File
180 writeLines [] file = file
181 writeLines [l:ls] file = writeLines ls (file <<< l)
183 openInpFile :: *World String -> (File, *World)
184 openInpFile world path
185 # (ok, file, world) = sfopen path 0 world
186 | not ok = abort "Error reading the file."
189 openOutFile :: *World String -> (*File, *World)
190 openOutFile world path
191 # (ok, file, world) = fopen path 1 world
192 | not ok = abort "Can not write to a file."
195 closeFile :: *World *File -> (Bool, *World)
197 # world = fclose file world
200 Start :: *World -> *World
202 # (p, w) = parse inpath w
204 # (f, w) = openOutFile w outpath
206 # (ok, w) = closeFile w f