code/SokobanCoord.icl

   1 module SokobanCoord
   2
   3 import StdList, StdInt, StdBool, StdChar, StdMisc, StdClass, StdString, StdFile, StdArray, StdTuple, Data.Maybe, Data.Map, Data.Tuple, Data.Void
   4 from Text import class Text(concat,join), instance Text String
   5 import Sokoban
   6
   7 inpath  :== "screen.2001"
   8 outpath :== "solver.smv"
   9
  10 (<+) infixr 5 :: a b -> String | toString a & toString b
  11 (<+) a b = toString a +++ toString b
  12
  13 checkX :: [[SokobanTile]] Int -> Int
  14 checkX p x = if (x > (length p - 1)) (-1) x
  15
  16 checkY :: [[SokobanTile]] Int Int -> Int
  17 checkY p x y
  18   | ((x < 0) || (x > (length p - 1))) = -1
  19   | otherwise = if (y > (length (p !! x) - 1)) (-1) y
  20
  21 genField :: [[SokobanTile]] Int Int -> String
  22 genField p x y = "    init(x" <+ x <+ "_" <+ y <+ ") := " <+ fromTile ((p !! x) !! y) <+ ";"
  23
  24 genVars :: Int Int -> String
  25 genVars x y = "    x" <+ x <+ "_" <+ y <+ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};"
  26
  27 genCoord :: [[SokobanTile]] Int Int -> [String]
  28 genCoord p x y = ["  next(x" <+ x <+ "_" <+ y <+ ") := case",
  29                 "    x" <+ x <+ "_" <+ y <+ " = Wall: Wall;",
  30                 "    x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Agent | x"
  31                         <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = AgentOnTarget) & move = Left: Agent;",
  32                 "    x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
  33                         <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & move = Up: Agent;",
  34                 "    x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
  35                         <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & move = Right : Agent;",
  36                 "    x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
  37                         <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & move = Down : Agent;",
  38
  39                 "    x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Box | x"
  40                         <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = BoxOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+2)) <+ " = Agent | x"
  41                         <+ (checkX p x) <+ "_" <+ (checkY p x  (y+2)) <+ " = AgentOnTarget) & move = Left: Box;",
  42                 "    x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Box | x"
  43                         <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = BoxOnTarget) & (x" <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = Agent | x"
  44                         <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = AgentOnTarget) & move = Up: Box;",
  45                 "    x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Box | x"
  46                         <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = BoxOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = Agent | x"
  47                         <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = AgentOnTarget) & move = Right : Box;",
  48                 "    x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Box | x"
  49                         <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = BoxOnTarget) & (x" <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = Agent | x"
  50                         <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = AgentOnTarget) & move = Down : Box;",
  51
  52                 "    x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Target) & move = Right: Free;",
  53                 "    x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p x y) <+ " = Target) & move = Down: Free;",
  54                 "    x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left : Free;",
  55                 "    x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ "= Free | x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Target) & move = Up : Free;",
  56
  57                 "    x" <+ x <+ "_" <+ y <+ " = Agent &  (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Box | x"
  58                         <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = BoxOnTarget) & (x"
  59                         <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = Target) & move = Right: Free;",
  60                 "    x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p x y) <+ " = Box | x"
  61                         <+ (checkX p (x+1)) <+ "_" <+ (checkY p x y) <+ " = BoxOnTarget) & (x"
  62                         <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = Free | x" <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = Target) & move = Down: Free;",
  63                 "    x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Box | x"
  64                         <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = BoxOnTarget) & (x"
  65                         <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = Target) & move = Left: Free;",
  66                 "    x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Box | x"
  67                         <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = BoxOnTarget) & (x"
  68                         <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = Free | x" <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = Target) & move = Up: Free;",
  69
  70                 "    x" <+ x <+ "_" <+ y <+ " = Box & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Agent | x"
  71                         <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left: Agent;",
  72                 "    x" <+ x <+ "_" <+ y <+ " = Box & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
  73                         <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & (x" <+ (x-1) <+ "_" <+ (checkY p (x-1) y) <+ " = Free | x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Target) & move = Up: Agent;",
  74                 "    x" <+ x <+ "_" <+ y <+ " = Box & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
  75                         <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Target) & move = Right : Agent;",
  76                 "    x" <+ x <+ "_" <+ y <+ " = Box & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
  77                         <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p x y) <+ " = Target) & move = Down : Agent;",
  78
  79                 "    x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Agent | x"
  80                         <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = AgentOnTarget) & move = Left: AgentOnTarget;",
  81                 "    x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
  82                         <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & move = Up: AgentOnTarget;",
  83                 "    x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
  84                         <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & move = Right : AgentOnTarget;",
  85                 "    x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
  86                         <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & move = Down : AgentOnTarget;",
  87
  88                 "    x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Box | x"
  89                         <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = BoxOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+2)) <+ " = Agent | x"
  90                         <+ (checkX p x) <+ "_" <+ (checkY p x  (y+2)) <+ " = AgentOnTarget) & move = Left: BoxOnTarget;",
  91                 "    x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Box | x"
  92                         <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = BoxOnTarget) & (x" <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = Agent | x"
  93                         <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = AgentOnTarget) & move = Up: BoxOnTarget;",
  94                 "    x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Box | x"
  95                         <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = BoxOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = Agent | x"
  96                         <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = AgentOnTarget) & move = Right : BoxOnTarget;",
  97                 "    x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Box | x"
  98                         <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = BoxOnTarget) & (x" <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = Agent | x"
  99                         <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = AgentOnTarget) & move = Down : BoxOnTarget;",
 100
 101                 "    x" <+ x <+ "_" <+ y <+ " = AgentOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Target) & move = Right: Target;",
 102                 "    x" <+ x <+ "_" <+ y <+ " = AgentOnTarget & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Target) & move = Down: Target;",
 103                 "    x" <+ x <+ "_" <+ y <+ " = AgentOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left : Target;",
 104                 "    x" <+ x <+ "_" <+ y <+ " = AgentOnTarget & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Free | x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Target) & move = Up : Target;",
 105
 106                 "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Agent | x"
 107                         <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left: AgentOnTarget;",
 108                 "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
 109                         <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Free | x" <+ (checkX p (x-1)) <+ "_"
 110                         <+ (checkY p (x-1) y) <+ " = Target) & move = Up: AgentOnTarget;",
 111                 "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
 112                         <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Free | x" <+ x <+ "_" <+ (checkY p x  (y+1)) <+ " = Target) & move = Right : AgentOnTarget;",
 113                 "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
 114                         <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_"
 115                         <+ (checkY p (x+1) y) <+ " = Target) & move = Down : AgentOnTarget;",
 116
 117                 "    TRUE : x" <+ x <+ "_" <+ y <+ ";",
 118                 "  esac;"
 119                 ]
 120
 121 instance == SokobanTile
 122 where
 123   (==) Wall Wall = True
 124   (==) Free Free = True
 125   (==) Box Box = True
 126   (==) Agent Agent = True
 127   (==) Target Target = True
 128   (==) TargetBox TargetBox = True
 129   (==) TargetAgent TargetAgent = True
 130   (==) _ _ = False
 131
 132 fromTile :: SokobanTile -> String
 133 fromTile Wall = "Wall"
 134 fromTile Free = "Free"
 135 fromTile Box = "Box"
 136 fromTile Target = "Target"
 137 fromTile Agent = "Agent"
 138 fromTile TargetAgent = "AgentOnTarget"
 139 fromTile TargetBox = "BoxOnTarget"
 140
 141 genCond :: [[SokobanTile]] Int Int -> String
 142 genCond p x y
 143   | x < 0 || y < 0 || x > (length p) - 1 = ""
 144   | otherwise
 145     | y > (length (p !! x) - 1) = ""
 146     | otherwise = if ((p !! x) !! y == Target) ("x" <+ x <+ "_" <+ y <+ " = BoxOnTarget") ""
 147
 148 addLogic :: [String] -> [String]
 149 addLogic [] = []
 150 addLogic [x] = [x]
 151 addLogic [x:xs] = [x <+ " & ": addLogic xs]
 152
 153 genAll :: SokobanPuzzle -> String
 154 genAll puzzle = let (Sokoban p) = puzzle in
 155  join "\n" [
 156           "MODULE main"
 157           ,"VAR"
 158
 159           , join "\n" [genVars x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
 160           ,"    move : {Up, Down, Left, Right};"
 161           ,"  ASSIGN"
 162           ,"    init(move) := {Up, Down, Left, Right};"
 163           ,join "\n" [genField p x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
 164           ,join "\n" (flatten [filter (\x -> not (contains '-' x)) (genCoord p x y) \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]])
 165           ,"  next(move) := {Up, Down, Left, Right};"
 166           ,"INVARSPEC !("
 167           ,join "\n" (addLogic (filter (\x -> x <> "" ) [genCond p x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]))
 168           ,")"]
 169
 170 contains :: Char String -> Bool
 171 contains char str = not (isEmpty [c\\c<-:str | char == c])
 172
 173 readLines :: File -> [String]
 174 readLines file
 175   | sfend file = []
 176   # (line, file) = sfreadline file
 177   | otherwise = [line: readLines file]
 178
 179 writeLines :: [String] *File -> *File
 180 writeLines [] file = file
 181 writeLines [l:ls] file = writeLines ls (file <<< l)
 182
 183 openInpFile :: *World String -> (File, *World)
 184 openInpFile world path
 185   # (ok, file, world) = sfopen path 0 world
 186   | not ok = abort "Error reading the file."
 187   = (file, world)
 188
 189 openOutFile :: *World String -> (*File, *World)
 190 openOutFile world path
 191   # (ok, file, world) = fopen path 1 world
 192   | not ok = abort "Can not write to a file."
 193   = (file, world)
 194
 195 closeFile :: *World *File -> (Bool, *World)
 196 closeFile world file
 197   # world = fclose file world
 198   = world
 199
 200 Start :: *World -> *World
 201 Start w
 202   # (p, w) = parse inpath w
 203   # s = genAll p
 204   # (f, w) = openOutFile w outpath
 205   # f = fwrites s f
 206   # (ok, w) = closeFile w f
 207   = w