try optiE

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

diff --git a/afp/a11/a10.icl b/afp/a11/a11.icl
similarity index 66%
rename from afp/a11/a10.icl
rename to afp/a11/a11.icl
index 0344721..8c1600c 100644 (file)
--- a/afp/a11/a10.icl
+++ b/afp/a11/a11.icl
@@ -1,4 +1,4 @@
-module a10
+module a11
 
 import StdEnv
 
@@ -141,13 +141,89 @@ state0 =
        , variables = []
        }
 
-Start :: (String, Either String SemState, String, Either String SemState)
-Start =
-       ( concat $ runPrinter loadShip []
-       , execStateT loadShip state0
-       , concat $ runPrinter loadShip2 []
-       , execStateT loadShip2 state0
-       )
+//Optimization
+:: BM a b =
+       { t  :: a -> b
+       , f  :: b -> a
+       , 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))
+       | OMoveToQuay (BM a (Step High High))
+       | OMoveUp (BM a (Step Low High))
+       | OMoveDown (BM a (Step High Low))
+       | OLock (BM a (Step Low Low))
+       | OUnlock (BM a (Step Low Low))
+       | E.e: OWait (BM a (Step e e))
+       | E.e b: OWhile (BM b Bool) (BM a (Step e e)) (Opt b) (Opt a)
+       | E.pre post inter: OSeq (BM a (Step pre post)) (Opt (Step pre inter)) (Opt (Step inter post))
+       //Expressions
+       | OContainersBelow (BM a Int)
+       | E.b: OLit (BM a b) b                   & toString b
+       | E.b: OLe (BM a Bool) (Opt b) (Opt b)   & Ord b
+       | E.b: OGe (BM a Bool) (Opt b) (Opt b)   & Ord b
+       | E.b: OPlus (BM a b) (Opt b) (Opt b)    & + b
+       //Variables
+       | E.b: OVar (BM a b) (Opt (Var b))       & TC b
+       | E.b e: OAssign (BM a (Step e e)) (Opt (Var b)) (Opt b) & TC b
+       | E.e b c: ODef (BM a (Step b c)) (Opt e) ((Opt (Var e)) -> (Opt (Step b c))) & TC e
+
+instance action Opt
+where
+       moveToShip = OMoveToShip bm
+       moveToQuay = OMoveToQuay bm
+       moveUp = OMoveUp bm
+       moveDown = OMoveDown bm
+       lock = OLock bm
+       unlock = OUnlock bm
+       wait = OWait bm
+       (:.) a b = OSeq bm a b
+       While a b = OWhile bm bm a b
+
+instance expr Opt
+where
+       containersBelow = OContainersBelow bm
+       lit x = OLit bm x
+       (<.) a b = OLe bm a b
+       (>.) a b = OGe bm a b
+       (+.) a b = OPlus bm a b
+
+instance var Opt
+where
+       def a b = ODef bm a b
+       var v = OVar bm v
+       (=.) a b = OAssign bm a b
+
+opti :: (Opt a) -> v a | action, expr, var v
+//Action
+opti (OMoveToShip bm) = bm.f2 moveToShip
+opti (OMoveToQuay bm) = bm.f2 moveToQuay
+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 (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)) =
+opti (OSeq bm l r) = bm.f2 (opti l :. opti r)
+//Expr
+opti (OContainersBelow bm) = bm.f2 containersBelow
+opti (OLit bm x) = bm.f2 (lit x)
+opti (OLe bm x y) = bm.f2 (opti x <. opti y)
+opti (OGe bm x y) = bm.f2 (opti x >. opti y)
+opti (OPlus bm x y) = bm.f2 (opti x +. opti y)
+//Variables
+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)) []
        
 loadShip =
        While (containersBelow >. lit 0) (