diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,27 @@
+Copyright (c) 2008--2009 Thorsten Altenkirch, Andres Loeh
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,3 @@
+import Distribution.Simple
+
+main = defaultMain
diff --git a/examples/Bool.pi b/examples/Bool.pi
new file mode 100644
--- /dev/null
+++ b/examples/Bool.pi
@@ -0,0 +1,15 @@
+:l Empty.pi
+:l Unit.pi
+
+Bool : Type;
+Bool = { true false };
+
+T : Bool -> Type;
+T = \ b -> case b of {
+             true -> Unit
+	   | false -> Empty };
+
+andb : Bool -> Bool -> Bool;
+andb = \ b c -> case b of {
+                  true -> c
+                | false -> 'false };
diff --git a/examples/Conat.pi b/examples/Conat.pi
new file mode 100644
--- /dev/null
+++ b/examples/Conat.pi
@@ -0,0 +1,83 @@
+:l Empty.pi
+:l Unit.pi
+
+Nat' : Type;
+Nat' = (l : { z s }) * case l of {
+                           z -> Unit
+			 | s -> [^ Nat'] };
+
+
+zero : Nat';
+zero = ('z,'unit);
+
+succ : ^Nat' -> Nat';
+succ = \ n -> ('s,n);
+
+one : Nat';
+one = succ [zero];
+
+two : Nat';
+two = succ [one];
+
+omega : Nat';
+omega = succ [omega];
+
+
+add : Nat' -> Nat' -> Nat';
+add = \ m n -> split m with (lm , m') ->
+                 case lm of {
+		     z -> n
+ 		   | s -> succ [add (!m') n] };
+
+eq : Nat' -> Nat' -> Type;
+eq = \ m n -> split m with (lm , m') ->
+              split n with (ln , n') ->
+                   case lm of {
+		     z -> case ln of { 
+		             z -> Unit
+			   | s -> Empty }
+	           | s -> case ln of { 
+		             z -> Empty
+			   | s -> [^ (eq (! m') (! n'))]}};
+
+
+refl : (n:Nat') -> eq n n;
+refl = \ n -> split n with (ln , n') ->
+       	          case ln of {
+		     z -> 'unit
+		   | s -> [refl (!n')] };
+
+sym : (m:Nat') -> (n:Nat') -> eq m n -> eq n m;
+sym = \ m n p -> 
+              split m with (lm , m') ->
+              split n with (ln , n') ->
+                   case lm of {
+		     z -> case ln of {
+		             z -> 'unit
+			   | s -> case p of {}}
+	           | s -> case ln of { 
+		             z -> case p of {}
+			   | s -> [sym (! m') (! n') (! p)] }};
+
+{-
+subst : (P : Nat' -> Type) 
+      -> (m : Nat') -> (n : Nat')
+      -> (eq m n)
+      -> P m -> ^ (P n);
+subst = \ P m n q x -> 
+              split m with (lm , m') ->
+              split n with (ln , n') ->
+                 case lm of {
+		     z -> case ln of {
+		             z -> case m' of {
+			             unit -> case n' of {
+				                unit -> [x] }}
+			   | s -> case q of {}}
+	           | s -> case ln of { 
+		             z -> case q of {}
+			   | s -> [subst (\ i -> P (succ i)) (! m') (! n') (! q) x]}};
+-}
+
+{- seems we need an eliminator for boxes, e.g. unbox
+-}
+
diff --git a/examples/Data.pi b/examples/Data.pi
new file mode 100644
--- /dev/null
+++ b/examples/Data.pi
@@ -0,0 +1,107 @@
+:l Maybe.pi
+:l Bool.pi
+
+data : Type;
+El : data -> Type;
+
+data = ( l : {empty maybe sigma box} ) * 
+       case l of {
+         empty -> Unit
+       | maybe -> [data]
+       | sigma -> [(a : data) * (El a -> data)]
+       | box -> [^ data] };  
+
+El = \ a -> split a with (la,a') ->
+            case la of {
+	      empty -> {}
+	    | maybe -> [Maybe (El a')]
+	    | sigma -> split a' with (b,c) ->
+	      	         [(x:El b)*(El (c x))]
+            | box -> [El (! a')] };
+
+unit : data;
+unit = ('maybe,('empty,'unit));
+
+un : El unit;
+un = ('nothing,'unit);
+
+bool : data;
+bool = ('maybe, unit);
+
+tt : El bool;
+tt = ('nothing,'unit);
+
+ff : El bool;
+ff = ('just,('nothing,'unit));
+
+nat : data;
+nat = ('sigma,(bool,\ b -> split b with (lb,b') ->
+      		      	     case lb of {
+			       nothing -> unit
+			     | just -> ('box, [nat]) }));
+      		      	     
+zero : El nat;
+zero = (tt,un);
+
+succ : El nat -> El nat;
+succ = \ n -> (ff,n);
+
+Eq : Type -> Type;
+Eq = \ A -> A -> A -> Bool;
+
+eqMaybe : (A:Type) -> Eq A -> Eq (Maybe A);
+eqMaybe = \ A eqA a b ->
+	  split a with (la,a') ->
+	  split b with (lb,b') ->
+	  case la of {
+	    nothing -> case lb of {
+	    	         nothing -> 'true 
+		       | just -> 'false }
+          | just -> case lb of {
+	    	         nothing -> 'false
+		       | just -> eqA a' b'}};
+
+
+eq : (a : data) -> Eq (El a);
+
+subst : (a : data) 
+        -> (x:El a) -> (y : El a) -> T (eq a x y)
+	-> (P : El a -> Type) -> P x -> P y;
+
+sigmab : (b : Bool) -> (T b -> Bool) -> Bool;
+sigmab = \ b c -> case b of {
+       	            true -> c 'unit
+		  | false -> 'false };
+
+eq = \ a x y -> split a with (la,a') ->
+       	        ! case la of {
+		    empty -> case x of {} 
+		  | maybe -> [eqMaybe (El a') (eq a') x y]
+  		  | sigma -> split a' with (b,c) ->
+		  	     split x with (x0,x1) ->
+			     split y with (y0,y1) ->
+			       [sigmab (eq b x0 y0)
+			   	 (\ p -> eq (c y0) 
+				            (subst b x0 y0 p (\ x -> El (c x))
+					    	    x1) y1)]
+                  | box -> [eq (! a') x y]}; 					   
+
+{-
+subst = \ a x y p P px ->
+        split a with (la,a') ->
+       	        ! case la of {
+		    empty -> case x of {} 
+		  | maybe -> split x with (lx,x') ->
+		  	     split y with (ly,y') ->  
+	                     case lx of {
+	                       nothing -> (case ly of {
+	    	                             nothing -> (case x' of {
+					     	           unit -> case y' of {
+							             unit -> [px] } })
+					   | just -> case p of {}})
+			      | just -> case ly of {
+			       	             nothing -> (case p of {})
+					   | just -> [subst a' x' y' p (\ z -> P ('just,z)) px]}}
+  		  | sigma -> [subst a x y p P px]
+                  | box -> [subst (! a') x y p P px]};       	
+-}
diff --git a/examples/Empty.pi b/examples/Empty.pi
new file mode 100644
--- /dev/null
+++ b/examples/Empty.pi
@@ -0,0 +1,2 @@
+Empty : Type;
+Empty = { };
diff --git a/examples/EqProb.pi b/examples/EqProb.pi
new file mode 100644
--- /dev/null
+++ b/examples/EqProb.pi
@@ -0,0 +1,39 @@
+Eq : (a:Type) -> a -> a -> Type;
+Eq = \ a x y -> (P : a -> Type) -> P x -> P y;
+
+refl : (a:Type) -> (x:a) -> Eq a x x;
+refl = \ a x P px -> px;
+
+Stream : Type;
+Stream = (tag : {Cons}) * case tag of {Cons -> [^Stream] };
+
+ticks : Stream;
+ticks = ('Cons, [ticks]);
+
+l1 : Eq Stream ticks ('Cons, [ticks]);
+l1 = refl Stream ticks;
+
+l2 : (s : Stream) -> (t : Stream) -> (Eq Stream s t)
+                 -> Eq Stream ('Cons, [s]) ('Cons, [t]);
+l2 = \ s t q P p -> q (\ x -> P ('Cons,[x])) p;
+
+{- bad error message! -}
+
+{- unbox x with [y] -> t 
+
+   |- C : Type
+   |- x : ^A
+   y:A, x==[y] |- t : C
+   -----------------------------
+   |- unbox x with [y] -> t : C
+
+   unbox [a] with [y] -> t ==> let y=a in t
+
+
+   ![a] = a
+
+-}
+
+{-
+l3 : (A:Type) -> (a:A) -> (b:A) -> Eq A a b -> Eq (^A) [a] [b];
+-}
diff --git a/examples/Equal.pi b/examples/Equal.pi
new file mode 100644
--- /dev/null
+++ b/examples/Equal.pi
@@ -0,0 +1,54 @@
+Eq : (a:Type) -> a -> a -> Type;
+Eq = \ a x y -> (P : a -> Type) -> P x -> P y;
+
+refl : (a:Type) -> (x:a) -> Eq a x x;
+refl = \ a x P px -> px;
+
+A : Type;
+a : A;
+
+b : A;
+b = a;
+
+t0 : Eq A a b;
+t0 = refl A a;
+
+{-
+c : A;
+t1 : Eq A a c;
+t1 = refl A a;
+-}
+
+d : ^A;
+d = [a];
+
+t2 : Eq (^A) d [a];
+t2 = refl (^A) [a];
+
+{-
+t3 : Eq (^A) [a] [b];
+t3 = refl (^A) [a];
+-}
+
+e : A;
+e = a;
+
+t4 : Eq (^A) [e] [b];
+t4 = refl (^A) [e];
+
+id : A -> A;
+id = \ x -> x;
+
+f : A;
+f = id a;
+
+t5 : Eq (^A) [f] [b];
+t5 = refl (^A) [f];
+{-
+? f = b
+? id a = a [f=b=b]
+-}
+
+t6 : Eq A (id a) a;
+t6 = refl A a;
+
diff --git a/examples/Fin.pi b/examples/Fin.pi
new file mode 100644
--- /dev/null
+++ b/examples/Fin.pi
@@ -0,0 +1,40 @@
+:l Nat.pi
+
+Fin : Nat -> Type;
+Fin = \ n -> split n with (ln , n') ->
+                 ! case ln of {
+		     z -> [Empty]
+		   | s -> [(l : { z s }) * case l of {
+                                             z -> Unit
+			                   | s -> Fin n'}]};
+
+fz : (n:Nat) -> Fin (succ n);
+fz = \ n -> ('z , 'unit );
+
+fs : (n:Nat) -> Fin n -> Fin (succ n);
+fs = \ n i -> ('s, i);
+
+fmax : (n:Nat) -> Fin (succ n);
+fmax = \ n -> split n with (ln , n') ->
+                 ! case ln of {
+		     z -> [fz zero]
+		   | s -> [fs n (fmax n')] };
+
+femb : (n:Nat) -> Fin n -> Fin (succ n);
+femb = \ n i -> split n with (ln , n') ->
+                 ! case ln of {
+		     z -> case i of {}
+		   | s -> split i with (li , i') ->
+		       	     case li of {
+ 			       z -> [fz n]
+		             | s -> [fs n (femb n' i')] }};
+
+finv : (n:Nat) -> Fin n -> Fin n;
+finv = \ n i -> split n with (ln , n') ->
+                 ! case ln of {
+		     z -> case i of {}
+		   | s -> split i with (li , i') ->
+		       	     case li of {
+ 			       z -> [fmax n']
+			     | s -> [fs n' (finv n' i')] }};
+
diff --git a/examples/Maybe.pi b/examples/Maybe.pi
new file mode 100644
--- /dev/null
+++ b/examples/Maybe.pi
@@ -0,0 +1,10 @@
+:l Unit.pi
+
+Maybe : Type -> Type;
+Maybe = \ A -> (l : { nothing just }) *
+               case l of {
+	          nothing -> Unit
+	        | just -> A };
+
+
+          
diff --git a/examples/Nat.pi b/examples/Nat.pi
new file mode 100644
--- /dev/null
+++ b/examples/Nat.pi
@@ -0,0 +1,94 @@
+:l Bool.pi
+
+Nat : Type;
+Nat = (l : { z s }) * case l of {
+                           z -> Unit
+			 | s -> [Nat] };
+
+zero : Nat;
+zero = ('z,'unit);
+
+succ : Nat -> Nat;
+succ = \ n -> ('s,n);
+
+one : Nat;
+one = succ zero;
+
+two : Nat;
+two = succ one;
+
+add : Nat -> Nat -> Nat;
+add = \ m n -> split m with (lm , m') ->
+                 ! case lm of {
+		     z -> [n]
+ 		   | s -> [succ (add m' n)] };
+
+
+eqbNat : Nat -> Nat -> Bool;
+eqbNat = \ m n -> split m with (lm , m') ->
+                  split n with (ln , n') ->
+                  ! case lm of {
+		     z -> case ln of { 
+		             z -> ['true]
+			   | s -> ['false] }
+	           | s -> case ln of {
+		             z -> ['false]
+			   | s -> [eqbNat m' n'] } };
+
+eqNat : Nat -> Nat -> Type;
+eqNat = \ m n -> T (eqbNat m n);
+
+reflNat : (n:Nat) -> eqNat n n;
+reflNat = \ n -> split n with (ln , n') ->
+       	        ! case ln of {
+		     z -> ['unit]
+		   | s -> [reflNat n'] };
+
+substNat : (P : Nat -> Type) 
+      -> (m : Nat) -> (n : Nat)
+      -> (eqNat m n)
+      -> P m -> P n;
+substNat = \ P m n q x -> 
+              split m with (lm , m') ->
+              split n with (ln , n') ->
+                 ! case lm of {
+		     z -> case ln of {
+		             z -> case m' of {
+			             unit -> case n' of {
+				                unit -> [x]}}
+			   | s -> case q of {}}
+	           | s -> case ln of { 
+		             z -> case q of {}
+			   | s -> [substNat (\ i -> P (succ i)) m' n' q x]}};
+
+
+symNat : (m:Nat) -> (n:Nat) -> eqNat m n -> eqNat n m;
+symNat = \ m n p -> substNat (\ i -> eqNat i m) m n p (reflNat m);
+
+transNat : (i:Nat) -> (j:Nat) -> (k:Nat) ->
+      eqNat i j -> eqNat j k -> eqNat i k;
+transNat = \ i j k p q -> substNat (\ x -> eqNat i x) j k q p;
+
+addCom0 : (n:Nat) -> eqNat n (add n zero);
+addCom0 = \ n -> split n with (ln , n') ->
+	         ! case ln of { 
+		      z -> case n' of {
+		              unit -> [reflNat zero]}
+	            | s -> [addCom0 n'] };
+
+addComS : (m:Nat) -> (n:Nat) ->
+	  (eqNat  (add (succ m) n) (add m (succ n)));
+addComS = \ m n -> split m with (lm , m') ->
+	           ! case lm of {
+		       z -> [reflNat (succ n)]
+		     | s -> [addComS m' n] };
+
+addCom : (m:Nat) -> (n:Nat) ->
+	  (eqNat (add m n) (add n m));
+addCom = \ m n ->  split m with (lm , m') ->
+	           ! case lm of {
+		       z ->  case m' of {
+		                unit -> [addCom0 n] }
+		     | s -> [transNat (add (succ m') n) (add (succ n) m') (add n (succ m'))
+		                      (addCom m' n) (addComS n m')] };
+
diff --git a/examples/Streams.pi b/examples/Streams.pi
new file mode 100644
--- /dev/null
+++ b/examples/Streams.pi
@@ -0,0 +1,91 @@
+Unit : Type;
+Unit = { unit };
+
+Empty : Type;
+Empty = { };
+
+Bool : Type;
+Bool = { true false };
+
+T : Bool -> Type;
+T = \ b -> case b of {
+             true -> Unit
+	   | false -> Empty };
+
+
+Nat : Type;
+Nat = (l : { z s }) * case l of {
+                           z -> Unit
+			 | s -> [Nat] };
+
+zero : Nat;
+zero = ('z,'unit);
+
+succ : Nat -> Nat;
+succ = \ n -> ('s,n);
+
+one : Nat;
+one = succ zero;
+
+two : Nat;
+two = succ one;
+
+add : Nat -> Nat -> Nat;
+add = \ m n -> split m with (lm , m') ->
+                 ! case lm of {
+		     z -> [n]
+ 		   | s -> [succ (add m' n)] };
+
+eqbNat : Nat -> Nat -> Bool;
+eqbNat = \ m n -> split m with (lm , m') ->
+                  split n with (ln , n') ->
+                  ! case lm of {
+		     z -> case ln of { 
+		             z -> ['true]
+			   | s -> ['false] }
+	           | s -> case ln of {
+		             z -> ['false]
+			   | s -> [eqbNat m' n'] } };
+
+eqNat : Nat -> Nat -> Type;
+eqNat = \ m n -> T (eqbNat m n);
+
+reflNat : (n:Nat) -> eqNat n n;
+reflNat = \ n -> split n with (ln , n') ->
+       	        ! case ln of {
+		     z -> ['unit]
+		   | s -> [reflNat n'] };
+
+
+Stream : Type -> Type;
+Stream = \ a -> a * [^ (Stream a)];
+
+put : (a : Type) -> a -> Stream a -> Stream a;
+put = \ a x xs -> (x,[xs]);
+
+from : Nat -> Stream Nat;
+from = \ n -> (n, [from (succ n)]);
+
+tail : (a:Type) -> Stream a -> Stream a;
+tail = \ a xs -> split xs with (x , xs') -> ! xs';
+
+head : (a:Type) -> Stream a -> a;
+head = \ a xs -> split xs with (x , xs') -> x;
+
+map : (a : Type) -> (b : Type) -> (a -> b) -> Stream a -> Stream b;
+map = \ a b f xs -> split xs with (x , xs') -> (f x, [map a b f (! xs')]);
+
+eqStream : (a : Type) -> (a -> a -> Type) -> Stream a -> Stream a -> Type;
+eqStream = \ a eq xs ys -> split xs with (x , xs') ->
+	                   split ys with (y , ys') ->
+			   	 (eq x y) * [^ (eqStream a eq (! xs') (! ys'))];
+
+reflStream :  (a : Type) -> (eq : a -> a -> Type) 
+	   -> ((x : a) -> eq x x)
+	   -> (xs : Stream a) -> eqStream a eq xs xs;
+reflStream = \ a eq refl xs -> split xs with (x , xs') -> 
+	       	    	         ((refl x), [reflStream a eq refl (! xs')]);
+
+lemma : (n : Nat) -> eqStream Nat eqNat (from (succ n)) 
+                                        (map Nat Nat succ (from n));
+lemma = \ n -> ((reflNat (succ n)),[lemma (succ n)]);  
diff --git a/examples/Unit.pi b/examples/Unit.pi
new file mode 100644
--- /dev/null
+++ b/examples/Unit.pi
@@ -0,0 +1,2 @@
+Unit : Type;
+Unit = { unit };
diff --git a/examples/Universe.pi b/examples/Universe.pi
new file mode 100644
--- /dev/null
+++ b/examples/Universe.pi
@@ -0,0 +1,47 @@
+:l Maybe.pi
+
+data : Type;
+El : data -> Type;
+
+data = ( l : {empty maybe sigma box} ) * 
+       case l of {
+         empty -> Unit
+       | maybe -> [data]
+       | sigma -> [(a : data) * (El a -> data)]
+       | box -> [^ data] };  
+
+El = \ a -> split a with (la,a') ->
+            case la of {
+	      empty -> {}
+	    | maybe -> Maybe [El a']
+	    | sigma -> split a' with (b,c) ->
+	      	         [(x:El b)*(El (c x))]
+            | box -> [El (! a')] };
+
+unit : data;
+unit = ('maybe,('empty,'unit));
+
+un : El unit;
+un = ('nothing,'unit);
+
+bool : data;
+bool = ('maybe, unit);
+
+tt : El bool;
+tt = ('nothing,'unit);
+
+ff : El bool;
+ff = ('just,('nothing,'unit));
+
+nat : data;
+nat = ('sigma,(bool,\ b -> split b with (lb,b') ->
+      		      	     case lb of {
+			       nothing -> unit
+			     | just -> ('box, [nat]) }));
+      		      	     
+zero : El nat;
+zero = (tt,un);
+
+succ : El nat -> El nat;
+succ = \ n -> (ff,n);
+
diff --git a/examples/Vec.pi b/examples/Vec.pi
new file mode 100644
--- /dev/null
+++ b/examples/Vec.pi
@@ -0,0 +1,23 @@
+:l Fin.pi
+
+Vec : Nat -> Type -> Type;
+Vec = \ m a -> split m with (lm , m') ->
+                 ! case lm of {
+		     z -> [Unit]
+		   | s -> [a * Vec m' a] }; 
+
+vnil : (a : Type) -> Vec zero a;
+vnil = \ a -> 'unit;
+
+vcons : (a : Type) -> (n : Nat) -> a -> Vec n a -> Vec (succ n) a;
+vcons = \ a b x xs -> (x ,xs);
+
+nth : (a : Type) -> (n : Nat) -> (xs : Vec n a) -> Fin n -> a;
+nth = \ a n xs i -> split n with (ln , n') ->
+      	       	    ! case ln of {
+		        z -> case i of {}
+		      | s -> split xs with (x, xs') ->
+		             split i with (li , i') ->
+		               case li of {
+		 	         z -> [x]
+		               | s -> [nth a n' xs' i']}}
diff --git a/examples/stl.pi b/examples/stl.pi
new file mode 100644
--- /dev/null
+++ b/examples/stl.pi
@@ -0,0 +1,131 @@
+:l Bool.pi
+
+{- stl.pi
+
+Encoding of the simply typed lambda calculus
+-}
+
+pair : (a:Bool) -> (b:Bool) -> ((T a) * (T b)) -> T (andb a b);
+pair = \ a b xy ->
+       split xy with (x,y) -> 
+       case a of {
+         true -> y
+       | false -> case x of {}};
+
+unpair : (a:Bool) -> (b:Bool) -> T (andb a b) -> ((T a) * (T b));
+unpair = \ a b x ->
+       case a of {
+         true -> case b of {
+	            true -> ('unit,'unit)
+		  | false -> case x of {}}
+       | false -> case x of {}};
+
+Ty : Type;
+Ty = (l : {base arr}) * 
+     case l of {
+       base -> Unit
+     | arr -> [Ty * Ty] };
+
+base : Ty;
+base = ('base, 'unit);
+
+arr : Ty -> Ty -> Ty;
+arr = \ a b -> ('arr,(a,b));
+
+eqb : Ty -> Ty -> Bool;
+eqb = \ a b -> split a with (la, a') ->
+               split b with (lb, b') ->
+	       ! case la of {
+	           base -> case lb of { 
+		   	     base -> ['true]
+ 			   | arr -> ['false]}
+		 | arr -> case lb of {
+		       	     base -> ['false]
+			   | arr -> split a' with (a0, a1) ->
+			            split b' with (b0, b1) ->
+				      [andb (eqb a0 b0) (eqb a1 b1)]}};
+
+eq : Ty -> Ty -> Type;
+eq = \ a b -> T (eqb a b);
+
+refl : (a:Ty) -> eq a a;
+refl = \ a -> split a with (la, a') ->
+              ! case la of {
+	           base -> ['unit]
+		 | arr -> split a' with (b,c) ->
+		       	    [pair (eqb b b) (eqb c c) ((refl b) , (refl c))] };
+
+subst : (P : Ty -> Type) 
+      -> (a : Ty) -> (b : Ty)
+      -> (eq a b)
+      -> P a -> P b;
+subst = \ P a b p x -> 
+      	       split a with (la, a') ->
+               split b with (lb, b') ->
+	       ! case la of {
+	           base -> case lb of {
+		   	      base -> case a' of {
+			                 unit -> case b' of {
+					            unit -> [x]}}
+			    | arr -> case p of {}}
+                 | arr -> case lb of {
+		       	     base -> case p of {}
+			   | arr -> split a' with (a0 , a1) ->
+			            split b' with (b0 , b1) ->
+				    split (unpair (eqb a0 b0) (eqb a1 b1) p) with (p0, p1) ->
+				      [subst (\ z -> P (arr b0 z)) a1 b1 p1
+				             (subst (\ y -> P (arr y a1)) a0 b0 p0 x)]}};
+				    
+{- subst succesfully uses split on a non-variable! -}
+
+Con : Type;
+Con = ( l : {empty ext} ) * 
+      case l of {
+        empty -> Unit
+      | ext -> [Con * Ty] };
+
+empty : Con;
+empty = ('empty,'unit);
+
+ext : Con -> Ty -> Con;
+ext = \ g a -> ('ext,(g,a));
+
+Var : Con -> Ty -> Type;
+Var = \ g a -> 
+      split g with (lg, g') -> 
+      case lg of {
+        empty -> Empty
+      | ext -> split g' with (d, a') ->
+                  (l : {vz vs}) *
+		  ! case l of {
+		      vz -> [eq a a']
+		    | vs -> [Var d a] }};
+
+vz : (g:Con) -> (a:Ty) -> Var (ext g a) a;
+vz = \ g a -> ('vz, (refl a));
+	
+vs : (g:Con) -> (a:Ty) -> (b:Ty) -> Var g a -> Var (ext g b) a;
+vs = \ g a b x -> ('vs,x);
+
+Lam : Con -> Ty -> Type;
+Lam = \ g a -> 
+      (l : {var app lam}) *
+      case l of {
+         var -> Var g a
+       | app -> [(b : Ty) * ((Lam g (arr b a)) * (Lam g b))]
+       | lam -> split a with (la, a') ->
+       	     	case la of {
+		  base -> Empty
+		| arr -> split a' with (b, c) ->
+		           [Lam (ext g b) c] }};
+		  
+var : (g:Con) -> (a:Ty) -> Var g a -> Lam g a;
+var = \ g a x -> ('var,x);
+
+app : (g:Con) -> (a:Ty) -> (b:Ty)
+      -> Lam g (arr a b) -> Lam g a -> Lam g b;
+app = \ g a b t u -> ('app,(a,(t,u)));
+
+lam : (g:Con) -> (a:Ty) -> (b:Ty)
+      -> Lam (ext g a) b -> Lam g (arr a b);
+lam = \ g a b t -> ('lam,t);
diff --git a/pisigma.cabal b/pisigma.cabal
new file mode 100644
--- /dev/null
+++ b/pisigma.cabal
@@ -0,0 +1,24 @@
+cabal-version: >= 1.6
+name:          pisigma
+version:       0.1.0.1
+license:       BSD3
+license-file:  LICENSE
+data-files:    examples/*.pi
+author:        Thorsten Altenkirch <txa@cs.nott.ac.uk>,
+               Andres Loeh <kspisigma@andres-loeh.de>
+maintainer:    Thorsten Altenkirch <txa@cs.nott.ac.uk>,
+               Andres Loeh <kspisigma@andres-loeh.de>
+description:   dependently typed core language
+synopsis:      dependently typed core language
+category:      Development, Language, Dependent Types
+build-type:    Simple
+
+executable pisigma
+  main-is:       PiSigma.hs
+  hs-source-dirs:src
+  build-depends: base >= 4 && < 5,
+                 array >= 0.2 && < 0.3,
+                 mtl >= 1.1 && < 1.2,
+                 haskeline >= 0.6 && < 0.7,
+                 parsec >= 3 && < 4,
+                 ansi-wl-pprint >= 0.5 && <1
diff --git a/src/PiSigma.hs b/src/PiSigma.hs
new file mode 100644
--- /dev/null
+++ b/src/PiSigma.hs
@@ -0,0 +1,265 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Main where
+
+import Prelude hiding (catch)
+import System.IO
+import System.Environment
+import System.Console.Haskeline hiding (catch)
+import Control.Monad
+import Control.Monad.Trans
+import Control.Monad.State
+import Control.Exception
+import Data.List
+import Data.Char
+   
+import PiSigma.Syntax
+import PiSigma.Evaluation
+import PiSigma.Check
+import PiSigma.Print
+import PiSigma.Nf
+import PiSigma.Equality
+import PiSigma.Parser
+
+main :: IO ()
+main = 
+  do
+    args <- getArgs
+    let ini = mapM_ (handleCommand . Load) args
+    liftM fst $ runStateT (runInputT 
+                            (setComplete pisigmaCompletion defaultSettings)
+                            (ini >> repl))
+                          initialReplState
+
+-- | Completion in PiSigma. For the moment, we use file name completion
+-- while in a load command, and identifier completion everywhere else.
+pisigmaCompletion :: CompletionFunc (StateT ReplState IO)
+pisigmaCompletion (x1,x2)
+  | ":l" `isPrefixOf` reverse x1 = completeFilename (x1,x2)
+  | otherwise                    = completeWord Nothing " " identifier (x1,x2)
+  where
+    identifier x = do
+                     (Scope sc,env) <- gets replState
+                     let names = map fst sc
+                         xr    = reverse x
+                         cands = filter (x `isPrefixOf`) names
+                     return $ map simpleCompletion (sort cands)
+
+type Repl = InputT (StateT ReplState IO)
+type Continue = Bool
+
+data ReplState =
+  ReplState
+    { replState :: (Scope, EnvEntries)
+    , replFiles :: [FilePath]
+    }
+
+data ReplCommand =
+    Load String
+  | Reload
+  | Quit
+  | EvalPhrase Phrase
+  | Noop
+  | Clear
+  | Equal (Term,Term)
+  | TypeOf Term
+  | Help
+
+-- TODO:
+-- browse current identifiers
+
+-- | Preliminary interpreter help message.
+help :: String
+help =
+    unlines $
+    [ "PiSigma currently supports the following commands:",
+      "",
+      "  :l         load a source file",
+      "  :r         reload current source file",
+      "  :c         clear the environment",
+      "  :t         ask for the type of a term",
+      "  :e         test two terms for beta equality",
+      "  :q         quit",
+      "",
+      "Type a declaration or an expression to evaluate it." ]
+
+initialReplState :: ReplState
+initialReplState = 
+  ReplState (emptyScope, emptyE) []
+
+replStep :: Repl Continue
+replStep =
+  do
+    f <- lift $ gets replFiles
+    x <- getInputLine (unwords (reverse f) ++ "> ")
+    c <- interpretInput x
+    handleCommand c
+
+-- | Preliminary input interpretation, based on the
+-- current parser and no particular intelligence in
+-- parsing commands correctly.
+interpretInput :: Maybe String -> Repl ReplCommand
+interpretInput Nothing  = return Quit
+interpretInput (Just x)
+  | ":l" `isPrefixOf` x = case break (== ' ') x of
+                            (x1,x2) -> return (Load (norm (trim x2)))
+  | ":r" `isPrefixOf` x = return Reload
+  | ":q" `isPrefixOf` x = return Quit
+  | ":c" `isPrefixOf` x = return Clear
+  | ":e" `isPrefixOf` x = case break (== ' ') x of
+                            (x1,x2) -> parseInputInteractive s2Terms Equal x2
+  | ":t" `isPrefixOf` x = case break (== ' ') x of
+                            (x1,x2) -> parseInputInteractive sTerm TypeOf x2
+  | ":h" `isPrefixOf` x || ":?" `isPrefixOf` x
+                        = return Help
+  | ":"  `isPrefixOf` x = replMessage "unknown command" >> return Noop
+  | otherwise           = parseInputInteractive sPhrase EvalPhrase x
+
+-- | Turn a string into a Repl command.
+parseInput :: String -> SParser t -> (t -> ReplCommand) ->
+              String -> Repl ReplCommand
+parseInput f p cmd s =
+    case parse p f s of
+      Left s     -> do
+                      liftIO $ putStrLn ("Parse error: " ++ show s ++ "\n")
+                      return Noop
+      Right p    -> return (cmd p)
+
+parseInputInteractive = parseInput "<interactive>"
+
+-- | Placeholder for a message function that can depend
+-- on verbosity settings.
+replMessage :: String -> Repl ()
+replMessage = liftIO . putStrLn
+
+-- | Command handler. Returns a flag indicating whether
+-- the interpreter should continue.
+handleCommand :: ReplCommand -> Repl Continue
+handleCommand c =
+  case c of
+    Help ->
+      do
+        replMessage $ help
+        return True
+    Load f ->
+      do
+        fs <- lift $ gets replFiles
+        if f `elem` fs then do
+            replMessage $ "Skipping " ++ f ++ "."
+            return True
+          else do
+            mx <- liftIO $ catch (liftM Just (readFile f))
+                                 (\ (_ :: IOException) -> return Nothing)
+            case mx of
+              Nothing -> do
+                replMessage $ "Could not find " ++ f ++ "."
+                return True
+              Just x -> do
+                -- Allow source files to have interpreter commands at the top;
+                -- we currently use this as a replacement for a module system
+                let (cmds,rest) = span (":" `isPrefixOf`) (lines x)
+                mapM_ (\ c -> interpretInput (Just c) >>= handleCommand) cmds
+                -- We print the "Loaded" message after executing initial
+                -- interpreter commands in order to reflect the dependency
+                -- order of different source files.
+                replMessage $ "Loaded " ++ f ++ "."
+                p <- parseInput f sProg (EvalPhrase . Prog)
+                                (unlines (replicate (length cmds) "" ++ rest))
+                lift $ modify (\ s -> s { replFiles =
+                                            case replFiles s of
+                                             (g : fs) | g == f -> g : fs
+                                             xs                -> f : xs })
+                handleCommand p
+    Reload ->
+      do
+        f <- lift $ gets replFiles
+        handleCommand Clear
+        mapM_ (handleCommand . Load) (reverse f)
+        return True
+    Quit ->
+      return False
+    EvalPhrase (Prog p) ->
+      do
+        execProg p
+        return True
+    EvalPhrase (Term t) ->
+      do
+        execTerm t
+        return True
+    Equal (t1,t2) ->
+      do
+        eqTerms t1 t2
+        return True
+    TypeOf t ->
+      do
+        inferTerm t
+        return True
+    Clear ->
+      do
+        lift $ put initialReplState
+        return True
+    Noop ->
+      return True
+
+execProg :: Prog -> Repl ()
+execProg p =
+  do
+    s <- lift get
+    let (con,env) = replState s
+    case run env (checkProg (p,con)) of
+      Right s' -> lift $ put (s { replState = s' })
+      Left e   -> liftIO $ putStrLn e
+
+execTerm :: Term -> Repl ()
+execTerm t =
+  do
+    s <- lift get
+    let (con,env) = replState s
+        p = do
+          a <- infer (t,con)
+          pa <- prt a
+          t' <- nf [] (t,con)
+          pt <- prt t'
+          return (pt++"\n: "++pa)
+    case run env p of
+        Right (m,_) -> liftIO $ putStrLn m
+        Left  e     -> liftIO $ putStrLn e
+
+eqTerms :: Term -> Term -> Repl ()
+eqTerms t1 t2 =
+  do
+    s <- lift get
+    let (con,env) = replState s
+        p = eq (t1,con) (t2,con)
+    case run env p of
+        Right _ -> liftIO $ putStrLn "yes"
+        Left  e -> liftIO $ putStrLn e
+    
+
+inferTerm :: Term -> Repl ()
+inferTerm t =
+  do
+    s <- lift get
+    let (con,env) = replState s
+        p = infer (t,con) >>= prt
+    case run env p of
+        Right (m,_) -> liftIO $ putStrLn m
+        Left  e     -> liftIO $ putStrLn e
+
+-- | Run the interpreter as long as desired.
+repl :: Repl ()
+repl =
+  do
+    continue <- replStep
+    when continue repl
+
+-- * Helper functions
+
+trim :: String -> String
+trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace
+
+norm :: String -> String
+norm []          = []
+norm ('\\':c:xs) = c : norm xs
+norm (x:xs)      = x : norm xs
+