6 import Control.Applicative
7 import Control.Monad => qualified join
8 import Control.Monad.Trans
9 import Control.Monad.State
16 :: Step pre post = Step
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)
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)
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
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
48 :: Printer a = P (Int Int [String] -> [String])
49 runPrinter (P a) = a 0 0
51 word :: String -> Printer a
52 word s = P \v i c->[createArray i '\t',s:c]
54 instance action Printer
56 moveToShip = word "moveToShip"
57 moveToQuay = word "moveToQuay"
58 moveUp = word "moveUp"
59 moveDown = word "moveDown"
61 unlock = word "unlock"
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]]]
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]
74 varname i = "v" +++ toString i
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]]
79 (=.) (P a) (P b) = P \v i c->[createArray i '\t':a v i [" = ":b v i c]]
82 :: Eval a :== StateT SemState (Either String) a
83 cast f = f >>| pure Step
84 fail s = liftT (Left s)
86 instance action (StateT SemState (Either String))
88 moveToShip = 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"
105 (:.) x y = cast $ x >>| y
106 While x y = x >>= \b->if b (y :. (While x y)) (pure Step)
108 instance expr (StateT SemState (Either String))
110 containersBelow = gets (\s->length if s.craneOnQuay s.onQuay s.onShip)
112 (<.) x y = (<) <$> x <*> y
113 (>.) x y = (>) <$> x <*> y
114 (+.) x y = (+) <$> x <*> y
116 instance var (StateT SemState (Either String))
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
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})
130 , craneOnQuay :: Bool
131 , locked :: Maybe String
132 , variables :: [Dynamic]
137 , onQuay = ["apples","beer","camera's"]
147 { t2 :: A.v: (v a) -> v b
148 , f2 :: A.v: (v b) -> v a
152 = OMoveToShip (BM a (Step High High))
153 | OMoveToQuay (BM a (Step High High))
154 | OMoveUp (BM a (Step Low High))
155 | OMoveDown (BM a (Step High Low))
156 | OLock (BM a (Step Low Low))
157 | OUnlock (BM a (Step Low Low))
158 | E.e: OWait (BM a (Step e e))
159 | E.e b: OWhile (BM b Bool) (BM a (Step e e)) (Opt b) (Opt a)
160 | E.pre post inter: OSeq (BM a (Step pre post)) (Opt (Step pre inter)) (Opt (Step inter post))
162 | OContainersBelow (BM a Int)
163 | E.b: OLit (BM a b) b & toString b
164 | E.b: OLe (BM a Bool) (Opt b) (Opt b) & Ord b
165 | E.b: OGe (BM a Bool) (Opt b) (Opt b) & Ord b
166 | E.b: OPlus (BM a b) (Opt b) (Opt b) & + b
168 | E.b: OVar (BM a b) (Opt (Var b)) & TC b
169 | E.b e: OAssign (BM a (Step e e)) (Opt (Var b)) (Opt b) & TC b
170 | E.e b c: ODef (BM a (Step b c)) (Opt e) ((Opt (Var e)) -> (Opt (Step b c))) & TC e
174 moveToShip = OMoveToShip bm
175 moveToQuay = OMoveToQuay bm
177 moveDown = OMoveDown bm
181 (:.) a b = OSeq bm a b
182 While a b = OWhile bm bm a b
186 containersBelow = OContainersBelow bm
188 (<.) a b = OLe bm a b
189 (>.) a b = OGe bm a b
190 (+.) a b = OPlus bm a b
194 def a b = ODef bm a b
196 (=.) a b = OAssign bm a b
198 opti :: (Opt a) -> v a | action, expr, var v
200 opti (OMoveToShip bm) = bm.f2 moveToShip
201 opti (OMoveToQuay bm) = bm.f2 moveToQuay
202 opti (OMoveDown bm) = bm.f2 moveDown
203 opti (OMoveUp bm) = bm.f2 moveUp
204 opti (OLock bm) = bm.f2 lock
205 opti (OUnlock bm) = bm.f2 unlock
206 opti (OWait bm sbm) = bm.f2 wait
207 opti (OWhile bm1 bm2 p a) = bm2.f2 (While (opti (bm1.t2 p)) (opti (bm2.t2 a)))
208 //opti (OSeq bm1 (OWait bm2) r) =
210 l :: (Step pre inter)
211 | E.pre post inter: OSeq (BM a (Step pre post)) (Opt (Step pre inter)) (Opt (Step inter post))
212 bm2 :: BM (Step pre inter)
213 | E.e: OWait (BM (Step inter post) (Step post post)) (SBM inter post)
216 :: BM (Step pre inter) (Step pre post)
218 opti (OSeq bm1 l (OWait bm2 sbm)) = bm.f2 (opti (sbm.st2 l))
219 opti (OSeq bm l r) = bm.f2 (opti l :. opti r)
221 opti (OContainersBelow bm) = bm.f2 containersBelow
222 opti (OLit bm x) = bm.f2 (lit x)
223 opti (OLe bm x y) = bm.f2 (opti x <. opti y)
224 opti (OGe bm x y) = bm.f2 (opti x >. opti y)
225 opti (OPlus bm x y) = bm.f2 (opti x +. opti y)
227 opti (OVar bm v) = bm.f2 (var (opti v))
228 opti (OAssign bm a b) = bm.f2 (opti a =. opti b)
229 //opti (ODef bm a b) = bm.f2 (def (opti a) \v->opti (b (OVar bm v))
233 Start = runPrinter (opti (loadShip)) []
239 While (containersBelow >. lit 0) (
253 def containersBelow \n.
255 While (var n >. lit 0) (
266 n =. var n +. lit (-1)