35 files changed, 257 insertions, 188 deletions

diff --git a/README.md b/README.md
index 1d67821..ce6c1f8 100644
--- a/README.md
+++ b/README.md
@@ -28,7 +28,8 @@ not-function applied to `false` (which evaluates to `true`).
 
 - [x] figure out how to recover variable names in pretty-printing so we don't
   have to print de bruijn indices all the time
-- [ ] improve error messages and build a better repl
+- [x] build a better repl
+- [ ] improve error messages
 - [ ] implement top-level definitions
 - [ ] implement less aggrevating syntax for non-dependent function & pair types
 - [ ] add a type of natural numbers
diff --git a/bin/dune b/bin/dune
deleted file mode 100644
index 2e2f594..0000000
--- a/bin/dune
+++ /dev/null
@@ -1,5 +0,0 @@
-(executable
- (public_name toytt)
- (name main)
- (libraries toytt)
- (modes byte exe))
diff --git a/bin/main.ml b/bin/main.ml
deleted file mode 100644
index afae47c..0000000
--- a/bin/main.ml
+++ /dev/null
@@ -1,25 +0,0 @@
-open Toytt
-
-module Term = Asai.Tty.Make(Reporter.Message)
-
-let parse (s : string) : Ast.expr =
-  let lexbuf = Lexing.from_string s in
-  let string_source : Asai.Range.string_source = {
-    title = None;
-    content = s;
-  } in
-  let source = `String string_source in
-  ParserEff.Eff.run ~env:source @@ fun () ->
-  let ast = Parser.parse Lexer.lex lexbuf in
-  ast
-
-let rec repl () =
-  let input = read_line () in
-  let ast = parse input in
-  let (tp, tm) = Elab.infer_toplevel ast in
-  let value = Eval.eval ~env:Emp tm in
-  Format.printf "%a : %a\n%!" Syntax.Pretty.pp (Quote.quote ~size:0 value, Emp) Syntax.Pretty.pp (Quote.quote ~size:0 tp, Emp);
-  repl ()
-
-let () =
-  Reporter.run ~emit:Term.display ~fatal:Term.display @@ fun () -> repl ()
diff --git a/dune-project b/dune-project
index 0fa4b03..f3993f2 100644
--- a/dune-project
+++ b/dune-project
@@ -24,6 +24,7 @@
   asai
   bwd
   fmt
+  linenoise
   yuujinchou
  )
  (tags
diff --git a/lib/Eval.mli b/lib/Eval.mli
deleted file mode 100644
index 63c49cf..0000000
--- a/lib/Eval.mli
+++ /dev/null
@@ -1,2 +0,0 @@
-val eval : env:Domain.env -> Syntax.t -> Domain.t
-val inst_clo : Domain.clo -> Domain.t -> Domain.t
diff --git a/lib/ParserEff.ml b/lib/ParserEff.ml
deleted file mode 100644
index 84c0de8..0000000
--- a/lib/ParserEff.ml
+++ /dev/null
@@ -1 +0,0 @@
-module Eff = Algaeff.Reader.Make (struct type nonrec t = Asai.Range.source end)
diff --git a/lib/Quote.mli b/lib/Quote.mli
deleted file mode 100644
index 193b0b0..0000000
--- a/lib/Quote.mli
+++ /dev/null
@@ -1,2 +0,0 @@
-val quote : size:int -> Domain.t -> Syntax.t
-val quote_ne : size:int -> Domain.ne -> Syntax.t
diff --git a/lib/Syntax.ml b/lib/Syntax.ml
deleted file mode 100644
index fc58353..0000000
--- a/lib/Syntax.ml
+++ /dev/null
@@ -1,115 +0,0 @@
-open Bwd
-open Bwd.Infix
-
-type t = Data.syn =
-  | Var of int
-  | Pi of Ident.local * t * (* BINDS *) t
-  | Lam of Ident.local * (* BINDS *) t
-  | App of t * t
-  | Sg of Ident.local * t * (* BINDS *) t
-  | Pair of t * t
-  | Fst of t
-  | Snd of t
-  | Type
-  | Bool
-  | True
-  | False
-  | BoolElim of {
-      motive_var : Ident.local;
-      motive : (* BINDS *) t;
-      true_case : t;
-      false_case : t;
-      scrut : t;
-    }
-
-module Pretty =
-struct
-  module Internal =
-  struct
-    type env = {
-      names : Ident.local bwd;
-      prec : int;
-    }
-
-    module Eff = Algaeff.Reader.Make (struct type nonrec t = env end)
-
-    let bind (name : Ident.local) f fmt x =
-      let update env = { env with names = env.names <: name } in
-      Eff.scope update (fun () -> f fmt x)
-
-    let with_prec (prec : int) (inner : 'a Fmt.t) (fmt : Format.formatter) (v : 'a) =
-      Eff.scope (fun env -> { env with prec; }) (fun () -> inner fmt v)
-
-    let delimited inner = with_prec 0 inner
-
-    let parenthesize (prec : int) : 'a Fmt.t -> 'a Fmt.t =
-      if (Eff.read()).prec > prec then
-        Fmt.parens
-      else
-        Fun.id
-
-    let lassoc (prec : int)
-        (pp_left : 'l Fmt.t)
-        ?(sep = " ")
-        (pp_right : 'r Fmt.t) : ('l * 'r) Fmt.t = 
-      parenthesize prec @@ fun fmt v -> 
-      Fmt.pf fmt "@[%a@]%s@[%a@]" 
-        (with_prec prec pp_left) (fst v)
-        sep
-        (with_prec (prec + 1) pp_right) (snd v)
-
-    let rassoc (prec : int)
-        (pp_left : 'l Fmt.t)
-        ?(sep = " ")
-        (pp_right : 'r Fmt.t) : ('l * 'r) Fmt.t = 
-      parenthesize prec @@ fun fmt v -> 
-      Fmt.pf fmt "@[%a@]%s@[%a@]" 
-        (with_prec (prec + 1) pp_left) (fst v)
-        sep
-        (with_prec prec pp_right) (snd v)
-
-    let pp_local_name fmt name =
-      Fmt.string fmt @@ Option.value ~default:"_" name
-
-    let pp_var fmt ix =
-      let names = (Eff.read()).names in
-      match Bwd.nth_opt names ix with
-      (* the variable has a bound name which has not been shadowed *)
-      | Some ((Some name) as id) when Bwd.find_index ((=) id) names = Some ix -> Fmt.string fmt name
-      (* the variable does not have a bound name or its bound name has been shadowed *)
-      | Some _ -> Fmt.pf fmt "%@%d" ix
-      | None -> Reporter.bug "index out of range in pp_var"
-
-    let rec pp_pair fmt = (delimited @@ fun fmt (a, b) -> Fmt.pf fmt "@[(@[%a@], @[%a@])@]" pp a pp b) fmt
-
-    and pp_bool_elim fmt =
-      (delimited @@ fun fmt (motive_var, motive, true_case, false_case, scrut) -> Fmt.pf fmt
-         "@[bool-elim @[%a@] at @[%a@] -> @[%a@] [ true => @[%a@], false => @[%a@] ]@]"
-         pp scrut pp_local_name motive_var (bind motive_var pp) motive pp true_case pp false_case
-      ) fmt
-
-    and pp_arg fmt (name, tp) =
-      Fmt.pf fmt "(@[%a@] : @[%a@])" pp_local_name name pp tp
-
-    (* TODO: improve indentation *)
-    and pp fmt = function
-      | Var ix -> pp_var fmt ix
-      | Pi (name, base, fam) -> rassoc 1 pp_arg ~sep:" -> " (bind name pp) fmt ((name, base), fam)
-      | Lam (name, body) -> Fmt.pf fmt "@[\\@[%a@] -> @[%a@]@]" pp_local_name name (bind name pp) body
-      | Sg (name, base, fam) -> rassoc 2 pp_arg ~sep:" * " (bind name pp) fmt ((name, base), fam)
-      | App (a, b) -> lassoc 3 pp pp fmt (a, b)
-      | Pair (a, b) -> pp_pair fmt (a, b)
-      | Fst a -> lassoc 3 Fmt.string pp fmt ("fst", a)
-      | Snd a -> lassoc 3 Fmt.string pp fmt ("snd", a)
-      | Type -> Fmt.string fmt "type"
-      | Bool -> Fmt.string fmt "bool"
-      | True -> Fmt.string fmt "true"
-      | False -> Fmt.string fmt "false"
-      | BoolElim { motive_var; motive; true_case; false_case; scrut }
-        -> pp_bool_elim fmt (motive_var, motive, true_case, false_case, scrut)
-  end
-
-  let pp fmt (tm, names) =
-    let env : Internal.env = { names; prec = 0; } in
-    Internal.Eff.run ~env (fun () -> Internal.pp fmt tm)
-end
diff --git a/lib/dune b/lib/dune
deleted file mode 100644
index 3d2f366..0000000
--- a/lib/dune
+++ /dev/null
@@ -1,10 +0,0 @@
-(menhir
- (explain true)
- (modules Parser))
-
-(ocamllex Lexer)
-
-(library
- (name toytt)
- (libraries asai fmt yuujinchou)
- (preprocess (pps ppx_deriving.std)))
diff --git a/lib/Ast.ml b/src/ast/Ast.ml
index 1a1d4c5..1a1d4c5 100644
--- a/lib/Ast.ml
+++ b/src/ast/Ast.ml
diff --git a/src/ast/dune b/src/ast/dune
new file mode 100644
index 0000000..072fe89
--- /dev/null
+++ b/src/ast/dune
@@ -0,0 +1,4 @@
+(library
+ (name Ast)
+ (public_name toytt.ast)
+ (libraries asai toytt.ident))
diff --git a/src/bin/dune b/src/bin/dune
new file mode 100644
index 0000000..980d799
--- /dev/null
+++ b/src/bin/dune
@@ -0,0 +1,11 @@
+(executable
+ (public_name toytt)
+ (name main)
+ (libraries
+  asai
+  linenoise
+  toytt.elaborator
+  toytt.nbe
+  toytt.parser
+  toytt.reporter
+  ))
diff --git a/src/bin/main.ml b/src/bin/main.ml
new file mode 100644
index 0000000..f762d26
--- /dev/null
+++ b/src/bin/main.ml
@@ -0,0 +1,19 @@
+module Term = Asai.Tty.Make(Reporter.Message)
+
+let ep input =
+  let ast = Parser.parse_expr input in
+  let (tp, tm) = Elaborator.infer_toplevel ast in
+  let value = NbE.eval ~env:Emp tm in
+  Format.printf "%a : %a\n%!"
+    (Pretty.pp ~names:Emp) (NbE.quote ~size:0 value)
+    (Pretty.pp ~names:Emp) (NbE.quote ~size:0 tp)
+
+let rec repl () =
+  match LNoise.linenoise "toytt> " with
+  | Some input -> 
+    Reporter.run ~emit:Term.display ~fatal:Term.display (fun () -> ep input);
+    let _ = LNoise.history_add input in
+    repl ()
+  | None -> repl ()
+
+let () = repl ();
diff --git a/lib/Elab.ml b/src/elaborator/Elaborator.ml
index d911b9f..0f72f24 100644
--- a/lib/Elab.ml
+++ b/src/elaborator/Elaborator.ml
@@ -2,8 +2,8 @@ open Bwd
 open Bwd.Infix
 
 module A = Ast
-module S = Syntax
-module D = Domain
+module S = NbE.Syntax
+module D = NbE.Domain
 
 (* TODO: REALLY improve error messages *)
 
@@ -42,18 +42,18 @@ let bind ~(name : Ident.local) ~(tp : D.t) f =
 
 (** NbE helpers *)
 
-let eval tm = Eval.eval ~env:(Eff.read()).tms tm
+let eval tm = NbE.eval ~env:(Eff.read()).tms tm
 
 (** Evaluate under the current environment augmented by `arg` *)
 (* TODO: this is kind of inelegant, can we do better? *)
-let eval_at arg = Eval.eval ~env:((Eff.read()).tms <: arg)
+let eval_at arg = NbE.eval ~env:((Eff.read()).tms <: arg)
 
-let quote v = Quote.quote ~size:(Eff.read()).size v
+let quote v = NbE.quote ~size:(Eff.read()).size v
 
 (** Pretty-printing helpers *)
 
 let pp () = let names = (Eff.read()).names in fun fmt tm -> 
-  Syntax.Pretty.pp fmt (tm, names)
+  Pretty.pp ~names fmt tm
 
 (** Main algorithm *)
 
@@ -69,7 +69,7 @@ let rec check ~(tm : A.expr) ~(tp : D.t) : S.t =
   | A.Lam (name, body) -> begin match tp with
       | D.Pi (_, base, fam) -> 
         let body = bind ~name:name.value ~tp:base @@ fun arg ->
-          let fib = Eval.inst_clo fam arg in
+          let fib = NbE.inst_clo fam arg in
           check ~tm:body ~tp:fib in
         S.Lam (name.value, body)
       | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a Pi type" (pp()) (quote tp)
@@ -83,7 +83,7 @@ let rec check ~(tm : A.expr) ~(tp : D.t) : S.t =
   | A.Pair (fst, snd) -> begin match tp with
       | D.Sg (_, base, fam) -> 
         let fst = check ~tm:fst ~tp:base in
-        let fib = Eval.inst_clo fam (eval fst) in
+        let fib = NbE.inst_clo fam (eval fst) in
         let snd = check ~tm:snd ~tp:fib in
         S.Pair (fst, snd)
       | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a Sigma type" (pp()) (quote tp)
@@ -105,8 +105,8 @@ let rec check ~(tm : A.expr) ~(tp : D.t) : S.t =
       | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" (pp()) (quote tp)
     end
   | _ -> let (inferred_tp, tm) = infer tm in begin
-      try Conversion.equate ~size:((Eff.read()).size) inferred_tp tp with
-      | Conversion.Unequal ->
+      try NbE.equate ~size:((Eff.read()).size) inferred_tp tp with
+      | NbE.Unequal ->
         Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of type @[%a@]" (pp()) (quote tp) (pp()) (quote inferred_tp)
     end;
     tm
@@ -122,7 +122,7 @@ and infer (tm : A.expr) : D.t * S.t =
   | A.App (fn, arg) -> begin match infer fn with
       | (D.Pi (_, base, fam), fn) ->
         let arg = check ~tm:arg ~tp:base in
-        let tp = Eval.inst_clo fam (eval arg) in
+        let tp = NbE.inst_clo fam (eval arg) in
         let tm = S.App (fn, arg) in
         (tp, tm)
       | _ -> Reporter.fatalf Reporter.Message.IllTyped "cannot apply this term because it is not a function"
@@ -133,7 +133,7 @@ and infer (tm : A.expr) : D.t * S.t =
     end
   | A.Snd p -> begin match infer p with
       | (D.Sg (_, _, fam), p) ->
-        let tp = Eval.inst_clo fam (eval (S.Fst p)) in
+        let tp = NbE.inst_clo fam (eval (S.Fst p)) in
         let tm = S.Snd p in
         (tp, tm)
       | _ -> Reporter.fatalf Reporter.Message.IllTyped "cannot apply second projection to this term because it is of sigma type"
diff --git a/src/elaborator/dune b/src/elaborator/dune
new file mode 100644
index 0000000..46227f0
--- /dev/null
+++ b/src/elaborator/dune
@@ -0,0 +1,11 @@
+(library
+ (name Elaborator)
+ (public_name toytt.elaborator)
+ (libraries
+  algaeff
+  bwd
+  toytt.ast
+  toytt.ident
+  toytt.nbe
+  toytt.pretty
+  toytt.reporter))
diff --git a/lib/Ident.ml b/src/ident/Ident.ml
index 81c6575..81c6575 100644
--- a/lib/Ident.ml
+++ b/src/ident/Ident.ml
diff --git a/src/ident/dune b/src/ident/dune
new file mode 100644
index 0000000..732a2c7
--- /dev/null
+++ b/src/ident/dune
@@ -0,0 +1,4 @@
+(library
+ (name Ident)
+ (public_name toytt.ident)
+ (libraries fmt yuujinchou))
diff --git a/lib/Conversion.ml b/src/nbe/Conversion.ml
index 00bc942..00bc942 100644
--- a/lib/Conversion.ml
+++ b/src/nbe/Conversion.ml
diff --git a/lib/Data.ml b/src/nbe/Data.ml
index d2f94d3..d2f94d3 100644
--- a/lib/Data.ml
+++ b/src/nbe/Data.ml
diff --git a/lib/Domain.ml b/src/nbe/Domain.ml
index 6f5e11c..6f5e11c 100644
--- a/lib/Domain.ml
+++ b/src/nbe/Domain.ml
diff --git a/lib/Eval.ml b/src/nbe/Eval.ml
index bd8326e..bd8326e 100644
--- a/lib/Eval.ml
+++ b/src/nbe/Eval.ml
diff --git a/src/nbe/NbE.ml b/src/nbe/NbE.ml
new file mode 100644
index 0000000..3ec1f6d
--- /dev/null
+++ b/src/nbe/NbE.ml
@@ -0,0 +1,10 @@
+module Syntax = Syntax
+module Domain = Domain
+
+let eval = Eval.eval
+let inst_clo = Eval.inst_clo
+
+let quote = Quote.quote
+
+exception Unequal = Conversion.Unequal
+let equate = Conversion.equate
diff --git a/lib/Quote.ml b/src/nbe/Quote.ml
index 4b88e91..cc5a81e 100644
--- a/lib/Quote.ml
+++ b/src/nbe/Quote.ml
@@ -45,4 +45,3 @@ struct
 end
 
 let quote ~size v = Internal.Eff.run ~env:size (fun () -> Internal.quote v)
-let quote_ne ~size ne = Internal.Eff.run ~env:size (fun () -> Internal.quote_ne ne)
diff --git a/src/nbe/Syntax.ml b/src/nbe/Syntax.ml
new file mode 100644
index 0000000..dd690fb
--- /dev/null
+++ b/src/nbe/Syntax.ml
@@ -0,0 +1,20 @@
+type t = Data.syn =
+  | Var of int
+  | Pi of Ident.local * t * (* BINDS *) t
+  | Lam of Ident.local * (* BINDS *) t
+  | App of t * t
+  | Sg of Ident.local * t * (* BINDS *) t
+  | Pair of t * t
+  | Fst of t
+  | Snd of t
+  | Type
+  | Bool
+  | True
+  | False
+  | BoolElim of {
+      motive_var : Ident.local;
+      motive : (* BINDS *) t;
+      true_case : t;
+      false_case : t;
+      scrut : t;
+    }
diff --git a/src/nbe/dune b/src/nbe/dune
new file mode 100644
index 0000000..b7c9bed
--- /dev/null
+++ b/src/nbe/dune
@@ -0,0 +1,4 @@
+(library
+ (name NbE)
+ (public_name toytt.nbe)
+ (libraries algaeff bwd toytt.ident toytt.reporter))
diff --git a/src/parser/Eff.ml b/src/parser/Eff.ml
new file mode 100644
index 0000000..45887b8
--- /dev/null
+++ b/src/parser/Eff.ml
@@ -0,0 +1 @@
+include Algaeff.Reader.Make (struct type nonrec t = Asai.Range.source end)
\ No newline at end of file
diff --git a/lib/Parser.mly b/src/parser/Grammar.mly
index 8588b56..bb98029 100644
--- a/lib/Parser.mly
+++ b/src/parser/Grammar.mly
@@ -16,12 +16,12 @@ open Ast
 %right ASTERISK
 %left IDENT LPR APP BACKSLASH FST SND TYPE BOOL TRUE FALSE BOOL_ELIM
 
-%start <Ast.expr> parse
+%start <Ast.expr> start_expr
 
 %%
 
 %inline
-locate(X): e = X { Asai.Range.locate_lex ~source:(ParserEff.Eff.read()) $loc e }
+locate(X): e = X { Asai.Range.locate_lex ~source:(Eff.read()) $loc e }
 
 raw_ident: id = separated_nonempty_list(DOT, IDENT) { id }
 
@@ -77,4 +77,4 @@ raw_expr:
 %inline
 expr: e = locate(raw_expr) { e }
 
-parse: e = expr; EOF { e }
+start_expr: e = expr; EOF { e }
diff --git a/lib/Lexer.mll b/src/parser/Lexer.mll
index 98d1d6b..708bb64 100644
--- a/lib/Lexer.mll
+++ b/src/parser/Lexer.mll
@@ -1,14 +1,16 @@
 {
-open Parser
+open Grammar
+
+exception IllegalCharacter of char
 }
 
 let whitespace = [' ' '\t' '\r' '\n']+
 let letter = ['a'-'z' 'A'-'Z']
 let ident = letter+
 
-rule lex =
+rule token =
   parse
-  | whitespace { lex lexbuf }
+  | whitespace { token lexbuf }
   | "(" { LPR }
   | ")" { RPR }
   | "[" { LBR }
@@ -32,3 +34,4 @@ rule lex =
   | "bool-elim" { BOOL_ELIM }
   | ident { IDENT (Lexing.lexeme lexbuf) }
   | eof { EOF }
+  | (_ as illegal_char) { raise (IllegalCharacter illegal_char) }
diff --git a/src/parser/Parser.ml b/src/parser/Parser.ml
new file mode 100644
index 0000000..4593d82
--- /dev/null
+++ b/src/parser/Parser.ml
@@ -0,0 +1,13 @@
+let parse_expr (s : string) : Ast.expr =
+  let lexbuf = Lexing.from_string s in
+  let string_source : Asai.Range.string_source = {
+    title = None;
+    content = s;
+  } in
+  let source = `String string_source in
+  Eff.run ~env:source @@ fun () ->
+  try Grammar.start_expr Lexer.token lexbuf with
+  | Lexer.IllegalCharacter illegal_char ->
+    Reporter.illegal_character ~loc:(Asai.Range.of_lexbuf ~source lexbuf) illegal_char
+  | Grammar.Error ->
+    Reporter.syntax_error ~loc:(Asai.Range.of_lexbuf ~source lexbuf)
diff --git a/src/parser/dune b/src/parser/dune
new file mode 100644
index 0000000..fd4aae7
--- /dev/null
+++ b/src/parser/dune
@@ -0,0 +1,13 @@
+(menhir
+ (explain true)
+ (modules Grammar))
+
+(ocamllex Lexer)
+
+(library
+ (name Parser)
+ (public_name toytt.parser)
+ (libraries
+  asai
+  toytt.ast
+  toytt.reporter))
diff --git a/src/pretty/Pretty.ml b/src/pretty/Pretty.ml
new file mode 100644
index 0000000..66d6159
--- /dev/null
+++ b/src/pretty/Pretty.ml
@@ -0,0 +1,93 @@
+open Bwd
+open Bwd.Infix
+
+module S = NbE.Syntax
+
+module Internal =
+struct
+  type env = {
+    names : Ident.local bwd;
+    prec : int;
+  }
+
+  module Eff = Algaeff.Reader.Make (struct type nonrec t = env end)
+
+  let bind (name : Ident.local) f fmt x =
+    let update env = { env with names = env.names <: name } in
+    Eff.scope update (fun () -> f fmt x)
+
+  let with_prec (prec : int) (inner : 'a Fmt.t) (fmt : Format.formatter) (v : 'a) =
+    Eff.scope (fun env -> { env with prec; }) (fun () -> inner fmt v)
+
+  let delimited inner = with_prec 0 inner
+
+  let parenthesize (prec : int) : 'a Fmt.t -> 'a Fmt.t =
+    if (Eff.read()).prec > prec then
+      Fmt.parens
+    else
+      Fun.id
+
+  let lassoc (prec : int)
+      (pp_left : 'l Fmt.t)
+      ?(sep = " ")
+      (pp_right : 'r Fmt.t) : ('l * 'r) Fmt.t = 
+    parenthesize prec @@ fun fmt v -> 
+    Fmt.pf fmt "@[%a@]%s@[%a@]" 
+      (with_prec prec pp_left) (fst v)
+      sep
+      (with_prec (prec + 1) pp_right) (snd v)
+
+  let rassoc (prec : int)
+      (pp_left : 'l Fmt.t)
+      ?(sep = " ")
+      (pp_right : 'r Fmt.t) : ('l * 'r) Fmt.t = 
+    parenthesize prec @@ fun fmt v -> 
+    Fmt.pf fmt "@[%a@]%s@[%a@]" 
+      (with_prec (prec + 1) pp_left) (fst v)
+      sep
+      (with_prec prec pp_right) (snd v)
+
+  let pp_local_name fmt name =
+    Fmt.string fmt @@ Option.value ~default:"_" name
+
+  let pp_var fmt ix =
+    let names = (Eff.read()).names in
+    match Bwd.nth_opt names ix with
+    (* the variable has a bound name which has not been shadowed *)
+    | Some ((Some name) as id) when Bwd.find_index ((=) id) names = Some ix -> Fmt.string fmt name
+    (* the variable does not have a bound name or its bound name has been shadowed *)
+    | Some _ -> Fmt.pf fmt "%@%d" ix
+    | None -> Reporter.bug "index out of range in pp_var"
+
+  let rec pp_pair fmt = (delimited @@ fun fmt (a, b) -> Fmt.pf fmt "@[(@[%a@], @[%a@])@]" pp a pp b) fmt
+
+  and pp_bool_elim fmt =
+    (delimited @@ fun fmt (motive_var, motive, true_case, false_case, scrut) -> Fmt.pf fmt
+       "@[bool-elim @[%a@] at @[%a@] -> @[%a@] [ true => @[%a@], false => @[%a@] ]@]"
+       pp scrut pp_local_name motive_var (bind motive_var pp) motive pp true_case pp false_case
+    ) fmt
+
+  and pp_arg fmt (name, tp) =
+    Fmt.pf fmt "(@[%a@] : @[%a@])" pp_local_name name pp tp
+
+  (* TODO: improve indentation *)
+  and pp fmt = function
+    | S.Var ix -> pp_var fmt ix
+    | S.Pi (name, base, fam) -> rassoc 1 pp_arg ~sep:" -> " (bind name pp) fmt ((name, base), fam)
+    | S.Lam (name, body) -> Fmt.pf fmt "@[\\@[%a@] -> @[%a@]@]" pp_local_name name (bind name pp) body
+    | S.Sg (name, base, fam) -> rassoc 2 pp_arg ~sep:" * " (bind name pp) fmt ((name, base), fam)
+    | S.App (a, b) -> lassoc 3 pp pp fmt (a, b)
+    | S.Pair (a, b) -> pp_pair fmt (a, b)
+    | S.Fst a -> lassoc 3 Fmt.string pp fmt ("fst", a)
+    | S.Snd a -> lassoc 3 Fmt.string pp fmt ("snd", a)
+    | S.Type -> Fmt.string fmt "type"
+    | S.Bool -> Fmt.string fmt "bool"
+    | S.True -> Fmt.string fmt "true"
+    | S.False -> Fmt.string fmt "false"
+    | S.BoolElim { motive_var; motive; true_case; false_case; scrut }
+      -> pp_bool_elim fmt (motive_var, motive, true_case, false_case, scrut)
+end
+
+let pp ~names fmt tm =
+  let env : Internal.env = { names; prec = 0; } in
+  Internal.Eff.run ~env (fun () -> Internal.pp fmt tm)
diff --git a/src/pretty/dune b/src/pretty/dune
new file mode 100644
index 0000000..df46822
--- /dev/null
+++ b/src/pretty/dune
@@ -0,0 +1,9 @@
+(library
+ (name Pretty)
+ (public_name toytt.pretty)
+ (libraries
+  bwd
+  fmt
+  toytt.ident
+  toytt.nbe
+  toytt.reporter))
diff --git a/lib/Reporter.ml b/src/reporter/Reporter.ml
index a90966c..ee04c23 100644
--- a/lib/Reporter.ml
+++ b/src/reporter/Reporter.ml
@@ -1,32 +1,40 @@
 module Message =
 struct
   type t =
+    | IllegalCharacter
     | SyntaxError
-    | IllTyped
     | UnboundVariable
+    | IllTyped
     | CannotInferType
     | Bug
 
   let default_severity : t -> Asai.Diagnostic.severity =
     function
+    | IllegalCharacter -> Error
     | SyntaxError -> Error
-    | IllTyped -> Error
     | UnboundVariable -> Error
+    | IllTyped -> Error
     | CannotInferType -> Error
     | Bug -> Bug
 
   let short_code : t -> string =
     function
-    | SyntaxError -> "E001"
-    | IllTyped -> "E002"
-    | UnboundVariable -> "E003"
-    | CannotInferType -> "E004"
-    | Bug -> "BUG"
+    (* parser errors *)
+    | IllegalCharacter -> "E101"
+    | SyntaxError -> "E102"
+    (* elaboration errors *)
+    | UnboundVariable -> "E201"
+    | IllTyped -> "E202"
+    | CannotInferType -> "E202"
+    (* misc *)
+    | Bug -> "E900"
 end
 
 include Asai.Reporter.Make(Message)
 
-let unbound_variable id = fatalf UnboundVariable "unbound variable %a" Ident.pp id
+let illegal_character ~loc char = fatalf ~loc IllegalCharacter "illegal character '%s'" (Char.escaped char)
+let syntax_error ~loc = fatalf ~loc SyntaxError "syntax error"
+let unbound_variable id = fatalf UnboundVariable "unbound variable '%a'" Ident.pp id
 let expected_universe fmt x = fatalf IllTyped "expected a universe but got %a" fmt x
 
 let bug msg = fatalf Bug msg
diff --git a/src/reporter/dune b/src/reporter/dune
new file mode 100644
index 0000000..ab0f04a
--- /dev/null
+++ b/src/reporter/dune
@@ -0,0 +1,4 @@
+(library
+ (name Reporter)
+ (public_name toytt.reporter)
+ (libraries asai toytt.ident))
diff --git a/toytt.opam b/toytt.opam
index a10e9c7..ed17cae 100644
--- a/toytt.opam
+++ b/toytt.opam
@@ -18,6 +18,7 @@ depends: [
   "asai"
   "bwd"
   "fmt"
+  "linenoise"
   "yuujinchou"
   "odoc" {with-doc}
 ]