X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=code%2FSokobanCoord.icl;h=db780ccfdb8b85d146523b8b9368772ae542ff08;hb=bd74997680c2ff4a2af3445050f5ed7baa041e04;hp=0cce0c4d174ceaf400fc159a6f903802cecbbdfc;hpb=ac799d3f661e5440845954ec72b80a98ca26c511;p=mc1516pa.git

diff --git a/code/SokobanCoord.icl b/code/SokobanCoord.icl
index 0cce0c4..db780cc 100644
--- a/code/SokobanCoord.icl
+++ b/code/SokobanCoord.icl
@@ -1,78 +1,51 @@
-module SokobanCoord
+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]]
-
-size :: (Int, Int)
-size = (4,5)
+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
-
-/*
-  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;
-
-*/
-
+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",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Wall: Wall;\n",
@@ -112,11 +85,19 @@ genCoord x y = ["  next(x" +++ toString x +++ "_" +++ toString y +++ ") := case\
                 "  esac;\n"
                 ]
 
-/*
-genAll :: SokobanPuzzle -> [[String]]
-genAll p = [\\]
-genAll [x:xs] = []
-*/
+genAll :: [String]
+genAll = let (Sokoban p) = puzzle in
+         [
+          "MODULE main\n",
+          "VAR\n"
+          ] 
+      ++ genVars ((length p) - 1) ((length (hd p)) - 1)
+      ++ [
+          "  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
 contains char str = not (isEmpty [c\\c<-:str | char == c])
@@ -126,28 +107,26 @@ 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 = flatten [filter (\x -> not (contains '-' x)) (genCoord x y) \\ x <- [0..4], y <- [0..5]]
+  
+Start = genAll 
\ No newline at end of file