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 main",
	"VAR",
	encodeObVar "agent" maxX maxY,
	join "\n" [encodeObVar ("b" <+ i) maxX maxY\\i<-boxnums],
	"\tmovement: {left, up, right, down, finished};",
	"--Handy variable for deltas",
	deltaDefine,
	"--Initial values",
	"INIT",
	encodeObInit "agent" agent <+ " &",
	join " &\n" [encodeObInit ("b" <+ i) p\\p<-boxes & i<-[0..]],
	"--Agent not on the box",
	"INVAR " <+ encodeAgentNotOnBox boxnums <+ ";",
	"--Allowed box positions on the field",
	join "\n" ["INVAR "<+encodeObPosition ("b"<+b) legalPos<+";"\\b<-boxnums],
	"--Box not on box",
	encodeBoxOnBoxes (indexList boxes),
	"--Allowed agent positions",
	"INVAR " <+ encodeObPosition "agent" legalPos,
	"--Goal state",
	"INVAR " <+ encodeGoalState boxnums targetPos <+ ";",
	"",
	encodeObMovement "agent",
	encodeBoxMovement boxnums,
	"CTLSPEC ! EF (movement = finished);",

	""]
	where
		targetPos = getTargets annot
		boxes = getBoxes annot
		boxnums = indexList boxes
		agent = hd $ getAgents annot
		legalPos = legalPositions annot
		annot = annotate p
		(maxX, maxY) = getMetrics annot

deltaDefine :: String
deltaDefine = join "\n" [
	"DEFINE dx := 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;"]

//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))

getAgents :: AnnotatedSokoban -> [(Int, Int)]
getAgents p = [(x, y)\\(x, y, Agent)<-p] ++ [(x, y)\\(x, y, TargetAgent)<-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) <+ ")<->movement=finished"
	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]

encodeBoxOnBoxes :: [Int] -> String
encodeBoxOnBoxes [] = ""
encodeBoxOnBoxes [b] = ""
encodeBoxOnBoxes [b:bs] = "INVAR " <+ encodeBoxOnBox b bs <+ ";\n" <+
	encodeBoxOnBoxes bs
	where
		encodeBoxOnBox :: Int [Int] -> String
		encodeBoxOnBox x bs = join " & " ["!(b" <+ x <+ "x=b" <+ b <+ "x &" <+ 
			"b" <+ x <+ "y=b" <+ b <+ "y)"\\b<-bs]

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

encodeObMovement :: String -> String
encodeObMovement s = "TRANS next(" <+ s <+ "x) = " <+ s <+ "x + dx;\n" <+
	"TRANS next(" <+ s <+ "y) = " <+ s <+ "y + dy;"

encodeObPosition :: String [(Int, Int)] -> String
encodeObPosition b p = join " |\n\t" [forThisX b x p\\x<-removeDup $ map fst p]
	where
		forThisX :: String Int [(Int, Int)] -> String
		forThisX s cx p = "(" <+ s <+ "x=" <+ cx <+ " & (" <+
			join " | " [s <+ "y=" <+ y \\(x, y)<-p | x == cx] <+ "))"

encodeObInit :: String (Int, Int) -> String
encodeObInit s (x, y) = "\t" <+ s <+ "x=" <+ x <+ " & " <+ s <+ "y=" <+ y

encodeObVar :: String Int Int -> String
encodeObVar s mx my = "\t" <+ s <+ "x: 0.." <+ mx <+ ";\n" <+ 
	"\t" <+ s <+ "y: 0.." <+ my <+ ";\n"

encodeBoxMovement :: [Int] -> String
encodeBoxMovement bs = join "\n" $ map ebm bs
	where
		ebm :: Int -> String
		ebm i = "TRANS next(b" <+ i <+ "x) = case\n" <+
			"\t\tnext(agentx) = b" <+ i <+ "x & " <+
			"next(agenty) = b" <+ i <+ "y: b" <+ i <+ "x + dx;\n" <+
			"\t\tTRUE: b" <+ i <+ "x;\n" <+
			"\tesac;\n" <+
			"TRANS next(b" <+ i <+ "y) = case\n" <+
			"\t\tnext(agentx) = b" <+ i <+ "x & " <+
			"next(agenty) = b" <+ i <+ "y: b" <+ i <+ "y + dy;\n" <+
			"\t\tTRUE: b" <+ i <+ "y;\n" <+
			"\tesac;"