Transfer: fleshed out overloading examples.

transfer/examples/overload.tr

@@ -1,29 +1,148 @@
-Monoid : Type -> Type
-Monoid A = sig { zero : A; plus : A -> A -> A }
+--
+-- The Add class
+--
 
-Additive : Type -> Type
-Additive = Monoid
+-- FIXME: reimplement in terms of Monoid?
 
-additive_Integer : Additive Integer
-additive_Integer = rec { zero = 0; plus = prim_add_Int }
+Add : Type -> Type
+Add = sig { zero : A; plus : A -> A -> A }
 
-sum : (A:Type) -> Additive A -> List 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 { compare : A -> A -> Ordering }
+
+compare : (A : Type) -> Ord A -> A -> A -> Ordering
+compare _ 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 _  rec{show = show} x = show x
-
+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 
@@ -31,7 +150,7 @@ Compos C T = sig
       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 _ _ rec{composOp=composOp} c f t = composOp c f t
+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 _ _ rec{composFold=composFold} b m c f t = composFold b m c f t
+composFold _ _ d b m c f t = d.composFold b m c f t