Moved transfer libraries to transfer/lib

7 files changed, 324 insertions, 0 deletions

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
+