module SocobanCoord
import StdList, StdInt, StdChar, StdMisc, StdClass, StdString, StdFile, StdArray, StdTuple, Data.Maybe, Data.Map, Control.Monad, Data.Tuple, Data.Void
+import Sokoban
inputfile :== "screen.1"
outputfile :== "solver.smv"
-:: SokobanPuzzle :== [[SokobanTile]]
-:: SokobanTile = Wall | Free | Box | Target | Agent
-
puzzle :: SokobanPuzzle
-puzzle = [[Wall, Wall, Wall, Wall, Wall, Wall],
- [Wall, Free, Free, Free, Free, Wall],
- [Wall, Agent,Free, Box, Free, Wall],
- [Wall, Free, Free, Free, Target, Wall],
- [Wall, Wall, Wall, Wall, Wall, Wall]]
-
+puzzle = Sokoban [[Wall, Wall, Wall, Wall, Wall, Wall],
+ [Wall, Free, Free, Free, Free, Wall],
+ [Wall, Agent,Free, Box, Free, Wall],
+ [Wall, Free, Free, Free, Target, Wall],
+ [Wall, Wall, Wall, Wall, Wall, Wall]]
+
+fromTile :: SokobanTile -> String
+fromTile Wall = "Wall"
+fromTile Free = "Free"
+fromTile Box = "Box"
+fromTile Target = "Target"
+fromTile Agent = "Agent"
+fromTile TargetAgent = "AgentOnTarget"
+fromTile TargetBox = "BoxOnTarget"
checkX :: Int -> Int
-checkX x = if (x > length (hd puzzle)) (-1) x
+checkX x = let (Sokoban p) = puzzle in if (x > length (hd p)) (-1) x
checkY :: Int -> Int
-checkY y = if (y > length puzzle) (-1) y
+checkY y = let (Sokoban p) = puzzle in if (y > length p) (-1) y
+
+genField :: SokobanPuzzle -> [String]
+genField p = let (Sokoban pzl) = p in genField` pzl 0 0 []
+where
+ genField` :: [[SokobanTile]] Int Int [String] -> [String]
+ genField` p i j rs
+ | i+1 == length (hd p) = rs
+ | j == (length p) = genField` p (i+1) 0 [" init(x" +++ toString i +++ "_" +++ toString j +++ ") := " +++ fromTile ((p !! i) !! j) +++ ";\n": rs]
+ | otherwise = genField` p i (j+1) [" init(x" +++ toString i +++ "_" +++ toString j +++ ") := " +++ fromTile ((p !! i) !! j) +++ ";\n": rs]
genVars :: Int Int -> [String]
genVars x y = genVars` x y 0 0 []
| (a+1) == x = res
| b == y = genVars` a b (x+1) 0 [" x" +++ toString x +++ "_" +++ toString y +++ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};\n":res]
| otherwise = genVars` a b x (y+1) [" x" +++ toString x +++ "_" +++ toString y +++ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};\n":res]
-
+
genCoord :: Int Int -> [String]
genCoord x y = [" next(x" +++ toString x +++ "_" +++ toString y +++ ") := case\n",
" x" +++ toString x +++ "_" +++ toString y +++ " = Wall: Wall;\n",
]
genAll :: [String]
-genAll = [
+genAll = let (Sokoban p) = puzzle in
+ [
"MODULE main\n",
"VAR\n"
- ]
- ++ genVars ((length puzzle) - 1) ((length (hd puzzle)) - 1)
+ ]
+ ++ genVars ((length p) - 1) ((length (hd p)) - 1)
++ [
- "ASSIGN",
- "init(x0_0) := Wall;", //currently just a stub
- "init(x0_1) := Wall;",
- "init(x0_2) := Wall;",
- "init(x0_3) := Wall;",
- "init(x0_4) := Wall;",
- "init(x0_5) := Wall;",
- "init(x1_0) := Wall;",
- "init(x1_1) := Free;",
- "init(x1_2) := Free;",
- "init(x1_3) := Free;",
- "init(x1_4) := Free;",
- "init(x1_5) := Wall;",
- "init(x2_0) := Wall;",
- "init(x2_1) := Agent;",
- "init(x2_2) := Free;",
- "init(x2_3) := Box;",
- "init(x2_4) := Free;",
- "init(x2_5) := Wall;",
- "init(x3_0) := Wall;",
- "init(x3_1) := Free;",
- "init(x3_2) := Free;",
- "init(x3_3) := Free;",
- "init(x3_4) := Target;",
- "init(x3_5) := Wall;",
- "init(x4_0) := Wall;",
- "init(x4_1) := Wall;",
- "init(x4_2) := Wall;",
- "init(x4_3) := Wall;",
- "init(x4_4) := Wall;",
- "init(x4_5) := Wall;",
- "init(move) := {Up, Down, Left, Right};"
+ " ASSIGN\n",
+ " init(move) := {Up, Down, Left, Right};\n"
]
+ ++ genField puzzle
++ flatten [filter (\x -> not (contains '-' x)) (genCoord x y) \\ x <- [0..4], y <- [0..5]]
contains :: Char String -> Bool
| sfend file = []
# (line, file) = sfreadline file
| otherwise = [line: readLines file]
-
+
writeLines :: [String] *File -> *File
writeLines [] file = file
writeLines [l:ls] file = writeLines ls (file <<< l)
-
-openInpFile :: *World String -> (File, *World)
+
+openInpFile :: *World String -> (File, *World)
openInpFile world path
# (ok, file, world) = sfopen path 0 world
| not ok = abort "Error reading the file."
= (file, world)
-
+
openOutFile :: *World String -> (*File, *World)
openOutFile world path
# (ok, file, world) = fopen path 1 world
| not ok = abort "Can not write to a file."
= (file, world)
-
+
closeFile :: *World *File -> (Bool, *World)
closeFile world file
# world = fclose file world
= world
-
-Start = genAll
+
+Start = genAll
\ No newline at end of file