Moved transfer libraries to transfer/lib

transfer/examples/array.tr

@@ -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)

transfer/examples/bool.tr

@@ -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

transfer/examples/list.tr

@@ -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)

transfer/examples/maybe.tr

@@ -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

transfer/examples/nat.tr

@@ -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))

transfer/examples/pair.tr

@@ -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

transfer/examples/prelude.tr

@@ -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
-