code/SokobanObjectwise.icl

   1 module SokobanObjectwise
   2
   3 import StdString
   4 import StdFile
   5 import StdTuple
   6 import StdFunc
   7 import StdOrdList
   8 import StdList
   9
  10 from Data.Func import $
  11 from Data.List import intercalate, maximum, permutations
  12 from Text import class Text(concat,join), instance Text String
  13
  14 import Sokoban
  15
  16 :: AnnotatedSokoban :== [(Int, Int, SokobanTile)]
  17
  18 Start :: *World -> *World
  19 Start w
  20 # (io, w) = stdio w
  21 # (puzzle, io) = parseFromFile io
  22 # io = io <<< encode puzzle <<< "\n"
  23 = snd (fclose io w)
  24
  25 encode :: SokobanPuzzle -> String
  26 encode p = join "\n" [
  27         "MODULE main",
  28         "VAR",
  29         encodeObVar "agent" maxX maxY,
  30         join "\n" [encodeObVar ("b" <+ i) maxX maxY\\i<-boxnums],
  31         "\tmovement: {left, up, right, down, finished};",
  32         "--Handy variable for deltas",
  33         deltaDefine,
  34         "--Initial values",
  35         "INIT",
  36         encodeObInit "agent" agent <+ " &",
  37         join " &\n" [encodeObInit ("b" <+ i) p\\p<-boxes & i<-[0..]],
  38         "--Agent not on the box",
  39         "INVAR " <+ encodeAgentNotOnBox boxnums <+ ";",
  40         "--Allowed box positions on the field",
  41         join "\n" ["INVAR "<+encodeObPosition ("b"<+b) legalPos<+";"\\b<-boxnums],
  42         "--Box not on box",
  43         encodeBoxOnBoxes (indexList boxes),
  44         "--Allowed agent positions",
  45         "INVAR " <+ encodeObPosition "agent" legalPos,
  46         "--Goal state",
  47         "INVAR " <+ encodeGoalState boxnums targetPos <+ ";",
  48         "",
  49         encodeObMovement "agent",
  50         encodeBoxMovement boxnums,
  51         "CTLSPEC ! EF (movement = finished);",
  52
  53         ""]
  54         where
  55                 targetPos = getTargets annot
  56                 boxes = getBoxes annot
  57                 boxnums = indexList boxes
  58                 agent = hd $ getAgents annot
  59                 legalPos = legalPositions annot
  60                 annot = annotate p
  61                 (maxX, maxY) = getMetrics annot
  62
  63 deltaDefine :: String
  64 deltaDefine = join "\n" [
  65         "DEFINE dx := case",
  66         "\t\tmovement = left : -1;",
  67         "\t\tmovement = right: +1;",
  68         "\t\tTRUE:              0;",
  69         "\tesac;",
  70         "\tdy := case",
  71         "\t\tmovement = up  : -1;",
  72         "\t\tmovement = down: +1;",
  73         "\t\tTRUE:             0;",
  74         "\tesac;"]
  75
  76 //THIS IS NAIVE AND SHOULD BE IMPROVED
  77 legalPositions :: AnnotatedSokoban -> [(Int, Int)]
  78 legalPositions p = [(x, y)\\(x, y, t)<-p | case t of Wall=False; _=True]
  79
  80 annotate :: SokobanPuzzle -> AnnotatedSokoban
  81 annotate (Sokoban p) = flatten [[(x, y, t)\\t<-r & x<-[0..]]\\r<-p & y<-[0..]]
  82
  83 getTargets :: AnnotatedSokoban -> [(Int, Int)]
  84 getTargets p = [(x, y)\\(x, y, t)<-p |
  85         case t of Target=True;TargetBox=True;TargetAgent=True;_=False]
  86
  87 getMetrics :: AnnotatedSokoban -> (Int, Int)
  88 getMetrics p = (maximum (map fst3 p),maximum (map snd3 p))
  89
  90 getAgents :: AnnotatedSokoban -> [(Int, Int)]
  91 getAgents p = [(x, y)\\(x, y, Agent)<-p] ++ [(x, y)\\(x, y, TargetAgent)<-p]
  92
  93 getBoxes :: AnnotatedSokoban -> [(Int, Int)]
  94 getBoxes p = [(x, y)\\(x, y, Box)<-p] ++ [(x, y)\\(x, y, TargetBox)<-p]
  95
  96 (<+) infixr 5 :: a b -> String | toString a & toString b
  97 (<+) a b = toString a +++ toString b
  98
  99 encodeGoalState :: [Int] [(Int, Int)] -> String
 100 encodeGoalState boxes targets = "(" <+
 101         join " |\n\t" (map encodeOneGoal boxtargets) <+ ")<->movement=finished"
 102         where
 103                 boxtargets = map (zip2 targets) (permutations boxes)
 104
 105                 encodeOneGoal :: [((Int, Int), Int)] -> String
 106                 encodeOneGoal p = "(" <+ join " & " (encodeOneGoal` p) <+ ")"
 107
 108                 encodeOneGoal` :: [((Int, Int), Int)] -> [String]
 109                 encodeOneGoal` [] = []
 110                 encodeOneGoal` [((x, y), b):xs] = [
 111                         "b" <+ b <+ "x = " <+ x <+ " & " <+
 112                         "b" <+ b <+ "y = " <+ y:encodeOneGoal` xs]
 113
 114 encodeBoxOnBoxes :: [Int] -> String
 115 encodeBoxOnBoxes [] = ""
 116 encodeBoxOnBoxes [b] = ""
 117 encodeBoxOnBoxes [b:bs] = "INVAR " <+ encodeBoxOnBox b bs <+ ";\n" <+
 118         encodeBoxOnBoxes bs
 119         where
 120                 encodeBoxOnBox :: Int [Int] -> String
 121                 encodeBoxOnBox x bs = join " & " ["!(b" <+ x <+ "x=b" <+ b <+ "x &" <+
 122                         "b" <+ x <+ "y=b" <+ b <+ "y)"\\b<-bs]
 123
 124 encodeAgentNotOnBox :: [Int] -> String
 125 encodeAgentNotOnBox bs = join " &\n\t" [
 126         "!(b" <+ i <+ "x = agentx & b" <+ i <+ "y = agenty)"\\i<-bs]
 127
 128 encodeObMovement :: String -> String
 129 encodeObMovement s = "TRANS next(" <+ s <+ "x) = " <+ s <+ "x + dx;\n" <+
 130         "TRANS next(" <+ s <+ "y) = " <+ s <+ "y + dy;"
 131
 132 encodeObPosition :: String [(Int, Int)] -> String
 133 encodeObPosition b p = join " |\n\t" [forThisX b x p\\x<-removeDup $ map fst p]
 134         where
 135                 forThisX :: String Int [(Int, Int)] -> String
 136                 forThisX s cx p = "(" <+ s <+ "x=" <+ cx <+ " & (" <+
 137                         join " | " [s <+ "y=" <+ y \\(x, y)<-p | x == cx] <+ "))"
 138
 139 encodeObInit :: String (Int, Int) -> String
 140 encodeObInit s (x, y) = "\t" <+ s <+ "x=" <+ x <+ " & " <+ s <+ "y=" <+ y
 141
 142 encodeObVar :: String Int Int -> String
 143 encodeObVar s mx my = "\t" <+ s <+ "x: 0.." <+ mx <+ ";\n" <+
 144         "\t" <+ s <+ "y: 0.." <+ my <+ ";\n"
 145
 146 encodeBoxMovement :: [Int] -> String
 147 encodeBoxMovement bs = join "\n" $ map ebm bs
 148         where
 149                 ebm :: Int -> String
 150                 ebm i = "TRANS next(b" <+ i <+ "x) = case\n" <+
 151                         "\t\tnext(agentx) = b" <+ i <+ "x & " <+
 152                         "next(agenty) = b" <+ i <+ "y: b" <+ i <+ "x + dx;\n" <+
 153                         "\t\tTRUE: b" <+ i <+ "x;\n" <+
 154                         "\tesac;\n" <+
 155                         "TRANS next(b" <+ i <+ "y) = case\n" <+
 156                         "\t\tnext(agentx) = b" <+ i <+ "x & " <+
 157                         "next(agenty) = b" <+ i <+ "y: b" <+ i <+ "y + dy;\n" <+
 158                         "\t\tTRUE: b" <+ i <+ "y;\n" <+
 159                         "\tesac;"