module SokobanCoord

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.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

checkY :: [[SokobanTile]] Int Int -> Int
checkY p x y 
  | ((x < 0) || (x > (length p - 1))) = -1 
  | otherwise = if (y > (length (p !! x) - 1)) (-1) y

genField :: [[SokobanTile]] Int Int -> String
genField p x y = "    init(x" <+ x <+ "_" <+ y <+ ") := " <+ fromTile ((p !! x) !! y) <+ ";"
    
genVars :: Int Int -> String
genVars x y = "    x" <+ x <+ "_" <+ y <+ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};"

genCoord :: [[SokobanTile]] Int Int -> [String]
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" <+ 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" <+ 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" <+ 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" <+ 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" <+ 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" <+ 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" <+ 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" <+ 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" <+ x <+ "_" <+ y <+ ";",
                "  esac;"
                ]

instance == SokobanTile
where
  (==) Wall Wall = True
  (==) Free Free = True
  (==) Box Box = True
  (==) Agent Agent = True
  (==) Target Target = True
  (==) TargetBox TargetBox = True
  (==) TargetAgent TargetAgent = True
  (==) _ _ = False

fromTile :: SokobanTile -> String
fromTile Wall = "Wall"
fromTile Free = "Free"
fromTile Box = "Box"
fromTile Target = "Target"
fromTile Agent = "Agent"
fromTile TargetAgent = "AgentOnTarget"
fromTile TargetBox = "BoxOnTarget"

genCond :: [[SokobanTile]] Int Int -> String
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" <+ x <+ "_" <+ y <+ " = BoxOnTarget") ""
    
addLogic :: [String] -> [String]
addLogic [] = []
addLogic [x] = [x]
addLogic [x:xs] = [x <+ " & ": addLogic xs]

genAll :: SokobanPuzzle -> String
genAll puzzle = let (Sokoban p) = puzzle in
 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])

readLines :: File -> [String]
readLines file
  | sfend file = []
  # (line, file) = sfreadline file
  | otherwise = [line: readLines file]

writeLines :: [String] *File -> *File
writeLines [] file = file
writeLines [l:ls] file = writeLines ls (file <<< l)

openInpFile :: *World String -> (File, *World)
openInpFile world path
  # (ok, file, world) = sfopen path 0 world
  | not ok = abort "Error reading the file."
  = (file, world)

openOutFile :: *World String -> (*File, *World)
openOutFile world path
  # (ok, file, world) = fopen path 1 world
  | not ok = abort "Can not write to a file."
  = (file, world)

closeFile :: *World *File -> (Bool, *World)
closeFile world file
  # world = fclose file world
  = world

Start :: *World -> *World
Start w
  # (p, w) = parse inpath w
  # s = genAll p
  # (f, w) = openOutFile w outpath
  # f = fwrites s f
  # (ok, w) = closeFile w f
  = w