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)",
  28         "VAR",
  29         "\tx: 0.." <+ maxX <+ ";",
  30         "\ty: 0.." <+ maxY <+ ";",
  31         "INIT x=ix & y=iy",
  32         "INVAR " <+ encodeObPosition legalPos,
  33         "",
  34         "MODULE main",
  35         "VAR",
  36         "\tagent: " <+ declareObject agent,
  37         join "\n" ["\tb" <+ i <+ ": " <+ declareObject b\\i<-boxnums & b<-boxes],
  38         "\tmovement: {left, up, right, down, finished};",
  39         "--Handy variable for deltas",
  40         deltaDefine,
  41         "--Agent not on the box",
  42         "INVAR " <+ encodeAgentNotOnBox boxnums <+ ";",
  43         "--Box not on box",
  44         "INVAR " <+ encodeBoxOnBoxes boxnums <+ ";",
  45         "--Goal state",
  46         "INVAR " <+ encodeGoalState boxnums targetPos <+ ";",
  47         "--Agent movement",
  48         encodeObMovement "agent",
  49         "--Box movement",
  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 declareObject :: (Int, Int) -> String
  64 declareObject (x, y) = "ob(" <+ x <+ ", " <+ y <+ ");"
  65
  66 deltaDefine :: String
  67 deltaDefine = join "\n" [
  68         "DEFINE dx := case",
  69         "\t\tmovement = left : -1;",
  70         "\t\tmovement = right: +1;",
  71         "\t\tTRUE:              0;",
  72         "\tesac;",
  73         "\tdy := case",
  74         "\t\tmovement = up  : -1;",
  75         "\t\tmovement = down: +1;",
  76         "\t\tTRUE:             0;",
  77         "\tesac;"]
  78
  79 //THIS IS NAIVE AND SHOULD BE IMPROVED
  80 legalPositions :: AnnotatedSokoban -> [(Int, Int)]
  81 legalPositions p = [(x, y)\\(x, y, t)<-p | case t of Wall=False; _=True]
  82
  83 annotate :: SokobanPuzzle -> AnnotatedSokoban
  84 annotate (Sokoban p) = flatten [[(x, y, t)\\t<-r & x<-[0..]]\\r<-p & y<-[0..]]
  85
  86 getTargets :: AnnotatedSokoban -> [(Int, Int)]
  87 getTargets p = [(x, y)\\(x, y, t)<-p |
  88         case t of Target=True;TargetBox=True;TargetAgent=True;_=False]
  89
  90 getMetrics :: AnnotatedSokoban -> (Int, Int)
  91 getMetrics p = (maximum (map fst3 p),maximum (map snd3 p))
  92
  93 getAgents :: AnnotatedSokoban -> [(Int, Int)]
  94 getAgents p = [(x, y)\\(x, y, Agent)<-p] ++ [(x, y)\\(x, y, TargetAgent)<-p]
  95
  96 getBoxes :: AnnotatedSokoban -> [(Int, Int)]
  97 getBoxes p = [(x, y)\\(x, y, Box)<-p] ++ [(x, y)\\(x, y, TargetBox)<-p]
  98
  99 (<+) infixr 5 :: a b -> String | toString a & toString b
 100 (<+) a b = toString a +++ toString b
 101
 102 encodeGoalState :: [Int] [(Int, Int)] -> String
 103 encodeGoalState boxes targets = "(" <+
 104         join " |\n\t" (map encodeOneGoal boxtargets) <+ ")<->movement=finished"
 105         where
 106                 boxtargets = map (zip2 targets) (permutations boxes)
 107
 108                 encodeOneGoal :: [((Int, Int), Int)] -> String
 109                 encodeOneGoal p = "(" <+ join " & " (encodeOneGoal` p) <+ ")"
 110
 111                 encodeOneGoal` :: [((Int, Int), Int)] -> [String]
 112                 encodeOneGoal` [] = []
 113                 encodeOneGoal` [((x, y), b):xs] = [
 114                         "b" <+ b <+ ".x = " <+ x <+ " & " <+
 115                         "b" <+ b <+ ".y = " <+ y:encodeOneGoal` xs]
 116
 117 encodeBoxOnBoxes :: [Int] -> String
 118 encodeBoxOnBoxes [] = ""
 119 encodeBoxOnBoxes [b] = "TRUE"
 120 encodeBoxOnBoxes [b:bs] = encodeBoxOnBox b bs <+ " &\n\t" <+
 121         encodeBoxOnBoxes bs
 122         where
 123                 encodeBoxOnBox :: Int [Int] -> String
 124                 encodeBoxOnBox x bs = join " & " ["!(b" <+ x <+ ".x=b" <+ b <+ ".x &" <+
 125                         "b" <+ x <+ ".y=b" <+ b <+ ".y)"\\b<-bs]
 126
 127 encodeAgentNotOnBox :: [Int] -> String
 128 encodeAgentNotOnBox bs = join " &\n\t" [
 129         "!(b" <+ i <+ ".x = agent.x & b" <+ i <+ ".y = agent.y)"\\i<-bs]
 130
 131 encodeObMovement :: String -> String
 132 encodeObMovement s = "TRANS next(" <+ s <+ ".x) = " <+ s <+ ".x + dx & " <+
 133         "next(" <+ s <+ ".y) = " <+ s <+ ".y + dy;"
 134
 135 encodeObPosition :: [(Int, Int)] -> String
 136 encodeObPosition p = join " |\n\t" [forThisX x p\\x<-removeDup $ map fst p]
 137         where
 138                 forThisX :: Int [(Int, Int)] -> String
 139                 forThisX cx p = "(x=" <+ cx <+ " & (" <+
 140                         join " | " ["y=" <+ y \\(x, y)<-p | x == cx] <+ "))"
 141
 142 encodeBoxMovement :: [Int] -> String
 143 encodeBoxMovement bs = join "\n" $ map ebm bs
 144         where
 145                 ebm :: Int -> String
 146                 ebm i = "TRANS next(b" <+ i <+ ".x) = case\n" <+
 147                         "\t\tnext(agent.x) = b" <+ i <+ ".x & " <+
 148                         "next(agent.y) = b" <+ i <+ ".y: b" <+ i <+ ".x + dx;\n" <+
 149                         "\t\tTRUE: b" <+ i <+ ".x;\n" <+
 150                         "\tesac;\n" <+
 151                         "TRANS next(b" <+ i <+ ".y) = case\n" <+
 152                         "\t\tnext(agent.x) = b" <+ i <+ ".x & " <+
 153                         "next(agent.y) = b" <+ i <+ ".y: b" <+ i <+ ".y + dy;\n" <+
 154                         "\t\tTRUE: b" <+ i <+ ".y;\n" <+
 155                         "\tesac;"