From: Mart Lubbers <mart@martlubbers.net>
Date: Thu, 6 Dec 2018 10:56:50 +0000 (+0100)
Subject: try optiE
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=a6430be4c031085335f00380efc7d0a135d55a16;p=clean-tests.git

try optiE
'
---

diff --git a/afp/a10/a10.icl b/afp/a10/a10.icl
index 1da0267..9a44cd8 100644
--- 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
--- 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) (