update

[clean-tests.git] / afp / a11 / a11.icl

diff --git a/afp/a11/a11.icl b/afp/a11/a11.icl
index 8c1600c..f586122 100644 (file)
--- a/afp/a11/a11.icl
+++ b/afp/a11/a11.icl
@@ -85,7 +85,7 @@ fail s = liftT (Left s)
 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})
@@ -141,15 +141,12 @@ state0 =
        , 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))
@@ -180,7 +177,7 @@ where
        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
 
@@ -206,10 +203,19 @@ opti (OMoveDown bm) = bm.f2 moveDown
 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
@@ -221,9 +227,13 @@ opti (OPlus bm x y) = bm.f2 (opti x +. opti y)
 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) (