diff options
| -rw-r--r-- | pretyping/unification.ml | 43 | ||||
| -rw-r--r-- | pretyping/unification.mli | 1 | ||||
| -rw-r--r-- | proofs/clenv.ml | 7 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 1 | ||||
| -rw-r--r-- | tactics/auto.ml | 1 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 1 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 3 |
8 files changed, 43 insertions, 16 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 0af0aae3a7..c233674aec 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -164,6 +164,7 @@ type unify_flags = { resolve_evars : bool; use_evars_pattern_unification : bool; frozen_evars : ExistentialSet.t; + restrict_conv_on_strict_subterms : bool; modulo_betaiota : bool; modulo_eta : bool; allow_K_in_toplevel_higher_order_unification : bool @@ -177,6 +178,7 @@ let default_unify_flags = { resolve_evars = false; use_evars_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 @@ -190,11 +192,17 @@ let default_no_delta_unify_flags = { resolve_evars = false; use_evars_pattern_unification = false; frozen_evars = ExistentialSet.empty; + restrict_conv_on_strict_subterms = false; modulo_betaiota = false; modulo_eta = true; allow_K_in_toplevel_higher_order_unification = false } +(* Note: at least up to 13/6/11, elim_flags and elim_no_delta_flags have no + effect (to the exception of 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 *) + let elim_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = true; @@ -203,6 +211,7 @@ let elim_flags = { resolve_evars = false; use_evars_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 @@ -216,6 +225,7 @@ let elim_no_delta_flags = { resolve_evars = false; use_evars_pattern_unification = false; frozen_evars = ExistentialSet.empty; + restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; modulo_eta = true; allow_K_in_toplevel_higher_order_unification = true @@ -231,7 +241,11 @@ let expand_key env = function | Some (RelKey _) -> None | None -> None -let key_of flags f = +let subterm_restriction is_subterm flags = + not is_subterm && flags.restrict_conv_on_strict_subterms + +let key_of b flags f = + if subterm_restriction b flags then None else match kind_of_term f with | Const cst when is_transparent (ConstKey cst) && Cpred.mem cst (snd flags.modulo_delta) -> @@ -378,14 +392,14 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag expand curenvnb pb b substn cM f1 l1 cN f2 l2 and reduce curenvnb pb b (sigma, metas, evars as substn) cM cN = - if flags.modulo_betaiota then + if flags.modulo_betaiota && not (subterm_restriction b flags) then let cM' = do_reduce (fst curenvnb) sigma cM in if not (eq_constr cM cM') then - unirec_rec curenvnb pb true substn cM' cN + unirec_rec curenvnb pb b substn cM' cN else let cN' = do_reduce (fst curenvnb) sigma cN in if not (eq_constr cN cN') then - unirec_rec curenvnb pb true substn cM cN' + unirec_rec curenvnb pb b substn cM cN' else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) @@ -407,7 +421,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag essentially for apply)... *) match flags.modulo_conv_on_closed_terms with | None -> false - | Some convflags -> + | Some convflags when not (subterm_restriction b flags) -> let subst = if flags.use_metas_eagerly then metasubst else ms in match subst_defined_metas subst cM with | None -> (* some undefined Metas in cM *) false @@ -415,6 +429,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag match subst_defined_metas subst cN with | None -> (* some undefined Metas in cN *) false | Some n1 -> + (* No subterm restriction there, too much incompatibilities *) if is_trans_fconv pb convflags env sigma m1 n1 then true else if is_ground_term sigma m1 && is_ground_term sigma n1 then @@ -423,9 +438,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag then substn else - if b then - (* Try delta-expansion if in subterms or if asked to conv at top *) - let cf1 = key_of flags f1 and cf2 = key_of flags f2 in + let cf1 = key_of b flags f1 and cf2 = key_of b flags f2 in match oracle_order curenv cf1 cf2 with | None -> error_cannot_unify curenv sigma (cM,cN) | Some true -> @@ -452,8 +465,6 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag (whd_betaiotazeta sigma (mkApp(c,l1))) cN | None -> error_cannot_unify curenv sigma (cM,cN))) - else - error_cannot_unify curenv sigma (cM,cN) and canonical_projections curenvnb pb b cM cN (sigma,_,_ as substn) = let f1 () = @@ -465,7 +476,8 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) in - if flags.modulo_conv_on_closed_terms = None then + if flags.modulo_conv_on_closed_terms = None || + subterm_restriction b flags then error_cannot_unify (fst curenvnb) sigma (cM,cN) else try f1 () with e when precatchable_exception e -> @@ -504,10 +516,11 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag in let evd = sigma in - if (if occur_meta_or_undefined_evar evd m || occur_meta_or_undefined_evar evd n then false + if (if occur_meta_or_undefined_evar evd m || occur_meta_or_undefined_evar evd n + || subterm_restriction conv_at_top flags then false else if (match flags.modulo_conv_on_closed_terms with - | Some flags -> is_trans_fconv cv_pb flags env sigma m n - | None -> constr_cmp cv_pb m n) then true + | Some convflags -> is_trans_fconv cv_pb convflags env sigma m n + | _ -> constr_cmp cv_pb m n) then true else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with | Some (cv_id, cv_k), (dl_id, dl_k) -> Idpred.subset dl_id cv_id && Cpred.subset dl_k cv_k @@ -828,7 +841,7 @@ let w_unify_core_0 env with_types cv_pb flags m n evd = let (mc1,evd') = retract_coercible_metas evd in let (sigma,ms,es) = check_types env flags (evd,mc1,[]) m n in let subst2 = - unify_0_with_initial_metas (evd',ms,es) true env cv_pb flags m n + unify_0_with_initial_metas (evd',ms,es) false env cv_pb flags m n in let evd = w_merge env with_types flags subst2 in if flags.resolve_evars then diff --git a/pretyping/unification.mli b/pretyping/unification.mli index aa0267698e..44b1c3889c 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -18,6 +18,7 @@ type unify_flags = { resolve_evars : bool; use_evars_pattern_unification : bool; frozen_evars : ExistentialSet.t; + restrict_conv_on_strict_subterms : bool; modulo_betaiota : bool; modulo_eta : bool; allow_K_in_toplevel_higher_order_unification : bool diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 35552b8d85..8c05499a2f 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -356,7 +356,12 @@ let connect_clenv gls clenv = In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma]. *) -let clenv_fchain ?(flags=elim_flags) mv clenv nextclenv = + +let fchain_flags = + { default_unify_flags with + allow_K_in_toplevel_higher_order_unification = true } + +let clenv_fchain ?(flags=fchain_flags) mv clenv nextclenv = (* Add the metavars of [nextclenv] to [clenv], with their name-environment *) let clenv' = { templval = clenv.templval; diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index dad4b5041e..a266405f7a 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -108,6 +108,7 @@ let fail_quick_unif_flags = { resolve_evars = false; use_evars_pattern_unification = false; frozen_evars = ExistentialSet.empty; + restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; modulo_eta = true; allow_K_in_toplevel_higher_order_unification = false diff --git a/tactics/auto.ml b/tactics/auto.ml index 6780ae2fcf..18e71661ff 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -846,6 +846,7 @@ let auto_unif_flags = { resolve_evars = true; use_evars_pattern_unification = false; frozen_evars = ExistentialSet.empty; + restrict_conv_on_strict_subterms = false; (* Compat *) modulo_betaiota = false; modulo_eta = true; allow_K_in_toplevel_higher_order_unification = false diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 3f4e773eca..b460222b95 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -80,6 +80,7 @@ let auto_unif_flags = { resolve_evars = false; use_evars_pattern_unification = true; frozen_evars = ExistentialSet.empty; + restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = true; modulo_eta = true; allow_K_in_toplevel_higher_order_unification = false diff --git a/tactics/equality.ml b/tactics/equality.ml index f6e8837f8b..98f47d8fbf 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -88,6 +88,7 @@ let rewrite_unif_flags = { Unification.resolve_evars = true; Unification.use_evars_pattern_unification = true; Unification.frozen_evars = ExistentialSet.empty; + Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; Unification.modulo_eta = true; Unification.allow_K_in_toplevel_higher_order_unification = false @@ -144,6 +145,7 @@ let rewrite_conv_closed_unif_flags = { Unification.resolve_evars = false; Unification.use_evars_pattern_unification = true; Unification.frozen_evars = ExistentialSet.empty; + Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; Unification.modulo_eta = true; Unification.allow_K_in_toplevel_higher_order_unification = false diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index b8ebf84a61..821284ec7f 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -308,6 +308,7 @@ let rewrite_unif_flags = { Unification.resolve_evars = true; Unification.use_evars_pattern_unification = true; Unification.frozen_evars = ExistentialSet.empty; + Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; Unification.modulo_eta = true; Unification.allow_K_in_toplevel_higher_order_unification = true @@ -321,6 +322,7 @@ let rewrite2_unif_flags = Unification.resolve_evars = true; Unification.use_evars_pattern_unification = true; Unification.frozen_evars = ExistentialSet.empty; + Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = true; Unification.modulo_eta = true; Unification.allow_K_in_toplevel_higher_order_unification = true @@ -335,6 +337,7 @@ let general_rewrite_unif_flags () = Unification.resolve_evars = true; Unification.use_evars_pattern_unification = true; Unification.frozen_evars = ExistentialSet.empty; + Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = true; Unification.modulo_eta = true; Unification.allow_K_in_toplevel_higher_order_unification = true } |