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