From: Alexander Fedotov Date: Sun, 13 Mar 2016 10:49:54 +0000 (+0100) Subject: some cleanup X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=fce8f94ed6880b60ee021e5a56cdd815fa3b0fd2;p=mc1516pa.git some cleanup --- diff --git a/code/SokobanCoord.icl b/code/SokobanCoord.icl index 1c98cb8..96430fe 100644 --- a/code/SokobanCoord.icl +++ b/code/SokobanCoord.icl @@ -1,11 +1,15 @@ module SokobanCoord -import StdList, StdInt, StdBool, StdChar, StdMisc, StdClass, StdString, StdFile, StdArray, StdTuple, Data.Maybe, Data.Map, Control.Monad, Data.Tuple, Data.Void +import StdList, StdInt, StdBool, StdChar, StdMisc, StdClass, StdString, StdFile, StdArray, StdTuple, Data.Maybe, Data.Map, Data.Tuple, Data.Void +from Text import class Text(concat,join), instance Text String import Sokoban -inpath :== "screen.1001" +inpath :== "screen.2001" outpath :== "solver.smv" +(<+) infixr 5 :: a b -> String | toString a & toString b +(<+) a b = toString a +++ toString b + checkX :: [[SokobanTile]] Int -> Int checkX p x = if (x > (length p - 1)) (-1) x @@ -15,103 +19,103 @@ checkY p x y | otherwise = 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" +genField p x y = " init(x" <+ x <+ "_" <+ y <+ ") := " <+ fromTile ((p !! x) !! y) <+ ";" genVars :: Int Int -> String -genVars x y = " x" +++ toString x +++ "_" +++ toString y +++ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};\n" +genVars x y = " x" <+ x <+ "_" <+ y <+ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};" 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 (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Agent | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = AgentOnTarget) & move = Left: Agent;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent | x" - +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = AgentOnTarget) & move = Up: Agent;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = AgentOnTarget) & move = Right : Agent;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent | x" - +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = AgentOnTarget) & move = Down : Agent;\n", +genCoord p x y = [" next(x" <+ x <+ "_" <+ y <+ ") := case", + " x" <+ x <+ "_" <+ y <+ " = Wall: Wall;", + " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Agent | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = AgentOnTarget) & move = Left: Agent;", + " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x" + <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & move = Up: Agent;", + " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & move = Right : Agent;", + " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x" + <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & move = Down : Agent;", - " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Box | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = BoxOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = Agent | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = AgentOnTarget) & move = Left: Box;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Box | x" - +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = BoxOnTarget) & (x" +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Agent | x" - +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = AgentOnTarget) & move = Up: Box;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Box | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = BoxOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Agent | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = AgentOnTarget) & move = Right : Box;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Box | x" - +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = BoxOnTarget) & (x" +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Agent | x" - +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = AgentOnTarget) & move = Down : Box;\n", + " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Box | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = BoxOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = Agent | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = AgentOnTarget) & move = Left: Box;", + " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Box | x" + <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = BoxOnTarget) & (x" <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = Agent | x" + <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = AgentOnTarget) & move = Up: Box;", + " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Box | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = BoxOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = Agent | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = AgentOnTarget) & move = Right : Box;", + " x" <+ x <+ "_" <+ y <+ " = Free & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Box | x" + <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = BoxOnTarget) & (x" <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = Agent | x" + <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = AgentOnTarget) & move = Down : Box;", - " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Free | x" +++ toString (checkX p 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 (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = Target) & move = Down: Free;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left : Free;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ "= Free | x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up : Free;\n", + " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Target) & move = Right: Free;", + " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p x y) <+ " = Target) & move = Down: Free;", + " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left : Free;", + " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ "= Free | x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Target) & move = Up : Free;", - " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Box | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = BoxOnTarget) & (x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = Target) & move = Right: Free;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = Box | x" - +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = BoxOnTarget) & (x" - +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Free | x" +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Target) & move = Down: Free;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Box | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = BoxOnTarget) & (x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Target) & move = Left: Free;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Box | x" - +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = BoxOnTarget) & (x" - +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Free | x" +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Target) & move = Up: Free;\n", + " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Box | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = BoxOnTarget) & (x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = Target) & move = Right: Free;", + " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p x y) <+ " = Box | x" + <+ (checkX p (x+1)) <+ "_" <+ (checkY p x y) <+ " = BoxOnTarget) & (x" + <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = Free | x" <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = Target) & move = Down: Free;", + " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Box | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = BoxOnTarget) & (x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = Target) & move = Left: Free;", + " x" <+ x <+ "_" <+ y <+ " = Agent & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Box | x" + <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = BoxOnTarget) & (x" + <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = Free | x" <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = Target) & move = Up: Free;", - " x" +++ toString x +++ "_" +++ toString y +++ " = Box & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Agent | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = AgentOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left: Agent;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Box & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent | x" - +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = AgentOnTarget) & (x" +++ toString (x-1) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Free | x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up: Agent;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Box & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = AgentOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Target) & move = Right : Agent;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Box & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent | x" - +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = AgentOnTarget) & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = Target) & move = Down : Agent;\n", + " x" <+ x <+ "_" <+ y <+ " = Box & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Agent | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left: Agent;", + " x" <+ x <+ "_" <+ y <+ " = Box & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x" + <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & (x" <+ (x-1) <+ "_" <+ (checkY p (x-1) y) <+ " = Free | x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Target) & move = Up: Agent;", + " x" <+ x <+ "_" <+ y <+ " = Box & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Target) & move = Right : Agent;", + " x" <+ x <+ "_" <+ y <+ " = Box & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x" + <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p x y) <+ " = Target) & move = Down : Agent;", - " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Agent | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = AgentOnTarget) & move = Left: AgentOnTarget;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent | x" - +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = AgentOnTarget) & move = Up: AgentOnTarget;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = AgentOnTarget) & move = Right : AgentOnTarget;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent | x" - +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = AgentOnTarget) & move = Down : AgentOnTarget;\n", + " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Agent | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = AgentOnTarget) & move = Left: AgentOnTarget;", + " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x" + <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & move = Up: AgentOnTarget;", + " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & move = Right : AgentOnTarget;", + " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x" + <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & move = Down : AgentOnTarget;", - " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Box | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = BoxOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = Agent | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = AgentOnTarget) & move = Left: BoxOnTarget;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Box | x" - +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = BoxOnTarget) & (x" +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Agent | x" - +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = AgentOnTarget) & move = Up: BoxOnTarget;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Box | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = BoxOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Agent | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = AgentOnTarget) & move = Right : BoxOnTarget;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Box | x" - +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = BoxOnTarget) & (x" +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Agent | x" - +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = AgentOnTarget) & move = Down : BoxOnTarget;\n", + " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Box | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = BoxOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = Agent | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y+2)) <+ " = AgentOnTarget) & move = Left: BoxOnTarget;", + " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Box | x" + <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = BoxOnTarget) & (x" <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = Agent | x" + <+ (checkX p (x+2)) <+ "_" <+ (checkY p (x+2) y) <+ " = AgentOnTarget) & move = Up: BoxOnTarget;", + " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Box | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = BoxOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = Agent | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y-2)) <+ " = AgentOnTarget) & move = Right : BoxOnTarget;", + " x" <+ x <+ "_" <+ y <+ " = Target & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Box | x" + <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = BoxOnTarget) & (x" <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = Agent | x" + <+ (checkX p (x-2)) <+ "_" <+ (checkY p (x-2) y) <+ " = AgentOnTarget) & move = Down : BoxOnTarget;", - " x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Free | x" +++ toString (checkX p 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 (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Target) & move = Down: Target;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left : Target;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Free | x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up : Target;\n", + " x" <+ x <+ "_" <+ y <+ " = AgentOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Target) & move = Right: Target;", + " x" <+ x <+ "_" <+ y <+ " = AgentOnTarget & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Target) & move = Down: Target;", + " x" <+ x <+ "_" <+ y <+ " = AgentOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left : Target;", + " x" <+ x <+ "_" <+ y <+ " = AgentOnTarget & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Free | x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Target) & move = Up : Target;", - " x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Agent | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = AgentOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left: AgentOnTarget;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent | x" - +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = AgentOnTarget) & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Free | x" +++ toString (checkX p (x-1)) +++ "_" - +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up: AgentOnTarget;\n", - " x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent | x" - +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = AgentOnTarget) & (x" +++ toString (checkX p 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 (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent | x" - +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = AgentOnTarget) & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" - +++ toString (checkY p (x+1) y) +++ " = Target) & move = Down : AgentOnTarget;\n", + " x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Agent | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left: AgentOnTarget;", + " x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x" + <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Free | x" <+ (checkX p (x-1)) <+ "_" + <+ (checkY p (x-1) y) <+ " = Target) & move = Up: AgentOnTarget;", + " x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x" + <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y+1)) <+ " = Free | x" <+ x <+ "_" <+ (checkY p x (y+1)) <+ " = Target) & move = Right : AgentOnTarget;", + " x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x" + <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_" + <+ (checkY p (x+1) y) <+ " = Target) & move = Down : AgentOnTarget;", - " TRUE : x" +++ toString x +++ "_" +++ toString y +++ ";\n", - " esac;\n" + " TRUE : x" <+ x <+ "_" <+ y <+ ";", + " esac;" ] instance == SokobanTile @@ -139,31 +143,29 @@ genCond p x y | x < 0 || y < 0 || x > (length p) - 1 = "" | otherwise | y > (length (p !! x) - 1) = "" - | otherwise = if ((p !! x) !! y == Target) ("x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget") "" + | otherwise = if ((p !! x) !! y == Target) ("x" <+ x <+ "_" <+ y <+ " = BoxOnTarget") "" addLogic :: [String] -> [String] addLogic [] = [] addLogic [x] = [x] -addLogic [x:xs] = [x +++ " & ": addLogic xs] +addLogic [x:xs] = [x <+ " & ": addLogic xs] -genAll :: SokobanPuzzle -> [String] +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"] - ++ ["INVARSPEC !("] - ++ addLogic (filter (\x -> x <> "" ) [genCond p x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]) - ++ [")\n"] + join "\n" [ + "MODULE main" + ,"VAR" + + , join "\n" [genVars x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]] + ," move : {Up, Down, Left, Right};" + ," ASSIGN" + ," init(move) := {Up, Down, Left, Right};" + ,join "\n" [genField p x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]] + ,join "\n" (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};" + ,"INVARSPEC !(" + ,join "\n" (addLogic (filter (\x -> x <> "" ) [genCond p x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]])) + ,")"] contains :: Char String -> Bool contains char str = not (isEmpty [c\\c<-:str | char == c]) @@ -200,6 +202,6 @@ Start w # (p, w) = parse inpath w # s = genAll p # (f, w) = openOutFile w outpath - # f = writeLines s f + # f = fwrites s f # (ok, w) = closeFile w f = w \ No newline at end of file