From 728c5d66f20c4b243dae105cff5df5b3207b8875 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Tue, 27 Nov 2018 16:55:16 +0100 Subject: [PATCH] new a10A --- afp/a10/a10.icl | 242 +++++++++++++++----------------------------- afp/a10/setGADT.icl | 182 +++++++++++++++++++++++++++++++++ afp/a9/a9.icl | 10 +- 3 files changed, 268 insertions(+), 166 deletions(-) create mode 100644 afp/a10/setGADT.icl 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 = -- 2.20.1