From cba2fcb9b118cedb603b171ac7d7581c5adb844c Mon Sep 17 00:00:00 2001 From: bringert Date: Wed, 30 Nov 2005 16:00:06 +0000 Subject: Moved transfer libraries to transfer/lib --- transfer/examples/array.tr | 9 -- transfer/examples/bool.tr | 10 -- transfer/examples/list.tr | 17 --- transfer/examples/maybe.tr | 11 -- transfer/examples/nat.tr | 18 --- transfer/examples/pair.tr | 11 -- transfer/examples/prelude.tr | 217 ------------------------------------ transfer/lib/array.tr | 9 ++ transfer/lib/bool.tr | 4 + transfer/lib/list.tr | 17 +++ transfer/lib/maybe.tr | 11 ++ transfer/lib/nat.tr | 18 +++ transfer/lib/pair.tr | 11 ++ transfer/lib/prelude.tr | 254 +++++++++++++++++++++++++++++++++++++++++++ 14 files changed, 324 insertions(+), 293 deletions(-) delete mode 100644 transfer/examples/array.tr delete mode 100644 transfer/examples/bool.tr delete mode 100644 transfer/examples/list.tr delete mode 100644 transfer/examples/maybe.tr delete mode 100644 transfer/examples/nat.tr delete mode 100644 transfer/examples/pair.tr delete mode 100644 transfer/examples/prelude.tr create mode 100644 transfer/lib/array.tr create mode 100644 transfer/lib/bool.tr create mode 100644 transfer/lib/list.tr create mode 100644 transfer/lib/maybe.tr create mode 100644 transfer/lib/nat.tr create mode 100644 transfer/lib/pair.tr create mode 100644 transfer/lib/prelude.tr diff --git a/transfer/examples/array.tr b/transfer/examples/array.tr deleted file mode 100644 index e91fe35e7..000000000 --- a/transfer/examples/array.tr +++ /dev/null @@ -1,9 +0,0 @@ -import nat - -data Array : Type -> Nat -> Type where - Empty : (A:Type) -> Array A Zero - Cell : (A:Type) -> (n:Nat) -> A -> Array A n -> Array A (Succ n) - -mapA : (A:Type) -> (B:Type) -> (n:Nat) -> (A -> B) -> Array A n -> Array B n -mapA A B _ f (Empty _) = Empty B -mapA A B (Succ n) f (Cell _ _ x xs) = Cell B n (f x) (mapA A B n f xs) diff --git a/transfer/examples/bool.tr b/transfer/examples/bool.tr deleted file mode 100644 index 401d238ef..000000000 --- a/transfer/examples/bool.tr +++ /dev/null @@ -1,10 +0,0 @@ -data Bool : Type where - True : Bool - False : Bool; - -depif : (A:Type) -> (B:Type) -> (b:Bool) -> A -> B -> if Type b then A else B -depif _ _ True x _ = x -depif _ _ False _ y = y - -not : Bool -> Bool -not b = if b then False else True diff --git a/transfer/examples/list.tr b/transfer/examples/list.tr deleted file mode 100644 index 079208167..000000000 --- a/transfer/examples/list.tr +++ /dev/null @@ -1,17 +0,0 @@ -import nat - -data List : (_:Type) -> Type where - Nil : (A:Type) -> List A - Cons : (A:Type) -> A -> List A -> List A - -size : (A:Type) -> List A -> Nat -size _ (Nil _) = Zero -size A (Cons _ x xs) = Succ (size A xs) - -map : (A:Type) -> (B:Type) -> (A -> B) -> List A -> List B -map _ B _ (Nil _) = Nil B -map A B f (Cons _ x xs) = Cons B (f x) (map A B f xs) - -append : (A:Type) -> (xs:List A) -> List A -> List A -append _ (Nil _) ys = ys -append A (Cons _ x xs) ys = Cons A x (append A xs ys) diff --git a/transfer/examples/maybe.tr b/transfer/examples/maybe.tr deleted file mode 100644 index 02d7fe56d..000000000 --- a/transfer/examples/maybe.tr +++ /dev/null @@ -1,11 +0,0 @@ -data Maybe : Type -> Type where - Nothing : (A : Type) -> Maybe A - Just : (A : Type) -> A -> Maybe A - -fromMaybe : (A : Type) -> A -> Maybe A -> A -fromMaybe _ x Nothing = x -fromMaybe _ _ (Just x) = x - -maybe : (A : Type) -> (B : Type) -> B -> (A -> B) -> Maybe A -> A -maybe _ _ x _ Nothing = x -maybe _ _ _ f (Just x) = f x \ No newline at end of file diff --git a/transfer/examples/nat.tr b/transfer/examples/nat.tr deleted file mode 100644 index c529e5238..000000000 --- a/transfer/examples/nat.tr +++ /dev/null @@ -1,18 +0,0 @@ -data Nat : Type where - Zero : Nat - Succ : (n:Nat) -> Nat - -plus : Nat -> Nat -> Nat -plus Zero y = y -plus (Succ x) y = Succ (plus x y) - -pred : Nat -> Nat -pred Zero = Zero -pred (Succ n) = n - -natToInt : Nat -> Int -natToInt Zero = 0 -natToInt (Succ n) = 1 + natToInt n - -intToNat : Int -> Nat -intToNat n = if n == 0 then Zero else Succ (intToNat (n-1)) diff --git a/transfer/examples/pair.tr b/transfer/examples/pair.tr deleted file mode 100644 index 1b70411e8..000000000 --- a/transfer/examples/pair.tr +++ /dev/null @@ -1,11 +0,0 @@ -Pair : Type -> Type -> Type -Pair A B = sig { p1 : A; p2 : B } - -pair : (A:Type) -> (B:Type) -> A -> B -> Pair A B -pair _ _ x y = rec { p1 = x; p2 = y } - -fst : (A:Type) -> (B:Type) -> Pair A B -> A -fst _ _ p = case p of Pair _ _ x _ -> x - -snd : (A:Type) -> (B:Type) -> Pair A B -> B -snd _ _ p = case p of Pair _ _ x _ -> x diff --git a/transfer/examples/prelude.tr b/transfer/examples/prelude.tr deleted file mode 100644 index 162599e0c..000000000 --- a/transfer/examples/prelude.tr +++ /dev/null @@ -1,217 +0,0 @@ --- --- 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 - - - --- --- 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 - diff --git a/transfer/lib/array.tr b/transfer/lib/array.tr new file mode 100644 index 000000000..e91fe35e7 --- /dev/null +++ b/transfer/lib/array.tr @@ -0,0 +1,9 @@ +import nat + +data Array : Type -> Nat -> Type where + Empty : (A:Type) -> Array A Zero + Cell : (A:Type) -> (n:Nat) -> A -> Array A n -> Array A (Succ n) + +mapA : (A:Type) -> (B:Type) -> (n:Nat) -> (A -> B) -> Array A n -> Array B n +mapA A B _ f (Empty _) = Empty B +mapA A B (Succ n) f (Cell _ _ x xs) = Cell B n (f x) (mapA A B n f xs) diff --git a/transfer/lib/bool.tr b/transfer/lib/bool.tr new file mode 100644 index 000000000..b8c1c95a5 --- /dev/null +++ b/transfer/lib/bool.tr @@ -0,0 +1,4 @@ +depif : (A:Type) -> (B:Type) -> (b:Bool) -> A -> B -> if Type b then A else B +depif _ _ True x _ = x +depif _ _ False _ y = y + diff --git a/transfer/lib/list.tr b/transfer/lib/list.tr new file mode 100644 index 000000000..079208167 --- /dev/null +++ b/transfer/lib/list.tr @@ -0,0 +1,17 @@ +import nat + +data List : (_:Type) -> Type where + Nil : (A:Type) -> List A + Cons : (A:Type) -> A -> List A -> List A + +size : (A:Type) -> List A -> Nat +size _ (Nil _) = Zero +size A (Cons _ x xs) = Succ (size A xs) + +map : (A:Type) -> (B:Type) -> (A -> B) -> List A -> List B +map _ B _ (Nil _) = Nil B +map A B f (Cons _ x xs) = Cons B (f x) (map A B f xs) + +append : (A:Type) -> (xs:List A) -> List A -> List A +append _ (Nil _) ys = ys +append A (Cons _ x xs) ys = Cons A x (append A xs ys) diff --git a/transfer/lib/maybe.tr b/transfer/lib/maybe.tr new file mode 100644 index 000000000..02d7fe56d --- /dev/null +++ b/transfer/lib/maybe.tr @@ -0,0 +1,11 @@ +data Maybe : Type -> Type where + Nothing : (A : Type) -> Maybe A + Just : (A : Type) -> A -> Maybe A + +fromMaybe : (A : Type) -> A -> Maybe A -> A +fromMaybe _ x Nothing = x +fromMaybe _ _ (Just x) = x + +maybe : (A : Type) -> (B : Type) -> B -> (A -> B) -> Maybe A -> A +maybe _ _ x _ Nothing = x +maybe _ _ _ f (Just x) = f x \ No newline at end of file diff --git a/transfer/lib/nat.tr b/transfer/lib/nat.tr new file mode 100644 index 000000000..c529e5238 --- /dev/null +++ b/transfer/lib/nat.tr @@ -0,0 +1,18 @@ +data Nat : Type where + Zero : Nat + Succ : (n:Nat) -> Nat + +plus : Nat -> Nat -> Nat +plus Zero y = y +plus (Succ x) y = Succ (plus x y) + +pred : Nat -> Nat +pred Zero = Zero +pred (Succ n) = n + +natToInt : Nat -> Int +natToInt Zero = 0 +natToInt (Succ n) = 1 + natToInt n + +intToNat : Int -> Nat +intToNat n = if n == 0 then Zero else Succ (intToNat (n-1)) diff --git a/transfer/lib/pair.tr b/transfer/lib/pair.tr new file mode 100644 index 000000000..1b70411e8 --- /dev/null +++ b/transfer/lib/pair.tr @@ -0,0 +1,11 @@ +Pair : Type -> Type -> Type +Pair A B = sig { p1 : A; p2 : B } + +pair : (A:Type) -> (B:Type) -> A -> B -> Pair A B +pair _ _ x y = rec { p1 = x; p2 = y } + +fst : (A:Type) -> (B:Type) -> Pair A B -> A +fst _ _ p = case p of Pair _ _ x _ -> x + +snd : (A:Type) -> (B:Type) -> Pair A B -> B +snd _ _ p = case p of Pair _ _ x _ -> x diff --git a/transfer/lib/prelude.tr b/transfer/lib/prelude.tr new file mode 100644 index 000000000..cf2167c6d --- /dev/null +++ b/transfer/lib/prelude.tr @@ -0,0 +1,254 @@ +-- +-- 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 + + +-- +-- The Bool type +-- + +data Bool : Type where + True : Bool + False : Bool + +not : Bool -> Bool +not b = if b then False else True + + + +-- +-- 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 Neg class +-- + +Neg : Type -> Type +Neg = sig negate : A -> A + +negate : (A : Type) -> Neg A -> A -> A +negate _ d = d.neg + +-- Operators: + +{- + (-x) => negate ? ? x +-} + +-- Instances: + +neg_Integer : Neg Integer +neg_Integer = rec negate = prim_neg_Int + +neg_Bool : Neg Bool +neg_Bool = rec negate = not + + + +-- +-- 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 + -- cgit v1.2.3