diff options
Diffstat (limited to 'pretyping/clenv.mli')
-rw-r--r-- | pretyping/clenv.mli | 117 |
1 files changed, 117 insertions, 0 deletions
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli new file mode 100644 index 00000000..f585dfea --- /dev/null +++ b/pretyping/clenv.mli @@ -0,0 +1,117 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: clenv.mli 7659 2005-12-17 21:07:17Z herbelin $ i*) + +(*i*) +open Util +open Names +open Term +open Sign +open Environ +open Evd +open Evarutil +open Mod_subst +(*i*) + +(***************************************************************) +(* The Type of Constructions clausale environments. *) + +(* [templenv] is the typing context + * [env] is the mapping from metavar and evar numbers to their types + * and values. + * [templval] is the template which we are trying to fill out. + * [templtyp] is its type. + * [namenv] is a mapping from metavar numbers to names, for + * use in instantiating metavars by name. + *) +type clausenv = { + templenv : env; + env : evar_defs; + templval : constr freelisted; + templtyp : constr freelisted } + +(* 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 : evar_info sigma -> constr * types -> clausenv +val mk_clenv_from_n : + evar_info sigma -> int option -> constr * types -> clausenv +val mk_clenv_rename_from : evar_info sigma -> constr * types -> clausenv +val mk_clenv_rename_from_n : + evar_info sigma -> int option -> constr * types -> clausenv +val mk_clenv_type_of : evar_info sigma -> constr -> clausenv + +(***************************************************************) +(* linking of clenvs *) + +val connect_clenv : evar_info sigma -> clausenv -> clausenv +val clenv_fchain : metavariable -> clausenv -> clausenv -> clausenv + +(***************************************************************) +(* Unification with clenvs *) + +(* Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *) +val clenv_unify : + bool -> conv_pb -> constr -> constr -> clausenv -> clausenv + +(* unifies the concl of the goal with the type of the clenv *) +val clenv_unique_resolver : + bool -> clausenv -> evar_info sigma -> clausenv + +(* same as above ([allow_K=false]) but replaces remaining metas + with fresh evars *) +val evar_clenv_unique_resolver : + clausenv -> evar_info sigma -> clausenv + +(***************************************************************) +(* 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. *) +type arg_bindings = (int * constr) list + +val clenv_independent : clausenv -> metavariable list +val clenv_missing : clausenv -> metavariable list + +(* defines metas corresponding to the name of the bindings *) +val clenv_match_args : + constr Rawterm.explicit_bindings -> clausenv -> clausenv +val clenv_constrain_with_bindings : arg_bindings -> clausenv -> clausenv + +(* start with a clenv to refine with a given term with bindings *) + +(* 1- the arity of the lemma is fixed *) +val make_clenv_binding_apply : + evar_info sigma -> int -> constr * constr -> constr Rawterm.bindings -> + clausenv +val make_clenv_binding : + evar_info sigma -> constr * constr -> constr Rawterm.bindings -> clausenv + +(* other stuff *) +val clenv_environments : + evar_defs -> int option -> types -> evar_defs * constr list * types +val clenv_environments_evars : + env -> evar_defs -> int option -> types -> evar_defs * constr list * types + +(***************************************************************) +(* Pretty-print *) +val pr_clenv : clausenv -> Pp.std_ppcmds + |