Changed all example programs to use layout syntax.

transfer/examples/array.tr

@@ -1,10 +1,9 @@
-import nat ;
+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) ;
- } ;
+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) ;
+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,8 +1,10 @@
-data Bool : Type where { True : Bool; False : Bool; } ;
+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 ;
+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 ;
+not : Bool -> Bool
+not b = if b then False else True

transfer/examples/fib.tr

@@ -1,11 +1,11 @@
-import nat ;
+import nat
 
-fib : Int -> Int ;
-fib 0 = 1 ;
-fib 1 = 1 ;
-fib n = fib (n-1) + fib (n-2) ;
+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) ;
+fibNat : Nat -> Nat
+fibNat Zero = Succ Zero
+fibNat (Succ Zero) = Succ Zero
+fibNat (Succ (Succ n)) = plus (fibNat (Succ n)) (fibNat n)

transfer/examples/list.tr

@@ -1,17 +1,17 @@
-import nat ;
+import nat
 
 data List : (_:Type) -> Type where 
-	{ Nil : (A:Type) -> List A ;
-          Cons : (A:Type) -> A -> List A -> List A ; } ;
+	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) ;
+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) ;
+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) ;
+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/nat.tr

@@ -1,23 +1,22 @@
-data Nat : Type where { 
-	Zero : Nat ;
-  	Succ : (n:Nat) -> Nat ;
- } ;
+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) ;
+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 ;
+pred : Nat -> Nat
+pred Zero = Zero
+pred (Succ n) = n
 
-natToInt : Nat -> Int ;
-natToInt Zero = 0 ;
-natToInt (Succ n) = 1 + natToInt 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) ;
+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)) ;
+intToNat : Int -> Nat
+intToNat n = if n == 0 then Zero else Succ (intToNat (n-1))

transfer/examples/overload.tr

@@ -0,0 +1,16 @@
+Additive : Type -> Type
+Additive A = { zero : A; plus : A -> A -> A }
+
+additive_Integer : Additive Integer
+additive_Integer = { zero = 0; plus = prim_add_Int }
+
+sum : (A:Type) -> Additive A -> List A -> A
+sum _ d (Nil _) = d.zero
+sum A d (Cons _ x xs) = d.plus x (sum A d xs)
+
+Showable : Type -> Type
+Showable A = { show : A -> String }
+
+
+--Compositional : Type -> Type
+--Compositional A = { composOp : }

transfer/examples/pair.tr

@@ -1,11 +1,11 @@
-Pair : Type -> Type -> Type ;
-Pair A B = { p1 : A; p2 : B } ;
+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 } ;
+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 } ;
+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 } ;
+snd : (A:Type) -> (B:Type) -> Pair A B -> B
+snd _ _ p = case p of Pair _ _ x _ -> x

transfer/examples/prelude.tr

@@ -1,5 +1,5 @@
-const : (A:Type) -> (B:Type) -> A -> B -> A ;
-const _ _ x _ = x ;
+const : (A:Type) -> (B:Type) -> A -> B -> A
+const _ _ x _ = x
 
-id : (A:Type) -> A -> A ;
-id A x = x ;
+id : (A:Type) -> A -> A
+id _ x = x

transfer/examples/prim.tr

@@ -1,23 +0,0 @@
---
--- 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 ;

transfer/examples/test.tr

@@ -1,3 +1,3 @@
-import nat ;
+import nat
 
-main = natToInt (intToNat 100) ;
+main = natToInt (intToNat 100)