X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=afp%2Fa11%2Fa11.icl;fp=afp%2Fa11%2Fa11.icl;h=f586122531f613aa99403f869a51175dc184eec2;hb=01bad43f6e31dfb1ff59371ed264e94397745df9;hp=8c1600c3b44b414aab9c3086e700a1e201bcebfc;hpb=3842e90cb6c88f3073c433d30b52c3e2985df521;p=clean-tests.git

diff --git a/afp/a11/a11.icl b/afp/a11/a11.icl
index 8c1600c..f586122 100644
--- 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) (