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

1 files changed, 15 insertions, 15 deletions

diff --git a/lib/Ast.ml b/lib/Ast.ml
index 35611ac..1a1d4c5 100644
--- a/lib/Ast.ml
+++ b/lib/Ast.ml
@@ -1,13 +1,13 @@
-type raw_ident = Yuujinchou.Trie.path
-type ident = raw_ident Asai.Range.located
+type ident = Ident.t Asai.Range.located
+type local_name = Ident.local Asai.Range.located
 
-type arg = ident * expr
+type arg = local_name * expr
 
 and raw_expr =
-  | Var of raw_ident
+  | Var of Ident.t
   | Check of expr * expr
   | Pi of arg * expr
-  | Lam of ident * expr
+  | Lam of local_name * expr
   | App of expr * expr
   | Sg of arg * expr
   | Pair of expr * expr
@@ -18,7 +18,7 @@ and raw_expr =
   | True
   | False
   | BoolElim of {
-      motive_var : ident;
+      motive_var : local_name;
       motive_body : expr;
       true_case : expr;
       false_case : expr;
@@ -27,17 +27,17 @@ 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 dump_ident fmt ({ value; _ } : ident) = Ident.pp fmt value
+
+let dump_local_name fmt ({ value; _ } : local_name) = match value with
+  | Some name -> Format.pp_print_string fmt name
+  | None -> Format.pp_print_char fmt '_'
 
 let rec dump_arg fmt ((name, tp) : arg) =
-  Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" dump_ident name dump_expr tp
+  Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" dump_local_name name dump_expr tp
 
 and dump_raw_expr fmt = function
-  | Var id -> Format.fprintf fmt "Var @[%a@]" dump_raw_ident id
+  | Var id -> Format.fprintf fmt "Var @[%a@]" Ident.pp 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"
@@ -45,7 +45,7 @@ and dump_raw_expr fmt = function
   | BoolElim { motive_var; motive_body; true_case; false_case; scrut } ->
     Format.fprintf fmt
       "@[<10>BoolElim (@[%a@] ->@ @[%a@],@ @[%a@],@ @[%a@],@ @[%a@])@]"
-      dump_ident motive_var
+      dump_local_name motive_var
       dump_expr motive_body
       dump_expr true_case
       dump_expr false_case
@@ -53,7 +53,7 @@ and dump_raw_expr fmt = function
   | Pi (dom, cod) ->
     Format.fprintf fmt "@[<4>Pi (@[%a@],@ @[%a@])@]" dump_arg dom dump_expr cod
   | Lam (var, body) ->
-    Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" dump_ident var dump_expr body
+    Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" dump_local_name var dump_expr body
   | App (fn, arg) ->
     Format.fprintf fmt "@[<5>App (@[%a@],@ @[%a@])@]" dump_expr fn dump_expr arg
   | Sg (fst, snd) ->