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,
"--Goal state",
"INVAR " <+ encodeGoalState boxnums targetPos <+ ";",
"",
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",
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 [] = ""
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;"