[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

dev/base_include

@@ -172,8 +172,13 @@ let constr_of_string s =
 open Declarations;;
 open Declareops;;
 
+let locate_constant qid =
+  match Nametab.GlobRef.locate qid with
+  | GlobRef.ConstRef c -> c
+  | _ -> raise Not_found
+
 let constbody_of_string s =
-  let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_string s)) in
+  let b = Global.lookup_constant (locate_constant (qualid_of_string s)) in
   Option.get (Global.body_of_constant_body Library.indirect_accessor b);;
 
 (* Get the current goal *)

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 ->
@@ -284,7 +284,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

@@ -898,7 +898,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

@@ -20,7 +20,8 @@ type univ_name_list = Names.lname list
 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

@@ -44,11 +44,11 @@ let toggle_abbreviation ~on ~use kn =
       | 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 =
@@ -57,23 +57,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 sp 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 *)
@@ -114,7 +114,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

@@ -200,7 +200,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
@@ -430,7 +430,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)
@@ -795,7 +795,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"
@@ -1275,7 +1275,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

@@ -120,7 +120,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"
@@ -789,7 +789,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) 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
@@ -1171,7 +1171,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))
@@ -2815,7 +2815,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
         Option.map (fun cl -> cl, clapp) (Typeclasses.class_info gr)
     with Not_found -> None
   in

interp/modintern.ml

@@ -51,12 +51,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

@@ -1041,13 +1041,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
 
@@ -1520,7 +1520,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)

library/coqlib.ml

@@ -81,13 +81,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
@@ -100,7 +100,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

@@ -355,18 +355,18 @@ module SynterpActions : LibActions with type summary = Summary.Synterp.frozen =
 
   let check_mod_fresh ~is_type prefix id =
     let exists =
-      if is_type then Nametab.exists_cci (Libnames.make_path prefix.Nametab.obj_dir id)
-      else Nametab.exists_module prefix.Nametab.obj_dir
+      if is_type then Nametab.GlobRef.exists (Libnames.make_path prefix.Nametab.obj_dir id)
+      else Nametab.Module.exists prefix.Nametab.obj_dir
     in
     if exists then
       CErrors.user_err Pp.(Id.print id ++ str " already exists.")
 
   let check_section_fresh obj_dir id =
-    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 push_section_name obj_dir =
-    Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection obj_dir))
+    Nametab.Dir.push (Until 1) obj_dir (Nametab.GlobDirRef.DirOpenSection obj_dir)
 
   let close_section fs = Summary.Synterp.unfreeze_summaries ~partial:true fs