From b0ef649660542ae840ea945d7ab4f1f3ae7b85cd Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 17:58:08 +0200 Subject: Split off Universes functions dealing with names. This API is a bit strange, I expect it will change at some point. --- engine/engine.mllib | 1 + engine/evd.mli | 4 +- engine/termops.ml | 2 +- engine/uState.ml | 4 +- engine/uState.mli | 4 +- engine/univNames.ml | 105 +++++++++++++++++++++++++++++++++++++++++++++ engine/univNames.mli | 41 ++++++++++++++++++ engine/universes.ml | 117 +++++++++------------------------------------------ engine/universes.mli | 67 ++++++++++++++++------------- 9 files changed, 213 insertions(+), 132 deletions(-) create mode 100644 engine/univNames.ml create mode 100644 engine/univNames.mli (limited to 'engine') diff --git a/engine/engine.mllib b/engine/engine.mllib index a5df5a9fa..207dbde1e 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -1,3 +1,4 @@ +UnivNames Universes Univops UState diff --git a/engine/evd.mli b/engine/evd.mli index 509db525d..7ce525744 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -550,7 +550,7 @@ val constrain_variables : Univ.LSet.t -> UState.t -> UState.t val evar_universe_context_of_binders : - Universes.universe_binders -> UState.t + UnivNames.universe_binders -> UState.t [@@ocaml.deprecated "Alias of UState.of_binders"] val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t @@ -559,7 +559,7 @@ val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map (** Raises Not_found if not a name for a universe in this map. *) val universe_of_name : evar_map -> Id.t -> Univ.Level.t -val universe_binders : evar_map -> Universes.universe_binders +val universe_binders : evar_map -> UnivNames.universe_binders val add_constraints_context : UState.t -> Univ.Constraint.t -> UState.t [@@ocaml.deprecated "Alias of UState.add_constraints"] diff --git a/engine/termops.ml b/engine/termops.ml index df43be28e..9e975da58 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -47,7 +47,7 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) = let pr_puniverses p u = if Univ.Instance.is_empty u then p - else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" + else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" let rec pr_constr c = match kind c with | Rel n -> str "#"++int n diff --git a/engine/uState.ml b/engine/uState.ml index df50bae86..ffb54d441 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -24,7 +24,7 @@ module UPairSet = Universes.UPairSet (* 2nd part used to check consistency on the fly. *) type t = - { uctx_names : Universes.universe_binders * uinfo Univ.LMap.t; + { uctx_names : UnivNames.universe_binders * uinfo Univ.LMap.t; uctx_local : Univ.ContextSet.t; (** The local context of variables *) uctx_seff_univs : Univ.LSet.t; (** Local universes used through private constants *) uctx_univ_variables : Universes.universe_opt_subst; @@ -298,7 +298,7 @@ let reference_of_level uctx = fun l -> try CAst.make @@ Libnames.Ident (Option.get (Univ.LMap.find l map_rev).uname) with Not_found | Option.IsNone -> - Universes.reference_of_level l + UnivNames.reference_of_level l let pr_uctx_level uctx l = Libnames.pr_reference (reference_of_level uctx l) diff --git a/engine/uState.mli b/engine/uState.mli index 48c38fafc..b1fcefb0a 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -34,9 +34,9 @@ val union : t -> t -> t val of_context_set : Univ.ContextSet.t -> t -val of_binders : Universes.universe_binders -> t +val of_binders : UnivNames.universe_binders -> t -val universe_binders : t -> Universes.universe_binders +val universe_binders : t -> UnivNames.universe_binders (** {5 Projections} *) diff --git a/engine/univNames.ml b/engine/univNames.ml new file mode 100644 index 000000000..6e59a7c9e --- /dev/null +++ b/engine/univNames.ml @@ -0,0 +1,105 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + let qid = + try Nametab.shortest_qualid_of_universe na + with Not_found -> + let name = Id.of_string_soft (string_of_int n) in + Libnames.make_qualid d name + in Libnames.Qualid qid + | None -> Libnames.Ident Id.(of_string_soft (Level.to_string l)) + +let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l) + +(** Global universe information outside the kernel, to handle + polymorphic universe names in sections that have to be discharged. *) + +let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref) + +let add_global_universe u p = + match Level.name u with + | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map + | None -> () + +let is_polymorphic l = + match Level.name l with + | Some n -> + (try Nametab.UnivIdMap.find n !universe_map + with Not_found -> false) + | None -> false + +(** Local universe names of polymorphic references *) + +type universe_binders = Univ.Level.t Names.Id.Map.t + +let empty_binders = Id.Map.empty + +let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders" + +let universe_binders_of_global ref : universe_binders = + try + let l = Refmap.find ref !universe_binders_table in l + with Not_found -> Names.Id.Map.empty + +let cache_ubinder (_,(ref,l)) = + universe_binders_table := Refmap.add ref l !universe_binders_table + +let subst_ubinder (subst,(ref,l as orig)) = + let ref' = fst (Globnames.subst_global subst ref) in + if ref == ref' then orig else ref', l + +let discharge_ubinder (_,(ref,l)) = + Some (Lib.discharge_global ref, l) + +let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj = + let open Libobject in + declare_object { (default_object "universe binder") with + cache_function = cache_ubinder; + load_function = (fun _ x -> cache_ubinder x); + classify_function = (fun x -> Substitute x); + subst_function = subst_ubinder; + discharge_function = discharge_ubinder; + rebuild_function = (fun x -> x); } + +let register_universe_binders ref ubinders = + (* Add the polymorphic (section) universes *) + let ubinders = UnivIdMap.fold (fun lvl poly ubinders -> + let qid = Nametab.shortest_qualid_of_universe lvl in + let level = Level.make (fst lvl) (snd lvl) in + if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders + else ubinders) + !universe_map ubinders + in + if not (Id.Map.is_empty ubinders) + then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders)) + +type univ_name_list = Misctypes.lname list + +let universe_binders_with_opt_names ref levels = function + | None -> universe_binders_of_global ref + | Some udecl -> + if Int.equal(List.length levels) (List.length udecl) + then + List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with + | Anonymous -> acc + | Name na -> Names.Id.Map.add na lvl acc) + empty_binders udecl levels + else + CErrors.user_err ~hdr:"universe_binders_with_opt_names" + Pp.(str "Universe instance should have length " ++ int (List.length levels)) diff --git a/engine/univNames.mli b/engine/univNames.mli new file mode 100644 index 000000000..e3bc3193d --- /dev/null +++ b/engine/univNames.mli @@ -0,0 +1,41 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Pp.t +val reference_of_level : Level.t -> Libnames.reference + +(** Global universe information outside the kernel, to handle + polymorphic universes in sections that have to be discharged. *) +val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit + +(** Is [lvl] a global polymorphic universe? (ie section polymorphic universe) *) +val is_polymorphic : Level.t -> bool + +(** Local universe name <-> level mapping *) + +type universe_binders = Univ.Level.t Names.Id.Map.t + +val empty_binders : universe_binders + +val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit +val universe_binders_of_global : Names.GlobRef.t -> universe_binders + +type univ_name_list = Misctypes.lname list + +(** [universe_binders_with_opt_names ref u l] + + If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous). + May error if the lengths mismatch. + + Otherwise return [universe_binders_of_global ref]. *) +val universe_binders_with_opt_names : Names.GlobRef.t -> + Univ.Level.t list -> univ_name_list option -> universe_binders diff --git a/engine/universes.ml b/engine/universes.ml index 96d49361f..1dccde025 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -15,102 +15,6 @@ open Names open Constr open Environ open Univ -open Globnames -open Nametab - -module UPairs = OrderedType.UnorderedPair(Univ.Level) -module UPairSet = Set.Make (UPairs) - -let reference_of_level l = CAst.make @@ - match Level.name l with - | Some (d, n as na) -> - let qid = - try Nametab.shortest_qualid_of_universe na - with Not_found -> - let name = Id.of_string_soft (string_of_int n) in - Libnames.make_qualid d name - in Libnames.Qualid qid - | None -> Libnames.Ident Id.(of_string_soft (Level.to_string l)) - -let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l) - -(** Global universe information outside the kernel, to handle - polymorphic universe names in sections that have to be discharged. *) - -let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref) - -let add_global_universe u p = - match Level.name u with - | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map - | None -> () - -let is_polymorphic l = - match Level.name l with - | Some n -> - (try Nametab.UnivIdMap.find n !universe_map - with Not_found -> false) - | None -> false - -(** Local universe names of polymorphic references *) - -type universe_binders = Univ.Level.t Names.Id.Map.t - -let empty_binders = Id.Map.empty - -let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders" - -let universe_binders_of_global ref : universe_binders = - try - let l = Refmap.find ref !universe_binders_table in l - with Not_found -> Names.Id.Map.empty - -let cache_ubinder (_,(ref,l)) = - universe_binders_table := Refmap.add ref l !universe_binders_table - -let subst_ubinder (subst,(ref,l as orig)) = - let ref' = fst (Globnames.subst_global subst ref) in - if ref == ref' then orig else ref', l - -let discharge_ubinder (_,(ref,l)) = - Some (Lib.discharge_global ref, l) - -let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj = - let open Libobject in - declare_object { (default_object "universe binder") with - cache_function = cache_ubinder; - load_function = (fun _ x -> cache_ubinder x); - classify_function = (fun x -> Substitute x); - subst_function = subst_ubinder; - discharge_function = discharge_ubinder; - rebuild_function = (fun x -> x); } - -let register_universe_binders ref ubinders = - let open Names in - (* Add the polymorphic (section) universes *) - let ubinders = UnivIdMap.fold (fun lvl poly ubinders -> - let qid = Nametab.shortest_qualid_of_universe lvl in - let level = Level.make (fst lvl) (snd lvl) in - if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders - else ubinders) - !universe_map ubinders - in - if not (Id.Map.is_empty ubinders) - then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders)) - -type univ_name_list = Misctypes.lname list - -let universe_binders_with_opt_names ref levels = function - | None -> universe_binders_of_global ref - | Some udecl -> - if Int.equal(List.length levels) (List.length udecl) - then - List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with - | Anonymous -> acc - | Name na -> Names.Id.Map.add na lvl acc) - empty_binders udecl levels - else - CErrors.user_err ~hdr:"universe_binders_with_opt_names" - Pp.(str "Universe instance should have length " ++ int (List.length levels)) (* To disallow minimization to Set *) @@ -917,6 +821,9 @@ let minimize_univ_variables ctx us algs left right cstrs = else LSet.remove u ctx, us, LSet.remove u algs, seen, cstrs) us (ctx, us, algs, lbounds, cstrs) +module UPairs = OrderedType.UnorderedPair(Univ.Level) +module UPairSet = Set.Make (UPairs) + let normalize_context_set g ctx us algs weak = let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in (** Keep the Prop/Set <= i constraints separate for minimization *) @@ -1111,3 +1018,21 @@ let solve_constraints_system levels level_bounds level_min = done; done; v + +(** Deprecated *) +type universe_binders = UnivNames.universe_binders +type univ_name_list = UnivNames.univ_name_list + +let pr_with_global_universes = UnivNames.pr_with_global_universes +let reference_of_level = UnivNames.reference_of_level + +let add_global_universe = UnivNames.add_global_universe + +let is_polymorphic = UnivNames.is_polymorphic + +let empty_binders = UnivNames.empty_binders + +let register_universe_binders = UnivNames.register_universe_binders +let universe_binders_of_global = UnivNames.universe_binders_of_global + +let universe_binders_with_opt_names = UnivNames.universe_binders_with_opt_names diff --git a/engine/universes.mli b/engine/universes.mli index 46d65f257..aaf295c1d 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -19,35 +19,6 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t) (** Universes *) -val pr_with_global_universes : Level.t -> Pp.t -val reference_of_level : Level.t -> Libnames.reference - -(** Global universe information outside the kernel, to handle - polymorphic universes in sections that have to be discharged. *) -val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit - -val is_polymorphic : Level.t -> bool - -(** Local universe name <-> level mapping *) - -type universe_binders = Univ.Level.t Names.Id.Map.t - -val empty_binders : universe_binders - -val register_universe_binders : GlobRef.t -> universe_binders -> unit -val universe_binders_of_global : GlobRef.t -> universe_binders - -type univ_name_list = Misctypes.lname list - -(** [universe_binders_with_opt_names ref u l] - - If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous). - May error if the lengths mismatch. - - Otherwise return [universe_binders_of_global ref]. *) -val universe_binders_with_opt_names : Names.GlobRef.t -> - Univ.Level.t list -> univ_name_list option -> universe_binders - (** The global universe counter *) type universe_id = DirPath.t * int @@ -226,3 +197,41 @@ val pr_universe_opt_subst : universe_opt_subst -> Pp.t val solve_constraints_system : Universe.t option array -> Universe.t array -> Universe.t array -> Universe.t array + +(** *********************************** Deprecated *) +[@@@ocaml.warning "-3"] +val set_minimization : bool ref +[@@ocaml.deprecated "Becoming internal."] +val is_set_minimization : unit -> bool +[@@ocaml.deprecated "Becoming internal."] + +(** ****** Deprecated: moved to [UnivNames] *) + +val pr_with_global_universes : Level.t -> Pp.t +[@@ocaml.deprecated "Use [UnivNames.pr_with_global_universes]"] +val reference_of_level : Level.t -> Libnames.reference +[@@ocaml.deprecated "Use [UnivNames.reference_of_level]"] + +val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit +[@@ocaml.deprecated "Use [UnivNames.add_global_universe]"] + +val is_polymorphic : Level.t -> bool +[@@ocaml.deprecated "Use [UnivNames.is_polymorphic]"] + +type universe_binders = UnivNames.universe_binders +[@@ocaml.deprecated "Use [UnivNames.universe_binders]"] + +val empty_binders : universe_binders +[@@ocaml.deprecated "Use [UnivNames.empty_binders]"] + +val register_universe_binders : Globnames.global_reference -> universe_binders -> unit +[@@ocaml.deprecated "Use [UnivNames.register_universe_binders]"] +val universe_binders_of_global : Globnames.global_reference -> universe_binders +[@@ocaml.deprecated "Use [UnivNames.universe_binders_of_global]"] + +type univ_name_list = UnivNames.univ_name_list +[@@ocaml.deprecated "Use [UnivNames.univ_name_list]"] + +val universe_binders_with_opt_names : Globnames.global_reference -> + Univ.Level.t list -> univ_name_list option -> universe_binders +[@@ocaml.deprecated "Use [UnivNames.universe_binders_with_opt_names]"] -- cgit v1.2.3