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

1 files changed, 44 insertions, 38 deletions

diff --git a/lib/Syntax.ml b/lib/Syntax.ml
index c4cf80d..fc58353 100644
--- a/lib/Syntax.ml
+++ b/lib/Syntax.ml
@@ -1,11 +1,12 @@
 open Bwd
+open Bwd.Infix
 
 type t = Data.syn =
   | Var of int
-  | Pi of t * (* BINDS *) t
-  | Lam of (* BINDS *) t
+  | Pi of Ident.local * t * (* BINDS *) t
+  | Lam of Ident.local * (* BINDS *) t
   | App of t * t
-  | Sg of t * (* BINDS *) t
+  | Sg of Ident.local * t * (* BINDS *) t
   | Pair of t * t
   | Fst of t
   | Snd of t
@@ -14,6 +15,7 @@ type t = Data.syn =
   | True
   | False
   | BoolElim of {
+      motive_var : Ident.local;
       motive : (* BINDS *) t;
       true_case : t;
       false_case : t;
@@ -22,23 +24,21 @@ type t = Data.syn =
 
 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 = {
+      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 _ -> { prec; }) (fun () -> inner fmt v)
+      Eff.scope (fun env -> { env with prec; }) (fun () -> inner fmt v)
 
     let delimited inner = with_prec 0 inner
 
@@ -49,49 +49,54 @@ struct
         Fun.id
 
     let lassoc (prec : int)
-        ?(pre = "")
         (pp_left : 'l Fmt.t)
-        ?(middle = " ")
-        (pp_right : 'r Fmt.t)
-        ?(post = "") : ('l * 'r) Fmt.t = 
+        ?(sep = " ")
+        (pp_right : 'r Fmt.t) : ('l * 'r) Fmt.t = 
       parenthesize prec @@ fun fmt v -> 
-      Fmt.pf fmt "%s@[%a@]%s@[%a@]%s" 
-        pre
+      Fmt.pf fmt "@[%a@]%s@[%a@]" 
         (with_prec prec pp_left) (fst v)
-        middle 
+        sep
         (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 = 
+        ?(sep = " ")
+        (pp_right : 'r Fmt.t) : ('l * 'r) Fmt.t = 
       parenthesize prec @@ fun fmt v -> 
-      Fmt.pf fmt "%s@[%a@]%s@[%a@]%s" 
-        pre
+      Fmt.pf fmt "@[%a@]%s@[%a@]" 
         (with_prec (prec + 1) pp_left) (fst v)
-        middle 
+        sep
         (with_prec prec pp_right) (snd v)
-        post
 
-    let pp_var ix fmt = Fmt.pf fmt "%@%d" ix
+    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, 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
+      (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 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)
+      | 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)
@@ -100,10 +105,11 @@ struct
       | 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)
+      | 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 =
-    let env : Internal.env = { prec = 0; } in
+  let pp fmt (tm, names) =
+    let env : Internal.env = { names; prec = 0; } in
     Internal.Eff.run ~env (fun () -> Internal.pp fmt tm)
 end