code/SokobanCoord.icl

   1 module SocobanCoord
   2
   3 import StdList, StdInt, StdChar, StdMisc, StdClass, StdString, StdFile, StdArray, StdTuple, Data.Maybe, Data.Map, Control.Monad, Data.Tuple, Data.Void
   4
   5 inputfile  :== "screen.1"
   6 outputfile :== "solver.smv"
   7
   8 :: SokobanPuzzle :== [[SokobanTile]]
   9 :: SokobanTile = Wall | Free | Box | Target | Agent
  10
  11 puzzle :: SokobanPuzzle
  12 puzzle = [[Wall, Wall, Wall, Wall, Wall,   Wall],
  13           [Wall, Free, Free, Free, Free,   Wall],
  14           [Wall, Agent,Free, Box,  Free,   Wall],
  15           [Wall, Free, Free, Free, Target, Wall],
  16           [Wall, Wall, Wall, Wall, Wall,   Wall]]
  17
  18
  19 checkX :: Int -> Int
  20 checkX x = if (x > length (hd puzzle)) (-1) x
  21
  22 checkY :: Int -> Int
  23 checkY y = if (y > length puzzle) (-1) y
  24
  25 genVars :: Int Int -> [String]
  26 genVars x y = genVars` x y 0 0 []
  27 where
  28   genVars` :: Int Int Int Int [String] -> [String]
  29   genVars` a b x y res
  30     | (a+1) == x = res
  31     | b == y = genVars` a b (x+1) 0 ["    x" +++ toString x +++ "_" +++ toString y +++ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};\n":res]
  32     | otherwise = genVars` a b x (y+1) ["    x" +++ toString x +++ "_" +++ toString y +++ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};\n":res]
  33
  34 genCoord :: Int Int -> [String]
  35 genCoord x y = ["  next(x" +++ toString x +++ "_" +++ toString y +++ ") := case\n",
  36                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Wall: Wall;\n",
  37                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Agent & move = Left: Agent;\n",
  38                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: Agent;\n",
  39                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & move = Right : Agent;\n",
  40                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & move = Down : Agent;\n",
  41                 "    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",
  42                 "    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",
  43                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Box & x" +++ toString x +++ "_" +++ toString (x-2) +++ " = Agent & move = Right : Box;\n",
  44                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-2) +++ "_" +++ toString y +++ " = Agent & move = Down : Box;\n",
  45                 "    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",
  46                 "    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",
  47                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left : Free;\n",
  48                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (x-1) +++ "_" +++ toString y +++ "= Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up : Free;\n",
  49                 "    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",
  50                 "    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",
  51                 "    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",
  52                 "    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",
  53                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Agent & move = Left: AgentOnTarget;\n",
  54                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: AgentOnTarget;\n",
  55                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & move = Right : AgentOnTarget;\n",
  56                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & move = Down : AgentOnTarget;\n",
  57                 "    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",
  58                 "    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",
  59                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Box & x" +++ toString x +++ "_" +++ toString (y-2) +++ " = Agent & move = Right : BoxOnTarget;\n",
  60                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-2) +++ "_" +++ toString y +++ " = Agent & move = Down : BoxOnTarget;\n",
  61                 "    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",
  62                 "    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",
  63                 "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left : Target;\n",
  64                 "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up : Target;\n",
  65                 "    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",
  66                 "    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",
  67                 "    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",
  68                 "    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",
  69                 "    TRUE : x" +++ toString x +++ "_" +++ toString y +++ ";\n",
  70                 "  esac;\n"
  71                 ]
  72
  73 genAll :: [String]
  74 genAll = [
  75           "MODULE main\n",
  76           "VAR\n"
  77           ]
  78       ++ genVars ((length puzzle) - 1) ((length (hd puzzle)) - 1)
  79       ++ [
  80           "ASSIGN",
  81           "init(x0_0) := Wall;", //currently just a stub
  82           "init(x0_1) := Wall;",
  83           "init(x0_2) := Wall;",
  84           "init(x0_3) := Wall;",
  85           "init(x0_4) := Wall;",
  86           "init(x0_5) := Wall;",
  87           "init(x1_0) := Wall;",
  88           "init(x1_1) := Free;",
  89           "init(x1_2) := Free;",
  90           "init(x1_3) := Free;",
  91           "init(x1_4) := Free;",
  92           "init(x1_5) := Wall;",
  93           "init(x2_0) := Wall;",
  94           "init(x2_1) := Agent;",
  95           "init(x2_2) := Free;",
  96           "init(x2_3) := Box;",
  97           "init(x2_4) := Free;",
  98           "init(x2_5) := Wall;",
  99           "init(x3_0) := Wall;",
 100           "init(x3_1) := Free;",
 101           "init(x3_2) := Free;",
 102           "init(x3_3) := Free;",
 103           "init(x3_4) := Target;",
 104           "init(x3_5) := Wall;",
 105           "init(x4_0) := Wall;",
 106           "init(x4_1) := Wall;",
 107           "init(x4_2) := Wall;",
 108           "init(x4_3) := Wall;",
 109           "init(x4_4) := Wall;",
 110           "init(x4_5) := Wall;",
 111           "init(move) := {Up, Down, Left, Right};"
 112          ]
 113       ++ flatten [filter (\x -> not (contains '-' x)) (genCoord x y) \\ x <- [0..4], y <- [0..5]]
 114
 115 contains :: Char String -> Bool
 116 contains char str = not (isEmpty [c\\c<-:str | char == c])
 117
 118 readLines :: File -> [String]
 119 readLines file
 120   | sfend file = []
 121   # (line, file) = sfreadline file
 122   | otherwise = [line: readLines file]
 123
 124 writeLines :: [String] *File -> *File
 125 writeLines [] file = file
 126 writeLines [l:ls] file = writeLines ls (file <<< l)
 127
 128 openInpFile :: *World String -> (File, *World)
 129 openInpFile world path
 130   # (ok, file, world) = sfopen path 0 world
 131   | not ok = abort "Error reading the file."
 132   = (file, world)
 133
 134 openOutFile :: *World String -> (*File, *World)
 135 openOutFile world path
 136   # (ok, file, world) = fopen path 1 world
 137   | not ok = abort "Can not write to a file."
 138   = (file, world)
 139
 140 closeFile :: *World *File -> (Bool, *World)
 141 closeFile world file
 142   # world = fclose file world
 143   = world
 144
 145 Start = genAll