Skip to content

Commit

Permalink
[nametab] Introduce type of imperative nametabs, unify API
Browse files Browse the repository at this point in the history
This is both a cleanup and a step towards pushing the state upwards,
and handling the nametabs functionally.

Related to coq#16746 and
coq/rfcs#65
  • Loading branch information
ejgallego committed Nov 2, 2022
1 parent ff5b5d8 commit 0349d3e
Show file tree
Hide file tree
Showing 32 changed files with 448 additions and 374 deletions.
4 changes: 2 additions & 2 deletions engine/namegen.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down
6 changes: 3 additions & 3 deletions interp/abbreviation.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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,_) ->
Expand All @@ -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 *)
Expand Down
6 changes: 3 additions & 3 deletions interp/constrintern.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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))
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions interp/dumpglob.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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"

Expand Down
2 changes: 1 addition & 1 deletion interp/implicit_quantifiers.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions interp/modintern.ml
Original file line number Diff line number Diff line change
Expand Up @@ -49,12 +49,12 @@ let lookup_module_or_modtype kind qid =
let loc = qid.CAst.loc in
try
if kind == ModType then raise Not_found;
let mp = Nametab.locate_module qid in
let mp = Nametab.Module.locate qid in
Dumpglob.dump_modref ?loc mp "modtype"; (mp,Module)
with Not_found ->
try
if kind == Module then raise Not_found;
let mp = Nametab.locate_modtype qid in
let mp = Nametab.ModType.locate qid in
Dumpglob.dump_modref ?loc mp "mod"; (mp,ModType)
with Not_found as exn ->
let _, info = Exninfo.capture exn in
Expand Down
4 changes: 2 additions & 2 deletions interp/notation.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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)
Expand Down
6 changes: 3 additions & 3 deletions library/coqlib.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 ".")

Expand Down
8 changes: 4 additions & 4 deletions library/lib.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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.");
Expand Down Expand Up @@ -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
Expand Down
Loading

0 comments on commit 0349d3e

Please sign in to comment.