diff options
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 45 |
1 files changed, 29 insertions, 16 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 896bf26c..c915d4b0 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evarutil.mli 9573 2007-01-31 20:18:18Z notin $ i*) +(*i $Id: evarutil.mli 11136 2008-06-18 10:41:34Z herbelin $ i*) (*i*) open Util @@ -34,10 +34,10 @@ val new_untyped_evar : unit -> existential_key (***********************************************************) (* Creating a fresh evar given their type and context *) val new_evar : - evar_defs -> env -> ?src:loc * hole_kind -> types -> evar_defs * constr + evar_defs -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> evar_defs * constr (* the same with side-effects *) val e_new_evar : - evar_defs ref -> env -> ?src:loc * hole_kind -> types -> constr + evar_defs ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> 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 @@ -46,16 +46,18 @@ val e_new_evar : 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_defs -> types -> ?src:loc * hole_kind -> - constr list -> evar_defs * constr + named_context_val -> evar_defs -> types -> ?src:loc * hole_kind -> ?filter:bool list -> constr list -> evar_defs * constr -(***********************************************************) -(* Instanciate evars *) +val make_pure_subst : evar_info -> constr array -> (identifier * constr) list -(* suspicious env ? *) -val evar_define : - env -> existential -> constr -> evar_defs -> evar_defs * evar list +(***********************************************************) +(* Instantiate evars *) +(* [evar_define 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; + failed if the instance is not valid for the given [ev] *) +val evar_define : env -> existential -> constr -> evar_defs -> evar_defs (***********************************************************) (* Evars/Metas switching... *) @@ -71,8 +73,10 @@ val non_instantiated : evar_map -> (evar * evar_info) list (* Unification utils *) val is_ground_term : evar_defs -> constr -> bool -val is_eliminator : constr -> bool -val head_is_embedded_evar : evar_defs -> constr -> bool +val solve_refl : + (env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool) + -> env -> evar_defs -> existential_key -> constr array -> constr array -> + evar_defs val solve_simple_eqn : (env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool) -> env -> evar_defs -> conv_pb * existential * constr -> @@ -82,12 +86,12 @@ val solve_simple_eqn : new unresolved evar remains in [c] *) val check_evars : env -> evar_map -> evar_defs -> constr -> unit -val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types +val define_evar_as_product : evar_defs -> existential -> evar_defs * types val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts -val is_unification_pattern_evar : existential -> constr list -> bool -val is_unification_pattern : constr -> constr array -> bool +val is_unification_pattern_evar : env -> existential -> constr list -> bool +val is_unification_pattern : env -> constr -> constr array -> bool val solve_pattern_eqn : env -> constr list -> constr -> constr (***********************************************************) @@ -136,6 +140,10 @@ val tj_nf_evar : 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 + (* Same for evar defs *) val nf_isevar : evar_defs -> constr -> constr val j_nf_isevar : evar_defs -> unsafe_judgment -> unsafe_judgment @@ -153,6 +161,10 @@ exception Uninstantiated_evar of existential_key val whd_ise : evar_map -> constr -> constr val whd_castappevar : 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 *) +val expand_vars_in_term : env -> constr -> constr + (*********************************************************************) (* debug pretty-printer: *) @@ -162,4 +174,5 @@ val pr_tycon : env -> type_constraint -> Pp.std_ppcmds (**********************************) (* Removing hyps in evars'context *) -val clear_hyps_in_evi : evar_defs ref -> evar_info -> identifier list -> evar_info +val clear_hyps_in_evi : evar_defs ref -> named_context_val -> types -> + identifier list -> named_context_val * types |