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 ob(ix, iy, movement)",
  28         "VAR",
  29         "\tx: 0 .. " <+ maxX <+ ";",
  30         "\ty: 0 .. " <+ maxX <+ ";",
  31
  32         "INVAR " <+ encodeObjectPositions legalPos <+ ";",
  33
  34         "ASSIGN",
  35         "\tinit(x):=ix;",
  36         "\tinit(y):=iy;\n",
  37
  38         "MODULE main",
  39         "VAR",
  40         "\tmovement: {left, up, right, down, finished};",
  41         "\tagent: " <+ encodeAgent annot,
  42         encodeBoxes boxes,
  43
  44         "DEFINE",
  45         "\tdx := case",
  46         "\t\tmovement = left : -1;",
  47         "\t\tmovement = right: +1;",
  48         "\t\tTRUE:              0;",
  49         "\tesac;",
  50         "\tdy := case",
  51         "\t\tmovement = up  : -1;",
  52         "\t\tmovement = down: +1;",
  53         "\t\tTRUE:             0;",
  54         "\tesac;",
  55
  56         "INVAR (" <+ encodeGoalState (indexList boxes) targetPos <+
  57                 ") <-> movement = finished;",
  58         "INVAR " <+ encodeAgentNotOnBox (indexList boxes) <+ ";",
  59         "INVAR " <+ encodeBoxesNotOnBox (indexList boxes),
  60         "TRANS next(agent.x) = agent.x + dx;",
  61         "TRANS next(agent.y) = agent.y + dy;",
  62         encodeBlockMovement (indexList boxes),
  63         "CTLSPEC ! EF (movement = finished)",
  64         "CTLSPEC EF (b0.x=3)"
  65         ]
  66         where
  67                 targetPos = getTargets annot
  68                 boxes = getBoxes annot
  69                 legalPos = legalPositions annot
  70                 annot = annotate p
  71                 (maxX, maxY) = getMetrics annot
  72
  73 //THIS IS NAIVE AND SHOULD BE IMPROVED
  74 legalPositions :: AnnotatedSokoban -> [(Int, Int)]
  75 legalPositions p = [(x, y)\\(x, y, t)<-p | case t of Wall=False; _=True]
  76
  77 annotate :: SokobanPuzzle -> AnnotatedSokoban
  78 annotate (Sokoban p) = flatten [[(x, y, t)\\t<-r & x<-[0..]]\\r<-p & y<-[0..]]
  79
  80 getTargets :: AnnotatedSokoban -> [(Int, Int)]
  81 getTargets p = [(x, y)\\(x, y, t)<-p |
  82         case t of Target=True;TargetBox=True;TargetAgent=True;_=False]
  83
  84 getMetrics :: AnnotatedSokoban -> (Int, Int)
  85 getMetrics p = (maximum (map fst3 p),maximum (map snd3 p))
  86
  87 getBoxes :: AnnotatedSokoban -> [(Int, Int)]
  88 getBoxes p = [(x, y)\\(x, y, Box)<-p] ++ [(x, y)\\(x, y, TargetBox)<-p]
  89
  90 (<+) infixr 5 :: a b -> String | toString a & toString b
  91 (<+) a b = toString a +++ toString b
  92
  93 encodeGoalState :: [Int] [(Int, Int)] -> String
  94 encodeGoalState boxes targets = join " |\n\t" $ map encodeOneGoal boxtargets
  95         where
  96                 boxtargets = map (zip2 targets) (permutations boxes)
  97
  98                 encodeOneGoal :: [((Int, Int), Int)] -> String
  99                 encodeOneGoal p = "(" <+ join " & " (encodeOneGoal` p) <+ ")"
 100
 101                 encodeOneGoal` :: [((Int, Int), Int)] -> [String]
 102                 encodeOneGoal` [] = []
 103                 encodeOneGoal` [((x, y), b):xs] = [
 104                         "b" <+ b <+ ".x = " <+ x <+ " & " <+
 105                         "b" <+ b <+ ".y = " <+ y:encodeOneGoal` xs]
 106
 107
 108 encodeBlockMovement :: [Int] -> String
 109 encodeBlockMovement bs = join "\n" $ map ebm bs
 110         where
 111                 ebm :: Int -> String
 112                 ebm i =
 113                         "TRANS next(b" <+ i <+ ".x) = case\n" <+
 114                         "\t\tnext(agent.x) != b" <+ i <+ ".x | " <+
 115                         "next(agent.y) != b" <+ i <+ ".y: b" <+ i <+ ".x;\n" <+
 116                         "\t\tTRUE: b" <+ i <+ ".x + dx;\n" <+
 117                         "\tesac;\n" <+
 118                         "TRANS next(b" <+ i <+ ".y) = case\n" <+
 119                         "\t\tnext(agent.x) != b" <+ i <+ ".x | " <+
 120                         "next(agent.y) != b" <+ i <+ ".y: b" <+ i <+ ".x;\n" <+
 121                         "\t\tTRUE: b" <+ i <+ ".y + dy;\n" <+
 122                         "\tesac;"
 123
 124 //TODO
 125 encodeBoxesNotOnBox :: [Int] -> String
 126 encodeBoxesNotOnBox _ = "TRUE;"
 127
 128 encodeAgentNotOnBox :: [Int] -> String
 129 encodeAgentNotOnBox bs = join " &\n\t" [
 130         "(b" <+ i <+ ".x != agent.x & b" <+ i <+ ".y != agent.y)"\\i<-bs]
 131
 132 encodeObjectPositions :: [(Int, Int)] -> String
 133 encodeObjectPositions p = join " | " ["x="<+x<+" & "<+"y="<+y\\(x, y)<-p]
 134
 135 encodeAgent :: AnnotatedSokoban -> String
 136 encodeAgent [x:xs] = case x of
 137         (x, y, Agent) = "ob(" <+ x <+ "," <+ y <+ ", movement);"
 138         (x, y, TargetAgent) = "ob(" <+ x <+ "," <+ y <+ ", movement);"
 139         _ = encodeAgent xs
 140
 141 encodeBoxes :: [(Int, Int)] -> String
 142 encodeBoxes p = join "\n"
 143         ["\tb" <+ i <+ ": ob(" <+ bx <+ ", " <+ by <+ ", movement);"
 144         \\(bx, by)<-p & i<-[0..]]