diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evarutil.ml | 38 | ||||
| -rw-r--r-- | engine/evarutil.mli | 30 | ||||
| -rw-r--r-- | engine/termops.mli | 12 | ||||
| -rw-r--r-- | engine/universes.ml | 92 | ||||
| -rw-r--r-- | engine/universes.mli | 230 |
5 files changed, 1 insertions, 401 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index b1d880b0ad..fc2189f870 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -11,7 +11,6 @@ open CErrors open Util open Names -open Term open Constr open Environ open Evd @@ -43,9 +42,6 @@ let evd_comb2 f evdref x y = evdref := evd'; z -let e_new_global evdref x = - evd_comb1 (Evd.fresh_global (Global.env())) evdref x - let new_global evd x = let (evd, c) = Evd.fresh_global (Global.env()) evd x in (evd, c) @@ -87,23 +83,6 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} = let nf_evars_universes evm = UnivSubst.nf_evars_and_universes_opt_subst (safe_evar_value evm) (Evd.universe_subst evm) - -let nf_evars_and_universes evm = - let evm = Evd.minimize_universes evm in - evm, nf_evars_universes evm - -let e_nf_evars_and_universes evdref = - evdref := Evd.minimize_universes !evdref; - nf_evars_universes !evdref, Evd.universe_subst !evdref - -let nf_evar_map_universes evm = - let evm = Evd.minimize_universes evm in - let subst = Evd.universe_subst evm in - if Univ.LMap.is_empty subst then evm, nf_evar0 evm - else - let f = nf_evars_universes evm in - let f' c = EConstr.of_constr (f (EConstr.Unsafe.to_constr c)) in - Evd.raw_map (fun _ -> map_evar_info f') evm, f let nf_named_context_evar sigma ctx = Context.Named.map (nf_evar0 sigma) ctx @@ -490,26 +469,11 @@ let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid = let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in evd', (e, s) -let e_new_type_evar env evdref ?src ?filter ?naming ?principal ?hypnaming rigid = - let (evd, c) = new_type_evar env !evdref ?src ?filter ?naming ?principal ?hypnaming rigid in - evdref := evd; - c - let new_Type ?(rigid=Evd.univ_flexible) evd = let open EConstr in let (evd, s) = new_sort_variable rigid evd in (evd, mkSort s) -let e_new_Type ?(rigid=Evd.univ_flexible) evdref = - let evd', s = new_sort_variable rigid !evdref in - evdref := evd'; EConstr.mkSort s - - (* The same using side-effect *) -let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ?hypnaming ty = - let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ?hypnaming ty in - evdref := evd'; - ev - (* Safe interface to unification problems *) type unification_pb = conv_pb * env * EConstr.constr * EConstr.constr @@ -853,7 +817,7 @@ let occur_evar_upto sigma n c = let judge_of_new_Type evd = let open EConstr in let (evd', s) = new_univ_variable univ_rigid evd in - (evd', { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }) + (evd', { uj_val = mkSort (Sorts.Type s); uj_type = mkSort (Sorts.Type (Univ.super s)) }) let subterm_source evk ?where (loc,k) = let evk = match k with diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 0ad323ac4b..1046fdc8d8 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -173,14 +173,6 @@ val nf_evar_map_undefined : evar_map -> evar_map val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr -val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) -[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] - -(** Normalize the evar map w.r.t. universes, after simplification of constraints. - Return the substitution function for constrs as well. *) -val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) -[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evar_map and nf_evars_universes"] - (** Replacing all evars, possibly raising [Uninstantiated_evar] *) exception Uninstantiated_evar of Evar.t val flush_and_check_evars : evar_map -> constr -> Constr.constr @@ -273,25 +265,3 @@ val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Lo Evar_kinds.t Loc.located val meta_counter_summary_tag : int Summary.Dyn.tag - -val e_new_evar : - env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> - ?naming:intro_pattern_naming_expr -> - ?principal:bool -> ?hypnaming:naming_mode -> types -> constr -[@@ocaml.deprecated "Use [Evarutil.new_evar]"] - -val e_new_type_evar : env -> evar_map ref -> - ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:intro_pattern_naming_expr -> - ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t -[@@ocaml.deprecated "Use [Evarutil.new_type_evar]"] - -val e_new_Type : ?rigid:rigid -> evar_map ref -> constr -[@@ocaml.deprecated "Use [Evarutil.new_Type]"] - -val e_new_global : evar_map ref -> GlobRef.t -> constr -[@@ocaml.deprecated "Use [Evarutil.new_global]"] - -val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * UnivSubst.universe_opt_subst -[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] diff --git a/engine/termops.mli b/engine/termops.mli index 0e5d564d3f..64e3977d68 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -335,16 +335,4 @@ val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t val print_rel_context : env -> Pp.t val print_env : env -> Pp.t -val print_constr : constr -> Pp.t -[@@deprecated "use print_constr_env"] - end - -val print_constr : constr -> Pp.t -[@@deprecated "This is an internal, debug printer. WARNING, it is *extremely* likely that you want to use [Printer.pr_econstr_env] instead"] - -val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t -[@@deprecated "This is an internal, debug printer. WARNING, it is *extremely* likely that you want to use [Printer.pr_econstr_env] instead"] - -val print_rel_context : env -> Pp.t -[@@deprecated "This is an internal, debug printer. WARNING, this function is not suitable for plugin code, if you still want to use it then call [Internal.print_rel_context] instead"] diff --git a/engine/universes.ml b/engine/universes.ml deleted file mode 100644 index 5d0157b2db..0000000000 --- a/engine/universes.ml +++ /dev/null @@ -1,92 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Univ - -(** Deprecated *) - -(** UnivNames *) -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.qualid_of_level - -let empty_binders = UnivNames.empty_binders - -let register_universe_binders = UnivNames.register_universe_binders - -let universe_binders_with_opt_names = UnivNames.universe_binders_with_opt_names - -(** UnivGen *) -type universe_id = UnivGen.universe_id - -let set_remote_new_univ_id = UnivGen.set_remote_new_univ_id -let new_univ_id = UnivGen.new_univ_id -let new_univ_level = UnivGen.new_univ_level -let new_univ = UnivGen.new_univ -let new_Type = UnivGen.new_Type -let new_Type_sort = UnivGen.new_Type_sort -let new_global_univ = UnivGen.new_global_univ -let new_sort_in_family = UnivGen.new_sort_in_family -let fresh_instance_from_context = UnivGen.fresh_instance_from_context -let fresh_instance_from = UnivGen.fresh_instance_from -let fresh_sort_in_family = UnivGen.fresh_sort_in_family -let fresh_constant_instance = UnivGen.fresh_constant_instance -let fresh_inductive_instance = UnivGen.fresh_inductive_instance -let fresh_constructor_instance = UnivGen.fresh_constructor_instance -let fresh_global_instance = UnivGen.fresh_global_instance -let fresh_global_or_constr_instance = UnivGen.fresh_global_or_constr_instance -let fresh_universe_context_set_instance = UnivGen.fresh_universe_context_set_instance -let global_of_constr = UnivGen.global_of_constr -let constr_of_global_univ = UnivGen.constr_of_global_univ -let extend_context = UnivGen.extend_context -let constr_of_global = UnivGen.constr_of_global -let constr_of_reference = UnivGen.constr_of_global -let type_of_global = UnivGen.type_of_global - -(** UnivSubst *) - -let level_subst_of = UnivSubst.level_subst_of -let subst_univs_constraints = UnivSubst.subst_univs_constraints -let subst_univs_constr = UnivSubst.subst_univs_constr -type universe_opt_subst = UnivSubst.universe_opt_subst -let make_opt_subst = UnivSubst.make_opt_subst -let subst_opt_univs_constr = UnivSubst.subst_opt_univs_constr -let normalize_univ_variables = UnivSubst.normalize_univ_variables -let normalize_univ_variable = UnivSubst.normalize_univ_variable -let normalize_univ_variable_opt_subst = UnivSubst.normalize_univ_variable_opt_subst -let normalize_univ_variable_subst = UnivSubst.normalize_univ_variable_subst -let normalize_universe_opt_subst = UnivSubst.normalize_universe_opt_subst -let normalize_universe_subst = UnivSubst.normalize_universe_subst -let nf_evars_and_universes_opt_subst = UnivSubst.nf_evars_and_universes_opt_subst -let pr_universe_opt_subst = UnivSubst.pr_universe_opt_subst - -(** UnivProblem *) - -type universe_constraint = UnivProblem.t = - | 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 = UnivProblem.Set -type 'a constraint_accumulator = 'a UnivProblem.accumulator -type 'a universe_constrained = 'a UnivProblem.constrained -type 'a universe_constraint_function = 'a UnivProblem.constraint_function -let subst_univs_universe_constraints = UnivProblem.Set.subst_univs -let enforce_eq_instances_univs = UnivProblem.enforce_eq_instances_univs -let to_constraints = UnivProblem.to_constraints -let eq_constr_univs_infer_with = UnivProblem.eq_constr_univs_infer_with - -(** UnivMinim *) -module UPairSet = UnivMinim.UPairSet - -let normalize_context_set = UnivMinim.normalize_context_set diff --git a/engine/universes.mli b/engine/universes.mli deleted file mode 100644 index 0d3bae4c95..0000000000 --- a/engine/universes.mli +++ /dev/null @@ -1,230 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Constr -open Environ -open Univ - -(** ************************************** *) -(** This entire module is deprecated. **** *) -(** ************************************** *) -[@@@ocaml.warning "-3"] - -(** ****** 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.qualid -[@@ocaml.deprecated "Use [UnivNames.qualid_of_level]"] - -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]"] - -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_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 : 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]"] - -(** ****** 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 * 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]"] - -(** ****** 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]"] |