From 86df2a69b149c1f4ff2cb9139447f5a6faccd483 Mon Sep 17 00:00:00 2001 From: bringert Date: Wed, 30 Nov 2005 15:51:43 +0000 Subject: [PATCH] Moved class stuff to prelude. --- src/Transfer/SyntaxToCore.hs | 2 +- transfer/examples/overload.tr | 157 ------------------------- transfer/examples/prelude.tr | 214 +++++++++++++++++++++++++++++++++- 3 files changed, 214 insertions(+), 159 deletions(-) delete mode 100644 transfer/examples/overload.tr diff --git a/src/Transfer/SyntaxToCore.hs b/src/Transfer/SyntaxToCore.hs index 1b17e4a3f..3a5bdac20 100644 --- a/src/Transfer/SyntaxToCore.hs +++ b/src/Transfer/SyntaxToCore.hs @@ -57,7 +57,7 @@ numberMetas = mapM f EMeta -> do st <- get put (st { nextMeta = nextMeta st + 1}) - return $ EVar $ Ident $ "?" ++ show (nextMeta st) + return $ EVar $ Ident $ "?" ++ show (nextMeta st) -- FIXME: hack _ -> composOpM f t -- diff --git a/transfer/examples/overload.tr b/transfer/examples/overload.tr deleted file mode 100644 index dafefa203..000000000 --- a/transfer/examples/overload.tr +++ /dev/null @@ -1,157 +0,0 @@ --- --- The Add class --- - --- FIXME: reimplement in terms of Monoid? - -Add : Type -> Type -Add = sig { zero : A; plus : A -> A -> A } - -zero : (A : Type) -> Add A -> A -zero _ d = d.zero - -plus : (A : Type) -> Add A -> A -> A -> A -plus _ d = d.plus - -add_Integer : Add Integer -add_Integer = rec { zero = 0; plus = prim_add_Int } - -sum : (A:Type) -> Add A -> List A -> A -sum _ d (Nil _) = d.zero -sum A d (Cons _ x xs) = d.plus x (sum A d xs) - -{- Operators: - - (x + y) => (plus ? ? x y) - --} - --- --- The Prod class --- - --- FIXME: reimplement in terms of Monoid? - -Prod : Type -> Type -Prod = sig { one : A; times : A -> A -> A } - -one : (A : Type) -> Prod A -> A -one _ d = d.zero - -times : (A : Type) -> Prod A -> A -> A -> A -times _ d = d.plus - -prod_Integer : Add Integer -prod_Integer = rec { one = 1; times = prim_mul_Int } - -product : (A:Type) -> Prod A -> List A -> A -product _ d (Nil _) = d.one -product A d (Cons _ x xs) = d.times x (product A d xs) - -{- Operators: - - (x * y) => (times ? ? x y) - --} - - - --- --- The Eq class --- - -Eq : Type -> Type -Eq A = sig { eq : A -> A -> Bool } - -eq : (A : Type) -> Eq A -> A -> A -> Bool -eq _ d = d.eq - -neq : (A : Type) -> Eq A -> A -> A -> Bool -neq A d x y = not (eq A d x y) - - -{- Operators: - - (x == y) => (eq ? ? x y) - (x /= y) => (neq ? ? x y) - --} - - --- --- The Ord class --- - --- FIXME: require Eq for Ord - -data Ordering : Type where - LT : Ordering - EQ : Ordering - GT : Ordering - -Ord : Type -> Type -Ord A = sig eq : A -> A -> Bool - compare : A -> A -> Ordering - -compare : (A : Type) -> Ord A -> A -> A -> Ordering -compare _ d = d.compare - -ordOp : (Ordering -> Bool) -> (A : Type) -> Ord A -> A -> A -> Bool -ordOp f A d x y = f (compare A d x y) - -lt : (A : Type) -> Ord A -> A -> A -> Bool -lt = ordOp (\o -> case o of { LT -> True; _ -> False }) - -le : (A : Type) -> Ord A -> A -> A -> Bool -le = ordOp (\o -> case o of { GT -> False; _ -> True }) - -ge : (A : Type) -> Ord A -> A -> A -> Bool -ge = ordOp (\o -> case o of { LT -> False; _ -> True }) - -gt : (A : Type) -> Ord A -> A -> A -> Bool -gt = ordOp (\o -> case o of { GT -> True; _ -> False }) - - - -{- Operators: - - (x < y) => (lt ? ? x y) - (x <= y) => (le ? ? x y) - (x >= y) => (ge ? ? x y) - (x > y) => (gt ? ? x y) - --} - - --- --- The Show class --- - -Show : Type -> Type -Show A = sig { show : A -> String } - -show : (A : Type) -> Show A -> A -> String -show _ d = d.show - -show_Integer : Show Integer -show_Integer = rec { show = prim_show_Int } - - --- --- The Compos class --- - - -Monoid : Type -> Type -Monoid = sig { mzero : A; mplus : A -> A -> A } - -Compos : (C : Type) -> (C -> Type) -> Type -Compos C T = sig - composOp : (c : C) -> ((d : C) -> T d -> T d) -> T c -> T c - composFold : (B : Type) -> Monoid B -> (c : C) -> ((d : C) -> T d -> b) -> T c -> b - -composOp : (T : Type) -> (C : Type) -> Compos C T -> (c : C) -> ((d : C) -> T d -> T d) -> T c -> T c -composOp _ _ d c f t = d.composOp c f t - -composFold : (T : Type) -> (C : Type) -> Compos C T -> (B : Type) -> Monoid B -> ((d : C) -> T d -> b) -> T c -> b -composFold _ _ d b m c f t = d.composFold b m c f t \ No newline at end of file diff --git a/transfer/examples/prelude.tr b/transfer/examples/prelude.tr index c8388db7b..162599e0c 100644 --- a/transfer/examples/prelude.tr +++ b/transfer/examples/prelude.tr @@ -1,5 +1,217 @@ +-- +-- Prelude for the transfer language. +-- + + +-- +-- Basic functions +-- + const : (A:Type) -> (B:Type) -> A -> B -> A const _ _ x _ = x id : (A:Type) -> A -> A -id _ x = x \ No newline at end of file +id _ x = x + + + +-- +-- The Add class +-- + +Add : Type -> Type +Add = sig zero : A + plus : A -> A -> A + +zero : (A : Type) -> Add A -> A +zero _ d = d.zero + +plus : (A : Type) -> Add A -> A -> A -> A +plus _ d = d.plus + +sum : (A:Type) -> Add A -> List A -> A +sum _ d (Nil _) = d.zero +sum A d (Cons _ x xs) = d.plus x (sum A d xs) + +-- Operators: + +{- + (x + y) => (plus ? ? x y) +-} + +-- Instances: + +add_Integer : Add Integer +add_Integer = rec zero = 0 + plus = prim_add_Int + +add_String : Add String +add_String = rec zero = "" + plus = prim_add_Str + + + +-- +-- The Prod class +-- + +Prod : Type -> Type +Prod = sig one : A + times : A -> A -> A + +one : (A : Type) -> Prod A -> A +one _ d = d.one + +times : (A : Type) -> Prod A -> A -> A -> A +times _ d = d.times + +product : (A:Type) -> Prod A -> List A -> A +product _ d (Nil _) = d.one +product A d (Cons _ x xs) = d.times x (product A d xs) + +-- Operators: + +{- + (x * y) => (times ? ? x y) +-} + +-- Instances: + +prod_Integer : Add Integer +prod_Integer = rec one = 1 + times = prim_mul_Int + + + +-- +-- The Eq class +-- + +Eq : Type -> Type +Eq A = sig eq : A -> A -> Bool + +eq : (A : Type) -> Eq A -> A -> A -> Bool +eq _ d = d.eq + +neq : (A : Type) -> Eq A -> A -> A -> Bool +neq A d x y = not (eq A d x y) + + +-- Operators: + +{- + (x == y) => (eq ? ? x y) + (x /= y) => (neq ? ? x y) +-} + +-- Instances: + +eq_Integer : Eq Integer +eq_Integer = rec eq = prim_eq_Int + +eq_String : Eq String +eq_String = rec eq = prim_eq_Str + + + +-- +-- The Ord class +-- + +data Ordering : Type where + LT : Ordering + EQ : Ordering + GT : Ordering + +Ord : Type -> Type +Ord A = sig eq : A -> A -> Bool + compare : A -> A -> Ordering + +compare : (A : Type) -> Ord A -> A -> A -> Ordering +compare _ d = d.compare + +ordOp : (Ordering -> Bool) -> (A : Type) -> Ord A -> A -> A -> Bool +ordOp f A d x y = f (compare A d x y) + +lt : (A : Type) -> Ord A -> A -> A -> Bool +lt = ordOp (\o -> case o of { LT -> True; _ -> False }) + +le : (A : Type) -> Ord A -> A -> A -> Bool +le = ordOp (\o -> case o of { GT -> False; _ -> True }) + +ge : (A : Type) -> Ord A -> A -> A -> Bool +ge = ordOp (\o -> case o of { LT -> False; _ -> True }) + +gt : (A : Type) -> Ord A -> A -> A -> Bool +gt = ordOp (\o -> case o of { GT -> True; _ -> False }) + +-- Operators + +{- + (x < y) => (lt ? ? x y) + (x <= y) => (le ? ? x y) + (x >= y) => (ge ? ? x y) + (x > y) => (gt ? ? x y) +-} + +-- Instances + +ord_Integer : Ord Integer +ord_Integer = rec eq = prim_eq_Int + compare = prim_cmp_Int + +ord_String : Ord String +ord_String = rec eq = prim_eq_Str + compare = prim_cmp_Str + + + +-- +-- The Show class +-- + +Show : Type -> Type +Show A = sig show : A -> String + +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 + + + +-- +-- The Monoid class +-- + +Monoid : Type -> Type +Monoid = sig mzero : A + mplus : A -> A -> A + + + +-- +-- The Compos class +-- + +Compos : Type -> Type +Compos T = sig + C : Type + composOp : (c : C) -> ((a : C) -> T a -> T a) -> T c -> T c + composFold : (B : Type) -> Monoid B -> (c : C) -> ((a : C) -> T a -> b) -> T c -> b + +composOp : (T : Type) -> (d : Compos T) + -> (c : d.C) -> ((a : d.C) -> T a -> T a) -> T c -> T c +composOp _ d = d.composOp + +composFold : (T : Type) -> (d : Compos T) -> (B : Type) -> Monoid B + -> (c : d.C) -> ((a : d.C) -> T a -> b) -> T c -> b +composFold _ _ d = d.composFold +