From aa5e962c9888889380ae85a7cbd82a8ac4779a0f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 17:26:18 +0200 Subject: Make set minimization option internal to Universes --- engine/universes.mli | 3 --- 1 file changed, 3 deletions(-) (limited to 'engine/universes.mli') diff --git a/engine/universes.mli b/engine/universes.mli index df2e961d60..46d65f257e 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -17,9 +17,6 @@ open Univ (** Unordered pairs of universe levels (ie (u,v) = (v,u)) *) module UPairSet : CSet.S with type elt = (Level.t * Level.t) -val set_minimization : bool ref -val is_set_minimization : unit -> bool - (** Universes *) val pr_with_global_universes : Level.t -> Pp.t -- cgit v1.2.3 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/universes.mli | 67 +++++++++++++++++++++++++++++----------------------- 1 file changed, 38 insertions(+), 29 deletions(-) (limited to 'engine/universes.mli') diff --git a/engine/universes.mli b/engine/universes.mli index 46d65f257e..aaf295c1db 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 From a51dda2344679dc6d9145f3f34acad29721f6c75 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 19:26:21 +0200 Subject: Split off Universes functions dealing with generating new universes. --- engine/universes.mli | 154 ++++++++++++++++++++++++++++----------------------- 1 file changed, 85 insertions(+), 69 deletions(-) (limited to 'engine/universes.mli') diff --git a/engine/universes.mli b/engine/universes.mli index aaf295c1db..da4a007515 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -19,22 +19,6 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t) (** Universes *) -(** The global universe counter *) -type universe_id = DirPath.t * int - -val set_remote_new_univ_id : universe_id RemoteCounter.installer - -(** Side-effecting functions creating new universe levels. *) - -val new_univ_id : unit -> universe_id -val new_univ_level : unit -> Level.t -val new_univ : unit -> Universe.t -val new_Type : unit -> types -val new_Type_sort : unit -> Sorts.t - -val new_global_univ : unit -> Universe.t in_universe_context_set -val new_sort_in_family : Sorts.family -> Sorts.t - (** {6 Constraints for type inference} When doing conversion of universes, not only do we have =/<= constraints but @@ -82,43 +66,6 @@ val eq_constr_univs_infer_with : (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option -(** Build a fresh instance for a given context, its associated substitution and - the instantiated constraints. *) - -val fresh_instance_from_context : AUContext.t -> - Instance.t constrained - -val fresh_instance_from : AUContext.t -> Instance.t option -> - Instance.t in_universe_context_set - -val fresh_sort_in_family : env -> Sorts.family -> - Sorts.t in_universe_context_set -val fresh_constant_instance : env -> Constant.t -> - pconstant in_universe_context_set -val fresh_inductive_instance : env -> inductive -> - pinductive in_universe_context_set -val fresh_constructor_instance : env -> constructor -> - pconstructor in_universe_context_set - -val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t -> - constr in_universe_context_set - -val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> - constr in_universe_context_set - -(** Get fresh variables for the universe context. - Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) -val fresh_universe_context_set_instance : ContextSet.t -> - universe_level_subst * ContextSet.t - -(** Raises [Not_found] if not a global reference. *) -val global_of_constr : constr -> GlobRef.t puniverses - -val constr_of_global_univ : GlobRef.t puniverses -> constr - -val extend_context : 'a in_universe_context_set -> ContextSet.t -> - 'a in_universe_context_set - (** Simplification and pruning of constraints: [normalize_context_set ctx us] @@ -166,22 +113,6 @@ val normalize_universe_opt_subst : universe_opt_subst -> val normalize_universe_subst : universe_subst -> (Universe.t -> Universe.t) -(** Create a fresh global in the global environment, without side effects. - BEWARE: this raises an ANOMALY on polymorphic constants/inductives: - the constraints should be properly added to an evd. - See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for - the proper way to get a fresh copy of a global reference. *) -val constr_of_global : GlobRef.t -> constr - -(** ** DEPRECATED ** synonym of [constr_of_global] *) -val constr_of_reference : GlobRef.t -> constr -[@@ocaml.deprecated "synonym of [constr_of_global]"] - -(** Returns the type of the global reference, by creating a fresh instance of polymorphic - references and computing their instantiated universe context. (side-effect on the - universe counter, use with care). *) -val type_of_global : GlobRef.t -> types in_universe_context_set - (** Full universes substitutions into terms *) val nf_evars_and_universes_opt_subst : (existential -> constr option) -> @@ -199,6 +130,7 @@ val solve_constraints_system : Universe.t option array -> Universe.t array -> Un Universe.t array (** *********************************** Deprecated *) + [@@@ocaml.warning "-3"] val set_minimization : bool ref [@@ocaml.deprecated "Becoming internal."] @@ -235,3 +167,87 @@ type univ_name_list = 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]"] + +(** ****** Deprecated: moved to [UnivGen] *) + +type universe_id = UnivGen.universe_id +[@@ocaml.deprecated "Use [UnivGen.universe_id]"] + +val set_remote_new_univ_id : universe_id RemoteCounter.installer +[@@ocaml.deprecated "Use [UnivGen.set_remote_new_univ_id]"] + +val new_univ_id : unit -> universe_id +[@@ocaml.deprecated "Use [UnivGen.new_univ_id]"] + +val new_univ_level : unit -> Level.t +[@@ocaml.deprecated "Use [UnivGen.new_univ_level]"] + +val new_univ : unit -> Universe.t +[@@ocaml.deprecated "Use [UnivGen.new_univ]"] + +val new_Type : unit -> types +[@@ocaml.deprecated "Use [UnivGen.new_Type]"] + +val new_Type_sort : unit -> Sorts.t +[@@ocaml.deprecated "Use [UnivGen.new_Type_sort]"] + +val new_global_univ : unit -> Universe.t in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.new_global_univ]"] + +val new_sort_in_family : Sorts.family -> Sorts.t +[@@ocaml.deprecated "Use [UnivGen.new_sort_in_family]"] + +val fresh_instance_from_context : AUContext.t -> + Instance.t constrained +[@@ocaml.deprecated "Use [UnivGen.fresh_instance_from_context]"] + +val fresh_instance_from : AUContext.t -> Instance.t option -> + Instance.t in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_instance_from]"] + +val fresh_sort_in_family : env -> Sorts.family -> + Sorts.t in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_sort_in_family]"] + +val fresh_constant_instance : env -> Constant.t -> + pconstant in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_constant_instance]"] + +val fresh_inductive_instance : env -> inductive -> + pinductive in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_inductive_instance]"] + +val fresh_constructor_instance : env -> constructor -> + pconstructor in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_constructor_instance]"] + +val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_reference -> + constr in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_global_instance]"] + +val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> + constr in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_global_or_constr_instance]"] + +val fresh_universe_context_set_instance : ContextSet.t -> + universe_level_subst * ContextSet.t +[@@ocaml.deprecated "Use [UnivGen.fresh_universe_context_set_instance]"] + +val global_of_constr : constr -> Globnames.global_reference puniverses +[@@ocaml.deprecated "Use [UnivGen.global_of_constr]"] + +val constr_of_global_univ : Globnames.global_reference puniverses -> constr +[@@ocaml.deprecated "Use [UnivGen.constr_of_global_univ]"] + +val extend_context : 'a in_universe_context_set -> ContextSet.t -> + 'a in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.extend_context]"] + +val constr_of_global : Globnames.global_reference -> constr +[@@ocaml.deprecated "Use [UnivGen.constr_of_global]"] + +val constr_of_reference : Globnames.global_reference -> constr +[@@ocaml.deprecated "Use [UnivGen.constr_of_global]"] + +val type_of_global : Globnames.global_reference -> types in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.type_of_global]"] -- cgit v1.2.3 From a7153b347f8196122394e9ce912055cdf9e575ae Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 19:47:48 +0200 Subject: Move solve_constraint_system near its only use site (comInductive) --- engine/universes.mli | 5 ----- 1 file changed, 5 deletions(-) (limited to 'engine/universes.mli') diff --git a/engine/universes.mli b/engine/universes.mli index da4a007515..bd315f2778 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -124,11 +124,6 @@ val refresh_constraints : UGraph.t -> ContextSet.t -> ContextSet.t * UGraph.t val pr_universe_opt_subst : universe_opt_subst -> Pp.t -(** {6 Support for template polymorphism } *) - -val solve_constraints_system : Universe.t option array -> Universe.t array -> Universe.t array -> - Universe.t array - (** *********************************** Deprecated *) [@@@ocaml.warning "-3"] -- cgit v1.2.3 From 302adae094bbf76d8c951c557c85acb12a97aedc Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 21:27:15 +0200 Subject: Split off Universes functions about substitutions and constraints --- engine/universes.mli | 180 ++++++++++++++++++++++++++------------------------- 1 file changed, 93 insertions(+), 87 deletions(-) (limited to 'engine/universes.mli') diff --git a/engine/universes.mli b/engine/universes.mli index bd315f2778..3e397ed577 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -8,64 +8,17 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Util open Names open Constr open Environ open Univ +open UnivSubst (** Unordered pairs of universe levels (ie (u,v) = (v,u)) *) module UPairSet : CSet.S with type elt = (Level.t * Level.t) (** Universes *) -(** {6 Constraints for type inference} - - When doing conversion of universes, not only do we have =/<= constraints but - also Lub constraints which correspond to unification of two levels which might - not be necessary if unfolding is performed. - - UWeak constraints come from irrelevant universes in cumulative polymorphism. -*) - -type universe_constraint = - | ULe of Universe.t * Universe.t - | UEq of Universe.t * Universe.t - | ULub of Level.t * Level.t - | UWeak of Level.t * Level.t - -module Constraints : sig - include Set.S with type elt = universe_constraint - - val is_trivial : universe_constraint -> bool - - val pr : t -> Pp.t -end - -type universe_constraints = Constraints.t -[@@ocaml.deprecated "Use Constraints.t"] - -type 'a constraint_accumulator = Constraints.t -> 'a -> 'a option -type 'a universe_constrained = 'a * Constraints.t -type 'a universe_constraint_function = 'a -> 'a -> Constraints.t -> Constraints.t - -val subst_univs_universe_constraints : universe_subst_fn -> - Constraints.t -> Constraints.t - -val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function - -(** With [force_weak] UWeak constraints are turned into equalities, - otherwise they're forgotten. *) -val to_constraints : force_weak:bool -> UGraph.t -> Constraints.t -> Constraint.t - -(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of - {!eq_constr_univs_infer} taking kind-of-term functions, to expose - subterms of [m] and [n], arguments. *) -val eq_constr_univs_infer_with : - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option - (** Simplification and pruning of constraints: [normalize_context_set ctx us] @@ -77,53 +30,14 @@ val eq_constr_univs_infer_with : (a global one if there is one) and transitively saturate the constraints w.r.t to the equalities. *) -val level_subst_of : universe_subst_fn -> universe_level_subst_fn -val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t - -val subst_univs_constr : universe_subst -> constr -> constr - -type universe_opt_subst = Universe.t option universe_map - -val make_opt_subst : universe_opt_subst -> universe_subst_fn - -val subst_opt_univs_constr : universe_opt_subst -> constr -> constr - val normalize_context_set : UGraph.t -> ContextSet.t -> universe_opt_subst (* The defined and undefined variables *) -> LSet.t (* univ variables that can be substituted by algebraics *) -> UPairSet.t (* weak equality constraints *) -> (universe_opt_subst * LSet.t) in_universe_context_set -val normalize_univ_variables : universe_opt_subst -> - universe_opt_subst * LSet.t * LSet.t * universe_subst - -val normalize_univ_variable : - find:(Level.t -> Universe.t) -> - Level.t -> Universe.t - -val normalize_univ_variable_opt_subst : universe_opt_subst -> - (Level.t -> Universe.t) - -val normalize_univ_variable_subst : universe_subst -> - (Level.t -> Universe.t) - -val normalize_universe_opt_subst : universe_opt_subst -> - (Universe.t -> Universe.t) - -val normalize_universe_subst : universe_subst -> - (Universe.t -> Universe.t) - -(** Full universes substitutions into terms *) - -val nf_evars_and_universes_opt_subst : (existential -> constr option) -> - universe_opt_subst -> constr -> constr - val refresh_constraints : UGraph.t -> ContextSet.t -> ContextSet.t * UGraph.t -(** Pretty-printing *) - -val pr_universe_opt_subst : universe_opt_subst -> Pp.t - (** *********************************** Deprecated *) [@@@ocaml.warning "-3"] @@ -246,3 +160,95 @@ val constr_of_reference : Globnames.global_reference -> constr val type_of_global : Globnames.global_reference -> types in_universe_context_set [@@ocaml.deprecated "Use [UnivGen.type_of_global]"] + +(** ****** Deprecated: moved to [UnivSubst] *) + +val level_subst_of : universe_subst_fn -> universe_level_subst_fn +[@@ocaml.deprecated "Use [UnivSubst.level_subst_of]"] + +val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t +[@@ocaml.deprecated "Use [UnivSubst.subst_univs_constraints]"] + +val subst_univs_constr : universe_subst -> constr -> constr +[@@ocaml.deprecated "Use [UnivSubst.subst_univs_constr]"] + +type universe_opt_subst = UnivSubst.universe_opt_subst +[@@ocaml.deprecated "Use [UnivSubst.universe_opt_subst]"] + +val make_opt_subst : universe_opt_subst -> universe_subst_fn +[@@ocaml.deprecated "Use [UnivSubst.make_opt_subst]"] + +val subst_opt_univs_constr : universe_opt_subst -> constr -> constr +[@@ocaml.deprecated "Use [UnivSubst.subst_opt_univs_constr]"] + +val normalize_univ_variables : universe_opt_subst -> + universe_opt_subst * LSet.t * LSet.t * universe_subst +[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variables]"] + +val normalize_univ_variable : + find:(Level.t -> Universe.t) -> + Level.t -> Universe.t +[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variable]"] + +val normalize_univ_variable_opt_subst : universe_opt_subst -> + (Level.t -> Universe.t) +[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variable_opt_subst]"] + +val normalize_univ_variable_subst : universe_subst -> + (Level.t -> Universe.t) +[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variable_subst]"] + +val normalize_universe_opt_subst : universe_opt_subst -> + (Universe.t -> Universe.t) +[@@ocaml.deprecated "Use [UnivSubst.normalize_universe_opt_subst]"] + +val normalize_universe_subst : universe_subst -> + (Universe.t -> Universe.t) +[@@ocaml.deprecated "Use [UnivSubst.normalize_universe_subst]"] + +val nf_evars_and_universes_opt_subst : (existential -> constr option) -> + universe_opt_subst -> constr -> constr +[@@ocaml.deprecated "Use [UnivSubst.nf_evars_and_universes_opt_subst]"] + +val pr_universe_opt_subst : universe_opt_subst -> Pp.t +[@@ocaml.deprecated "Use [UnivSubst.pr_universe_opt_subst]"] + +(** ****** Deprecated: moved to [UnivProblem] *) + +type universe_constraint = UnivProblem.t = + | ULe of Universe.t * Universe.t [@ocaml.deprecated "Use [UnivProblem.ULe]"] + | UEq of Universe.t * Universe.t [@ocaml.deprecated "Use [UnivProblem.UEq]"] + | ULub of Level.t * Level.t [@ocaml.deprecated "Use [UnivProblem.ULub]"] + | UWeak of Level.t * Level.t [@ocaml.deprecated "Use [UnivProblem.UWeak]"] +[@@ocaml.deprecated "Use [UnivProblem.t]"] + +module Constraints = UnivProblem.Set +[@@ocaml.deprecated "Use [UnivProblem.Set]"] + +type 'a constraint_accumulator = 'a UnivProblem.accumulator +[@@ocaml.deprecated "Use [UnivProblem.accumulator]"] +type 'a universe_constrained = 'a UnivProblem.constrained +[@@ocaml.deprecated "Use [UnivProblem.constrained]"] +type 'a universe_constraint_function = 'a UnivProblem.constraint_function +[@@ocaml.deprecated "Use [UnivProblem.constraint_function]"] + +val subst_univs_universe_constraints : universe_subst_fn -> + Constraints.t -> Constraints.t +[@@ocaml.deprecated "Use [UnivProblem.Set.subst_univs]"] + +val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function +[@@ocaml.deprecated "Use [UnivProblem.enforce_eq_instances_univs]"] + +(** With [force_weak] UWeak constraints are turned into equalities, + otherwise they're forgotten. *) +val to_constraints : force_weak:bool -> UGraph.t -> Constraints.t -> Constraint.t +[@@ocaml.deprecated "Use [UnivProblem.to_constraints]"] + +(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of + {!eq_constr_univs_infer} taking kind-of-term functions, to expose + subterms of [m] and [n], arguments. *) +val eq_constr_univs_infer_with : + (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> + (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> + UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option +[@@ocaml.deprecated "Use [UnivProblem.eq_constr_univs_infer_with]"] -- cgit v1.2.3 From d41eaff0b2c6f2ff10ef851864abfa3366862d22 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 21:30:59 +0200 Subject: Make Universes.refresh_constraints internal to UState --- engine/universes.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'engine/universes.mli') diff --git a/engine/universes.mli b/engine/universes.mli index 3e397ed577..4d7105e726 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -36,8 +36,6 @@ val normalize_context_set : UGraph.t -> ContextSet.t -> UPairSet.t (* weak equality constraints *) -> (universe_opt_subst * LSet.t) in_universe_context_set -val refresh_constraints : UGraph.t -> ContextSet.t -> ContextSet.t * UGraph.t - (** *********************************** Deprecated *) [@@@ocaml.warning "-3"] -- cgit v1.2.3 From 748a33cee41900d285897b24b4d8e29dd9eb2a3d Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 21:36:57 +0200 Subject: Split off Universes functions for minimization. This finishes the splitting of Universes. --- engine/universes.mli | 44 +++++++++++++++----------------------------- 1 file changed, 15 insertions(+), 29 deletions(-) (limited to 'engine/universes.mli') diff --git a/engine/universes.mli b/engine/universes.mli index 4d7105e726..46ff33a473 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -12,37 +12,11 @@ open Names open Constr open Environ open Univ -open UnivSubst - -(** Unordered pairs of universe levels (ie (u,v) = (v,u)) *) -module UPairSet : CSet.S with type elt = (Level.t * Level.t) - -(** Universes *) - -(** Simplification and pruning of constraints: - [normalize_context_set ctx us] - - - Instantiate the variables in [us] with their most precise - universe levels respecting the constraints. - - - Normalizes the context [ctx] w.r.t. equality constraints, - choosing a canonical universe in each equivalence class - (a global one if there is one) and transitively saturate - the constraints w.r.t to the equalities. *) - -val normalize_context_set : UGraph.t -> ContextSet.t -> - universe_opt_subst (* The defined and undefined variables *) -> - LSet.t (* univ variables that can be substituted by algebraics *) -> - UPairSet.t (* weak equality constraints *) -> - (universe_opt_subst * LSet.t) in_universe_context_set - -(** *********************************** Deprecated *) +(** ************************************** *) +(** This entire module is 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] *) @@ -250,3 +224,15 @@ val eq_constr_univs_infer_with : (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option [@@ocaml.deprecated "Use [UnivProblem.eq_constr_univs_infer_with]"] + +(** ****** Deprecated: moved to [UnivMinim] *) + +module UPairSet = UnivMinim.UPairSet +[@@ocaml.deprecated "Use [UnivMinim.UPairSet]"] + +val normalize_context_set : UGraph.t -> ContextSet.t -> + universe_opt_subst (* The defined and undefined variables *) -> + LSet.t (* univ variables that can be substituted by algebraics *) -> + UPairSet.t (* weak equality constraints *) -> + (universe_opt_subst * LSet.t) in_universe_context_set +[@@ocaml.deprecated "Use [UnivMinim.normalize_context_set]"] -- cgit v1.2.3