[nametab] Introduce type of imperative nametabs, unify API

This is both a cleanup and a step towards pushing the state upwards,
and handling the nametabs functionally.

Related to rocq-prover#16746 and
rocq-prover/rfcs#65

Author: ejgallego

engine/namegen.ml

@@ -81,14 +81,14 @@ let is_imported_ref = let open GlobRef in function
 
 let is_global id =
   try
-    let ref = Nametab.locate (qualid_of_ident id) in
+    let ref = Nametab.GlobRef.locate (qualid_of_ident id) in
     not (is_imported_ref ref)
   with Not_found ->
     false
 
 let is_constructor id =
   try
-    match Nametab.locate (qualid_of_ident id) with
+    match Nametab.GlobRef.locate (qualid_of_ident id) with
       | GlobRef.ConstructRef _ -> true
       | _ -> false
   with Not_found ->
@@ -281,7 +281,7 @@ let visible_ids sigma (nenv, c) =
     let g = global_of_constr c in
     if not (GlobRef.Set_env.mem g gseen) then
       let gseen = GlobRef.Set_env.add g gseen in
-      let ids = match Nametab.shortest_qualid_of_global Id.Set.empty g with
+      let ids = match Nametab.GlobRef.shortest_qualid Id.Set.empty g with
       | short ->
         let dir, id = repr_qualid short in
         if DirPath.is_empty dir then Id.Set.add id ids else ids

engine/termops.ml

@@ -886,7 +886,7 @@ let free_rels_and_unqualified_refs sigma t =
       if not (GlobRef.Set_env.mem g gseen) then begin
         try
           let gseen = GlobRef.Set_env.add g gseen in
-          let short = Nametab.shortest_qualid_of_global Id.Set.empty g in
+          let short = Nametab.GlobRef.shortest_qualid Id.Set.empty g in
           let dir, id = Libnames.repr_qualid short in
           let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in
           (gseen, vseen, ids)

engine/univNames.ml

@@ -15,7 +15,8 @@ open Univ
 let qualid_of_level ctx l =
   match Level.name l with
   | Some qid  ->
-    (try Some (Nametab.shortest_qualid_of_universe ctx qid)
+    let ctx = Id.Map.domain ctx in
+    (try Some (Nametab.Universe.shortest_qualid ctx qid)
      with Not_found -> None)
   | None -> None
 

interp/abbreviation.ml

@@ -39,17 +39,17 @@ let toggle_abbreviation ~on ~use kn =
   if data.abbrev_activated != on then
     begin
       abbrev_table := KNmap.add kn {data with abbrev_activated = on} !abbrev_table;
-      let sp = Nametab.path_of_abbreviation kn in
+      let sp = Nametab.Abbrev.path kn in
       match use with
       | OnlyPrinting -> ()
       | OnlyParsing | ParsingAndPrinting ->
          if on then
            begin
-             Nametab.push_abbreviation (Nametab.Until 1) sp kn;
-             Nametab.push_abbreviation (Nametab.Exactly 1) sp kn
+             Nametab.Abbrev.push (Nametab.Until 1) sp kn;
+             Nametab.Abbrev.push (Nametab.Exactly 1) sp kn
            end
          else
-           Nametab.remove_abbreviation sp kn
+           Nametab.Abbrev.remove sp kn
     end
 
 let toggle_abbreviations ~on ~use filter =
@@ -58,23 +58,23 @@ let toggle_abbreviations ~on ~use filter =
   !abbrev_table ()
 
 let load_abbreviation i ((sp,kn),(_local,abbrev)) =
-  if Nametab.exists_cci sp then
+  if Nametab.GlobRef.exists sp then
     user_err
       (Id.print (basename sp) ++ str " already exists.");
   add_abbreviation kn abbrev;
-  Nametab.push_abbreviation (Nametab.Until i) sp kn
+  Nametab.Abbrev.push (Nametab.Until i) sp kn
 
 let is_alias_of_already_visible_name sp = function
   | _,NRef (ref,_) ->
-      let (dir,id) = repr_qualid (Nametab.shortest_qualid_of_global Id.Set.empty ref) in
+      let (dir,id) = repr_qualid (Nametab.GlobRef.shortest_qualid Id.Set.empty ref) in
       DirPath.is_empty dir && Id.equal id (basename sp)
   | _ ->
       false
 
 let open_abbreviation i ((sp,kn),(_local,abbrev)) =
   let pat = abbrev.abbrev_pattern in
   if not (Int.equal i 1 && is_alias_of_already_visible_name sp pat) then begin
-    Nametab.push_abbreviation (Nametab.Exactly i) sp kn;
+    Nametab.Abbrev.push (Nametab.Exactly i) sp kn;
     if not abbrev.abbrev_onlyparsing then
       (* Redeclare it to be used as (short) name in case an other (distfix)
          notation was declared in between *)
@@ -115,7 +115,7 @@ let declare_abbreviation ~local ?(also_in_cases_pattern=true) deprecation id ~on
   in
   add_leaf (inAbbreviation id (local,abbrev))
 
-let pr_abbreviation kn = pr_qualid (Nametab.shortest_qualid_of_abbreviation Id.Set.empty kn)
+let pr_abbreviation kn = pr_qualid (Nametab.Abbrev.shortest_qualid Id.Set.empty kn)
 
 let warn_deprecated_abbreviation =
   Deprecation.create_warning ~object_name:"Notation" ~warning_name:"deprecated-syntactic-definition"

interp/constrextern.ml

@@ -128,7 +128,7 @@ let _show_inactive_notations () =
       (function
        | NotationRule (inscope, ntn) ->
          Feedback.msg_notice (pr_notation ntn ++ show_scope inscope)
-       | AbbrevRule kn -> Feedback.msg_notice (str (string_of_qualid (Nametab.shortest_qualid_of_abbreviation Id.Set.empty kn))))
+       | AbbrevRule kn -> Feedback.msg_notice (str (string_of_qualid (Nametab.Abbrev.shortest_qualid Id.Set.empty kn))))
       !inactive_notations_table
 
 let deactivate_scope sc =
@@ -266,7 +266,7 @@ let path_of_global = function
   | GlobRef.ConstructRef ((ind,n),p) -> Libnames.make_path (dirpath_of_modpath (MutInd.modpath ind)) (Id.of_string_soft ("<constructor:" ^ Label.to_string (MutInd.label ind) ^ ":" ^ string_of_int n ^ ":" ^ string_of_int (p+1) ^ ">"))
 
 let default_extern_reference ?loc vars r =
-  try Nametab.shortest_qualid_of_global ?loc vars r
+  try Nametab.GlobRef.shortest_qualid ?loc vars r
   with Not_found when GlobRef.is_bound r -> qualid_of_path (path_of_global r)
 
 let my_extern_reference = ref default_extern_reference
@@ -496,7 +496,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop
       match availability_of_entry_coercion custom InConstrEntrySomeLevel with
       | None -> raise No_match
       | Some coercion ->
-      let qid = Nametab.shortest_qualid_of_abbreviation ?loc vars kn in
+      let qid = Nametab.Abbrev.shortest_qualid ?loc vars kn in
       let l1 =
         List.rev_map (fun (c,(subentry,(scopt,scl))) ->
           extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c)
@@ -861,7 +861,7 @@ let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_lo
 
 (* this helper function is copied from notation.ml as it's not exported *)
 let qualid_of_ref n =
-  n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
+  n |> Coqlib.lib_ref |> Nametab.GlobRef.shortest_qualid Id.Set.empty
 
 let q_infinity () = qualid_of_ref "num.float.infinity"
 let q_neg_infinity () = qualid_of_ref "num.float.neg_infinity"
@@ -1336,7 +1336,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
                   extern true (subentry,(scopt,scl@snd scopes)) (vars,uvars) c)
                   terms
               in
-              let cf = Nametab.shortest_qualid_of_abbreviation ?loc vars kn in
+              let cf = Nametab.Abbrev.shortest_qualid ?loc vars kn in
               let a = CRef (cf,None) in
               let args = fill_arg_scopes args argsscopes allscopes in
               let args = extern_args (extern true) (vars,uvars) args in

interp/constrintern.ml

@@ -130,7 +130,7 @@ let explain_bad_patterns_number n1 n2 =
 
 let inductive_of_record s =
   let inductive = GlobRef.IndRef (s.Structure.name) in
-  Nametab.shortest_qualid_of_global Id.Set.empty inductive
+  Nametab.GlobRef.shortest_qualid Id.Set.empty inductive
 
 let explain_field_not_a_projection field_id =
   pr_qualid field_id ++ str ": Not a projection"
@@ -797,7 +797,7 @@ let terms_of_binders bl =
     | PatVar (Name id)   -> CRef (qualid_of_ident id, None)
     | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc ()
     | PatCstr (c,l,_) ->
-       let qid = qualid_of_path ?loc (Nametab.path_of_global (GlobRef.ConstructRef c)) in
+       let qid = qualid_of_path ?loc (Nametab.GlobRef.path (GlobRef.ConstructRef c)) in
        let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in
        let params = List.make (Inductiveops.inductive_nparams (Global.env()) (fst c)) hole in
        CAppExpl ((qid,None),params @ List.map term_of_pat l)) pt in
@@ -1164,7 +1164,7 @@ let intern_sort_name ~local_univs = function
     match local with
     | Some u -> GUniv u
     | None ->
-      try GUniv (Univ.Level.make (Nametab.locate_universe qid))
+      try GUniv (Univ.Level.make (Nametab.Universe.locate qid))
       with Not_found ->
         if is_id && local_univs.unb_univs
         then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid))
@@ -2809,7 +2809,7 @@ let interp_named_context_evars ?(program_mode=false) ?(impl_env=empty_internaliz
 let known_universe_level_name evd lid =
   try Evd.universe_of_name evd lid.CAst.v
   with Not_found ->
-    let u = Nametab.locate_universe (Libnames.qualid_of_lident lid) in
+    let u = Nametab.Universe.locate (Libnames.qualid_of_lident lid) in
     Univ.Level.make u
 
 let known_glob_level evd = function

interp/dumpglob.ml

@@ -248,7 +248,7 @@ let add_glob_gen ?loc sp lib_dp ty =
 
 let add_glob ?loc ref =
   if dump () then
-    let sp = Nametab.path_of_global ref in
+    let sp = Nametab.GlobRef.path ref in
     let lib_dp = Lib.library_part ref in
     let ty = type_of_global_ref ref in
     add_glob_gen ?loc sp lib_dp ty
@@ -259,7 +259,7 @@ let mp_of_kn kn =
 
 let add_glob_kn ?loc kn =
   if dump () then
-    let sp = Nametab.path_of_abbreviation kn in
+    let sp = Nametab.Abbrev.path kn in
     let lib_dp = Names.ModPath.dp (mp_of_kn kn) in
     add_glob_gen ?loc sp lib_dp "abbrev"
 

interp/implicit_quantifiers.ml

@@ -188,7 +188,7 @@ let implicit_application env ty =
       let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in
       if Libnames.idset_mem_qualid qid env then None
       else
-        let gr = Nametab.locate qid in
+        let gr = Nametab.GlobRef.locate qid in
         if Typeclasses.is_class gr then Some (clapp, gr) else None
     with Not_found -> None
   in

interp/modintern.ml

@@ -49,12 +49,12 @@ let lookup_module_or_modtype kind qid =
   let loc = qid.CAst.loc in
   try
     if kind == ModType then raise Not_found;
-    let mp = Nametab.locate_module qid in
+    let mp = Nametab.Module.locate qid in
     Dumpglob.dump_modref ?loc mp "modtype"; (mp,Module)
   with Not_found ->
     try
       if kind == Module then raise Not_found;
-      let mp = Nametab.locate_modtype qid in
+      let mp = Nametab.ModType.locate qid in
       Dumpglob.dump_modref ?loc mp "mod"; (mp,ModType)
     with Not_found as exn ->
       let _, info = Exninfo.capture exn in

interp/notation.ml

@@ -1028,13 +1028,13 @@ module Strings = struct
 open PrimTokenNotation
 
 let qualid_of_ref n =
-  n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
+  n |> Coqlib.lib_ref |> Nametab.GlobRef.shortest_qualid Id.Set.empty
 
 let q_list () = qualid_of_ref "core.list.type"
 let q_byte () = qualid_of_ref "core.byte.type"
 
 let unsafe_locate_ind q =
-  match Nametab.locate q with
+  match Nametab.GlobRef.locate q with
   | GlobRef.IndRef i -> i
   | _ -> raise Not_found
 
@@ -1506,7 +1506,7 @@ let is_printing_inactive_rule rule pat =
   | NotationRule (scope,ntn) ->
     not (is_printing_active_in_scope (scope,ntn) pat)
   | AbbrevRule kn ->
-    try let _ = Nametab.path_of_abbreviation kn in false with Not_found -> true
+    try let _ = Nametab.Abbrev.path kn in false with Not_found -> true
 
 let availability_of_notation (ntn_scope,ntn) scopes =
   find_without_delimiters (has_active_parsing_rule_in_scope ntn) (ntn_scope,Some ntn) (make_current_scopes scopes)
@@ -2467,7 +2467,7 @@ let warn_abbreviation_not_bound_to_scope =
 
 let toggle_abbreviations ~on found ntn_pattern =
   let data_of_interp kn i =
-    let q = Nametab.shortest_qualid_of_abbreviation Id.Set.empty kn in
+    let q = Nametab.Abbrev.shortest_qualid Id.Set.empty kn in
     ((DirPath.empty, DirPath.empty), string_of_qualid q), i in
   match ntn_pattern.interp_rule_key_pattern, ntn_pattern.notation_entry_pattern, ntn_pattern.scope_pattern with
   | Some (Inr kn), [], None ->

library/coqlib.ml

@@ -74,13 +74,13 @@ let register_ref s c =
 (* Generic functions to find Coq objects *)
 
 let has_suffix_in_dirs dirs ref =
-  let dir = Libnames.dirpath (Nametab.path_of_global ref) in
+  let dir = Libnames.dirpath (Nametab.GlobRef.path ref) in
   List.exists (fun d -> Libnames.is_dirpath_prefix_of d dir) dirs
 
 let gen_reference_in_modules locstr dirs s =
   let dirs = List.map make_dir dirs in
   let qualid = Libnames.qualid_of_string s in
-  let all = Nametab.locate_all qualid in
+  let all = Nametab.GlobRef.locate_all qualid in
   let all = List.sort_uniquize GlobRef.UserOrd.compare all in
   let these = List.filter (has_suffix_in_dirs dirs) all in
   match these with
@@ -93,7 +93,7 @@ let gen_reference_in_modules locstr dirs s =
       CErrors.anomaly ~label:locstr
         Pp.(str "ambiguous name " ++ str s ++ str " can represent "
           ++ prlist_with_sep pr_comma (fun x ->
-            Libnames.pr_path (Nametab.path_of_global x)) l ++ str " in module"
+            Libnames.pr_path (Nametab.GlobRef.path x)) l ++ str " in module"
           ++ str (if List.length dirs > 1 then "s " else " ")
           ++ prlist_with_sep pr_comma DirPath.print dirs ++ str ".")
 

library/lib.ml

@@ -189,8 +189,8 @@ let start_mod is_type export id mp fs =
   in
   let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; } in
   let exists =
-    if is_type then Nametab.exists_cci (make_path id)
-    else Nametab.exists_module dir
+    if is_type then Nametab.GlobRef.exists (make_path id)
+    else Nametab.Module.exists dir
   in
   if exists then
     CErrors.user_err Pp.(Id.print id ++ str " already exists.");
@@ -373,12 +373,12 @@ let open_section id =
   let opp = !lib_state.path_prefix in
   let obj_dir = Libnames.add_dirpath_suffix opp.Nametab.obj_dir id in
   let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; } in
-  if Nametab.exists_dir obj_dir then
+  if Nametab.Dir.exists obj_dir then
     CErrors.user_err Pp.(Id.print id ++ str " already exists.");
   let fs = Summary.freeze_summaries ~marshallable:false in
   add_entry (OpenedSection (prefix, fs));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
-  Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection obj_dir));
+  Nametab.(Dir.push (Until 1) obj_dir (GlobDirRef.DirOpenSection obj_dir));
   lib_state := { !lib_state with path_prefix = prefix }
 
 (* Restore lib_stk and summaries as before the section opening, and