diff options
Diffstat (limited to 'engine/universes.mli')
| -rw-r--r-- | engine/universes.mli | 262 |
1 files changed, 133 insertions, 129 deletions
diff --git a/engine/universes.mli b/engine/universes.mli index 4823c574..ad937471 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -8,227 +8,231 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Util open Names open Constr open Environ open Univ -(** Unordered pairs of universe levels (ie (u,v) = (v,u)) *) -module UPairSet : CSet.S with type elt = (Level.t * Level.t) +(** ************************************** *) +(** This entire module is deprecated. **** *) +(** ************************************** *) +[@@@ocaml.warning "-3"] -val set_minimization : bool ref -val is_set_minimization : unit -> bool - -(** Universes *) +(** ****** Deprecated: moved to [UnivNames] *) val pr_with_global_universes : Level.t -> Pp.t -val reference_of_level : Level.t -> Libnames.reference +[@@ocaml.deprecated "Use [UnivNames.pr_with_global_universes]"] +val reference_of_level : Level.t -> Libnames.qualid +[@@ocaml.deprecated "Use [UnivNames.qualid_of_level]"] -(** 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 +[@@ocaml.deprecated "Use [UnivNames.add_global_universe]"] val is_polymorphic : Level.t -> bool +[@@ocaml.deprecated "Use [UnivNames.is_polymorphic]"] -(** Local universe name <-> level mapping *) - -type universe_binders = Univ.Level.t Names.Id.Map.t +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 = Misctypes.lname list - -(** [universe_binders_with_opt_names ref u l] +type univ_name_list = UnivNames.univ_name_list +[@@ocaml.deprecated "Use [UnivNames.univ_name_list]"] - 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 : Globnames.global_reference -> Univ.Level.t list -> univ_name_list option -> universe_binders +[@@ocaml.deprecated "Use [UnivNames.universe_binders_with_opt_names]"] -(** The global universe counter *) -type universe_id = DirPath.t * int +(** ****** Deprecated: moved to [UnivGen] *) -val set_remote_new_univ_id : universe_id RemoteCounter.installer +type universe_id = UnivGen.universe_id +[@@ocaml.deprecated "Use [UnivGen.universe_id]"] -(** Side-effecting functions creating new universe levels. *) +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 -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 - 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 +[@@ocaml.deprecated "Use [UnivGen.new_global_univ]"] -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 - -(** Build a fresh instance for a given context, its associated substitution and - the instantiated constraints. *) +val new_sort_in_family : Sorts.family -> Sorts.t +[@@ocaml.deprecated "Use [UnivGen.new_sort_in_family]"] -val fresh_instance_from_context : AUContext.t -> +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 -> +val fresh_sort_in_family : 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 -> +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 -> +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]"] -(** 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 -> +val fresh_universe_context_set_instance : ContextSet.t -> universe_level_subst * ContextSet.t +[@@ocaml.deprecated "Use [UnivGen.fresh_universe_context_set_instance]"] -(** Raises [Not_found] if not a global reference. *) 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 -> +val extend_context : 'a in_universe_context_set -> ContextSet.t -> 'a in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.extend_context]"] -(** Simplification and pruning of constraints: - [normalize_context_set ctx us] +val constr_of_global : Globnames.global_reference -> constr +[@@ocaml.deprecated "Use [UnivGen.constr_of_global]"] - - Instantiate the variables in [us] with their most precise - universe levels respecting the constraints. +val constr_of_reference : Globnames.global_reference -> constr +[@@ocaml.deprecated "Use [UnivGen.constr_of_global]"] - - 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 type_of_global : Globnames.global_reference -> types in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.type_of_global]"] -module UF : Unionfind.PartitionSig with type elt = Level.t +(** ****** 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 = Universe.t option universe_map +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_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 * universe_subst +[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variables]"] -val normalize_univ_variables : universe_opt_subst -> - universe_opt_subst * LSet.t * LSet.t * universe_subst - -val normalize_univ_variable : +val normalize_univ_variable : find:(Level.t -> Universe.t) -> - update:(Level.t -> Universe.t -> Universe.t) -> Level.t -> Universe.t +[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variable]"] -val normalize_univ_variable_opt_subst : universe_opt_subst ref -> +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 ref -> +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 ref -> +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 ref -> +val normalize_universe_subst : universe_subst -> (Universe.t -> Universe.t) +[@@ocaml.deprecated "Use [UnivSubst.normalize_universe_subst]"] -(** 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 : Globnames.global_reference -> constr +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]"] -(** ** DEPRECATED ** synonym of [constr_of_global] *) -val constr_of_reference : Globnames.global_reference -> constr -[@@ocaml.deprecated "synonym of [constr_of_global]"] +val pr_universe_opt_subst : universe_opt_subst -> Pp.t +[@@ocaml.deprecated "Use [UnivSubst.pr_universe_opt_subst]"] -(** 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 : Globnames.global_reference -> types in_universe_context_set +(** ****** Deprecated: moved to [UnivProblem] *) -(** Full universes substitutions into terms *) +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]"] -val nf_evars_and_universes_opt_subst : (existential -> constr option) -> - universe_opt_subst -> constr -> constr +module Constraints = UnivProblem.Set +[@@ocaml.deprecated "Use [UnivProblem.Set]"] -val refresh_constraints : UGraph.t -> ContextSet.t -> ContextSet.t * UGraph.t +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]"] -(** Pretty-printing *) +val subst_univs_universe_constraints : universe_subst_fn -> + Constraints.t -> Constraints.t +[@@ocaml.deprecated "Use [UnivProblem.Set.subst_univs]"] -val pr_universe_opt_subst : universe_opt_subst -> Pp.t +val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function +[@@ocaml.deprecated "Use [UnivProblem.enforce_eq_instances_univs]"] -(** {6 Support for template polymorphism } *) +(** 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]"] -val solve_constraints_system : Universe.t option array -> Universe.t array -> Universe.t array -> - Universe.t array +(** [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]"] + +(** ****** 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]"] |