module SokobanObjectwise

import StdString
import StdFile
import StdTuple
import StdFunc
import StdOrdList
import StdList

from Data.Func import $
from Data.List import intercalate, maximum, permutations
from Text import class Text(concat,join), instance Text String

import Sokoban

:: AnnotatedSokoban :== [(Int, Int, SokobanTile)]

Start :: *World -> *World
Start w
# (io, w) = stdio w
# (puzzle, io) = parseFromFile io
# io = io <<< encode puzzle <<< "\n"
= snd (fclose io w)

encode :: SokobanPuzzle -> String
encode p = join "\n" [
	"MODULE ob(ix, iy, movement)",
	"VAR",
	"\tx: 0 .. " <+ maxX <+ ";",
	"\ty: 0 .. " <+ maxX <+ ";",

	"INVAR " <+ encodeObjectPositions legalPos <+ ";",

	"ASSIGN",
	"\tinit(x):=ix;",
	"\tinit(y):=iy;\n",

	"MODULE main",
	"VAR",
	"\tmovement: {left, up, right, down, finished};",
	"\tagent: " <+ encodeAgent annot,
	encodeBoxes boxes,
	
	"DEFINE",
	"\tdx := case",
	"\t\tmovement = left : -1;",
	"\t\tmovement = right: +1;",
	"\t\tTRUE:              0;",
	"\tesac;",
	"\tdy := case",
	"\t\tmovement = up  : -1;",
	"\t\tmovement = down: +1;",
	"\t\tTRUE:             0;",
	"\tesac;",

	"INVAR (" <+ encodeGoalState (indexList boxes) targetPos <+ 
		") <-> movement = finished;",
	"INVAR " <+ encodeAgentNotOnBox (indexList boxes) <+ ";",
	"TRANS next(agent.x) = agent.x + dx;",
	"TRANS next(agent.y) = agent.y + dy;",
	encodeBlockMovement (indexList boxes),
	"CTLSPEC ! EF (movement = finished)",
	"CTLSPEC EF (b0.x=3)"
	]
	where
		targetPos = getTargets annot
		boxes = getBoxes annot
		legalPos = legalPositions annot
		annot = annotate p
		(maxX, maxY) = getMetrics annot

//THIS IS NAIVE AND SHOULD BE IMPROVED
legalPositions :: AnnotatedSokoban -> [(Int, Int)]
legalPositions p = [(x, y)\\(x, y, t)<-p | case t of Wall=False; _=True]

annotate :: SokobanPuzzle -> AnnotatedSokoban
annotate (Sokoban p) = flatten [[(x, y, t)\\t<-r & x<-[0..]]\\r<-p & y<-[0..]]

getTargets :: AnnotatedSokoban -> [(Int, Int)]
getTargets p = [(x, y)\\(x, y, t)<-p | 
	case t of Target=True;TargetBox=True;TargetAgent=True;_=False] 

getMetrics :: AnnotatedSokoban -> (Int, Int)
getMetrics p = (maximum (map fst3 p),maximum (map snd3 p))

getBoxes :: AnnotatedSokoban -> [(Int, Int)]
getBoxes p = [(x, y)\\(x, y, Box)<-p] ++ [(x, y)\\(x, y, TargetBox)<-p]

(<+) infixr 5 :: a b -> String | toString a & toString b
(<+) a b = toString a +++ toString b

encodeGoalState :: [Int] [(Int, Int)] -> String
encodeGoalState boxes targets = join " |\n\t" $ map encodeOneGoal boxtargets
	where
		boxtargets = map (zip2 targets) (permutations boxes)
		
		encodeOneGoal :: [((Int, Int), Int)] -> String
		encodeOneGoal p = "(" <+ join " & " (encodeOneGoal` p) <+ ")"

		encodeOneGoal` :: [((Int, Int), Int)] -> [String]
		encodeOneGoal` [] = []
		encodeOneGoal` [((x, y), b):xs] = [
			"b" <+ b <+ ".x = " <+ x <+ " & " <+
			"b" <+ b <+ ".y = " <+ y:encodeOneGoal` xs]
		

encodeBlockMovement :: [Int] -> String
encodeBlockMovement bs = join "\n" $ map ebm bs
	where
		ebm :: Int -> String
		ebm i =
			"TRANS next(b" <+ i <+ ".x) = case\n" <+
			"\t\tnext(agent.x) != b" <+ i <+ ".x | " <+
			"next(agent.y) != b" <+ i <+ ".y: b" <+ i <+ ".x;\n" <+
			"\t\tTRUE: b" <+ i <+ ".x + dx;\n" <+
			"\tesac;\n" <+
			"TRANS next(b" <+ i <+ ".y) = case\n" <+
			"\t\tnext(agent.x) != b" <+ i <+ ".x | " <+
			"next(agent.y) != b" <+ i <+ ".y: b" <+ i <+ ".x;\n" <+
			"\t\tTRUE: b" <+ i <+ ".y + dy;\n" <+
			"\tesac;"

encodeAgentNotOnBox :: [Int] -> String
encodeAgentNotOnBox bs = join " &\n\t" [
	"(b" <+ i <+ ".x != agent.x & b" <+ i <+ ".y != agent.y)"\\i<-bs]

encodeObjectPositions :: [(Int, Int)] -> String
encodeObjectPositions p = join " | " ["x="<+x<+" & "<+"y="<+y\\(x, y)<-p]

encodeAgent :: AnnotatedSokoban -> String
encodeAgent [x:xs] = case x of
	(x, y, Agent) = "ob(" <+ x <+ "," <+ y <+ ", movement);"
	(x, y, TargetAgent) = "ob(" <+ x <+ "," <+ y <+ ", movement);"
	_ = encodeAgent xs

encodeBoxes :: [(Int, Int)] -> String
encodeBoxes p = join "\n" 
	["\tb" <+ i <+ ": ob(" <+ bx <+ ", " <+ by <+ ", movement);"
	\\(bx, by)<-p & i<-[0..]]