X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=code%2FSokobanObjectwise.icl;h=4b9542d6c62b1aef29d6f08969e5ea26735c253f;hb=f36e9ed1caf9e2577c2215c6ca08877aa4729626;hp=15fb732e63b2f230d023c634a381dacff171a7c3;hpb=a7a9fa5ded371c89459ba6872290774488ec7c3d;p=mc1516pa.git

diff --git a/code/SokobanObjectwise.icl b/code/SokobanObjectwise.icl
index 15fb732..4b9542d 100644
--- a/code/SokobanObjectwise.icl
+++ b/code/SokobanObjectwise.icl
@@ -24,29 +24,29 @@ Start w
 
 encode :: SokobanPuzzle -> String
 encode p = join "\n" [
+	"MODULE ob(ix, iy)",
+	"VAR",
+	"\tx: 0.." <+ maxX <+ ";",
+	"\ty: 0.." <+ maxY <+ ";",
+	"INIT x=ix & y=iy",
+	"INVAR " <+ encodeObPosition legalPos,
+	"",
 	"MODULE main",
 	"VAR",
-	encodeObVar "agent" maxX maxY,
-	join "\n" [encodeObVar ("b" <+ i) maxX maxY\\i<-boxnums],
+	"\tagent: " <+ declareObject agent,
+	join "\n" ["\tb" <+ i <+ ": " <+ declareObject b\\i<-boxnums & b<-boxes],
 	"\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,
+	encodeBoxOnBoxes boxnums,
 	"--Goal state",
 	"INVAR " <+ encodeGoalState boxnums targetPos <+ ";",
-	"",
+	"--Agent movement",
 	encodeObMovement "agent",
+	"--Box movement",
 	encodeBoxMovement boxnums,
 	"CTLSPEC ! EF (movement = finished);",
 
@@ -60,6 +60,9 @@ encode p = join "\n" [
 		annot = annotate p
 		(maxX, maxY) = getMetrics annot
 
+declareObject :: (Int, Int) -> String
+declareObject (x, y) = "ob(" <+ x <+ ", " <+ y <+ ");"
+
 deltaDefine :: String
 deltaDefine = join "\n" [
 	"DEFINE dx := case",
@@ -108,8 +111,8 @@ encodeGoalState boxes targets = "(" <+
 		encodeOneGoal` :: [((Int, Int), Int)] -> [String]
 		encodeOneGoal` [] = []
 		encodeOneGoal` [((x, y), b):xs] = [
-			"b" <+ b <+ "x = " <+ x <+ " & " <+
-			"b" <+ b <+ "y = " <+ y:encodeOneGoal` xs]
+			"b" <+ b <+ ".x = " <+ x <+ " & " <+
+			"b" <+ b <+ ".y = " <+ y:encodeOneGoal` xs]
 
 encodeBoxOnBoxes :: [Int] -> String
 encodeBoxOnBoxes [] = ""
@@ -118,42 +121,35 @@ 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]
+		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]
+	"!(b" <+ i <+ ".x = agent.x & b" <+ i <+ ".y = agent.y)"\\i<-bs]
 
 encodeObMovement :: String -> String
-encodeObMovement s = "TRANS next(" <+ s <+ "x) = " <+ s <+ "x + dx;\n" <+
-	"TRANS next(" <+ s <+ "y) = " <+ s <+ "y + dy;"
+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]
+encodeObPosition :: [(Int, Int)] -> String
+encodeObPosition p = join " |\n\t" [forThisX 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"
+		forThisX :: Int [(Int, Int)] -> String
+		forThisX cx p = "(x=" <+ cx <+ " & (" <+
+			join " | " ["y=" <+ y \\(x, y)<-p | x == cx] <+ "))"
 
 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" <+
+		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 + 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" <+
+			"TRANS next(b" <+ i <+ ".y) = case\n" <+
+			"\t\tnext(agent.x) = b" <+ i <+ ".x & " <+
+			"next(agent.y) = b" <+ i <+ ".y: b" <+ i <+ ".y + dy;\n" <+
+			"\t\tTRUE: b" <+ i <+ ".y;\n" <+
 			"\tesac;"