diff --git a/emacs-mode/eri.el b/emacs-mode/eri.el
new file mode 100644
--- /dev/null
+++ b/emacs-mode/eri.el
@@ -0,0 +1,186 @@
+;;; eri.el --- Enhanced relative indentation (eri)
+
+;;; Commentary:
+
+;;; Code:
+
+(require 'cl)
+
+(defun eri-current-line-length nil
+  "Calculates length of current line."
+  (- (line-end-position) (line-beginning-position)))
+
+(defun eri-current-line-empty nil
+  "Return non-nil if the current line is empty (not counting white space)."
+  (equal (current-indentation)
+         (eri-current-line-length)))
+
+(defun eri-maximum (xs)
+  "Calculate maximum element in XS.  Return nil if the list is empty."
+  (if xs (apply 'max xs)))
+
+(defun eri-take (n xs)
+  "Return the first N elements of XS."
+  (butlast xs (- (length xs) n)))
+
+(defun eri-split (x xs)
+  "Return a pair of lists (XS1 . XS2).
+If XS is sorted, then XS = (append XS1 XS2), and all elements in XS1 are <= X,
+whereas all elements in XS2 are > X."
+  (let* ((pos (or (position-if (lambda (y) (> y x)) xs) (length xs)))
+         (xs1 (eri-take pos xs))
+         (xs2 (nthcdr pos xs)))
+    `(,xs1 . ,xs2)))
+
+(defun eri-calculate-indentation-points-on-line (max)
+  "Calculate indentation points on current line.
+Only points left of column number MAX are included.
+If MAX is nil, then all points are included.  Return points in ascending order.
+
+Example (positions marked with ^ are returned):
+
+  f x y = g 3 (Just y) 5 4
+  ^ ^ ^ ^ ^ ^ ^     ^  |
+                       |
+                       MAX"
+  (let ((result))
+    (save-restriction
+      (beginning-of-line)
+      ; To make \\` work in the regexp below:
+      (narrow-to-region (line-beginning-position) (line-end-position))
+      (while
+          (progn
+            (let ((pos (and (search-forward-regexp
+                             "\\(?:\\s-\\|\\`\\)\\(\\S-\\)" nil t)
+                            (match-beginning 1))))
+              (when (not (null pos))
+                (let ((pos1 (- pos (line-beginning-position))))
+                  (when (or (null max) (< pos1 max))
+                    (add-to-list 'result pos1))))
+              (and pos
+                   (< (point) (line-end-position))
+                   (or (null max) (< (current-column) max))))))
+      (nreverse result) ; Destructive operation.
+      )))
+
+(defun eri-new-indentation-point ()
+  "Calculate a new indentation point, two steps in from the
+indentation of the first non-empty line above the current line.
+If there is no such line 2 is returned."
+  (save-excursion
+    (while
+        (progn
+          (forward-line -1)
+          (not (or (bobp)
+                   (not (eri-current-line-empty))))))
+    (+ 2 (current-indentation))))
+
+(defun eri-calculate-indentation-points (reverse)
+  "Calculate some indentation points.  Gives them in reverse order if
+REVERSE is non-nil.  See `eri-indent' for a description of how
+the indentation points are calculated."
+  ;; First find a bunch of indentations used above the current line.
+  (let ((points)
+        (max))
+    (save-excursion
+      (while
+          (progn
+            (forward-line -1)
+            ; Skip lines with only white space.
+            (unless (eri-current-line-empty)
+              (setq points
+                    (append
+                     (eri-calculate-indentation-points-on-line max)
+                     points))
+              (setq max (car points)))
+            ;; Stop after hitting the beginning of the buffer or a
+            ;; non-empty, non-indented line.
+            (not (or (bobp)
+                     (and (equal (current-indentation) 0)
+                          (> (eri-current-line-length) 0)))))))
+    ;; Add a new indentation point. Sort the indentations.
+    ;; Rearrange the points so that the next point is the one after the
+    ;; current one.
+    (let* ((ps (add-to-list 'points (eri-new-indentation-point)))
+           (ps1 (sort ps '<)) ; Note: sort is destructive.
+           (ps2 (eri-split (current-indentation)
+                           (remove (current-indentation) ps1))))
+      (if reverse
+          (append (nreverse (car ps2)) (nreverse (cdr ps2)))
+        (append (cdr ps2) (car ps2))))))
+
+(defun eri-indent (&optional reverse)
+  "Cycle between some possible indentation points.
+With prefix argument REVERSE, cycle in reverse order.
+
+Assume that a file contains the following lines of code, with point on
+the line with three dots:
+
+frob = loooooooooooooooooooooooooong identifier
+foo = f a b
+  where
+    f (Foo x) y = let bar = x
+                      baz = 3 + 5
+
+...
+
+^ ^ ^ ^    ^  ^ ^ ^   ^ * ^ ^ ^ ^
+
+Then the ^'s and the * mark the indentation points that this function
+cycles through.  The indentation points are selected as follows:
+
+  * All lines before the current one, up to and including the first
+    non-indented line (or the beginning of the buffer) are considered.
+
+      foo = f a b
+        where
+          f (Foo x) y = let bar = x
+                            baz = 3 + 5
+
+  * On these lines, erase all characters that stand to the right of
+    some non-white space character on a lower line.
+
+      foo
+        whe
+          f (Foo x) y = let b
+                            baz = 3 + 5
+
+  * Also erase all characters not immediately preceded by white
+    space.
+
+      f
+        w
+          f (    x  y = l   b
+                            b   = 3 + 5
+
+  * The columns of all remaining characters are indentation points.
+
+      f w f (    x  y = l   b   = 3 + 5
+      ^ ^ ^ ^    ^  ^ ^ ^   ^   ^ ^ ^ ^
+
+  * A new indentation point is also added, two steps in from the
+    indentation of the first non-empty line above the current line
+    (or in the second column, if there is no such line).
+
+      f w f (    x  y = l   b   = 3 + 5
+      ^ ^ ^ ^    ^  ^ ^ ^   ^ * ^ ^ ^ ^"
+  (interactive "P")
+  (let* ((points (eri-calculate-indentation-points reverse))
+         (remaining-points (cdr (member (current-indentation) points)))
+         (indentation (if remaining-points
+                          (car remaining-points)
+                        (car points))))
+    (when indentation
+      (save-excursion (indent-line-to indentation))
+      (if (< (current-column) indentation)
+          (indent-line-to indentation)))))
+
+(defun eri-indent-reverse nil
+  "Cycle between some possible indentation points (in reverse order).
+See `eri-indent' for a description of how the indentation points are
+calculated."
+  (interactive)
+  (eri-indent t))
+
+(provide 'eri)
+;;; eri.el ends here
diff --git a/emacs-mode/pisigma-input.el b/emacs-mode/pisigma-input.el
new file mode 100644
--- /dev/null
+++ b/emacs-mode/pisigma-input.el
@@ -0,0 +1,740 @@
+;;; pisigma-input.el --- The PiSigma input method
+
+;;; Commentary:
+
+;; A highly customisable input method which can inherit from other
+;; Quail input methods. By default the input method is geared towards
+;; the input of mathematical and other symbols in PiSigma programs.
+;;
+;; Use M-x customize-group pisigma-input to customise this input
+;; method.  Note that the functions defined under "Functions used to
+;; tweak translation pairs" below can be used to tweak both the key
+;; translations inherited from other input methods as well as the ones
+;; added specifically for this one.
+;;
+;; Use pisigma-input-show-translations to see all the characters which
+;; can be typed using this input method (except for those
+;; corresponding to ASCII characters).
+
+;;; Code:
+
+(require 'quail)
+(require 'cl)
+
+;; Quail is quite stateful, so be careful when editing this code.
+;; Note that with-temp-buffer is used below whenever buffer-local
+;; state is modified.
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Utility functions
+
+(defun pisigma-input-concat-map (f xs)
+  "Concat (map F XS)."
+  (apply 'append (mapcar f xs)))
+
+(defun pisigma-input-to-string-list (s)
+  "Convert a string S to a list of one-character strings, after
+removing all space and newline characters."
+  (pisigma-input-concat-map
+   (lambda (c) (if (member c (string-to-list " \n"))
+              nil
+            (list (string c))))
+   (string-to-list s)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Functions used to tweak translation pairs
+
+;; lexical-let is used since Elisp lacks lexical scoping.
+
+(defun pisigma-input-compose (f g)
+  "\x -> concatMap F (G x)"
+  (lexical-let ((f1 f) (g1 g))
+    (lambda (x) (pisigma-input-concat-map f1 (funcall g1 x)))))
+
+(defun pisigma-input-or (f g)
+  "\x -> F x ++ G x"
+  (lexical-let ((f1 f) (g1 g))
+    (lambda (x) (append (funcall f1 x) (funcall g1 x)))))
+
+(defun pisigma-input-nonempty ()
+  "Only keep pairs with a non-empty first component."
+  (lambda (x) (if (> (length (car x)) 0) (list x))))
+
+(defun pisigma-input-prepend (prefix)
+  "Prepend PREFIX to all key sequences."
+  (lexical-let ((prefix1 prefix))
+    (lambda (x) `((,(concat prefix1 (car x)) . ,(cdr x))))))
+
+(defun pisigma-input-prefix (prefix)
+  "Only keep pairs whose key sequence starts with PREFIX."
+  (lexical-let ((prefix1 prefix))
+    (lambda (x)
+      (if (equal (substring (car x) 0 (length prefix1)) prefix1)
+          (list x)))))
+
+(defun pisigma-input-suffix (suffix)
+  "Only keep pairs whose key sequence ends with SUFFIX."
+  (lexical-let ((suffix1 suffix))
+    (lambda (x)
+      (if (equal (substring (car x)
+                            (- (length (car x)) (length suffix1)))
+                 suffix1)
+          (list x)))))
+
+(defun pisigma-input-drop (ss)
+  "Drop pairs matching one of the given key sequences.
+SS should be a list of strings."
+  (lexical-let ((ss1 ss))
+    (lambda (x) (unless (member (car x) ss1) (list x)))))
+
+(defun pisigma-input-drop-beginning (n)
+  "Drop N characters from the beginning of each key sequence."
+  (lexical-let ((n1 n))
+    (lambda (x) `((,(substring (car x) n1) . ,(cdr x))))))
+
+(defun pisigma-input-drop-end (n)
+  "Drop N characters from the end of each key sequence."
+  (lexical-let ((n1 n))
+    (lambda (x)
+      `((,(substring (car x) 0 (- (length (car x)) n1)) .
+         ,(cdr x))))))
+
+(defun pisigma-input-drop-prefix (prefix)
+  "Only keep pairs whose key sequence starts with PREFIX.
+This prefix is dropped."
+  (pisigma-input-compose
+   (pisigma-input-drop-beginning (length prefix))
+   (pisigma-input-prefix prefix)))
+
+(defun pisigma-input-drop-suffix (suffix)
+  "Only keep pairs whose key sequence ends with SUFFIX.
+This suffix is dropped."
+  (lexical-let ((suffix1 suffix))
+    (pisigma-input-compose
+     (pisigma-input-drop-end (length suffix1))
+     (pisigma-input-suffix suffix1))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Customization
+
+;; The :set keyword is set to
+;; 'pisigma-input-incorporate-changed-setting so that the input method
+;; gets updated immediately when users customize it. However, the
+;; setup functions cannot be run before all variables have been
+;; defined. Hence the :initialize keyword is set to
+;; 'custom-initialize-default to ensure that the setup is not
+;; performed until pisigma-input-setup is called at the end of this
+;; file.
+
+(defgroup pisigma-input nil
+  "The PiSigma input method.
+After tweaking these settings you may want to inspect the
+resulting translations using `pisigma-input-show-translations'."
+  :group 'pisigma
+  :group 'leim)
+
+(defcustom pisigma-input-tweak-all
+  '(pisigma-input-compose
+    (pisigma-input-prepend "\\")
+    (pisigma-input-nonempty))
+  "An expression yielding a function which can be used to tweak
+all translations before they are included in the input method.
+The resulting function (if non-nil) is applied to every
+\(KEY-SEQUENCE . TRANSLATION) pair and should return a list of
+such pairs. (Note that the translations can be anything accepted
+by `quail-defrule'.)
+
+If you change this setting manually (without using the
+customization buffer) you need to call `pisigma-input-setup' in
+order for the change to take effect."
+  :group 'pisigma-input
+  :set 'pisigma-input-incorporate-changed-setting
+  :initialize 'custom-initialize-default
+  :type 'sexp)
+
+(defcustom pisigma-input-inherit
+  `(("TeX" . (pisigma-input-compose
+              (pisigma-input-drop '("geq" "leq" "bullet" "qed"))
+              (pisigma-input-or
+               (pisigma-input-drop-prefix "\\")
+               (pisigma-input-or
+                (pisigma-input-compose
+                 (pisigma-input-drop '("^o"))
+                 (pisigma-input-prefix "^"))
+                (pisigma-input-prefix "_")))))
+    )
+  "A list of Quail input methods whose translations should be
+inherited by the PiSigma input method (with the exception of
+translations corresponding to ASCII characters).
+
+The list consists of pairs (qp . tweak), where qp is the name of
+a Quail package, and tweak is an expression of the same kind as
+`pisigma-input-tweak-all' which is used to tweak the translation
+pairs of the input method.
+
+The inherited translation pairs are added last, after
+`pisigma-input-user-translations' and
+`pisigma-input-translations'.
+
+If you change this setting manually (without using the
+customization buffer) you need to call `pisigma-input-setup' in
+order for the change to take effect."
+  :group 'pisigma-input
+  :set 'pisigma-input-incorporate-changed-setting
+  :initialize 'custom-initialize-default
+  :type '(repeat (cons (string :tag "Quail package")
+                       (sexp :tag "Tweaking function"))))
+
+(defcustom pisigma-input-translations
+  (let ((max-lisp-eval-depth 2800)) `(
+
+  ;; Equality and similar symbols.
+
+  ("eq"  . ,(pisigma-input-to-string-list "=∼∽≈≋∻∾∿≀≃⋍≂≅ ≌≊≡≣≐≑≒≓≔≕≖≗≘≙≚≛≜≝≞≟≍≎≏≬⋕"))
+  ("eqn" . ,(pisigma-input-to-string-list "≠≁ ≉     ≄  ≇≆  ≢                 ≭    "))
+
+                    ("=n"  . ("≠"))
+  ("~"    . ("∼"))  ("~n"  . ("≁"))
+  ("~~"   . ("≈"))  ("~~n" . ("≉"))
+  ("~~~"  . ("≋"))
+  (":~"   . ("∻"))
+  ("~-"   . ("≃"))  ("~-n" . ("≄"))
+  ("-~"   . ("≂"))
+  ("~="   . ("≅"))  ("~=n" . ("≇"))
+  ("~~-"  . ("≊"))
+  ("=="   . ("≡"))  ("==n" . ("≢"))
+  ("==="  . ("≣"))
+  (".="   . ("≐"))  (".=." . ("≑"))
+  (":="   . ("≔"))  ("=:"  . ("≕"))
+  ("=o"   . ("≗"))
+  ("(="   . ("≘"))
+  ("and=" . ("≙"))  ("or=" . ("≚"))
+  ("*="   . ("≛"))
+  ("t="   . ("≜"))
+  ("def=" . ("≝"))
+  ("m="   . ("≞"))
+  ("?="   . ("≟"))
+
+  ;; Inequality and similar symbols.
+
+  ("leq"  . ,(pisigma-input-to-string-list "<≪⋘≤≦≲ ≶≺≼≾⊂⊆ ⋐⊏⊑ ⊰⊲⊴⋖⋚⋜⋞"))
+  ("leqn" . ,(pisigma-input-to-string-list "≮  ≰≨≴⋦≸⊀ ⋨⊄⊈⊊  ⋢⋤ ⋪⋬   ⋠"))
+  ("geq"  . ,(pisigma-input-to-string-list ">≫⋙≥≧≳ ≷≻≽≿⊃⊇ ⋑⊐⊒ ⊱⊳⊵⋗⋛⋝⋟"))
+  ("geqn" . ,(pisigma-input-to-string-list "≯  ≱≩≵⋧≹⊁ ⋩⊅⊉⊋  ⋣⋥ ⋫⋭   ⋡"))
+
+  ("<="   . ("≤"))  (">="   . ("≥"))
+  ("<=n"  . ("≰"))  (">=n"  . ("≱"))
+  ("len"  . ("≰"))  ("gen"  . ("≱"))
+  ("<n"   . ("≮"))  (">n"   . ("≯"))
+  ("<~"   . ("≲"))  (">~"   . ("≳"))
+  ("<~n"  . ("⋦"))  (">~n"  . ("⋧"))
+  ("<~nn" . ("≴"))  (">~nn" . ("≵"))
+
+  ("sub"   . ("⊂"))  ("sup"   . ("⊃"))
+  ("subn"  . ("⊄"))  ("supn"  . ("⊅"))
+  ("sub="  . ("⊆"))  ("sup="  . ("⊇"))
+  ("sub=n" . ("⊈"))  ("sup=n" . ("⊉"))
+
+  ("squb"   . ("⊏"))  ("squp"   . ("⊐"))
+  ("squb="  . ("⊑"))  ("squp="  . ("⊒"))
+  ("squb=n" . ("⋢"))  ("squp=n" . ("⋣"))
+
+  ;; Set membership etc.
+
+  ("member" . ,(pisigma-input-to-string-list "∈∉∊∋∌∍⋲⋳⋴⋵⋶⋷⋸⋹⋺⋻⋼⋽⋾⋿"))
+
+  ("inn" . ("∉"))
+  ("nin" . ("∌"))
+
+  ;; Intersections, unions etc.
+
+  ("intersection" . ,(pisigma-input-to-string-list "∩⋂∧⋀⋏⨇⊓⨅⋒∏ ⊼      ⨉"))
+  ("union"        . ,(pisigma-input-to-string-list "∪⋃∨⋁⋎⨈⊔⨆⋓∐⨿⊽⊻⊍⨃⊎⨄⊌∑⅀"))
+
+  ("and" . ("∧"))  ("or"  . ("∨"))
+  ("And" . ("⋀"))  ("Or"  . ("⋁"))
+  ("i"   . ("∩"))  ("un"  . ("∪"))  ("u+" . ("⊎"))  ("u." . ("⊍"))
+  ("I"   . ("⋂"))  ("Un"  . ("⋃"))  ("U+" . ("⨄"))  ("U." . ("⨃"))
+  ("glb" . ("⊓"))  ("lub" . ("⊔"))
+  ("Glb" . ("⨅"))  ("Lub" . ("⨆"))
+
+  ;; Entailment etc.
+
+  ("entails" . ,(pisigma-input-to-string-list "⊢⊣⊤⊥⊦⊧⊨⊩⊪⊫⊬⊭⊮⊯"))
+
+  ("|-"   . ("⊢"))  ("|-n"  . ("⊬"))
+  ("-|"   . ("⊣"))
+  ("|="   . ("⊨"))  ("|=n"  . ("⊭"))
+  ("||-"  . ("⊩"))  ("||-n" . ("⊮"))
+  ("||="  . ("⊫"))  ("||=n" . ("⊯"))
+  ("|||-" . ("⊪"))
+
+  ;; Divisibility, parallelity.
+
+  ("|"  . ("∣"))  ("|n"  . ("∤"))
+  ("||" . ("∥"))  ("||n" . ("∦"))
+
+  ;; Some symbols from logic and set theory.
+
+  ("all" . ("∀"))
+  ("ex"  . ("∃"))
+  ("exn" . ("∄"))
+  ("0"   . ("∅"))
+  ("C"   . ("∁"))
+
+  ;; Corners, ceilings and floors.
+
+  ("c"  . ,(pisigma-input-to-string-list "⌜⌝⌞⌟⌈⌉⌊⌋"))
+  ("cu" . ,(pisigma-input-to-string-list "⌜⌝  ⌈⌉  "))
+  ("cl" . ,(pisigma-input-to-string-list "  ⌞⌟  ⌊⌋"))
+
+  ("cul" . ("⌜"))  ("cuL" . ("⌈"))
+  ("cur" . ("⌝"))  ("cuR" . ("⌉"))
+  ("cll" . ("⌞"))  ("clL" . ("⌊"))
+  ("clr" . ("⌟"))  ("clR" . ("⌋"))
+
+  ;; Various operators/symbols.
+
+  ("qed"       . ("∎"))
+  ("x"         . ("×"))
+  ("o"         . ("∘"))
+  ("comp"      . ("∘"))
+  ("."         . ("∙"))
+  ("*"         . ("⋆"))
+  (".+"        . ("∔"))
+  (".-"        . ("∸"))
+  (":"         . ("∶"))
+  ("::"        . ("∷"))
+  ("::-"       . ("∺"))
+  ("-:"        . ("∹"))
+  ("+ "        . ("⊹"))
+  ("surd3"     . ("∛"))
+  ("surd4"     . ("∜"))
+  ("increment" . ("∆"))
+  ("inf"       . ("∞"))
+
+  ;; Circled operators.
+
+  ("o+"  . ("⊕"))
+  ("o--" . ("⊖"))
+  ("ox"  . ("⊗"))
+  ("o/"  . ("⊘"))
+  ("o."  . ("⊙"))
+  ("oo"  . ("⊚"))
+  ("o*"  . ("⊛"))
+  ("o="  . ("⊜"))
+  ("o-"  . ("⊝"))
+
+  ("O+"  . ("⨁"))
+  ("Ox"  . ("⨂"))
+  ("O."  . ("⨀"))
+  ("O*"  . ("⍟"))
+
+  ;; Boxed operators.
+
+  ("b+" . ("⊞"))
+  ("b-" . ("⊟"))
+  ("bx" . ("⊠"))
+  ("b." . ("⊡"))
+
+  ;; Various symbols.
+
+  ("integral" . ,(pisigma-input-to-string-list "∫∬∭∮∯∰∱∲∳"))
+  ("angle"    . ,(pisigma-input-to-string-list "∟∡∢⊾⊿"))
+  ("join"     . ,(pisigma-input-to-string-list "⋈⋉⋊⋋⋌⨝⟕⟖⟗"))
+
+  ;; Arrows.
+
+  ("l"  . ,(pisigma-input-to-string-list "←⇐⇚⇇⇆↤⇦↞↼↽⇠⇺↜⇽⟵⟸↚⇍⇷ ↹     ↢↩↫⇋⇜⇤⟻⟽⤆↶↺⟲                                    "))
+  ("r"  . ,(pisigma-input-to-string-list "→⇒⇛⇉⇄↦⇨↠⇀⇁⇢⇻↝⇾⟶⟹↛⇏⇸⇶ ↴    ↣↪↬⇌⇝⇥⟼⟾⤇↷↻⟳⇰⇴⟴⟿ ➵➸➙➔➛➜➝➞➟➠➡➢➣➤➧➨➩➪➫➬➭➮➯➱➲➳➺➻➼➽➾"))
+  ("u"  . ,(pisigma-input-to-string-list "↑⇑⟰⇈⇅↥⇧↟↿↾⇡⇞          ↰↱➦ ⇪⇫⇬⇭⇮⇯                                          "))
+  ("d"  . ,(pisigma-input-to-string-list "↓⇓⟱⇊⇵↧⇩↡⇃⇂⇣⇟         ↵↲↳➥ ↯                                               "))
+  ("ud" . ,(pisigma-input-to-string-list "↕⇕   ↨⇳                                                                   "))
+  ("lr" . ,(pisigma-input-to-string-list "↔⇔         ⇼↭⇿⟷⟺↮⇎⇹                                                       "))
+  ("ul" . ,(pisigma-input-to-string-list "↖⇖                        ⇱↸                                              "))
+  ("ur" . ,(pisigma-input-to-string-list "↗⇗                                         ➶➹➚                            "))
+  ("dr" . ,(pisigma-input-to-string-list "↘⇘                        ⇲                ➴➷➘                            "))
+  ("dl" . ,(pisigma-input-to-string-list "↙⇙                                                                        "))
+
+  ("l-"  . ("←"))  ("<-"  . ("←"))  ("l="  . ("⇐"))
+  ("r-"  . ("→"))  ("->"  . ("→"))  ("r="  . ("⇒"))  ("=>"  . ("⇒"))
+  ("u-"  . ("↑"))                   ("u="  . ("⇑"))
+  ("d-"  . ("↓"))                   ("d="  . ("⇓"))
+  ("ud-" . ("↕"))                   ("ud=" . ("⇕"))
+  ("lr-" . ("↔"))  ("<->" . ("↔"))  ("lr=" . ("⇔"))  ("<=>" . ("⇔"))
+  ("ul-" . ("↖"))                   ("ul=" . ("⇖"))
+  ("ur-" . ("↗"))                   ("ur=" . ("⇗"))
+  ("dr-" . ("↘"))                   ("dr=" . ("⇘"))
+  ("dl-" . ("↙"))                   ("dl=" . ("⇙"))
+
+  ("l==" . ("⇚"))  ("l-2" . ("⇇"))                   ("l-r-" . ("⇆"))
+  ("r==" . ("⇛"))  ("r-2" . ("⇉"))  ("r-3" . ("⇶"))  ("r-l-" . ("⇄"))
+  ("u==" . ("⟰"))  ("u-2" . ("⇈"))                   ("u-d-" . ("⇅"))
+  ("d==" . ("⟱"))  ("d-2" . ("⇊"))                   ("d-u-" . ("⇵"))
+
+  ("l--"  . ("⟵"))  ("<--"  . ("⟵"))  ("l~"  . ("↜" "⇜"))
+  ("r--"  . ("⟶"))  ("-->"  . ("⟶"))  ("r~"  . ("↝" "⇝" "⟿"))
+  ("lr--" . ("⟷"))  ("<-->" . ("⟷"))  ("lr~" . ("↭"))
+
+  ("l-n"  . ("↚"))  ("<-n"  . ("↚"))  ("l=n"  . ("⇍"))
+  ("r-n"  . ("↛"))  ("->n"  . ("↛"))  ("r=n"  . ("⇏"))  ("=>n"  . ("⇏"))
+  ("lr-n" . ("↮"))  ("<->n" . ("↮"))  ("lr=n" . ("⇎"))  ("<=>n" . ("⇎"))
+
+  ("l-|"  . ("↤"))  ("ll-" . ("↞"))
+  ("r-|"  . ("↦"))  ("rr-" . ("↠"))
+  ("u-|"  . ("↥"))  ("uu-" . ("↟"))
+  ("d-|"  . ("↧"))  ("dd-" . ("↡"))
+  ("ud-|" . ("↨"))
+
+  ("dz" . ("↯"))
+
+  ;; Ellipsis.
+
+  ("..." . ,(pisigma-input-to-string-list "⋯⋮⋰⋱"))
+
+  ;; Box-drawing characters.
+
+  ("---" . ,(pisigma-input-to-string-list "─│┌┐└┘├┤┬┼┴╴╵╶╷╭╮╯╰╱╲╳"))
+  ("--=" . ,(pisigma-input-to-string-list "═║╔╗╚╝╠╣╦╬╩     ╒╕╘╛╞╡╤╪╧ ╓╖╙╜╟╢╥╫╨"))
+  ("--_" . ,(pisigma-input-to-string-list "━┃┏┓┗┛┣┫┳╋┻╸╹╺╻
+                                        ┍┯┑┕┷┙┝┿┥┎┰┒┖┸┚┠╂┨┞╀┦┟╁┧┢╈┪┡╇┩
+                                        ┮┭┶┵┾┽┲┱┺┹╊╉╆╅╄╃ ╿╽╼╾"))
+  ("--." . ,(pisigma-input-to-string-list "╌╎┄┆┈┊
+                                        ╍╏┅┇┉┋"))
+
+  ;; Triangles.
+
+  ;; Big/small, black/white.
+
+  ("t" . ,(pisigma-input-to-string-list "◂◃◄◅▸▹►▻▴▵▾▿◢◿◣◺◤◸◥◹"))
+  ("T" . ,(pisigma-input-to-string-list "◀◁▶▷▲△▼▽◬◭◮"))
+
+  ("tb" . ,(pisigma-input-to-string-list "◂▸▴▾◄►◢◣◤◥"))
+  ("tw" . ,(pisigma-input-to-string-list "◃▹▵▿◅▻◿◺◸◹"))
+
+  ("Tb" . ,(pisigma-input-to-string-list "◀▶▲▼"))
+  ("Tw" . ,(pisigma-input-to-string-list "◁▷△▽"))
+
+  ;; Squares.
+
+  ("sq"  . ,(pisigma-input-to-string-list "■□◼◻◾◽▣▢▤▥▦▧▨▩◧◨◩◪◫◰◱◲◳"))
+  ("sqb" . ,(pisigma-input-to-string-list "■◼◾"))
+  ("sqw" . ,(pisigma-input-to-string-list "□◻◽"))
+  ("sq." . ("▣"))
+  ("sqo" . ("▢"))
+
+  ;; Rectangles.
+
+  ("re"  . ,(pisigma-input-to-string-list "▬▭▮▯"))
+  ("reb" . ,(pisigma-input-to-string-list "▬▮"))
+  ("rew" . ,(pisigma-input-to-string-list "▭▯"))
+
+  ;; Parallelograms.
+
+  ("pa"  . ,(pisigma-input-to-string-list "▰▱"))
+  ("pab" . ("▰"))
+  ("paw" . ("▱"))
+
+  ;; Diamonds.
+
+  ("di"  . ,(pisigma-input-to-string-list "◆◇◈"))
+  ("dib" . ("◆"))
+  ("diw" . ("◇"))
+  ("di." . ("◈"))
+
+  ;; Circles.
+
+  ("ci"   . ,(pisigma-input-to-string-list "●○◎◌◯◍◐◑◒◓◔◕◖◗◠◡◴◵◶◷⚆⚇⚈⚉"))
+  ("cib"  . ("●"))
+  ("ciw"  . ("○"))
+  ("ci."  . ("◎"))
+  ("ci.." . ("◌"))
+  ("ciO"  . ("◯"))
+
+  ;; Stars.
+
+  ("st"   . ,(pisigma-input-to-string-list "⋆✦✧✶✴✹ ★☆✪✫✯✰✵✷✸"))
+  ("st4"  . ,(pisigma-input-to-string-list "✦✧"))
+  ("st6"  . ("✶"))
+  ("st8"  . ("✴"))
+  ("st12" . ("✹"))
+
+  ;; Blackboard bold letters.
+
+  ("bn"   . ("ℕ"))
+  ("bz"   . ("ℤ"))
+  ("bq"   . ("ℚ"))
+  ("br"   . ("ℝ"))
+  ("bc"   . ("ℂ"))
+  ("bp"   . ("ℙ"))
+  ("bsum" . ("⅀"))
+
+  ;; Parentheses.
+
+  ("(" . ,(pisigma-input-to-string-list "([{⁅⁽₍〈⎴⟦⟨⟪〈《「『【〔〖〚︵︷︹︻︽︿﹁﹃﹙﹛﹝（［｛｢"))
+  (")" . ,(pisigma-input-to-string-list ")]}⁆⁾₎〉⎵⟧⟩⟫〉》」』】〕〗〛︶︸︺︼︾﹀﹂﹄﹚﹜﹞）］｝｣"))
+
+  ("[[" . ("⟦"))
+  ("]]" . ("⟧"))
+  ("<"  . ("⟨"))
+  (">"  . ("⟩"))
+  ("<<" . ("⟪"))
+  (">>" . ("⟫"))
+
+  ;; Primes.
+
+  ("'" . ,(pisigma-input-to-string-list "′″‴⁗"))
+  ("`" . ,(pisigma-input-to-string-list "‵‶‷"))
+
+  ;; Fractions.
+
+  ("frac" . ,(pisigma-input-to-string-list "¼½¾⅓⅔⅕⅖⅗⅘⅙⅚⅛⅜⅝⅞⅟"))
+
+  ;; Bullets.
+
+  ("bu"  . ,(pisigma-input-to-string-list "•◦‣⁌⁍"))
+  ("bub" . ("•"))
+  ("buw" . ("◦"))
+  ("but" . ("‣"))
+
+  ;; Musical symbols.
+
+  ("note" . ,(pisigma-input-to-string-list "♩♪♫♬"))
+  ("b"    . ("♭"))
+  ("#"    . ("♯"))
+
+  ;; Other punctuation and symbols.
+
+  ("\\"         . ("\\"))
+  ("en"         . ("–"))
+  ("em"         . ("—"))
+  ("^i"         . ("ⁱ"))
+  ("!!"         . ("‼"))
+  ("??"         . ("⁇"))
+  ("?!"         . ("‽" "⁈"))
+  ("!?"         . ("⁉"))
+  ("die"        . ,(pisigma-input-to-string-list "⚀⚁⚂⚃⚄⚅"))
+  ("asterisk"   . ,(pisigma-input-to-string-list "⁎⁑⁂✢✣✤✥✱✲✳✺✻✼✽❃❉❊❋"))
+  ("8<"         . ("✂" "✄"))
+  ("tie"        . ("⁀"))
+  ("undertie"   . ("‿"))
+  ("apl"        . ,(pisigma-input-to-string-list "⌶⌷⌸⌹⌺⌻⌼⌽⌾⌿⍀⍁⍂⍃⍄⍅⍆⍇⍈
+                                               ⍉⍊⍋⍌⍍⍎⍏⍐⍑⍒⍓⍔⍕⍖⍗⍘⍙⍚⍛
+                                               ⍜⍝⍞⍟⍠⍡⍢⍣⍤⍥⍦⍧⍨⍩⍪⍫⍬⍭⍮
+                                               ⍯⍰⍱⍲⍳⍴⍵⍶⍷⍸⍹⍺⎕"))
+
+  ;; Shorter forms of many greek letters plus ƛ.
+
+  ("Ga"  . ("α"))  ("GA"  . ("Α"))
+  ("Gb"  . ("β"))  ("GB"  . ("Β"))
+  ("Gg"  . ("γ"))  ("GG"  . ("Γ"))
+  ("Gd"  . ("δ"))  ("GD"  . ("Δ"))
+  ("Ge"  . ("ε"))  ("GE"  . ("Ε"))
+  ("Gz"  . ("ζ"))  ("GZ"  . ("Ζ"))
+  ;; \eta \Eta
+  ("Gth" . ("θ"))  ("GTH" . ("θ"))
+  ("Gi"  . ("ι"))  ("GI"  . ("Ι"))
+  ("Gk"  . ("κ"))  ("GK"  . ("Κ"))
+  ("Gl"  . ("λ"))  ("GL"  . ("Λ"))  ("Gl-" . ("ƛ"))
+  ("Gm"  . ("μ"))  ("GM"  . ("Μ"))
+  ("Gn"  . ("ν"))  ("GN"  . ("Ν"))
+  ("Gx"  . ("ξ"))  ("GX"  . ("Ξ"))
+  ;; \omicron \Omicron
+  ;; \pi \Pi
+  ("Gr"  . ("ρ"))  ("GR"  . ("Ρ"))
+  ("Gs"  . ("σ"))  ("GS"  . ("Σ"))
+  ("Gt"  . ("τ"))  ("GT"  . ("Τ"))
+  ("Gu"  . ("υ"))  ("GU"  . ("Υ"))
+  ("Gf"  . ("φ"))  ("GF"  . ("Φ"))
+  ("Gc"  . ("χ"))  ("GC"  . ("Χ"))
+  ("Gp"  . ("ψ"))  ("GP"  . ("Ψ"))
+  ("Go"  . ("ω"))  ("GO"  . ("Ω"))
+
+  ;; Some ISO8859-1 characters.
+
+  (" "         . (" "))
+  ("!"         . ("¡"))
+  ("cent"      . ("¢"))
+  ("brokenbar" . ("¦"))
+  ("degree"    . ("°"))
+  ("?"         . ("¿"))
+  ("^a_"       . ("ª"))
+  ("^o_"       . ("º"))
+
+  ;; Circled, parenthesised etc. numbers and letters.
+
+  ( "(0)" . ,(pisigma-input-to-string-list " ⓪"))
+  ( "(1)" . ,(pisigma-input-to-string-list "⑴①⒈❶➀➊"))
+  ( "(2)" . ,(pisigma-input-to-string-list "⑵②⒉❷➁➋"))
+  ( "(3)" . ,(pisigma-input-to-string-list "⑶③⒊❸➂➌"))
+  ( "(4)" . ,(pisigma-input-to-string-list "⑷④⒋❹➃➍"))
+  ( "(5)" . ,(pisigma-input-to-string-list "⑸⑤⒌❺➄➎"))
+  ( "(6)" . ,(pisigma-input-to-string-list "⑹⑥⒍❻➅➏"))
+  ( "(7)" . ,(pisigma-input-to-string-list "⑺⑦⒎❼➆➐"))
+  ( "(8)" . ,(pisigma-input-to-string-list "⑻⑧⒏❽➇➑"))
+  ( "(9)" . ,(pisigma-input-to-string-list "⑼⑨⒐❾➈➒"))
+  ("(10)" . ,(pisigma-input-to-string-list "⑽⑩⒑❿➉➓"))
+  ("(11)" . ,(pisigma-input-to-string-list "⑾⑪⒒"))
+  ("(12)" . ,(pisigma-input-to-string-list "⑿⑫⒓"))
+  ("(13)" . ,(pisigma-input-to-string-list "⒀⑬⒔"))
+  ("(14)" . ,(pisigma-input-to-string-list "⒁⑭⒕"))
+  ("(15)" . ,(pisigma-input-to-string-list "⒂⑮⒖"))
+  ("(16)" . ,(pisigma-input-to-string-list "⒃⑯⒗"))
+  ("(17)" . ,(pisigma-input-to-string-list "⒄⑰⒘"))
+  ("(18)" . ,(pisigma-input-to-string-list "⒅⑱⒙"))
+  ("(19)" . ,(pisigma-input-to-string-list "⒆⑲⒚"))
+  ("(20)" . ,(pisigma-input-to-string-list "⒇⑳⒛"))
+
+  ("(a)"  . ,(pisigma-input-to-string-list "⒜Ⓐⓐ"))
+  ("(b)"  . ,(pisigma-input-to-string-list "⒝Ⓑⓑ"))
+  ("(c)"  . ,(pisigma-input-to-string-list "⒞Ⓒⓒ"))
+  ("(d)"  . ,(pisigma-input-to-string-list "⒟Ⓓⓓ"))
+  ("(e)"  . ,(pisigma-input-to-string-list "⒠Ⓔⓔ"))
+  ("(f)"  . ,(pisigma-input-to-string-list "⒡Ⓕⓕ"))
+  ("(g)"  . ,(pisigma-input-to-string-list "⒢Ⓖⓖ"))
+  ("(h)"  . ,(pisigma-input-to-string-list "⒣Ⓗⓗ"))
+  ("(i)"  . ,(pisigma-input-to-string-list "⒤Ⓘⓘ"))
+  ("(j)"  . ,(pisigma-input-to-string-list "⒥Ⓙⓙ"))
+  ("(k)"  . ,(pisigma-input-to-string-list "⒦Ⓚⓚ"))
+  ("(l)"  . ,(pisigma-input-to-string-list "⒧Ⓛⓛ"))
+  ("(m)"  . ,(pisigma-input-to-string-list "⒨Ⓜⓜ"))
+  ("(n)"  . ,(pisigma-input-to-string-list "⒩Ⓝⓝ"))
+  ("(o)"  . ,(pisigma-input-to-string-list "⒪Ⓞⓞ"))
+  ("(p)"  . ,(pisigma-input-to-string-list "⒫Ⓟⓟ"))
+  ("(q)"  . ,(pisigma-input-to-string-list "⒬Ⓠⓠ"))
+  ("(r)"  . ,(pisigma-input-to-string-list "⒭Ⓡⓡ"))
+  ("(s)"  . ,(pisigma-input-to-string-list "⒮Ⓢⓢ"))
+  ("(t)"  . ,(pisigma-input-to-string-list "⒯Ⓣⓣ"))
+  ("(u)"  . ,(pisigma-input-to-string-list "⒰Ⓤⓤ"))
+  ("(v)"  . ,(pisigma-input-to-string-list "⒱Ⓥⓥ"))
+  ("(w)"  . ,(pisigma-input-to-string-list "⒲Ⓦⓦ"))
+  ("(x)"  . ,(pisigma-input-to-string-list "⒳Ⓧⓧ"))
+  ("(y)"  . ,(pisigma-input-to-string-list "⒴Ⓨⓨ"))
+  ("(z)"  . ,(pisigma-input-to-string-list "⒵Ⓩⓩ"))
+
+  ))
+  "A list of translations specific to the PiSigma input method.
+Each element is a pair (KEY-SEQUENCE-STRING . LIST-OF-TRANSLATION-STRINGS).
+All the translation strings are possible translations
+of the given key sequence; if there is more than one you can choose
+between them using the arrow keys.
+
+Note that if you customize this setting you will not
+automatically benefit (or suffer) from modifications to its
+default value when the library is updated.  If you just want to
+add some bindings it is probably a better idea to customize
+`pisigma-input-user-translations'.
+
+These translation pairs are included after those in
+`pisigma-input-user-translations', but before the ones inherited
+from other input methods (see `pisigma-input-inherit').
+
+If you change this setting manually (without using the
+customization buffer) you need to call `pisigma-input-setup' in
+order for the change to take effect."
+  :group 'pisigma-input
+  :set 'pisigma-input-incorporate-changed-setting
+  :initialize 'custom-initialize-default
+  :type '(repeat (cons (string :tag "Key sequence")
+                       (repeat :tag "Translations" string))))
+
+(defcustom pisigma-input-user-translations nil
+  "Like `pisigma-input-translations', but more suitable for user
+customizations since by default it is empty.
+
+These translation pairs are included first, before those in
+`pisigma-input-translations' and the ones inherited from other input
+methods."
+  :group 'pisigma-input
+  :set 'pisigma-input-incorporate-changed-setting
+  :initialize 'custom-initialize-default
+  :type '(repeat (cons (string :tag "Key sequence")
+                       (repeat :tag "Translations" string))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Inspecting and modifying translation maps
+
+(defun pisigma-input-get-translations (qp)
+  "Return a list containing all translations from the Quail
+package QP (except for those corresponding to ASCII).
+Each pair in the list has the form (KEY-SEQUENCE . TRANSLATION)."
+  (with-temp-buffer
+    (activate-input-method qp) ; To make sure that the package is loaded.
+    (unless (quail-package qp)
+      (error "%s is not a Quail package." qp))
+    (let ((decode-map (list 'decode-map)))
+      (quail-build-decode-map (list (quail-map)) "" decode-map 0)
+      (cdr decode-map))))
+
+(defun pisigma-input-show-translations (qp)
+  "Display all translations used by the Quail package QP (a string).
+\(Except for those corresponding to ASCII)."
+  (interactive (list (read-input-method-name
+                      "Quail input method (default %s): " "PiSigma")))
+  (let ((buf (concat "*" qp " input method translations*")))
+    (with-output-to-temp-buffer buf
+      (with-current-buffer buf
+        (quail-insert-decode-map
+         (cons 'decode-map (pisigma-input-get-translations qp)))))))
+
+(defun pisigma-input-add-translations (trans)
+  "Add the given translations TRANS to the PiSigma input method.
+TRANS is a list of pairs (KEY-SEQUENCE . TRANSLATION). The
+translations are appended to the current translations."
+  (with-temp-buffer
+    (dolist (tr (pisigma-input-concat-map (eval pisigma-input-tweak-all) trans))
+      (quail-defrule (car tr) (cdr tr) "PiSigma" t))))
+
+(defun pisigma-input-inherit-package (qp &optional fun)
+  "Let the PiSigma input method inherit the translations from the
+Quail package QP (except for those corresponding to ASCII).
+
+The optional function FUN can be used to modify the translations.
+It is given a pair (KEY-SEQUENCE . TRANSLATION) and should return
+a list of such pairs."
+  (let ((trans (pisigma-input-get-translations qp)))
+    (pisigma-input-add-translations
+     (if fun (pisigma-input-concat-map fun trans)
+       trans))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Setting up the input method
+
+(defun pisigma-input-setup ()
+  "Set up the PiSigma input method based on the customisable
+variables and underlying input methods."
+
+  ;; Create (or reset) the input method.
+  (with-temp-buffer
+    (quail-define-package "PiSigma" "UTF-8" "∏Σ" t ; guidance
+     "PiSigma input method.
+The purpose of this input method is to edit PiSigma programs, but
+since it is highly customisable it can be made useful for other
+tasks as well."
+     nil nil nil nil nil nil t ; maximum-shortest
+     ))
+
+  (pisigma-input-add-translations
+   (mapcar (lambda (tr) (cons (car tr) (vconcat (cdr tr))))
+           (append pisigma-input-user-translations
+                   pisigma-input-translations)))
+  (dolist (def pisigma-input-inherit)
+    (pisigma-input-inherit-package (car def)
+                                (eval (cdr def)))))
+
+(defun pisigma-input-incorporate-changed-setting (sym val)
+  "Update the PiSigma input method based on the customisable
+variables and underlying input methods.  Suitable for use in
+the :set field of `defcustom'."
+  (set-default sym val)
+  (pisigma-input-setup))
+
+;; Set up the input method.
+
+(pisigma-input-setup)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Administrative details
+
+(provide 'pisigma-input)
+;;; pisigma-input.el ends here
diff --git a/emacs-mode/pisigma-mode.el b/emacs-mode/pisigma-mode.el
new file mode 100644
--- /dev/null
+++ b/emacs-mode/pisigma-mode.el
@@ -0,0 +1,140 @@
+;;; pisigma-mode.el --- PiSigma major mode
+
+;; Author: DarinMorrison
+;; Keywords: extensions
+
+;; Copyright (c) 2009, Darin Morrison
+;; 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 COPYRIGHT HOLDERS AND CONTRIBUTORS
+;; "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
+;; COPYRIGHT HOLDER 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.
+
+;;; Commentary:
+;; 
+
+;;; History:
+;; 
+
+;;; Code:
+
+(require 'eri)
+(require 'pisigma-input)
+
+;; Associate .pi files with pisigma-mode
+(add-to-list 'auto-mode-alist '("\\.pi\\'" . pisigma-mode))
+(modify-coding-system-alist 'file "\\.pi$" 'utf-8)
+
+(defgroup pisigma nil
+  "Major mode for editing PiSigma programs."
+  :group 'languages)
+
+(defcustom pisigma-mode-hook nil
+  "Hook run after entering PiSigma mode."
+  :type  'hook
+  :group 'pisigma)
+
+(defvar pisigma-mode-map
+  (let ((keymap (make-sparse-keymap)))
+    keymap)
+  "Keymap for `pisigma-mode'.")
+
+(defvar pisigma-mode-syntax-table
+  (let ((syntax-table (make-syntax-table)))
+    (modify-syntax-entry ?\  " "      syntax-table)
+    (modify-syntax-entry ?\t " "      syntax-table)
+    (modify-syntax-entry ?\' "\'"     syntax-table)
+    (modify-syntax-entry ?_  "w"      syntax-table)
+    (modify-syntax-entry ?\( "()"     syntax-table)
+    (modify-syntax-entry ?\) ")("     syntax-table)
+    (modify-syntax-entry ?\[ "(]"     syntax-table)
+    (modify-syntax-entry ?\] ")["     syntax-table)
+    (modify-syntax-entry ?{  "(}1n"   syntax-table)
+    (modify-syntax-entry ?}  "){4n"   syntax-table)
+    (modify-syntax-entry ?-  "w 123b" syntax-table)
+    (modify-syntax-entry ?\n "> b"    syntax-table)
+    syntax-table)
+  "Syntax table for `pisigma-mode'.")
+
+;; TODO: 1. matcher functions for type signatures and variables.
+;;       2. multiline font-lock for case?
+(defvar pisigma-font-lock-keywords
+  '(("^\\(:l\\)\\s-*\\([^ \t\n]+\\)"
+     (1 font-lock-preprocessor-face)
+     (2 font-lock-constant-face))
+    ("^\\([[:alpha:]][[:alnum:]_']*\\)[[:space:]]*:"
+     (1 font-lock-function-name-face))
+    ("^\\([[:alpha:]][[:alnum:]_']*\\)[[:space:]]*="
+     (1 font-lock-function-name-face))
+    ("\\<Type\\>" . font-lock-type-face)
+    ("\\<\\(case\\|in\\|let\\|of\\|split\\|with\\)\\>" . font-lock-keyword-face)
+    ("\\[\\|\\]\\|♯\\|!\\|♭\\|\\^\\|∞" . font-lock-warning-face)
+    ("\\('\\)\\([[:alpha:]][[:alnum:]_']*\\)"
+     (1 font-lock-warning-face)
+     (2 font-lock-constant-face)))
+  "Keyword highlighting specification for `pisigma-mode'.")
+
+(defvar pisigma-imenu-generic-expression
+  nil)
+
+(defvar pisigma-outline-regexp
+  nil)
+
+;;; Indentation
+
+(defun pisigma-indent-line ()
+  "This is what happens when TAB is pressed."
+  (interactive)
+  (eri-indent))
+
+(defun agda2-indent-line-reverse ()
+  "This is what happens when S-TAB is pressed."
+  (interactive)
+  (eri-indent-reverse))
+
+;;;###autoload
+(define-derived-mode pisigma-mode fundamental-mode "PiSigma"
+  "A major mode for editing PiSigma files."
+  :syntax-table pisigma-mode-syntax-table
+  (set (make-local-variable 'comment-start) "-- ")
+  (set (make-local-variable 'comment-start-skip) "[-{]-[ \t]*")
+  (set (make-local-variable 'comment-end) "")
+  (set (make-local-variable 'comment-end-skip) "[ \t]*\\(-}\\|\\s>\\)")
+  (set (make-local-variable 'font-lock-defaults) '(pisigma-font-lock-keywords))
+  (set (make-local-variable 'indent-line-function) 'pisigma-indent-line)
+  (set (make-local-variable 'imenu-generic-expression) pisigma-imenu-generic-expression)
+  (set (make-local-variable 'outline-regexp) pisigma-outline-regexp)
+  (set (make-local-variable 'parse-sexp-ignore-comments) t)
+  ;; Protect global value of default-input-method from set-input-method.
+  (make-local-variable 'default-input-method)
+  (set (make-local-variable 'ident-tabs-mode) nil)
+  (set (make-local-variable 'tab-width) 8)
+  (set-input-method "PiSigma"))
+
+(provide 'pisigma-mode)
+;;; pisigma-mode.el ends here
diff --git a/examples/Broken.pi b/examples/Broken.pi
new file mode 100644
--- /dev/null
+++ b/examples/Broken.pi
@@ -0,0 +1,9 @@
+Bool : Type;
+Bool = { true false };
+
+broken : Bool -> Bool;
+broken = \ b -> case b of {
+                 true  -> 'true
+               | true  -> 'true
+               | false -> 'true };
+
diff --git a/examples/Curry.pi b/examples/Curry.pi
new file mode 100644
--- /dev/null
+++ b/examples/Curry.pi
@@ -0,0 +1,13 @@
+⊥ : Type;
+⊥ = {};
+
+-- Curry's paradox (usually ruled out by positivity check).
+
+A : Type;
+A = [A] → ⊥;
+
+¬A : A → ⊥;
+¬A = λ x → x x;
+
+contradiction : ⊥;
+contradiction = ¬A (λ x → ¬A x);
diff --git a/examples/Data.pi b/examples/Data.pi
deleted file mode 100644
--- a/examples/Data.pi
+++ /dev/null
@@ -1,107 +0,0 @@
-: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/EqProb.pi b/examples/EqProb.pi
deleted file mode 100644
--- a/examples/EqProb.pi
+++ /dev/null
@@ -1,39 +0,0 @@
-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
--- a/examples/Equal.pi
+++ b/examples/Equal.pi
@@ -52,3 +52,63 @@
 t6 : Eq A (id a) a;
 t6 = refl A a;
 
+c:A;
+
+t7 : Eq (A*(^A)) (let x:A=a in (a,[x])) (a,let x:A=a in [x])
+   = refl (A*(^A)) (let x:A=a in (a,[x]));
+
+
+t8 : Eq (A*(^A)) (let x:A=a in (a,[x])) (a,let x:A=a in [x])
+   = refl (A*(^A)) (let x:A=a in (a,[x]));
+
+{-
+t8a : Eq (^A) (let x:A=a in [x]) (let x:A=c in [x])
+   = refl (^A) (let x:A=c in [x]);
+-}
+
+t9 : Eq (^(A * A)) (let x:A=a; y:A=c in [(x,y)]) (let y:A=c; x:A=a in [(x,y)])
+   = refl (^(A * A)) (let x:A=a; y:A=c in [(x,y)]);
+
+t9a : Eq (^(A * A)) (let x:A=a; y:A=c in [(x,y)]) (let y:A=c; x:A=a in [(x,y)])
+   = refl (^(A * A)) (let x:A=a; y:A=c in [(x,y)]);
+
+t10 : Eq (^A) (let x:A=a in [x]) (let x:A=a;y:A=x in [y])
+    = refl (^A) (let x:A=a in [x]);
+{- according due to the draft rules (Friday 30/10/09) should not work. -}
+
+t11 : Eq (^(^A)) [let x:A=a in [x]] [let x:A=a;y:A=x in [y]]
+    = refl (^(^A)) [let x:A=a in [x]];
+{- works, uses bet equality in contexts. -}
+
+t11a : Eq (^(^A)) [let x:A=a in [x]] [let y:A=a in [y]]
+    = refl (^(^A)) [let x:A=a in [x]]; 
+{- works now -}
+
+t12 : Eq (^A) (let y:A=y in [y]) (let z:A=z in [z])
+    = refl (^A)  (let y:A=y in [y]);
+
+{-
+t13 : Eq (^A) [let x:A=a in x] [a]
+    = refl (^A) [a];
+{- doesn't work and shouldn't. -}
+-}
+
+Stream : Type;
+Stream = A * [∞ Stream];
+
+as : Stream;
+as = (a, [as]);
+
+repeat : (x : A) → Stream;
+repeat = λ x → (x, [repeat x]);
+
+-- as is equal to its unfolding.
+
+unfolds : Eq Stream as (a, [as]);
+unfolds = refl Stream as;
+
+-- repeat a is not equal to its unfolding.
+{-
+doesNotUnfold : Eq Stream (repeat a) (a, [repeat a]);
+doesNotUnfold = refl Stream (repeat a);
+-}
diff --git a/examples/Foo.pi b/examples/Foo.pi
new file mode 100644
--- /dev/null
+++ b/examples/Foo.pi
@@ -0,0 +1,1 @@
+Nat
diff --git a/examples/Hurkens.pi b/examples/Hurkens.pi
new file mode 100644
--- /dev/null
+++ b/examples/Hurkens.pi
@@ -0,0 +1,42 @@
+-- Hurkens' Paradox, a simplification of Girard's Paradox
+
+-- (translated from Agda examples)
+
+⊥ : Type;
+⊥ = (α : Type) → α;
+
+¬ : Type → Type;
+¬ = λ α → α → ⊥;
+
+P : Type → Type;
+P = λ α → α → Type;
+
+U : Type;
+U = (χ : Type) → (P (P χ) → χ) → P (P χ);
+
+τ : P (P U) → U;
+τ = λ t χ f p → t (λ x → p (f (x χ f)));
+
+σ : U → P (P U);
+σ = λ s → s U (λ t → τ t);
+
+Δ : P U;
+Δ = λ y → ¬ ((p : P U) → σ y p → p (τ (σ y)));
+
+Ω : U;
+Ω = τ (λ p → (x : U) → σ x p → p x);
+
+D : Type;
+D = (p : P U) → σ Ω p → p (τ (σ Ω));
+
+lem1 : (p : P U) → ((x : U) → σ x p → p x) → p Ω;
+lem1 = λ p H1 → H1 Ω (λ x → H1 (τ (σ x)));
+
+lem2 : ¬ D;
+lem2 = lem1 Δ (λ x H2 H3 → H3 Δ H2 (λ p → H3 (λ y → p (τ (σ y)))));
+
+lem3 : D;
+lem3 = λ p → lem1 (λ y → p (τ (σ y)));
+
+loop : ⊥;
+loop = lem2 lem3;
diff --git a/examples/Parser.pi b/examples/Parser.pi
new file mode 100644
--- /dev/null
+++ b/examples/Parser.pi
@@ -0,0 +1,89 @@
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
+Nat : type;
diff --git a/examples/Parser2.pi b/examples/Parser2.pi
new file mode 100644
--- /dev/null
+++ b/examples/Parser2.pi
@@ -0,0 +1,331 @@
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
+Nat;
diff --git a/examples/Parser3.pi b/examples/Parser3.pi
new file mode 100644
--- /dev/null
+++ b/examples/Parser3.pi
@@ -0,0 +1,331 @@
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
+Nat
diff --git a/examples/SubjectReduction.pi b/examples/SubjectReduction.pi
new file mode 100644
--- /dev/null
+++ b/examples/SubjectReduction.pi
@@ -0,0 +1,58 @@
+-- Context:
+--   Recursion with boxes
+--   Thorsten Altenkirch
+--   http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=104
+
+Stream : Type;
+Stream = [∞ Stream];
+
+ticks : Stream;
+ticks = [ticks];
+
+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;
+
+unfold : Eq Stream ticks [ticks];
+unfold = refl Stream ticks;
+
+-- We can prove this variant of congruence for boxes:
+
+cong : (xs ys : Stream) → Eq Stream xs ys →
+       Eq Stream [let zs : Stream = xs in zs]
+                 [let zs : Stream = ys in zs];
+cong = λ xs ys eq P p → eq (λ zs → P [let us : Stream = zs in us]) p;
+
+-- This does not (obviously) break subject reduction, because the
+-- following property can be proved using refl:
+
+unfoldInContext : Eq Stream [let xs : Stream =  ticks  in xs]
+                            [let xs : Stream = [ticks] in xs];
+unfoldInContext = cong ticks [ticks] unfold;
+unfoldInContext = refl Stream [let xs : Stream = ticks in xs];
+
+-- Note also that unlimited unfolding is not possible (using refl):
+
+-- unfoldTwiceInContext : Eq Stream [let xs : Stream =   ticks   in xs]
+--                                  [let xs : Stream = [[ticks]] in xs];
+-- unfoldTwiceInContext = refl Stream [let xs : Stream = ticks in xs];
+
+-- However, we can move lets through boxes, so the idea from
+-- Thorsten's blog post needs to be qualified.
+
+letThroughBox : (xs : Stream) →
+                Eq Stream [let ys : Stream = xs in  ys]
+                          (let ys : Stream = xs in [ys]);
+letThroughBox = λ xs → refl Stream [let ys : Stream = xs in ys];
+
+letThrough2Boxes : (xs : Stream) →
+                   Eq Stream [[let ys : Stream = xs in  ys]]
+                             (let ys : Stream = xs in [[ys]]);
+letThrough2Boxes = λ xs → refl Stream [[let ys : Stream = xs in ys]];
+
+anotherExample : (A : Type) → (x : A) →
+                 Eq (∞ (∞ A)) [let y : A = x in [y]]
+                              (let y : A = x in [[let z : A = y in z]]);
+anotherExample = λ A x → refl (∞ (∞ A)) (let y : A = x in [[y]]);
diff --git a/examples/Universe.pi b/examples/Universe.pi
deleted file mode 100644
--- a/examples/Universe.pi
+++ /dev/null
@@ -1,47 +0,0 @@
-: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/stl.pi b/examples/stl.pi
--- a/examples/stl.pi
+++ b/examples/stl.pi
@@ -129,3 +129,17 @@
 lam : (g:Con) -> (a:Ty) -> (b:Ty)
       -> Lam (ext g a) b -> Lam g (arr a b);
 lam = \ g a b t -> ('lam,t);
+
+{- 
+
+Ren : Con -> Con -> Type
+Subst : Con -> Con -> Type
+
+Subst Γ Δ = {A : Ty} → Var Γ A → Tm Δ A
+
+subst : (Γ Δ : Con) → ({A : Ty} → Var Γ A → Tm Δ A) → {A : Ty} → Tm Δ A → Tm Γ A
+ren: (Γ Δ : Con) → Subst Γ Δ → {A : Ty} → Tm Δ A → Tm Γ A
+
+monad laws...
+
+-}
diff --git a/pisigma.cabal b/pisigma.cabal
--- a/pisigma.cabal
+++ b/pisigma.cabal
@@ -1,11 +1,15 @@
 cabal-version: >= 1.6
 name:          pisigma
-version:       0.1.0.2
+version:       0.1.0.3
 license:       BSD3
 license-file:  LICENSE
 data-files:    examples/*.pi
+               emacs-mode/*.el
 author:        Thorsten Altenkirch <txa@cs.nott.ac.uk>,
-               Andres Loeh <kspisigma@andres-loeh.de>
+               Andres Loeh <kspisigma@andres-loeh.de>,
+               Nils Anders Danielsson <nad@cs.nott.ac.uk>,
+               Nicolas Oury <Nicolas.Oury@ed.ac.uk>,
+               Darin Morrison <dwm@cs.nott.ac.uk>
 maintainer:    Thorsten Altenkirch <txa@cs.nott.ac.uk>,
                Andres Loeh <kspisigma@andres-loeh.de>
 description:   dependently typed core language
@@ -13,19 +17,50 @@
 category:      Development, Language, Dependent Types
 build-type:    Simple
 
+library
+  build-depends:    array           >= 0.2   && < 0.3,
+                    base            >= 4.0   && < 5.0,
+                    bytestring      >= 0.9   && < 1.0,
+                    haskeline       >= 0.6   && < 0.7,
+                    haskeline-class >= 0.6.1 && < 0.7,
+                    mpppc           >= 0.1.0 && < 0.2,
+                    mtl             >= 1.1   && < 1.2,
+                    parsec          >= 3.0   && < 4.0,
+                    text            >= 0.5   && < 0.6,
+                    utf8-string     >= 0.3.5 && < 0.4
+
+  exposed-modules:  Language.PiSigma.Check
+                    Language.PiSigma.Equality
+                    Language.PiSigma.Evaluate
+                    Language.PiSigma.Normalise
+                    Language.PiSigma.Lexer
+                    Language.PiSigma.Parser
+                    Language.PiSigma.Pretty
+                    Language.PiSigma.Syntax
+                    Language.PiSigma.Util.String.Internal
+                    Language.PiSigma.Util.String.Parser
+
+  ghc-options:      -funbox-strict-fields
+
+  hs-source-dirs:   src
+
+
+
 executable pisigma
-  main-is:       PiSigma.hs
-  other-modules: PiSigma.Check
-                 PiSigma.Equality
-                 PiSigma.Evaluation
-                 PiSigma.Nf
-                 PiSigma.Parser
-                 PiSigma.Print
-                 PiSigma.Syntax
-  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
+  ghc-options:      -funbox-strict-fields
+
+  hs-source-dirs:   src
+
+  main-is:          Tools/Interpreter/Main.hs
+
+  other-modules:    Language.PiSigma.Check
+                    Language.PiSigma.Equality
+                    Language.PiSigma.Evaluate
+                    Language.PiSigma.Normalise
+                    Language.PiSigma.Lexer
+                    Language.PiSigma.Parser
+                    Language.PiSigma.Pretty
+                    Language.PiSigma.Syntax
+                    Language.PiSigma.Util.String.Internal
+                    Language.PiSigma.Util.String.Parser
+                    Tools.Interpreter.REPL
diff --git a/src/Language/PiSigma/Check.hs b/src/Language/PiSigma/Check.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/PiSigma/Check.hs
@@ -0,0 +1,261 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Language.PiSigma.Check
+  ( checkProg
+  , infer )
+  where
+
+import Control.Arrow
+  ( first )
+import Control.Monad.Error
+import qualified Data.List
+  as List
+
+import Language.PiSigma.Equality
+import Language.PiSigma.Evaluate
+import Language.PiSigma.Pretty
+import Language.PiSigma.Syntax
+import qualified Language.PiSigma.Util.String.Internal
+  as Internal
+
+--import Debug.Trace
+--trace "check\n" $
+
+-- closures are the other way around
+-- should be fixed by changing closures.
+
+{-
+fog :: CTerm -> Closure
+fog (g,t) = (con2scope g,t)
+-}
+
+throwErrorc :: (Print b, GetLoc b, Env e) => b -> Pretty -> Eval e a
+throwErrorc t m =
+  do
+    pt <- evalPrint t
+    throwError $ fromPretty $
+             text (Seq $ Internal.fromString $ locMessage $ getLoc t)
+         <$> "Expression:   " <+> align pt
+         <$> m
+
+expected :: (Env e) => Clos Term -> Val -> Pretty -> Eval e ()
+expected t expected' inferred = do
+  pExpected <- evalPrint expected'
+  throwErrorc t $ "Expected type:" <+> align pExpected <$> parens inferred
+
+expectedButFound :: (GetLoc a, Print a, Print b, Print c, Env e)
+                 => a
+                 -> b
+                 -> c
+                 -> Internal.String
+                 -> Eval e d
+expectedButFound t expected' found inferred =
+  do
+    pExpected <- evalPrint expected'
+    pFound    <- evalPrint found
+    throwErrorc t $
+          "Inferred type:" <+> align pFound
+      <$> "Expected type:" <+> align pExpected
+      <$> parens (text . Seq $ inferred)
+
+duplicateLabels :: (GetLoc a, Print a, Env e) => a -> Eval e d
+duplicateLabels t =
+  throwErrorc t $ "Duplicate labels in enum type"
+
+nonLinearSplit :: (GetLoc a, Print a, Env e) => a -> Eval e d
+nonLinearSplit t =
+  throwErrorc t $ "Repeated variables in a split"
+
+-- | Takes a term and an (unevaluated) type. We first
+-- handle the cases that may potentially change the
+-- environment. If none of those cases match, we can
+-- safely evaluate the type and call check'.
+check :: Env e => Clos Term -> Clos Type -> Eval e ()
+--check (g,t) c | trace ("check\ng ="++(show g)++"\n t="++(show t)++"\nc="++(show c)++"\n") False = undefined
+
+check (Let _ p t,g) c = 
+    do g' <- checkProg (p,g)
+       check (t,g') c
+
+check (Split _ t (x,(y,u)),g) c | x==y = nonLinearSplit t
+check (Split _ t (x,(y,u)),g) c | otherwise =
+    do sigab <- infer' (t,g)
+       case sigab of
+         (VQ Sigma ((a,(z,b)),s)) -> 
+             do t'      <- eval (t,g)
+                (_,g')  <- tdecl x g (a,s) 
+                b'      <- subst (z,(b,s)) (Var Unknown x, g')
+                (_,g'') <- tdecl y g' b'
+                case t' of
+                  (Ne (NVar i)) ->
+                      letn' i (Pair Unknown (Var Unknown x) (Var Unknown y), g'')
+                                (check (u,g'') c)
+                      -- this is a bit silly since we know the ids.
+                  _ -> check (u,g'') c
+                      -- instead of failing, we just omit the assignment.
+         _ -> expectedButFound (t,g) msg1 sigab msg2
+                where
+                  msg1 = "sigma type" :: Internal.String
+                  msg2 = "split"      :: Internal.String
+
+check gt @ (Case _ t lus,g) c = 
+    do enum <- infer' (t,g)
+       case enum of
+         VEnum ls -> 
+             let ls' = map fst lus
+             in if ls /= ls'
+                then -- pt' <- evalPrint t'
+                  throwErrorc gt $ text $ Seq $
+                    Internal.concat [ "Labels don't match."
+                                    , "\nProvided labels: ", Internal.fromString $ show ls
+                                    , "\nExpected labels: ", Internal.fromString $ show ls'
+                                    , "\n(Case)\n"
+                                    ]
+                -- set equivalence would be sufficent
+                else do t' <- eval (t,g)
+                        case t' of
+                          -- if the scrutinee is a variable, we add a constraint
+                          -- while checking each of the branches
+                          (Ne (NVar i)) ->
+                               mapM_ (\ (l,u) -> 
+                                      letn' i (label l)
+                                            (check (u,g) c)) lus
+                          -- if the scrutinee is not a variable, we do not add
+                          -- a constraint, but continue
+                          _ -> mapM_ (\ (_,u) -> check (u,g) c) lus
+         _ -> expectedButFound (t,g) msg1 enum msg2
+                where
+                  msg1 = "enum type" :: Internal.String
+                  msg2 = "case"      :: Internal.String
+                  
+
+         {- Problem: here and other places: we try to print the term t which isn't yet 
+            typechecked and may contain undefined variables which may crash the printer...
+            see undef-bug.pi
+         -}
+check (Force _ t,g) (a , s) =
+    check (t,g) (Lift Unknown a , s)
+
+check t a = check' t =<< feval a
+
+check' :: Env e => Clos Term -> Val -> Eval e ()
+-- we ignore boxes in types, this is the other part of the lifting story.
+check' gt (VBox (Boxed a)) = check gt a  
+check' (Lam _ (x,t),g) (VQ Pi ((a,(y,b)),s)) =
+    do (i,g') <- tdecl x g (a,s)
+       let s' = extendScope s y (i,Nothing)
+       check (t,g') (b,s')
+check' gt @ (Lam _ _,_) a =
+    expected gt a "Lam"
+check' (Pair _ t u,g) (VQ Sigma ((a,(y,b)),s)) =
+    do check (t,g) (a,s)
+       b' <- subst (y,(b,s)) (t,g)
+       check (u,g) b'
+check' gt @ (Pair _ _ _, _) a =
+    expected gt a "Pair"
+-- Labels cannot be inferred because there is no way to know
+-- what the other labels are.
+check' (Label _ l,_) (VEnum ls) | l `elem` ls = return ()
+check' gt @ (Label _ _,_) a =
+    expected gt a "Label"
+-- To check that [sigma] is a type, it's sufficient to know
+-- that sigma is a type. The alternative would seem to be to
+-- assume that ^Type == Type, but that does not work.
+check' (Box _ a,g) VType = 
+    check (a,g) ty
+check' (Box _ t,g) (VLift a) =
+    check (t,g) a
+check' gt @ (Box _ _,_) a =
+    expected gt a "Box"
+check' t a =
+    do b <- infer' t
+       catchE (eq a b) $ const $ expectedButFound t a b "check"
+
+inferVar :: Env e => Loc -> Clos Name -> Eval e (Clos Type)
+inferVar l (x,g) =
+    case lookupCon g x of
+      Just a  -> return a
+      Nothing -> throwError msg
+        where
+          msg = Internal.concat [ Internal.fromString $ locMessage l
+                                , "\nUndefined variable: "
+                                , x
+                                , "\n(inferVar)\n"
+                                ]
+
+infer :: Env e => Clos Term -> Eval e (Clos Type)
+--infer (g,t) | trace ("infer\ng ="++(show g)++"\n t="++(show t)++"\n") False = undefined
+
+infer (Var l x,g) = inferVar l (x,g)
+
+infer (Let _ tel t,g) = 
+    do g' <- checkProg (tel,g)
+       infer (t,g')  
+
+infer (Type _,_) = return ty
+
+infer (Q _ _ (a,(x,b)),g) = 
+    do check (a,g) ty
+       (_,g') <- tdecl x g (a,g)
+       check (b,g') ty
+       return ty
+
+infer (App t u,g) = 
+    do piab <- infer' (t,g)
+       case piab of 
+         (VQ Pi ((a,(x,b)),s)) -> do check (u,g) (a,s)
+                                     subst (x,(b,s)) (u,g)
+         _ -> expectedButFound (t,g) msg1 piab msg2
+                where
+                  msg1 = "pi type" :: Internal.String
+                  msg2 = "App"     :: Internal.String
+
+infer (t@(Enum _ ls),_) =
+    if List.length (List.nub ls) < List.length ls
+      then duplicateLabels t
+      else return ty
+
+infer (Box  _ t,g) = liftM (first $ Lift Unknown) (infer (t,g))
+
+-- TODO: either use infer', or explain why forced eval
+-- cannot be used here.
+infer (Force _ t,g) =
+    do a  <- infer (t,g)
+       a' <- eval a
+       case a' of
+         VLift b -> return b
+         _       -> expectedButFound (t,g) msg1 a' msg2
+                      where
+                        msg1 = "lifted type" :: Internal.String
+                        msg2 = "Force"       :: Internal.String
+
+infer (Lift _ a,g) =
+    do check (a,g) ty
+       return ty
+
+-- infer (LType _ a,g) =
+--     do check (a,g) lty
+--        return ty
+
+
+infer gt = throwErrorc gt $ "Not inferable" <$> "(infer)"
+
+
+-- | Infers a type and evaluates it.
+infer' :: Env e => Clos Term -> Eval e Val
+infer' gt = feval =<< infer gt
+
+checkProg :: Env e => Clos Prog -> Eval e Scope
+checkProg ([],g) = return g
+checkProg ((Decl _ x a):tel,g) = 
+    do check (a,g) ty 
+       (_,g') <- decl x PrtInfo{ name = x, expand = False } g (Just (a,g))
+       checkProg (tel,g')
+checkProg ((Defn l x t):tel,g) =
+    do a <- inferVar l (x,g)
+       check (t,g) a
+       i <- getId l x g
+       defn' i (t,g)
+       checkProg (tel,g)
+       
+                             
diff --git a/src/Language/PiSigma/Equality.hs b/src/Language/PiSigma/Equality.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/PiSigma/Equality.hs
@@ -0,0 +1,129 @@
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+module Language.PiSigma.Equality
+  ( eq )
+  where
+
+import Control.Monad
+
+import Language.PiSigma.Evaluate
+import Language.PiSigma.Syntax
+
+class Equal a where
+    eq :: Env e => a -> a -> Eval e ()
+
+instance Equal (Clos Term) where
+    eq t u = do t' <- eval t
+                u' <- eval u
+                eq t' u'
+
+-- unused?
+-- eq' :: Env e => Clos (Term,Term) -> Eval e ()
+-- eq' ((t,u),s) = eq (t,s) (u,s)
+
+eqBind :: (Env e,Closure a) =>
+          (a -> a -> Eval e ()) ->
+          Bind a -> Bind a -> Eval e ()
+eqBind eqArg (x0,c0) (x1,c1) =
+  do let s0 = getScope c0
+         s1 = getScope c1
+     (i,s0') <- decl' x0 s0
+     let s1' = extendScope s1 x1 (i,Nothing)
+     let c0' = putScope c0 s0'
+         c1' = putScope c1 s1'
+     eqArg c0' c1'
+
+instance (Equal a,Closure a) => Equal (Bind a) where
+    eq = eqBind eq
+
+instance Equal Val where
+    eq (Ne t0) (Ne t1) = eq t0 t1
+    eq (VQ ps0 ((a0,(x0,b0)),s0)) (VQ ps1 ((a1,(x1,b1)),s1))
+      | ps0 == ps1 = 
+        do eq (a0,s0) (a1,s1)
+           eq (x0,(b0,s0)) (x1,(b1,s1))
+    eq (VLam xt0) (VLam xt1) = eq xt0 xt1
+    eq (VPair ((t0,u0),s0)) (VPair ((t1,u1),s1)) = 
+        do eq (t0,s0) (t1,s1)
+           eq (u0,s0) (u1,s1)
+    eq (VBox b) (VBox b') = eq b b' 
+    eq (VLift a) (VLift a') = eq a a'
+--    eq (VLType a) (VLType a') = eq a a'
+    eq v0 v1 | v0 == v1 = return () -- Type, Label, Enum
+             | otherwise = fail "Different values"
+
+{- eqBox implements alpha equality -}
+eqBox :: Env e => Clos Term -> Clos Term -> Eval e ()
+--eqBox c c' | c == c' = return ()
+eqBox (Var l x,s) (Var l' y,s') = 
+    do x' <- getId l  x s
+       y' <- getId l' y s'
+       eq x' y'
+eqBox (Let _ p t,s) c = 
+    do s' <- evalProg (p,s)
+       eqBox (t,s') c
+eqBox c c'@(Let _ _ _,_) = eqBox c' c 
+eqBox (Q _ ps (a,(x,b)),s) (Q _ ps' (a',(x',b')),s')
+      | ps == ps' = 
+          do eqBox (a,s) (a',s')
+             eq (x,Boxed (b,s)) (x',Boxed (b',s'))
+eqBox (Lam _ (x,t),s) (Lam _ (x',t'),s') =
+      eq (x,Boxed (t,s)) (x',Boxed (t',s'))
+eqBox (App t u,s) (App t' u',s') =
+    do eqBox (t,s) (t',s')
+       eqBox (u,s) (u',s')
+eqBox (Pair _ t u,s) (Pair _ t' u',s') =
+    do eqBox (t,s) (t',s')
+       eqBox (u,s) (u',s')
+eqBox (Split _ t (x,(y,u)),s) (Split _ t' (x',(y',u')),s') =
+    do eqBox (t,s) (t',s')
+       eq (x,(y,Boxed (u,s))) (x',(y',Boxed (u',s')))
+eqBox (Case _ t bs,s) (Case _ t' bs',s') =
+    do eqBox (t,s) (t',s')
+       zipWithM_ (\ (l,t'') (l',t''') -> 
+                      if l==l' then eqBox (t'',s) (t''',s')
+                      else fail "eqBox case") bs bs'
+eqBox (Lift _ t,s)  (Lift _ t',s')  = eqBox (t,s) (t',s')
+-- eqBox (LType _ t,s)  (LType _ t',s')  = eqBox (t,s) (t',s')
+eqBox (Box _ t,s)   (Box _ t',s')   = eqBox (t,s) (t',s')
+eqBox (Force _ t,s) (Force _ t',s') = eqBox (t,s) (t',s')               
+eqBox (t,_) (t',_) | t == t'   = return () -- Type, Label, Enum
+                    | otherwise = fail "Different terms"
+    
+instance Equal Boxed where
+    eq (Boxed c) (Boxed c') = eqBox c c'
+
+instance Equal Id where
+    eq i0 i1  
+        | i0 == i1  = return ()
+        | otherwise = do ei0 <- lookupId i0
+                         ei1 <- lookupId i1
+                         case (ei0,ei1) of
+                           (Id j0, Id j1) -> unless (j0 == j1)
+                                               (fail "Different variables")
+                           (Closure t0, Closure t1) ->
+                               letn i0 (Id i0)
+                                    (letn i1 (Id i0)
+                                          (eq t0 t1))
+                           _ -> fail "Variable vs neutral"
+
+instance Equal Ne where
+    eq (NVar i0) (NVar i1) = eq i0 i1
+    eq (t0 :.. u0) (t1 :.. u1) = 
+        do eq t0 t1
+           eq u0 u1
+    eq (NSplit t0 xyu0) (NSplit t1 xyu1) =
+        do eq t0 t1
+           eq xyu0 xyu1
+    eq (NCase t0 (lus0,s0)) (NCase t1 (lus1,s1)) =
+        do eq t0 t1
+           let eqBranches []             []             = return ()
+               eqBranches ((l0,u0):lus0') ((l1,u1):lus1')
+                   | l0 == l1                           = do
+                      eq (u0,s0) (u1,s1)
+                      eqBranches lus0' lus1'
+               eqBranches _ _ = fail "Case: branches differ"
+           eqBranches lus0 lus1
+    eq (NForce t) (NForce t') = eq t t'
+    eq t u = fail ("Different neutrals:\n"++ show t ++"\n/=\n"++ show u ++"\n")
diff --git a/src/Language/PiSigma/Evaluate.hs b/src/Language/PiSigma/Evaluate.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/PiSigma/Evaluate.hs
@@ -0,0 +1,190 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE OverloadedStrings          #-}
+{-# LANGUAGE TypeSynonymInstances       #-}
+
+module Language.PiSigma.Evaluate
+  ( Eval (..)
+  , catchE
+  , decl
+  , decl'
+  , defn'
+  , eval
+  , evalProg
+  , feval
+  , getEnv
+  , getId
+  , letn
+  , letn'
+  , lookupId
+  , run
+  , subst
+  , tdecl )
+  where
+
+import Control.Monad.Error
+import Control.Monad.State
+import Control.Monad.Identity
+
+import Language.PiSigma.Syntax
+import qualified Language.PiSigma.Util.String.Internal
+  as Internal
+
+-- * Monad used for evaluation
+
+type EvalErr = Internal.String
+
+instance Error EvalErr where
+
+
+newtype Eval e a = Eval { unEval :: StateT e (ErrorT EvalErr Identity) a }
+  deriving ( Monad
+           , MonadError EvalErr
+           , MonadState e )
+
+run :: e -> Eval e a -> Either EvalErr (a, e)
+run e (Eval p) = runIdentity $ runErrorT $ runStateT p e 
+
+catchE :: Eval e a -> (EvalErr -> Eval e a) -> Eval e a
+catchE = catchError
+
+getEnv :: Eval e e
+getEnv = get
+
+setEnv :: e -> Eval e ()
+setEnv = put
+
+getId :: Loc -> Name -> Scope -> Eval e Id
+getId l x s = case lookupScope s x of 
+  Just i  -> return i
+  Nothing -> throwError msg
+    where
+      msg = Internal.concat [ Internal.fromString $ locMessage l
+                            , "\nUndefined variable: "
+                            , x
+                            , "\n"
+                            ]
+
+-- | Takes a name, a scope, and potentially a type.
+-- It extends the environment and the scope with that name.
+decl :: Env e
+     => Name
+     -> PrtInfo
+     -> Scope
+     -> Maybe  (Clos Type)
+     -> Eval e (Id, Scope)
+decl x x' s a =
+    do e <- getEnv
+       let (i,e') = extE e x'
+       setEnv e'
+       return (i,extendScope s x (i,a))
+
+decl' :: Env e => Name -> Scope -> Eval e (Id, Scope)
+decl' x s   = decl x PrtInfo{ name = x, expand = True } s Nothing
+
+tdecl :: Env e => Name -> Scope -> (Clos Type) -> Eval e (Id, Scope)
+tdecl x g = decl x PrtInfo{ name = x, expand = True } g . Just
+
+-- | Updates the environment.
+defn :: Env e => Id -> EnvEntry -> Eval e ()
+defn i ei =
+    do e <- getEnv
+       setEnv (setE e i ei)
+
+defn' :: Env e => Id -> Clos Type -> Eval e ()
+defn' i = defn i . Closure
+
+-- | Locally updates the environment.
+letn :: Env e => Id -> EnvEntry -> Eval e a -> Eval e a
+letn i ei p =
+    do eo <- lookupId i
+       defn i ei
+       a  <- p
+       defn i eo
+       return a
+
+letn' :: Env e => Id -> Clos Type -> Eval e a -> Eval e a
+letn' i = letn i . Closure
+
+subst :: Env e => Bind (Clos Term) -> (Clos Term) -> Eval e (Clos Term)
+subst (x,(t,s)) u =
+    do (i,s') <- decl' x s
+       defn' i u    
+       return (t,s')
+
+evalApp :: Env e => Val -> (Clos Term) -> Eval e Val
+evalApp (VLam xt) u = eval =<< subst xt u
+evalApp (Ne t)    u = return (Ne (t :.. u))
+evalApp _         _ = throwError "function expected"
+
+lookupId :: Env e => Id -> Eval e EnvEntry
+lookupId i = liftM (flip getE i) getEnv
+
+evalId :: Env e => Id -> Eval e Val
+evalId i =
+    do ei <- lookupId i
+       case ei of
+         Closure t -> eval t
+         Id j      -> return (Ne (NVar j))
+
+-- use subst!
+evalSplit :: Env e
+          => Val
+          -> Bind (Bind (Clos Term))
+          -> Eval e Val
+evalSplit (VPair ((l,r),s)) (x,(y,(t,s'))) = 
+    do (x',s2) <- decl' x s'
+       (y',s3) <- decl' y s2
+       defn' x' (l,s)
+       defn' y' (r,s)
+       eval (t,s3)
+
+evalSplit (Ne n) (xy,t) = return (Ne (NSplit n (xy,t)))
+evalSplit _ _ = throwError "Pair expected"
+
+evalCase :: Env e => Val -> Clos [(Label,Term)] -> Eval e Val
+evalCase (VLabel l) (lts,s) = 
+    case lookup l lts of
+      Nothing -> throwError "case not matched"
+      Just t  -> eval (t,s)
+evalCase (Ne n) lts = return (Ne (NCase n lts))
+evalCase _ _ = throwError "Label expected"
+
+force :: Env e => Val -> Eval e Val
+force (VBox (Boxed c)) = eval c
+force (Ne n) = return (Ne (NForce n))
+force _ = throwError "Box expected"
+
+eval :: Env e => (Clos Term) -> Eval e Val
+eval (Var l x, s)               = evalId =<< getId l x s
+eval (Let _ g t, s)             = curry eval t =<< evalProg (g,s)
+eval (Type _, _)                = return VType
+eval (Q _ ps axb, s)            = return (VQ ps (axb,s))
+eval (Lift _ t, s)              = return (VLift (t,s))
+--eval (LType _ t, s)   = return (VLType (t,s))
+eval (Lam _ (x,t), s)           = return (VLam (x,(t,s)))
+eval (App t u, s)               = flip evalApp (u,s) =<< eval (t,s)
+eval (Pair _ t u, s)            = return (VPair ((t,u),s))
+eval (Split _ t (x, (y, u)), s) = flip evalSplit (x,(y,(u,s))) =<< eval (t,s)
+eval (Enum _ ls, _)             = return (VEnum ls)
+eval (Label _ l, _)             = return (VLabel l)
+eval (Case _ t lts, s)          = flip evalCase (lts,s) =<< eval (t,s)
+eval (Box _ t, s)               = return (VBox (Boxed (t,s)))
+eval (Force _ t, s)             = force =<< eval (t,s)
+
+
+-- forced eval (should be integrated into eval?)
+feval :: Env e => (Clos Term) -> Eval e Val
+feval t = do t' <- eval t
+             case t' of 
+               VBox (Boxed u) -> feval u
+               v -> return v
+
+               
+
+evalProg :: Env e => Clos Prog -> Eval e Scope
+evalProg ([],s) = return s
+evalProg ((Decl _ x _):tel, s) = do (_,s') <- decl x (PrtInfo x False) s Nothing
+                                    evalProg (tel,s')
+evalProg ((Defn l x t):tel, s) = do i <- getId l x s
+                                    defn' i (t,s)
+                                    evalProg (tel,s)
diff --git a/src/Language/PiSigma/Lexer.hs b/src/Language/PiSigma/Lexer.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/PiSigma/Lexer.hs
@@ -0,0 +1,278 @@
+{-# OPTIONS_GHC -fno-warn-orphans     #-}
+{-# LANGUAGE    FlexibleInstances     #-}
+{-# LANGUAGE    MultiParamTypeClasses #-}
+{-# LANGUAGE    TypeSynonymInstances  #-}
+
+module Language.PiSigma.Lexer
+  ( Parser
+  , angles
+  , braces
+  , brackets
+  , charLiteral
+  , colon
+  , comma
+  , commaSep
+  , commaSep1
+  , decimal
+  , dot
+  , float
+  , hexadecimal
+  , identifier
+  , integer
+  , locate
+  , location
+  , locReserved
+  , locReservedOp
+  , locSymbol
+  , lexeme
+  , natural
+  , naturalOrFloat
+  , octal
+  , operator
+  , parens
+  , reserved
+  , reservedOp
+  , semi
+  , semiSep
+  , semiSep1
+  , squares
+  , stringLiteral
+  , symbol
+  , tokArr
+  , tokForce
+  , tokLam
+  , tokLift
+  , whiteSpace )
+  where
+
+import Control.Applicative
+import Control.Monad.Identity
+import Data.Char
+import Text.Parsec.Prim
+  ( Parsec
+  , Stream (..)
+  , (<?>)
+  , getPosition
+  )
+import qualified Text.Parsec.Token
+  as Token
+import Text.ParserCombinators.Parsec
+  ( SourcePos
+  , choice
+  , sourceColumn
+  , sourceLine
+  , sourceName )
+import Text.ParserCombinators.Parsec.Char
+
+import Language.PiSigma.Syntax
+  ( Loc (..) )
+import qualified Language.PiSigma.Util.String.Parser
+  as Parser
+
+instance (Monad m) => Stream Parser.String m Char where
+  uncons = return . Parser.uncons
+
+type Parser = Parsec Parser.String ()
+
+nonIdentStr :: String
+nonIdentStr = [ '('
+              , ')'
+              , '['
+              , ']'
+              , '{'
+              , '}' ]
+
+opLetterStr :: String
+opLetterStr = [ '!'
+              , '*'
+              , ','
+              , '-'
+              , ':'
+              , ';'
+              , '='
+              , '>'
+              , '\\'
+              , '^'
+              , '|'
+              , '♭'
+              , '♯'
+              , 'λ'
+              , '→'
+              , '∞' ]
+
+-- * The lexical definition of PiSigma.  Used to make token parsers.
+pisigmaDef :: (Monad m) => Token.GenLanguageDef Parser.String u m
+pisigmaDef = Token.LanguageDef
+  { Token.commentStart    = "{-"
+  , Token.commentEnd      = "-}"
+  , Token.commentLine     = "--"
+  , Token.nestedComments  = True
+  , Token.identStart      = satisfy $ \ c -> not (isSpace   c)
+                                          && not (c `elem` nonIdentStr)
+                                          && not (c `elem` opLetterStr)
+                                          && not (isControl c)
+                                          && not (isDigit   c)
+  , Token.identLetter     = satisfy $ \ c -> not (isSpace   c)
+                                          && not (c `elem` nonIdentStr)
+                                          && not (c `elem` opLetterStr)
+                                          && not (isControl c)
+  , Token.opStart         = oneOf ""
+  , Token.opLetter        = oneOf opLetterStr
+  , Token.reservedNames   = [ "Type"
+                            , "case"
+                            , "in"
+                            , "let"
+                            , "of"
+                            , "split"
+                            , "with" ]
+  , Token.reservedOpNames = [ "!"
+                            , "*"
+                            , ","
+                            , "->"
+                            , ":"
+                            , ";"
+                            , "="   
+                            , "\\"
+                            , "^"
+                            , "|"
+                            , "♭"
+                            , "♯"
+                            , "λ"
+                            , "→"
+                            , "∞" ]
+  , Token.caseSensitive   = True
+  }
+
+-- * The PiSigma token parser, generated from the lexical definition.
+
+tokenParser :: Token.GenTokenParser Parser.String () Identity
+tokenParser =  Token.makeTokenParser pisigmaDef
+
+-- * PiSigma parser combinators.
+
+angles           ::  Parser a -> Parser a
+angles            =  Token.angles         tokenParser
+
+braces           ::  Parser a -> Parser a
+braces            =  Token.braces         tokenParser
+
+brackets         ::  Parser a -> Parser a
+brackets          =  Token.brackets       tokenParser
+
+charLiteral      ::  Parser Char
+charLiteral       =  Token.charLiteral    tokenParser
+
+colon            ::  Parser String
+colon             =  Token.colon          tokenParser
+
+comma            ::  Parser String
+comma             =  Token.comma          tokenParser
+
+commaSep         ::  Parser a -> Parser [a]
+commaSep          =  Token.commaSep       tokenParser
+
+commaSep1        ::  Parser a -> Parser [a]
+commaSep1         =  Token.commaSep1      tokenParser
+
+decimal          ::  Parser Integer
+decimal           =  Token.decimal        tokenParser
+
+dot              ::  Parser String
+dot               =  Token.dot            tokenParser
+
+float            ::  Parser Double
+float             =  Token.float          tokenParser
+
+hexadecimal      ::  Parser Integer
+hexadecimal       =  Token.hexadecimal    tokenParser
+
+identifier       ::  Parser String
+identifier        =  Token.identifier     tokenParser
+
+integer          ::  Parser Integer
+integer           =  Token.integer        tokenParser
+
+lexeme           ::  Parser a -> Parser a
+lexeme            =  Token.lexeme         tokenParser
+
+natural          ::  Parser Integer
+natural           =  Token.natural        tokenParser
+
+naturalOrFloat   ::  Parser (Either Integer Double)
+naturalOrFloat    =  Token.naturalOrFloat tokenParser
+
+octal            ::  Parser Integer
+octal             =  Token.octal          tokenParser
+
+operator         ::  Parser String
+operator          =  Token.operator       tokenParser
+
+parens           ::  Parser a -> Parser a
+parens            =  Token.parens         tokenParser
+
+reserved         ::  String -> Parser ()
+reserved          =  Token.reserved       tokenParser
+
+reservedOp       ::  String -> Parser ()
+reservedOp        =  Token.reservedOp     tokenParser
+
+semi             ::  Parser String
+semi              =  Token.semi           tokenParser
+
+semiSep          ::  Parser a -> Parser [a]
+semiSep           =  Token.semiSep        tokenParser
+
+semiSep1         ::  Parser a -> Parser [a]
+semiSep1          =  Token.semiSep1       tokenParser
+
+squares          ::  Parser a -> Parser a
+squares           =  Token.squares        tokenParser
+
+stringLiteral    ::  Parser String
+stringLiteral     =  Token.stringLiteral  tokenParser
+
+symbol           ::  String -> Parser String
+symbol            =  Token.symbol         tokenParser
+
+whiteSpace       ::  Parser ()
+whiteSpace        =  Token.whiteSpace     tokenParser
+
+-- * Derived parser combinators
+
+location         :: Parser Loc
+location          = sourcePosToLoc <$> getPosition
+
+locate           :: Parser a -> Parser Loc
+locate            = (location <*)
+
+sourcePosToLoc   :: SourcePos -> Loc
+sourcePosToLoc p  = Loc (sourceName p) (sourceLine p) (sourceColumn p)
+
+locReserved      :: String -> Parser Loc
+locReserved       = locate . reserved
+
+locReservedOp    :: String -> Parser Loc
+locReservedOp     = locate . reservedOp
+
+locSymbol        :: String -> Parser Loc
+locSymbol xs      = locate (symbol xs) <?> show xs
+
+tokArr           :: Parser Loc
+tokArr            = locate (choice [ reservedOp "->"
+                                   , reservedOp "→"
+                                   ] <?> "->")
+
+tokForce         :: Parser Loc
+tokForce          = locate (choice [ reservedOp "!"
+                                   , reservedOp "♭"
+                                   ] <?> "!")
+
+tokLam           :: Parser Loc
+tokLam            = locate (choice [ reservedOp "\\"
+                                   , reservedOp "λ"
+                                   ] <?> "\\")
+
+tokLift          :: Parser Loc
+tokLift           = locate (choice [ reservedOp "^"
+                                   , reservedOp "∞"
+                                   ] <?> "^")
diff --git a/src/Language/PiSigma/Normalise.hs b/src/Language/PiSigma/Normalise.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/PiSigma/Normalise.hs
@@ -0,0 +1,123 @@
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE OverloadedStrings      #-}
+{-# LANGUAGE TypeSynonymInstances   #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+module Language.PiSigma.Normalise
+  ( quote
+  , nf )
+  where
+
+import Control.Monad
+
+import Language.PiSigma.Evaluate
+import Language.PiSigma.Syntax
+import qualified Language.PiSigma.Util.String.Internal
+  as Internal
+
+{- Implementation of a normalisation function.
+   Useful for testing.
+-}
+
+type Vars = [Name]
+
+fresh :: Name -> Vars -> Name
+fresh x xs
+  | x /= "" && x `elem` xs = (x `Internal.append` "'") `fresh` xs
+  | otherwise              = x
+
+class Nf a b | a -> b where
+    nf :: Env e => Vars -> a -> Eval e b
+    nf = nf' True
+    quote :: Env e => Vars -> a -> Eval e b
+    quote = nf' False
+    nf' :: Env e => Bool -> Vars -> a -> Eval e b
+
+
+instance Nf (Clos Term) Term where
+    nf' True  xs t = nf' True xs =<< eval t
+    nf' False xs t = qq xs t
+
+instance Nf Id Term where
+    nf' b xs i = do e <- getEnv
+                    let (PrtInfo x shouldExpand) = prtE e i
+                    case getE e i of
+                      (Id _)      -> return (Var Unknown x) 
+                      (Closure t) -> if shouldExpand then nf' b xs t
+                                     -- this is bad, we should not
+                                     -- expand inside a box!
+                                     else return (Var Unknown x) 
+
+qq :: Env e => Vars -> Clos Term -> Eval e Term
+qq xs (Var l x  , s) = quote xs =<< getId l x s
+qq _  (Let _ _ _, _) = return (Label Unknown "*quote-let-not-implemented*")
+--qq xs (Let l g t, s) = fail "quote let: not implemented!"
+{-do s' <- evalProg (g,s)
+                        qq xs (t,s')  
+                       -- this seems wrong! we should return a Let
+                       -- and we should extend xs!
+-}
+qq xs (Q l ps (a,(x,b)),s) = 
+    do a' <- qq xs (a,s)
+       xb' <- quote xs (x,(b,s))
+       return (Q l ps (a',xb'))
+qq xs (Lift l t,s) = liftM (Lift l) (qq xs (t,s))
+-- qq xs (LType l t,s) = liftM (LType l) (qq xs (t,s))
+qq xs (Lam l (x,t), s) = liftM (Lam l) (quote xs (x,(t,s)))
+qq xs (App t u ,s) = do t' <- qq xs (t,s)
+                        u' <- qq xs (u,s)
+                        return (App t' u')
+qq xs (Pair l t u,s) = do t' <- qq xs (t,s)
+                          u' <- qq xs (u,s)
+                          return (Pair l t' u')
+qq xs (Split l t (x,(y,u)),s) = do t' <- qq xs (t,s)
+                                   xyu' <- quote xs (x,(y,(u,s)))
+                                   return (Split l t' xyu')
+qq xs (Case l t lts,s) = do t' <- qq xs (t,s)
+                            lts' <- mapM (\ (l',t'') -> 
+                                              do t''' <- qq xs (t'',s)
+                                                 return (l',t''')) lts
+                            return (Case l t' lts')              
+qq xs (Box l t,s) = liftM (Box l) (qq xs (t,s))
+qq xs (Force l t,s) = liftM (Force l) (qq xs (t,s))
+qq _ (t,_) = return t -- Type, Enum, Label
+
+instance (Closure a,Nf a b) => Nf (Bind a) (Bind b) where
+    nf' b xs (x,t)  = do let x' = fresh x xs
+                         (_,s') <- decl x (PrtInfo x' True) (getScope t) Nothing
+                         t' <- nf' b (x':xs) (putScope t s')
+                         return (x',t')
+
+instance Nf Val Term where
+    nf' b xs (Ne n) = nf' b xs n
+    nf' _ _  VType = return (Type Unknown)
+    nf' b xs (VQ ps ((a,(x,c)),s)) = do a' <- nf' b xs (a,s) 
+                                        xc' <- nf' b xs (x,(c,s))
+                                        return (Q Unknown ps (a',xc'))
+    nf' b xs (VLift c) = liftM (Lift Unknown) (nf' b xs c)
+--    nf' b xs (VLType c) = liftM (LType Unknown) (nf' b xs c)
+    nf' b xs (VLam xt) = liftM (Lam Unknown) (nf' b xs xt)
+    nf' b xs (VPair ((t,u),s)) = do t' <- nf' b xs (t,s)
+                                    u' <- nf' b xs (u,s)
+                                    return (Pair Unknown t' u')
+    nf' _ xs (VBox (Boxed c)) = liftM (Box Unknown) (nf' False xs c)
+    nf' _ _  (VEnum ls) = return (Enum Unknown ls)
+    nf' _ _  (VLabel l) = return (Label Unknown l)
+
+
+instance Nf Ne Term where
+    nf' b xs (NVar i) = nf' b xs i
+    nf' b xs (t :.. u) = do t' <- nf' b xs t
+                            u' <- nf' b xs u
+                            return (App t' u')
+    nf' b xs (NSplit t xyu) = do t' <- nf' b xs t
+                                 xyu' <- nf' b xs xyu
+                                 return (Split Unknown t' xyu')
+    nf' b xs (NCase t (lus,s)) = do t' <- nf xs t
+                                    lus' <- mapM (\ (l,u) -> 
+                                                   do u' <- nf' b xs (u,s)
+                                                      return (l,u')) lus
+                                    return (Case Unknown t' lus')
+    nf' _ xs (NForce t) = liftM (Force Unknown) (nf xs t)
diff --git a/src/Language/PiSigma/Parser.hs b/src/Language/PiSigma/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/PiSigma/Parser.hs
@@ -0,0 +1,160 @@
+module Language.PiSigma.Parser
+  ( parse
+  , sPhrase
+  , sProg
+  , s2Terms
+  , sTerm )
+  where
+
+import Prelude hiding (pi)
+import Control.Monad
+import Control.Applicative hiding ((<|>), many)
+import Data.List
+import Text.Parsec.Combinator
+import Text.Parsec.Error
+  ( ParseError )
+import Text.Parsec.Pos
+  ( SourceName )
+import Text.Parsec.Prim
+  hiding
+    ( label
+    , parse
+    , token )
+import qualified Text.ParserCombinators.Parsec
+  as Parsec
+    ( parse )
+import Text.ParserCombinators.Parsec.Char
+  ( string )
+
+import Language.PiSigma.Lexer
+import Language.PiSigma.Syntax hiding (label)
+import qualified Language.PiSigma.Util.String.Internal
+  as Internal
+import qualified Language.PiSigma.Util.String.Parser
+  as Parser
+
+sLabel :: Parser Name
+sLabel  = Internal.fromString <$> (string "'" *> identifier)
+
+sName  :: Parser Name
+sName   = Internal.fromString <$> identifier
+
+-- * Terms
+
+sTerm5 :: Parser Term
+sTerm5 = choice
+  [ Type  <$> locReserved "Type"
+
+  , Enum  <$>     location
+              <*> braces (many sName)
+          <?> "enumeration"
+
+  , Case  <$>     locReserved "case"
+              <*> sTerm
+              <*  reserved    "of"
+              <*> braces (sBranch `sepBy` locReservedOp "|")
+
+  , Label <$>     location
+              <*> sLabel
+          <?> "label"
+
+  , Box   <$>     location
+              <*> boxed sTerm
+          <?> "box"
+
+  , Lift  <$>     tokLift
+              <*> sTerm5
+          <?> "'^'"
+
+  , Var   <$> location <*> sName
+  , parens sTerm
+  ]
+  where
+    boxed p = choice [ brackets          p
+                     , reservedOp "♯" *> p
+                     ]
+
+sTerm4 :: Parser Term
+sTerm4 = choice
+  [ try $ (uncurry . Pair) <$> location
+                           <*> parens ((,) <$> sTerm <* comma <*> sTerm)
+  , sTerm5
+  ]
+
+sTerm3 :: Parser Term
+sTerm3 = choice
+  [ try (parens (sigmas <$> many1 ((,) <$> location <*> sName) <* reservedOp ":" <*> sTerm) <* reservedOp "*") <*> sTerm2
+  ,        Force <$> tokForce <*> sTerm4
+  , foldl1 App   <$> many1 sTerm4
+  ]
+
+sTerm2 :: Parser Term
+sTerm2 = foldr1 (-*-) <$> sTerm3 `sepBy1` reservedOp "*"
+
+-- TODO: make more beautiful or renumber
+sTerm1b :: Parser Term
+sTerm1b = choice
+  [ try (parens (pis <$> many1 ((,) <$> location <*> sName) <* reservedOp ":" <*> sTerm) <* tokArr) <*> sTerm
+  , sTerm2
+  ]
+       
+sTerm1 :: Parser Term
+sTerm1 = foldr1 (->-) <$> sTerm1b `sepBy1` tokArr
+
+sTerm :: Parser Term
+sTerm = choice
+  [ lam   <$  tokLam
+          <*> many ((,) <$> location <*> sName)
+          <*  tokArr
+          <*> sTerm
+
+  , split <$> locReserved "split"
+          <*> sTerm
+          <*     reserved "with"
+          <*> parens ((,) <$> sName
+                          <*  comma
+                          <*> sName)
+          <*  tokArr
+          <*> sTerm
+
+  , Let   <$> locReserved "let"
+          <*> sProg
+          <*     reserved "in"
+          <*> sTerm
+  , sTerm1
+  ]
+
+sProg :: Parser Prog
+sProg = concat <$> (sEntry `sepEndBy` semi)
+
+sEntry :: Parser [Entry]
+sEntry =
+    do
+      l <- location
+      n <- sName
+      b <- choice [ True  <$ reservedOp ":"
+                  , False <$ reservedOp "="
+                  ]
+      t <- sTerm
+      if b
+        then do
+               d <- option Nothing (Just <$ reservedOp "=" <*> sTerm)
+               case d of
+                 Nothing -> return [Decl l n t]
+                 Just t' -> return [Decl l n t, Defn l n t']
+        else return [Defn l n t]
+
+sBranch :: Parser (Label,Term)
+sBranch = (,) <$> sName <* tokArr <*> sTerm
+
+sPhrase :: Parser Phrase
+sPhrase = choice
+  [ try $ Prog <$> sProg <* eof
+  ,       Term <$> sTerm <* eof
+  ]
+
+s2Terms :: Parser (Term, Term)
+s2Terms = (,) <$> sTerm5 <*> sTerm5
+
+parse :: Parser a -> SourceName -> Parser.String -> Either ParseError a
+parse p = Parsec.parse (whiteSpace *> p <* eof)
diff --git a/src/Language/PiSigma/Pretty.hs b/src/Language/PiSigma/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/PiSigma/Pretty.hs
@@ -0,0 +1,193 @@
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE OverloadedStrings    #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+module Language.PiSigma.Pretty
+  ( module Text.PrettyPrint.MPPPC.OneDim
+  , Pretty
+  , Print
+  , evalPrint
+  , fromPretty )
+  where
+
+import Control.Monad.Error
+import Text.PrettyPrint.MPPPC.OneDim
+  hiding
+    ( Pretty )
+import qualified Text.PrettyPrint.MPPPC.OneDim
+  as OneDim
+
+import Language.PiSigma.Evaluate
+import Language.PiSigma.Normalise
+import Language.PiSigma.Syntax
+import qualified Language.PiSigma.Util.String.Internal
+  as Internal
+
+type Pretty = OneDim.Pretty (Seq Internal.String Char) (Tok Internal.String Char)
+
+-- * Print class for various types
+
+class Print a where
+    evalPrint :: Env e => a -> Eval e Pretty
+
+instance Print Internal.String where
+    evalPrint   = return . text . Seq
+
+instance Print Pretty where
+    evalPrint   = return
+
+instance Print Val where
+    evalPrint a = evalPrint =<< quote [] a
+
+instance Print (Clos Term) where
+    evalPrint a = evalPrint =<< quote [] a
+
+instance Print Ne where
+    evalPrint a = evalPrint =<< quote [] a
+
+instance Print Term where
+    evalPrint   = return . prettyTerm 0
+
+fromPretty :: Pretty -> Internal.String
+fromPretty = unSeq . renderSeq
+
+data Msg
+  = MsgV Val
+  | MsgC (Clos Term)
+  | MsgT Term
+  | MsgS Internal.String
+  | MsgD Pretty
+
+instance Print Msg where
+    evalPrint (MsgV v) = evalPrint v
+    evalPrint (MsgC c) = evalPrint c
+    evalPrint (MsgT t) = evalPrint t
+    evalPrint (MsgS s) = evalPrint s
+    evalPrint (MsgD d) = evalPrint d
+
+-- * Pretty printer for terms
+
+-- | Context for printing. Determines whether parentheses are
+-- required.
+type PrintContext = Int
+
+
+prettyTerm :: PrintContext -> Term -> Pretty
+
+prettyTerm _ (Var _ x)                   =
+      text $ Seq x
+
+prettyTerm _ (Let _ p t)                 =
+      list (map prettyEntry p)
+  <>  prettyTerm 0 t
+
+prettyTerm _ (Type _)                    =
+      text "Type"
+
+prettyTerm c (Q _ Pi (t1, (n, t2)))      =
+      contextParens c 1
+   $  group
+   $  binding 2 n t1
+  <$> text "->"
+  <+> prettyTerm 1 t2
+
+prettyTerm c (Q _ Sigma (t1, (n, t2)))   =
+      contextParens c 2
+   $  binding 3 n t1
+  <+> text "*"
+  <+> prettyTerm 2 t2
+
+prettyTerm c (Lam _ (n, t))              =
+      contextParens c 0
+   $  text "\\"
+  <+> text (Seq n)
+  <+> text "->"
+  <+> prettyTerm 0 t
+
+prettyTerm c (App t1 t2)                 =
+      group
+   $  hang 2
+   $  contextParens c 3
+   $  prettyTerm 3 t1
+  <$> prettyTerm 4 t2
+
+prettyTerm _ (Pair _ t1 t2)              =
+      tupled $ map (prettyTerm 0) [t1, t2]
+
+prettyTerm c (Split _ t1 (n1, (n2, t2))) =
+      contextParens c 0
+   $  hang 2
+   $  text "split"
+  <+> prettyTerm 0 t1
+  <+> text "with"
+  <+> (parens $  text (Seq n1)
+              <> comma
+              <> text (Seq n2))
+  <+> text "->"
+  <$> prettyTerm 0 t2
+
+prettyTerm _ (Enum _ ls)                 =
+      braces
+   $  sep
+   $  map (text . Seq) ls
+
+prettyTerm _ (Label _ l)                 =
+      text $ Tok '\'' `cons` Seq l
+
+prettyTerm _ (Case _ t bs)               =
+      hang 1
+   $  text "case"
+  <+> prettyTerm 0 t
+  <+> text "of"
+  <$> branches bs
+
+prettyTerm c (Lift _ t)                  =
+     contextParens c 5
+   $ text "^"
+  <> prettyTerm 5 t
+
+prettyTerm _ (Box _ t)                   =
+      brackets $ prettyTerm 0 t
+
+prettyTerm c (Force _ t)                 =
+     contextParens c 3
+   $ text "!"
+  <> prettyTerm 4 t
+
+
+prettyEntry :: Entry -> Pretty
+
+prettyEntry (Defn _ n t)                 =
+      hang 2
+   $  text (Seq n)
+  <+> text "="
+  <$> prettyTerm 0 t
+  <>  text ";"
+
+prettyEntry (Decl _ n t)                 =
+      hang 2
+   $  text (Seq n)
+  <+> text ":"
+  <$> prettyTerm 0 t
+  <>  text ";"
+
+
+binding :: PrintContext -> Name -> Term -> Pretty
+binding c n t | Internal.null n =  prettyTerm c t
+              | otherwise       =  parens
+                                $  text (Seq n)
+                               <+> colon
+                               <+> prettyTerm 0 t
+
+branches :: [(Label,Term)] -> Pretty
+branches = encloseSep (text " { ") (text " } ") (text " | ") . map branch
+  where
+    branch (n, t) =  text (Seq n)
+                 <+> text "->"
+                 <+> prettyTerm 0 t
+
+-- | Prints parens if the current context is higher
+-- than a certain limit.
+contextParens :: PrintContext -> PrintContext -> Pretty -> Pretty
+contextParens c d p | c > d     = parens p
+                    | otherwise = p
diff --git a/src/Language/PiSigma/Syntax.hs b/src/Language/PiSigma/Syntax.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/PiSigma/Syntax.hs
@@ -0,0 +1,356 @@
+{-# LANGUAGE OverloadedStrings    #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+module Language.PiSigma.Syntax
+  ( Bind
+  , Boxed    (..)
+  , Clos
+  , Closure  (..)
+  , Entry    (..)
+  , Enum
+  , Env
+  , EnvEntry (..)
+  , EnvEntries
+  , GetLoc   (..)
+  , Id
+  , Label
+  , Loc      (..)
+  , Name
+  , Ne       (..)
+  , Phrase   (..)
+  , PiSigma  (..)
+  , Prog
+  , PrtInfo  (..)
+  , Scope    (..)
+  , Term     (..)
+  , Type
+  , Val      (..)
+  , (-*-)
+  , (->-)
+  , emptyE
+  , emptyScope
+  , extE
+  , extendScope
+  , getE
+  , label
+  , lam
+  , locMessage
+  , lookupCon
+  , lookupScope
+  , pis
+  , prtE
+  , setE
+  , sigmas
+  , split
+  , ty )
+  where
+
+import Prelude
+  hiding
+    ( pi )
+import Data.Maybe
+  ( fromJust )
+
+import qualified Language.PiSigma.Util.String.Internal
+  as Internal
+
+-- * Locations
+
+data Loc
+  = Unknown
+  | Loc { filename :: !String
+        , line     :: !Int
+        , column   :: !Int }
+  deriving Show
+
+locMessage :: Loc -> String
+locMessage Unknown     = "<unknown>:"
+locMessage (Loc f l c) = concat
+                       [ f
+                       , ":"
+                       , show l
+                       , ":"
+                       , show c
+                       , ":"
+                       ]
+
+-- | Locations are always equal. This allows us to
+-- derive equality for the abstract syntax that ignores
+-- the locations.
+instance Eq Loc where
+  _ == _ = True
+
+class GetLoc a where
+  getLoc :: a -> Loc
+
+-- * Abstract syntax
+
+data Phrase
+  = Prog Prog
+  | Term Term
+  deriving (Show, Eq)
+
+type Name  = Internal.String
+
+type Label = Internal.String
+
+data Entry
+  = Decl Loc Name Type
+  | Defn Loc Name Term
+  deriving (Show, Eq)
+
+instance GetLoc Entry where
+  getLoc (Decl l _ _) = l
+  getLoc (Defn l _ _) = l
+
+type Prog = [Entry]
+
+{-
+Maybe better
+data Prog = Decl Type (Bind Prog) | Defn Name Term Prog
+-}
+
+type Type = Term
+
+-- | The use of Bind indicates the scope of the
+-- bound identifier.
+type Bind a = (Name, a)
+
+-- | For treating quantifiers in a uniform way.
+data PiSigma
+  = Pi
+  | Sigma
+  deriving (Show, Eq)
+
+data Term
+  = Var   Loc Name
+  | Let   Loc Prog Term
+  | Type  Loc
+  | Q     Loc PiSigma (Type, Bind Type)
+  | Lam   Loc (Bind Term)
+  | App   Term Term
+  | Pair  Loc Term Term
+  | Split Loc Term (Bind (Bind Term)) -- split t with (x,y) -> u
+  | Enum  Loc [Name]
+  | Label Loc Label
+  | Case  Loc Term [(Label, Term)]     -- case t of { L -> u }
+  | Lift  Loc Term
+  | Box   Loc Term
+  | Force Loc Term
+--  | LType Loc Term -- lazy type ($ sigma)
+  deriving (Show,Eq)
+
+instance GetLoc Term where
+  getLoc (Var   l _  ) = l
+  getLoc (Let   l _ _) = l
+  getLoc (Type  l    ) = l
+  getLoc (Q     l _ _) = l
+  getLoc (Lam   l _  ) = l
+  getLoc (App   t _  ) = getLoc t
+  getLoc (Pair  l _ _) = l
+  getLoc (Split l _ _) = l
+  getLoc (Enum  l _  ) = l
+  getLoc (Label l _  ) = l
+  getLoc (Case  l _ _) = l
+  getLoc (Lift  l _  ) = l
+  getLoc (Box   l _  ) = l
+  getLoc (Force l _  ) = l
+--  getLoc (LType l _)   = l
+
+-- * Smart constructors
+
+-- | Smart constructor for lambda abstractions.
+lam :: [(Loc, Name)] -> Term -> Term
+lam []            t = t
+lam ((l, x) : xs) t = Lam l (x, lam xs t)
+
+-- | Smart constructor for split.
+split :: Loc -> Term -> (Name, Name) -> Term -> Term
+split l t1 (x, y) t2 = Split l t1 (x, (y, t2))
+
+-- | Smart constructor for quantifiers.
+q :: PiSigma -> [(Loc, Name, Type)] -> Type -> Type
+q _  []                b = b
+q ps ((l, x, a) : xas) b = Q l ps (a, (x, q ps xas b))
+
+-- | Smart constructor for multiple Pi applications.
+pis' :: [(Loc, Name, Type)] -> Type -> Type
+pis'     = q Pi
+
+-- | Smart constructor for multiple Pi applications.
+pis :: [(Loc, Name)] -> Type -> Type -> Type
+pis ns t = pis' (map (\ (l, n) -> (l, n, t)) ns)
+
+-- | Smart constructor for Pi.
+pi :: Loc -> Name -> Type -> Type -> Type
+pi l n t = pis' [(l, n, t)]
+
+-- | Smart constructor for multiple Sigma applications.
+sigmas' :: [(Loc,Name,Type)] -> Type -> Type
+sigmas' = q Sigma
+
+-- | Smart constructor for multiple Sigma applications.
+sigmas :: [(Loc,Name)] -> Type -> Type -> Type
+sigmas ns t = sigmas' (map (\ (l, n) -> (l, n, t)) ns)
+
+-- | Smart constructor for Sigma.
+sigma :: Loc -> Name -> Type -> Type -> Type
+sigma l n t = sigmas' [(l, n, t)]
+
+-- | Smart constructor for function space.
+(->-) :: Type -> Type -> Type
+(->-) t = pi (getLoc t) "" t
+
+-- | Smart constructor for product.
+(-*-) :: Type -> Type -> Type
+(-*-) t = sigma (getLoc t) "" t
+
+-- * Values (well-scoped WHNFs) and environments
+
+-- ** Identifiers
+
+type Id = Int -- index in (potentially multiple) environments
+
+-- ** Scopes
+
+newtype Scope = Scope [(Name, (Id, Maybe (Clos Type)))]
+  deriving (Show, Eq)
+
+{-
+
+TODO:
+
+Perhaps return to the following types for scopes:
+
+data Sc a = Scope [(Name,(Id, a))]
+
+type Scope = Sc ()
+type Ctx   = Sc (Clos Type)
+
+We then need a forgetful mapping:
+
+fog :: Ctx -> Scope
+fog c = map (\ (x,(i,a)) -> (x,(i,()))) c 
+
+Alternatively, we can try to make Scopes
+existential, essentially:
+
+type Scope = exists a. Sc a
+
+-}
+
+emptyScope :: Scope
+emptyScope = Scope []
+
+extendScope :: Scope -> Name -> (Id, Maybe (Clos Type)) -> Scope
+extendScope (Scope s) x (i, a) = Scope $ (x, (i, a)) : s
+
+lookupScope :: Scope -> Name -> Maybe Id
+lookupScope (Scope s) x = do idCon <- lookup x s
+                             return $! fst idCon
+
+lookupCon   :: Scope -> Name -> Maybe (Clos Type)
+lookupCon   (Scope s) x = do idCon <- lookup x s
+                             return $! fromJust $! snd idCon
+
+-- ** Closures
+
+type Clos a = (a, Scope)
+
+instance GetLoc a => GetLoc (Clos a) where
+  getLoc (x, _) = getLoc x
+
+--type C a = (Con,a)
+
+--c2clos :: C a -> Clos a
+--c2clos (g,a) = (a,fog g)
+
+-- fix order, name of C...
+
+class Closure a where 
+  getScope :: a -> Scope
+  putScope :: a -> Scope -> a
+
+instance Closure (Clos a) where
+  getScope (_, s)   = s
+  putScope (a, _) s = (a, s)
+
+instance Closure a => Closure (Bind a) where
+  getScope (_, a)   = getScope a
+  putScope (x, a) s = (x, putScope a s)
+
+instance Closure Boxed where
+  getScope (Boxed c) = getScope c
+  putScope (Boxed c) = Boxed . putScope c
+
+{- could be used to refactor the code using bindings. -}
+
+ty :: Clos Type
+ty = (Type Unknown, emptyScope)
+
+--lty :: Clos Type
+--lty = (Lift Unknown (Type Unknown), emptyScope)
+
+label :: Label -> Clos Term
+label s = (Label Unknown s, emptyScope)
+
+-- type VType = Val -- unused?
+
+newtype Boxed = Boxed (Clos Term)
+  deriving (Show, Eq)
+
+-- ** Values
+
+data Val
+  = Ne Ne
+  | VType 
+  | VQ PiSigma (Clos (Type, Bind Type))
+  | VLift (Clos Type)
+  | VLam (Bind (Clos Term))
+  | VPair (Clos (Term, Term))
+  | VEnum [Label]
+  | VLabel Label 
+  | VBox Boxed
+--  | VLType (Clos Type)
+  deriving (Show, Eq)
+
+-- | Neutral terms.
+data Ne
+  = NVar Id
+  | Ne :.. (Clos Term)
+  | NSplit Ne (Bind (Bind (Clos Term)))
+  | NCase Ne (Clos [(Label, Term)])
+  | NForce Ne
+  deriving (Show, Eq)
+
+-- ** Environments
+
+data EnvEntry
+  = Id Id
+  | Closure (Clos Term)
+  deriving Show
+
+data PrtInfo
+  =  PrtInfo { name   :: Name
+             , expand :: Bool }
+
+class Env e where 
+  emptyE :: e
+  extE   :: e -> PrtInfo -> (Id,e)
+  setE   :: e -> Id -> EnvEntry -> e
+  getE   :: e -> Id -> EnvEntry
+  prtE   :: e -> Id -> PrtInfo
+
+set :: [a] -> Int -> a -> [a]
+set []       _ _ = error "list is empty"
+set (_ : as) 0 b = b : as
+set (a : as) i b = a : set as (i - 1) b
+
+type EnvEntries = [(EnvEntry, PrtInfo)]
+
+instance Env EnvEntries where
+  emptyE     = []
+  extE e x   = case length e of i    -> (i, e ++ [(Id i, x)])
+  setE e i v = case e !! i of (_, x) -> set e i (v, x)
+  getE e i   = case e !! i of (v, _) -> v
+  prtE e i   = case e !! i of (_, x) -> x
diff --git a/src/Language/PiSigma/Util/String/Internal.hs b/src/Language/PiSigma/Util/String/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/PiSigma/Util/String/Internal.hs
@@ -0,0 +1,48 @@
+module Language.PiSigma.Util.String.Internal
+  ( String
+  , append
+  , concat
+  , fromString
+  , isPrefixOf
+  , null
+  , putStrLn
+  , toString )
+  where
+
+import Prelude
+  hiding
+    ( String
+    , concat
+    , null
+    , putStrLn )
+import qualified Prelude
+  as Prelude
+import qualified Data.ByteString
+  as Word8
+import qualified Data.Text
+  as Text
+import qualified Data.Text.Encoding
+  as Text
+
+type String = Text.Text
+
+append     :: String -> String -> String
+append      = Text.append
+
+concat     :: [String] -> String
+concat      = Text.concat
+
+fromString :: Prelude.String -> String
+fromString  = Text.pack
+
+isPrefixOf :: String -> String -> Bool
+isPrefixOf  = Text.isPrefixOf
+
+null       :: String -> Bool
+null        = Text.null
+
+putStrLn   :: String -> IO ()
+putStrLn    = Word8.putStrLn . Text.encodeUtf8
+
+toString   :: String -> Prelude.String
+toString    = Text.unpack
diff --git a/src/Language/PiSigma/Util/String/Parser.hs b/src/Language/PiSigma/Util/String/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/PiSigma/Util/String/Parser.hs
@@ -0,0 +1,118 @@
+{-# LANGUAGE OverloadedStrings    #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+module Language.PiSigma.Util.String.Parser
+  ( String
+  , append
+  , fromString
+  , isPrefixOf
+  , lines
+  , null
+  , readFile
+  , span
+  , toString
+  , uncons
+  , unlines )
+  where
+
+import Prelude
+  hiding
+    ( String
+    , lines
+    , null
+    , readFile
+    , replicate
+    , span
+    , unlines )
+import qualified Prelude
+  as Prelude
+import qualified Data.ByteString.Lazy
+  as Lazy
+import qualified Data.ByteString.Lazy.UTF8
+  as LazyUTF8
+import qualified Data.String as String
+
+-- * The parser input type
+
+type String = LazyUTF8.ByteString
+
+instance String.IsString String where
+  fromString = fromString
+
+append     :: String -> String -> String
+append      = Lazy.append
+
+fromString :: Prelude.String -> String
+fromString  = LazyUTF8.fromString
+
+isPrefixOf :: String -> String -> Bool
+isPrefixOf  = Lazy.isPrefixOf
+
+lines      :: String -> [String]
+lines       = LazyUTF8.lines
+
+null       :: String -> Bool
+null        = Lazy.null
+
+readFile   :: FilePath -> IO String
+readFile    = Lazy.readFile
+
+span       :: (Char -> Bool) -> String -> (String, String)
+span        = LazyUTF8.span
+
+toString   :: String -> Prelude.String
+toString    = LazyUTF8.toString
+
+uncons     :: String -> Maybe (Char, String)
+uncons      = LazyUTF8.uncons
+
+unlines    :: [String] -> String
+unlines     = Lazy.intercalate "\n"
+
+
+
+-- NOTE: Commenting out the code above and uncommenting the code below
+-- results in an incredible slowdown during parsing.  I'm not sure why
+-- this is since Data.Text should be pretty fast.  Using strict versus
+-- lazy Data.Text is even worse.
+
+-- import Control.Monad
+--   ( liftM )
+-- import qualified Data.ByteString.Lazy
+--   as Word8
+-- import qualified Data.Text.Lazy
+--   as Text
+-- import qualified Data.Text.Lazy.Encoding
+--   as Text
+
+-- type String = Text.Text
+
+-- append     :: String -> String -> String
+-- append      = Text.append
+
+-- fromString :: Prelude.String -> String
+-- fromString  = Text.pack
+
+-- isPrefixOf :: String -> String -> Bool
+-- isPrefixOf  = Text.isPrefixOf
+
+-- lines      :: String -> [String]
+-- lines       = Text.lines
+
+-- null       :: String -> Bool
+-- null        = Text.null
+
+-- readFile   :: FilePath -> IO String
+-- readFile    = liftM Text.decodeUtf8 . Word8.readFile
+
+-- span       :: (Char -> Bool) -> String -> (String, String)
+-- span        = Text.spanBy
+
+-- toString   :: String -> Prelude.String
+-- toString    = Text.unpack
+
+-- uncons     :: String -> Maybe (Char, String)
+-- uncons      = Text.uncons
+
+-- unlines    :: [String] -> String
+-- unlines     = Text.unlines
diff --git a/src/PiSigma.hs b/src/PiSigma.hs
deleted file mode 100644
--- a/src/PiSigma.hs
+++ /dev/null
@@ -1,265 +0,0 @@
-{-# 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
-
diff --git a/src/PiSigma/Check.hs b/src/PiSigma/Check.hs
deleted file mode 100644
--- a/src/PiSigma/Check.hs
+++ /dev/null
@@ -1,189 +0,0 @@
-module PiSigma.Check where
-
-import Control.Monad
-
-import PiSigma.Syntax
-import PiSigma.Evaluation
-import PiSigma.Print
-import PiSigma.Equality
-
---import Debug.Trace
---trace "check\n" $
-
--- closures are the other way around
--- should be fixed by changing closures.
-
-{-
-fog :: CTerm -> Closure
-fog (g,t) = (con2scope g,t)
--}
-
-failc :: Env e => Clos Term -> [Msg] -> Eval e a
-failc t m = failp ([S "Checking:\t",C t,S "\n"]++m)
-
--- | Takes a term and an (unevaluated) type. We first
--- handle the cases that may potentially change the
--- environment. If none of those cases match, we can
--- safely evaluate the type and call check'.
-check :: Env e => Clos Term -> Clos Type -> Eval e ()
---check (g,t) c | trace ("check\ng ="++(show g)++"\n t="++(show t)++"\nc="++(show c)++"\n") False = undefined
-
-check (Let p t,g) c = 
-    do g' <- checkProg (p,g)
-       check (t,g') c
-
-check (gt @  (Split t (x,(y,u)),g)) c = 
-    do sigab <- infer' (t,g)
-       case sigab of
-         (VQ Sigma ((a,(z,b)),s)) -> 
-             do t'      <- eval (t,g)
-                (_,g')  <- tdecl x g (a,s)
-                b       <- subst (z,(b,s)) (Var x, g')
-                (_,g'') <- tdecl y g' b
-                case t' of
-                  (Ne (NVar i)) ->
-                      letn' i (Pair (Var x,Var y), g'')
-                                (check (u,g'') c)
-                      -- this is a bit silly since we know the ids.
-                  _ -> check (u,g'') c
-                      -- instead of failing, we just omit the assignment.
-         _ -> failc gt [S "split : Sigma type expected\nFound:\t",V sigab,S "\n(split)\n"]
-
-check gt @ (t'@(Case t lus),g) c = 
-    do enum <- infer' (t,g)
-       case enum of
-         VEnum ls -> 
-             let ls' = map fst lus
-             in if ls /= ls'
-                then do -- pt' <- prt t'
-                        failc gt [S ("case: labels don't match"
-                                     ++ "\n expected : " ++ show ls
-                                     ++ "\n inferred : " ++ show ls'
-                                     ++ "\n(match)\n")]
-                -- set equivalence would be sufficent
-                else do t' <- eval (t,g)
-                        case t' of
-                          -- if the scrutinee is a variable, we add a constraint
-                          -- while checking each of the branches
-                          (Ne (NVar i)) ->
-                               mapM_ (\ (l,u) -> 
-                                      letn' i (label l)
-                                            (check (u,g) c)) lus
-                          -- if the scrutinee is not a variable, we do not add
-                          -- a constraint, but continue
-                          _ -> mapM_ (\ (l,u) -> check (u,g) c) lus
-         _ -> failc gt [S "case : enum type expected\nFound:\t",V enum,S "\n(case)\n"]
-         {- Problem: here and other places: we try to print the term t which isn't yet 
-            typechecked and may contain undefined variables which may crash the printer...
-            see undef-bug.pi
-         -}
-check (Force t,g) (a , s) =
-    check (t,g) (Lift a , s)
-
-check t a = do a' <- feval a
-               check' t a'
-
-check' :: Env e => Clos Term -> Val -> Eval e ()
-check' gt (VBox (Boxed a)) = check gt a  -- do we still need this line?
-check' (Lam (x,t),g) (VQ Pi ((a,(y,b)),s)) =
-    do (i,g') <- tdecl x g (a,s)
-       let s' = extendScope s y (i,Nothing)
-       check (t,g') (b,s')
-check' gt @ (Lam _,g) a = failc gt [S "Expected:\t",V a,S "\n(Lam)\n"]
-check' (Pair (t,u),g) (VQ Sigma ((a,(y,b)),s)) =
-    do check (t,g) (a,s)
-       b <- subst (y,(b,s)) (t,g)
-       check (u,g) b
-check' gt @ (t @ (Pair _),g) a = failc gt [S "Expected\t",V a,S "\n(Pair)\n"]
--- Labels cannot be inferred because there is no way to know
--- what the other labels are.
-check' gt @ (Label l,g) a @ (VEnum ls) | l `elem` ls = return ()
-check' gt @ (Label l,g) a = failc gt [S "Expected\t",V a,S "\n(Label)\n"]
--- To check that [sigma] is a type, it's sufficient to know
--- that sigma is a type. The alternative would seem to be to
--- assume that ^Type == Type, but that does not work.
-check' (Box a,g) VType =
-    check (a,g) ty
-check' (Box t,g) (VLift a) =
-    check (t,g) a
-check' gt @ (Box _,g) a = failc gt [S "Expected\t",V a,S "\n(Box)\n"]
-check' t a =
-    do b <- infer' t
-       catchE (eq a b)
-         (\ s -> failc t [S "Expected:\t",V a,
-                          S "\nFound:\t",V b,S $ "\n(check)\n"])
--- ++s++"\n"++(show a)++"\n"++(show b)])
--- useful for debugging.
-
-inferVar :: Env e => Clos Name -> Eval e (Clos Type)
-inferVar (x,g) =
-    case lookupCon g x of
-      Just a  -> return a
-      Nothing -> fail ("Undefined variable: "++x++"\n(inferVar)\n")
-
-infer :: Env e => Clos Term -> Eval e (Clos Type)
---infer (g,t) | trace ("infer\ng ="++(show g)++"\n t="++(show t)++"\n") False = undefined
-
-infer (Var x,g) = inferVar (x,g)
-
-infer (Let tel t,g) = 
-    do g' <- checkProg (tel,g)
-       infer (t,g')  
-
-infer (Type,g) = return ty
-
-infer (Q _ (a,(x,b)),g) = 
-    do check (a,g) ty
-       (_,g') <- tdecl x g (a,g)
-       check (b,g') ty
-       return ty
-
-infer gt@(t :. u,g) = 
-    do piab <- infer' (t,g)
-       case piab of 
-         (VQ Pi ((a,(x,b)),s)) -> do check (u,g) (a,s)
-                                     subst (x,(b,s)) (u,g)
-         _ -> failc gt [S "Pi type expected, but found:\t",
-                        V piab,
-                        S "\n(app)\n"]
-
-infer (Enum _,_) = return ty
-
-infer (Box t,g) =
-    liftM (\ (a,s) -> (Lift a,s)) (infer (t,g))
-
--- TODO: either use infer', or explain why forced eval
--- cannot be used here.
-infer gt@(Force t,g) =
-    do a  <- infer (t,g)
-       a' <- eval a
-       case a' of
-         VLift b -> return b
-         _       -> failc gt [S "Lifted type expected\n(Force)\n"]
-infer (Lift a,g) =
-    do check (a,g) ty
-       return ty
-
-infer gt = failc gt [S "Not inferable\n(infer)\n"]
-
-
--- | Infers a type and evaluates it.
-infer' :: Env e => Clos Term -> Eval e Val
-infer' gt =
-    do a <- infer gt
-       feval a
-
-checkProg :: Env e => Clos Prog -> Eval e Scope
-checkProg ([],g) = return g
-checkProg ((Decl x a):tel,g) = 
-    do check (a,g) ty 
-       (_,g') <- decl x (PrtInfo {name=x, expand=False}) g (Just (a,g))
-       checkProg (tel,g')
-checkProg ((Defn x t):tel,g) =
-    do a <- inferVar (x,g)
-       check (t,g) a
-       i <- getId x g
-       defn' i (t,g)
-       checkProg (tel,g)
-       
-                             
diff --git a/src/PiSigma/Equality.hs b/src/PiSigma/Equality.hs
deleted file mode 100644
--- a/src/PiSigma/Equality.hs
+++ /dev/null
@@ -1,128 +0,0 @@
-{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
-module PiSigma.Equality where
-
-import Control.Monad
-
-import PiSigma.Syntax
-import PiSigma.Evaluation
-
-class Equal a where
-    eq :: Env e => a -> a -> Eval e ()
-
-instance Equal (Clos Term) where
-    eq t u = do t' <- eval t
-                u' <- eval u
-                eq t' u'
-
-eq' :: Env e => Clos (Term,Term) -> Eval e ()
-eq' ((t,u),s) = eq (t,s) (u,s)
-
-eqBind :: (Env e,Closure a) =>
-          (a -> a -> Eval e ()) ->
-          Bind a -> Bind a -> Eval e ()
-eqBind eq (x0,c0) (x1,c1) =
-  do let s0 = getScope c0
-         s1 = getScope c1
-     (i,s0') <- decl' x0 s0
-     let s1' = extendScope s1 x1 (i,Nothing)
-     let c0' = putScope c0 s0'
-         c1' = putScope c1 s1'
-     eq c0' c1'
-
-instance (Equal a,Closure a) => Equal (Bind a) where
-    eq = eqBind eq
-
-instance Equal Val where
-    eq (Ne t0) (Ne t1) = eq t0 t1
-    eq (VQ ps0 ((a0,(x0,b0)),s0)) (VQ ps1 ((a1,(x1,b1)),s1))
-      | ps0 == ps1 = 
-        do eq (a0,s0) (a1,s1)
-           eq (x0,(b0,s0)) (x1,(b1,s1))
-    eq (VLam xt0) (VLam xt1) = eq xt0 xt1
-    eq (VPair ((t0,u0),s0)) (VPair ((t1,u1),s1)) = 
-        do eq (t0,s0) (t1,s1)
-           eq (u0,s0) (u1,s1)
-    eq (VBox b) (VBox b') = eq b b' 
-    eq (VLift a) (VLift a') = eq a a'
-    eq v0 v1 | v0 == v1 = return () -- Type, Label, Enum
-             | otherwise = fail "Different values"
-
-eqBox :: Env e => Clos Term -> Clos Term -> Eval e ()
-eqBox (Var x,s) (Var y,s') = 
-    do x' <- getId x s
-       y' <- getId y s'
-       eq x' y'
-{-
-eqBox (Var x,s) u =
-    do x' <- getId x s
-       ei <- lookupId x'
-       case ei of
-         Closure t -> eqBox t u
-         Id j -> fail "eqBox: var vs term"
-       -- wrong level - this should use functions in Evaluation
-       -- have to avoid races: don't unfold the same id twice!
-eqBox t u @ (Var _,_) = eqBox u t          
--}
-eqBox (Let p t,s) c = fail "eqBox: let not implemented"
-{-
-    do s' <- evalProg (p,s)
-       eqBox (t,s') c
--}
-eqBox c c'@(Let p t,s) = eqBox c' c 
-eqBox (Q ps (a,(x,b)),s) (Q ps' (a',(x',b')),s')
-      | ps == ps' = 
-          do eqBox (a,s) (a',s')
-             eq (x,Boxed (b,s)) (x',Boxed (b',s'))
-eqBox (t :. u,s) (t' :. u',s') =
-    do eqBox (t,s) (t',s')
-       eqBox (u,s) (u',s')
-eqBox (Split t (x,(y,u)),s) (Split t' (x',(y',u')),s') =
-    do eqBox (t,s) (t',s')
-       eq (x,(y,Boxed (u,s))) (x',(y',Boxed (u',s')))
-eqBox (Case t bs,s) (Case t' bs',s') =
-    do eqBox (t,s) (t',s')
-       zipWithM_ (\ (l,t) (l',t') -> 
-                      if l==l' then eqBox (t,s) (t',s')
-                      else fail "eqBox case") bs bs'
-eqBox (Lift t,s) (Lift t',s') = eqBox (t,s) (t',s')
-eqBox (Box t,s) (Box t',s') = eqBox (t,s) (t',s')
-eqBox (Force t,s) (Force t',s') = eqBox (t,s) (t',s')               
-eqBox (t,s) (t',s') | t == t' = return () -- Type, Label, Enum
-                    | otherwise = fail "Different terms"
--- TODO: check that it cannot happen that t and t' are syntacically equal but not alpha equivalent!
-    
-instance Equal Boxed where
-    eq (Boxed c) (Boxed c') = eqBox c c'
-
-instance Equal Id where
-    eq i0 i1  
-        | i0 == i1  = return ()
-        | otherwise = do ei0 <- lookupId i0
-                         ei1 <- lookupId i1
-                         case (ei0,ei1) of
-                           (Id j0, Id j1) -> unless (j0 == j1)
-                                               (fail "Different variables")
-                           (Closure t0, Closure t1) ->
-                               letn i0 (Id i0)
-                                    (letn i1 (Id i0)
-                                          (eq t0 t1))
-                           _ -> fail "Variable vs neutral"
-
-instance Equal Ne where
-    eq (NVar i0) (NVar i1) = eq i0 i1
-    eq (t0 :.. u0) (t1 :.. u1) = 
-        do eq t0 t1
-           eq u0 u1
-    eq (NSplit t0 xyu0) (NSplit t1 xyu1) =
-        do eq t0 t1
-           eq xyu0 xyu1
-    eq (NCase t0 (lus0,s0)) (NCase t1 (lus1,s1)) =
-        do eq t0 t1
-           let eqBranches [] [] = return ()
-               eqBranches ((l0,u0):lus0) ((l1,u1):lus1) | l0 == l1 =
-                 do eq (u0,s0) (u1,s1)
-                    eqBranches lus0 lus1
-               eqBranches _ _ = fail "Case: branches differ"
-           eqBranches lus0 lus1
-    eq (NForce t) (NForce t') = eq t t'
-    eq t u = fail ("Different neutrals:\n"++ show t ++"\n/=\n"++ show u ++"\n")
diff --git a/src/PiSigma/Evaluation.hs b/src/PiSigma/Evaluation.hs
deleted file mode 100644
--- a/src/PiSigma/Evaluation.hs
+++ /dev/null
@@ -1,151 +0,0 @@
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-module PiSigma.Evaluation where
-
-import Control.Monad.Error
-import Control.Monad.State
-import Control.Monad.Identity
-
-import PiSigma.Syntax
-
--- * Monad used for evaluation
-
-newtype Eval e a =
-  Eval {unEval :: StateT e (ErrorT String Identity) a}
-  deriving (Monad,MonadError String,MonadState e)
-
-run :: e -> Eval e a -> Either String (a,e)
-run e (Eval p) = runIdentity $ runErrorT $ runStateT p e 
-
-catchE :: Eval e a -> (String -> Eval e a) -> Eval e a
-catchE  = catchError
-
-getEnv :: Eval e e
-getEnv = get
-
-setEnv :: e -> Eval e ()
-setEnv = put
-
-getId :: Name -> Scope -> Eval e Id
-getId x s = case lookupScope s x of 
-              Just i -> return i
-              Nothing -> fail ("Undefined Variable: "++x++"\n")
-
--- | Takes a name, a scope, and potentially a type.
--- It extends the environment and the scope with that name.
-decl :: Env e =>
-        Name -> PrtInfo -> Scope -> Maybe (Clos Type) ->
-        Eval e (Id,Scope)
-decl x x' s a =
-    do e <- getEnv
-       let (i,e') = extE e x'
-       setEnv e'
-       return (i,extendScope s x (i,a))
-
-decl' :: Env e => Name -> Scope -> Eval e (Id,Scope)
-decl' x s   = decl x (PrtInfo {name = x, expand = True}) s Nothing
-
-tdecl :: Env e => Name -> Scope -> (Clos Type) -> Eval e (Id,Scope)
-tdecl x g a = decl x (PrtInfo {name = x, expand = True}) g (Just a)
-
--- | Updates the environment.
-defn :: Env e => Id -> EnvEntry -> Eval e ()
-defn i ei =
-    do e <- getEnv
-       setEnv (setE e i ei)
-
-defn' :: Env e => Id -> Clos Type -> Eval e ()
-defn' i t = defn i (Closure t)
-
--- | Locally updates the environment.
-letn :: Env e => Id -> EnvEntry -> Eval e a -> Eval e a
-letn i ei p =
-    do eo <- lookupId i
-       defn i ei
-       a <- p
-       defn i eo
-       return a
-
-letn' :: Env e => Id -> Clos Type -> Eval e a -> Eval e a
-letn' i t p = letn i (Closure t) p
-
-subst :: Env e => Bind (Clos Term) -> (Clos Term) -> Eval e (Clos Term)
-subst (x,(t,s)) u =
-    do (i,s') <- decl' x s
-       defn' i u    
-       return (t,s')
-
-evalApp :: Env e => Val -> (Clos Term) -> Eval e Val
-evalApp (VLam xt) u = subst xt u >>= eval
-evalApp (Ne t)    u = return (Ne (t :.. u))
-evalApp _         _ = fail "function expected"
-
-lookupId :: Env e => Id -> Eval e EnvEntry
-lookupId i = liftM (flip getE i) getEnv
-
-evalId :: Env e => Id -> Eval e Val
-evalId i =
-    do ei <- lookupId i
-       case ei of
-         Closure t -> eval t
-         Id j      -> return (Ne (NVar j))
-
--- use subst!
-evalSplit :: Env e => Val -> (Bind (Bind (Clos Term))) ->
-             Eval e Val
-evalSplit (VPair ((l,r),s)) (x,(y,(t,s'))) = 
-    do (x',s2) <- decl' x s'
-       (y',s3) <- decl' y s2
-       defn' x' (l,s)
-       defn' y' (r,s)
-       eval (t,s3)
-
-evalSplit (Ne n) (xy,t) = return (Ne (NSplit n (xy,t)))
-evalSplit _ _ = fail "Pair expected"
-
-evalCase :: Env e => Val -> Clos [(Label,Term)] -> Eval e Val
-evalCase (VLabel l) (lts,s) = 
-    case lookup l lts of
-      Nothing -> fail "case not matched"
-      Just t  -> eval (t,s)
-evalCase (Ne n) lts = return (Ne (NCase n lts))
-evalCase _ _ = fail "Label expected"
-
-force :: Env e => Val -> Eval e Val
-force (VBox (Boxed c)) = eval c
-force (Ne n) = return (Ne (NForce n))
-force _ = fail "Box expected"
-
-eval :: Env e => (Clos Term) -> Eval e Val
-eval (Var x, s)     = getId x s >>= evalId
-eval (Let g t, s)   = evalProg (g,s) >>= curry eval t
-eval (Type,s)       = return VType
-eval (Q ps axb,s)   = return (VQ ps (axb,s))
-eval (Lift t,s)     = return (VLift (t,s))
-eval (Lam (x,t), s) = return (VLam (x,(t,s)))
-eval (t :. u ,s)    = eval (t,s) >>= flip evalApp (u,s)
-eval (Pair tu,s)    = return (VPair (tu,s))
-eval (Split t (x,(y,u)),s)
-                    = eval (t,s) >>= flip evalSplit (x,(y,(u,s)))
-eval (Enum ls,s)    = return (VEnum ls)
-eval (Label l,s)    = return (VLabel l)
-eval (Case t lts,s) = eval (t,s) >>= flip evalCase (lts,s)
-eval (Box t,s)      = return (VBox (Boxed (t,s)))
-eval (Force t,s)    = eval (t,s) >>= force
-
-
--- forced eval (should be integrated into eval?)
-feval :: Env e => (Clos Term) -> Eval e Val
-feval t = do t' <- eval t
-             case t' of 
-               VBox (Boxed u) -> feval u
-               v -> return v
-
-               
-
-evalProg :: Env e => Clos Prog -> Eval e Scope
-evalProg ([],s) = return s
-evalProg ((Decl x _):tel, s) = do (_,s') <- decl x (PrtInfo x False) s Nothing
-                                  evalProg (tel,s')
-evalProg ((Defn x t):tel, s) = do i <- getId x s
-                                  defn' i (t,s)
-                                  evalProg (tel,s)
diff --git a/src/PiSigma/Nf.hs b/src/PiSigma/Nf.hs
deleted file mode 100644
--- a/src/PiSigma/Nf.hs
+++ /dev/null
@@ -1,111 +0,0 @@
-{-# LANGUAGE UndecidableInstances, MultiParamTypeClasses, FunctionalDependencies,
-             TypeSynonymInstances, FlexibleInstances #-}
-module PiSigma.Nf where
-
-{- Implementation of a normalisation function.
-   Useful for testing.
--}
-
-import Control.Monad
-
-import PiSigma.Syntax
-import PiSigma.Evaluation
-
-type Vars = [String]
-
-fresh :: Name -> Vars -> Name
-fresh x xs = if x/="" && elem x xs then fresh (x++"'") xs
-             else x
-
-class Nf a b | a -> b where
-    nf :: Env e => Vars -> a -> Eval e b
-    nf = nf' True
-    quote :: Env e => Vars -> a -> Eval e b
-    quote = nf' False
-    nf' :: Env e => Bool -> Vars -> a -> Eval e b
-
-
-instance Nf (Clos Term) Term where
-    nf' True xs t = do t' <- eval t
-                       nf' True xs t'
-    nf' False xs t = qq xs t
-
-instance Nf Id Term where
-    nf' b xs i = do e <- getEnv
-                    let (PrtInfo x exp) = prtE e i
-                    case getE e i of
-                      (Id _) -> return (Var x) 
-                      (Closure t) -> if exp then nf' b xs t
-                                     -- this is bad, we should not
-                                     -- expand inside a box!
-                                     else return (Var x) 
-
-qq :: Env e => Vars -> Clos Term -> Eval e Term
-qq xs (Var x,s) = do i <- getId x s
-                     quote xs i
-qq xs (Let g t, s) = fail "quote let: not implemented!"
-{-do s' <- evalProg (g,s)
-                        qq xs (t,s')  
-                       -- this seems wrong! we should return a Let
-                       -- and we should extend xs!
--}
-qq xs (Q ps (a,(x,b)),s) = 
-    do a' <- qq xs (a,s)
-       xb' <- quote xs (x,(b,s))
-       return (Q ps (a',xb'))
-qq xs (Lift t,s) = liftM Lift (qq xs (t,s))
-qq xs (Lam (x,t), s) = liftM Lam (quote xs (x,(t,s)))
-qq xs (t :. u ,s) = do t' <- qq xs (t,s)
-                       u' <- qq xs (u,s)
-                       return (t' :. u')
-qq xs (Pair (t,u),s) = do t' <- qq xs (t,s)
-                          u' <- qq xs (u,s)
-                          return (Pair (t',u'))
-qq xs (Split t (x,(y,u)),s) = do t' <- qq xs (t,s)
-                                 xyu' <- quote xs (x,(y,(u,s)))
-                                 return (Split t' xyu')
-qq xs (Case t lts,s) = do t' <- qq xs (t,s)
-                          lts' <- mapM (\ (l,t) -> 
-                                            do t' <- qq xs (t,s)
-                                               return (l,t')) lts
-                          return (Case t' lts')              
-qq xs (Box t,s) = liftM Box (qq xs (t,s))
-qq xs (Force t,s) = liftM Force (qq xs (t,s))
-qq xs (t,s) = return t -- Type, Enum, Label
-
-instance (Closure a,Nf a b) => Nf (Bind a) (Bind b) where
-    nf' b xs (x,t)  = do let x' = fresh x xs
-                         (i,s') <- decl x (PrtInfo x' True) (getScope t) Nothing
-                         t' <- nf' b (x':xs) (putScope t s')
-                         return (x',t')
-
-instance Nf Val Term where
-    nf' b xs (Ne n) = nf' b xs n
-    nf' b xs VType = return Type
-    nf' b xs (VQ ps ((a,(x,c)),s)) = do a' <- nf' b xs (a,s) 
-                                        xc' <- nf' b xs (x,(c,s))
-                                        return (Q ps (a',xc'))
-    nf' b xs (VLift c) = liftM Lift (nf' b xs c)
-    nf' b xs (VLam xt) = liftM Lam (nf' b xs xt)
-    nf' b xs (VPair ((t,u),s)) = do t' <- nf' b xs (t,s)
-                                    u' <- nf' b xs (u,s)
-                                    return (Pair (t',u'))
-    nf' b xs (VBox (Boxed c)) = liftM Box (nf' False xs c)
-    nf' b xs (VEnum ls) = return (Enum ls)
-    nf' b xs (VLabel l) = return (Label l)
-
-
-instance Nf Ne Term where
-    nf' b xs (NVar i) = nf' b xs i
-    nf' b xs (t' :.. u) = do t <- nf' b xs t'
-                             u' <- nf' b xs u
-                             return (t :. u')
-    nf' b xs (NSplit t xyu) = do t' <- nf' b xs t
-                                 xyu' <- nf' b xs xyu
-                                 return (Split t' xyu')
-    nf' b xs (NCase t (lus,s)) = do t' <- nf xs t
-                                    lus' <- mapM (\ (l,u) -> 
-                                                   do u' <- nf' b xs (u,s)
-                                                      return (l,u')) lus
-                                    return (Case t' lus')
-    nf' b xs (NForce t) = liftM Force (nf xs t)
diff --git a/src/PiSigma/Parser.hs b/src/PiSigma/Parser.hs
deleted file mode 100644
--- a/src/PiSigma/Parser.hs
+++ /dev/null
@@ -1,141 +0,0 @@
-module PiSigma.Parser (module PiSigma.Parser, Parser) where
-
-import Prelude hiding (pi)
-import Data.Char
-import Data.List
-
-import Control.Monad
-import Control.Applicative hiding ((<|>), many)
-
-import Text.ParserCombinators.Parsec as P hiding (token, label)
-
-import PiSigma.Syntax hiding (label)
-
-type SParser = CharParser ()
-
--- * Comments and whitespace
-
-blockComment :: SParser ()
-blockComment = () <$ try (string "{-") <* inComment <* string "-}"
-
-inComment :: SParser ()
-inComment =
-  () <$ many (choice [ () <$ noneOf "{-"
-                     , try $ () <$ char '-' <* notFollowedBy (char '}')
-                     , try $ () <$ char '{' <* notFollowedBy (char '-')
-                     , blockComment ])
-
-lineComment :: SParser ()
-lineComment = () <$ try (string "--") <* many (noneOf "\n")
-
-whiteSpace :: SParser ()
-whiteSpace = () <$ spaces <* many ((lineComment <|> blockComment) <* spaces)
-             <?> ""
-
--- * Identifiers
-
-identChar :: SParser Char
-identChar = alphaNum <|> oneOf "_'"
-
-ident :: SParser String
-ident = 
-  (try $  do
-            xs <- (:) <$> letter <*> many identChar <* whiteSpace
-            guard (xs `notElem` keywords)
-            return xs) <?> "identifier"
-
-keywords :: [String]
-keywords = [ "case", "of", "let", "in", "split", "Type", "with" ]
-
-label :: SParser Name
-label = char '\'' *> ident
-
--- * Tokens
-
-token :: String -> SParser String
-token xs = (try $ (string xs <* whiteSpace)) <?> show xs
-
--- * Brackets
-
-parensed   = between (token "(") (token ")")
-braced     = between (token "{") (token "}")
-bracketed  = between (token "[") (token "]")
-
--- * Terms
-
-sTerm5 :: SParser Term
-sTerm5 =
-       Type   <$  token "Type"
-  <|>  (Enum  <$> braced (many ident) <?> "enumeration")
-  <|>  Case   <$  token "case" <*> sTerm <* token "of"
-              <*> braced (sBranch `sepBy` token "|")
-  <|>  (Label <$> label <?> "label")
-  <|>  (Box   <$> bracketed sTerm <?> "box")
-  <|>  (Lift  <$  token "^" <*> sTerm5 <?> "'^'")
-  <|>  Var    <$> ident
-  <|>  parensed sTerm
-
-sTerm4 :: SParser Term
-sTerm4 =
-       try (parensed (curry Pair <$> sTerm <* token "," <*> sTerm))
-  <|>  sTerm5
-
-sTerm3 :: SParser Term
-sTerm3 =
-       try (parensed (sigmas <$> many1 ident <* token ":" <*> sTerm) <* token "*")
-          <*> sTerm3
-  <|>  Force <$  token "!" <*> sTerm4
-  <|>  foldl1 (:.) <$> many1 sTerm4
-
-sTerm2 :: SParser Term
-sTerm2 =
-       foldl1 (-*-) <$> sTerm3 `sepBy1` token "*"
-
--- TODO: make more beautiful or renumber
-sTerm1b :: SParser Term
-sTerm1b =
-       try (parensed (pis <$> many1 ident <* token ":" <*> sTerm) <* token "->")
-          <*> sTerm
-  <|>  sTerm2
-       
-sTerm1 :: SParser Term
-sTerm1 =
-       flip ($) <$> sTerm1b <*> option id (flip (->-) <$ token "->" <*> sTerm)
-
-sTerm :: SParser Term
-sTerm =
-       lam   <$  token "\\" <*> many ident <* token "->" <*> sTerm
-  <|>  split <$  token "split" <*> sTerm <* token "with"
-             <*  token "(" <*> ident <* token "," <*> ident <* token ")"
-             <*  token "->" <*> sTerm
-  <|>  Let   <$  token "let" <*> sProg <* token "in" <*> sTerm
-  <|>  sTerm1
-
-sProg :: SParser Prog
-sProg = concat <$> (sEntry `sepEndBy` token ";")
-
-sEntry :: SParser [Entry]
-sEntry = 
-    do
-      n <- ident
-      b <- (True <$ token ":" <|> False <$ token "=")
-      t <- sTerm
-      if b
-        then do
-               d <- option Nothing (Just <$ token "=" <*> sTerm)
-               case d of
-                 Nothing -> return [Decl n t]
-                 Just t' -> return [Decl n t, Defn n t']
-        else return [Defn n t]
-
-sBranch :: SParser (Label,Term)
-sBranch = (,) <$> ident <* token "->" <*> sTerm
-
-sPhrase :: SParser Phrase
-sPhrase =
-       (try $ Prog <$> sProg <* eof) <|> Term <$> sTerm <* eof
-
-s2Terms :: SParser (Term, Term)
-s2Terms = (,) <$> sTerm5 <*> sTerm5
-
-parse p = P.parse (whiteSpace *> p <* eof)
diff --git a/src/PiSigma/Print.hs b/src/PiSigma/Print.hs
deleted file mode 100644
--- a/src/PiSigma/Print.hs
+++ /dev/null
@@ -1,108 +0,0 @@
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE FlexibleInstances    #-}
-module PiSigma.Print where
-
-import Control.Monad
-
-import Text.PrettyPrint.ANSI.Leijen
-
-import PiSigma.Syntax
-import PiSigma.Evaluation
-import PiSigma.Nf
-
--- * Print class for various types
-
-class Print a where
-    prt :: Env e => a -> Eval e String
-
-instance Print Val where
-    prt a = quote [] a >>= prt
-
-instance Print (Clos Term) where
-    prt a = quote [] a >>= prt
-
-instance Print Ne where
-    prt a = quote [] a >>= prt
-
-instance Print Term where
-    prt a = return (displayS (renderPretty 0.8 75 (pretty a)) "")
-
-
-data Msg = V Val | C (Clos Term) | T Term | S String
-
-instance Print Msg where
-    prt (V v) = prt v
-    prt (C c) = prt c
-    prt (T t) = prt t
-    prt (S s) = return s
-
-failp :: (Print a, Env e) => [a] -> Eval e b
-failp ps = do msg <- foldM (\ msg p -> do s <- prt p
-                                          return (msg++s)) "" ps
-              fail msg
-
--- * Pretty printer for terms
-
--- | Context for printing. Determines whether parentheses are
--- required.
-type PrintContext = Int
-
-prettyTerm :: PrintContext -> Term -> Doc
-prettyTerm _ (Var x)        = text x
-prettyTerm _ (Let p t)      = pretty p <> pretty t
-prettyTerm _ Type           = text "Type"
-prettyTerm c (Q Pi (t1,(n,t2))) =
-  contextParens c 1 $
-  group (binding 2 n t1 <$> text "->" <+> prettyTerm 1 t2)
-prettyTerm c (Q Sigma (t1,(n,t2))) =
-  contextParens c 2 $
-  binding 2 n t1 <+> text "*" <+> prettyTerm 3 t2
-prettyTerm _ (Lam (n,t))    =
-  text "\\" <+> text n <+> text "->" <+> prettyTerm 0 t
-prettyTerm c (t1 :. t2)     =
-  group (hang 2 (contextParens c 3 (prettyTerm 3 t1 <$> prettyTerm 4 t2)))
-prettyTerm c (Pair (t1,t2)) =
-  tupled (map (prettyTerm 0) [t1,t2])
-prettyTerm _ (Split t1 (n1,(n2,t2))) =
-  hang 2 (text "split" <+> prettyTerm 0 t1 <+> text "with"
-            <+> parens (text n1 <> comma <> text n2)
-            <+> text "->" <$> prettyTerm 0 t2)
-prettyTerm _ (Enum ls)      = braces (sep (map text ls))
-prettyTerm _ (Label l)      = text ('\'' : l)
-prettyTerm _ (Case t bs)    =
-  hang 2 (text "case" <+> prettyTerm 0 t <+> text "of" <$> branches bs)
-prettyTerm c (Lift t)       =
-  contextParens c 5 $
-  text "^" <> prettyTerm 5 t
-prettyTerm _ (Box t)        =
-  brackets (prettyTerm 0 t)
-prettyTerm c (Force t)      =
-  contextParens c 3 $
-  text "!" <> prettyTerm 4 t
-
-prettyEntry :: Entry -> Doc
-prettyEntry (Defn n t)      =
-  hang 2 (text n <+> text "=" <$> prettyTerm 0 t <> text ";")
-prettyEntry (Decl n t)      =
-  hang 2 (text n <+> text ":" <$> prettyTerm 0 t <> text ";")
-
-binding :: PrintContext -> String -> Term -> Doc
-binding c "" t = prettyTerm c t
-binding _ n  t = parens (text n <+> colon <+> prettyTerm 0 t)
-
-branches :: [(Label,Term)] -> Doc
-branches bs = encloseSep lbrace rbrace (text "|") (map branch bs)
-  where branch (n,t) = text n <+> text "->" <+> prettyTerm 0 t
-
--- | Prints parens if the current context is higher
--- than a certain limit.
-contextParens :: PrintContext -> PrintContext -> Doc -> Doc
-contextParens c d p | c > d     = parens p
-                    | otherwise = p
-
-instance Pretty Term where
-  pretty = prettyTerm 0
-
-instance Pretty Entry where
-  pretty = prettyEntry
-
diff --git a/src/PiSigma/Syntax.hs b/src/PiSigma/Syntax.hs
deleted file mode 100644
--- a/src/PiSigma/Syntax.hs
+++ /dev/null
@@ -1,234 +0,0 @@
-{-# LANGUAGE TypeSynonymInstances #-}
-module PiSigma.Syntax where
-
-import Prelude hiding (pi)
-
--- * Abstract syntax
-
-data Phrase = Prog Prog | Term Term
-  deriving (Show,Eq)
-
-type Name = String
-
-type Label = String
-
-data Entry = Decl Name Type | Defn Name Term
-  deriving (Show,Eq)
-
-type Prog = [Entry]
-
-{-
-Maybe better
-data Prog = Decl Type (Bind Prog) | Defn Name Term Prog
--}
-
-type Type = Term
-
--- | The use of Bind indicates the scope of the
--- bound identifier.
-type Bind a = (Name,a)
-
--- | For treating quantifiers in a uniform way.
-data PiSigma = Pi | Sigma
-  deriving (Show,Eq)
-
-data Term =
-    Var   String
-  | Let   Prog Term
-  | Type
-  | Q     PiSigma (Type,Bind Type)
-  | Lam   (Bind Term)
-  | Term :. Term
-  | Pair  (Term,Term)
-  | Split Term (Bind (Bind Term)) -- split t with (x,y) -> u
-  | Enum  [Label]
-  | Label Label
-  | Case  Term [(Label,Term)]     -- case t of { L -> u }
-  | Lift  Term
-  | Box   Term
-  | Force Term
-  deriving (Show,Eq)
-
--- * Smart constructors
-
--- | Smart constructor for lambda abstractions.
-lam :: [Name] -> Term -> Term
-lam []     t = t
-lam (x:xs) t = Lam (x,lam xs t)
-
--- | Smart constructor for split.
-split :: Term -> Name -> Name -> Term -> Term
-split t1 x y t2 = Split t1 (x,(y,t2))
-
--- | Smart constructor for quantifiers.
-q :: PiSigma -> [(Name,Type)] -> Type -> Type
-q ps []          b = b
-q ps ((x,a):xas) b = Q ps (a,(x,q ps xas b))
-
--- | Smart constructor for multiple Pi applications.
-pis' :: [(Name,Type)] -> Type -> Type
-pis'    = q Pi
-
--- | Smart constructor for multiple Pi applications.
-pis :: [Name] -> Type -> Type -> Type
-pis ns t = pis' (map (\ n -> (n,t)) ns)
-
--- | Smart constructor for Pi.
-pi :: Name -> Type -> Type -> Type
-pi n t = pis' [(n,t)]
-
--- | Smart constructor for multiple Sigma applications.
-sigmas' :: [(Name,Type)] -> Type -> Type
-sigmas' = q Sigma
-
--- | Smart constructor for multiple Sigma applications.
-sigmas :: [Name] -> Type -> Type -> Type
-sigmas ns t = sigmas' (map (\ n -> (n,t)) ns)
-
--- | Smart constructor for Sigma.
-sigma :: Name -> Type -> Type -> Type
-sigma n t = sigmas' [(n,t)]
-
--- | Smart constructor for function space.
-(->-) :: Type -> Type -> Type
-(->-) = pi ""
-
--- | Smart constructor for product.
-(-*-) :: Type -> Type -> Type
-(-*-) = sigma ""
-
--- * Values (well-scoped WHNFs) and environments
-
--- ** Identifiers
-
-type Id = Int -- index in (potentially multiple) environments
-
--- ** Scopes
-
-data Scope = Scope [(Name,(Id,Maybe (Clos Type)))]
-  deriving (Show,Eq)
-
-{-
-
-TODO:
-
-Perhaps return to the following types for scopes:
-
-data Sc a = Scope [(Name,(Id, a))]
-
-type Scope = Sc ()
-type Ctx   = Sc (Clos Type)
-
-We then need a forgetful mapping:
-
-fog :: Ctx -> Scope
-fog c = map (\ (x,(i,a)) -> (x,(i,()))) c 
-
-Alternatively, we can try to make Scopes
-existential, essentially:
-
-type Scope = exists a. Sc a
-
--}
-
-emptyScope :: Scope
-emptyScope = Scope []
-
-extendScope :: Scope -> Name -> (Id,Maybe (Clos Type)) -> Scope
-extendScope (Scope s) x (i,a) = Scope ((x,(i,a)) : s)
-
-lookupScope :: Scope -> Name -> Maybe Id
-lookupScope (Scope s) x = do (i,_) <- lookup x s
-                             return i
-
-lookupCon :: Scope -> Name -> Maybe (Clos Type)
-lookupCon (Scope s) x = do (_,Just a) <- lookup x s
-                           return a
-
--- ** Closures
-
-type Clos a = (a,Scope)
-
---type C a = (Con,a)
-
---c2clos :: C a -> Clos a
---c2clos (g,a) = (a,fog g)
-
--- fix order, name of C...
-
-class Closure a where 
-    getScope :: a -> Scope
-    putScope :: a -> Scope -> a
-
-instance Closure (Clos a) where
-    getScope (_,s)   = s
-    putScope (a,_) s = (a,s)
-
-instance Closure a => Closure (Bind a) where
-    getScope (_,a)   = getScope a
-    putScope (x,a) s = (x,putScope a s)
-
-instance Closure Boxed where
-    getScope (Boxed c)   = getScope c
-    putScope (Boxed c) s = Boxed (putScope c s)
-
-{- could be used to refactor the code using bindings. -}
-
-ty :: Clos Type
-ty = (Type,emptyScope)
-
-label :: String -> Clos Term
-label s = (Label s,emptyScope)
-
-type VType = Val
-
-newtype Boxed = Boxed (Clos Term) deriving (Show,Eq)
-
--- ** Values
-
-data Val =
-    Ne Ne
-  | VType 
-  | VQ PiSigma (Clos (Type,Bind Type))
-  | VLift (Clos Type)
-  | VLam (Bind (Clos Term))
-  | VPair (Clos (Term, Term))
-  | VEnum [Label]
-  | VLabel Label 
-  | VBox Boxed
-  deriving (Show,Eq)
-
--- | Neutral terms.
-data Ne =
-    NVar Id
-  | Ne :.. (Clos Term)
-  | NSplit Ne (Bind (Bind (Clos Term)))
-  | NCase Ne (Clos [(Label,Term)])
-  | NForce Ne
-  deriving (Show,Eq)
-
--- ** Environments
-
-data EnvEntry = Id Id | Closure (Clos Term) deriving Show
-
-data PrtInfo = PrtInfo {name :: Name, expand :: Bool}
-
-class Env e where 
-    emptyE :: e
-    extE   :: e -> PrtInfo -> (Id,e)
-    setE   :: e -> Id -> EnvEntry -> e
-    getE   :: e -> Id -> EnvEntry
-    prtE   :: e -> Id -> PrtInfo
-
-set :: [a] -> Int -> a -> [a]
-set (a:as) 0 b = b:as
-set (a:as) i b = a:set as (i-1) b
- 
-type EnvEntries = [(EnvEntry,PrtInfo)]
-
-instance Env EnvEntries where
-    emptyE     = []
-    extE e x   = let i = length e in (i,e++[(Id i,x)])
-    setE e i v = let (_,x) = e!!i in set e i (v,x)
-    getE e i   = let (v,_) = e!!i in v
-    prtE e i   = let (_,x) = e!!i in x
diff --git a/src/Tools/Interpreter/Main.hs b/src/Tools/Interpreter/Main.hs
new file mode 100644
--- /dev/null
+++ b/src/Tools/Interpreter/Main.hs
@@ -0,0 +1,15 @@
+module Main where
+
+import System.Environment
+
+import Tools.Interpreter.REPL
+
+main :: IO ()
+main = 
+  do
+    args <- getArgs
+    let ini = mapM_ (handleCommand . Load) args
+    runREPL (handleCommand Startup >> ini >> repl)
+
+-- TODO: better command line arg handling; allow non-interactive mode
+
diff --git a/src/Tools/Interpreter/REPL.hs b/src/Tools/Interpreter/REPL.hs
new file mode 100644
--- /dev/null
+++ b/src/Tools/Interpreter/REPL.hs
@@ -0,0 +1,356 @@
+{-# OPTIONS_GHC -fno-warn-orphans          #-}
+{-# LANGUAGE    GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE    OverloadedStrings          #-}
+{-# LANGUAGE    ScopedTypeVariables        #-}
+
+module Tools.Interpreter.REPL
+  ( REPL (..)
+  , REPLCommand (..)
+  , handleCommand
+  , repl
+  , runREPL )
+  where
+
+import Prelude hiding (catch)
+import Control.Monad.Error
+import Control.Monad.State
+import Control.Monad.Trans
+import Data.Char
+import qualified Data.List as List
+import System.Console.Haskeline.Class
+import System.IO
+import Data.Version (showVersion)
+
+import Language.PiSigma.Check
+import Language.PiSigma.Equality
+import Language.PiSigma.Evaluate
+import Language.PiSigma.Lexer
+  as Lexer
+    ( Parser )
+import Language.PiSigma.Normalise
+import Language.PiSigma.Parser
+import Language.PiSigma.Pretty
+import Language.PiSigma.Syntax
+import qualified Language.PiSigma.Util.String.Internal
+  as Internal
+import qualified Language.PiSigma.Util.String.Parser
+  as Parser
+
+import Paths_pisigma
+
+-- * Instances needed for newtype deriving
+
+instance (Error e, MonadException m) => MonadException (ErrorT e m) where
+  catch m = ErrorT . catch (runErrorT m) . (runErrorT .)
+  block   = mapErrorT block
+  unblock = mapErrorT unblock
+
+instance (Error e, MonadHaskeline m) => MonadHaskeline (ErrorT e m) where
+  getInputLine = lift . getInputLine
+  getInputChar = lift . getInputChar
+  outputStr    = lift . outputStr
+  outputStrLn  = lift . outputStrLn
+
+-- * Types
+
+-- | The REPL monad has exceptions, a line editor with history using
+-- Haskeline, and state.
+newtype REPL a = REPL { unREPL :: ErrorT REPLError (HaskelineT (StateT REPLState IO)) a }
+  deriving ( Monad
+           , MonadException
+           , MonadError REPLError
+           , MonadHaskeline
+           , MonadIO
+           , MonadState REPLState )
+
+-- | The state currently keeps track of identifiers defined and their
+-- types, as well as a list of files currently loaded.
+data REPLState =
+  REPLState
+    { replState :: (Scope, EnvEntries)
+    , replFiles :: [FilePath]
+    }
+
+-- TODO: Add a search path and verbosity options.
+
+-- ** Commands
+
+-- | Commands that can be entered at the REPL prompt.
+data REPLCommand =
+    Load String
+  | Reload
+  | Quit
+  | EvalPhrase Phrase
+  | Noop
+  | Clear
+  | Equal (Term,Term)
+  | TypeOf Term
+  | Help
+  | Browse
+  | Startup
+  | Version
+
+-- ** Errors
+
+-- | Normal Errors abort the current command but do not quit the REPL.
+-- If we actually wish to quit, we can throw a Terminate error.
+data REPLError =
+    Error
+  | Terminate
+
+instance Error REPLError where
+  noMsg    = Error
+  strMsg _ = Error
+
+-- * REPL monad
+
+initialREPLState :: REPLState
+initialREPLState = 
+  REPLState (emptyScope, emptyE) []
+
+runREPL :: REPL () -> IO ()
+runREPL r =
+  do
+    runStateT (runHaskelineT (setComplete pisigmaCompletion defaultSettings)
+                         (runErrorT (unREPL r)))
+              initialREPLState
+    return ()
+
+-- * Haskeline
+
+-- | 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" `List.isPrefixOf` List.reverse x1 = completeFilename (x1, x2)
+  | otherwise                              = completeWord Nothing " " identifier (x1, x2)
+  where
+    identifier :: String -> StateT REPLState IO [Completion]
+    identifier x = do
+      (Scope sc, _) <- gets replState
+      let names = map fst sc
+          cands = filter (Internal.fromString x `Internal.isPrefixOf`) names
+      return $ map (simpleCompletion . Internal.toString) (List.sort cands)
+
+-- * Help
+
+-- | Preliminary interpreter help message.
+help :: String
+help = List.unlines
+  [ "PiSigma currently supports the following commands:"
+  , ""
+  , "  :l         load a source file"
+  , "  :r         reload current source file"
+  , "  :b         browse current identifiers"
+  , "  :c         clear the environment"
+  , "  :t         ask for the type of a term"
+  , "  :e         test two terms for beta equality"
+  , "  :v         version"
+  , "  :q         quit"
+  , ""
+  , "Type a declaration or an expression to evaluate it."
+  ]
+
+-- * REPL core
+
+-- | Performs a single REPL step. Print prompt, read input,
+-- dispatch.
+replStep :: REPL ()
+replStep =
+  do
+    f <- gets replFiles
+    x <- getInputLine (List.unwords (List.reverse f) ++ "> ")
+    c <- interpretInput (fmap id x)
+    handleCommand c
+
+-- | Run the interpreter as long as desired.
+repl :: REPL ()
+repl =
+  do
+    catchError replStep
+      (\ e -> case e of
+                Error      ->  return ()
+                Terminate  ->  throwError Terminate)
+    repl
+
+-- * Command handling
+
+-- | 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" `List.isPrefixOf` x = return $ Load $ norm $ strip xArg
+  | ":r" `List.isPrefixOf` x = return Reload
+  | ":b" `List.isPrefixOf` x = return Browse
+  | ":q" `List.isPrefixOf` x = return Quit
+  | ":c" `List.isPrefixOf` x = return Clear
+  | ":e" `List.isPrefixOf` x = parseInputInteractive s2Terms Equal  xArg
+  | ":t" `List.isPrefixOf` x = parseInputInteractive sTerm   TypeOf xArg
+  | ":h" `List.isPrefixOf` x
+ || ":?" `List.isPrefixOf` x = return Help
+  | ":v" `List.isPrefixOf` x = return Version
+  | ":"  `List.isPrefixOf` x = replMessage "unknown command" >> return Noop
+  | otherwise                = parseInputInteractive sPhrase EvalPhrase x
+  where
+    norm  :: String -> String
+    norm []              = []
+    norm ('\\' : c : xs) = c : norm xs
+    norm (       c : xs) = c : norm xs
+
+    strip :: String -> String
+    strip                = List.reverse
+                         . List.dropWhile isSpace
+                         . List.reverse
+                         . List.dropWhile isSpace
+
+    xArg  :: String
+    xArg                 = snd $ break (== ' ') x
+
+-- | Turn a string into a REPL command.
+parseInput :: FilePath
+           -> Parser t
+           -> (t -> REPLCommand)
+           -> Parser.String
+           -> REPL REPLCommand
+parseInput f p cmd s =
+    case parse p f s of
+      Left err   -> do
+        replMessage $ "Parse error: " ++ (show) err ++ "\n"
+        return Noop
+      Right p'   -> return (cmd p')
+
+parseInputInteractive :: Parser t
+                      -> (t -> REPLCommand)
+                      -> String
+                      -> REPL REPLCommand
+parseInputInteractive p cmd = parseInput "<interactive>" p cmd . Parser.fromString
+
+-- | Command handler. Returns a flag indicating whether
+-- the interpreter should continue.
+handleCommand :: REPLCommand -> REPL ()
+handleCommand c =
+  case c of
+    Version-> replMessage $ "PiSigma version " ++ showVersion version
+    Startup-> handleCommand Version >> replMessage "Type :? for help."
+    Help   -> replMessage help
+    Load f ->
+      do
+        fs <- gets replFiles
+        if f `elem` fs then
+            replMessage $ "Skipping " ++ f ++ "."
+          else do
+            mx <- liftIO $ liftM (Just) (Parser.readFile f)
+                    `catch` (\ (_ :: IOException) -> return Nothing)
+            case mx of
+              Nothing -> do
+                replMessage $ "Could not find " ++ f ++ "."
+                throwError Error
+              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 spanP s      = case Parser.uncons s of
+                                     Just (':', _) -> True
+                                     _             -> False
+                    (cmds, rest) = List.span spanP $ Parser.lines x
+                mapM_ (\ c' -> handleCommand =<< (interpretInput . Just . Parser.toString) c') cmds
+                p <- parseInput f sProg (EvalPhrase . Prog)
+                                (Parser.unlines (List.replicate (List.length cmds) "" ++ rest))
+                handleCommand p
+                modify (\ s -> s { replFiles =
+                                            case replFiles s of
+                                             (g : fs') | g == f -> g : fs'
+                                             xs                 -> f : xs })
+                -- We print the "Loaded" message after executing initial
+                -- interpreter commands in order to reflect the dependency
+                -- order of different source files.
+                replMessage $ "Loaded " ++ f ++ "."
+    Reload ->
+      do
+        f <- gets replFiles
+        handleCommand Clear
+        mapM_ (handleCommand . Load) (List.reverse f)
+    Browse ->
+      do
+        (Scope sc, _) <- gets replState
+        let names :: [Pretty]
+            names = map (text . Seq . fst) sc
+        liftIO $ putPretty $ vcat names
+        liftIO $ putStrLn ""
+    Quit ->
+      throwError Terminate
+    EvalPhrase (Prog p) ->
+      execProg p
+    EvalPhrase (Term t) ->
+      execTerm t
+    Equal (t1,t2) ->
+      eqTerms t1 t2
+    TypeOf t ->
+      inferTerm t
+    Clear ->
+      put initialREPLState
+    Noop ->
+      return ()
+
+-- ** Command handler helpers
+
+execProg :: Prog -> REPL ()
+execProg p =
+  do
+    s <- get
+    let (con,env) = replState s
+    case run env (checkProg (p,con)) of
+      Right s' -> put (s { replState = s' })
+      Left e   -> do
+                    liftIO $ Internal.putStrLn e
+                    throwError Error
+
+execTerm :: Term -> REPL ()
+execTerm t =
+  do
+    s <- get
+    let (con,env) = replState s
+        p = do
+          a  <- infer (t,con)
+          t' <- nf [] (t,con)
+          pa <- evalPrint a
+          pt <- evalPrint t'
+          return $ fromPretty $ pt <$> colon <+> align pa
+    case run env p of
+        Right (m,_) -> liftIO $ Internal.putStrLn m
+        Left e      -> do
+                         liftIO $ Internal.putStrLn e
+                         throwError Error
+
+eqTerms :: Term -> Term -> REPL ()
+eqTerms t1 t2 =
+  do
+    s <- get
+    let (con,env) = replState s
+        p = eq (t1,con) (t2,con)
+    case run env p of
+        Right _ -> liftIO $ putStrLn "yes"
+        Left e  -> do
+                     liftIO $ Internal.putStrLn e
+                     throwError Error
+    
+
+inferTerm :: Term -> REPL ()
+inferTerm t =
+  do
+    s <- get
+    let (con,env) = replState s
+        p = evalPrint =<< infer (t,con)
+    case run env p of
+        Right (m,_) -> do
+          liftIO $ putPretty m
+          liftIO $ putStrLn ""
+        Left e      -> do
+                         liftIO $ Internal.putStrLn e
+                         throwError Error
+
+-- | Placeholder for a message function that can depend
+-- on verbosity settings.
+replMessage :: String -> REPL ()
+replMessage = liftIO . putStrLn