about summary refs log tree commit diff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--bin/dune3
-rw-r--r--bin/main.ml15
-rw-r--r--dune-project1
-rw-r--r--lib/Ast.ml12
-rw-r--r--lib/Conversion.ml75
-rw-r--r--lib/Data.ml51
-rw-r--r--lib/Domain.ml34
-rw-r--r--lib/Elab.ml163
-rw-r--r--lib/Eval.ml18
-rw-r--r--lib/Eval.mli4
-rw-r--r--lib/Lexer.mll1
-rw-r--r--lib/Parser.mly17
-rw-r--r--lib/ParserEff.ml1
-rw-r--r--lib/Quote.ml14
-rw-r--r--lib/Quote.mli4
-rw-r--r--lib/Reporter.ml28
-rw-r--r--lib/Syntax.ml114
-rw-r--r--lib/dune2
-rw-r--r--toytt.opam1
19 files changed, 490 insertions, 68 deletions
diff --git a/bin/dune b/bin/dune
index 52ff1d3..2e2f594 100644
--- a/bin/dune
+++ b/bin/dune
@@ -1,4 +1,5 @@
 (executable
  (public_name toytt)
  (name main)
- (libraries toytt))
+ (libraries toytt)
+ (modes byte exe))
diff --git a/bin/main.ml b/bin/main.ml
index 6c62764..ec5c4d2 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -1,14 +1,25 @@
 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
-  Format.printf "%a\n%!" Ast.pp_expr ast;
+  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) Syntax.Pretty.pp (Quote.quote ~size:0 tp);
   repl ()
 
-let () = repl ()
+let () =
+  Reporter.run ~emit:Term.display ~fatal:Term.display @@ fun () -> repl ()
diff --git a/dune-project b/dune-project
index e09f88d..0fa4b03 100644
--- a/dune-project
+++ b/dune-project
@@ -23,6 +23,7 @@
   algaeff
   asai
   bwd
+  fmt
   yuujinchou
  )
  (tags
diff --git a/lib/Ast.ml b/lib/Ast.ml
index 70e03dd..35611ac 100644
--- a/lib/Ast.ml
+++ b/lib/Ast.ml
@@ -1,11 +1,11 @@
 type raw_ident = Yuujinchou.Trie.path
 type ident = raw_ident Asai.Range.located
 
-type raw_arg = { name : ident; ty : expr }
-and arg = raw_arg Asai.Range.located
+type arg = ident * expr
 
 and raw_expr =
   | Var of raw_ident
+  | Check of expr * expr
   | Pi of arg * expr
   | Lam of ident * expr
   | App of expr * expr
@@ -27,18 +27,18 @@ and raw_expr =
 
 and expr = raw_expr Asai.Range.located
 
+(* TODO this is the same as Syntax.pretty.pp_name *)
 let dump_raw_ident fmt (id : raw_ident) = Format.pp_print_list
     ~pp_sep:(fun fmt () -> Format.pp_print_char fmt '.')
     Format.pp_print_string fmt id
 let dump_ident fmt ({ value; _ } : ident) = dump_raw_ident fmt value
 
-let rec dump_raw_arg fmt ({ name; ty } : raw_arg) =
-  Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" dump_ident name dump_expr ty
-
-and dump_arg fmt ({ value; _ } : arg) = dump_raw_arg fmt value
+let rec dump_arg fmt ((name, tp) : arg) =
+  Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" dump_ident name dump_expr tp
 
 and dump_raw_expr fmt = function
   | Var id -> Format.fprintf fmt "Var @[%a@]" dump_raw_ident id
+  | Check (tm, tp) -> Format.fprintf fmt "@[%a@] : @[%a@]" dump_expr tm dump_expr tp
   | Bool -> Format.pp_print_string fmt "Bool"
   | True -> Format.pp_print_string fmt "True"
   | False -> Format.pp_print_string fmt "False"
diff --git a/lib/Conversion.ml b/lib/Conversion.ml
new file mode 100644
index 0000000..b70a070
--- /dev/null
+++ b/lib/Conversion.ml
@@ -0,0 +1,75 @@
+open Bwd
+open Bwd.Infix
+
+module D = Domain
+
+exception Unequal
+
+module Internal =
+struct
+  (** Context size *)
+  type env = int
+
+  module Eff = Algaeff.Reader.Make (struct type nonrec t = env end)
+
+  let bind f =
+    let arg = D.var (Eff.read()) in
+    Eff.scope (fun size -> size + 1) (fun () -> f arg)
+
+  let rec equate v1 v2 = match v1, v2 with
+    | D.Neutral ne, v | v, D.Neutral ne -> equate_ne ne v
+    | D.Pi (base1, fam1), D.Pi (base2, fam2) ->
+      equate base1 base2;
+      equate_clo fam1 fam2
+    | D.Lam clo1, D.Lam clo2 -> equate_clo clo1 clo2
+    | D.Sg (base1, fam1), D.Sg (base2, fam2) ->
+      equate base1 base2;
+      equate_clo fam1 fam2
+    | D.Pair (fst1, snd1), D.Pair (fst2, snd2) ->
+      equate fst1 fst2;
+      equate snd1 snd2
+    | Type, Type -> ()
+    | Bool, Bool -> ()
+    | True, True -> ()
+    | False, False -> ()
+    | _ -> raise Unequal
+
+  and equate_clo clo1 clo2 = bind @@ fun arg ->
+    equate (Eval.inst_clo clo1 arg) (Eval.inst_clo clo2 arg)
+
+  and equate_ne_head (D.Var lvl1) (D.Var lvl2) =
+    if lvl1 = lvl2 then () else raise Unequal
+
+  and equate_frm frm1 frm2 = match frm1, frm2 with
+    | D.App arg1, D.App arg2 -> equate arg1 arg2
+    | D.Fst, D.Fst -> ()
+    | D.Snd, D.Snd -> ()
+    | D.BoolElim { cmot = mot1; vtrue = t1; vfalse = f1 },
+      D.BoolElim { cmot = mot2; vtrue = t2; vfalse = f2 } ->
+      equate_clo mot1 mot2;
+      equate t1 t2;
+      equate f1 f2;
+    | _ -> raise Unequal
+
+  and equate_spine sp1 sp2 = match sp1, sp2 with
+    | Emp, Emp -> ()
+    | Snoc (sp1, frm1), Snoc (sp2, frm2) ->
+      equate_frm frm1 frm2;
+      equate_spine sp1 sp2
+    | _ -> raise Unequal
+
+  and equate_ne (hd, sp) v = match v with
+    | D.Neutral (hd2, sp2) ->
+      equate_ne_head hd hd2;
+      equate_spine sp sp2
+    (* eta expansion *)
+    | D.Lam clo -> bind @@ fun arg ->
+      equate_ne (hd, sp <: D.App arg) (Eval.inst_clo clo arg)
+    | D.Pair (fst, snd) ->
+      equate_ne (hd, sp <: D.Fst) fst;
+      equate_ne (hd, sp <: D.Snd) snd
+    | _ -> raise Unequal
+end
+
+let equate ~size v1 v2 = Internal.Eff.run ~env:size @@ fun () ->
+  Internal.equate v1 v2
diff --git a/lib/Data.ml b/lib/Data.ml
new file mode 100644
index 0000000..19ca67d
--- /dev/null
+++ b/lib/Data.ml
@@ -0,0 +1,51 @@
+open Bwd
+
+(** Syntactic terms *)
+
+type syn =
+  | Var of int
+  | Pi of syn * (* BINDS *) syn
+  | Lam of (* BINDS *) syn
+  | App of syn * syn
+  | Sg of syn * (* BINDS *) syn
+  | Pair of syn * syn
+  | Fst of syn
+  | Snd of syn
+  | Type
+  | Bool
+  | True
+  | False
+  | BoolElim of {
+      motive : (* BINDS *) syn;
+      true_case : syn;
+      false_case : syn;
+      scrut : syn;
+    }
+
+(** Semantic domain *)
+
+type value =
+  | Neutral of ne
+  | Pi of value * clo
+  | Lam of clo
+  | Sg of value * clo
+  | Pair of value * value
+  | Type
+  | Bool
+  | True
+  | False
+
+and ne = ne_head * frm bwd
+and ne_head = Var of int (* De Bruijn levels *)
+and frm = 
+  | App of value
+  | Fst
+  | Snd
+  | BoolElim of {
+      cmot: clo;
+      vtrue: value;
+      vfalse: value;
+    }
+
+and env = value bwd
+and clo = Clo of { body : syn; env : env }
diff --git a/lib/Domain.ml b/lib/Domain.ml
index 88560c2..67ac4ae 100644
--- a/lib/Domain.ml
+++ b/lib/Domain.ml
@@ -1,31 +1,29 @@
 open Bwd
 
-type value =
+type t = Data.value =
   | Neutral of ne
-  | Pi of value * clos
-  | Lam of clos
-  | Sg of value * clos
-  | Pair of value * value
+  | Pi of t * clo
+  | Lam of clo
+  | Sg of t * clo
+  | Pair of t * t
   | Type
   | Bool
   | True
   | False
 
-and ne = ne_head * frame bwd
-and ne_head = Var of int (* De Bruijn levels *)
-and frame = 
-  | BoolElim of {
-      cmot: clos;
-      vtrue: value;
-      vfalse: value;
-    }
-  | App of value
+and ne = Data.ne
+and ne_head = Data.ne_head = Var of int (* De Bruijn levels *)
+and frm = Data.frm =
+  | App of t
   | Fst
   | Snd
+  | BoolElim of {
+      cmot: clo;
+      vtrue: t;
+      vfalse: t;
+    }
 
-and env = value bwd
-and clos = Clos of { body : Syntax.tm; env : env }
-
-type cell = { tm : value; tp : value }
+and env = Data.env
+and clo = Data.clo = Clo of { body : Data.syn; env : env }
 
 let var i = Neutral (Var i, Bwd.Emp)
diff --git a/lib/Elab.ml b/lib/Elab.ml
new file mode 100644
index 0000000..5bda770
--- /dev/null
+++ b/lib/Elab.ml
@@ -0,0 +1,163 @@
+open Bwd
+open Bwd.Infix
+
+module A = Ast
+module S = Syntax
+module D = Domain
+module R = Reporter
+
+(* TODO: REALLY improve error messages *)
+
+(* `None` means that an underscore was used in the binder *)
+(* TODO: actually implement this *)
+type local_name = Yuujinchou.Trie.path option
+
+(* invariant: `tps`, `tms` and `names` all have length `size` *)
+type env = {
+  tps : D.env;
+  tms : D.env;
+  names : local_name bwd;
+  size : int;
+}
+
+module Eff = Algaeff.Reader.Make (struct type nonrec t = env end)
+
+(** General helpers *)
+
+let lookup_name name : D.t * S.t = 
+  let env = Eff.read() in
+  match Bwd.find_index ((=) (Some name)) env.names with
+  | Some ix ->
+    let tp = Bwd.nth env.tps ix in
+    let tm = Quote.quote ~size:env.size (Bwd.nth env.tms ix) in
+    (tp, tm)
+  | None -> R.fatalf R.Message.UnboundVariable 
+              "unbound variable @[%a@]" S.Pretty.pp_name name
+
+let define ~(name : A.raw_ident) ~(tp : D.t) ~(tm : D.t) f =
+  let update env = {
+    tps = env.tps <: tp;
+    tms = env.tms <: tm;
+    names = env.names <: Some name;
+    size = env.size + 1;
+  } in
+  Eff.scope update f
+
+let bind ~(name : A.raw_ident) ~(tp : D.t) f =
+  let arg = D.var (Eff.read()).size in
+  define ~name ~tp ~tm:arg (fun () -> f arg)
+
+(** NbE helpers *)
+
+let eval tm = Eval.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 quote v = Quote.quote ~size:(Eff.read()).size v
+
+(** Main algorithm *)
+
+let rec check ~(tm : A.expr) ~(tp : D.t) : S.t =
+  R.tracef ?loc:tm.loc "when checking against the type @[%a@]" Syntax.Pretty.pp (quote tp) @@ fun () ->
+  match tm.value with
+  | A.Pi ((name, base), fam) -> begin match tp with
+      | D.Type ->
+        let base = check ~tm:base ~tp in
+        let fam = bind ~name:name.value ~tp:(eval base) @@ fun _ -> check ~tm:fam ~tp in
+        S.Pi (base, fam)
+      | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" Syntax.Pretty.pp (quote tp) end
+  | 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
+          check ~tm:body ~tp:fib in
+        S.Lam body
+      | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a Pi type" Syntax.Pretty.pp (quote tp)
+    end
+  | A.Sg ((name, base), fam) -> begin match tp with
+      | D.Type ->
+        let base = check ~tm:base ~tp in
+        let fam = bind ~name:name.value ~tp:(eval base) @@ fun _ -> check ~tm:fam ~tp in
+        S.Sg (base, fam)
+      | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" Syntax.Pretty.pp (quote tp) end
+  | 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 snd = check ~tm:snd ~tp:fib in
+        S.Pair (fst, snd)
+      | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a Sigma type" Syntax.Pretty.pp (quote tp)
+    end
+  | A.Type -> begin match tp with (* TODO type-in-type *)
+      | D.Type -> S.Type
+      | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" Syntax.Pretty.pp (quote tp)
+    end
+  | A.Bool -> begin match tp with
+      | D.Type -> S.Bool
+      | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" Syntax.Pretty.pp (quote tp)
+    end
+  | A.True -> begin match tp with
+      | D.Bool -> S.True
+      | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" Syntax.Pretty.pp (quote tp)
+    end
+  | A.False -> begin match tp with
+      | D.Bool -> S.False
+      | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" Syntax.Pretty.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 ->
+        R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of type @[%a@]" Syntax.Pretty.pp (quote tp) Syntax.Pretty.pp (quote inferred_tp)
+    end;
+    tm
+
+and infer (tm : A.expr) : D.t * S.t =
+  R.tracef ?loc:tm.loc "when inferring the type" @@ fun () ->
+  match tm.value with
+  | A.Var name -> lookup_name name
+  | A.Check (tm, tp) ->
+    let tp = eval @@ check ~tp:D.Type ~tm:tp in
+    let tm = check ~tp ~tm in
+    (tp, tm)
+  | 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 tm = S.App (fn, arg) in
+        (tp, tm)
+      | _ -> R.fatalf R.Message.IllTyped "cannot apply this term because it is not a function"
+    end
+  | A.Fst p -> begin match infer p with
+      | (D.Sg (base, _), p) -> (base, S.Fst p)
+      | _ -> R.fatalf R.Message.IllTyped "cannot apply first projection to this term because it is not of sigma type"
+    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 tm = S.Snd p in
+        (tp, tm)
+      | _ -> R.fatalf R.Message.IllTyped "cannot apply second projection to this term because it is of sigma type"
+    end
+  | A.BoolElim { motive_var; motive_body; true_case; false_case; scrut } ->
+    let scrut = check ~tm:scrut ~tp:D.Bool in
+    let motive = bind ~name:motive_var.value ~tp:D.Bool @@ fun _ ->
+      check ~tm:motive_body ~tp:D.Type in
+    let motive_true = eval_at D.True motive in
+    let motive_false = eval_at D.False motive in
+    let motive_scrut = eval_at (eval scrut) motive in
+    let true_case = check ~tm:true_case ~tp:motive_true in
+    let false_case = check ~tm:false_case ~tp:motive_false in
+    let tm = S.BoolElim { motive; true_case; false_case; scrut } in
+    (motive_scrut, tm)
+  | _ -> R.fatalf R.Message.CannotInferType "cannot infer type"
+
+let empty_env : env = {
+  tps = Emp;
+  tms = Emp;
+  names = Emp;
+  size = 0;
+}
+
+let infer_toplevel (tm : A.expr) = Eff.run ~env:empty_env @@ fun () -> infer tm
\ No newline at end of file
diff --git a/lib/Eval.ml b/lib/Eval.ml
index 8f6722b..033ee8c 100644
--- a/lib/Eval.ml
+++ b/lib/Eval.ml
@@ -8,14 +8,14 @@ module Internal =
 struct
   module Eff = Algaeff.Reader.Make (struct type nonrec t = D.env end)
 
-  let make_clos body = D.Clos { body; env = Eff.read() }
+  let make_clo body = D.Clo { body; env = Eff.read() }
 
-  let rec inst_clos (D.Clos { body; env }) arg =
+  let rec inst_clo (D.Clo { body; env }) arg =
     let env = env <: arg in
     Eff.run ~env @@ fun () -> eval body
 
   and app v w = match v with
-    | D.Lam clos -> inst_clos clos w
+    | D.Lam clo -> inst_clo clo w
     | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.App w)
     | _ -> invalid_arg "Eval.app"
 
@@ -37,10 +37,10 @@ struct
 
   and eval = function
     | S.Var i -> Bwd.nth (Eff.read()) i
-    | S.Pi (base, fam) -> D.Pi (eval base, make_clos fam)
-    | S.Lam body -> D.Lam (make_clos body)
+    | S.Pi (base, fam) -> D.Pi (eval base, make_clo fam)
+    | S.Lam body -> D.Lam (make_clo body)
     | S.App (a, b) -> app (eval a) (eval b)
-    | S.Sg (base, fam) -> D.Sg (eval base, make_clos fam)
+    | S.Sg (base, fam) -> D.Sg (eval base, make_clo fam)
     | S.Pair (a, b) -> D.Pair (eval a, eval b)
     | S.Fst a -> fst (eval a)
     | S.Snd a -> snd (eval a)
@@ -49,8 +49,8 @@ struct
     | S.True -> D.True
     | S.False -> D.False
     | S.BoolElim { motive; true_case; false_case; scrut } ->
-      bool_elim (make_clos motive) (eval true_case) (eval false_case) (eval scrut)
+      bool_elim (make_clo motive) (eval true_case) (eval false_case) (eval scrut)
 end
 
-let eval ~env tm = Internal.Eff.run ~env (fun () -> Internal.eval tm)
-let inst_clos = Internal.inst_clos
+let eval ~env tm = Internal.Eff.run ~env @@ fun () -> Internal.eval tm
+let inst_clo = Internal.inst_clo
diff --git a/lib/Eval.mli b/lib/Eval.mli
index 24fa87d..63c49cf 100644
--- a/lib/Eval.mli
+++ b/lib/Eval.mli
@@ -1,2 +1,2 @@
-val eval : env:Domain.env -> Syntax.tm -> Domain.value
-val inst_clos : Domain.clos -> Domain.value -> Domain.value
+val eval : env:Domain.env -> Syntax.t -> Domain.t
+val inst_clo : Domain.clo -> Domain.t -> Domain.t
diff --git a/lib/Lexer.mll b/lib/Lexer.mll
index 3f178f5..c33acae 100644
--- a/lib/Lexer.mll
+++ b/lib/Lexer.mll
@@ -16,6 +16,7 @@ rule lex =
   | "->" { ARROW }
   | "*" { ASTERISK }
   | "\\" { BACKSLASH }
+  | "::" { DOUBLE_COLON }
   | ":" { COLON }
   | "," { COMMA }
   | "." { DOT }
diff --git a/lib/Parser.mly b/lib/Parser.mly
index 0390b3c..fc82d1a 100644
--- a/lib/Parser.mly
+++ b/lib/Parser.mly
@@ -5,13 +5,15 @@ open Ast
 %token <string> IDENT
 %token LPR RPR
 %token LBR RBR
-%token ARROW ASTERISK BACKSLASH COLON COMMA DOT FATARROW
+%token ARROW ASTERISK BACKSLASH COLON DOUBLE_COLON COMMA DOT FATARROW
 %token BOOL TRUE FALSE BOOL_ELIM AT
 %token FST SND
 %token TYPE
 %token EOF
 
-%right ARROW ASTERISK
+%nonassoc DOUBLE_COLON
+%right ARROW
+%right ASTERISK
 %left IDENT LPR APP BACKSLASH FST SND TYPE BOOL TRUE FALSE BOOL_ELIM
 
 %start <Ast.expr> parse
@@ -19,24 +21,23 @@ open Ast
 %%
 
 %inline
-locate(X): e = X { Asai.Range.locate_lex $loc e }
+locate(X): e = X { Asai.Range.locate_lex ~source:(ParserEff.Eff.read()) $loc e }
 
 raw_ident: id = separated_nonempty_list(DOT, IDENT) { id }
 
 %inline
 ident: id = locate(raw_ident) { id }
 
-raw_arg: LPR; name = ident; COLON; ty = expr; RPR
-	{ { name; ty } }
-
-%inline
-arg: a = locate(raw_arg) { a }
+arg: LPR; name = ident; COLON; tp = expr; RPR
+	{ (name, tp) }
 
 raw_expr:
   | name = raw_ident
 	{ Var name }
   | LPR; e = raw_expr; RPR
 	{ e }
+  | tm = expr; DOUBLE_COLON; tp = expr
+    { Check (tm, tp) }
 
   | a = arg; ARROW; b = expr
 	{ Pi (a, b) }
diff --git a/lib/ParserEff.ml b/lib/ParserEff.ml
new file mode 100644
index 0000000..84c0de8
--- /dev/null
+++ b/lib/ParserEff.ml
@@ -0,0 +1 @@
+module Eff = Algaeff.Reader.Make (struct type nonrec t = Asai.Range.source end)
diff --git a/lib/Quote.ml b/lib/Quote.ml
index 5989870..611843a 100644
--- a/lib/Quote.ml
+++ b/lib/Quote.ml
@@ -15,28 +15,28 @@ struct
     
   let rec quote = function
     | D.Neutral ne -> quote_ne ne
-    | D.Pi (base, fam) -> S.Pi (quote base, quote_clos fam)
-    | D.Lam clos -> S.Lam (quote_clos clos)
-    | D.Sg (base, fam) -> S.Sg (quote base, quote_clos fam)
+    | D.Pi (base, fam) -> S.Pi (quote base, quote_clo fam)
+    | D.Lam clo -> S.Lam (quote_clo clo)
+    | D.Sg (base, fam) -> S.Sg (quote base, quote_clo fam)
     | D.Pair (v, w) -> S.Pair (quote v, quote w)
     | D.Type -> S.Type
     | D.Bool -> S.Bool
     | D.True -> S.True
     | D.False -> S.False
 
-  and quote_clos clos = bind @@ fun arg -> quote (Eval.inst_clos clos arg)
+  and quote_clo clo = bind @@ fun arg -> quote (Eval.inst_clo clo arg)
 
-  and quote_ne (hd, frms) = Bwd.fold_left quote_frame (quote_ne_head hd) frms
+  and quote_ne (hd, frms) = Bwd.fold_left quote_frm (quote_ne_head hd) frms
 
   and quote_ne_head (D.Var i) = S.Var (Eff.read() - i - 1) (* converting from levels to indices *)
 
-  and quote_frame hd = function
+  and quote_frm hd = function
     | D.App v -> S.App (hd, quote v)
     | D.Fst -> S.Fst hd
     | D.Snd -> S.Snd hd
     | D.BoolElim { cmot; vtrue; vfalse } ->
       S.BoolElim {
-        motive = quote_clos cmot;
+        motive = quote_clo cmot;
         true_case = quote vtrue;
         false_case = quote vfalse;
         scrut = hd;
diff --git a/lib/Quote.mli b/lib/Quote.mli
index c55aa8b..193b0b0 100644
--- a/lib/Quote.mli
+++ b/lib/Quote.mli
@@ -1,2 +1,2 @@
-val quote : size:int -> Domain.value -> Syntax.tm
-val quote_ne : size:int -> Domain.ne -> Syntax.tm
+val quote : size:int -> Domain.t -> Syntax.t
+val quote_ne : size:int -> Domain.ne -> Syntax.t
diff --git a/lib/Reporter.ml b/lib/Reporter.ml
new file mode 100644
index 0000000..c86a04a
--- /dev/null
+++ b/lib/Reporter.ml
@@ -0,0 +1,28 @@
+module Message =
+struct
+  type t = 
+    | SyntaxError
+    | IllTyped
+    | UnboundVariable
+    | CannotInferType
+
+  let default_severity : t -> Asai.Diagnostic.severity =
+    function
+    | SyntaxError -> Error
+    | IllTyped -> Error
+    | UnboundVariable -> Error
+    | CannotInferType -> Error
+
+  let short_code : t -> string =
+    function
+    | SyntaxError -> "E0001"
+    | IllTyped -> "E0002"
+    | UnboundVariable -> "E0003"
+    | CannotInferType -> "E0004"
+end
+
+include Asai.Reporter.Make(Message)
+
+let invalid_local_name (name : Ast.raw_ident) = fatalf SyntaxError "invalid local variable name `%a`" Ast.dump_raw_ident name
+
+let expected_universe fmt x = fatalf IllTyped "expected a universe but got %a" fmt x
\ No newline at end of file
diff --git a/lib/Syntax.ml b/lib/Syntax.ml
index 6cd988a..c4cf80d 100644
--- a/lib/Syntax.ml
+++ b/lib/Syntax.ml
@@ -1,19 +1,109 @@
-type tm =
+open Bwd
+
+type t = Data.syn =
   | Var of int
-  | Pi of tm * (* BINDS *) tm
-  | Lam of (* BINDS *) tm
-  | App of tm * tm
-  | Sg of tm * (* BINDS *) tm
-  | Pair of tm * tm
-  | Fst of tm
-  | Snd of tm
+  | Pi of t * (* BINDS *) t
+  | Lam of (* BINDS *) t
+  | App of t * t
+  | Sg of t * (* BINDS *) t
+  | Pair of t * t
+  | Fst of t
+  | Snd of t
   | Type
   | Bool
   | True
   | False
   | BoolElim of {
-      motive : (* BINDS *) tm;
-      true_case : tm;
-      false_case : tm;
-      scrut : tm;
+      motive : (* BINDS *) t;
+      true_case : t;
+      false_case : t;
+      scrut : t;
     }
+
+module Pretty =
+struct
+  type local_names = Yuujinchou.Trie.path option bwd
+  type tm_with_names = t * local_names
+  
+  let pp_name fmt (id : Yuujinchou.Trie.path) = Format.pp_print_list
+      ~pp_sep:(fun fmt () -> Format.pp_print_char fmt '.')
+      Format.pp_print_string fmt id
+
+  module Internal =
+  struct
+    type env = {
+      prec : int;
+    }
+
+    module Eff = Algaeff.Reader.Make (struct type nonrec t = env end)
+
+    let with_prec (prec : int) (inner : 'a Fmt.t) (fmt : Format.formatter) (v : 'a) =
+      Eff.scope (fun _ -> { 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)
+        ?(pre = "")
+        (pp_left : 'l Fmt.t)
+        ?(middle = " ")
+        (pp_right : 'r Fmt.t)
+        ?(post = "") : ('l * 'r) Fmt.t = 
+      parenthesize prec @@ fun fmt v -> 
+      Fmt.pf fmt "%s@[%a@]%s@[%a@]%s" 
+        pre
+        (with_prec prec pp_left) (fst v)
+        middle 
+        (with_prec (prec + 1) pp_right) (snd v)
+        post
+
+    let rassoc (prec : int)
+        ?(pre = "")
+        (pp_left : 'l Fmt.t)
+        ?(middle = " ")
+        (pp_right : 'r Fmt.t)
+        ?(post = "") : ('l * 'r) Fmt.t = 
+      parenthesize prec @@ fun fmt v -> 
+      Fmt.pf fmt "%s@[%a@]%s@[%a@]%s" 
+        pre
+        (with_prec (prec + 1) pp_left) (fst v)
+        middle 
+        (with_prec prec pp_right) (snd v)
+        post
+
+    let pp_var ix fmt = Fmt.pf fmt "%@%d" ix
+
+    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, true_case, false_case, scrut) -> Fmt.pf fmt
+         "@[bool-elim @[%a@] at _ -> @[%a@] [ true => @[%a@], false => @[%a@] ]@]"
+         pp scrut pp motive pp true_case pp false_case
+      ) fmt
+
+    (* TODO: improve indentation *)
+    and pp fmt = function
+      | Var ix -> pp_var ix fmt
+      | Pi (base, fam) -> rassoc 1 ~pre:"(_ : " pp ~middle:") -> " pp fmt (base, fam)
+      | Lam body -> Fmt.pf fmt "@[\\_ -> @[%a@]@]" pp body
+      | Sg (base, fam) -> rassoc 2 ~pre:"(_ : " pp ~middle:") * " pp fmt (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; true_case; false_case; scrut } -> pp_bool_elim fmt (motive, true_case, false_case, scrut)
+  end
+
+  let pp fmt tm =
+    let env : Internal.env = { prec = 0; } in
+    Internal.Eff.run ~env (fun () -> Internal.pp fmt tm)
+end
diff --git a/lib/dune b/lib/dune
index 7889c59..3d2f366 100644
--- a/lib/dune
+++ b/lib/dune
@@ -6,5 +6,5 @@
 
 (library
  (name toytt)
- (libraries asai yuujinchou)
+ (libraries asai fmt yuujinchou)
  (preprocess (pps ppx_deriving.std)))
diff --git a/toytt.opam b/toytt.opam
index c111515..a10e9c7 100644
--- a/toytt.opam
+++ b/toytt.opam
@@ -17,6 +17,7 @@ depends: [
   "algaeff"
   "asai"
   "bwd"
+  "fmt"
   "yuujinchou"
   "odoc" {with-doc}
 ]
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-09-27 17:20:51 +0000