works!

diff --git a/code/SokobanObjectwise.icl b/code/SokobanObjectwise.icl
index 7297c32..15fb732 100644 (file)
--- a/code/SokobanObjectwise.icl
+++ b/code/SokobanObjectwise.icl
@@ -26,48 +26,53 @@ encode :: SokobanPuzzle -> String
 encode p = join "\n" [
        "MODULE main",
        "VAR",
-       encodeAgentVars maxX maxY,
-       encodeBoxVars (indexList boxes) maxX maxY,
+       encodeObVar "agent" maxX maxY,
+       join "\n" [encodeObVar ("b" <+ i) maxX maxY\\i<-boxnums],
        "\tmovement: {left, up, right, down, finished};",
-       "",
-       "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;",
-       "",
+       "--Handy variable for deltas",
+       deltaDefine,
+       "--Initial values",
        "INIT",
-       encodeAgentInit agent <+ " &",
-       encodeBoxInit boxes <+ ";",
+       encodeObInit "agent" agent <+ " &",
+       join " &\n" [encodeObInit ("b" <+ i) p\\p<-boxes & i<-[0..]],
        "--Agent not on the box",
-       "INVAR " <+ encodeAgentNotOnBox (indexList boxes) <+ ";",
+       "INVAR " <+ encodeAgentNotOnBox boxnums <+ ";",
        "--Allowed box positions on the field",
-       encodeBoxPositions (indexList boxes) legalPos,
+       join "\n" ["INVAR "<+encodeObPosition ("b"<+b) legalPos<+";"\\b<-boxnums],
        "--Box not on box",
        encodeBoxOnBoxes (indexList boxes),
        "--Allowed agent positions",
-       "INVAR " <+ encodeAgentPositions legalPos,
+       "INVAR " <+ encodeObPosition "agent" legalPos,
        "--Goal state",
-       "INVAR " <+ encodeGoalState (indexList boxes) targetPos <+ ";",
+       "INVAR " <+ encodeGoalState boxnums targetPos <+ ";",
        "",
-       encodeAgentMovement,
-       encodeBoxMovement (indexList boxes),
+       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]
@@ -120,46 +125,29 @@ 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 " | " [
-       "(" <+ b <+ "x=" <+ x <+ " & " <+
-       b <+ "y=" <+ y <+ ")"\\ (x, y)<-p]
-
-encodeAgentInit :: (Int, Int) -> String
-encodeAgentInit (x, y) = "\tagentx=" <+ x <+ " & " <+ "agenty=" <+ y
-
-encodeAgentVars :: Int Int -> String
-encodeAgentVars mx my = 
-       "\tagentx: 0.." <+ mx <+ ";\n\tagenty: 0.." <+ my <+ ";\n"
-
-encodeAgentPositions :: [(Int, Int)] -> String
-encodeAgentPositions p = encodeObPosition "agent" p
-
-encodeAgentMovement :: String
-encodeAgentMovement = "TRANS next(agentx) = agentx + dx;\n" <+
-       "TRANS next(agenty) = agenty + dy;"
-
-encodeBoxInit :: [(Int,Int)] -> String
-encodeBoxInit bs = join " &\n" [
-       "\tb" <+ i <+ "x=" <+ x <+ " & " <+
-       "b" <+ i <+ "y=" <+ y
-       \\(x, y)<-bs & i<-[0..]]
-
-encodeBoxVars :: [Int] Int Int -> String
-encodeBoxVars p mx my = join "\n" 
-       ["\tb" <+ i <+ "x: 0.." <+ mx <+ ";\n" <+
-       "\tb" <+ i <+ "y: 0.." <+ my <+ ";" \\ i<-p]
-       
-encodeBoxPositions :: [Int] [(Int, Int)] -> String
-encodeBoxPositions bs ps = join "\n" [
-       "INVAR " <+ encodeObPosition ("b" <+ b) ps <+ ";"\\b<-bs]
+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" <+
+               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" <+