runEval = runStateT
instance action (StateT SemState (Either String))
where
- moveToShip = cast $ modify (\s->{s & craneOnQuay=False})
+ moveToShip = modify (\s->{s & craneOnQuay=False})
moveToQuay = cast $ modify (\s->{s & craneOnQuay=True})
moveUp = cast $ modify (\s->{s & craneUp=True})
moveDown = cast $ modify (\s->{s & craneUp=False})
, variables = []
}
+/*
//Optimization
:: BM a b =
- { t :: a -> b
- , f :: b -> a
- , t2 :: A.v: (v a) -> v b
+ { t2 :: A.v: (v a) -> v b
, f2 :: A.v: (v b) -> v a
}
-bm :: BM a a
-bm = {t=id,f=id,t2=id,f2=id}
:: Opt a
//Actions
= OMoveToShip (BM a (Step High High))
moveDown = OMoveDown bm
lock = OLock bm
unlock = OUnlock bm
- wait = OWait bm
+ wait = OWait bm sbm
(:.) a b = OSeq bm a b
While a b = OWhile bm bm a b
opti (OMoveUp bm) = bm.f2 moveUp
opti (OLock bm) = bm.f2 lock
opti (OUnlock bm) = bm.f2 unlock
-opti (OWait bm) = bm.f2 wait
+opti (OWait bm sbm) = bm.f2 wait
opti (OWhile bm1 bm2 p a) = bm2.f2 (While (opti (bm1.t2 p)) (opti (bm2.t2 a)))
//opti (OSeq bm1 (OWait bm2) r) =
-//opti (OSeq bm1 l (OWait bm2)) =
+/*
+l :: (Step pre inter)
+| E.pre post inter: OSeq (BM a (Step pre post)) (Opt (Step pre inter)) (Opt (Step inter post))
+bm2 :: BM (Step pre inter)
+| E.e: OWait (BM (Step inter post) (Step post post)) (SBM inter post)
+
+need:
+:: BM (Step pre inter) (Step pre post)
+*/
+opti (OSeq bm1 l (OWait bm2 sbm)) = bm.f2 (opti (sbm.st2 l))
opti (OSeq bm l r) = bm.f2 (opti l :. opti r)
//Expr
opti (OContainersBelow bm) = bm.f2 containersBelow
opti (OVar bm v) = bm.f2 (var (opti v))
opti (OAssign bm a b) = bm.f2 (opti a =. opti b)
//opti (ODef bm a b) = bm.f2 (def (opti a) \v->opti (b (OVar bm v))
+//
Start :: [String]
Start = runPrinter (opti (loadShip)) []
+*/
+
+Start = 42
loadShip =
While (containersBelow >. lit 0) (