3 import StdList, StdInt, StdChar, StdMisc, StdClass, StdString, StdFile, StdArray, StdTuple, Data.Maybe, Data.Map, Control.Monad, Data.Tuple, Data.Void
6 inpath :== "screen.2000"
7 outpath :== "solver.smv"
10 puzzle :: SokobanPuzzle
11 puzzle = Sokoban [[Wall, Wall, Wall, Wall, Wall, Wall],
12 [Wall, Free, Free, Free, Free, Wall],
13 [Wall, Agent,Free, Box, Free, Wall],
14 [Wall, Free, Free, Free, Target, Wall],
15 [Wall, Wall, Wall, Wall, Wall, Wall]]
18 checkX :: [[SokobanTile]] Int -> Int
19 checkX p x = if (x > (length p - 1)) (-1) x
21 checkY :: [[SokobanTile]] Int Int -> Int
22 checkY p x y = if (y > (length (p !! x) - 1)) (-1) y
24 genField :: [[SokobanTile]] Int Int -> String
25 genField p x y = " init(x" +++ toString x +++ "_" +++ toString y +++ ") := " +++ fromTile ((p !! x) !! y) +++ ";\n"
27 genVars :: Int Int -> String
28 genVars x y = " x" +++ toString x +++ "_" +++ toString y +++ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};\n"
30 genCoord :: [[SokobanTile]] Int Int -> [String]
31 genCoord p x y = [" next(x" +++ toString x +++ "_" +++ toString y +++ ") := case\n",
32 " x" +++ toString x +++ "_" +++ toString y +++ " = Wall: Wall;\n",
33 " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (checkY p x (y+1)) +++ " = Agent & move = Left: Agent;\n",
34 " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: Agent;\n",
35 " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & move = Right : Agent;\n",
36 " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & move = Down : Agent;\n",
37 " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (checkY p x (y+1)) +++ " = Box & x" +++ toString x +++ "_" +++ toString (checkY p x (y+2)) +++ " = Agent & move = Left: Box;\n",
38 " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX p (x+2)) +++ "_" +++ toString x +++ " = Agent & move = Up: Box;\n",
39 " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Box & x" +++ toString x +++ "_" +++ toString (x-2) +++ " = Agent & move = Right : Box;\n",
40 " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-2) +++ "_" +++ toString y +++ " = Agent & move = Down : Box;\n",
41 " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (checkY p x (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY p x (y+1)) +++ " = Target) & move = Right: Free;\n",
42 " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Target) & move = Down: Free;\n",
43 " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left : Free;\n",
44 " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (x-1) +++ "_" +++ toString y +++ "= Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up : Free;\n",
45 " x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString x +++ "_" +++ toString (checkY p x (y+1)) +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left: Agent;\n",
46 " x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up: Agent;\n",
47 " x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (checkY p x (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY p x (y+1)) +++ " = Target) & move = Right : Agent;\n",
48 " x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Target) & move = Down : Agent;\n",
49 " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (checkY p x (y+1)) +++ " = Agent & move = Left: AgentOnTarget;\n",
50 " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: AgentOnTarget;\n",
51 " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & move = Right : AgentOnTarget;\n",
52 " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & move = Down : AgentOnTarget;\n",
53 " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (checkY p x (y+1)) +++ " = Box & x" +++ toString x +++ "_" +++ toString (checkY p x (y+2)) +++ " = Agent & move = Left: BoxOnTarget;\n",
54 " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX p (x+2)) +++ "_" +++ toString y +++ " = Agent & move = Up: BoxOnTarget;\n",
55 " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Box & x" +++ toString x +++ "_" +++ toString (y-2) +++ " = Agent & move = Right : BoxOnTarget;\n",
56 " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-2) +++ "_" +++ toString y +++ " = Agent & move = Down : BoxOnTarget;\n",
57 " x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString x +++ "_" +++ toString (checkY p x (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY p x (y+1)) +++ " = Target) & move = Right: Target;\n",
58 " x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Target) & move = Down: Target;\n",
59 " x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left : Target;\n",
60 " x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up : Target;\n",
61 " x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString x +++ "_" +++ toString (checkY p x (y+1)) +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left: AgentOnTarget;\n",
62 " x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up: AgentOnTarget;\n",
63 " x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (checkY p x (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY p x (y+1)) +++ " = Target) & move = Right : AgentOnTarget;\n",
64 " x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Target) & move = Down : AgentOnTarget;\n",
65 " TRUE : x" +++ toString x +++ "_" +++ toString y +++ ";\n",
69 fromTile :: SokobanTile -> String
70 fromTile Wall = "Wall"
71 fromTile Free = "Free"
73 fromTile Target = "Target"
74 fromTile Agent = "Agent"
75 fromTile TargetAgent = "AgentOnTarget"
76 fromTile TargetBox = "BoxOnTarget"
78 genAll :: SokobanPuzzle -> [String]
79 genAll puzzle = let (Sokoban p) = puzzle in
84 ++ [genVars x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
85 ++ [" move : {Up, Down, Left, Right};\n"]
88 " init(move) := {Up, Down, Left, Right};\n"
90 ++ [genField p x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
91 ++ flatten [filter (\x -> not (contains '-' x)) (genCoord p x y) \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
92 ++ [" next(move) := {Up, Down, Left, Right};\n"]
94 contains :: Char String -> Bool
95 contains char str = not (isEmpty [c\\c<-:str | char == c])
97 readLines :: File -> [String]
100 # (line, file) = sfreadline file
101 | otherwise = [line: readLines file]
103 writeLines :: [String] *File -> *File
104 writeLines [] file = file
105 writeLines [l:ls] file = writeLines ls (file <<< l)
107 openInpFile :: *World String -> (File, *World)
108 openInpFile world path
109 # (ok, file, world) = sfopen path 0 world
110 | not ok = abort "Error reading the file."
113 openOutFile :: *World String -> (*File, *World)
114 openOutFile world path
115 # (ok, file, world) = fopen path 1 world
116 | not ok = abort "Can not write to a file."
119 closeFile :: *World *File -> (Bool, *World)
121 # world = fclose file world
125 Start :: *World -> *World
127 # (p, w) = parse inpath w
129 # (f, w) = openOutFile w outpath
131 # (ok, w) = closeFile w f