diff options
Diffstat (limited to 'engine/evarutil.mli')
| -rw-r--r-- | engine/evarutil.mli | 133 |
1 files changed, 80 insertions, 53 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 7fdc7aac..e289ca16 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -1,15 +1,18 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 Term +open Constr open Evd open Environ +open EConstr (** This module provides useful higher-level functions for evar manipulation. *) @@ -20,23 +23,30 @@ val new_meta : unit -> metavariable val mk_new_meta : unit -> constr (** {6 Creating a fresh evar given their type and context} *) + +val new_evar_from_context : + named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?candidates:constr list -> ?store:Store.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> types -> evar_map * EConstr.t + val new_evar : - env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> (constr, 'r) Sigma.sigma + ?principal:bool -> types -> evar_map * EConstr.t val new_pure_evar : - named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> (evar, 'r) Sigma.sigma + ?principal:bool -> types -> evar_map * Evar.t -val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma +val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t (** the same with side-effects *) val e_new_evar : - env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> types -> constr @@ -44,23 +54,23 @@ val e_new_evar : (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : - env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> - (constr * sorts, 'r) Sigma.sigma + evar_map * (constr * Sorts.t) val e_new_type_evar : env -> evar_map ref -> - ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * Sorts.t -val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma +val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr -val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t -> - constr list option -> (existential_key, 'r) Sigma.sigma +val restrict_evar : evar_map -> Evar.t -> Filter.t -> + ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t (** Polymorphic constants *) -val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma +val new_global : evar_map -> Globnames.global_reference -> evar_map * constr val e_new_global : evar_map ref -> Globnames.global_reference -> constr (** Create a fresh evar in a context different from its definition context: @@ -70,15 +80,15 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - named_context_val -> 'r Sigma.t -> types -> - ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> + named_context_val -> evar_map -> types -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> - constr list -> (constr, 'r) Sigma.sigma + constr list -> evar_map * constr -val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list +val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list -val safe_evar_value : evar_map -> existential -> constr option +val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option (** {6 Evars/Metas switching...} *) @@ -88,7 +98,7 @@ val non_instantiated : evar_map -> evar_info Evar.Map.t (** [head_evar c] returns the head evar of [c] if any *) exception NoHeadEvar -val head_evar : constr -> existential_key (** may raise NoHeadEvar *) +val head_evar : evar_map -> constr -> Evar.t (** may raise NoHeadEvar *) (* Expand head evar if any *) val whd_head_evar : evar_map -> constr -> constr @@ -108,13 +118,13 @@ val is_ground_env : evar_map -> env -> bool associating to each dependent evar [None] if it has no (partial) definition or [Some s] if [s] is the list of evars appearing in its (partial) definition. *) -val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.Map.t +val gather_dependent_evars : evar_map -> Evar.t list -> (Evar.Set.t option) Evar.Map.t (** [advance sigma g] returns [Some g'] if [g'] is undefined and is the current avatar of [g] (for instance [g] was changed by [clear] into [g']). It returns [None] if [g] has been (partially) solved. *) -val advance : evar_map -> evar -> evar option +val advance : evar_map -> Evar.t -> Evar.t option (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. @@ -125,14 +135,20 @@ val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t +type undefined_evars_cache + +val create_undefined_evars_cache : unit -> undefined_evars_cache + +val filtered_undefined_evars_of_evar_info : ?cache:undefined_evars_cache -> evar_map -> evar_info -> Evar.Set.t + (** [occur_evar_upto sigma k c] returns [true] if [k] appears in [c]. It looks up recursively in [sigma] for the value of existential variables. *) -val occur_evar_upto : evar_map -> Evar.t -> Constr.t -> bool +val occur_evar_upto : evar_map -> Evar.t -> constr -> bool (** {6 Value/Type constraints} *) -val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma +val judge_of_new_Type : evar_map -> evar_map * unsafe_judgment (***********************************************************) @@ -150,7 +166,7 @@ val tj_nf_evar : evar_map -> unsafe_type_judgment -> unsafe_type_judgment val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t -val nf_rel_context_evar : evar_map -> Context.Rel.t -> Context.Rel.t +val nf_rel_context_evar : evar_map -> rel_context -> rel_context val nf_env_evar : evar_map -> env -> env val nf_evar_info : evar_map -> evar_info -> evar_info @@ -159,46 +175,57 @@ val nf_evar_map_undefined : evar_map -> evar_map (** Presenting terms without solved evars *) -val nf_evars_universes : evar_map -> constr -> constr +val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr -val nf_evars_and_universes : evar_map -> evar_map * (constr -> constr) -val e_nf_evars_and_universes : evar_map ref -> (constr -> constr) * Universes.universe_opt_subst +val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) +val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst (** 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) +val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) (** Replacing all evars, possibly raising [Uninstantiated_evar] *) -exception Uninstantiated_evar of existential_key -val flush_and_check_evars : evar_map -> constr -> constr +exception Uninstantiated_evar of Evar.t +val flush_and_check_evars : evar_map -> constr -> Constr.constr (** {6 Term manipulation up to instantiation} *) (** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t] as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the value of [e] in [sigma] is (recursively) used. *) -val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term +val kind_of_term_upto : evar_map -> Constr.constr -> + (Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) kind_of_term (** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and [u] up to existential variable instantiation and equalisable universes. The term [t] is interpreted in [sigma1] while [u] is interpreted in [sigma2]. The universe constraints in [sigma2] are assumed to be an extention of those in [sigma1]. *) -val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool +val eq_constr_univs_test : evar_map -> evar_map -> Constr.constr -> Constr.constr -> bool + +(** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns + [Inl sigma'] where [sigma'] is [sigma] augmented with universe + constraints such that [u1 cv_pb? u2] according to [variance]. + Additionally flexible universes in irrelevant positions are unified + if possible. Returns [Inr p] when the former is impossible. *) +val compare_cumulative_instances : Reduction.conv_pb -> Univ.Variance.t array -> + Univ.Instance.t -> Univ.Instance.t -> evar_map -> + (evar_map, Univ.univ_inconsistency) Util.union + +(** We should only compare constructors at convertible types, so this + is only an opportunity to unify universes. *) +val compare_constructor_instances : evar_map -> + Univ.Instance.t -> Univ.Instance.t -> evar_map (** {6 Removing hyps in evars'context} raise OccurHypInSimpleClause if the removal breaks dependencies *) type clear_dependency_error = | OccurHypInSimpleClause of Id.t option -| EvarTypingBreak of existential +| EvarTypingBreak of Constr.existential exception ClearDependencyError of Id.t * clear_dependency_error -(* spiwack: marks an evar that has been "defined" by clear. - used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*) -val cleared : bool Store.field - val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> Id.Set.t -> named_context_val * types @@ -208,17 +235,16 @@ val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> ty type csubst val empty_csubst : csubst -val csubst_subst : csubst -> Constr.t -> Constr.t +val csubst_subst : csubst -> constr -> constr type ext_named_context = - csubst * (Id.t * Constr.constr) list * - Id.Set.t * Context.Named.t + csubst * Id.Set.t * named_context val push_rel_decl_to_named_context : - Context.Rel.Declaration.t -> ext_named_context -> ext_named_context + evar_map -> rel_declaration -> ext_named_context -> ext_named_context -val push_rel_context_to_named_context : Environ.env -> types -> - named_context_val * types * constr list * csubst * (identifier*constr) list +val push_rel_context_to_named_context : Environ.env -> evar_map -> types -> + named_context_val * types * constr list * csubst val generalize_evar_over_rels : evar_map -> existential -> types * constr list @@ -228,12 +254,13 @@ val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a -val subterm_source : existential_key -> Evar_kinds.t Loc.located -> +val subterm_source : Evar.t -> Evar_kinds.t Loc.located -> Evar_kinds.t Loc.located -val meta_counter_summary_name : string - -(** Deprecater *) +val meta_counter_summary_tag : int Summary.Dyn.tag +(** Deprecated *) type type_constraint = types option +[@@ocaml.deprecated "use the version in Evardefine"] type val_constraint = constr option +[@@ocaml.deprecated "use the version in Evardefine"] |