coord solution (unfinished)

diff --git a/code/SokobanCoord.icl b/code/SokobanCoord.icl
new file mode 100644 (file)
index 0000000..0cce0c4
--- /dev/null
+++ b/code/SokobanCoord.icl
@@ -0,0 +1,153 @@
+module SokobanCoord
+
+import StdList, StdInt, StdChar, StdMisc, StdClass, StdString, StdFile, StdArray, StdTuple, Data.Maybe, Data.Map, Control.Monad, Data.Tuple, Data.Void
+
+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]]
+
+size :: (Int, Int)
+size = (4,5)
+
+checkX :: Int -> Int
+checkX x = if (x > length (hd puzzle)) (-1) x
+
+checkY :: Int -> Int
+checkY y = if (y > length puzzle) (-1) y
+
+/*
+  next(x2_2) := case
+    x2_2 = Wall: Wall;
+
+    x2_2 = Free & x2_3 = Agent & move = Left: Agent;
+    x2_2 = Free & x3_2 = Agent & move = Up: Agent;
+    x2_2 = Free & x2_1 = Agent & move = Right : Agent;
+    x2_2 = Free & x1_2 = Agent & move = Down : Agent;
+
+    x2_2 = Free & x2_3 = Box & x2_4 = Agent & move = Left: Box;
+    x2_2 = Free & x3_2 = Box & x4_2 = Agent & move = Up: Box;
+    x2_2 = Free & x2_1 = Box & x2_0 = Agent & move = Right : Box;
+    x2_2 = Free & x1_2 = Box & x0_2 = Agent & move = Down : Box;
+
+    x2_2 = Agent & (x2_3 = Free | x2_3 = Target) & move = Right: Free;
+    x2_2 = Agent & (x3_2 = Free | x3_2 = Target) & move = Down: Free;
+    x2_2 = Agent & (x2_1 = Free | x2_1 = Target) & move = Left : Free;
+    x2_2 = Agent & (x1_2 = Free | x1_2 = Target) & move = Up : Free;
+
+    x2_2 = Box & x2_3 = Agent & (x2_1 = Free | x2_1 = Target) & move = Left: Agent;
+    x2_2 = Box & x3_2 = Agent & (x1_2 = Free | x1_2 = Target) & move = Up: Agent;
+    x2_2 = Box & x2_1 = Agent & (x2_3 = Free | x2_3 = Target) & move = Right : Agent;
+    x2_2 = Box & x1_2 = Agent & (x3_2 = Free | x3_2 = Target) & move = Down : Agent;
+
+    x2_2 = Target & x2_3 = Agent & move = Left: AgentOnTarget;
+    x2_2 = Target & x3_2 = Agent & move = Up: AgentOnTarget;
+    x2_2 = Target & x2_1 = Agent & move = Right : AgentOnTarget;
+    x2_2 = Target & x1_2 = Agent & move = Down : AgentOnTarget;
+
+    x2_2 = Target & x2_3 = Box & x2_4 = Agent & move = Left: BoxOnTarget;
+    x2_2 = Target & x3_2 = Box & x4_2 = Agent & move = Up: BoxOnTarget;
+    x2_2 = Target & x2_1 = Box & x2_0 = Agent & move = Right : BoxOnTarget;
+    x2_2 = Target & x1_2 = Box & x0_2 = Agent & move = Down : BoxOnTarget;
+
+    x2_2 = AgentOnTarget & (x2_3 = Free | x2_3 = Target) & move = Right: Target;
+    x2_2 = AgentOnTarget & (x3_2 = Free | x3_2 = Target) & move = Down: Target;
+    x2_2 = AgentOnTarget & (x2_1 = Free | x2_1 = Target) & move = Left : Target;
+    x2_2 = AgentOnTarget & (x1_2 = Free | x1_2 = Target) & move = Up : Target;
+
+    x2_2 = BoxOnTarget & x2_3 = Agent & (x2_1 = Free | x2_1 = Target) & move = Left: AgentOnTarget;
+    x2_2 = BoxOnTarget & x3_2 = Agent & (x1_2 = Free | x1_2 = Target) & move = Up: AgentOnTarget;
+    x2_2 = BoxOnTarget & x2_1 = Agent & (x2_3 = Free | x2_3 = Target) & move = Right : AgentOnTarget;
+    x2_2 = BoxOnTarget & x1_2 = Agent & (x3_2 = Free | x3_2 = Target) & move = Down : AgentOnTarget;
+
+    TRUE : x2_2;
+  esac;
+
+*/
+
+genCoord :: Int Int -> [String]
+genCoord 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 (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 (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 (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 +++ " = 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 (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 (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",
+                "    TRUE : x" +++ toString x +++ "_" +++ toString y +++ ";\n",
+                "  esac;\n"
+                ]
+
+/*
+genAll :: SokobanPuzzle -> [[String]]
+genAll p = [\\]
+genAll [x:xs] = []
+*/
+
+contains :: Char String -> Bool
+contains char str = not (isEmpty [c\\c<-:str | char == c])
+
+readLines :: File -> [String]
+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 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 = flatten [filter (\x -> not (contains '-' x)) (genCoord x y) \\ x <- [0..4], y <- [0..5]]