[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 ->

interp/abbreviation.ml

@@ -33,11 +33,11 @@ let add_abbreviation kn abbrev =
   abbrev_table := KNmap.add kn abbrev !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,_) ->
@@ -49,7 +49,7 @@ let is_alias_of_already_visible_name sp = function
 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 *)

interp/constrintern.ml

@@ -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
@@ -1160,7 +1160,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))
@@ -2805,7 +2805,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.Module.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

@@ -1189,7 +1189,7 @@ 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
 
@@ -1686,7 +1686,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

@@ -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

library/nametab.ml

@@ -82,8 +82,8 @@ end
    the same object.
 *)
 module type NAMETREE = sig
-  type elt
   type t
+  type elt
   type user_name
 
   val empty : t
@@ -317,6 +317,7 @@ module ExtRefEqual = Globnames.ExtRefOrdered
 module MPEqual = Names.ModPath
 
 module ExtRefTab = Make(FullPath)(ExtRefEqual)
+
 module MPTab = Make(FullPath)(MPEqual)
 
 type ccitab = ExtRefTab.t
@@ -331,14 +332,17 @@ struct
 end
 
 module MPDTab = Make(DirPath')(MPEqual)
+
 module DirTab = Make(DirPath')(GlobDirRef)
 
 module UnivIdEqual =
 struct
   type t = Univ.UGlobal.t
   let equal = Univ.UGlobal.equal
 end
+
 module UnivTab = Make(FullPath)(UnivIdEqual)
+
 type univtab = UnivTab.t
 let the_univtab = Summary.ref ~name:"univtab" (UnivTab.empty : univtab)
 
@@ -425,7 +429,7 @@ let push_cci visibility sp ref =
 let push_abbreviation visibility sp kn =
   push_xref visibility sp (Abbrev kn)
 
-let push = push_cci
+let _push = push_cci
 
 let push_modtype vis sp kn =
   let open Modules in
@@ -495,11 +499,11 @@ let locate_all qid =
 
 let locate_extended_all qid = ExtRefTab.find_prefixes qid !the_ccitab
 
-let locate_extended_all_dir qid = DirTab.find_prefixes qid Modules.(!nametab.dirtab)
+let _locate_extended_all_dir qid = DirTab.find_prefixes qid Modules.(!nametab.dirtab)
 
-let locate_extended_all_modtype qid = MPTab.find_prefixes qid Modules.(!nametab.modtypetab)
+let _locate_extended_all_modtype qid = MPTab.find_prefixes qid Modules.(!nametab.modtypetab)
 
-let locate_extended_all_module qid = MPDTab.find_prefixes qid Modules.(!nametab.modtab)
+let _locate_extended_all_module qid = MPDTab.find_prefixes qid Modules.(!nametab.modtab)
 
 (* Completion *)
 let completion_canditates qualid =
@@ -560,7 +564,7 @@ let basename_of_global ref =
 let path_of_abbreviation kn =
   Globnames.ExtRefMap.find (Abbrev kn) !the_globrevtab
 
-let dirpath_of_module mp =
+let _dirpath_of_module mp =
   MPmap.find mp Modules.(!nametab.modrevtab)
 
 let path_of_modtype mp =
@@ -609,3 +613,80 @@ let global_inductive qid =
   | ref ->
       CErrors.user_err ?loc:qid.CAst.loc
         Pp.(pr_qualid qid ++ spc () ++ str "is not an inductive type.")
+
+(** Type of nametabs (imperative) *)
+module type S = sig
+
+  type elt
+  type path
+
+  val push : visibility -> path -> elt -> unit
+  val locate : qualid -> elt
+  val locate_all : qualid -> elt list
+  val exists : path -> bool
+  val path : elt -> path
+
+  (* future work *)
+  (* val shortest_qualid : *)
+end
+
+module GlobRef_ = GlobRef
+module GlobRef : S
+  with type elt := GlobRef.t and type path := full_path =
+struct
+  let push = push_cci
+  let locate = locate
+  let locate_all = locate_all
+  let exists = exists_cci
+  let path = path_of_global
+end
+
+module Abbrev : S
+  with type elt := Globnames.abbreviation and type path := full_path =
+struct
+  let push = push_abbreviation
+  let locate = locate_abbreviation
+  let locate_all x = locate_extended_all x |> List.filter_map (fun x -> match x with Globnames.Abbrev a -> Some a | _ -> None)
+  let exists = exists_cci
+  let path = path_of_abbreviation
+end
+
+module ModType : S
+  with type elt := ModPath.t and type path := full_path =
+struct
+  let push = push_modtype
+  let locate = locate_modtype
+  let locate_all = Obj.magic
+  let exists = exists_modtype
+  let path = path_of_modtype
+end
+
+module Module : S
+  with type elt := ModPath.t and type path := DirPath.t =
+struct
+  let push = push_module
+  let locate = locate_module
+  let locate_all = Obj.magic
+  let exists = exists_module
+  let path = Obj.magic
+end
+
+module Dir : S
+  with type elt := GlobDirRef.t and type path := DirPath.t =
+struct
+  let push = push_dir
+  let locate = locate_dir
+  let locate_all = Obj.magic
+  let exists = exists_dir
+  let path = Obj.magic
+end
+
+module Universe : S
+  with type elt := Univ.UGlobal.t and type path := full_path =
+struct
+  let push = push_universe
+  let locate = locate_universe
+  let locate_all = Obj.magic
+  let exists = exists_universe
+  let path = path_of_universe
+end