X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=code%2FSokobanCoord.icl;h=4a664adc1f4bf187062c2eeba9d8420be87f5fe0;hb=d5453a5f0ccce9a424aea90b3f6c5c92d4712602;hp=0cce0c4d174ceaf400fc159a6f903802cecbbdfc;hpb=ac799d3f661e5440845954ec72b80a98ca26c511;p=mc1516pa.git diff --git a/code/SokobanCoord.icl b/code/SokobanCoord.icl index 0cce0c4..4a664ad 100644 --- a/code/SokobanCoord.icl +++ b/code/SokobanCoord.icl @@ -1,122 +1,93 @@ module SokobanCoord import StdList, StdInt, StdChar, StdMisc, StdClass, StdString, StdFile, StdArray, StdTuple, Data.Maybe, Data.Map, Control.Monad, Data.Tuple, Data.Void +import Sokoban -inputfile :== "screen.1" -outputfile :== "solver.smv" - -:: SokobanPuzzle :== [[SokobanTile]] -:: SokobanTile = Wall | Free | Box | Target | Agent +inpath :== "screen.2000" +outpath :== "solver.smv" puzzle :: SokobanPuzzle -puzzle = [[Wall, Wall, Wall, Wall, Wall, Wall], - [Wall, Free, Free, Free, Free, Wall], - [Wall, Agent,Free, Box, Free, Wall], - [Wall, Free, Free, Free, Target, Wall], - [Wall, Wall, Wall, Wall, Wall, Wall]] - -size :: (Int, Int) -size = (4,5) - -checkX :: Int -> Int -checkX x = if (x > length (hd puzzle)) (-1) x - -checkY :: Int -> Int -checkY y = if (y > length puzzle) (-1) y - -/* - next(x2_2) := case - x2_2 = Wall: Wall; - - x2_2 = Free & x2_3 = Agent & move = Left: Agent; - x2_2 = Free & x3_2 = Agent & move = Up: Agent; - x2_2 = Free & x2_1 = Agent & move = Right : Agent; - x2_2 = Free & x1_2 = Agent & move = Down : Agent; - - x2_2 = Free & x2_3 = Box & x2_4 = Agent & move = Left: Box; - x2_2 = Free & x3_2 = Box & x4_2 = Agent & move = Up: Box; - x2_2 = Free & x2_1 = Box & x2_0 = Agent & move = Right : Box; - x2_2 = Free & x1_2 = Box & x0_2 = Agent & move = Down : Box; - - x2_2 = Agent & (x2_3 = Free | x2_3 = Target) & move = Right: Free; - x2_2 = Agent & (x3_2 = Free | x3_2 = Target) & move = Down: Free; - x2_2 = Agent & (x2_1 = Free | x2_1 = Target) & move = Left : Free; - x2_2 = Agent & (x1_2 = Free | x1_2 = Target) & move = Up : Free; - - x2_2 = Box & x2_3 = Agent & (x2_1 = Free | x2_1 = Target) & move = Left: Agent; - x2_2 = Box & x3_2 = Agent & (x1_2 = Free | x1_2 = Target) & move = Up: Agent; - x2_2 = Box & x2_1 = Agent & (x2_3 = Free | x2_3 = Target) & move = Right : Agent; - x2_2 = Box & x1_2 = Agent & (x3_2 = Free | x3_2 = Target) & move = Down : Agent; - - x2_2 = Target & x2_3 = Agent & move = Left: AgentOnTarget; - x2_2 = Target & x3_2 = Agent & move = Up: AgentOnTarget; - x2_2 = Target & x2_1 = Agent & move = Right : AgentOnTarget; - x2_2 = Target & x1_2 = Agent & move = Down : AgentOnTarget; - - x2_2 = Target & x2_3 = Box & x2_4 = Agent & move = Left: BoxOnTarget; - x2_2 = Target & x3_2 = Box & x4_2 = Agent & move = Up: BoxOnTarget; - x2_2 = Target & x2_1 = Box & x2_0 = Agent & move = Right : BoxOnTarget; - x2_2 = Target & x1_2 = Box & x0_2 = Agent & move = Down : BoxOnTarget; - - x2_2 = AgentOnTarget & (x2_3 = Free | x2_3 = Target) & move = Right: Target; - x2_2 = AgentOnTarget & (x3_2 = Free | x3_2 = Target) & move = Down: Target; - x2_2 = AgentOnTarget & (x2_1 = Free | x2_1 = Target) & move = Left : Target; - x2_2 = AgentOnTarget & (x1_2 = Free | x1_2 = Target) & move = Up : Target; - - x2_2 = BoxOnTarget & x2_3 = Agent & (x2_1 = Free | x2_1 = Target) & move = Left: AgentOnTarget; - x2_2 = BoxOnTarget & x3_2 = Agent & (x1_2 = Free | x1_2 = Target) & move = Up: AgentOnTarget; - x2_2 = BoxOnTarget & x2_1 = Agent & (x2_3 = Free | x2_3 = Target) & move = Right : AgentOnTarget; - x2_2 = BoxOnTarget & x1_2 = Agent & (x3_2 = Free | x3_2 = Target) & move = Down : AgentOnTarget; - - TRUE : x2_2; - esac; - -*/ - -genCoord :: Int Int -> [String] -genCoord x y = [" next(x" +++ toString x +++ "_" +++ toString y +++ ") := case\n", +puzzle = Sokoban [[Wall, Wall, Wall, Wall, Wall, Wall], + [Wall, Free, Free, Free, Free, Wall], + [Wall, Agent,Free, Box, Free, Wall], + [Wall, Free, Free, Free, Target, Wall], + [Wall, Wall, Wall, Wall, Wall, Wall]] + +checkX :: [[SokobanTile]] Int -> Int +checkX p x = let (Sokoban p) = puzzle in if (x > (length p - 1)) (-1) x + +checkY :: [[SokobanTile]] Int Int -> Int +checkY p x y = let (Sokoban p) = puzzle in if (y > (length (p !! x) - 1)) (-1) y + +genField :: [[SokobanTile]] Int Int -> String +genField p x y = " init(x" +++ toString x +++ "_" +++ toString y +++ ") := " +++ fromTile ((p !! x) !! y) +++ ";\n" + +genVars :: Int Int -> String +genVars x y = " x" +++ toString x +++ "_" +++ toString y +++ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};\n" + +genCoord :: [[SokobanTile]] Int Int -> [String] +genCoord p x y = [" next(x" +++ toString x +++ "_" +++ toString y +++ ") := case\n", " x" +++ toString x +++ "_" +++ toString y +++ " = Wall: Wall;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Agent & move = Left: Agent;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: Agent;\n", + " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (checkY p x (y+1)) +++ " = Agent & move = Left: Agent;\n", + " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: Agent;\n", " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & move = Right : Agent;\n", " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & move = Down : Agent;\n", - " 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", - " 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", + " 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", + " 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", " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Box & x" +++ toString x +++ "_" +++ toString (x-2) +++ " = Agent & move = Right : Box;\n", " x" +++ toString x +++ "_" +++ toString y +++ " = Free & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-2) +++ "_" +++ toString y +++ " = Agent & move = Down : Box;\n", - " 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", - " 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", + " 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", + " 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", " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left : Free;\n", " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (x-1) +++ "_" +++ toString y +++ "= Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up : Free;\n", - " 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", - " 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", - " 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", - " 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", - " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (checkY (y+1)) +++ " = Agent & move = Left: AgentOnTarget;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: AgentOnTarget;\n", + " 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", + " 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", + " 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", + " 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", + " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (checkY p x (y+1)) +++ " = Agent & move = Left: AgentOnTarget;\n", + " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (checkX p (x+1)) +++ "_" +++ toString y +++ " = Agent & move = Up: AgentOnTarget;\n", " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Agent & move = Right : AgentOnTarget;\n", " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Agent & move = Down : AgentOnTarget;\n", - " 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", - " 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", + " 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", + " 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", " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Box & x" +++ toString x +++ "_" +++ toString (y-2) +++ " = Agent & move = Right : BoxOnTarget;\n", " x" +++ toString x +++ "_" +++ toString y +++ " = Target & x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Box & x" +++ toString (x-2) +++ "_" +++ toString y +++ " = Agent & move = Down : BoxOnTarget;\n", - " 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", - " 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", + " 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", + " 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", " x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Free | x" +++ toString x +++ "_" +++ toString (y-1) +++ " = Target) & move = Left : Target;\n", " x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Free | x" +++ toString (x-1) +++ "_" +++ toString y +++ " = Target) & move = Up : Target;\n", - " 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", - " 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", - " 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", - " 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", + " 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", + " 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", + " 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", + " 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", " TRUE : x" +++ toString x +++ "_" +++ toString y +++ ";\n", " esac;\n" ] -/* -genAll :: SokobanPuzzle -> [[String]] -genAll p = [\\] -genAll [x:xs] = [] -*/ +fromTile :: SokobanTile -> String +fromTile Wall = "Wall" +fromTile Free = "Free" +fromTile Box = "Box" +fromTile Target = "Target" +fromTile Agent = "Agent" +fromTile TargetAgent = "AgentOnTarget" +fromTile TargetBox = "BoxOnTarget" + +genAll :: SokobanPuzzle -> [String] +genAll puzzle = let (Sokoban p) = puzzle in + [ + "MODULE main\n", + "VAR\n" + ] + ++ [genVars x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]] + ++ [" move : {Up, Down, Left, Right};\n"] + ++ [ + " ASSIGN\n", + " init(move) := {Up, Down, Left, Right};\n" + ] + ++ [genField p x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]] + ++ flatten [filter (\x -> not (contains '-' x)) (genCoord p x y) \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]] + ++ [" next(move) := {Up, Down, Left, Right};\n"] contains :: Char String -> Bool contains char str = not (isEmpty [c\\c<-:str | char == c]) @@ -149,5 +120,11 @@ closeFile world file = world - -Start = flatten [filter (\x -> not (contains '-' x)) (genCoord x y) \\ x <- [0..4], y <- [0..5]] +Start :: *World -> *World +Start w + # (p, w) = parse inpath w + # s = genAll p + # (f, w) = openOutFile w outpath + # f = writeLines s f + # (ok, w) = closeFile w f + = w