afp/a11/a11.icl

   1 module a11
   2
   3 import StdEnv
   4
   5 import Data.Functor
   6 import Control.Applicative
   7 import Control.Monad => qualified join
   8 import Control.Monad.Trans
   9 import Control.Monad.State
  10 import Data.Maybe
  11 import Data.Error
  12 import Data.Either
  13 import Data.Func
  14 import Text
  15
  16 :: Step pre post = Step
  17 :: High = High
  18 :: Low = Low
  19
  20 class action v
  21 where
  22         moveToShip :: v (Step High High)
  23         moveToQuay :: v (Step High High)
  24         moveUp :: v (Step Low High)
  25         moveDown :: v (Step High Low)
  26         lock :: v (Step Low Low)
  27         unlock :: v (Step Low Low)
  28         wait :: v (Step a a)
  29         (:.) infixl 1 :: (v (Step a b)) (v (Step b c)) -> v (Step a c)
  30         While :: (v Bool) (v (Step a a)) -> v (Step a a)
  31
  32 class expr v
  33 where
  34         containersBelow :: v Int
  35         lit :: t -> v t | toString t
  36         (<.) infix 4 :: (v t) (v t) -> (v Bool) | Ord t
  37         (>.) infix 4 :: (v t) (v t) -> (v Bool) | Ord t
  38         (+.) infix 4 :: (v t) (v t) -> (v t) | + t
  39
  40 :: Var a = Var Int
  41 class var v
  42 where
  43         def :: (v t) ((v (Var t)) -> (v (Step a b))) -> v (Step a b) | TC t
  44         var :: (v (Var t)) -> v t | TC t
  45         (=.) infixr 2 :: (v (Var t)) (v t) -> v (Step a a) | TC t
  46
  47 //Printing
  48 :: Printer a = P (Int Int [String] -> [String])
  49 runPrinter (P a) = a 0 0
  50
  51 word :: String -> Printer a
  52 word s = P \v i c->[createArray i '\t',s:c]
  53
  54 instance action Printer
  55 where
  56         moveToShip = word "moveToShip"
  57         moveToQuay = word "moveToQuay"
  58         moveUp = word "moveUp"
  59         moveDown = word "moveDown"
  60         lock = word "lock"
  61         unlock = word "unlock"
  62         wait = word "wait"
  63         (:.) (P a) (P b) = P \v i c->a v i [":.\n":b v i c]
  64         While (P b) (P a) = P \v i c->["while (":b v 0 [")\n":a v (i+1) ["\n)":c]]]
  65
  66 instance expr Printer
  67 where
  68         containersBelow = P \v i c->["containerBelow":c]
  69         lit x = P \v i c->[toString x:c]
  70         (<.) (P x) (P y) = P \v i c->x v i [" < ":y v i c]
  71         (>.) (P x) (P y) = P \v i c->x v i [" > ":y v i c]
  72         (+.) (P x) (P y) = P \v i c->x v i [" + ":y v i c]
  73
  74 varname i = "v" +++ toString i
  75 instance var Printer
  76 where
  77         def (P e) fun = P \v i c->[createArray i '\t',"def ":e v i [" \\",varname v,".\n":let (P f) = fun (P \_ i c->[varname v:c]) in f (inc v) i c]]
  78         var (P e) = P e
  79         (=.) (P a) (P b) = P \v i c->[createArray i '\t':a v i [" = ":b v i c]]
  80
  81 //Evaluating
  82 :: Eval a :== StateT SemState (Either String) a
  83 cast f = f >>| pure Step
  84 fail s = liftT (Left s)
  85 runEval = runStateT
  86 instance action (StateT SemState (Either String))
  87 where
  88         moveToShip = cast $ modify (\s->{s & craneOnQuay=False})
  89         moveToQuay = cast $ modify (\s->{s & craneOnQuay=True})
  90         moveUp     = cast $ modify (\s->{s & craneUp=True})
  91         moveDown   = cast $ modify (\s->{s & craneUp=False})
  92         lock       = cast $ getState >>= \s->case s of
  93                 {locked=Just _}                   = fail "Already locked"
  94                 {craneOnQuay=True,onQuay=[]}      = fail "No container to lock to"
  95                 {craneOnQuay=False,onShip=[]}     = fail "No container to lock to"
  96                 {craneOnQuay=True,onQuay=[x:xs]}  = put {s & onQuay=xs,locked=Just x}
  97                 {craneOnQuay=False,onShip=[x:xs]} = put {s & onShip=xs,locked=Just x}
  98                 _                                 = fail "Shouldn't happen"
  99         unlock       = cast $ getState >>= \s->case s of
 100                 {locked=Nothing}                  = fail "Already unlocked"
 101                 {craneOnQuay=True,locked=Just x}  = put {s & onQuay=[x:s.onQuay],locked=Nothing}
 102                 {craneOnQuay=False,locked=Just x} = put {s & onShip=[x:s.onShip],locked=Nothing}
 103                 _                                 = fail "Shouldn't happen"
 104         wait = pure Step
 105         (:.) x y = cast $ x >>| y
 106         While x y = x >>= \b->if b (y :. (While x y)) (pure Step)
 107
 108 instance expr (StateT SemState (Either String))
 109 where
 110         containersBelow = gets (\s->length if s.craneOnQuay s.onQuay s.onShip)
 111         lit x = pure x
 112         (<.) x y = (<) <$> x <*> y
 113         (>.) x y = (>) <$> x <*> y
 114         (+.) x y = (+) <$> x <*> y
 115
 116 instance var (StateT SemState (Either String))
 117 where
 118         def d fun = d >>= \v->gets (\s->length s.variables) >>= \i->modify (\s->{s & variables=s.variables ++ [dynamic v]}) >>| fun (pure (Var i))
 119         var a = a >>= \(Var i)->gets (\s->s.variables !! i) >>= cast
 120         where
 121                 cast :: Dynamic -> StateT SemState (Either String) a | TC a
 122                 cast (a :: a^) = pure a
 123                 cast_ =  fail "Something went horribly wrong"
 124         (=.) a b = cast $ a >>= \(Var i)->b >>= \v->modify (\s->{s & variables=updateAt i (dynamic v) s.variables})
 125
 126 :: SemState =
 127         { onShip      :: [String]
 128         , onQuay      :: [String]
 129         , craneUp     :: Bool
 130         , craneOnQuay :: Bool
 131         , locked      :: Maybe String
 132         , variables   :: [Dynamic]
 133         }
 134
 135 state0 =
 136         { onShip = []
 137         , onQuay = ["apples","beer","camera's"]
 138         , craneUp = True
 139         , craneOnQuay = True
 140         , locked = Nothing
 141         , variables = []
 142         }
 143
 144 //Optimization
 145 :: BM a b =
 146         { t  :: a -> b
 147         , f  :: b -> a
 148         , t2 :: A.v: (v a) -> v b
 149         , f2 :: A.v: (v b) -> v a
 150         }
 151 bm :: BM a a
 152 bm = {t=id,f=id,t2=id,f2=id}
 153 :: Opt a
 154         //Actions
 155         = OMoveToShip (BM a (Step High High))
 156         | OMoveToQuay (BM a (Step High High))
 157         | OMoveUp (BM a (Step Low High))
 158         | OMoveDown (BM a (Step High Low))
 159         | OLock (BM a (Step Low Low))
 160         | OUnlock (BM a (Step Low Low))
 161         | E.e: OWait (BM a (Step e e))
 162         | E.e b: OWhile (BM b Bool) (BM a (Step e e)) (Opt b) (Opt a)
 163         | E.pre post inter: OSeq (BM a (Step pre post)) (Opt (Step pre inter)) (Opt (Step inter post))
 164         //Expressions
 165         | OContainersBelow (BM a Int)
 166         | E.b: OLit (BM a b) b                   & toString b
 167         | E.b: OLe (BM a Bool) (Opt b) (Opt b)   & Ord b
 168         | E.b: OGe (BM a Bool) (Opt b) (Opt b)   & Ord b
 169         | E.b: OPlus (BM a b) (Opt b) (Opt b)    & + b
 170         //Variables
 171         | E.b: OVar (BM a b) (Opt (Var b))       & TC b
 172         | E.b e: OAssign (BM a (Step e e)) (Opt (Var b)) (Opt b) & TC b
 173         | E.e b c: ODef (BM a (Step b c)) (Opt e) ((Opt (Var e)) -> (Opt (Step b c))) & TC e
 174
 175 instance action Opt
 176 where
 177         moveToShip = OMoveToShip bm
 178         moveToQuay = OMoveToQuay bm
 179         moveUp = OMoveUp bm
 180         moveDown = OMoveDown bm
 181         lock = OLock bm
 182         unlock = OUnlock bm
 183         wait = OWait bm
 184         (:.) a b = OSeq bm a b
 185         While a b = OWhile bm bm a b
 186
 187 instance expr Opt
 188 where
 189         containersBelow = OContainersBelow bm
 190         lit x = OLit bm x
 191         (<.) a b = OLe bm a b
 192         (>.) a b = OGe bm a b
 193         (+.) a b = OPlus bm a b
 194
 195 instance var Opt
 196 where
 197         def a b = ODef bm a b
 198         var v = OVar bm v
 199         (=.) a b = OAssign bm a b
 200
 201 opti :: (Opt a) -> v a | action, expr, var v
 202 //Action
 203 opti (OMoveToShip bm) = bm.f2 moveToShip
 204 opti (OMoveToQuay bm) = bm.f2 moveToQuay
 205 opti (OMoveDown bm) = bm.f2 moveDown
 206 opti (OMoveUp bm) = bm.f2 moveUp
 207 opti (OLock bm) = bm.f2 lock
 208 opti (OUnlock bm) = bm.f2 unlock
 209 opti (OWait bm) = bm.f2 wait
 210 opti (OWhile bm1 bm2 p a) = bm2.f2 (While (opti (bm1.t2 p)) (opti (bm2.t2 a)))
 211 //opti (OSeq bm1 (OWait bm2) r) =
 212 //opti (OSeq bm1 l (OWait bm2)) =
 213 opti (OSeq bm l r) = bm.f2 (opti l :. opti r)
 214 //Expr
 215 opti (OContainersBelow bm) = bm.f2 containersBelow
 216 opti (OLit bm x) = bm.f2 (lit x)
 217 opti (OLe bm x y) = bm.f2 (opti x <. opti y)
 218 opti (OGe bm x y) = bm.f2 (opti x >. opti y)
 219 opti (OPlus bm x y) = bm.f2 (opti x +. opti y)
 220 //Variables
 221 opti (OVar bm v) = bm.f2 (var (opti v))
 222 opti (OAssign bm a b) = bm.f2 (opti a =. opti b)
 223 //opti (ODef bm a b) = bm.f2 (def (opti a) \v->opti (b (OVar bm v))
 224
 225 Start :: [String]
 226 Start = runPrinter (opti (loadShip)) []
 227
 228 loadShip =
 229         While (containersBelow >. lit 0) (
 230                 moveDown:.
 231                 lock:.
 232                 moveUp:.
 233                 moveToShip:.
 234                 wait:.
 235                 moveDown:.
 236                 wait:.
 237                 unlock:.
 238                 moveUp:.
 239                 moveToQuay
 240         )
 241
 242 loadShip2 =
 243         def containersBelow \n.
 244         def (lit 0) \m.
 245         While (var n >. lit 0) (
 246                 moveDown:.
 247                 lock:.
 248                 moveUp:.
 249                 moveToShip:.
 250                 wait:.
 251                 moveDown:.
 252                 wait:.
 253                 unlock:.
 254                 moveUp:.
 255                 moveToQuay:.
 256                 n =. var n +. lit (-1)
 257         )