X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=code%2FSokobanObjectwise.icl;h=d51ee5525255804c66ad39accf5897a335c98856;hb=f299e4212080c6cff79893ba99cebe7ab18a500e;hp=f234ae1ed96fffc984a8fd89ee74b8ebbfe5806d;hpb=81190f3341c4f7f12529ffa32f5f6a3ca984da77;p=mc1516pa.git

diff --git a/code/SokobanObjectwise.icl b/code/SokobanObjectwise.icl
index f234ae1..d51ee55 100644
--- a/code/SokobanObjectwise.icl
+++ b/code/SokobanObjectwise.icl
@@ -1,5 +1,139 @@
 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
 
-Start = "hi"
+:: 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..]]