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 import Sokoban
   5
   6 inputfile  :== "screen.1"
   7 outputfile :== "solver.smv"
   8
   9 puzzle :: SokobanPuzzle
  10 puzzle = Sokoban [[Wall, Wall, Wall, Wall, Wall,   Wall],
  11                   [Wall, Free, Free, Free, Free,   Wall],
  12                   [Wall, Agent,Free, Box,  Free,   Wall],
  13                   [Wall, Free, Free, Free, Target, Wall],
  14                   [Wall, Wall, Wall, Wall, Wall,   Wall]]
  15
  16 fromTile :: SokobanTile -> String
  17 fromTile Wall = "Wall"
  18 fromTile Free = "Free"
  19 fromTile Box = "Box"
  20 fromTile Target = "Target"
  21 fromTile Agent = "Agent"
  22 fromTile TargetAgent = "AgentOnTarget"
  23 fromTile TargetBox = "BoxOnTarget"
  24
  25 checkX :: Int -> Int
  26 checkX x = let (Sokoban p) = puzzle in if (x > length (hd p)) (-1) x
  27
  28 checkY :: Int -> Int
  29 checkY y = let (Sokoban p) = puzzle in if (y > length p) (-1) y
  30
  31 genField :: SokobanPuzzle -> [String]
  32 genField p = let (Sokoban pzl) = p in genField` pzl 0 0 []
  33 where
  34   genField` :: [[SokobanTile]] Int Int [String] -> [String]
  35   genField` p i j rs
  36     | i+1 == length (hd p) = rs
  37     | j == (length p) = genField` p (i+1) 0 ["    init(x" +++ toString i +++ "_" +++ toString j +++ ") := " +++ fromTile ((p !! i) !! j) +++ ";\n": rs]
  38     | otherwise = genField` p i (j+1) ["    init(x" +++ toString i +++ "_" +++ toString j +++ ") := " +++ fromTile ((p !! i) !! j) +++ ";\n": rs]
  39
  40 genVars :: Int Int -> [String]
  41 genVars x y = genVars` x y 0 0 []
  42 where
  43   genVars` :: Int Int Int Int [String] -> [String]
  44   genVars` a b x y res
  45     | (a+1) == x = res
  46     | b == y = genVars` a b (x+1) 0 ["    x" +++ toString x +++ "_" +++ toString y +++ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};\n":res]
  47     | otherwise = genVars` a b x (y+1) ["    x" +++ toString x +++ "_" +++ toString y +++ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};\n":res]
  48
  49 genCoord :: Int Int -> [String]
  50 genCoord x y = ["  next(x" +++ toString x +++ "_" +++ toString y +++ ") := case\n",
  51                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Wall: Wall;\n",
  52                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Agent & move = Left: Agent;\n",
  53                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: Agent;\n",
  54                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & move = Right : Agent;\n",
  55                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & move = Down : Agent;\n",
  56                 "    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",
  57                 "    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",
  58                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Box & x" +++ toString x +++ "_" +++ toString (x-2) +++ " = Agent & move = Right : Box;\n",
  59                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-2) +++ "_" +++ toString y +++ " = Agent & move = Down : Box;\n",
  60                 "    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",
  61                 "    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",
  62                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left : Free;\n",
  63                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (x-1) +++ "_" +++ toString y +++ "= Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up : Free;\n",
  64                 "    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",
  65                 "    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",
  66                 "    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",
  67                 "    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",
  68                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Agent & move = Left: AgentOnTarget;\n",
  69                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: AgentOnTarget;\n",
  70                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & move = Right : AgentOnTarget;\n",
  71                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & move = Down : AgentOnTarget;\n",
  72                 "    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",
  73                 "    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",
  74                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Box & x" +++ toString x +++ "_" +++ toString (y-2) +++ " = Agent & move = Right : BoxOnTarget;\n",
  75                 "    x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-2) +++ "_" +++ toString y +++ " = Agent & move = Down : BoxOnTarget;\n",
  76                 "    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",
  77                 "    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",
  78                 "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left : Target;\n",
  79                 "    x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up : Target;\n",
  80                 "    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",
  81                 "    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",
  82                 "    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",
  83                 "    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",
  84                 "    TRUE : x" +++ toString x +++ "_" +++ toString y +++ ";\n",
  85                 "  esac;\n"
  86                 ]
  87
  88 genAll :: [String]
  89 genAll = let (Sokoban p) = puzzle in
  90          [
  91           "MODULE main\n",
  92           "VAR\n"
  93           ]
  94       ++ genVars ((length p) - 1) ((length (hd p)) - 1)
  95       ++ [
  96           "  ASSIGN\n",
  97           "    init(move) := {Up, Down, Left, Right};\n"
  98          ]
  99       ++ genField puzzle
 100       ++ flatten [filter (\x -> not (contains '-' x)) (genCoord x y) \\ x <- [0..4], y <- [0..5]]
 101
 102 contains :: Char String -> Bool
 103 contains char str = not (isEmpty [c\\c<-:str | char == c])
 104
 105 readLines :: File -> [String]
 106 readLines file
 107   | sfend file = []
 108   # (line, file) = sfreadline file
 109   | otherwise = [line: readLines file]
 110
 111 writeLines :: [String] *File -> *File
 112 writeLines [] file = file
 113 writeLines [l:ls] file = writeLines ls (file <<< l)
 114
 115 openInpFile :: *World String -> (File, *World)
 116 openInpFile world path
 117   # (ok, file, world) = sfopen path 0 world
 118   | not ok = abort "Error reading the file."
 119   = (file, world)
 120
 121 openOutFile :: *World String -> (*File, *World)
 122 openOutFile world path
 123   # (ok, file, world) = fopen path 1 world
 124   | not ok = abort "Can not write to a file."
 125   = (file, world)
 126
 127 closeFile :: *World *File -> (Bool, *World)
 128 closeFile world file
 129   # world = fclose file world
 130   = world
 131
 132 Start = genAll