almost finished my bit
[mc1516pa.git] / code / SokobanCoord.icl
index c082875..1c98cb8 100644 (file)
@@ -3,29 +3,9 @@ module SokobanCoord
 import StdList, StdInt, StdBool, StdChar, StdMisc, StdClass, StdString, StdFile, StdArray, StdTuple, Data.Maybe, Data.Map, Control.Monad, Data.Tuple, Data.Void
 import Sokoban
 
-inpath  :== "screen.2001"
+inpath  :== "screen.1001"
 outpath :== "solver.smv"
 
-/*
-puzzle :: SokobanPuzzle
-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]]
-*/
-
-instance == SokobanTile
-where
-  (==) Wall Wall = True
-  (==) Free Free = True
-  (==) Box Box = True
-  (==) Agent Agent = True
-  (==) Target Target = True
-  (==) TargetBox TargetBox = True
-  (==) TargetAgent TargetAgent = True
-  (==) _ _ = False
-
 checkX :: [[SokobanTile]] Int -> Int
 checkX p x = if (x > (length p - 1)) (-1) x
 
@@ -43,54 +23,108 @@ genVars x y = "    x" +++ toString x +++ "_" +++ toString y +++ " : {Wall, Free,
 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 (checkX p 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 (checkY p (x+1) y) +++ " = Agent & move = Up: Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent & move = Right : Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent & move = Down : Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Box & x" +++ toString (checkX p 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 (checkY p (x+1) y) +++ " = Box & x" +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Agent & move = Up: Box;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Box & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Agent & move = Right : Box;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Box & x" +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Agent & move = Down : Box;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent | x"
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = AgentOnTarget) & move = Left: Agent;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent | x"
+                        +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = AgentOnTarget) & move = Up: Agent;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent | x" 
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = AgentOnTarget) & move = Right : Agent;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent | x"
+                        +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = AgentOnTarget) & move = Down : Agent;\n",
+                
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Box | x"
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = BoxOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+2)) +++ " = Agent | x" 
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+2)) +++ " = AgentOnTarget) & move = Left: Box;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Box | x"
+                        +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = BoxOnTarget) & (x" +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Agent | x" 
+                        +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = AgentOnTarget) & move = Up: Box;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Box | x"
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = BoxOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Agent | x" 
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = AgentOnTarget) & move = Right : Box;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Box | x" 
+                        +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = BoxOnTarget) & (x" +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Agent | x"
+                        +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = AgentOnTarget) & move = Down : Box;\n",
+                
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Free | x" +++ toString (checkX p 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 (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = Target) & move = Down: Free;\n",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left : Free;\n",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ "= Free | x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up : Free;\n",
                 
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Box & x" 
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent &  (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Box | x"
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = BoxOnTarget) & (x" 
                         +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = Target) & move = Right: Free;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = Box & x" 
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = Box | x" 
+                        +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = BoxOnTarget) & (x" 
                         +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Free | x" +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Target) & move = Down: Free;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Box & x" 
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Box | x"
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = BoxOnTarget) & (x" 
                         +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Target) & move = Left: Free;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Box & x" 
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Box | x" 
+                        +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = BoxOnTarget) & (x" 
                         +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Free | x" +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Target) & move = Up: Free;\n",                        
                         
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left: Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent & (x" +++ toString (x-1) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Free | x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up: Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Target) & move = Right : Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = Target) & move = Down : Agent;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p 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 (checkY p (x+1) y) +++ " = Agent & move = Up: AgentOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent & move = Right : AgentOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent & move = Down : AgentOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Box & x" +++ toString (checkX p 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 (checkY p (x+1) y) +++ " = Box & x" +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Agent & move = Up: BoxOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Box & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Agent & move = Right : BoxOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Box & x" +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Agent & move = Down : BoxOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent | x"
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = AgentOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left: Agent;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent | x"
+                        +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = AgentOnTarget) & (x" +++ toString (x-1) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Free | x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up: Agent;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent | x"
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = AgentOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Target) & move = Right : Agent;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Box & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent | x"
+                        +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = AgentOnTarget) & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = Target) & move = Down : Agent;\n",
+                
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent | x"
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = AgentOnTarget) & move = Left: AgentOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent | x"
+                        +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = AgentOnTarget) & move = Up: AgentOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent | x"
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = AgentOnTarget) & move = Right : AgentOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent | x"
+                        +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = AgentOnTarget) & move = Down : AgentOnTarget;\n",
+                
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Box | x"
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = BoxOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+2)) +++ " = Agent | x"
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+2)) +++ " = AgentOnTarget) & move = Left: BoxOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Box | x"
+                        +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = BoxOnTarget) & (x" +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Agent | x"
+                        +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = AgentOnTarget) & move = Up: BoxOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Box | x" 
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = BoxOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Agent | x"
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = AgentOnTarget) & move = Right : BoxOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Box | x"
+                        +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = BoxOnTarget) & (x" +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Agent | x"
+                        +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = AgentOnTarget) & move = Down : BoxOnTarget;\n",
+                
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Free | x" +++ toString (checkX p 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 (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Target) & move = Down: Target;\n",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left : Target;\n",
                 "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Free | x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up : Target;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left: AgentOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Free | x" +++ toString (checkX p (x-1)) +++ "_" 
+                
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = Agent | x"
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x  (y+1)) +++ " = AgentOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left: AgentOnTarget;\n",
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent | x"
+                        +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = AgentOnTarget) & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Free | x" +++ toString (checkX p (x-1)) +++ "_" 
                         +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up: AgentOnTarget;\n",
-                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent & (x" +++ toString (checkX p 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 (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" 
+                "    x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent | x"
+                        +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = AgentOnTarget) & (x" +++ toString (checkX p 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 (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent | x"
+                        +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = AgentOnTarget) & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" 
                         +++ toString (checkY p (x+1) y) +++ " = Target) & move = Down : AgentOnTarget;\n",
+                        
                 "    TRUE : x" +++ toString x +++ "_" +++ toString y +++ ";\n",
                 "  esac;\n"
                 ]
 
+instance == SokobanTile
+where
+  (==) Wall Wall = True
+  (==) Free Free = True
+  (==) Box Box = True
+  (==) Agent Agent = True
+  (==) Target Target = True
+  (==) TargetBox TargetBox = True
+  (==) TargetAgent TargetAgent = True
+  (==) _ _ = False
+
 fromTile :: SokobanTile -> String
 fromTile Wall = "Wall"
 fromTile Free = "Free"