From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 27 Nov 2018 15:55:16 +0000 (+0100)
Subject: new a10A
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=728c5d66f20c4b243dae105cff5df5b3207b8875;p=clean-tests.git

new a10A
---

diff --git a/afp/a10/a10.icl b/afp/a10/a10.icl
index d96183c..c561796 100644
--- a/afp/a10/a10.icl
+++ b/afp/a10/a10.icl
@@ -1,174 +1,90 @@
 module a10
 
-/*
-  Advanced Progrmming 2018, Assignment 8
-  Pieter Koopman, pieter@cs.ru.nl
-*/
 import StdEnv
 
-import iTasks => qualified return, >>=, >>|, sequence, forever, :: Set
-
+import Data.Functor
 import Control.Applicative
 import Control.Monad
-import Control.Monad.State
-import Control.Monad.Trans
-import Data.Func
-import Data.List
-import Data.Functor
-import Data.Either
 import Data.Maybe
+import Data.Error
 
-import Text => qualified join
-
-import qualified Data.List as List
-import qualified Data.Map as Map
-
-::  BM a b = { t :: a -> b, f :: b -> a, t2 :: A.t: (t a) -> (t b), f2 :: A.t: (t b) -> (t a)}
-
-bm :: BM a a
+:: 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}
 
-:: Expr a
-  = E.e: New        (BM a [e])   [e]                             & Ord, toString e 
-  | E.e: Lit        (BM a e)     e                               & toString e
-  | E.e: Variable   (BM a e)     Ident                           & TC e
-  | E.e: Size       (BM a Int)   (Expr [e])                      & toString e
-  | E.e: Plus       (BM a e)     (Expr e)   (Expr e)             & + e
-  | E.e: Minus      (BM a e)     (Expr e)   (Expr e)             & - e
-  | E.e: Times      (BM a e)     (Expr e)   (Expr e)             & * e
-  | E.e: Union      (BM a [e])   (Expr [e]) (Expr [e])           & Eq, Ord e
-  | E.e: Difference (BM a [e])   (Expr [e]) (Expr [e])           & Eq, Ord e
-  | E.e: Intersect  (BM a [e])   (Expr [e]) (Expr [e])           & Eq, Ord e
-  | E.e: Remove     (BM a [e])   (Expr e)   (Expr [e])           & Eq e
-  | E.e: Insert     (BM a [e])   (Expr e)   (Expr [e])           & Eq e
-  | E.e: Scale      (BM a [e])   (Expr e)   (Expr [e])           & * e
-  | E.e: Assign     (BM a e)     Ident (Expr e)                  & TC e
-  |      Not        (BM a Bool)  (Expr Bool)
-  |      And        (BM a Bool)  (Expr Bool)(Expr Bool)
-  |      Or         (BM a Bool)  (Expr Bool)(Expr Bool)
-  | E.e: ElemOf     (BM a Bool)  (Expr e)   (Expr [e])           & Eq e
-  | E.e: Equals     (BM a Bool)  (Expr e)   (Expr e)             & Eq e
-  | E.e: LesEquals  (BM a Bool)  (Expr e)   (Expr e)             & Ord e
-  | E.e: Expr       (BM a ())    (Expr e)
-  | E.e: For        (BM a ())    String (Expr [e]) (Expr ())     & TC e
-  | E.e: If         (BM a ())    (Expr Bool) (Expr ()) (Expr ())
-  |      Seq        (BM a ())    (Expr ()) (Expr ())
-
-// === Smart constructors
-new e = New bm e
-lit e = Lit bm e
-var e = Variable bm e
-size e = Size bm e
-(+.) infixl 6
-(+.) a b = Plus bm a b
-(-.) infixl 6
-(-.) a b = Minus bm a b
-(*.) infixl 6
-(*.) a b = Times bm a b
-union a b = Union bm a b
-difference a b = Difference bm a b
-intersect a b = Intersect bm a b
-remove a b = Remove bm a b
-insert a b = Insert bm a b
-scale a b = Scale bm a b
-(=.) infixl 2
-(=.) a b = Assign bm a b
-instance ~ (Expr Bool) where ~ a = Not bm a
-(&&.) infixr 2
-(&&.) a b = And bm a b
-(||.) infixr 2
-(||.) a b = Or bm a b
-(In) infix 4
-(In) a b = ElemOf bm a b
-(==.) infix 4
-(==.) a b = Equals bm a b
-(<=.) infix 4
-(<=.) a b = LesEquals bm a b
-expr a = Expr bm a
-for a b c = For bm a b c
-iff a b c = If bm a b c
-(:.) infixl 1
-(:.) a b = Seq bm a b
-
-:: Ident  :== String
-
-// === State
-:: Val :== Either Int [Int]
-:: SemState :== 'Map'.Map String Dynamic
-:: Sem a :== StateT SemState (Either String) a
-
-store :: Ident a -> Sem a | TC a
-store k v = modify ('Map'.put k (dynamic v)) *> pure v
-
-read :: Ident -> Sem a | TC a
-read k = gets ('Map'.get k) >>= \v->case v of
-	(Just (a :: a^)) = pure a
-	(Just _) = fail "Type mismatch in read"
-	Nothing = fail "No variable with that identifier"
-
-fail :: String -> Sem a
-fail s = liftT (Left s)
-
-eval :: (Expr e) -> Sem e
-eval (New {f2} s)          = f2 $ pure s
-eval (Lit {f2} i)          = f2 $ pure i
-eval (Variable {f2} i)     = f2 $ read i
-eval (Size {f2} s)         = f2 $ length <$> eval s
-eval (Plus {f2} a b)       = f2 $ (+) <$> eval a <*> eval b
-eval (Minus {f2} a b)      = f2 $ (-) <$> eval a <*> eval b
-eval (Times {f2} a b)      = f2 $ (*) <$> eval a <*> eval b
-eval (Union {f2} a b)      = f2 $ 'List'.union <$> eval a <*> eval b
-eval (Difference {f2} a b) = f2 $ 'List'.difference <$> eval a <*> eval b
-eval (Intersect {f2} a b)  = f2 $ 'List'.intersect <$> eval a <*> eval b
-eval (Remove {f2} a b)     = f2 $ 'List'.delete <$> eval a <*> eval b
-eval (Insert {f2} a b)     = f2 $ 'List'.union <$> (pure <$> eval a) <*> eval b
-eval (Scale {f2} a b)      = f2 $ (map o (*)) <$> eval a <*> eval b
-eval (Assign {f2} v b)     = f2 $ eval b >>= store v
-eval (Not {f2} b)          = f2 $ not <$> eval b
-eval (And {f2} b1 b2)      = f2 $ (&&) <$> eval b1 <*> eval b2
-eval (Or {f2} b1 b2)       = f2 $ (||) <$> eval b1 <*> eval b2
-eval (ElemOf {f2} e s)     = f2 $ 'List'.elem <$> eval e <*> eval s
-eval (Equals {f2} e1 e2)   = f2 $ (==) <$> eval e1 <*> eval e2
-eval (LesEquals {f2} e1 e2)= f2 $ (<=) <$> eval e2 <*> eval e2
-eval (Expr {f2} e)         = f2 $ eval e *> pure ()
-eval (For {f2} i bag b)    = f2 $ eval bag >>= foldr proc (pure ())
-where
-	//Needed to convince the compiler that there is a TC of e
-	proc :: e (Sem ()) -> Sem () | TC e
-	proc e m = store i e *> eval b *> m
-eval (If {f2} p t e)       = f2 $ eval p >>= \v->eval if v t e
-eval (Seq {f2} l r)        = f2 $ eval l *> eval r *> pure ()
-
-print :: (Expr e) [String] -> [String]
-print (New _ s)          c = ["[":'List'.intersperse "," $ map toString s] ++ ["]":c]
-print (Lit _ i)          c = [toString i:c]
-print (Variable _ i)     c = [i:c]
-print (Size _ s)         c = ["size(":print s [")":c]]
-print (Plus _ a b)       c = print a ["+":print b c]
-print (Minus _ a b)      c = print a ["-":print b c]
-print (Times _ a b)      c = print a ["*":print b c]
-print (Union _ a b)      c = print a ["+":print b c]
-print (Difference _ a b) c = print a ["-":print b c]
-print (Intersect _ a b)  c = print a ["*":print b c]
-print (Remove _ a b)     c = print a ["-":print b c]
-print (Insert _ a b)     c = print a ["+":print b c]
-print (Scale _ a b)      c = print a ["*":print b c]
-print (Assign _ v b)     c = [v,"=":print b c]
-print (Not _ b)          c = ["not":print b c]
-print (And _ a b)        c = print a ["&&":print b c]
-print (Or _ a b)         c = print a ["||":print b c]
-print (ElemOf _ a b)     c = print a ["in":print b c]
-print (Equals _ a b)     c = print a ["==":print b c]
-print (LesEquals _ a b)  c = print a ["<=":print b c]
-print (Expr _ e)         c = print e c
-print (For _ i bag b)    c = ["For",i,"in":print bag ["do":print b c]]
-print (If _ p t e)       c = ["If":print p ["then":print t ["else":print e c]]]
-print (Seq _ l r)        c = print l ["\n":print r c]
+:: 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)
+	| E.i: (:.) infixl 1 (Action b i) (Action i a)
+	| WhileContainerBelow (BM b a) (Action a a)
+:: High = High
+:: Low = Low
+
+moveToShip = MoveToShip bm bm
+moveToQuay = MoveToQuay bm bm
+moveUp     = MoveUp     bm bm
+moveDown   = MoveDown   bm bm
+lock       = Lock       bm bm
+unlock     = Unlock     bm bm
+wait       = Wait       bm
+whileContainerBelow = WhileContainerBelow bm
+
+:: State =
+	{ onShip      :: [String]
+	, onQuay      :: [String]
+	, craneUp     :: Bool
+	, craneOnQuay :: Bool
+	, locked      :: Maybe String
+	}
+
+state0 =
+	{ onShip = []
+	, onQuay = ["apples","beer","camera's"]
+	, craneUp = True
+	, craneOnQuay = True
+	, locked = Nothing
+	}
+
+// ================
+:: 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
+		= 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
+*/
 
-Start :: (Either String (), String)
-Start =
-	(evalStateT (eval stmt) 'Map'.newMap
-	,"\n" +++ 'Text'.join " " (print stmt [])
-	)
-where
-	stmt = expr ("x" =. new [42]) :. expr (lit 42 +. var "x")
+Start = 42
diff --git a/afp/a10/setGADT.icl b/afp/a10/setGADT.icl
new file mode 100644
index 0000000..144f0a7
--- /dev/null
+++ b/afp/a10/setGADT.icl
@@ -0,0 +1,182 @@
+module a10
+
+/*
+  Advanced Progrmming 2018, Assignment 8
+  Pieter Koopman, pieter@cs.ru.nl
+*/
+import StdEnv
+
+import iTasks => qualified return, >>=, >>|, sequence, forever, :: Set
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.State
+import Control.Monad.Trans
+import Data.Func
+import Data.List
+import Data.Functor
+import Data.Either
+import Data.Maybe
+
+import Text => qualified join
+
+import qualified Data.List as List
+import qualified Data.Map as Map
+
+::  BM a b = { t :: a -> b, f :: b -> a, t2 :: A.t: (t a) -> (t b), f2 :: A.t: (t b) -> (t a)}
+
+bm :: BM a a
+bm = {t = id, f = id, t2 = id, f2 = id}
+
+:: Expr a
+  = E.e: New        (BM a [e])   [e]                             & Eq, Ord, toString e 
+  | E.e: Lit        (BM a e)     e                               & toString e
+  | E.e: Variable   (BM a e)     Ident                           & TC e
+  | E.e: Size       (BM a Int)   (Expr [e])                      & toString e
+  | E.e: Plus       (BM a e)     (Expr e)   (Expr e)             & + e
+  | E.e: Minus      (BM a e)     (Expr e)   (Expr e)             & - e
+  | E.e: Times      (BM a e)     (Expr e)   (Expr e)             & * e
+  | E.e: Union      (BM a [e])   (Expr [e]) (Expr [e])           & Eq, Ord e
+  | E.e: Difference (BM a [e])   (Expr [e]) (Expr [e])           & Eq, Ord e
+  | E.e: Intersect  (BM a [e])   (Expr [e]) (Expr [e])           & Eq, Ord e
+  | E.e: Remove     (BM a [e])   (Expr e)   (Expr [e])           & Eq e
+  | E.e: Insert     (BM a [e])   (Expr e)   (Expr [e])           & Eq e
+  | E.e: Scale      (BM a [e])   (Expr e)   (Expr [e])           & * e
+  | E.e: Assign     (BM a e)     Ident (Expr e)                  & TC e
+  |      Not        (BM a Bool)  (Expr Bool)
+  |      And        (BM a Bool)  (Expr Bool)(Expr Bool)
+  |      Or         (BM a Bool)  (Expr Bool)(Expr Bool)
+  | E.e: ElemOf     (BM a Bool)  (Expr e)   (Expr [e])           & Eq e
+  | E.e: Equals     (BM a Bool)  (Expr e)   (Expr e)             & Eq e
+  | E.e: LesEquals  (BM a Bool)  (Expr e)   (Expr e)             & Ord e
+  | E.e: Expr       (BM a ())    (Expr e)
+  | E.e: For        (BM a ())    String (Expr [e]) (Expr ())     & TC e
+  | E.e: If         (BM a ())    (Expr Bool) (Expr ()) (Expr ())
+  |      Seq        (BM a ())    (Expr ()) (Expr ())
+
+// === Smart constructors
+new e = New bm e
+lit e = Lit bm e
+var e = Variable bm e
+size e = Size bm e
+(+.) infixl 6
+(+.) a b = Plus bm a b
+(-.) infixl 6
+(-.) a b = Minus bm a b
+(*.) infixl 6
+(*.) a b = Times bm a b
+union a b = Union bm a b
+difference a b = Difference bm a b
+intersect a b = Intersect bm a b
+remove a b = Remove bm a b
+insert a b = Insert bm a b
+scale a b = Scale bm a b
+(=.) infixl 2
+(=.) a b = Assign bm a b
+instance ~ (Expr Bool) where ~ a = Not bm a
+(&&.) infixr 2
+(&&.) a b = And bm a b
+(||.) infixr 2
+(||.) a b = Or bm a b
+(In) infix 4
+(In) a b = ElemOf bm a b
+(==.) infix 4
+(==.) a b = Equals bm a b
+(<=.) infix 4
+(<=.) a b = LesEquals bm a b
+expr a = Expr bm a
+for a b c = For bm a b c
+iff a b c = If bm a b c
+(:.) infixl 1
+(:.) a b = Seq bm a b
+
+:: Ident  :== String
+
+// === State
+:: Val :== Either Int [Int]
+:: SemState :== 'Map'.Map String Dynamic
+:: Sem a :== StateT SemState (Either String) a
+
+store :: Ident a -> Sem a | TC a
+store k v = modify ('Map'.put k (dynamic v)) *> pure v
+
+read :: Ident -> Sem a | TC a
+read k = gets ('Map'.get k) >>= \v->case v of
+	(Just (a :: a^)) = pure a
+	(Just a) = fail
+		(   "Type mismatch... expected: "
+		+++ toString (undef :: a^)
+		+++ " got: "
+		+++ printType a
+		)
+	Nothing = fail ("No variable with ident " +++ k)
+where
+	printType :: Dynamic -> String
+	printType a = toString (typeCodeOfDynamic a)
+
+fail :: String -> Sem a
+fail s = liftT (Left s)
+
+eval :: (Expr e) -> Sem e
+eval (New {f,f2} s)        = f2 $ pure ('List'.nub s)
+eval (Lit {f2} i)          = f2 $ pure i
+eval (Variable {f2} i)     = f2 $ read i
+eval (Size {f2} s)         = f2 $ length <$> eval s
+eval (Plus {f2} a b)       = f2 $ (+) <$> eval a <*> eval b
+eval (Minus {f2} a b)      = f2 $ (-) <$> eval a <*> eval b
+eval (Times {f2} a b)      = f2 $ (*) <$> eval a <*> eval b
+eval (Union {f2} a b)      = f2 $ 'List'.union <$> eval a <*> eval b
+eval (Difference {f2} a b) = f2 $ 'List'.difference <$> eval a <*> eval b
+eval (Intersect {f2} a b)  = f2 $ 'List'.intersect <$> eval a <*> eval b
+eval (Remove {f2} a b)     = f2 $ 'List'.delete <$> eval a <*> eval b
+eval (Insert {f2} a b)     = f2 $ 'List'.union <$> (pure <$> eval a) <*> eval b
+eval (Scale {f2} a b)      = f2 $ (map o (*)) <$> eval a <*> eval b
+eval (Assign {f2} v b)     = f2 $ eval b >>= store v
+eval (Not {f2} b)          = f2 $ not <$> eval b
+eval (And {f2} b1 b2)      = f2 $ (&&) <$> eval b1 <*> eval b2
+eval (Or {f2} b1 b2)       = f2 $ (||) <$> eval b1 <*> eval b2
+eval (ElemOf {f2} e s)     = f2 $ 'List'.elem <$> eval e <*> eval s
+eval (Equals {f2} e1 e2)   = f2 $ (==) <$> eval e1 <*> eval e2
+eval (LesEquals {f2} e1 e2)= f2 $ (<=) <$> eval e2 <*> eval e2
+eval (Expr {f2} e)         = f2 $ eval e *> pure ()
+eval (For {f2} i bag b)    = f2 $ eval bag >>= foldr proc (pure ())
+where
+	//Needed to convince the compiler that there is a TC of e
+	proc :: e (Sem ()) -> Sem () | TC e
+	proc e m = store i e *> eval b *> m
+eval (If {f2} p t e)       = f2 $ eval p >>= \v->eval if v t e
+eval (Seq {f2} l r)        = f2 $ eval l *> eval r *> pure ()
+
+print :: (Expr e) [String] -> [String]
+print (New _ s)          c = ["[":'List'.intersperse "," $ map toString s] ++ ["]":c]
+print (Lit _ i)          c = [toString i:c]
+print (Variable _ i)     c = [i:c]
+print (Size _ s)         c = ["size(":print s [")":c]]
+print (Plus _ a b)       c = print a ["+":print b c]
+print (Minus _ a b)      c = print a ["-":print b c]
+print (Times _ a b)      c = print a ["*":print b c]
+print (Union _ a b)      c = print a ["+":print b c]
+print (Difference _ a b) c = print a ["-":print b c]
+print (Intersect _ a b)  c = print a ["*":print b c]
+print (Remove _ a b)     c = print a ["-":print b c]
+print (Insert _ a b)     c = print a ["+":print b c]
+print (Scale _ a b)      c = print a ["*":print b c]
+print (Assign _ v b)     c = [v,"=":print b c]
+print (Not _ b)          c = ["not":print b c]
+print (And _ a b)        c = print a ["&&":print b c]
+print (Or _ a b)         c = print a ["||":print b c]
+print (ElemOf _ a b)     c = print a ["in":print b c]
+print (Equals _ a b)     c = print a ["==":print b c]
+print (LesEquals _ a b)  c = print a ["<=":print b c]
+print (Expr _ e)         c = print e c
+print (For _ i bag b)    c = ["For",i,"in":print bag ["do":print b c]]
+print (If _ p t e)       c = ["If":print p ["then":print t ["else":print e c]]]
+print (Seq _ l r)        c = print l ["\n":print r c]
+
+Start :: (Either String (), String)
+Start =
+	(evalStateT (eval stmt) 'Map'.newMap
+	,"\n" +++ 'Text'.join " " (print stmt [])
+	)
+where
+	stmt = expr ("x" =. new [42]) :. expr (lit 42 +. var "x")
diff --git a/afp/a9/a9.icl b/afp/a9/a9.icl
index 5614d69..d89b07b 100644
--- a/afp/a9/a9.icl
+++ b/afp/a9/a9.icl
@@ -219,10 +219,14 @@ logical :: Logical -> Stmt
 logical e = {evaluator = e.evaluator *> pure (), printer = e.printer}
 
 For :: String Set Stmt -> Stmt
-For i e s =
-	{ evaluator = (i =. e).evaluator *> s.evaluator
-	, printer   = \c->["For",i,"=":e.printer ["In":s.printer c]]
+For ident bag body =
+	{ evaluator = bag.evaluator >>= \v->
+		foldr proc (pure ()) [ident =. integer e\\e<-v]
+	, printer   = \c->["For",ident,"=":bag.printer ["In":body.printer c]]
 	}
+where
+	proc :: (Sem Int) (StateT SemState (Either String) ()) -> StateT SemState (Either String) ()
+	proc e m = e.evaluator *> body.evaluator *> m
 
 If :: Logical Stmt Stmt -> Stmt
 If l s1 s2 =