From c703a92136ce579282c63c6e31fff76cc84b37ce Mon Sep 17 00:00:00 2001 From: bringert Date: Tue, 6 Dec 2005 16:33:40 +0000 Subject: Transfer: Changed transfer program file extension from .tr to .tra to avoid collision with Troff file extension. --- transfer/lib/array.tr | 9 - transfer/lib/array.tra | 9 + transfer/lib/bool.tr | 6 - transfer/lib/bool.tra | 6 + transfer/lib/nat.tr | 24 --- transfer/lib/nat.tra | 24 +++ transfer/lib/prelude.tr | 502 ----------------------------------------------- transfer/lib/prelude.tra | 502 +++++++++++++++++++++++++++++++++++++++++++++++ 8 files changed, 541 insertions(+), 541 deletions(-) delete mode 100644 transfer/lib/array.tr create mode 100644 transfer/lib/array.tra delete mode 100644 transfer/lib/bool.tr create mode 100644 transfer/lib/bool.tra delete mode 100644 transfer/lib/nat.tr create mode 100644 transfer/lib/nat.tra delete mode 100644 transfer/lib/prelude.tr create mode 100644 transfer/lib/prelude.tra (limited to 'transfer/lib') diff --git a/transfer/lib/array.tr b/transfer/lib/array.tr deleted file mode 100644 index e91fe35e7..000000000 --- a/transfer/lib/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/lib/array.tra b/transfer/lib/array.tra new file mode 100644 index 000000000..e91fe35e7 --- /dev/null +++ b/transfer/lib/array.tra @@ -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 deleted file mode 100644 index 2639422b7..000000000 --- a/transfer/lib/bool.tr +++ /dev/null @@ -1,6 +0,0 @@ -import prelude - -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/bool.tra b/transfer/lib/bool.tra new file mode 100644 index 000000000..2639422b7 --- /dev/null +++ b/transfer/lib/bool.tra @@ -0,0 +1,6 @@ +import prelude + +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/nat.tr b/transfer/lib/nat.tr deleted file mode 100644 index b13a809ed..000000000 --- a/transfer/lib/nat.tr +++ /dev/null @@ -1,24 +0,0 @@ -import prelude - -data Nat : Type where - Zero : Nat - Succ : (n:Nat) -> Nat - -add_Nat : Add Nat -add_Nat = rec zero = Zero - plus = natPlus - -natPlus : Nat -> Nat -> Nat -natPlus Zero y = y -natPlus (Succ x) y = Succ (natPlus x y) - -pred : Nat -> Nat -pred Zero = Zero -pred (Succ n) = n - -natToInt : Nat -> Integer -natToInt Zero = 0 -natToInt (Succ n) = 1 + natToInt n - -intToNat : Integer -> Nat -intToNat n = if n == 0 then Zero else Succ (intToNat (n-1)) diff --git a/transfer/lib/nat.tra b/transfer/lib/nat.tra new file mode 100644 index 000000000..b13a809ed --- /dev/null +++ b/transfer/lib/nat.tra @@ -0,0 +1,24 @@ +import prelude + +data Nat : Type where + Zero : Nat + Succ : (n:Nat) -> Nat + +add_Nat : Add Nat +add_Nat = rec zero = Zero + plus = natPlus + +natPlus : Nat -> Nat -> Nat +natPlus Zero y = y +natPlus (Succ x) y = Succ (natPlus x y) + +pred : Nat -> Nat +pred Zero = Zero +pred (Succ n) = n + +natToInt : Nat -> Integer +natToInt Zero = 0 +natToInt (Succ n) = 1 + natToInt n + +intToNat : Integer -> Nat +intToNat n = if n == 0 then Zero else Succ (intToNat (n-1)) diff --git a/transfer/lib/prelude.tr b/transfer/lib/prelude.tr deleted file mode 100644 index fe2d1b296..000000000 --- a/transfer/lib/prelude.tr +++ /dev/null @@ -1,502 +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 - -flip : (A:Type) -> (B:Type) -> (C:Type) -> (A -> B -> C) -> B -> A -> C -flip _ _ _ f x y = f y x - -compose : (A:Type) -> (B:Type) -> (C:Type) -> (B -> C) -> (A -> B) -> A -> C -compose _ _ _ f g x = f (g x) - -otherwise : Bool -otherwise = True - - --- --- The Integer type --- - --- Instances: - -num_Integer : Num Integer -num_Integer = rec zero = 0 - plus = prim_add_Integer - minus = prim_sub_Integer - one = 1 - times = prim_mul_Integer - div = prim_div_Integer - mod = prim_mod_Integer - negate = prim_neg_Integer - eq = prim_eq_Integer - compare = prim_cmp_Integer - -show_Integer : Show Integer -show_Integer = rec show = prim_show_Integer - - --- --- The Double type --- - --- Instances: - -num_Double : Num Double -num_Double = rec zero = 0.0 - plus = prim_add_Double - minus = prim_sub_Double - one = 1.0 - times = prim_mul_Double - div = prim_div_Double - mod = prim_mod_Double - negate = prim_neg_Double - eq = prim_eq_Double - compare = prim_cmp_Double - -show_Double : Show Double -show_Double = rec show = prim_show_Double - - - --- --- The String type --- - --- Instances: - -add_String : Add String -add_String = rec zero = "" - plus = prim_add_String - - -ord_String : Ord String -ord_String = rec eq = prim_eq_Str - compare = prim_cmp_String - -show_String : Show String -show_String = rec show = prim_show_String - - --- --- 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 - - --- --- Tuples --- - -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 - -{- - - syntax: - - (x1,...,xn) => { p1 = e1; ... ; pn = en } - - where n >= 2 and x1,...,xn are expressions or patterns - --} - - --- --- The List type --- - -data List : Type -> Type where - Nil : (A:Type) -> List A - Cons : (A:Type) -> A -> List A -> List A - -foldr : (A : Type) -> (B : Type) -> (A -> B -> B) -> B -> List A -> B -foldr _ _ _ x [] = x -foldr A B f x (y::ys) = f y (foldr A B f x ys) - -length : (A:Type) -> List A -> Integer -length A = foldr A Integer (\_ -> \y -> y+1) 0 - -map : (A:Type) -> (B:Type) -> (A -> B) -> List A -> List B -map _ _ _ [] = [] -map A B f (x::xs) = f x :: map A B f xs - -filter : (A:Type) -> (A -> Bool) -> List A -> List A -filter _ _ [] = [] -filter A f (x::xs) | f x = x :: filter A f xs -filter A f (x::xs) = filter A f xs - -append : (A:Type) -> List A -> List A -> List A -append A xs ys = foldr A (List A) (Cons A) ys xs - -concat : (A : Type) -> List (List A) -> List A -concat A = foldr (List A) (List A) (append A) (Nil A) - -partition : (A : Type) -> (A -> Bool) -> List A -> Pair (List A) (List A) -partition _ _ [] = ([],[]) -partition A p (x::xs) = - let r : Pair (List A) (List A) = partition A p xs - in if p x then (x :: fst r, snd r) else (fst r, x :: snd r) - - --- 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 --- - -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 - -maybe : (A : Type) -> (B : Type) -> B -> (A -> B) -> Maybe A -> A -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 --- - -Num : Type -> Type -Num = sig zero : A - plus : A -> A -> A - minus : A -> A -> A - one : A - times : A -> A -> A - div : A -> A -> A - mod : A -> A -> A - negate : A -> A - eq : A -> A -> Bool - compare : A -> A -> Ordering - - - - --- --- 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 A d = foldr A A d.plus d.zero - - --- Operators: - -{- - (x + y) => (plus ? ? x y) --} - - - - - --- --- The Sub class --- - -Sub : Type -> Type -Sub = sig minus : A -> A -> A - -minus : (A : Type) -> Sub A -> A -minus _ d = d.minus - - - - - --- --- The Mul class --- - -Mul : Type -> Type -Mul = sig one : A - times : A -> A -> A - -one : (A : Type) -> Mul A -> A -one _ d = d.one - -times : (A : Type) -> Mul A -> A -> A -> A -times _ d = d.times - -product : (A:Type) -> Mul A -> List A -> A -product A d = foldr A A d.times d.one - --- Operators: - -{- - (x * y) => (times ? ? x y) --} - - - - --- --- The Div class --- - -Div : Type -> Type -Div = sig div : A -> A -> A - mod : A -> A -> A - -div : (A : Type) -> Div A -> A -> A -> A -div _ d = d.div - -mod : (A : Type) -> Div A -> A -> A -> A -mod _ d = d.mod - --- Operators: - -{- - (x / y) => (div ? ? x y) - (x % y) => (mod ? ? x y) --} - - - - - --- --- The Neg class --- - -Neg : Type -> Type -Neg = sig negate : A -> A - -negate : (A : Type) -> Neg A -> A -> A -negate _ d = d.negate - --- Operators: - -{- - (-x) => negate ? ? x --} - - - - --- --- 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 --- - -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 - - - - - - --- --- The Monoid class --- - -Monoid : Type -> Type -Monoid = sig mzero : A - mplus : A -> A -> A - - - - --- --- The Compos class --- - -Compos : (C : Type) -> (C -> Type) -> Type -Compos C T = sig - 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 : (C : Type) -> (T : C -> Type) -> (d : Compos C T) - -> (c : C) -> ((a : C) -> T a -> T a) -> T c -> T c -composOp _ _ d = d.composOp - -composFold : (C : Type) -> (T : C -> Type) -> (d : Compos C T) -> (B : Type) -> Monoid B - -> (c : C) -> ((a : C) -> T a -> b) -> T c -> b -composFold _ _ d = d.composFold - - - - - --- --- The Monad class --- - -Monad : (Type -> Type) -> Type -Monad M = sig return : (A : Type) -> M A - bind : (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B - -return : (M : Type -> Type) -> Monad M -> M A -return _ d = d.return - -bind : (M : Type -> Type) -> Monad M - -> (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B -bind _ d = d.bind - --- Operators: - -{- - (x >>= y) => bind ? ? ? ? x y - (x >> y) => bind ? ? ? ? x (\_ -> y) --} - diff --git a/transfer/lib/prelude.tra b/transfer/lib/prelude.tra new file mode 100644 index 000000000..fe2d1b296 --- /dev/null +++ b/transfer/lib/prelude.tra @@ -0,0 +1,502 @@ +-- +-- 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 + +flip : (A:Type) -> (B:Type) -> (C:Type) -> (A -> B -> C) -> B -> A -> C +flip _ _ _ f x y = f y x + +compose : (A:Type) -> (B:Type) -> (C:Type) -> (B -> C) -> (A -> B) -> A -> C +compose _ _ _ f g x = f (g x) + +otherwise : Bool +otherwise = True + + +-- +-- The Integer type +-- + +-- Instances: + +num_Integer : Num Integer +num_Integer = rec zero = 0 + plus = prim_add_Integer + minus = prim_sub_Integer + one = 1 + times = prim_mul_Integer + div = prim_div_Integer + mod = prim_mod_Integer + negate = prim_neg_Integer + eq = prim_eq_Integer + compare = prim_cmp_Integer + +show_Integer : Show Integer +show_Integer = rec show = prim_show_Integer + + +-- +-- The Double type +-- + +-- Instances: + +num_Double : Num Double +num_Double = rec zero = 0.0 + plus = prim_add_Double + minus = prim_sub_Double + one = 1.0 + times = prim_mul_Double + div = prim_div_Double + mod = prim_mod_Double + negate = prim_neg_Double + eq = prim_eq_Double + compare = prim_cmp_Double + +show_Double : Show Double +show_Double = rec show = prim_show_Double + + + +-- +-- The String type +-- + +-- Instances: + +add_String : Add String +add_String = rec zero = "" + plus = prim_add_String + + +ord_String : Ord String +ord_String = rec eq = prim_eq_Str + compare = prim_cmp_String + +show_String : Show String +show_String = rec show = prim_show_String + + +-- +-- 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 + + +-- +-- Tuples +-- + +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 + +{- + + syntax: + + (x1,...,xn) => { p1 = e1; ... ; pn = en } + + where n >= 2 and x1,...,xn are expressions or patterns + +-} + + +-- +-- The List type +-- + +data List : Type -> Type where + Nil : (A:Type) -> List A + Cons : (A:Type) -> A -> List A -> List A + +foldr : (A : Type) -> (B : Type) -> (A -> B -> B) -> B -> List A -> B +foldr _ _ _ x [] = x +foldr A B f x (y::ys) = f y (foldr A B f x ys) + +length : (A:Type) -> List A -> Integer +length A = foldr A Integer (\_ -> \y -> y+1) 0 + +map : (A:Type) -> (B:Type) -> (A -> B) -> List A -> List B +map _ _ _ [] = [] +map A B f (x::xs) = f x :: map A B f xs + +filter : (A:Type) -> (A -> Bool) -> List A -> List A +filter _ _ [] = [] +filter A f (x::xs) | f x = x :: filter A f xs +filter A f (x::xs) = filter A f xs + +append : (A:Type) -> List A -> List A -> List A +append A xs ys = foldr A (List A) (Cons A) ys xs + +concat : (A : Type) -> List (List A) -> List A +concat A = foldr (List A) (List A) (append A) (Nil A) + +partition : (A : Type) -> (A -> Bool) -> List A -> Pair (List A) (List A) +partition _ _ [] = ([],[]) +partition A p (x::xs) = + let r : Pair (List A) (List A) = partition A p xs + in if p x then (x :: fst r, snd r) else (fst r, x :: snd r) + + +-- 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 +-- + +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 + +maybe : (A : Type) -> (B : Type) -> B -> (A -> B) -> Maybe A -> A +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 +-- + +Num : Type -> Type +Num = sig zero : A + plus : A -> A -> A + minus : A -> A -> A + one : A + times : A -> A -> A + div : A -> A -> A + mod : A -> A -> A + negate : A -> A + eq : A -> A -> Bool + compare : A -> A -> Ordering + + + + +-- +-- 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 A d = foldr A A d.plus d.zero + + +-- Operators: + +{- + (x + y) => (plus ? ? x y) +-} + + + + + +-- +-- The Sub class +-- + +Sub : Type -> Type +Sub = sig minus : A -> A -> A + +minus : (A : Type) -> Sub A -> A +minus _ d = d.minus + + + + + +-- +-- The Mul class +-- + +Mul : Type -> Type +Mul = sig one : A + times : A -> A -> A + +one : (A : Type) -> Mul A -> A +one _ d = d.one + +times : (A : Type) -> Mul A -> A -> A -> A +times _ d = d.times + +product : (A:Type) -> Mul A -> List A -> A +product A d = foldr A A d.times d.one + +-- Operators: + +{- + (x * y) => (times ? ? x y) +-} + + + + +-- +-- The Div class +-- + +Div : Type -> Type +Div = sig div : A -> A -> A + mod : A -> A -> A + +div : (A : Type) -> Div A -> A -> A -> A +div _ d = d.div + +mod : (A : Type) -> Div A -> A -> A -> A +mod _ d = d.mod + +-- Operators: + +{- + (x / y) => (div ? ? x y) + (x % y) => (mod ? ? x y) +-} + + + + + +-- +-- The Neg class +-- + +Neg : Type -> Type +Neg = sig negate : A -> A + +negate : (A : Type) -> Neg A -> A -> A +negate _ d = d.negate + +-- Operators: + +{- + (-x) => negate ? ? x +-} + + + + +-- +-- 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 +-- + +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 + + + + + + +-- +-- The Monoid class +-- + +Monoid : Type -> Type +Monoid = sig mzero : A + mplus : A -> A -> A + + + + +-- +-- The Compos class +-- + +Compos : (C : Type) -> (C -> Type) -> Type +Compos C T = sig + 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 : (C : Type) -> (T : C -> Type) -> (d : Compos C T) + -> (c : C) -> ((a : C) -> T a -> T a) -> T c -> T c +composOp _ _ d = d.composOp + +composFold : (C : Type) -> (T : C -> Type) -> (d : Compos C T) -> (B : Type) -> Monoid B + -> (c : C) -> ((a : C) -> T a -> b) -> T c -> b +composFold _ _ d = d.composFold + + + + + +-- +-- The Monad class +-- + +Monad : (Type -> Type) -> Type +Monad M = sig return : (A : Type) -> M A + bind : (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B + +return : (M : Type -> Type) -> Monad M -> M A +return _ d = d.return + +bind : (M : Type -> Type) -> Monad M + -> (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B +bind _ d = d.bind + +-- Operators: + +{- + (x >>= y) => bind ? ? ? ? x y + (x >> y) => bind ? ? ? ? x (\_ -> y) +-} + -- cgit v1.2.3