diff options
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 163 |
1 files changed, 100 insertions, 63 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index e29effc2..61f503c7 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -1,117 +1,148 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evarutil.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Util open Names -open Rawterm +open Glob_term open Term open Sign open Evd open Environ open Reductionops -(*i*) -(*s This modules provides useful functions for unification modulo evars *) +(** {5 This modules provides useful functions for unification modulo evars } *) -(***********************************************************) -(* Metas *) +(** {6 Metas} *) -(* [new_meta] is a generator of unique meta variables *) +(** [new_meta] is a generator of unique meta variables *) val new_meta : unit -> metavariable val mk_new_meta : unit -> constr -(* [new_untyped_evar] is a generator of unique evar keys *) +(** [new_untyped_evar] is a generator of unique evar keys *) val new_untyped_evar : unit -> existential_key -(***********************************************************) -(* Creating a fresh evar given their type and context *) +(** {6 Creating a fresh evar given their type and context} *) val new_evar : - evar_map -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> evar_map * constr -(* the same with side-effects *) + evar_map -> env -> ?src:loc * hole_kind -> ?filter:bool list -> + ?candidates:constr list -> types -> evar_map * constr + +(** the same with side-effects *) val e_new_evar : - evar_map ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> constr + evar_map ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> + ?candidates:constr list -> types -> constr -(* Create a fresh evar in a context different from its definition context: +(** Create a new Type existential variable, as we keep track of + them during type-checking and unification. *) +val new_type_evar : + ?src:loc * hole_kind -> ?filter:bool list -> evar_map -> env -> evar_map * constr + +(** Create a fresh evar in a context different from its definition context: [new_evar_instance sign evd ty inst] creates a new evar of context [sign] and type [ty], [inst] is a mapping of the evar context to the context where the evar should occur. This means that the terms of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - named_context_val -> evar_map -> types -> ?src:loc * hole_kind -> ?filter:bool list -> constr list -> evar_map * constr + named_context_val -> evar_map -> types -> ?src:loc * hole_kind -> ?filter:bool list -> ?candidates:constr list -> constr list -> evar_map * constr val make_pure_subst : evar_info -> constr array -> (identifier * constr) list -(***********************************************************) -(* Instantiate evars *) +(** {6 Instantiate evars} *) + +type conv_fun = + env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool -(* [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]), +(** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]), possibly solving related unification problems, possibly leaving open some problems that cannot be solved in a unique way (except if choose is true); fails if the instance is not valid for the given [ev] *) -val evar_define : ?choose:bool -> env -> existential -> constr -> evar_map -> evar_map +val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> + existential -> constr -> evar_map -(***********************************************************) -(* Evars/Metas switching... *) +(** {6 Evars/Metas switching...} *) -(* [evars_to_metas] generates new metavariables for each non dependent +(** [evars_to_metas] generates new metavariables for each non dependent existential and performs the replacement in the given constr; it also returns the evar_map extended with dependent evars *) val evars_to_metas : evar_map -> open_constr -> (evar_map * constr) val non_instantiated : evar_map -> (evar * evar_info) list -(***********************************************************) -(* Unification utils *) +(** {6 Unification utils} *) +(** [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 : constr -> existential_key (** may raise NoHeadEvar *) (* Expand head evar if any *) val whd_head_evar : evar_map -> constr -> constr val is_ground_term : evar_map -> constr -> bool val is_ground_env : evar_map -> env -> bool -val solve_refl : - (env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool) - -> env -> evar_map -> existential_key -> constr array -> constr array -> - evar_map -val solve_simple_eqn : - (env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool) - -> ?choose:bool -> env -> evar_map -> bool option * existential * constr -> - evar_map * bool - -(* [check_evars env initial_sigma extended_sigma c] fails if some +val solve_refl : conv_fun -> env -> evar_map -> + existential_key -> constr array -> constr array -> evar_map +val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map -> + bool option * existential * constr -> evar_map * bool +val reconsider_conv_pbs : conv_fun -> evar_map -> evar_map * bool + +(** [check_evars env initial_sigma extended_sigma c] fails if some new unresolved evar remains in [c] *) val check_evars : env -> evar_map -> evar_map -> constr -> unit -val subtract_evars : evar_map -> evar_map -> evar_map * evar_map val define_evar_as_product : evar_map -> existential -> evar_map * types -val define_evar_as_lambda : evar_map -> existential -> evar_map * types +val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types val define_evar_as_sort : evar_map -> existential -> evar_map * sorts -val is_unification_pattern_evar : env -> existential -> constr list -> - constr -> bool -val is_unification_pattern : env * int -> constr -> constr array -> - constr -> bool +val is_unification_pattern_evar : env -> evar_map -> existential -> constr list -> + constr -> constr list option + +val is_unification_pattern : env * int -> evar_map -> constr -> constr list -> + constr -> constr list option + +val evar_absorb_arguments : env -> evar_map -> existential -> constr list -> + evar_map * existential + val solve_pattern_eqn : env -> constr list -> constr -> constr +(** The following functions return the set of evars immediately + contained in the object, including defined evars *) + + val evars_of_term : constr -> Intset.t + +(** returns the evars contained in the term associated with + the evars they contain themselves in their body, if any. + If the evar has no body, [None] is associated to it. *) +val evars_of_evars_of_term : evar_map -> constr -> (Intset.t option) Intmap.t val evars_of_named_context : named_context -> Intset.t val evars_of_evar_info : evar_info -> Intset.t -(***********************************************************) -(* Value/Type constraints *) +(** returns the evars which can be found in the typing context of the argument evars, + in the same format as {!evars_of_evars_of_term}. + It explores recursively the evars in the body of the argument evars -- but does + not return them. *) +(* spiwack: tongue in cheek: it should have been called + [evars_of_evars_in_types_of_list_and_recursively_in_bodies] *) +val evars_of_evars_in_types_of_list : evar_map -> evar list -> (Intset.t option) Intmap.t + + +(** The following functions return the set of undefined evars + contained in the object, the defined evars being traversed. + This is roughly a combination of the previous functions and + [nf_evar]. *) + +val undefined_evars_of_term : evar_map -> constr -> Intset.t +val undefined_evars_of_named_context : evar_map -> named_context -> Intset.t +val undefined_evars_of_evar_info : evar_map -> evar_info -> Intset.t + +(** {6 Value/Type constraints} *) -val judge_of_new_Type : unit -> unsafe_judgment +val judge_of_new_Type : evar_map -> evar_map * unsafe_judgment type type_constraint_type = (int * int) option * constr type type_constraint = type_constraint_type option @@ -139,8 +170,8 @@ val lift_tycon : int -> type_constraint -> type_constraint (***********************************************************) -(* [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains *) -(* uninstantiated; [nf_evar] leave uninstantiated evars as is *) +(** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains + uninstantiated; [nf_evar] leaves uninstantiated evars as is *) val nf_evar : evar_map -> constr -> constr val j_nf_evar : evar_map -> unsafe_judgment -> unsafe_judgment @@ -151,34 +182,30 @@ val jv_nf_evar : val tj_nf_evar : evar_map -> unsafe_type_judgment -> unsafe_type_judgment -val nf_evar_info : evar_map -> evar_info -> evar_info -val nf_evars : evar_map -> evar_map - val nf_named_context_evar : evar_map -> named_context -> named_context 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 val nf_evar_map : evar_map -> evar_map +val nf_evar_map_undefined : evar_map -> evar_map -(* Replacing all evars, possibly raising [Uninstantiated_evar] *) -(* exception Uninstantiated_evar of existential_key *) +(** Replacing all evars, possibly raising [Uninstantiated_evar] *) exception Uninstantiated_evar of existential_key val flush_and_check_evars : evar_map -> constr -> constr -(* Replace the vars and rels that are aliases to other vars and rels by *) -(* their representative that is most ancient in the context *) +(** Replace the vars and rels that are aliases to other vars and rels by + their representative that is most ancient in the context *) val expand_vars_in_term : env -> constr -> constr -(*********************************************************************) -(* debug pretty-printer: *) +(** {6 debug pretty-printer:} *) val pr_tycon_type : env -> type_constraint_type -> Pp.std_ppcmds val pr_tycon : env -> type_constraint -> Pp.std_ppcmds -(*********************************************************************) -(* Removing hyps in evars'context; *) -(* raise OccurHypInSimpleClause if the removal breaks dependencies *) +(** {6 Removing hyps in evars'context} +raise OccurHypInSimpleClause if the removal breaks dependencies *) type clear_dependency_error = | OccurHypInSimpleClause of identifier option @@ -186,8 +213,18 @@ type clear_dependency_error = exception ClearDependencyError of identifier * 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.t + val clear_hyps_in_evi : evar_map ref -> named_context_val -> types -> identifier list -> named_context_val * types -val push_rel_context_to_named_context : Environ.env -> types -> - named_context_val * types * constr list +val push_rel_context_to_named_context : Environ.env -> types -> + named_context_val * types * constr list * constr list + +val generalize_evar_over_rels : evar_map -> existential -> types * constr list + +val check_evar_instance : evar_map -> existential_key -> constr -> conv_fun -> + evar_map + |