diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 4 | ||||
| -rw-r--r-- | library/global.mli | 2 | ||||
| -rw-r--r-- | library/libnames.ml | 2 | ||||
| -rw-r--r-- | library/libnames.mli | 1 | ||||
| -rw-r--r-- | library/nametab.ml | 12 | ||||
| -rw-r--r-- | library/nametab.mli | 5 |
6 files changed, 19 insertions, 7 deletions
diff --git a/library/global.ml b/library/global.ml index 5c847fda96..71cadb3600 100644 --- a/library/global.ml +++ b/library/global.ml @@ -105,9 +105,9 @@ let is_cumulative_sprop () = (typing_flags()).Declarations.cumulative_sprop let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) let sprop_allowed () = Environ.sprop_allowed (env()) let export_private_constants cd = globalize (Safe_typing.export_private_constants cd) -let add_constant id d = globalize (Safe_typing.add_constant (i2l id) d) +let add_constant ?typing_flags id d = globalize (Safe_typing.add_constant ?typing_flags (i2l id) d) let add_private_constant id d = globalize (Safe_typing.add_private_constant (i2l id) d) -let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie) +let add_mind ?typing_flags id mie = globalize (Safe_typing.add_mind ?typing_flags (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl) diff --git a/library/global.mli b/library/global.mli index 5faf0e8bbd..c9b9d7f536 100644 --- a/library/global.mli +++ b/library/global.mli @@ -52,10 +52,12 @@ val export_private_constants : Safe_typing.exported_private_constant list val add_constant : + ?typing_flags:Declarations.typing_flags -> Id.t -> Safe_typing.global_declaration -> Constant.t val add_private_constant : Id.t -> Safe_typing.side_effect_declaration -> Constant.t * Safe_typing.private_constants val add_mind : + ?typing_flags:Declarations.typing_flags -> Id.t -> Entries.mutual_inductive_entry -> MutInd.t (** Extra universe constraints *) diff --git a/library/libnames.ml b/library/libnames.ml index 88b2e41855..ba1ef1e2f9 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -145,6 +145,8 @@ let qualid_of_dirpath ?loc dir = let (l,a) = split_dirpath dir in make_qualid ?loc l a +let qualid_of_lident lid = qualid_of_ident ?loc:lid.CAst.loc lid.CAst.v + let qualid_is_ident qid = DirPath.is_empty qid.CAst.v.dirpath diff --git a/library/libnames.mli b/library/libnames.mli index a384510879..65aca0c87d 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -77,6 +77,7 @@ val qualid_of_string : ?loc:Loc.t -> string -> qualid val qualid_of_path : ?loc:Loc.t -> full_path -> qualid val qualid_of_dirpath : ?loc:Loc.t -> DirPath.t -> qualid val qualid_of_ident : ?loc:Loc.t -> Id.t -> qualid +val qualid_of_lident : lident -> qualid val qualid_is_ident : qualid -> bool val qualid_path : qualid -> DirPath.t diff --git a/library/nametab.ml b/library/nametab.ml index a51c281f2b..e94b696b60 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -98,6 +98,7 @@ module type NAMETREE = sig val find : user_name -> t -> elt val exists : user_name -> t -> bool val user_name : qualid -> t -> user_name + val shortest_qualid_gen : ?loc:Loc.t -> (Id.t -> bool) -> user_name -> t -> qualid val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid val find_prefixes : qualid -> t -> elt list @@ -252,9 +253,9 @@ let exists uname tab = with Not_found -> false -let shortest_qualid ?loc ctx uname tab = +let shortest_qualid_gen ?loc hidden uname tab = let id,dir = U.repr uname in - let hidden = Id.Set.mem id ctx in + let hidden = hidden id in let rec find_uname pos dir tree = let is_empty = match pos with [] -> true | _ -> false in match tree.path with @@ -269,6 +270,9 @@ let shortest_qualid ?loc ctx uname tab = let found_dir = find_uname [] dir ptab in make_qualid ?loc (DirPath.make found_dir) id +let shortest_qualid ?loc ctx uname tab = + shortest_qualid_gen ?loc (fun id -> Id.Set.mem id ctx) uname tab + let push_node node l = match node with | Absolute (_,o) | Relative (_,o) when not (List.mem_f E.equal o l) -> o::l @@ -562,9 +566,9 @@ let shortest_qualid_of_modtype ?loc kn = let sp = MPmap.find kn !the_modtyperevtab in MPTab.shortest_qualid ?loc Id.Set.empty sp !the_modtypetab -let shortest_qualid_of_universe ?loc kn = +let shortest_qualid_of_universe ?loc ctx kn = let sp = UnivIdMap.find kn !the_univrevtab in - UnivTab.shortest_qualid ?loc Id.Set.empty sp !the_univtab + UnivTab.shortest_qualid_gen ?loc (fun id -> Id.Map.mem id ctx) sp !the_univtab let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) diff --git a/library/nametab.mli b/library/nametab.mli index 8a8b59733c..33aebca0b9 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -206,7 +206,9 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid -val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid + +(** 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.Level.UGlobal.t -> qualid (** {5 Generic name handling} *) @@ -236,6 +238,7 @@ module type NAMETREE = sig val find : user_name -> t -> elt val exists : user_name -> t -> bool val user_name : qualid -> t -> user_name + val shortest_qualid_gen : ?loc:Loc.t -> (Id.t -> bool) -> user_name -> t -> qualid val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid val find_prefixes : qualid -> t -> elt list val match_prefixes : qualid -> t -> elt list |