diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 14 | ||||
| -rw-r--r-- | library/global.mli | 7 | ||||
| -rw-r--r-- | library/nametab.ml | 55 | ||||
| -rw-r--r-- | library/nametab.mli | 13 |
4 files changed, 64 insertions, 25 deletions
diff --git a/library/global.ml b/library/global.ml index 43097dc5d..03d7612a4 100644 --- a/library/global.ml +++ b/library/global.ml @@ -8,7 +8,6 @@ open Names open Environ -open Decl_kinds (** We introduce here the global environment of the system, and we declare it as a synchronized table. *) @@ -231,18 +230,7 @@ let universes_of_global env r = let universes_of_global gr = universes_of_global (env ()) gr -(** Global universe names *) -type universe_names = - (polymorphic * Univ.Level.t) Id.Map.t * Id.t Univ.LMap.t - -let global_universes = - Summary.ref ~name:"Global universe names" - ((Id.Map.empty, Univ.LMap.empty) : universe_names) - -let global_universe_names () = !global_universes -let set_global_universe_names s = global_universes := s - -let is_polymorphic r = +let is_polymorphic r = let env = env() in match r with | VarRef id -> false diff --git a/library/global.mli b/library/global.mli index 51fe53181..1d68d1082 100644 --- a/library/global.mli +++ b/library/global.mli @@ -102,13 +102,6 @@ val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option (** Same as {!body_of_constant} but on {!Declarations.constant_body}. *) -(** Global universe name <-> level mapping *) -type universe_names = - (Decl_kinds.polymorphic * Univ.Level.t) Id.Map.t * Id.t Univ.LMap.t - -val global_universe_names : unit -> universe_names -val set_global_universe_names : universe_names -> unit - (** {6 Compiled libraries } *) val start_library : DirPath.t -> ModPath.t diff --git a/library/nametab.ml b/library/nametab.ml index 222c4cedc..84225f863 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -302,6 +302,16 @@ module DirTab = Make(DirPath')(GlobDir) type dirtab = DirTab.t let the_dirtab = ref (DirTab.empty : dirtab) +type universe_id = DirPath.t * int + +module UnivIdEqual = +struct + type t = universe_id + let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i' +end +module UnivTab = Make(FullPath)(UnivIdEqual) +type univtab = UnivTab.t +let the_univtab = ref (UnivTab.empty : univtab) (* Reversed name tables ***************************************************) @@ -318,6 +328,21 @@ let the_modrevtab = ref (MPmap.empty : mprevtab) type mptrevtab = full_path MPmap.t let the_modtyperevtab = ref (MPmap.empty : mptrevtab) +module UnivIdOrdered = +struct + type t = universe_id + let hash (d, i) = i + DirPath.hash d + let compare (d, i) (d', i') = + let c = Int.compare i i' in + if Int.equal c 0 then DirPath.compare d d' + else c +end + +module UnivIdMap = HMap.Make(UnivIdOrdered) + +type univrevtab = full_path UnivIdMap.t +let the_univrevtab = ref (UnivIdMap.empty : univrevtab) + (* Push functions *********************************************************) (* This is for permanent constructions (never discharged -- but with @@ -362,6 +387,11 @@ let push_dir vis dir dir_ref = | DirModule { obj_mp; _ } -> the_modrevtab := MPmap.add obj_mp dir !the_modrevtab | _ -> () +(* This is for global universe names *) + +let push_universe vis sp univ = + the_univtab := UnivTab.push vis sp univ !the_univtab; + the_univrevtab := UnivIdMap.add univ sp !the_univrevtab (* Locate functions *******************************************************) @@ -382,6 +412,8 @@ let locate_syndef qid = match locate_extended qid with let locate_modtype qid = MPTab.locate qid !the_modtypetab let full_name_modtype qid = MPTab.user_name qid !the_modtypetab +let locate_universe qid = UnivTab.locate qid !the_univtab + let locate_dir qid = DirTab.locate qid !the_dirtab let locate_module qid = @@ -447,6 +479,8 @@ let exists_module = exists_dir let exists_modtype sp = MPTab.exists sp !the_modtypetab +let exists_universe kn = UnivTab.exists kn !the_univtab + (* Reverse locate functions ***********************************************) let path_of_global ref = @@ -469,6 +503,9 @@ let dirpath_of_module mp = let path_of_modtype mp = MPmap.find mp !the_modtyperevtab +let path_of_universe mp = + UnivIdMap.find mp !the_univrevtab + (* Shortest qualid functions **********************************************) let shortest_qualid_of_global ctx ref = @@ -490,6 +527,10 @@ let shortest_qualid_of_modtype kn = let sp = MPmap.find kn !the_modtyperevtab in MPTab.shortest_qualid Id.Set.empty sp !the_modtypetab +let shortest_qualid_of_universe kn = + let sp = UnivIdMap.find kn !the_univrevtab in + UnivTab.shortest_qualid Id.Set.empty sp !the_univtab + let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) with Not_found as e -> @@ -508,24 +549,28 @@ let global_inductive r = (********************************************************************) (* Registration of tables as a global table and rollback *) -type frozen = ccitab * dirtab * mptab - * globrevtab * mprevtab * mptrevtab +type frozen = ccitab * dirtab * mptab * univtab + * globrevtab * mprevtab * mptrevtab * univrevtab let freeze _ : frozen = !the_ccitab, !the_dirtab, !the_modtypetab, + !the_univtab, !the_globrevtab, !the_modrevtab, - !the_modtyperevtab + !the_modtyperevtab, + !the_univrevtab -let unfreeze (ccit,dirt,mtyt,globr,modr,mtyr) = +let unfreeze (ccit,dirt,mtyt,univt,globr,modr,mtyr,univr) = the_ccitab := ccit; the_dirtab := dirt; the_modtypetab := mtyt; + the_univtab := univt; the_globrevtab := globr; the_modrevtab := modr; - the_modtyperevtab := mtyr + the_modtyperevtab := mtyr; + the_univrevtab := univr let _ = Summary.declare_summary "names" diff --git a/library/nametab.mli b/library/nametab.mli index c02447a7c..77fafa100 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -78,6 +78,12 @@ val push_modtype : visibility -> full_path -> ModPath.t -> unit val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit val push_syndef : visibility -> full_path -> syndef_name -> unit +type universe_id = DirPath.t * int + +module UnivIdMap : CMap.ExtS with type key = universe_id + +val push_universe : visibility -> full_path -> universe_id -> unit + (** {6 The following functions perform globalization of qualified names } *) (** These functions globalize a (partially) qualified name or fail with @@ -91,6 +97,7 @@ val locate_modtype : qualid -> ModPath.t val locate_dir : qualid -> global_dir_reference val locate_module : qualid -> ModPath.t val locate_section : qualid -> DirPath.t +val locate_universe : qualid -> universe_id (** These functions globalize user-level references into global references, like [locate] and co, but raise a nice error message @@ -119,6 +126,7 @@ val exists_modtype : full_path -> bool val exists_dir : DirPath.t -> bool val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) +val exists_universe : full_path -> bool (** {6 These functions locate qualids into full user names } *) @@ -138,6 +146,10 @@ val path_of_global : global_reference -> 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 : universe_id -> full_path + (** Returns in particular the dirpath or the basename of the full path associated to global reference *) @@ -158,6 +170,7 @@ val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid val shortest_qualid_of_modtype : ModPath.t -> qualid val shortest_qualid_of_module : ModPath.t -> qualid +val shortest_qualid_of_universe : universe_id -> qualid (** Deprecated synonyms *) |