coord generator update

diff --git a/code/SokobanCoord.icl b/code/SokobanCoord.icl
index db780cc..4a664ad 100644 (file)
--- a/code/SokobanCoord.icl
+++ b/code/SokobanCoord.icl
@@ -1,103 +1,93 @@
-module SocobanCoord
+module SokobanCoord
 
 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"
+inpath  :== "screen.2000"
+outpath :== "solver.smv"
 
 puzzle :: SokobanPuzzle
-puzzle = Sokoban [[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 :: [[SokobanTile]] Int -> Int
+checkX p x = let (Sokoban p) = puzzle in if (x > (length p - 1)) (-1) x
 
-checkX :: Int -> Int
-checkX x = let (Sokoban p) = puzzle in if (x > length (hd p)) (-1) x
-
-checkY :: Int -> Int
-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 []
-where
-  genVars` :: Int Int Int Int [String] -> [String]
-  genVars` a b x y res
-    | (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",
+checkY :: [[SokobanTile]] Int Int -> Int
+checkY p x y = let (Sokoban p) = puzzle in if (y > (length (p !! x) - 1)) (-1) y
+
+genField :: [[SokobanTile]] Int Int -> String
+genField p x y = "    init(x" +++ toString x +++ "_" +++ toString y +++ ") := " +++ fromTile ((p !! x) !! y) +++ ";\n"
+    
+genVars :: Int Int -> String
+genVars x y = "    x" +++ toString x +++ "_" +++ toString y +++ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};\n"
+
+genCoord :: [[SokobanTile]] Int Int -> [String]
+genCoord p x y = ["  next(x" +++ toString x +++ "_" +++ toString y +++ ") := case\n",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Wall: Wall;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Agent & move = Left: Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: Agent;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent & move = Left: Agent;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: Agent;\n",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & move = Right : Agent;\n",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & move = Down : Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Box & x" +++ toString x +++ "_" +++ toString (checkY (y+2)) +++ " = Agent & move = Left: Box;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX (x+2)) +++ "_" +++ toString x +++ " = Agent & move = Up: Box;\n",
+                "    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",
+                "    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",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Box & x" +++ toString x +++ "_" +++ toString (x-2) +++ " = Agent & move = Right : Box;\n",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-2) +++ "_" +++ toString y +++ " = Agent & move = Down : Box;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Target) & move = Right: Free;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Free | x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Target) & move = Down: Free;\n",
+                "    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",
+                "    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",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left : Free;\n",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (x-1) +++ "_" +++ toString y +++ "= Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up : Free;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left: Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up: Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Target) & move = Right : Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Free | x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Target) & move = Down : Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Agent & move = Left: AgentOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: AgentOnTarget;\n",
+                "    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",
+                "    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",
+                "    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",
+                "    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",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent & move = Left: AgentOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: AgentOnTarget;\n",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & move = Right : AgentOnTarget;\n",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & move = Down : AgentOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Box & x" +++ toString x +++ "_" +++ toString (checkY (y+2)) +++ " = Agent & move = Left: BoxOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX (x+2)) +++ "_" +++ toString y +++ " = Agent & move = Up: BoxOnTarget;\n",
+                "    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",
+                "    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",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Box & x" +++ toString x +++ "_" +++ toString (y-2) +++ " = Agent & move = Right : BoxOnTarget;\n",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-2) +++ "_" +++ toString y +++ " = Agent & move = Down : BoxOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Target) & move = Right: Target;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Free | x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Target) & move = Down: Target;\n",
+                "    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",
+                "    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",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left : Target;\n",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up : Target;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left: AgentOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up: AgentOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Target) & move = Right : AgentOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Free | x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Target) & move = Down : AgentOnTarget;\n",
+                "    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",
+                "    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",
+                "    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",
+                "    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",
                 "    TRUE : x" +++ toString x +++ "_" +++ toString y +++ ";\n",
                 "  esac;\n"
                 ]
 
-genAll :: [String]
-genAll = let (Sokoban p) = puzzle in
+fromTile :: SokobanTile -> String
+fromTile Wall = "Wall"
+fromTile Free = "Free"
+fromTile Box = "Box"
+fromTile Target = "Target"
+fromTile Agent = "Agent"
+fromTile TargetAgent = "AgentOnTarget"
+fromTile TargetBox = "BoxOnTarget"
+
+genAll :: SokobanPuzzle -> [String]
+genAll puzzle = let (Sokoban p) = puzzle in
          [
           "MODULE main\n",
           "VAR\n"
-          ] 
-      ++ genVars ((length p) - 1) ((length (hd p)) - 1)
+          ]
+      ++ [genVars x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
+      ++ ["    move : {Up, Down, Left, Right};\n"]
       ++ [
           "  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]]
+      ++ [genField p x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
+      ++ flatten [filter (\x -> not (contains '-' x)) (genCoord p x y) \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
+      ++ ["  next(move) := {Up, Down, Left, Right};\n"]
 
 contains :: Char String -> Bool
 contains char str = not (isEmpty [c\\c<-:str | char == c])
@@ -107,26 +97,34 @@ readLines file
   | 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 
\ No newline at end of file
+
+
+Start :: *World -> *World
+Start w
+  # (p, w) = parse inpath w
+  # s = genAll p
+  # (f, w) = openOutFile w outpath
+  # f = writeLines s f
+  # (ok, w) = closeFile w f
+  = w