begonnen met gadt
authorMart Lubbers <mart@martlubbers.net>
Sun, 13 Dec 2015 20:09:43 +0000 (21:09 +0100)
committerMart Lubbers <mart@martlubbers.net>
Sun, 13 Dec 2015 20:09:43 +0000 (21:09 +0100)
a12/mart/skeleton12.icl
a12/mart/skeleton12.prj
a12/mart/skeleton12_1-3.icl [new file with mode: 0644]

index 72c38a5..2ee5441 100644 (file)
 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]]
index 983035a..1121c8e 100644 (file)
@@ -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 (file)
index 0000000..72c38a5
--- /dev/null
@@ -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")
+*/