From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- proofs/clenv.mli | 142 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 142 insertions(+) create mode 100644 proofs/clenv.mli (limited to 'proofs/clenv.mli') diff --git a/proofs/clenv.mli b/proofs/clenv.mli new file mode 100644 index 00000000..10e0004e --- /dev/null +++ b/proofs/clenv.mli @@ -0,0 +1,142 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* metavariable + +(* [exist_to_meta] generates new metavariables for each existential + and performs the replacement in the given constr *) +val exist_to_meta : + Evd.evar_map -> Pretyping.open_constr -> (Termops.metamap * constr) + +(* The Type of Constructions clausale environments. *) + +module Metaset : Set.S with type elt = metavariable + +module Metamap : Map.S with type key = metavariable + +type 'a freelisted = { + rebus : 'a; + freemetas : Metaset.t } + +type clbinding = + | Cltyp of constr freelisted + | Clval of constr freelisted * constr freelisted + +type 'a clausenv = { + templval : constr freelisted; + templtyp : constr freelisted; + namenv : identifier Metamap.t; + env : clbinding Metamap.t; + hook : 'a } + +type wc = named_context sigma (* for a better reading of the following *) + +(* [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 instanciating metavars by name. + * [env] is the mapping from metavar numbers to their types + * and values. + * [hook] is the pointer to the current walking context, for + * integrating existential vars and metavars. *) + +val collect_metas : constr -> metavariable list +val mk_clenv : 'a -> constr -> 'a clausenv +val mk_clenv_from : 'a -> constr * constr -> 'a clausenv +val mk_clenv_from_n : 'a -> int option -> constr * constr -> 'a clausenv +val mk_clenv_rename_from : wc -> constr * constr -> wc clausenv +val mk_clenv_rename_from_n : wc -> int option -> constr * constr -> wc clausenv +val mk_clenv_hnf_constr_type_of : wc -> constr -> wc clausenv +val mk_clenv_type_of : wc -> constr -> wc clausenv + +val subst_clenv : (substitution -> 'a -> 'a) -> + substitution -> 'a clausenv -> 'a clausenv + +val connect_clenv : wc -> 'a clausenv -> wc clausenv +(*i Was used in wcclausenv.ml +val clenv_change_head : constr * constr -> 'a clausenv -> 'a clausenv +i*) +val clenv_assign : metavariable -> constr -> 'a clausenv -> 'a clausenv +val clenv_instance_term : wc clausenv -> constr -> constr +val clenv_pose : name * metavariable * constr -> 'a clausenv -> 'a clausenv +val clenv_template : 'a clausenv -> constr freelisted +val clenv_template_type : 'a clausenv -> constr freelisted +val clenv_instance_type : wc clausenv -> metavariable -> constr +val clenv_instance_template : wc clausenv -> constr +val clenv_instance_template_type : wc clausenv -> constr +val clenv_type_of : wc clausenv -> constr -> constr +val clenv_fchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv +val clenv_bchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv + +(* Unification with clenv *) +type arg_bindings = (int * constr) list + +val unify_0 : + Reductionops.conv_pb -> wc -> constr -> constr + -> Termops.metamap * (constr * constr) list +val clenv_unify : + bool -> Reductionops.conv_pb -> constr -> constr -> + wc clausenv -> wc clausenv +val clenv_match_args : + constr Rawterm.explicit_bindings -> wc clausenv -> wc clausenv +val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv + +(* Bindings *) +val clenv_independent : wc clausenv -> metavariable list +val clenv_missing : 'a clausenv -> metavariable list +val clenv_constrain_missing_args : (* Used in user contrib Lannion *) + constr list -> wc clausenv -> wc clausenv +(* +val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv +*) +val clenv_lookup_name : 'a clausenv -> identifier -> metavariable +val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv + +val make_clenv_binding_apply : + wc -> int -> constr * constr -> types Rawterm.bindings -> wc clausenv +val make_clenv_binding : + wc -> constr * constr -> types Rawterm.bindings -> wc clausenv + +(* Tactics *) +val unify : constr -> tactic +val clenv_refine : (wc -> tactic) -> wc clausenv -> tactic +val res_pf : (wc -> tactic) -> wc clausenv -> tactic +val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic +val elim_res_pf : (wc -> tactic) -> wc clausenv -> bool -> tactic +val e_res_pf : (wc -> tactic) -> wc clausenv -> tactic +val elim_res_pf_THEN_i : + (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic array) -> tactic + +(* Pretty-print *) +val pr_clenv : 'a clausenv -> Pp.std_ppcmds + +(* Exported for debugging *) +val unify_to_subterm : + wc clausenv -> constr * constr -> wc clausenv * constr +val unify_to_subterm_list : + bool -> wc clausenv -> constr list -> constr -> wc clausenv * constr list +val clenv_typed_unify : + Reductionops.conv_pb -> constr -> constr -> wc clausenv -> wc clausenv + +(*i This should be in another module i*) + +(* [abstract_list_all env sigma t c l] *) +(* abstracts the terms in l over c to get a term of type t *) +val abstract_list_all : + Environ.env -> Evd.evar_map -> constr -> constr -> constr list -> constr -- cgit v1.2.3