try optiE

'

diff --git a/afp/a10/a10.icl b/afp/a10/a10.icl
index 1da0267..9a44cd8 100644 (file)
--- a/afp/a10/a10.icl
+++ b/afp/a10/a10.icl
@@ -9,7 +9,12 @@ import Data.Maybe
 import Data.Error
 import Text => qualified join
 
-:: BM a b = {t :: a->b, f :: b->a, t2 :: A.c t:(t c a)->t c b, f2 :: A.c t:(t b c)->t a c}
+:: BM a b =
+       { t :: a->b
+       , f :: b->a
+       , t2 :: A.c t:(t c a)->t c b
+       , f2 :: A.c t:(t b c)->t a c
+       }
 bm = {t = id, f = id, t2 = id, f2 = id}
 
 :: Action b a

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) (