From 2172958a1f212da7c0770ceffc215cbbf5434a73 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 3 Sep 2022 15:57:35 +0200 Subject: [PATCH] [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 https://github.com/coq/coq/pull/16746 and https://github.com/coq/ceps/pull/65 --- dev/base_include | 7 +- engine/namegen.ml | 6 +- engine/termops.ml | 2 +- engine/univNames.ml | 3 +- interp/abbreviation.ml | 16 +- interp/constrextern.ml | 8 +- interp/constrintern.ml | 8 +- interp/dumpglob.ml | 4 +- interp/implicit_quantifiers.ml | 2 +- interp/modintern.ml | 4 +- interp/notation.ml | 6 +- library/coqlib.ml | 6 +- library/lib.ml | 8 +- library/nametab.ml | 533 ++++++++++-------- library/nametab.mli | 147 +++-- plugins/extraction/extract_env.ml | 2 +- plugins/extraction/table.ml | 6 +- .../funind/functional_principles_proofs.ml | 2 +- plugins/funind/indfun_common.ml | 8 +- plugins/funind/recdef.ml | 7 +- plugins/ltac/tacentries.ml | 2 +- plugins/ltac/tacintern.ml | 2 +- plugins/ltac2/tac2core.ml | 6 +- plugins/micromega/zify.ml | 2 +- plugins/syntax/number.ml | 10 +- plugins/syntax/string_notation.ml | 4 +- pretyping/coercionops.ml | 8 +- pretyping/glob_ops.ml | 2 +- pretyping/indrec.ml | 2 +- pretyping/tacred.ml | 2 +- tactics/hints.ml | 2 +- tactics/ind_tables.ml | 2 +- vernac/comInductive.ml | 4 +- vernac/declare.ml | 10 +- vernac/declareInd.ml | 6 +- vernac/declareUctx.ml | 2 +- vernac/declareUniv.ml | 4 +- vernac/declaremods.ml | 52 +- vernac/himsg.ml | 4 +- vernac/prettyp.ml | 42 +- vernac/printmod.ml | 16 +- vernac/search.ml | 8 +- vernac/synterp.ml | 2 +- vernac/vernacentries.ml | 20 +- 44 files changed, 523 insertions(+), 476 deletions(-) diff --git a/dev/base_include b/dev/base_include index 993b72b95756e..9f0572b213a48 100644 --- a/dev/base_include +++ b/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 *) diff --git a/engine/namegen.ml b/engine/namegen.ml index c2e47ef0d9158..179b8697d80e3 100644 --- a/engine/namegen.ml +++ b/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 diff --git a/engine/termops.ml b/engine/termops.ml index 03249ddee0f26..abcb7b90ae2d9 100644 --- a/engine/termops.ml +++ b/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) diff --git a/engine/univNames.ml b/engine/univNames.ml index 16fd451fe1071..5f4501a6360f4 100644 --- a/engine/univNames.ml +++ b/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 diff --git a/interp/abbreviation.ml b/interp/abbreviation.ml index cff329409cd9b..8e3192cc1fc12 100644 --- a/interp/abbreviation.ml +++ b/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,15 +57,15 @@ 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 @@ -73,7 +73,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 *) @@ -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" diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 6b7ba1a0c30b8..c2939d2d41bb0 100644 --- a/interp/constrextern.ml +++ b/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 ("")) 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 diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 9e2a9f09528ec..eae32e54ec924 100644 --- a/interp/constrintern.ml +++ b/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 diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index adb405e2f8768..e3615e78adf20 100644 --- a/interp/dumpglob.ml +++ b/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" diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index a2dadb64151cf..43277f82d82b2 100644 --- a/interp/implicit_quantifiers.ml +++ b/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 diff --git a/interp/modintern.ml b/interp/modintern.ml index 2dd31ee5b43a2..28bc32690c357 100644 --- a/interp/modintern.ml +++ b/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 diff --git a/interp/notation.ml b/interp/notation.ml index 0941af19e9c4c..e8aeeeecef690 100644 --- a/interp/notation.ml +++ b/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) diff --git a/library/coqlib.ml b/library/coqlib.ml index dd5caef5b9169..08c84390e9d44 100644 --- a/library/coqlib.ml +++ b/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 ".") diff --git a/library/lib.ml b/library/lib.ml index f249b18e41af3..6507222132777 100644 --- a/library/lib.ml +++ b/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 diff --git a/library/nametab.ml b/library/nametab.ml index 9c2206a8b0052..44060beafe19f 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -11,6 +11,7 @@ open Names open Libnames +(* Shadowing help *) type object_prefix = { obj_dir : DirPath.t; obj_mp : ModPath.t; @@ -82,8 +83,8 @@ end the same object. *) module type NAMETREE = sig - type elt type t + type elt type user_name val empty : t @@ -347,7 +348,34 @@ let match_prefixes = end -(* Global name tables *************************************************) +(** Type of nametabs (imperative) *) +module type S = sig + + type elt + type path + + val push : visibility -> path -> elt -> unit + val remove : path -> elt -> unit + val locate : qualid -> elt + val locate_all : qualid -> elt list + val exists : path -> bool + + (* future work *) + (* val shortest_qualid : *) +end + +module type SR = sig + include S + val path : elt -> path + val shortest_qualid : ?loc:Loc.t -> Names.Id.Set.t -> elt -> qualid +end + +(***********************************************************************) +(* For Global References *) + +(* This is for permanent constructions (never discharged -- but with + possibly limited visibility, i.e. Theorem, Lemma, Definition, + Axiom, Parameter but also Remark and Fact) *) module FullPath = struct @@ -356,309 +384,338 @@ struct let to_string = string_of_path let repr sp = let dir,id = repr_path sp in - id, (DirPath.repr dir) + id, (DirPath.repr dir) end module ExtRefEqual = Globnames.ExtRefOrdered -module MPEqual = Names.ModPath - module ExtRefTab = Make(FullPath)(ExtRefEqual) -module MPTab = Make(FullPath)(MPEqual) - type ccitab = ExtRefTab.t let the_ccitab = Summary.ref ~name:"ccitab" (ExtRefTab.empty : ccitab) -module DirPath' = -struct - include DirPath - let repr dir = match DirPath.repr dir with - | [] -> CErrors.anomaly (Pp.str "Empty dirpath.") - | id :: l -> (id, l) -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) - -(* Reversed name tables ***************************************************) - (* This table translates extended_global_references back to section paths *) type globrevtab = full_path Globnames.ExtRefMap.t let the_globrevtab = Summary.ref ~name:"globrevtab" (Globnames.ExtRefMap.empty : globrevtab) +let extended_global_of_path sp = ExtRefTab.find sp !the_ccitab -type mprevtab = DirPath.t MPmap.t - -type mptrevtab = full_path MPmap.t - -module UnivIdOrdered = -struct - type t = Univ.UGlobal.t - let hash = Univ.UGlobal.hash - let compare = Univ.UGlobal.compare -end - -module UnivIdMap = HMap.Make(UnivIdOrdered) - -type univrevtab = full_path UnivIdMap.t -let the_univrevtab = Summary.ref ~name:"univrevtab" (UnivIdMap.empty : univrevtab) - -(** Module-related nametab *) -module Modules = struct - - type t = { - modtypetab : MPTab.t; - modtab : MPDTab.t; - dirtab : DirTab.t; - modrevtab : mprevtab; - modtyperevtab : mptrevtab; - } - - let initial = { - modtypetab = MPTab.empty; - modtab = MPDTab.empty; - dirtab = DirTab.empty; - modrevtab = MPmap.empty; - modtyperevtab = MPmap.empty - } - - let nametab, summary_tag = - Summary.ref_tag ~stage:Summary.Stage.Synterp ~name:"MODULES-NAMETAB" initial - - let freeze () = !nametab - let unfreeze v = nametab := v - -end - -(* Push functions *********************************************************) - -(* This is for permanent constructions (never discharged -- but with - possibly limited visibility, i.e. Theorem, Lemma, Definition, Axiom, - Parameter but also Remark and Fact) *) - -let push_xref visibility sp xref = +let push_xref visibility (sp : Libnames.full_path) (xref : Globnames.extended_global_reference) = match visibility with - | Until _ -> + | Until _ -> + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; + the_globrevtab := Globnames.ExtRefMap.add xref sp !the_globrevtab + | _ -> + begin + if ExtRefTab.exists sp !the_ccitab then + let open GlobRef in + match extended_global_of_path sp with + | TrueGlobal( ConstRef _) + | TrueGlobal( IndRef _) + | TrueGlobal( ConstructRef _) as xref -> + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; + | TrueGlobal( VarRef _ ) + | Abbrev _ -> + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; + else the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; - the_globrevtab := Globnames.ExtRefMap.add xref sp !the_globrevtab - | _ -> - begin - if ExtRefTab.exists sp !the_ccitab then - let open GlobRef in - match ExtRefTab.find sp !the_ccitab with - | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) | - TrueGlobal( ConstructRef _) as xref -> - the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; - | _ -> - the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; - else - the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; - end - -let remove_xref sp xref = + end + +let remove_xref (sp : Libnames.full_path) (xref : Globnames.extended_global_reference) : unit = the_ccitab := ExtRefTab.remove sp !the_ccitab; the_globrevtab := Globnames.ExtRefMap.remove xref !the_globrevtab -let push_cci visibility sp ref = - push_xref visibility sp (TrueGlobal ref) +(* This should be used when syntactic definitions are allowed *) +let locate_extended qid = ExtRefTab.locate qid !the_ccitab +let locate_extended_all qid = ExtRefTab.find_prefixes qid !the_ccitab +let full_name_cci qid = ExtRefTab.user_name qid !the_ccitab -(* This is for Syntactic Definitions *) -let push_abbreviation visibility sp kn = - push_xref visibility sp (Abbrev kn) +module GlobRef : SR + with type elt := GlobRef.t and type path := full_path = +struct -let remove_abbreviation sp kn = - remove_xref sp (Abbrev kn) + let push visibility sp ref = + push_xref visibility sp (TrueGlobal ref) -let push = push_cci + let remove sp ref = remove_xref sp (TrueGlobal ref) -let push_modtype vis sp kn = - let open Modules in - nametab := { !nametab with - modtypetab = MPTab.push vis sp kn !nametab.modtypetab; - modtyperevtab = MPmap.add kn sp !nametab.modtyperevtab; - } + (* This should be used when no syntactic definitions is expected *) + let locate qid = match locate_extended qid with + | TrueGlobal ref -> ref + | Abbrev _ -> raise Not_found -let push_module vis dir mp = - let open Modules in - nametab := { !nametab with - modtab = MPDTab.push vis dir mp !nametab.modtab; - modrevtab = MPmap.add mp dir !nametab.modrevtab; - } + let locate_all qid = + locate_extended_all qid + |> List.filter_map (fun x -> match x with Globnames.TrueGlobal a -> Some a | _ -> None) -(* This is to remember absolute Section/Module names and to avoid redundancy *) -let push_dir vis dir dir_ref = - let open Modules in - nametab := { !nametab with - dirtab = DirTab.push vis dir dir_ref !Modules.nametab.dirtab; - } + let exists sp = ExtRefTab.exists sp !the_ccitab + let path ref = + let open GlobRef in + match ref with + | VarRef id -> make_path DirPath.empty id + | _ -> Globnames.ExtRefMap.find (TrueGlobal ref) !the_globrevtab -(* This is for global universe names *) + (* XXX: refactor with the above *) + let shortest_qualid ?loc ctx ref = + match ref with + | GlobRef.VarRef id -> make_qualid ?loc DirPath.empty id + | _ -> + let sp = Globnames.ExtRefMap.find (TrueGlobal ref) !the_globrevtab in + ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab +end -let push_universe vis sp univ = - the_univtab := UnivTab.push vis sp univ !the_univtab; - the_univrevtab := UnivIdMap.add univ sp !the_univrevtab +(* Completion *) +let completion_canditates qualid = ExtRefTab.match_prefixes qualid !the_ccitab -(* Locate functions *******************************************************) +(* Derived functions *) +let locate_constant qid = + match GlobRef.locate qid with + | ConstRef kn -> kn + | _ -> raise Not_found +let global_of_path sp = + match extended_global_of_path sp with + | TrueGlobal ref -> ref + | _ -> raise Not_found -(* This should be used when abbreviations are allowed *) -let locate_extended qid = ExtRefTab.locate qid !the_ccitab +let global qid = + try match locate_extended qid with + | TrueGlobal ref -> ref + | Abbrev _ -> + CErrors.user_err ?loc:qid.CAst.loc + Pp.(str "Unexpected reference to a notation: " ++ + pr_qualid qid ++ str ".") + with + | Not_found as exn -> + let _, info = Exninfo.capture exn in + error_global_not_found ~info qid -(* This should be used when no abbreviations are expected *) -let locate qid = match locate_extended qid with - | TrueGlobal ref -> ref - | Abbrev _ -> raise Not_found -let full_name_cci qid = ExtRefTab.user_name qid !the_ccitab +let pr_global_env env ref = + try pr_qualid (GlobRef.shortest_qualid env ref) + with Not_found as exn -> + let exn, info = Exninfo.capture exn in + if CDebug.(get_flag misc) then Feedback.msg_debug (Pp.str "pr_global_env not found"); + Exninfo.iraise (exn, info) -let locate_abbreviation qid = match locate_extended qid with - | TrueGlobal _ -> raise Not_found - | Abbrev kn -> kn +let global_inductive qid = + match global qid with + | IndRef ind -> ind + | ref -> + CErrors.user_err ?loc:qid.CAst.loc + Pp.(pr_qualid qid ++ spc () ++ str "is not an inductive type.") -let locate_modtype qid = MPTab.locate qid Modules.(!nametab.modtypetab) -let full_name_modtype qid = MPTab.user_name qid Modules.(!nametab.modtypetab) +(* Reverse locate functions ***********************************************) +let dirpath_of_global ref = fst (repr_path (GlobRef.path ref)) +let basename_of_global ref = snd (repr_path (GlobRef.path ref)) -let locate_universe qid = UnivTab.locate qid !the_univtab +(***********************************************************************) +(* Syntactic Definitions. *) +module Abbrev : SR + with type elt := Globnames.abbreviation and type path := full_path = +struct -let locate_dir qid = DirTab.locate qid Modules.(!nametab.dirtab) + let push visibility sp kn = push_xref visibility sp (Abbrev kn) -let locate_module qid = MPDTab.locate qid Modules.(!nametab.modtab) + let remove sp kn = remove_xref sp (Abbrev kn) -let full_name_module qid = MPDTab.user_name qid Modules.(!nametab.modtab) + let locate qid = match locate_extended qid with + | TrueGlobal _ -> raise Not_found + | Abbrev kn -> kn -let locate_section qid = - match locate_dir qid with - | GlobDirRef.DirOpenSection dir -> dir - | _ -> raise Not_found + let locate_all qid = + locate_extended_all qid + |> List.filter_map (fun x -> match x with Globnames.Abbrev a -> Some a | _ -> None) -let locate_all qid = - List.fold_right (fun a l -> - match a with - | Globnames.TrueGlobal a -> a::l - | _ -> l) - (ExtRefTab.find_prefixes qid !the_ccitab) [] + let exists sp = ExtRefTab.exists sp !the_ccitab + let path kn = Globnames.ExtRefMap.find (Abbrev kn) !the_globrevtab -let locate_extended_all qid = ExtRefTab.find_prefixes qid !the_ccitab + let shortest_qualid ?loc ctx kn = + let sp = path kn in + ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab +end -let locate_extended_all_dir qid = DirTab.find_prefixes qid Modules.(!nametab.dirtab) +(***********************************************************************) +(* For modules *) +module MPEqual = Names.ModPath +module MPTab = Make(FullPath)(MPEqual) -let locate_extended_all_modtype qid = MPTab.find_prefixes qid Modules.(!nametab.modtypetab) +module DirPath' = +struct + include DirPath + let repr dir = match DirPath.repr dir with + | [] -> CErrors.anomaly (Pp.str "Empty dirpath.") + | id :: l -> (id, l) +end -let locate_extended_all_module qid = MPDTab.find_prefixes qid Modules.(!nametab.modtab) +module MPDTab = Make(DirPath')(MPEqual) +module DirTab = Make(DirPath')(GlobDirRef) -(* Completion *) -let completion_canditates qualid = - ExtRefTab.match_prefixes qualid !the_ccitab +(** Module-related nametab *) +module Modules = struct -(* Derived functions *) + type t = + { modtypetab : MPTab.t + ; modtyperevtab : full_path MPmap.t -let locate_constant qid = - let open GlobRef in - match locate_extended qid with - | TrueGlobal (ConstRef kn) -> kn - | _ -> raise Not_found + ; modtab : MPDTab.t + ; modrevtab : DirPath.t MPmap.t -let global_of_path sp = - match ExtRefTab.find sp !the_ccitab with - | TrueGlobal ref -> ref - | _ -> raise Not_found + ; dirtab : DirTab.t + } -let extended_global_of_path sp = ExtRefTab.find sp !the_ccitab + let initial = + { modtypetab = MPTab.empty + ; modtyperevtab = MPmap.empty + ; modtab = MPDTab.empty + ; modrevtab = MPmap.empty + ; dirtab = DirTab.empty + } -let global qid = - try match locate_extended qid with - | TrueGlobal ref -> ref - | Abbrev _ -> - CErrors.user_err ?loc:qid.CAst.loc - Pp.(str "Unexpected reference to a notation: " ++ - pr_qualid qid ++ str ".") - with Not_found as exn -> - let _, info = Exninfo.capture exn in - error_global_not_found ~info qid + let nametab, summary_tag = + Summary.ref_tag ~stage:Summary.Stage.Synterp ~name:"MODULES-NAMETAB" initial -(* Exists functions ********************************************************) + let freeze () = !nametab + let unfreeze v = nametab := v -let exists_cci sp = ExtRefTab.exists sp !the_ccitab +end -let exists_dir dir = DirTab.exists dir Modules.(!nametab.dirtab) +(***********************************************************************) +(* Module types *) +module ModType : SR + with type elt := ModPath.t and type path := full_path = +struct + let push vis sp kn = + let open Modules in + nametab := { !nametab with + modtypetab = MPTab.push vis sp kn !nametab.modtypetab + ; modtyperevtab = MPmap.add kn sp !nametab.modtyperevtab + } + + let remove sp kn = + let open Modules in + nametab := { !nametab with + modtypetab = MPTab.remove sp !nametab.modtypetab + ; modtyperevtab = MPmap.remove kn !nametab.modtyperevtab + } + + let locate qid = MPTab.locate qid Modules.(!nametab.modtypetab) + let locate_all qid = MPTab.find_prefixes qid Modules.(!nametab.modtypetab) + + let exists sp = MPTab.exists sp Modules.(!nametab.modtypetab) + let path mp = MPmap.find mp Modules.(!nametab.modtyperevtab) + let shortest_qualid ?loc ctx kn = + let sp = path kn in + MPTab.shortest_qualid ?loc ctx sp Modules.(!nametab.modtypetab) +end -let exists_module dir = MPDTab.exists dir Modules.(!nametab.modtab) +(***********************************************************************) +(* Module implementations *) +module Module : SR + with type elt := ModPath.t and type path := DirPath.t = +struct + let push vis dir mp = + let open Modules in + nametab := { !nametab with + modtab = MPDTab.push vis dir mp !nametab.modtab + ; modrevtab = MPmap.add mp dir !nametab.modrevtab; + } -let exists_modtype sp = MPTab.exists sp Modules.(!nametab.modtypetab) + let remove dir mp = + let open Modules in + nametab := { !nametab with + modtab = MPDTab.remove dir !nametab.modtab + ; modrevtab = MPmap.remove mp !nametab.modrevtab; + } -let exists_universe kn = UnivTab.exists kn !the_univtab + let locate qid = MPDTab.locate qid Modules.(!nametab.modtab) -(* Reverse locate functions ***********************************************) + let locate_all qid = MPDTab.find_prefixes qid Modules.(!nametab.modtab) -let path_of_global ref = - let open GlobRef in - match ref with - | VarRef id -> make_path DirPath.empty id - | _ -> Globnames.ExtRefMap.find (TrueGlobal ref) !the_globrevtab + let exists dir = MPDTab.exists dir Modules.(!nametab.modtab) + + let path mp = MPmap.find mp Modules.(!nametab.modrevtab) -let dirpath_of_global ref = - fst (repr_path (path_of_global ref)) + let shortest_qualid ?loc ctx mp = + let dir = path mp in + MPDTab.shortest_qualid ?loc ctx dir Modules.(!nametab.modtab) -let basename_of_global ref = - snd (repr_path (path_of_global ref)) +end -let path_of_abbreviation kn = - Globnames.ExtRefMap.find (Abbrev kn) !the_globrevtab -let dirpath_of_module mp = - MPmap.find mp Modules.(!nametab.modrevtab) +(***********************************************************************) +(* For ... *) +module Dir : S + with type elt := GlobDirRef.t and type path := DirPath.t = +struct -let path_of_modtype mp = - MPmap.find mp Modules.(!nametab.modtyperevtab) + (* This is to remember absolute Section/Module names and to avoid redundancy *) + let push vis dir dir_ref = + let open Modules in + nametab := { !nametab with + dirtab = DirTab.push vis dir dir_ref !Modules.nametab.dirtab + } + + let remove dir dir_ref = + let open Modules in + nametab := { !nametab with + dirtab = DirTab.remove dir !Modules.nametab.dirtab + } + + let locate qid = DirTab.locate qid Modules.(!nametab.dirtab) + let locate_all qid = DirTab.find_prefixes qid Modules.(!nametab.dirtab) + let exists dir = DirTab.exists dir Modules.(!nametab.dirtab) +end -let path_of_universe mp = - UnivIdMap.find mp !the_univrevtab +let locate_section qid = + match Dir.locate qid with + | GlobDirRef.DirOpenSection dir -> dir + | _ -> raise Not_found -(* Shortest qualid functions **********************************************) +(* Aux *) +let full_name_modtype qid = MPTab.user_name qid Modules.(!nametab.modtypetab) +let full_name_module qid = MPDTab.user_name qid Modules.(!nametab.modtab) -let shortest_qualid_of_global ?loc ctx ref = - let open GlobRef in - match ref with - | VarRef id -> make_qualid ?loc DirPath.empty id - | _ -> - let sp = Globnames.ExtRefMap.find (TrueGlobal ref) !the_globrevtab in - ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab +(***********************************************************************) +(* For global universe names *) +module UnivIdEqual = +struct + type t = Univ.UGlobal.t + let equal = Univ.UGlobal.equal +end -let shortest_qualid_of_abbreviation ?loc ctx kn = - let sp = path_of_abbreviation kn in - ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab +module UnivTab = Make(FullPath)(UnivIdEqual) -let shortest_qualid_of_module ?loc mp = - let dir = MPmap.find mp Modules.(!nametab.modrevtab) in - MPDTab.shortest_qualid ?loc Id.Set.empty dir Modules.(!nametab.modtab) +type univtab = UnivTab.t +let the_univtab = Summary.ref ~name:"univtab" (UnivTab.empty : univtab) -let shortest_qualid_of_modtype ?loc kn = - let sp = MPmap.find kn Modules.(!nametab.modtyperevtab) in - MPTab.shortest_qualid ?loc Id.Set.empty sp Modules.(!nametab.modtypetab) +module UnivIdOrdered = +struct + type t = Univ.UGlobal.t + let hash = Univ.UGlobal.hash + let compare = Univ.UGlobal.compare +end -let shortest_qualid_of_universe ?loc ctx kn = - let sp = UnivIdMap.find kn !the_univrevtab in - UnivTab.shortest_qualid_gen ?loc (fun id -> Id.Map.mem id ctx) sp !the_univtab +(* Reverse map *) +module UnivIdMap = HMap.Make(UnivIdOrdered) -let pr_global_env env ref = - try pr_qualid (shortest_qualid_of_global env ref) - with Not_found as exn -> - let exn, info = Exninfo.capture exn in - if CDebug.(get_flag misc) then Feedback.msg_debug (Pp.str "pr_global_env not found"); - Exninfo.iraise (exn, info) +type univrevtab = full_path UnivIdMap.t +let the_univrevtab = Summary.ref ~name:"univrevtab" (UnivIdMap.empty : univrevtab) -let global_inductive qid = - let open GlobRef in - match global qid with - | IndRef ind -> ind - | ref -> - CErrors.user_err ?loc:qid.CAst.loc - Pp.(pr_qualid qid ++ spc () ++ str "is not an inductive type.") +module Universe : SR + with type elt := Univ.UGlobal.t and type path := full_path = +struct + let push vis sp univ = + the_univtab := UnivTab.push vis sp univ !the_univtab; + the_univrevtab := UnivIdMap.add univ sp !the_univrevtab + + let remove sp univ = + the_univtab := UnivTab.remove sp !the_univtab; + the_univrevtab := UnivIdMap.remove univ !the_univrevtab + + let locate qid = UnivTab.locate qid !the_univtab + let locate_all = Obj.magic + let exists kn = UnivTab.exists kn !the_univtab + let path mp = UnivIdMap.find mp !the_univrevtab + let shortest_qualid ?loc ctx kn = + let sp = path kn in + UnivTab.shortest_qualid_gen ?loc (fun id -> Id.Set.mem id ctx) sp !the_univtab +end diff --git a/library/nametab.mli b/library/nametab.mli index b5f0492b5bdc1..ef65de9d200a6 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -99,100 +99,59 @@ val error_global_not_found : info:Exninfo.info -> qualid -> 'a containing ...) the object is opened (imported) *) - type visibility = Until of int | Exactly of int val map_visibility : (int -> int) -> visibility -> visibility -val push : visibility -> full_path -> GlobRef.t -> unit -val push_modtype : visibility -> full_path -> ModPath.t -> unit -val push_module : visibility -> DirPath.t -> ModPath.t -> unit -val push_dir : visibility -> DirPath.t -> GlobDirRef.t -> unit -val push_abbreviation : visibility -> full_path -> Globnames.abbreviation -> unit +(** Type of imperative nametabs *) +module type S = sig -module UnivIdMap : CMap.ExtS with type key = Univ.UGlobal.t + type elt + type path -val push_universe : visibility -> full_path -> Univ.UGlobal.t -> unit + val push : visibility -> path -> elt -> unit + val remove : path -> elt -> unit + val locate : qualid -> elt + val locate_all : qualid -> elt list + val exists : path -> bool +end -(** {6 The following functions perform globalization of qualified names } *) +(** {6 Reverse lookup } + Finding user names corresponding to the given + internal name *) -(** These functions globalize a (partially) qualified name or fail with - [Not_found] *) +(** Type of imperative nametabs with reverse resolution *) +module type SR = sig + include S -val locate : qualid -> GlobRef.t -val locate_extended : qualid -> Globnames.extended_global_reference -val locate_constant : qualid -> Constant.t -val locate_abbreviation : qualid -> Globnames.abbreviation -val locate_modtype : qualid -> ModPath.t -val locate_dir : qualid -> GlobDirRef.t -val locate_module : qualid -> ModPath.t -val locate_section : qualid -> DirPath.t -val locate_universe : qualid -> Univ.UGlobal.t + (** [path] Returns the full path bound to a [elt], and the (full) + [path] associated to it *) + val path : elt -> path + + (** The [shortest_qualid] functions given an object with [user_name] + Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and + Coq.A.B.x that denotes the same object. + @raise Not_found for unknown objects. *) + val shortest_qualid : ?loc:Loc.t -> Names.Id.Set.t -> elt -> qualid +end -(** Remove the binding to an abbreviation *) +(***********************************************************************) +(** Nametab for [GlobRef.t] *) -val remove_abbreviation : full_path -> Globnames.abbreviation -> unit +(** Helper *) +val locate_constant : qualid -> Constant.t (** These functions globalize user-level references into global references, like [locate] and co, but raise a nice error message in case of failure *) - val global : qualid -> GlobRef.t val global_inductive : qualid -> inductive -(** These functions locate all global references with a given suffix; - if [qualid] is valid as such, it comes first in the list *) - -val locate_all : qualid -> GlobRef.t list -val locate_extended_all : qualid -> Globnames.extended_global_reference list -val locate_extended_all_dir : qualid -> GlobDirRef.t list -val locate_extended_all_modtype : qualid -> ModPath.t list -val locate_extended_all_module : qualid -> ModPath.t list - -(** Experimental completion support, API is _unstable_ *) -val completion_canditates : qualid -> Globnames.extended_global_reference list -(** [completion_canditates qualid] will return the list of global - references that have [qualid] as a prefix. UI usually will want to - compose this with [shortest_qualid_of_global] *) - (** Mapping a full path to a global reference *) - val global_of_path : full_path -> GlobRef.t -val extended_global_of_path : full_path -> Globnames.extended_global_reference - -(** {6 These functions tell if the given absolute name is already taken } *) - -val exists_cci : full_path -> bool -val exists_modtype : full_path -> bool -val exists_module : DirPath.t -> bool -val exists_dir : DirPath.t -> bool -val exists_universe : full_path -> bool - -(** {6 These functions locate qualids into full user names } *) - -val full_name_cci : qualid -> full_path -val full_name_modtype : qualid -> full_path -val full_name_module : qualid -> DirPath.t - -(** {6 Reverse lookup } - Finding user names corresponding to the given - internal name *) - -(** Returns the full path bound to a global reference or syntactic - definition, and the (full) dirpath associated to a module path *) - -val path_of_abbreviation : Globnames.abbreviation -> full_path -val path_of_global : GlobRef.t -> full_path -val dirpath_of_module : ModPath.t -> DirPath.t -val path_of_modtype : ModPath.t -> full_path - -(** A universe_id might not be registered with a corresponding user name. - @raise Not_found if the universe was not introduced by the user. *) -val path_of_universe : Univ.UGlobal.t -> full_path (** Returns in particular the dirpath or the basename of the full path associated to global reference *) - val dirpath_of_global : GlobRef.t -> DirPath.t val basename_of_global : GlobRef.t -> Id.t @@ -200,19 +159,45 @@ val basename_of_global : GlobRef.t -> Id.t @raise Not_found when the reference is not in the global tables. *) val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t +module GlobRef : SR with type elt := GlobRef.t and type path := full_path + +(***********************************************************************) +(** Abbreviations *) +module Abbrev : SR with type elt := Globnames.abbreviation and type path := full_path + +(***********************************************************************) +(** Common functions for Global Refs and abbreviations *) + +(** These functions locate all global references with a given suffix; + if [qualid] is valid as such, it comes first in the list *) +val locate_extended : qualid -> Globnames.extended_global_reference +val locate_extended_all : qualid -> Globnames.extended_global_reference list +val extended_global_of_path : full_path -> Globnames.extended_global_reference + +(** Locate qualids into full user names *) +val full_name_cci : qualid -> full_path + +(** [completion_canditates qualid] will return the list of global + references that have [qualid] as a prefix. UI usually will want to + compose this with [shortest_qualid_of_global]. + Experimental API, note that it is _unstable_ *) +val completion_canditates : qualid -> Globnames.extended_global_reference list -(** The [shortest_qualid] functions given an object with [user_name] - Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and - Coq.A.B.x that denotes the same object. - @raise Not_found for unknown objects. *) +(***********************************************************************) +(** Modules *) +module ModType : SR with type elt := ModPath.t and type path := full_path +val full_name_modtype : qualid -> full_path -val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid -val shortest_qualid_of_abbreviation : ?loc:Loc.t -> Id.Set.t -> Globnames.abbreviation -> qualid -val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid -val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid +module Module : SR with type elt := ModPath.t and type path := DirPath.t +val full_name_module : qualid -> DirPath.t + +module Dir : S with type elt := GlobDirRef.t and type path := DirPath.t +val locate_section : qualid -> DirPath.t -(** In general we have a [UnivNames.universe_binders] around rather than a [Id.Set.t] *) -val shortest_qualid_of_universe : ?loc:Loc.t -> 'u Id.Map.t -> Univ.UGlobal.t -> qualid +(** Note for [Universe.path]: A universe_id might not be registered + with a corresponding user name. @raise Not_found if the universe + was not introduced by the user. *) +module Universe : SR with type elt := Univ.UGlobal.t and type path := full_path (** {5 Generic name handling} *) diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 34f3a892afafd..fa7140be05cb3 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -583,7 +583,7 @@ let warns () = let rec locate_ref = function | [] -> [],[] | qid::l -> - let mpo = try Some (Nametab.locate_module qid) with Not_found -> None + let mpo = try Some (Nametab.Module.locate qid) with Not_found -> None and ro = try Some (Smartlocate.global_with_alias qid) with Nametab.GlobalizationError _ | UserError _ -> None diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 7b0a0dc031082..74b942389272a 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -276,7 +276,7 @@ let safe_basename_of_global r = | VarRef v -> v let string_of_global r = - try string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty r) + try string_of_qualid (Nametab.GlobRef.shortest_qualid Id.Set.empty r) with Not_found -> Id.to_string (safe_basename_of_global r) let safe_pr_global r = str (string_of_global r) @@ -292,10 +292,10 @@ let safe_pr_long_global r = | _ -> assert false let pr_long_mp mp = - let lid = DirPath.repr (Nametab.dirpath_of_module mp) in + let lid = DirPath.repr (Nametab.Module.path mp) in str (String.concat "." (List.rev_map Id.to_string lid)) -let pr_long_global ref = pr_path (Nametab.path_of_global ref) +let pr_long_global ref = pr_path (Nametab.GlobRef.path ref) (*S Warning and Error messages. *) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index e5b80f0b00f3b..c55434f5fe9b0 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -925,7 +925,7 @@ let do_replace (evd : Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num equation_lemma = Some ( match - Nametab.locate (qualid_of_ident equation_lemma_id) + Nametab.GlobRef.locate (qualid_of_ident equation_lemma_id) with | GlobRef.ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.") ) } diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 01ac232db6ce2..0bddbd217c3af 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -19,7 +19,7 @@ let get_name avoid ?(default = "H") = function | Name n -> Name n let array_get_start a = Array.init (Array.length a - 1) (fun i -> a.(i)) -let locate qid = Nametab.locate qid +let locate qid = Nametab.GlobRef.locate qid let locate_ind ref = match locate ref with GlobRef.IndRef x -> x | _ -> raise Not_found @@ -76,7 +76,7 @@ let coq_constant s = UnivGen.constr_of_monomorphic_global (Global.env ()) @@ Coq let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in - Nametab.locate (make_qualid dp (Id.of_string s)) + Nametab.GlobRef.locate (make_qualid dp (Id.of_string s)) let eq = lazy (EConstr.of_constr (coq_constant "core.eq.type")) let refl_equal = lazy (EConstr.of_constr (coq_constant "core.eq.refl")) @@ -256,7 +256,7 @@ let in_Function : function_info -> Libobject.obj = let find_or_none id = try Some - ( match Nametab.locate (qualid_of_ident id) with + ( match Nametab.GlobRef.locate (qualid_of_ident id) with | GlobRef.ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.") ) with Not_found -> None @@ -278,7 +278,7 @@ let add_Function is_general f = and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind") and sprop_lemma = find_or_none (Nameops.add_suffix f_id "_sind") and graph_ind = - match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) with + match Nametab.GlobRef.locate (qualid_of_ident (mk_rel_id f_id)) with | GlobRef.IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.") in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 69f54524d78a8..c935395022dca 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -25,7 +25,6 @@ open Util open UnivGen open Tacticals open Tactics -open Nametab open Tacred open Glob_term open Pretyping @@ -49,7 +48,7 @@ let coq_init_constant s = let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in - locate (make_qualid dp (Id.of_string s)) + Nametab.GlobRef.locate (make_qualid dp (Id.of_string s)) let declare_fun name kind ?univs value = let ce = Declare.definition_entry ?univs value (*FIXME *) in @@ -1724,7 +1723,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) let hook {Declare.Hook.S.uctx; _} = - let term_ref = Nametab.locate (qualid_of_ident term_id) in + let term_ref = Nametab.GlobRef.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name Decls.(IsProof Lemma) arg_types term_ref in @@ -1751,7 +1750,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls true in if not stop then - let eq_ref = Nametab.locate (qualid_of_ident equation_id) in + let eq_ref = Nametab.GlobRef.locate (qualid_of_ident equation_id) in let f_ref = destConst (constr_of_monomorphic_global (Global.env ()) f_ref) and functional_ref = destConst (constr_of_monomorphic_global (Global.env ()) functional_ref) diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 505e694f84cd4..de4ca64ffcf9f 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -568,7 +568,7 @@ let pr_ltac_fun_arg n = spc () ++ Name.print n let print_ltac_body qid tac = let filter mp = - try Some (Nametab.shortest_qualid_of_module mp) + try Some (Nametab.Module.shortest_qualid Id.Set.empty mp) with Not_found -> None in let mods = List.map_filter filter tac.Tacenv.tac_redef in diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index f644852510fc8..44c14a61e478d 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -396,7 +396,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = subterm matched when a pattern *) let r = match r with | {v=AN r} -> r - | {loc} -> (qualid_of_path ?loc (Nametab.path_of_global (smart_global r))) in + | {loc} -> (qualid_of_path ?loc (Nametab.GlobRef.path (smart_global r))) in let sign = { Constrintern.ltac_vars = ist.ltacvars; ltac_bound = Id.Set.empty; diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index 5a8db2e818508..904fdabb2330e 100644 --- a/plugins/ltac2/tac2core.ml +++ b/plugins/ltac2/tac2core.ml @@ -1197,13 +1197,13 @@ let () = define1 "env_expand" (list ident) begin fun ids -> let (id, path) = List.sep_last ids in let path = DirPath.make (List.rev path) in let qid = Libnames.make_qualid path id in - Nametab.locate_all qid + Nametab.GlobRef.locate_all qid in return (Value.of_list Value.of_reference r) end let () = define1 "env_path" reference begin fun r -> - match Nametab.path_of_global r with + match Nametab.GlobRef.path r with | fp -> let (path, id) = Libnames.repr_path fp in let path = DirPath.repr path in @@ -1474,7 +1474,7 @@ let () = GlbVal (GlobRef.VarRef id), gtypref t_reference | Tac2qexpr.QReference qid -> let gr = - try Nametab.locate qid + try Nametab.GlobRef.locate qid with Not_found as exn -> let _, info = Exninfo.capture exn in Nametab.error_global_not_found ~info qid diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index 4ee36a6c8e4f5..0f51e485c8a33 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -675,7 +675,7 @@ module MakeTable (E : Elt) : S = struct *) let register c = try - let c = UnivGen.constr_of_monomorphic_global (Global.env ()) (Nametab.locate c) in + let c = UnivGen.constr_of_monomorphic_global (Global.env ()) (Nametab.GlobRef.locate c) in let _ = Lib.add_leaf (register_obj c) in () with Not_found -> diff --git a/plugins/syntax/number.ml b/plugins/syntax/number.ml index d550d42759b1e..255fc1a09d1b6 100644 --- a/plugins/syntax/number.ml +++ b/plugins/syntax/number.ml @@ -45,12 +45,12 @@ let get_constructors ind = (Array.mapi (fun j c -> GlobRef.ConstructRef (ind, j + 1)) mc) 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_option () = qualid_of_ref "core.option.type" let unsafe_locate_ind q = - match Nametab.locate q with + match Nametab.GlobRef.locate q with | GlobRef.IndRef i -> i | _ -> raise Not_found @@ -427,11 +427,11 @@ let locate_global_inductive_or_int63_or_float env allow_params qid = if allow_params && Coqlib.has_ref int63n && Environ.QGlobRef.equal env (Smartlocate.global_with_alias qid) (Coqlib.lib_ref int63n) then TargetPrim (mkRefC (qualid_of_string int63w), [Coqlib.lib_ref int63c], - (Nametab.path_of_global (Coqlib.lib_ref int63n), [])) + (Nametab.GlobRef.path (Coqlib.lib_ref int63n), [])) else if allow_params && Coqlib.has_ref floatn && Environ.QGlobRef.equal env (Smartlocate.global_with_alias qid) (Coqlib.lib_ref floatn) then TargetPrim (mkRefC (qualid_of_string floatw), [Coqlib.lib_ref floatc], - (Nametab.path_of_global (Coqlib.lib_ref floatn), [])) + (Nametab.GlobRef.path (Coqlib.lib_ref floatn), [])) else TargetInd (Smartlocate.global_inductive_with_alias qid, []) let vernac_number_notation local ty f g opts scope = @@ -522,7 +522,7 @@ let vernac_number_notation local ty f g opts scope = match via with | None -> elaborate_to_post_params env sigma tyc params | Some (ty, l) -> elaborate_to_post_via env sigma ty tyc l in - to_post, (Nametab.path_of_global (GlobRef.IndRef tyc), []), pt_refs in + to_post, (Nametab.GlobRef.path (GlobRef.IndRef tyc), []), pt_refs in let o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name; warning = opts } in diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml index f7da93766ba0d..19f3464943c45 100644 --- a/plugins/syntax/string_notation.ml +++ b/plugins/syntax/string_notation.ml @@ -19,7 +19,7 @@ open Number (** * String notation *) 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_option () = qualid_of_ref "core.option.type" let q_list () = qualid_of_ref "core.list.type" @@ -86,7 +86,7 @@ let vernac_string_notation local ty f g via scope = { pt_local = local; pt_scope = scope; pt_interp_info = StringNotation o; - pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[]; + pt_required = Nametab.GlobRef.path (GlobRef.IndRef tyc),[]; pt_refs; pt_in_match = true } in diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml index 94f0e5795ebcb..f845660b571c1 100644 --- a/pretyping/coercionops.ml +++ b/pretyping/coercionops.ml @@ -220,14 +220,14 @@ let string_of_class = function | CL_FUN -> "Funclass" | CL_SORT -> "Sortclass" | CL_CONST sp -> - string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.ConstRef sp)) + string_of_qualid (Nametab.GlobRef.shortest_qualid Id.Set.empty (GlobRef.ConstRef sp)) | CL_PROJ sp -> let sp = Projection.Repr.constant sp in - string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.ConstRef sp)) + string_of_qualid (Nametab.GlobRef.shortest_qualid Id.Set.empty (GlobRef.ConstRef sp)) | CL_IND sp -> - string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.IndRef sp)) + string_of_qualid (Nametab.GlobRef.shortest_qualid Id.Set.empty (GlobRef.IndRef sp)) | CL_SECVAR sp -> - string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.VarRef sp)) + string_of_qualid (Nametab.GlobRef.shortest_qualid Id.Set.empty (GlobRef.VarRef sp)) let pr_class x = str (string_of_class x) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index d79a8c18ae0aa..b353e31738b9e 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -345,7 +345,7 @@ let free_glob_vars = let glob_visible_short_qualid c = let rec aux acc c = match DAst.get c with | GRef (c,_) -> - let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in + let qualid = Nametab.GlobRef.shortest_qualid Id.Set.empty c in let dir,id = Libnames.repr_qualid qualid in if DirPath.is_empty dir then Id.Set.add id acc else acc | _ -> diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index f4afe5a5f7629..e3de70b1e4a0f 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -731,7 +731,7 @@ let lookup_eliminator env ind_sp s = else (* Then try to get a user-defined eliminator in some other places *) (* using short name (e.g. for "eq_rec") *) - try Nametab.locate (qualid_of_ident id) + try Nametab.GlobRef.locate (qualid_of_ident id) with Not_found -> user_err (strbrk "Cannot find the elimination combinator " ++ diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 24097fc9b9743..18cd23b5587d9 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1192,7 +1192,7 @@ let string_of_evaluable_ref env = function | EvalVarRef id -> Id.to_string id | EvalConstRef kn -> Libnames.string_of_qualid - (Nametab.shortest_qualid_of_global (vars_of_env env) (GlobRef.ConstRef kn)) + (Nametab.GlobRef.shortest_qualid (vars_of_env env) (GlobRef.ConstRef kn)) (* Removing fZETA for finer behaviour would break many developments *) let unfold_side_flags = RedFlags.[fBETA;fMATCH;fFIX;fCOFIX;fZETA] diff --git a/tactics/hints.ml b/tactics/hints.ml index 0885b91009687..a067ca48c62bf 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1655,7 +1655,7 @@ let pr_searchtable env sigma = let print_mp mp = try - let qid = Nametab.shortest_qualid_of_module mp in + let qid = Nametab.Module.shortest_qualid Id.Set.empty mp in str " from " ++ pr_qualid qid with Not_found -> mt () diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 5fbc1b896a30a..a5cb48c0d4422 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -78,7 +78,7 @@ let declare_individual_scheme_object s ?deps ?(aux="") f = (* Defining/retrieving schemes *) let is_visible_name id = - try ignore (Nametab.locate (Libnames.qualid_of_ident id)); true + try ignore (Nametab.GlobRef.locate (Libnames.qualid_of_ident id)); true with Not_found -> false let compute_name internal id = diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 1e4e0ede0688c..4fd9374638963 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -811,7 +811,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ?typing_flags ~pr (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation ~local:false (Global.env ())) where_notations; (* Declare the coercions *) - List.iter (fun qid -> ComCoercion.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly ~nonuniform:false ~reversible:true) coercions + List.iter (fun qid -> ComCoercion.try_add_new_coercion (Nametab.GlobRef.locate qid) ~local:false ~poly ~nonuniform:false ~reversible:true) coercions (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name @@ -850,7 +850,7 @@ let make_cases ind = Id.to_string n' :: rename (Id.Set.add n' avoid) l in let al' = rename Id.Set.empty al in let consref = GlobRef.ConstructRef (ith_constructor_of_inductive ind (i + 1)) in - (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l) + (Libnames.string_of_qualid (Nametab.GlobRef.shortest_qualid Id.Set.empty consref) :: al') :: l) mip.mind_nf_lc [] module Internal = diff --git a/vernac/declare.ml b/vernac/declare.ml index 1fb523c745ac1..91b43637b483d 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -168,10 +168,10 @@ type constant_obj = { } let load_constant i ((sp,kn), obj) = - if Nametab.exists_cci sp then + if Nametab.GlobRef.exists sp then raise (DeclareUniv.AlreadyDeclared (None, Libnames.basename sp)); let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Until i) sp (GlobRef.ConstRef con); + Nametab.GlobRef.push (Nametab.Until i) sp (GlobRef.ConstRef con); Dumpglob.add_constant_kind con obj.cst_kind; begin match obj.cst_locl with | Locality.ImportNeedQualified -> local_csts := Cset_env.add con !local_csts @@ -185,7 +185,7 @@ let open_constant i ((sp,kn), obj) = | Locality.ImportNeedQualified -> () | Locality.ImportDefaultBehavior -> let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con) + Nametab.GlobRef.push (Nametab.Exactly i) sp (GlobRef.ConstRef con) let exists_name id = Decls.variable_exists id || Global.exists_objlabel (Label.of_id id) @@ -196,7 +196,7 @@ let check_exists id = let cache_constant ((sp,kn), obj) = let kn = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef kn); + Nametab.GlobRef.push (Nametab.Until 1) sp (GlobRef.ConstRef kn); Dumpglob.add_constant_kind kn obj.cst_kind let discharge_constant obj = Some obj @@ -526,7 +526,7 @@ let declare_variable_core ~name ~kind d = let () = if opaque then warn_opaque_let name in Glob_term.Explicit, opaque, de.proof_entry_universes in - Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name); + Nametab.GlobRef.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name); Decls.(add_variable_data name {opaque;kind}); Lib.add_leaf (inVariable name); Impargs.declare_var_implicits ~impl name; diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml index d99c441c5ae15..2522dad7f5984 100644 --- a/vernac/declareInd.ml +++ b/vernac/declareInd.ml @@ -44,15 +44,15 @@ let inductive_names sp kn obj = let load_inductive i ((sp, kn), names) = let names = inductive_names sp kn names in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names + List.iter (fun (sp, ref) -> Nametab.GlobRef.push (Nametab.Until i) sp ref ) names let open_inductive i ((sp, kn), names) = let names = inductive_names sp kn names in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names + List.iter (fun (sp, ref) -> Nametab.GlobRef.push (Nametab.Exactly i) sp ref) names let cache_inductive ((sp, kn), names) = let names = inductive_names sp kn names in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names + List.iter (fun (sp, ref) -> Nametab.GlobRef.push (Nametab.Until 1) sp ref) names let discharge_inductive names = Some names diff --git a/vernac/declareUctx.ml b/vernac/declareUctx.ml index e6a3f784bfb94..0edf8661f2c3a 100644 --- a/vernac/declareUctx.ml +++ b/vernac/declareUctx.ml @@ -16,7 +16,7 @@ let name_instance inst = assert false | Some na -> try - let qid = Nametab.shortest_qualid_of_universe Names.Id.Map.empty na in + let qid = Nametab.Universe.shortest_qualid Names.Id.Set.empty na in Names.Name (Libnames.qualid_basename qid) with Not_found -> (* Best-effort naming from the string representation of the level. diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml index 7a329a4604e18..31c51df1aad2d 100644 --- a/vernac/declareUniv.ml +++ b/vernac/declareUniv.ml @@ -30,7 +30,7 @@ type universe_source = type universe_name_decl = universe_source * (Id.t * Univ.UGlobal.t) list let check_exists_universe sp = - if Nametab.exists_universe sp then + if Nametab.Universe.exists sp then raise (AlreadyDeclared (Some "Universe", Libnames.basename sp)) else () @@ -45,7 +45,7 @@ let qualify_univ i dp src id = let do_univ_name ~check i dp src (id,univ) = let i, sp = qualify_univ i dp src id in if check then check_exists_universe sp; - Nametab.push_universe i sp univ + Nametab.Universe.push i sp univ let cache_univ_names (prefix, (src, univs)) = let depth = Lib.sections_depth () in diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index 4f6fe85090d95..41a58e6783152 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -48,14 +48,14 @@ let inl2intopt = function let consistency_checks exists dir = if exists then let _ = - try Nametab.locate_module (qualid_of_dirpath dir) + try Nametab.Module.locate (qualid_of_dirpath dir) with Not_found -> user_err (DirPath.print dir ++ str " should already exist!") in () else - if Nametab.exists_module dir then + if Nametab.Module.exists dir then user_err (DirPath.print dir ++ str " already exists.") @@ -98,7 +98,7 @@ module type ModActions = sig val enter_modtype : ModPath.t -> full_path -> int -> unit - val open_module : open_filter -> ModPath.t -> DirPath.t -> int -> unit + val open_module : Libobject.open_filter -> ModPath.t -> DirPath.t -> int -> unit module Lib : Lib.StagedLibS @@ -120,16 +120,16 @@ struct let enter_module obj_mp obj_dir i = consistency_checks false obj_dir; - Nametab.push_module (Until i) obj_dir obj_mp + Nametab.Module.push (Until i) obj_dir obj_mp let enter_modtype mp sp i = - if Nametab.exists_modtype sp then + if Nametab.ModType.exists sp then anomaly (pr_path sp ++ str " already exists."); - Nametab.push_modtype (Nametab.Until i) sp mp + Nametab.ModType.push (Nametab.Until i) sp mp let open_module f obj_mp obj_dir i = consistency_checks true obj_dir; - if in_filter ~cat:None f then Nametab.push_module (Nametab.Exactly i) obj_dir obj_mp + if Libobject.in_filter ~cat:None f then Nametab.Module.push (Nametab.Exactly i) obj_dir obj_mp module Lib = Lib.Synterp @@ -231,7 +231,7 @@ let subst_filtered sub (f,mp as x) = else f, mp' let rec subst_aobjs sub = function - | Objs o as objs -> + | Libobject.Objs o as objs -> let o' = subst_objects sub o in if o == o' then objs else Objs o' | Ref (mp, sub0) as r -> @@ -245,7 +245,7 @@ and subst_sobjs sub (mbids,aobjs as sobjs) = and subst_objects subst seg = let subst_one node = match node with - | AtomicObject obj -> + | Libobject.AtomicObject obj -> let obj' = Libobject.subst_object (subst,obj) in if obj' == obj then node else AtomicObject obj' | ModuleObject (id, sobjs) -> @@ -306,7 +306,7 @@ module ModSubstObjs : end let expand_aobjs = function - | Objs o -> o + | Libobject.Objs o -> o | Ref (mp, sub) -> match ModSubstObjs.get mp with | (_,Objs o) -> subst_objects sub o @@ -395,7 +395,7 @@ let load_modtype i sp mp sobjs = let rec load_object i (prefix, obj) = match obj with - | AtomicObject o -> Libobject.load_object i (prefix, o) + | Libobject.AtomicObject o -> Libobject.load_object i (prefix, o) | ModuleObject (id,sobjs) -> let name = Lib.make_oname prefix id in do_module' load_objects i (name, sobjs) @@ -450,7 +450,7 @@ and collect_module (f,mp) acc = and collect_object f i prefix obj acc = match obj with - | ExportObject { mpl } -> collect_exports f i mpl acc + | Libobject.ExportObject { mpl } -> collect_exports f i mpl acc | AtomicObject _ | IncludeObject _ | KeepObject _ | ModuleObject _ | ModuleTypeObject _ -> mark_object f (prefix,obj) acc @@ -460,12 +460,12 @@ and collect_objects f i prefix objs acc = (List.rev objs) and collect_export f (f',mp) (exports,objs as acc) = - match filter_and f f' with + match Libobject.filter_and f f' with | None -> acc | Some f -> let exports' = MPmap.update mp (function | None -> Some f - | Some f0 -> Some (filter_or f f0)) + | Some f0 -> Some (Libobject.filter_or f f0)) exports in (* If the map doesn't change there is nothing new to export. @@ -487,16 +487,16 @@ and collect_exports f i mpl acc = let open_modtype i ((sp,kn),_) = let mp = mp_of_kn kn in let mp' = - try Nametab.locate_modtype (qualid_of_path sp) + try Nametab.ModType.locate (qualid_of_path sp) with Not_found -> anomaly (pr_path sp ++ str " should already exist!"); in assert (ModPath.equal mp mp'); - Nametab.push_modtype (Nametab.Exactly i) sp mp + Nametab.ModType.push (Nametab.Exactly i) sp mp let rec open_object f i (prefix, obj) = match obj with - | AtomicObject o -> Libobject.open_object f i (prefix, o) + | Libobject.AtomicObject o -> Libobject.open_object f i (prefix, o) | ModuleObject (id,sobjs) -> let name = Lib.make_oname prefix id in let dir = dir_of_sp (fst name) in @@ -539,14 +539,14 @@ and open_keep f i ((sp,kn),kobjs) = let cache_include (prefix, aobjs) = let o = expand_aobjs aobjs in load_objects 1 prefix o; - open_objects unfiltered 1 prefix o + open_objects Libobject.unfiltered 1 prefix o and cache_keep ((sp,kn),kobjs) = anomaly (Pp.str "This module should not be cached!") let cache_object (prefix, obj) = match obj with - | AtomicObject o -> Libobject.cache_object (prefix, o) + | Libobject.AtomicObject o -> Libobject.cache_object (prefix, o) | ModuleObject (id,sobjs) -> let name = Lib.make_oname prefix id in do_module' load_objects 1 (name, sobjs) @@ -588,7 +588,7 @@ let add_leaves objs = let mp_id mp id = MPdot (mp, Label.of_id id) let rec register_mod_objs mp obj = match obj with - | ModuleObject (id,sobjs) -> ModSubstObjs.set (mp_id mp id) sobjs + | Libobject.ModuleObject (id,sobjs) -> ModSubstObjs.set (mp_id mp id) sobjs | ModuleTypeObject (id,sobjs) -> ModSubstObjs.set (mp_id mp id) sobjs | IncludeObject aobjs -> List.iter (register_mod_objs mp) (expand_aobjs aobjs) @@ -625,7 +625,7 @@ let get_applications mexpr = let rec replace_module_object idl mp0 objs0 mp1 objs1 = match idl, objs0 with | _,[] -> [] - | id::idl,(ModuleObject (id', sobjs))::tail when Id.equal id id' -> + | id::idl,(Libobject.ModuleObject (id', sobjs))::tail when Id.equal id id' -> begin let mp_id = MPdot(mp0, Label.of_id id) in let objs = match idl with @@ -644,7 +644,7 @@ let rec get_module_sobjs is_mod env inl = function | MEident mp -> begin match ModSubstObjs.get mp with | (mbids,Objs _) when not (ModPath.is_bound mp) -> - (mbids,Ref (mp, empty_subst)) (* we create an alias *) + (mbids,Libobject.Ref (mp, empty_subst)) (* we create an alias *) | sobjs -> sobjs end | MEwith (mty, WithDef _) -> get_module_sobjs is_mod env inl mty @@ -779,7 +779,7 @@ let start_module export id args res fs = let mp, res_entry_o, mbids, sign, args = start_module_core id args res fs in set_openmod_syntax_info { cur_mp = mp; cur_typ = res_entry_o; cur_mbids = mbids }; let prefix = Lib.Synterp.start_module export id mp fs in - Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix.obj_mp)); + Nametab.Dir.push (Until 1) (prefix.obj_dir) (Nametab.GlobDirRef.DirOpenModule prefix.obj_mp); mp, args, sign let end_module_core id (m_info : current_module_syntax_info) objects fs = @@ -1031,7 +1031,7 @@ let end_module_core id m_info objects fs = | Some (mty, _) -> subst_sobjs (map_mp (get_module_path mty) mp resolver) sobjs in - let node = ModuleObject (id,sobjs) in + let node = Libobject.ModuleObject (id,sobjs) in (* We add the keep objects, if any, and if this isn't a functor *) let objects = match keep, mbids with | [], _ | _, _ :: _ -> special@[node] @@ -1126,7 +1126,7 @@ let start_modtype id args mtys fs = let mp, mbids, args, sub_mty_l = start_modtype_core id (openmod_syntax_info ()).cur_mp args mtys fs in set_openmod_syntax_info { cur_mp = mp; cur_typ = None; cur_mbids = mbids }; let prefix = Lib.Synterp.start_modtype id mp fs in - Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModtype prefix.obj_mp)); + Nametab.Dir.push (Until 1) (prefix.obj_dir) (Nametab.GlobDirRef.DirOpenModtype prefix.obj_mp); mp, args, sub_mty_l let end_modtype_core id mbids objects fs = @@ -1179,7 +1179,7 @@ let start_modtype id args mtys fs = let mp, _, sub_mty_l, _ = start_modtype_core id args mtys fs in openmodtype_info := sub_mty_l; let prefix = Lib.Interp.start_modtype id mp fs in - Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModtype mp)); + Nametab.Dir.push (Until 1) (prefix.obj_dir) (Nametab.GlobDirRef.DirOpenModtype mp); mp let end_modtype_core id sub_mty_l objects fs = diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a58578eb76004..64e9e0bc54156 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -976,12 +976,12 @@ let rec explain_pretype_error env sigma err = (* Module errors *) let pr_modpath mp = - Libnames.pr_qualid (Nametab.shortest_qualid_of_module mp) + Libnames.pr_qualid (Nametab.Module.shortest_qualid Id.Set.empty mp) let pr_modtype_subpath upper mp = let rec aux mp = try - let (dir,id) = Libnames.repr_qualid (Nametab.shortest_qualid_of_modtype mp) in + let (dir,id) = Libnames.repr_qualid (Nametab.ModType.shortest_qualid Id.Set.empty mp) in Libnames.add_dirpath_suffix dir id, [] with Not_found -> match mp with diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index cb6028735205a..c7bc4dd0d573a 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -313,7 +313,7 @@ let rec insert_fake_args volatile bidi impls = RealArg hd :: insert_fake_args (f volatile) (f bidi) tl let print_arguments ref = - let qid = Nametab.shortest_qualid_of_global Id.Set.empty ref in + let qid = Nametab.GlobRef.shortest_qualid Id.Set.empty ref in let flags, recargs, nargs_for_red = let open Reductionops.ReductionBehaviour in match get ref with @@ -425,15 +425,15 @@ let register_locatable name f = exception ObjFound of logical_name let locate_any_name qid = - try Term (Nametab.locate qid) + try Term (Nametab.GlobRef.locate qid) with Not_found -> - try Abbreviation (Nametab.locate_abbreviation qid) + try Abbreviation (Nametab.Abbrev.locate qid) with Not_found -> - try Dir (Nametab.locate_dir qid) + try Dir (Nametab.Dir.locate qid) with Not_found -> - try Module (Nametab.locate_module qid) + try Module (Nametab.Module.locate qid) with Not_found -> - try ModuleType (Nametab.locate_modtype qid) + try ModuleType (Nametab.ModType.locate qid) with Not_found -> let iter _ (Locatable info) = match info.locate qid with | None -> () @@ -445,7 +445,7 @@ let locate_any_name qid = let canonical_info ref = let cref = canonical_gr ref in if GlobRef.UserOrd.equal ref cref then mt () - else match Nametab.path_of_global cref with + else match Nametab.GlobRef.path cref with | path -> spc() ++ str "(syntactically equal to" ++ spc() ++ pr_path path ++ str ")" | exception Not_found -> spc() ++ str "(missing canonical, bug?)" @@ -458,9 +458,9 @@ let pr_located_qualid = function | VarRef _ -> "Variable" in let extra = canonical_info ref in - str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref) ++ extra + str ref_str ++ spc () ++ pr_path (Nametab.GlobRef.path ref) ++ extra | Abbreviation kn -> - str "Notation" ++ spc () ++ pr_path (Nametab.path_of_abbreviation kn) + str "Notation" ++ spc () ++ pr_path (Nametab.Abbrev.path kn) | Dir dir -> let s,mp = let open Nametab in @@ -471,9 +471,9 @@ let pr_located_qualid = function in str s ++ spc () ++ str (ModPath.to_string mp) | Module mp -> - str "Module" ++ spc () ++ DirPath.print (Nametab.dirpath_of_module mp) + str "Module" ++ spc () ++ DirPath.print (Nametab.Module.path mp) | ModuleType mp -> - str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp) + str "Module Type" ++ spc () ++ pr_path (Nametab.ModType.path mp) | Other (obj, info) -> info.name obj | Undefined qid -> pr_qualid qid ++ spc () ++ str "not a defined object." @@ -498,7 +498,7 @@ let display_alias = function begin match canonize_ref r with | None -> mt () | Some r' -> - let q' = Nametab.shortest_qualid_of_global Id.Set.empty r' in + let q' = Nametab.GlobRef.shortest_qualid Id.Set.empty r' in spc () ++ str "(alias of " ++ pr_qualid q' ++ str ")" end | _ -> mt () @@ -506,18 +506,18 @@ let display_alias = function let locate_term qid = let expand = function | TrueGlobal ref -> - Term ref, Nametab.shortest_qualid_of_global Id.Set.empty ref + Term ref, Nametab.GlobRef.shortest_qualid Id.Set.empty ref | Abbrev kn -> - Abbreviation kn, Nametab.shortest_qualid_of_abbreviation Id.Set.empty kn + Abbreviation kn, Nametab.Abbrev.shortest_qualid Id.Set.empty kn in List.map expand (Nametab.locate_extended_all qid) let locate_module qid = - let all = Nametab.locate_extended_all_module qid in - let map mp = Module mp, Nametab.shortest_qualid_of_module mp in + let all = Nametab.Module.locate_all qid in + let map mp = Module mp, Nametab.Module.shortest_qualid Id.Set.empty mp in let mods = List.map map all in (* Don't forget the opened modules: they are not part of the same name tab. *) - let all = Nametab.locate_extended_all_dir qid in + let all = Nametab.Dir.locate_all qid in let map dir = let open Nametab.GlobDirRef in match dir with | DirOpenModule _ -> Some (Dir dir, qid) | _ -> None @@ -525,11 +525,11 @@ let locate_module qid = mods @ List.map_filter map all let locate_modtype qid = - let all = Nametab.locate_extended_all_modtype qid in - let map mp = ModuleType mp, Nametab.shortest_qualid_of_modtype mp in + let all = Nametab.ModType.locate_all qid in + let map mp = ModuleType mp, Nametab.ModType.shortest_qualid Id.Set.empty mp in let modtypes = List.map map all in (* Don't forget the opened module types: they are not part of the same name tab. *) - let all = Nametab.locate_extended_all_dir qid in + let all = Nametab.Dir.locate_all qid in let map dir = let open Nametab.GlobDirRef in match dir with | DirOpenModtype _ -> Some (Dir dir, qid) | _ -> None @@ -683,7 +683,7 @@ let gallina_print_constant_with_infos sp udecl = with_line_skip (print_name_infos (GlobRef.ConstRef sp)) let gallina_print_abbreviation env kn = - let qid = Nametab.shortest_qualid_of_abbreviation Id.Set.empty kn + let qid = Nametab.Abbrev.shortest_qualid Id.Set.empty kn and (vars,a) = Abbreviation.search_abbreviation kn in let c = Notation_ops.glob_constr_of_notation_constr a in hov 2 diff --git a/vernac/printmod.ml b/vernac/printmod.ml index 47d5d5db2eca3..c98559bd165ad 100644 --- a/vernac/printmod.ml +++ b/vernac/printmod.ml @@ -61,7 +61,7 @@ let keyword s = tag_keyword (str s) let get_new_id locals id = let rec get_id l id = let dir = DirPath.make [id] in - if not (Nametab.exists_module dir || Nametab.exists_dir dir) then + if not (Nametab.Module.exists dir || Nametab.Module.exists dir) then id else get_id (Id.Set.add id l) (Namegen.next_ident_away id l) @@ -168,15 +168,15 @@ let rec print_local_modpath locals = function let print_modpath locals mp = try (* must be with let because streams are lazy! *) - let qid = Nametab.shortest_qualid_of_module mp in - pr_qualid qid + let qid = Nametab.Module.shortest_qualid Id.Set.empty mp in + pr_qualid qid with | Not_found -> print_local_modpath locals mp let print_kn locals kn = try - let qid = Nametab.shortest_qualid_of_modtype kn in - pr_qualid qid + let qid = Nametab.ModType.shortest_qualid Id.Set.empty kn in + pr_qualid qid with Not_found -> try @@ -187,7 +187,7 @@ let print_kn locals kn = let nametab_register_dir obj_mp = let id = mk_fake_top () in let obj_dir = DirPath.make [id] in - Nametab.(push_module (Until 1) obj_dir obj_mp) + Nametab.Module.push (Until 1) obj_dir obj_mp (** Nota: the [global_reference] we register in the nametab below might differ from internal ones, since we cannot recreate here @@ -197,7 +197,7 @@ let nametab_register_dir obj_mp = let nametab_register_body mp dir (l,body) = let push id ref = - Nametab.push (Nametab.Until (1+List.length (DirPath.repr dir))) + Nametab.GlobRef.push (Nametab.Until (1+List.length (DirPath.repr dir))) (make_path dir id) ref in match body with @@ -243,7 +243,7 @@ let nametab_register_modparam mbid mtb = with e when CErrors.noncritical e -> (* Otherwise, we try to play with the nametab ourselves *) let mp = MPbound mbid in - let check id = Nametab.exists_module (DirPath.make [id]) in + let check id = Nametab.Module.exists (DirPath.make [id]) in let id = Namegen.next_ident_away_from id check in let dir = DirPath.make [id] in nametab_register_dir mp; diff --git a/vernac/search.ml b/vernac/search.ml index 6383ee07f3670..2f30679bc96d9 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -182,7 +182,7 @@ let rec pattern_filter pat ref env sigma typ = | _ -> false let full_name_of_reference ref = - let (dir,id) = repr_path (Nametab.path_of_global ref) in + let (dir,id) = repr_path (Nametab.GlobRef.path ref) in DirPath.to_string dir ^ "." ^ Id.to_string id (** Whether a reference is blacklisted *) @@ -192,7 +192,7 @@ let blacklist_filter ref kind env sigma typ = CString.Set.for_all is_not_bl (SearchBlacklist.v ()) let module_filter (mods, outside) ref kind env sigma typ = - let sp = Nametab.path_of_global ref in + let sp = Nametab.GlobRef.path ref in let sl = dirpath sp in let is_outside md = not (is_dirpath_prefix_of md sl) in let is_inside md = is_dirpath_prefix_of md sl in @@ -310,7 +310,7 @@ let interface_search env sigma = in let filter_function ref env constr = let id = Names.Id.to_string (Nametab.basename_of_global ref) in - let path = Libnames.dirpath (Nametab.path_of_global ref) in + let path = Libnames.dirpath (Nametab.GlobRef.path ref) in let toggle x b = if x then b else not b in let match_name (regexp, flag) = toggle (Str.string_match regexp id 0) flag @@ -335,7 +335,7 @@ let interface_search env sigma = let ans = ref [] in let print_function ref env constr = let fullpath = DirPath.repr (Nametab.dirpath_of_global ref) in - let qualid = Nametab.shortest_qualid_of_global Id.Set.empty ref in + let qualid = Nametab.GlobRef.shortest_qualid Id.Set.empty ref in let (shortpath, basename) = Libnames.repr_qualid qualid in let shortpath = DirPath.repr shortpath in (* [shortpath] is a suffix of [fullpath] and we're looking for the missing diff --git a/vernac/synterp.ml b/vernac/synterp.ml index 8fe0415e047ea..358936429d603 100644 --- a/vernac/synterp.ml +++ b/vernac/synterp.ml @@ -141,7 +141,7 @@ let import_module_syntax_with_filter ~export cats m f = let synterp_import_mod (export,cats) qid f = let loc = qid.loc in - let m = try Nametab.locate_module qid + let m = try Nametab.Module.locate qid with Not_found -> CErrors.user_err ?loc Pp.(str "Cannot find module " ++ pr_qualid qid) in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 48aedb7f4424a..9ab99aed3394c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -137,18 +137,18 @@ let print_libraries () = let print_module qid = - match Nametab.locate_module qid with + match Nametab.Module.locate qid with | mp -> Printmod.print_module ~with_body:true mp | exception Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid ++ str".") let print_modtype qid = try - let kn = Nametab.locate_modtype qid in + let kn = Nametab.ModType.locate qid in Printmod.print_modtype kn with Not_found -> (* Is there a module of this name ? If yes we display its type *) try - let mp = Nametab.locate_module qid in + let mp = Nametab.Module.locate qid in Printmod.print_module ~with_body:false mp with Not_found -> user_err (str"Unknown Module Type or Module " ++ pr_qualid qid ++ str".") @@ -320,7 +320,7 @@ let dump_universes_gen prl g s = let universe_subgraph ?loc kept univ = let open Univ in let parse q = - try Level.make (Nametab.locate_universe q) + try Level.make (Nametab.Universe.locate q) with Not_found -> CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid q ++ str".") in @@ -505,8 +505,8 @@ let vernac_enable_notation ~module_local on rule interp flags scope = let check_name_freshness locality {CAst.loc;v=id} : unit = (* We check existence here: it's a bit late at Qed time *) - if Nametab.exists_cci (Lib.make_path id) || Termops.is_section_variable (Global.env ()) id || - locality <> Locality.Discharge && Nametab.exists_cci (Lib.make_path_except_section id) + if Nametab.GlobRef.exists (Lib.make_path id) || Termops.is_section_variable (Global.env ()) id || + locality <> Locality.Discharge && Nametab.GlobRef.exists (Lib.make_path_except_section id) then user_err ?loc (Id.print id ++ str " already exists.") @@ -1109,7 +1109,7 @@ let add_subnames_of ?loc len n ns full_n ref = ns Sorts.all_families let interp_names m ns = - let dp_m = Nametab.dirpath_of_module m in + let dp_m = Nametab.Module.path m in let ns = List.fold_left (fun ns (n,etc) -> let len, full_n = @@ -1120,7 +1120,7 @@ let interp_names m ns = with Not_found -> CErrors.user_err ?loc:n.loc Pp.(str "Cannot find name " ++ pr_qualid n ++ spc() ++ - str "in module " ++ pr_qualid (Nametab.shortest_qualid_of_module m) ++ str ".") + str "in module " ++ pr_qualid (Nametab.Module.shortest_qualid Id.Set.empty m) ++ str ".") in (* TODO dumpglob? *) match ref with @@ -1136,13 +1136,13 @@ let cache_name (len,n) = let open Globnames in let open GlobRef in match n with - | Abbrev kn -> Abbreviation.import_abbreviation (len+1) (Nametab.path_of_abbreviation kn) kn + | Abbrev kn -> Abbreviation.import_abbreviation (len+1) (Nametab.Abbrev.path kn) kn | TrueGlobal (VarRef _) -> assert false | TrueGlobal (ConstRef c) when Declare.is_local_constant c -> (* Can happen through functor application *) warn_not_importable c | TrueGlobal gr -> - Nametab.(push (Exactly (len+1)) (path_of_global gr) gr) + Nametab.(GlobRef.push (Exactly (len+1)) (GlobRef.path gr) gr) let cache_names ns = List.iter cache_name ns