removed transfer from gf3

6 files changed, 0 insertions, 646 deletions

diff --git a/transfer/lib/bintree.tra b/transfer/lib/bintree.tra
deleted file mode 100644
index 0dd21f184..000000000
--- a/transfer/lib/bintree.tra
+++ /dev/null
@@ -1,22 +0,0 @@
--- NOTE: this is unfinished and untested
-
-import prelude
-
-data BinTree : Type -> Type where
-	Leaf : (A:Type) -> BinTree A
-	Node : (A:Type) -> BinTree A -> A -> BinTree A -> BinTree A
-
-contains : (A:Type) -> Ord A -> A -> BinTree A -> Bool
-contains _ _ _ (Leaf _) = False
-contains A o x (Node _ l y r) 
-	| x < y = contains A o x l
-	| x > y = contains A o x r
-	| otherwise = True
-
-insert : (A:Type) -> Ord A -> A -> BinTree A -> BinTree A
-insert A o x (Leaf _) = Node A (Leaf A) x (Leaf A)
-insert A o x (Node _ l y r) 
-	| x < y = Node A (insert A o x l) y r
-	| x > y = Node A l y (insert A o x r)
-	| otherwise = Node A l x r
-
diff --git a/transfer/lib/bool.tra b/transfer/lib/bool.tra
deleted file mode 100644
index 2639422b7..000000000
--- a/transfer/lib/bool.tra
+++ /dev/null
@@ -1,6 +0,0 @@
-import prelude
-
-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/collection.tra b/transfer/lib/collection.tra
deleted file mode 100644
index 59b71a5e9..000000000
--- a/transfer/lib/collection.tra
+++ /dev/null
@@ -1,77 +0,0 @@
--- NOTE: this is unfinished and untested
-
-import prelude
-import bintree
-
-Collection : Type -> Type
-Collection C = 
-  sig 
-	-- types
-	Elem : Type
-	-- Add stuff
-	zero : C
-        plus : C -> C -> C
-	-- Collection-specific stuff
-        size : C -> Integer
-	add : Elem -> C -> C
-	elem : Elem -> C -> Bool
-        map : (Elem -> Elem) -> C -> C
-        filter : (Elem -> Bool) -> C -> C
-        fromList : List Elem -> C
-        toList : C -> List Elem
-
-
---
--- Collection String instance
---
-
-collection_String : Collection String
-collection_String =
-  rec
-	Elem = Char
-	zero = ""
-	plus = prim_add_String
-	size = prim_length_String
-	-- ...
-
-
---
--- Collection List instance
---
-
-collection_List : (A : Type) -> Collection (List A)
-collection_List A = 
-  rec
-	Elem = A
-	zero = Nil A
-	plus = append A
-	size = length A
-	add  = Cons A
-	-- ...
-
---
--- Collection Vector instance
---
-
-collection_Vector : (A : Type) -> (n : Nat) -> Collection (Vector A n)
-collection_Vector A n = 
-  rec
-	Elem = A
-	zero = Empty A
-	plus = appendV A n n -- FIXME: this only works for vectors of the same length!
-	-- ...
-
-
---
--- Collection BinTree instance
---
-
-collection_BinTree : (A : Type) -> Ord A -> Collection (BinTree A)
-collection_BinTree A o = 
-  rec
-	Elem = A
-	zero = Nil A
-	plus = merge A o
-	size = sizeBT A
-	add  = insert A o
-	-- ...
diff --git a/transfer/lib/nat.tra b/transfer/lib/nat.tra
deleted file mode 100644
index b13a809ed..000000000
--- a/transfer/lib/nat.tra
+++ /dev/null
@@ -1,24 +0,0 @@
-import prelude
-
-data Nat : Type where
-	Zero : Nat
-  	Succ : (n:Nat) -> Nat
-
-add_Nat : Add Nat
-add_Nat = rec zero = Zero
-	      plus = natPlus
-
-natPlus : Nat -> Nat -> Nat
-natPlus Zero y = y
-natPlus (Succ x) y = Succ (natPlus x y)
-
-pred : Nat -> Nat
-pred Zero = Zero
-pred (Succ n) = n
-
-natToInt : Nat -> Integer
-natToInt Zero = 0
-natToInt (Succ n) = 1 + natToInt n
-
-intToNat : Integer -> Nat
-intToNat n = if n == 0 then Zero else Succ (intToNat (n-1))
diff --git a/transfer/lib/prelude.tra b/transfer/lib/prelude.tra
deleted file mode 100644
index 054058db4..000000000
--- a/transfer/lib/prelude.tra
+++ /dev/null
@@ -1,502 +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
-
-flip : (A:Type) -> (B:Type) -> (C:Type) -> (A -> B -> C) -> B -> A -> C
-flip _ _ _ f x y = f y x
-
-compose : (A:Type) -> (B:Type) -> (C:Type) -> (B -> C) -> (A -> B) -> A -> C
-compose _ _ _ f g x = f (g x)
-
-otherwise : Bool
-otherwise = True
-
-
---
--- The Integer type
---
-
--- Instances:
-
-num_Integer : Num Integer
-num_Integer = rec zero = 0
-		  plus = prim_add_Integer
-		  minus = prim_sub_Integer
-		  one = 1
-              	  times = prim_mul_Integer
-		  div = prim_div_Integer
-              	  mod = prim_mod_Integer
-		  negate = prim_neg_Integer
-		  eq = prim_eq_Integer
-		  compare = prim_cmp_Integer
-
-show_Integer : Show Integer
-show_Integer = rec show = prim_show_Integer
-
-
---
--- The Double type
---
-
--- Instances:
-
-num_Double : Num Double
-num_Double = rec zero = 0.0
-		 plus = prim_add_Double
-		 minus = prim_sub_Double
-		 one = 1.0
-              	 times = prim_mul_Double
-		 div = prim_div_Double
-              	 mod = prim_mod_Double
-		 negate = prim_neg_Double
-		 eq = prim_eq_Double
-		 compare = prim_cmp_Double
-
-show_Double : Show Double
-show_Double = rec show = prim_show_Double
-
-
-
--- 
--- The String type
---
-
--- Instances:
-
-add_String : Add String
-add_String = rec zero = ""
-		 plus = prim_add_String
-
-
-ord_String : Ord String
-ord_String = rec eq = prim_eq_String
-		 compare = prim_cmp_String
-
-show_String : Show String
-show_String = rec show = prim_show_String
-
-
---
--- The Bool type
---
-
-data Bool : Type where 
-	True : Bool
-	False : Bool
-
--- derive Show Bool
-derive Eq Bool
--- derive Ord Bool
-
-not : Bool -> Bool
-not b = if b then False else True
-
--- Instances:
-
-neg_Bool : Neg Bool
-neg_Bool = rec negate = not
-
-add_Bool : Add Bool
-add_Bool = rec zero = False
-               plus = \x -> \y -> x || y
-
-mul_Bool : Add Bool
-mul_Bool = rec one = True
-               times = \x -> \y -> x && y
-
-
---
--- Tuples
---
-
-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
-
-{-
-
- syntax:
-
- (x1,...,xn) => { p1 = e1; ... ; pn = en }
-
- where n >= 2 and x1,...,xn are expressions or patterns
-
--}
-
-
---
--- The List type
---
-
-data List : Type -> Type where 
-	Nil : (A:Type) -> List A
-        Cons : (A:Type) -> A -> List A -> List A
-
-foldr : (A : Type) -> (B : Type) -> (A -> B -> B) -> B -> List A -> B
-foldr _ _ _ x [] = x
-foldr A B f x (y::ys) = f y (foldr A B f x ys)
-
-length : (A:Type) -> List A -> Integer
-length A = foldr A Integer (\_ -> \y -> y+1) 0
-
-map : (A:Type) -> (B:Type) -> (A -> B) -> List A -> List B
-map _ _ _ [] = []
-map A B f (x::xs) = f x :: map A B f xs
-
-filter : (A:Type) -> (A -> Bool) -> List A -> List A
-filter _ _ []            = []
-filter A f (x::xs) | f x = x :: filter A f xs
-filter A f (x::xs)       = filter A f xs
-
-append : (A:Type) -> List A -> List A -> List A
-append A xs ys = foldr A (List A) (Cons A) ys xs
-
-concat : (A : Type) -> List (List A) -> List A
-concat A = foldr (List A) (List A) (append A) (Nil A)
-
-partition : (A : Type) -> (A -> Bool) -> List A -> Pair (List A) (List A)
-partition _ _ [] = ([],[])
-partition A p (x::xs) = 
-  let r = partition A p xs
-   in if p x then (x :: r.p1, r.p2) else (r.p1, x :: r.p2)
-
-
--- Instances:
-
-add_List : (A : Type) -> Add (List A)
-add_List A = rec zero = Nil A
-		 plus = append A
-
-
-monad_List : Monad List
-monad_list = rec return = \A -> \x -> Cons A x (Nil A)
-		 bind = \A -> \B -> \m -> \k -> concat B (map A B k m)
-
-
-
-
-
---
--- The Maybe type
---
-
-data Maybe : Type -> Type where
-	Nothing : (A : Type) -> Maybe A
-	Just : (A : Type) -> A -> Maybe A
-
--- derive Show Maybe
-derive Eq Maybe
--- derive Ord Maybe
-
-
-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
-
-
--- Instances:
-
-monad_Maybe : Monad Maybe
-monad_Maybe = 
-  rec return = Just
-      bind = \A -> \B -> \m -> \k -> 
-         case m of
-		Nothing _ -> Nothing B
-		Just _ x  -> k x
-
-
-
-
---
--- The Num class
---
-
-Num : Type -> Type
-Num A = sig zero : A
-            plus : A -> A -> A
-	    minus : A -> A -> A
-	    one : A
-	    times : A -> A -> A
-	    div : A -> A -> A
-	    mod : A -> A -> A
-	    negate : A -> A
-	    eq : A -> A -> Bool
-	    compare : A -> A -> Ordering
-
-
-
-
---
--- The Add class
---
-
-Add : Type -> Type
-Add A = 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 A d = foldr A A d.plus d.zero
-
-
--- Operators:
-
-{-
-  (x + y) => (plus ? ? x y)
--}
-
-
-
-
-
---
--- The Sub class
---
-
-Sub : Type -> Type
-Sub = sig minus : A -> A -> A
-
-minus : (A : Type) -> Sub A -> A
-minus _ d = d.minus
-
-
-
-
-
---
--- The Mul class
---
-
-Mul : Type -> Type
-Mul A = sig one : A
-	    times : A -> A -> A
-
-one : (A : Type) -> Mul A -> A
-one _ d = d.one
-
-times : (A : Type) -> Mul A -> A -> A -> A
-times _ d = d.times
-
-product : (A:Type) -> Mul A -> List A -> A
-product A d = foldr A A d.times d.one
-
--- Operators:
-
-{- 
-  (x * y) => (times ? ? x y)
--}
-
-
-
-
---
--- The Div class
---
-
-Div : Type -> Type
-Div A = sig div : A -> A -> A
-	    mod : A -> A -> A
-
-div : (A : Type) -> Div A -> A -> A -> A
-div _ d = d.div
-
-mod : (A : Type) -> Div A -> A -> A -> A
-mod _ d = d.mod
-
--- Operators:
-
-{- 
-  (x / y) => (div ? ? x y)
-  (x % y) => (mod ? ? x y)
--}
-
-
-
-
-
---
--- The Neg class
---
-
-Neg : Type -> Type
-Neg A = sig negate : A -> A
-
-negate : (A : Type) -> Neg A -> A -> A
-negate _ d = d.negate
-
--- Operators:
-
-{-
-  (-x) => negate ? ? x
--}
-
-
-
-
---
--- 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
---
-
-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
-
-
-
-
-
-
---
--- The Monoid class
---
-
-Monoid : Type -> Type
-Monoid A = sig mzero : A
-	       mplus : A -> A -> A
-
-
-
-
---
--- The Compos class
---
-
-Compos : (C : Type) -> (C -> Type) -> Type
-Compos C T = sig 
-  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 : (C : Type) -> (T : C -> Type) -> (d : Compos C T) 
-        -> (c : C) -> ((a : C) -> T a -> T a) -> T c -> T c
-composOp _ _ d = d.composOp
-
-composFold : (C : Type) -> (T : C -> Type) -> (d : Compos C T) -> (B : Type) -> Monoid B 
-          -> (c : C) -> ((a : C) -> T a -> b) -> T c -> b
-composFold _ _ d = d.composFold
-
-
-
-
-
---
--- The Monad class
---
-
-Monad : (Type -> Type) -> Type
-Monad M = sig return : (A : Type) -> M A
-	      bind : (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B
-
-return : (M : Type -> Type) -> Monad M -> M A
-return _ d = d.return
-
-bind : (M : Type -> Type) -> Monad M 
-    -> (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B
-bind _ d = d.bind
-
--- Operators:
-
-{-
-  (x >>= y) => bind ? ? ? ? x y
-  (x >>  y) => bind ? ? ? ? x (\_ -> y)
--}
-
diff --git a/transfer/lib/vector.tra b/transfer/lib/vector.tra
deleted file mode 100644
index 2eda35167..000000000
--- a/transfer/lib/vector.tra
+++ /dev/null
@@ -1,15 +0,0 @@
--- NOTE: this is unfinished and untested
-
-import nat
-
-data Vector : Type -> Nat -> Type where
-   Empty : (A:Type) -> Vector A Zero
-   Cell : (A:Type) -> (n:Nat) -> A -> Vector A n -> Vector A (Succ n)
-
-mapV : (A:Type) -> (B:Type) -> (n:Nat) -> (A -> B) -> Vector A n -> Vector B n
-mapV A B _ f (Empty _) = Empty B
-mapV A B (Succ n) f (Cell _ _ x xs) = Cell B n (f x) (mapV A B n f xs)
-
-appendV : (A:Type) -> (n:Nat) -> (m:Nat) -> Vector A n -> Vector A m -> Vector A (plusNat n m)
-appendV A _ _ (Empty _) ys = ys
-appendV A (Succ n) m (Cell _ _ x xs) ys = appendV A n (Succ m) xs (Cell A m x ys)