X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=afp%2Fa10%2Fa10.icl;h=9a44cd8348c258da3c2c0b9d1c86bd02fb194ea9;hb=95e99be6bdd04513688b88f1afaefac360eeff1d;hp=c561796982d542e29ffdcda914643d977b504300;hpb=728c5d66f20c4b243dae105cff5df5b3207b8875;p=clean-tests.git

diff --git a/afp/a10/a10.icl b/afp/a10/a10.icl
index c561796..9a44cd8 100644
--- a/afp/a10/a10.icl
+++ b/afp/a10/a10.icl
@@ -7,18 +7,24 @@ import Control.Applicative
 import Control.Monad
 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
 	= MoveToShip (BM b High) (BM a High)
 	| MoveToQuay (BM b High) (BM a High)
-	| MoveUp (BM b Low) (BM a High)
-	| MoveDown (BM b High) (BM a Low)
-	| Lock (BM b Low) (BM a Low)
-	| Unlock (BM b Low) (BM a Low)
-	| Wait (BM b a)
+	| MoveUp     (BM b Low)  (BM a High)
+	| MoveDown   (BM b High) (BM a Low)
+	| Lock       (BM b Low)  (BM a Low)
+	| Unlock     (BM b Low)  (BM a Low)
+	| Wait       (BM b a)
 	| E.i: (:.) infixl 1 (Action b i) (Action i a)
 	| WhileContainerBelow (BM b a) (Action a a)
 :: High = High
@@ -50,41 +56,84 @@ state0 =
 	}
 
 // ================
-:: Sem a = Sem ((MaybeErrorString State) -> MaybeErrorString State)
-
-
 eval :: (Action i f) State -> MaybeErrorString State
-eval (MoveToShip b1 b2) s = pure {s & craneOnQuay = False}
-eval (MoveToQuay b1 b2) s = pure {s & craneOnQuay = True}
-eval (MoveUp b1 b2)     s = pure {s & craneUp = True}
-eval (MoveDown b1 b2)   s = pure {s & craneUp = False}
-eval (Lock b1 b2) s=:{locked=Nothing}
-	| s.craneOnQuay =  
-	                =
-eval (Lock b1 b2) s=:{locked=Nothing} = Error ("Cannot lock new container, craner contains " + container)
-eval (Lock b1 b2) s=:{locked=(Just _)} = Error ("Cannot lock new container, craner contains " + container)
-	Nothing
-		| s.craneOnQuay
+eval (MoveToShip _ _) s = pure {s & craneOnQuay = False}
+eval (MoveToQuay _ _) s = pure {s & craneOnQuay = True}
+eval (MoveUp _ _)     s = pure {s & craneUp = True}
+eval (MoveDown _ _)   s = pure {s & craneUp = False}
+eval (Lock _ _)       s=:{locked=Nothing}
+	| s.craneOnQuay
 		= case s.onQuay of
 			[c:r] = pure {s & onQuay = r, locked = Just c}
 			[]    = Error "Cannot lock container on empty quay"
 		= case s.onShip of
 			[c:r] = pure {s & onShip = r, locked = Just c}
 			[]    = Error "Cannot lock container on empty ship"
-	Just container
-		= Error ("Cannot lock new container, craner contains " + container)
-eval (Unlock b1 b2)     s =case s.locked of
-	Just container | s.craneOnQuay
-		 = Result {s & onQuay = [container:s.onQuay], locked = Nothing}
-			 = Result {s & onShip = [container:s.onShip], locked = Nothing}
-			Nothing = Error "Cannot unlock container, craner contains nothing"
-		Wait bm = Result s
-		a :. b  = eval b (eval a r)
-		WhileContainerBelow bm action
-			| s.craneOnQuay && not (isEmpty s.onQuay) ||
-			  not s.craneOnQuay && not (isEmpty s.onShip)
-			= eval (action :. WhileContainerBelow bm action) r
-			= r
-*/
+eval (Lock _ _)       s=:{locked=(Just c)}
+	= Error ("Cannot lock new container, craner contains " +++ c)
+eval (Unlock _ _)     s=:{locked=(Just c)}
+	| s.craneOnQuay = pure {s & onQuay = [c:s.onQuay], locked = Nothing}
+	                = pure {s & onShip = [c:s.onShip], locked = Nothing}
+eval (Unlock b1 b2)   s=:{locked=Nothing}
+	= Error "Cannot unlock container, crane contains nothing"
+eval (Wait _)       s = Ok s
+eval (a :. b)       s = eval a s >>= eval b
+eval (WhileContainerBelow _ action) s
+	| s.craneOnQuay && not (isEmpty s.onQuay) || not s.craneOnQuay && not (isEmpty s.onShip)
+		= eval (action :. whileContainerBelow action) s
+	= pure s
+
+opt :: (Action a b) -> Action a b
+opt (WhileContainerBelow b a) = WhileContainerBelow b (opt a)
+opt (Wait bm :. b) = opt (bm.f2 b)
+opt (a :. Wait bm) = opt (bm.t2 a)
+opt (a :. b) = opt a :. opt b
+opt x = x
+
+Start = opt (moveToShip :. wait :. moveDown)
+//print :: (Action i f) [String] -> [String]
+//print (MoveToShip _ _) s = ["Move to ship":s]
+//print (MoveToQuay _ _) s = ["Move to quay":s]
+//print (MoveUp _ _)     s = ["Move up":s]
+//print (MoveDown _ _)   s = ["Move down":s]
+//print (Lock _ _)       s = ["Lock":s]
+//print (Unlock _ _)     s = ["Unlock":s]
+//print (Wait _)         s = ["Wait":s]
+//print (a :. b)         s = print a ["\n":print b s]
+//print (WhileContainerBelow _ a) s
+//	= ["While container below (":indent ["\n":print a [")":s]]]
+//where
+//	indent s = map (\s->if (s.[0] == '\n') (s +++ "\t") s)
+//
+
+print :: (Action i f) String [String] -> [String]
+print (MoveToShip _ _) i s = [i,"Move to ship":s]
+print (MoveToQuay _ _) i s = [i,"Move to quay":s]
+print (MoveUp _ _)     i s = [i,"Move up":s]
+print (MoveDown _ _)   i s = [i,"Move down":s]
+print (Lock _ _)       i s = [i,"Lock":s]
+print (Unlock _ _)     i s = [i,"Unlock":s]
+print (Wait _)         i s = [i,"Wait":s]
+print (a :. b)         i s = print a i ["\n":print b i s]
+print (WhileContainerBelow _ a) i s
+	= [i,"While container below (\n":print a ("\t"+++i) ["\n",i,")":s]]
+
+Start = print loadShip "" []
+
+p1 = moveToShip :. moveDown
+
+//p2 = moveToShip :. wait :. lock // the required type error
 
-Start = 42
+loadShip =
+	whileContainerBelow (
+		moveDown:.
+		lock:.
+		moveUp:.
+		moveToShip:.
+		wait:.
+		moveDown:.
+		wait:.
+		unlock:.
+		moveUp:.
+		moveToQuay
+	) :. wait