mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 04:59:31 -06:00
157 lines
3.0 KiB
Plaintext
157 lines
3.0 KiB
Plaintext
--
|
|
-- 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 |