From bf12eb93f3f6a6a824a10878878fadd59745aae0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 29 Dec 2012 10:57:43 +0100 Subject: Imported Upstream version 8.4pl1dfsg --- pretyping/unification.ml | 56 ++++++++++++++++++------------------------------ 1 file changed, 21 insertions(+), 35 deletions(-) (limited to 'pretyping/unification.ml') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index c92c183d..63cdb378 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -198,11 +198,18 @@ type unify_flags = { (* (and activated for apply, rewrite but not auto since Feb 2008 for 8.2) *) modulo_delta : Names.transparent_state; - (* This controls which constant are unfoldable; this is on for apply *) + (* This controls which constants are unfoldable; this is on for apply *) (* (but not simple apply) since Feb 2008 for 8.2 *) modulo_delta_types : Names.transparent_state; + modulo_delta_in_merge : Names.transparent_state option; + (* This controls whether unfoldability is different when trying to unify *) + (* several instances of the same metavariable *) + (* Typical situation is when we give a pattern to be matched *) + (* syntactically against a subterm but we want the metas of the *) + (* pattern to be modulo convertibility *) + check_applied_meta_types : bool; (* This controls whether meta's applied to arguments have their *) (* type unified with the type of their instance *) @@ -240,12 +247,13 @@ type unify_flags = { } (* Default flag for unifying a type against a type (e.g. apply) *) -(* We set all conversion flags *) +(* We set all conversion flags (no flag should be modified anymore) *) let default_unify_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = full_transparent_state; modulo_delta_types = full_transparent_state; + modulo_delta_in_merge = None; check_applied_meta_types = true; resolve_evars = false; use_pattern_unification = true; @@ -258,24 +266,22 @@ let default_unify_flags = { (* in fact useless when not used in w_unify_to_subterm_list *) } +let set_merge_flags flags = + match flags.modulo_delta_in_merge with + | None -> flags + | Some ts -> + { flags with modulo_delta = ts; modulo_conv_on_closed_terms = Some ts } + (* Default flag for the "simple apply" version of unification of a *) (* type against a type (e.g. apply) *) (* We set only the flags available at the time the new "apply" extends *) (* out of "simple apply" *) -let default_no_delta_unify_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly_in_conv_on_closed_terms = true; +let default_no_delta_unify_flags = { default_unify_flags with modulo_delta = empty_transparent_state; - modulo_delta_types = full_transparent_state; check_applied_meta_types = false; - resolve_evars = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; - frozen_evars = ExistentialSet.empty; - restrict_conv_on_strict_subterms = false; modulo_betaiota = false; - modulo_eta = true; - allow_K_in_toplevel_higher_order_unification = false } (* Default flags for looking for subterms in elimination tactics *) @@ -283,36 +289,16 @@ let default_no_delta_unify_flags = { (* allow_K) because only closed terms are involved in *) (* induction/destruct/case/elim and w_unify_to_subterm_list does not *) (* call w_unify for induction/destruct/case/elim (13/6/2011) *) -let elim_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly_in_conv_on_closed_terms = true; - modulo_delta = full_transparent_state; - modulo_delta_types = full_transparent_state; - check_applied_meta_types = true; - resolve_evars = false; - use_pattern_unification = true; - use_meta_bound_pattern_unification = true; - frozen_evars = ExistentialSet.empty; +let elim_flags = { default_unify_flags with restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; - modulo_eta = true; allow_K_in_toplevel_higher_order_unification = true } -let elim_no_delta_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly_in_conv_on_closed_terms = true; +let elim_no_delta_flags = { elim_flags with modulo_delta = empty_transparent_state; - modulo_delta_types = full_transparent_state; check_applied_meta_types = false; - resolve_evars = false; use_pattern_unification = false; - use_meta_bound_pattern_unification = true; - frozen_evars = ExistentialSet.empty; - restrict_conv_on_strict_subterms = false; (* ? *) - modulo_betaiota = false; - modulo_eta = true; - allow_K_in_toplevel_higher_order_unification = true } let set_no_head_reduction flags = @@ -865,7 +851,7 @@ let w_merge env with_types flags (evd,metas,evars) = if Evd.is_defined evd evk then let v = Evd.existential_value evd ev in let (evd,metas',evars'') = - unify_0 curenv evd CONV flags rhs v in + unify_0 curenv evd CONV (set_merge_flags flags) rhs v in w_merge_rec evd (metas'@metas) (evars''@evars') eqns else begin (* This can make rhs' ill-typed if metas are *) @@ -943,7 +929,7 @@ let w_merge env with_types flags (evd,metas,evars) = let sp_env = Global.env_of_context ev.evar_hyps in let (evd', c) = applyHead sp_env evd nargs hdc in let (evd'',mc,ec) = - unify_0 sp_env evd' CUMUL flags + unify_0 sp_env evd' CUMUL (set_merge_flags flags) (get_type_of sp_env evd' c) ev.evar_concl in let evd''' = w_merge_rec evd'' mc ec [] in if evd' == evd''' -- cgit v1.2.3