keep track of bound names everywhere to be able to output names instead of de bruijn indices

1 files changed, 46 insertions, 48 deletions

diff --git a/lib/Elab.ml b/lib/Elab.ml
index 5bda770..d911b9f 100644
--- a/lib/Elab.ml
+++ b/lib/Elab.ml
@@ -4,19 +4,14 @@ 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;
+  names : Ident.local bwd;
   size : int;
 }
 
@@ -24,28 +19,26 @@ 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 lookup (id : Ident.t) : D.t * S.t = match Ident.to_local id with
+  | Some name -> begin
+      let env = Eff.read() in
+      match Bwd.find_index ((=) name) env.names with
+      | Some ix ->
+        let tp = Bwd.nth env.tps ix in
+        (tp, S.Var ix)
+      | None -> Reporter.unbound_variable id
+    end
+  | None -> Reporter.unbound_variable id
 
-let define ~(name : A.raw_ident) ~(tp : D.t) ~(tm : D.t) f =
+let bind ~(name : Ident.local) ~(tp : D.t) f =
+  let arg = D.var (Eff.read()).size in
   let update env = {
     tps = env.tps <: tp;
-    tms = env.tms <: tm;
-    names = env.names <: Some name;
+    tms = env.tms <: arg;
+    names = env.names <: 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)
+  Eff.scope update (fun () -> f arg)
 
 (** NbE helpers *)
 
@@ -57,88 +50,93 @@ let eval_at arg = Eval.eval ~env:((Eff.read()).tms <: arg)
 
 let quote v = Quote.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)
+
 (** 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 () ->
+  Reporter.tracef ?loc:tm.loc "when checking against the type @[%a@]" (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
+        S.Pi (name.value, base, fam)
+      | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp) end
   | A.Lam (name, body) -> begin match tp with
-      | D.Pi (base, fam) -> 
+      | 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)
+        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)
     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
+        S.Sg (name.value, base, fam)
+      | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp) end
   | A.Pair (fst, snd) -> begin match tp with
-      | D.Sg (base, fam) -> 
+      | 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)
+      | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a Sigma type" (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)
+      | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (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)
+      | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (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)
+      | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" (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)
+      | _ -> 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 ->
-        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)
+        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
 
 and infer (tm : A.expr) : D.t * S.t =
-  R.tracef ?loc:tm.loc "when inferring the type" @@ fun () ->
+  Reporter.tracef ?loc:tm.loc "when inferring the type" @@ fun () ->
   match tm.value with
-  | A.Var name -> lookup_name name
+  | A.Var name -> lookup 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) ->
+      | (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"
+      | _ -> Reporter.fatalf Reporter.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"
+      | (D.Sg (_, base, _), p) -> (base, S.Fst p)
+      | _ -> Reporter.fatalf Reporter.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) ->
+      | (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"
+      | _ -> Reporter.fatalf Reporter.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
@@ -149,9 +147,9 @@ and infer (tm : A.expr) : D.t * S.t =
     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
+    let tm = S.BoolElim { motive_var = motive_var.value; motive; true_case; false_case; scrut } in
     (motive_scrut, tm)
-  | _ -> R.fatalf R.Message.CannotInferType "cannot infer type"
+  | _ -> Reporter.fatalf Reporter.Message.CannotInferType "cannot infer type"
 
 let empty_env : env = {
   tps = Emp;