Move transfer into the GF repo.

11 files changed, 147 insertions, 0 deletions

diff --git a/transfer/examples/array.tr b/transfer/examples/array.tr
new file mode 100644
index 000000000..7dcf6d443
--- /dev/null
+++ b/transfer/examples/array.tr
@@ -0,0 +1,10 @@
+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/examples/bool.tr b/transfer/examples/bool.tr
new file mode 100644
index 000000000..291434a9f
--- /dev/null
+++ b/transfer/examples/bool.tr
@@ -0,0 +1,8 @@
+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 ;
diff --git a/transfer/examples/exp.tr b/transfer/examples/exp.tr
new file mode 100644
index 000000000..b7202fedf
--- /dev/null
+++ b/transfer/examples/exp.tr
@@ -0,0 +1,31 @@
+data Stm : Type where {} ;
+data Exp : Type where {} ;
+data Var : Type where {} ;
+data Typ : Type where {} ;
+
+data ListStm : Type where {} ;
+
+data Tree : Type -> Type where {
+  SDecl   : Tree Typ -> Tree Var -> Tree Stm ;
+  SAss    : Tree Var -> Tree Exp -> Tree Stm ;
+  SBlock  : Tree ListStm -> Tree Stm ;
+  EAdd    : Tree Exp -> Tree Exp -> Tree Exp ;
+  EStm    : Tree Stm -> Tree Exp ;
+  EVar    : Tree Var -> Tree Exp ;
+  EInt    : Integer -> Tree Exp ;
+  V       : String -> Tree Var ;
+  TInt    : Tree Typ ;
+  TFloat  : Tree Typ ;
+
+  NilStm  : Tree ListStm ;
+  ConsStm : Tree Stm -> Tree ListStm -> Tree ListStm ;
+ } ;
+
+derive composOp Tree ;
+
+rename : (String -> String) -> (C : Type) -> Tree C -> Tree C;
+rename f C t = case t of {
+		   V x -> V (f x) ;
+		   _ -> composOp_Tree C (rename f) t;
+                 } ;
+
diff --git a/transfer/examples/fib.tr b/transfer/examples/fib.tr
new file mode 100644
index 000000000..91bb69ed7
--- /dev/null
+++ b/transfer/examples/fib.tr
@@ -0,0 +1,11 @@
+import nat ;
+
+fib : Int -> Int ;
+fib 0 = 1 ;
+fib 1 = 1 ;
+fib n = fib (n-1) + fib (n-2) ;
+
+fibNat : Nat -> Nat ;
+fibNat Zero = Succ Zero ;
+fibNat (Succ Zero) = Succ Zero ;
+fibNat (Succ (Succ n)) = plus (fibNat (Succ n)) (fibNat n) ;
\ No newline at end of file
diff --git a/transfer/examples/layout.tr b/transfer/examples/layout.tr
new file mode 100644
index 000000000..15f0aac3a
--- /dev/null
+++ b/transfer/examples/layout.tr
@@ -0,0 +1,5 @@
+x : Apa
+x = let x : T = y 
+     in case y of
+         f -> q
+         _ -> a
diff --git a/transfer/examples/list.tr b/transfer/examples/list.tr
new file mode 100644
index 000000000..f31278f54
--- /dev/null
+++ b/transfer/examples/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/examples/nat.tr b/transfer/examples/nat.tr
new file mode 100644
index 000000000..f67dc55ce
--- /dev/null
+++ b/transfer/examples/nat.tr
@@ -0,0 +1,23 @@
+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 ;
+
+plus : Nat -> Nat -> Nat ;
+plus Zero y = y ;
+plus (Succ x) y = Succ (plus x y) ;
+
+intToNat : Int -> Nat ;
+intToNat n = if n == 0 then Zero else Succ (intToNat (n-1)) ;
diff --git a/transfer/examples/pair.tr b/transfer/examples/pair.tr
new file mode 100644
index 000000000..07182e301
--- /dev/null
+++ b/transfer/examples/pair.tr
@@ -0,0 +1,11 @@
+Pair : Type -> Type -> Type ;
+Pair A B = { p1 : A; p2 : B } ;
+
+pair : (A:Type) -> (B:Type) -> A -> B -> Pair A B ;
+pair _ _ x y = { 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/examples/prelude.tr b/transfer/examples/prelude.tr
new file mode 100644
index 000000000..a7e7443a1
--- /dev/null
+++ b/transfer/examples/prelude.tr
@@ -0,0 +1,5 @@
+const : (A:Type) -> (B:Type) -> A -> B -> A ;
+const _ _ x _ = x ;
+
+id : (A:Type) -> A -> A ;
+id A x = x ;
\ No newline at end of file
diff --git a/transfer/examples/prim.tr b/transfer/examples/prim.tr
new file mode 100644
index 000000000..fe0d32eac
--- /dev/null
+++ b/transfer/examples/prim.tr
@@ -0,0 +1,23 @@
+--
+-- Primitives
+--
+
+
+String : Type ;
+
+Int : Type ;
+
+prim_add_Int : (_:Int) -> (_:Int) -> Int ;
+prim_sub_Int : (_:Int) -> (_:Int) -> Int ;
+prim_mul_Int : (_:Int) -> (_:Int) -> Int ;
+prim_div_Int : (_:Int) -> (_:Int) -> Int ;
+prim_mod_Int : (_:Int) -> (_:Int) -> Int ;
+
+prim_neg_Int : (_:Int) -> Int ;
+
+prim_lt_Int : (_:Int) -> (_:Int) -> Bool ;
+prim_le_Int : (_:Int) -> (_:Int) -> Bool ;
+prim_gt_Int : (_:Int) -> (_:Int) -> Bool ;
+prim_ge_Int : (_:Int) -> (_:Int) -> Bool ;
+prim_eq_Int : (_:Int) -> (_:Int) -> Bool ;
+prim_ne_Int : (_:Int) -> (_:Int) -> Bool ;
diff --git a/transfer/examples/test.tr b/transfer/examples/test.tr
new file mode 100644
index 000000000..50aa638b4
--- /dev/null
+++ b/transfer/examples/test.tr
@@ -0,0 +1,3 @@
+import nat ;
+
+main = natToInt (intToNat 100) ;
\ No newline at end of file