From 4a40cf9861acc2b7e2cb94653d4ae7d28661508e Mon Sep 17 00:00:00 2001 From: bringert Date: Thu, 1 Dec 2005 11:30:15 +0000 Subject: [PATCH] Transfer: moved stuff around in prelude. Added some new simple instances. --- transfer/lib/prelude.tr | 166 +++++++++++++++++++++++++--------------- 1 file changed, 104 insertions(+), 62 deletions(-) diff --git a/transfer/lib/prelude.tr b/transfer/lib/prelude.tr index e452fcc66..9c4e1710b 100644 --- a/transfer/lib/prelude.tr +++ b/transfer/lib/prelude.tr @@ -15,16 +15,81 @@ id _ x = x -- --- The List type +-- The Integer type +-- + +-- Instances: + +num_Integer : Num Integer +num_Integer = rec zero = 0 + plus = prim_add_Int + minus = prim_sub_Int + one = 1 + times = prim_mul_Int + div = prim_div_Int + mod = prim_mod_Int + negate = prim_neg_Int + eq = prim_eq_Int + compare = prim_cmp_Int + +show_Integer : Show Integer +show_Integer = rec show = prim_show_Int + + + +-- +-- The String type +-- + +-- Instances: + +add_String : Add String +add_String = rec zero = "" + plus = prim_add_Str + + +ord_String : Ord String +ord_String = rec eq = prim_eq_Str + compare = prim_cmp_Str + +show_String : Show String +show_String = rec show = prim_show_Str + + +-- +-- The Bool type -- data Bool : Type where True : Bool False : Bool +-- derive Show Bool +-- derive Eq Bool +-- derive Ord Bool + not : Bool -> Bool not b = if b then False else True +-- Instances: + +neg_Bool : Neg Bool +neg_Bool = rec negate = not + +add_Bool : Add Bool +add_Bool = rec zero = False + plus = \x -> \y -> x || y + +mul_Bool : Add Bool +mul_Bool = rec one = True + times = \x -> \y -> x && y + + + + +-- +-- The List type +-- data List : (_:Type) -> Type where Nil : (A:Type) -> List A @@ -48,6 +113,20 @@ foldr : (A : Type) -> (B : Type) -> (A -> B -> B) -> B -> List A -> B foldr _ _ _ x (Nil _) = x foldr A B f x (Cons _ y ys) = f y (foldr A B f x ys) +-- Instances: + +add_List : (A : Type) -> Add (List A) +add_List A = rec zero = Nil A + plus = append A + + +monad_List : Monad List +monad_list = rec return = \A -> \x -> Cons A x (Nil A) + bind = \A -> \B -> \m -> \k -> concat B (map A B k m) + + + + -- -- The Maybe type @@ -57,6 +136,11 @@ data Maybe : Type -> Type where Nothing : (A : Type) -> Maybe A Just : (A : Type) -> A -> Maybe A +-- derive Show Maybe +-- derive Eq Maybe +-- derive Ord Maybe + + fromMaybe : (A : Type) -> A -> Maybe A -> A fromMaybe _ x Nothing = x fromMaybe _ _ (Just x) = x @@ -66,6 +150,19 @@ maybe _ _ x _ Nothing = x maybe _ _ _ f (Just x) = f x +-- Instances: + +monad_Maybe : Monad Maybe +monad_Maybe = + rec return = Just + bind = \A -> \B -> \m -> \k -> + case m of + Nothing _ -> Nothing B + Just _ x -> k x + + + + -- -- The Num class -- @@ -82,19 +179,8 @@ Num = sig zero : A eq : A -> A -> Bool compare : A -> A -> Ordering --- Instances: -num_Integer : Num Integer -num_Integer = rec zero = 0 - plus = prim_add_Int - minus = prim_sub_Int - one = 1 - times = prim_mul_Int - div = prim_div_Int - mod = prim_mod_Int - negate = prim_neg_Int - eq = prim_eq_Int - compare = prim_cmp_Int + -- -- The Add class @@ -120,17 +206,9 @@ sum A d = foldr A A d.plus d.zero (x + y) => (plus ? ? x y) -} --- Instances: --- num_Integer -add_String : Add String -add_String = rec zero = "" - plus = prim_add_Str -add_List : (A : Type) -> Add (List A) -add_List A = rec zero = Nil A - plus = append A -- -- The Sub class @@ -142,9 +220,8 @@ Sub = sig minus : A -> A -> A minus : (A : Type) -> Sub A -> A minus _ d = d.minus --- Instances: --- num_Integer + -- @@ -170,9 +247,7 @@ product A d = foldr A A d.times d.one (x * y) => (times ? ? x y) -} --- Instances: --- num_Integer -- @@ -196,9 +271,7 @@ mod _ d = d.mod (x % y) => (mod ? ? x y) -} --- Instances: --- num_Integer @@ -218,12 +291,6 @@ negate _ d = d.neg (-x) => negate ? ? x -} --- Instances: - --- num_Integer - -neg_Bool : Neg Bool -neg_Bool = rec negate = not @@ -248,12 +315,7 @@ neq A d x y = not (eq A d x y) (x /= y) => (neq ? ? x y) -} --- Instances: --- num_Integer - -eq_String : Eq String -eq_String = rec eq = prim_eq_Str @@ -297,13 +359,8 @@ gt = ordOp (\o -> case o of { GT -> True; _ -> False }) (x > y) => (gt ? ? x y) -} --- Instances: --- num_Integer -ord_String : Ord String -ord_String = rec eq = prim_eq_Str - compare = prim_cmp_Str @@ -318,13 +375,7 @@ show : (A : Type) -> Show A -> A -> String show _ d = d.show --- Instances: -show_Integer : Show Integer -show_Integer = rec show = prim_show_Int - -show_String : Show String -show_String = rec show = prim_show_Str @@ -338,6 +389,7 @@ Monoid = sig mzero : A + -- -- The Compos class -- @@ -356,6 +408,9 @@ composFold : (C : Type) -> (T : C -> Type) -> (d : Compos C T) -> (B : Type) -> composFold _ _ d = d.composFold + + + -- -- The Monad class -- @@ -378,16 +433,3 @@ bind _ d = d.bind (x >> y) => bind ? ? ? ? x (\_ -> y) -} --- Instances: - -monad_List : Monad List -monad_list = rec return = \A -> \x -> Cons A x (Nil A) - bind = \A -> \B -> \m -> \k -> concat B (map A B k m) - -monad_Maybe : Monad Maybe -monad_Maybe = - rec return = Just - bind = \A -> \B -> \m -> \k -> - case m of - Nothing _ -> Nothing B - Just _ x -> k x