forked from GitHub/gf-core
Moved transfer libraries to transfer/lib
This commit is contained in:
bringert
@@ -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)
|
||||
@@ -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
|
||||
@@ -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)
|
||||
@@ -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
|
||||
@@ -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))
|
||||
@@ -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
|
||||
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user