From: Mart Lubbers Date: Sun, 13 Dec 2015 20:09:43 +0000 (+0100) Subject: begonnen met gadt X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=df46cbcb0b61b8b4a27e6ecda20dfe66abbd6f31;p=ap2015.git begonnen met gadt --- diff --git a/a12/mart/skeleton12.icl b/a12/mart/skeleton12.icl index 72c38a5..2ee5441 100644 --- a/a12/mart/skeleton12.icl +++ b/a12/mart/skeleton12.icl @@ -1,120 +1,32 @@ module skeleton12 -from Text import class Text, instance Text String -import Control.Applicative, Control.Monad -import Data.Maybe, Data.Functor -import StdInt, StdString, StdBool, StdList -import qualified Text - -class arith x where - lit :: a -> x a | toString a - (+.) infixl 6 :: (x a) (x a) -> x a | + a - (*.) infixl 7 :: (x a) (x a) -> x a | * a -class store x where - read :: (x Int) - write :: (x Int) -> x Int -class truth x where - (XOR) infixr 3 :: (x Bool) (x Bool) -> x Bool - -. :: (x Bool) -> x Bool -class (=.=) infix 4 x :: (x a) (x a) -> x Bool | == a -class except x where - throw :: (x a) - try :: (x a) (x a) -> x a - -class aexpr x | arith, store, except, =.= x -class bexpr x | arith, truth, except, =.= x -class expr x | aexpr, bexpr x - -instance * Bool where (*) b1 b2 = b1 && b2 -instance + Bool where (+) b1 b2 = b1 || b2 - - -//Section 1: Showing expressions -:: Show a = Show ([String] -> [String]) -instance arith Show where - lit x = Show \s.[toString x:s] - (+.) (Show x1) (Show x2) = Show \s.x1 ["+":x2 s] - (*.) (Show x1) (Show x2) = Show \s.x1 ["*":x2 s] -instance store Show where - read = Show \s.["read":s] - write (Show x) = Show \s.["write (":x [")":s]] -instance truth Show where - (XOR) (Show x1) (Show x2) = Show \s.x1 ["⊕":x2 s] - -. (Show x) = Show \s.["¬":x s] -instance =.= Show where - (=.=) (Show x1) (Show x2) = Show \s.x1 ["=":x2 s] -instance except Show where - throw = Show \s.["throw":s] - try (Show x1) (Show x2) = Show \s.["try (":x1 [") except (":x2 [")":s]]] - -show (Show f) = 'Text'.concat (f ["\n"]) - -//Section 2: Evaluation -:: Step a = Step (State -> (Maybe a, State)) -:: State :== Int - -instance Functor Step where - fmap f (Step s) = Step \st.let (x, st`)=s st in (fmap f x, st`) -instance Applicative Step where - pure s = Step \st.(pure s, st) - (<*>) x1 x2 = ap x1 x2 -instance Monad Step where - bind (Step s) f = Step \st.case s st of - (Just x, st`) = let (Step s`) = f x in s` st` - (_, st`) = (Nothing, st`) - -instance arith Step where - lit x = pure x - (+.) x1 x2 = (+) <$> x1 <*> x2 - (*.) x1 x2 = (*) <$> x1 <*> x2 -instance store Step where - read = Step \st.(Just st, st) - write (Step x) = Step \st.case x st of - (Just v`, _) = (Just v`, v`) - (_, st) = (Nothing, st) -instance truth Step where - (XOR) x1 x2 = (\x.(\y.x && not y || not x && y)) <$> x1 <*> x2 - -. x1 = (not) <$> x1 -instance =.= Step where - (=.=) x1 x2 = (==) <$> x1 <*> x2 -instance except Step where - throw = Step \st.(Nothing, st) - try (Step x1) (Step x2) = Step \st.case x1 st of - (Just v`, st`) = (Just v`, st) - (Nothing, st`) = x2 st` - -eval (Step f) = f 0 - -seven :: e Int | aexpr e -seven = lit 3 +. lit 4 - -throw1 :: e Int | expr e -throw1 = lit 3 +. throw - -six :: e Int | expr e -six = write (lit 3) +. read - -try1 :: e Int | expr e -try1 = try throw1 (lit 42) - -loge :: e Bool | expr e -loge = lit True *. -. (lit True) - -comp :: e Bool | expr e -comp = lit 1 =.= lit 2 XOR -. (-. (lit True)) - -Start = ( - (eval seven, show seven), - (eval throw1, show throw1), - (eval six, show six), - (eval try1, show try1), - (eval loge, show loge), - (eval comp, show comp)) -/* -((Just 7),0),"3+4"), -((Nothing,0),"3+throw"), -(((Just 6),3),"write (3)+read"), -(((Just 42),0),"try (3+throw) except (42)"), -(((Just False),0),"True*¬True"), -(((Just True),0),"1=2⊕¬¬True") -*/ +import StdEnv +import StdMaybe + +:: BM a b = {t :: a -> b, f :: b -> a} +bm :: BM a a +bm = {f=id, t=id} +:: Expr a + = Lit a + | (+.) infixl 6 (Expr a) (Expr a) + | (*.) infixl 6 (Expr a) (Expr a) + | Read + | Write (Expr Int) + | XOR (Expr Bool) (Expr Bool) + | Not (Expr Bool) + | E.b: Eq (Expr b) ( Expr b) & == b + | Throw + | Try (Expr a) (Expr a) + +class show a :: a [String] -> [String] +instance show (Expr a) where + show (Lit x) l = [toString x:l] + show (x1 +. x2) l = show x1 ["+":show x2 l] + show (x1 *. x2) l = show x1 ["*":show x2 l] + show Read l = ["Read":l] + show (Write x) l = ["Write (":show x [")":l]] + show (XOR x1 x2) l = show x1 ["XOR":show x2 l] + show (Not x) l = ["Not":show x l] + show (Eq x1 x2) l = show x1 ["==":show x2 l] + show Throw l = ["throw":l] + show (Try x1 x2) l = ["Try":show x1 ["Except":show x2 l]] diff --git a/a12/mart/skeleton12.prj b/a12/mart/skeleton12.prj index 983035a..1121c8e 100644 --- a/a12/mart/skeleton12.prj +++ b/a12/mart/skeleton12.prj @@ -448,8 +448,8 @@ OtherModules ReuseUniqueNodes: True Fusion: False Module - Name: Text - Dir: {Application}/lib/iTasks-SDK/Dependencies/Platform/OS-Independent + Name: _SystemDynamic + Dir: {Application}/lib/iTasks-SDK/Patches/Dynamics Compiler NeverMemoryProfile: False NeverTimeProfile: False @@ -462,8 +462,8 @@ OtherModules ReuseUniqueNodes: True Fusion: False Module - Name: _SystemDynamic - Dir: {Application}/lib/iTasks-SDK/Patches/Dynamics + Name: GenEq + Dir: {Application}/lib/iTasks-SDK/Patches/Generics Compiler NeverMemoryProfile: False NeverTimeProfile: False @@ -476,8 +476,8 @@ OtherModules ReuseUniqueNodes: True Fusion: False Module - Name: GenEq - Dir: {Application}/lib/iTasks-SDK/Patches/Generics + Name: StdGeneric + Dir: {Application}/lib/iTasks-SDK/Patches/StdEnv Compiler NeverMemoryProfile: False NeverTimeProfile: False @@ -490,8 +490,8 @@ OtherModules ReuseUniqueNodes: True Fusion: False Module - Name: StdGeneric - Dir: {Application}/lib/iTasks-SDK/Patches/StdEnv + Name: StdMaybe + Dir: {Application}/lib/iTasks-SDK/Server/lib Compiler NeverMemoryProfile: False NeverTimeProfile: False diff --git a/a12/mart/skeleton12_1-3.icl b/a12/mart/skeleton12_1-3.icl new file mode 100644 index 0000000..72c38a5 --- /dev/null +++ b/a12/mart/skeleton12_1-3.icl @@ -0,0 +1,120 @@ +module skeleton12 + +from Text import class Text, instance Text String +import Control.Applicative, Control.Monad +import Data.Maybe, Data.Functor +import StdInt, StdString, StdBool, StdList +import qualified Text + +class arith x where + lit :: a -> x a | toString a + (+.) infixl 6 :: (x a) (x a) -> x a | + a + (*.) infixl 7 :: (x a) (x a) -> x a | * a +class store x where + read :: (x Int) + write :: (x Int) -> x Int +class truth x where + (XOR) infixr 3 :: (x Bool) (x Bool) -> x Bool + -. :: (x Bool) -> x Bool +class (=.=) infix 4 x :: (x a) (x a) -> x Bool | == a +class except x where + throw :: (x a) + try :: (x a) (x a) -> x a + +class aexpr x | arith, store, except, =.= x +class bexpr x | arith, truth, except, =.= x +class expr x | aexpr, bexpr x + +instance * Bool where (*) b1 b2 = b1 && b2 +instance + Bool where (+) b1 b2 = b1 || b2 + + +//Section 1: Showing expressions +:: Show a = Show ([String] -> [String]) +instance arith Show where + lit x = Show \s.[toString x:s] + (+.) (Show x1) (Show x2) = Show \s.x1 ["+":x2 s] + (*.) (Show x1) (Show x2) = Show \s.x1 ["*":x2 s] +instance store Show where + read = Show \s.["read":s] + write (Show x) = Show \s.["write (":x [")":s]] +instance truth Show where + (XOR) (Show x1) (Show x2) = Show \s.x1 ["⊕":x2 s] + -. (Show x) = Show \s.["¬":x s] +instance =.= Show where + (=.=) (Show x1) (Show x2) = Show \s.x1 ["=":x2 s] +instance except Show where + throw = Show \s.["throw":s] + try (Show x1) (Show x2) = Show \s.["try (":x1 [") except (":x2 [")":s]]] + +show (Show f) = 'Text'.concat (f ["\n"]) + +//Section 2: Evaluation +:: Step a = Step (State -> (Maybe a, State)) +:: State :== Int + +instance Functor Step where + fmap f (Step s) = Step \st.let (x, st`)=s st in (fmap f x, st`) +instance Applicative Step where + pure s = Step \st.(pure s, st) + (<*>) x1 x2 = ap x1 x2 +instance Monad Step where + bind (Step s) f = Step \st.case s st of + (Just x, st`) = let (Step s`) = f x in s` st` + (_, st`) = (Nothing, st`) + +instance arith Step where + lit x = pure x + (+.) x1 x2 = (+) <$> x1 <*> x2 + (*.) x1 x2 = (*) <$> x1 <*> x2 +instance store Step where + read = Step \st.(Just st, st) + write (Step x) = Step \st.case x st of + (Just v`, _) = (Just v`, v`) + (_, st) = (Nothing, st) +instance truth Step where + (XOR) x1 x2 = (\x.(\y.x && not y || not x && y)) <$> x1 <*> x2 + -. x1 = (not) <$> x1 +instance =.= Step where + (=.=) x1 x2 = (==) <$> x1 <*> x2 +instance except Step where + throw = Step \st.(Nothing, st) + try (Step x1) (Step x2) = Step \st.case x1 st of + (Just v`, st`) = (Just v`, st) + (Nothing, st`) = x2 st` + +eval (Step f) = f 0 + +seven :: e Int | aexpr e +seven = lit 3 +. lit 4 + +throw1 :: e Int | expr e +throw1 = lit 3 +. throw + +six :: e Int | expr e +six = write (lit 3) +. read + +try1 :: e Int | expr e +try1 = try throw1 (lit 42) + +loge :: e Bool | expr e +loge = lit True *. -. (lit True) + +comp :: e Bool | expr e +comp = lit 1 =.= lit 2 XOR -. (-. (lit True)) + +Start = ( + (eval seven, show seven), + (eval throw1, show throw1), + (eval six, show six), + (eval try1, show try1), + (eval loge, show loge), + (eval comp, show comp)) +/* +((Just 7),0),"3+4"), +((Nothing,0),"3+throw"), +(((Just 6),3),"write (3)+read"), +(((Just 42),0),"try (3+throw) except (42)"), +(((Just False),0),"True*¬True"), +(((Just True),0),"1=2⊕¬¬True") +*/