diff options
Diffstat (limited to 'proofs/clenv.mli')
-rw-r--r-- | proofs/clenv.mli | 139 |
1 files changed, 139 insertions, 0 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli new file mode 100644 index 00000000..7722544a --- /dev/null +++ b/proofs/clenv.mli @@ -0,0 +1,139 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Names +open Term +open Sign +open Environ +open Evd +open Evarutil +open Mod_subst +open Glob_term +open Unification + +(** {6 The Type of Constructions clausale environments.} *) + +type clausenv = { + env : env; (** the typing context *) + evd : evar_map; (** the mapping from metavar and evar numbers to their + types and values *) + templval : constr freelisted; (** the template which we are trying to fill + out *) + templtyp : constr freelisted (** its type *)} + +(** Substitution is not applied on templenv (because [subst_clenv] is + applied only on hints which typing env is overwritten by the + goal env) *) +val subst_clenv : substitution -> clausenv -> clausenv + +(** subject of clenv (instantiated) *) +val clenv_value : clausenv -> constr + +(** type of clenv (instantiated) *) +val clenv_type : clausenv -> types + +(** substitute resolved metas *) +val clenv_nf_meta : clausenv -> constr -> constr + +(** type of a meta in clenv context *) +val clenv_meta_type : clausenv -> metavariable -> types + +val mk_clenv_from : Goal.goal sigma -> constr * types -> clausenv +val mk_clenv_from_n : + Goal.goal sigma -> int option -> constr * types -> clausenv +val mk_clenv_type_of : Goal.goal sigma -> constr -> clausenv +val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv + +(** {6 linking of clenvs } *) + +val connect_clenv : Goal.goal sigma -> clausenv -> clausenv +val clenv_fchain : + ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv + +(** {6 Unification with clenvs } *) + +(** Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *) +val clenv_unify : + ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv + +(** unifies the concl of the goal with the type of the clenv *) +val clenv_unique_resolver : + ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv + +(** same as above ([allow_K=false]) but replaces remaining metas + with fresh evars if [evars_flag] is [true] *) +val evar_clenv_unique_resolver : + ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv + +val clenv_dependent : clausenv -> metavariable list + +val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv + +(** {6 Bindings } *) + +type arg_bindings = constr explicit_bindings + +(** bindings where the key is the position in the template of the + clenv (dependent or not). Positions can be negative meaning to + start from the rightmost argument of the template. *) +val clenv_independent : clausenv -> metavariable list +val clenv_missing : clausenv -> metavariable list + +(** for the purpose of inversion tactics *) +exception NoSuchBinding +val clenv_constrain_last_binding : constr -> clausenv -> clausenv + +(** defines metas corresponding to the name of the bindings *) +val clenv_match_args : arg_bindings -> clausenv -> clausenv + +val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv + +(** start with a clenv to refine with a given term with bindings *) + +(** the arity of the lemma is fixed + the optional int tells how many prods of the lemma have to be used + use all of them if None *) +val make_clenv_binding_env_apply : + env -> evar_map -> int option -> constr * constr -> constr bindings -> + clausenv + +val make_clenv_binding_apply : + Goal.goal sigma -> int option -> constr * constr -> constr bindings -> + clausenv +val make_clenv_binding : + Goal.goal sigma -> constr * constr -> constr bindings -> clausenv + +(** [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where + [lmetas] is a list of metas to be applied to a proof of [t] so that + it produces the unification pattern [ccl]; [sigma'] is [sigma] + extended with [lmetas]; if [n] is defined, it limits the size of + the list even if [ccl] is still a product; otherwise, it stops when + [ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x] + and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and + [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1] + and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *) +val clenv_environments : + evar_map -> int option -> types -> evar_map * constr list * types + +(** [clenv_environments_evars env sigma n t] does the same but returns + a list of Evar's defined in [env] and extends [sigma] accordingly *) +val clenv_environments_evars : + env -> evar_map -> int option -> types -> evar_map * constr list * types + +(** [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *) +val clenv_conv_leq : + env -> evar_map -> types -> constr -> int -> constr list + +(** if the clause is a product, add an extra meta for this product *) +exception NotExtensibleClause +val clenv_push_prod : clausenv -> clausenv + +(** {6 Pretty-print (debug only) } *) +val pr_clenv : clausenv -> Pp.std_ppcmds + |