code/SokobanCoord.icl

   1 module SokobanCoord
   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 size :: (Int, Int)
  19 size = (4,5)
  20
  21 checkX :: Int -> Int
  22 checkX x = if (x > length (hd puzzle)) (-1) x
  23
  24 checkY :: Int -> Int
  25 checkY y = if (y > length puzzle) (-1) y
  26
  27 /*
  28   next(x2_2) := case
  29     x2_2 = Wall: Wall;
  30
  31     x2_2 = Free & x2_3 = Agent & move = Left: Agent;
  32     x2_2 = Free & x3_2 = Agent & move = Up: Agent;
  33     x2_2 = Free & x2_1 = Agent & move = Right : Agent;
  34     x2_2 = Free & x1_2 = Agent & move = Down : Agent;
  35
  36     x2_2 = Free & x2_3 = Box & x2_4 = Agent & move = Left: Box;
  37     x2_2 = Free & x3_2 = Box & x4_2 = Agent & move = Up: Box;
  38     x2_2 = Free & x2_1 = Box & x2_0 = Agent & move = Right : Box;
  39     x2_2 = Free & x1_2 = Box & x0_2 = Agent & move = Down : Box;
  40
  41     x2_2 = Agent & (x2_3 = Free | x2_3 = Target) & move = Right: Free;
  42     x2_2 = Agent & (x3_2 = Free | x3_2 = Target) & move = Down: Free;
  43     x2_2 = Agent & (x2_1 = Free | x2_1 = Target) & move = Left : Free;
  44     x2_2 = Agent & (x1_2 = Free | x1_2 = Target) & move = Up : Free;
  45
  46     x2_2 = Box & x2_3 = Agent & (x2_1 = Free | x2_1 = Target) & move = Left: Agent;
  47     x2_2 = Box & x3_2 = Agent & (x1_2 = Free | x1_2 = Target) & move = Up: Agent;
  48     x2_2 = Box & x2_1 = Agent & (x2_3 = Free | x2_3 = Target) & move = Right : Agent;
  49     x2_2 = Box & x1_2 = Agent & (x3_2 = Free | x3_2 = Target) & move = Down : Agent;
  50
  51     x2_2 = Target & x2_3 = Agent & move = Left: AgentOnTarget;
  52     x2_2 = Target & x3_2 = Agent & move = Up: AgentOnTarget;
  53     x2_2 = Target & x2_1 = Agent & move = Right : AgentOnTarget;
  54     x2_2 = Target & x1_2 = Agent & move = Down : AgentOnTarget;
  55
  56     x2_2 = Target & x2_3 = Box & x2_4 = Agent & move = Left: BoxOnTarget;
  57     x2_2 = Target & x3_2 = Box & x4_2 = Agent & move = Up: BoxOnTarget;
  58     x2_2 = Target & x2_1 = Box & x2_0 = Agent & move = Right : BoxOnTarget;
  59     x2_2 = Target & x1_2 = Box & x0_2 = Agent & move = Down : BoxOnTarget;
  60
  61     x2_2 = AgentOnTarget & (x2_3 = Free | x2_3 = Target) & move = Right: Target;
  62     x2_2 = AgentOnTarget & (x3_2 = Free | x3_2 = Target) & move = Down: Target;
  63     x2_2 = AgentOnTarget & (x2_1 = Free | x2_1 = Target) & move = Left : Target;
  64     x2_2 = AgentOnTarget & (x1_2 = Free | x1_2 = Target) & move = Up : Target;
  65
  66     x2_2 = BoxOnTarget & x2_3 = Agent & (x2_1 = Free | x2_1 = Target) & move = Left: AgentOnTarget;
  67     x2_2 = BoxOnTarget & x3_2 = Agent & (x1_2 = Free | x1_2 = Target) & move = Up: AgentOnTarget;
  68     x2_2 = BoxOnTarget & x2_1 = Agent & (x2_3 = Free | x2_3 = Target) & move = Right : AgentOnTarget;
  69     x2_2 = BoxOnTarget & x1_2 = Agent & (x3_2 = Free | x3_2 = Target) & move = Down : AgentOnTarget;
  70
  71     TRUE : x2_2;
  72   esac;
  73
  74 */
  75
  76 genCoord :: Int Int -> [String]
  77 genCoord x y = ["  next(x" +++ toString x +++ "_" +++ toString y +++ ") := case\n",
  78                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Wall: Wall;\n",
  79                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Agent & move = Left: Agent;\n",
  80                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: Agent;\n",
  81                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & move = Right : Agent;\n",
  82                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & move = Down : Agent;\n",
  83                 "    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",
  84                 "    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",
  85                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Box & x" +++ toString x +++ "_" +++ toString (x-2) +++ " = Agent & move = Right : Box;\n",
  86                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-2) +++ "_" +++ toString y +++ " = Agent & move = Down : Box;\n",
  87                 "    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",
  88                 "    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",
  89                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left : Free;\n",
  90                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (x-1) +++ "_" +++ toString y +++ "= Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up : Free;\n",
  91                 "    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",
  92                 "    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",
  93                 "    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",
  94                 "    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",
  95                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Agent & move = Left: AgentOnTarget;\n",
  96                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: AgentOnTarget;\n",
  97                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & move = Right : AgentOnTarget;\n",
  98                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & move = Down : AgentOnTarget;\n",
  99                 "    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",
 100                 "    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",
 101                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Box & x" +++ toString x +++ "_" +++ toString (y-2) +++ " = Agent & move = Right : BoxOnTarget;\n",
 102                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-2) +++ "_" +++ toString y +++ " = Agent & move = Down : BoxOnTarget;\n",
 103                 "    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",
 104                 "    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",
 105                 "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left : Target;\n",
 106                 "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up : Target;\n",
 107                 "    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",
 108                 "    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",
 109                 "    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",
 110                 "    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",
 111                 "    TRUE : x" +++ toString x +++ "_" +++ toString y +++ ";\n",
 112                 "  esac;\n"
 113                 ]
 114
 115 /*
 116 genAll :: SokobanPuzzle -> [[String]]
 117 genAll p = [\\]
 118 genAll [x:xs] = []
 119 */
 120
 121 contains :: Char String -> Bool
 122 contains char str = not (isEmpty [c\\c<-:str | char == c])
 123
 124 readLines :: File -> [String]
 125 readLines file
 126   | sfend file = []
 127   # (line, file) = sfreadline file
 128   | otherwise = [line: readLines file]
 129
 130 writeLines :: [String] *File -> *File
 131 writeLines [] file = file
 132 writeLines [l:ls] file = writeLines ls (file <<< l)
 133
 134 openInpFile :: *World String -> (File, *World)
 135 openInpFile world path
 136   # (ok, file, world) = sfopen path 0 world
 137   | not ok = abort "Error reading the file."
 138   = (file, world)
 139
 140 openOutFile :: *World String -> (*File, *World)
 141 openOutFile world path
 142   # (ok, file, world) = fopen path 1 world
 143   | not ok = abort "Can not write to a file."
 144   = (file, world)
 145
 146 closeFile :: *World *File -> (Bool, *World)
 147 closeFile world file
 148   # world = fclose file world
 149   = world
 150
 151
 152
 153 Start = flatten [filter (\x -> not (contains '-' x)) (genCoord x y) \\ x <- [0..4], y <- [0..5]]