diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | lib/flags.ml | 2 | ||||
| -rw-r--r-- | lib/flags.mli | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 86 | ||||
| -rw-r--r-- | pretyping/unification.mli | 5 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 5 | ||||
| -rw-r--r-- | tactics/auto.ml | 7 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 5 | ||||
| -rw-r--r-- | tactics/equality.ml | 11 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 15 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
11 files changed, 105 insertions, 38 deletions
@@ -33,6 +33,9 @@ Tactics result in some rare incompatibilities (solvable by adapting name hypotheses). - Introduction pattern "_" made more robust. - Tactic (and Eval command) vm_compute can now be interrupted via Ctrl-C. +- Unification in "apply" supports unification of patterns of the form + ?f x y = g(x,y) (compatibility ensured by using + "Unset Tactic Pattern Unification"). Vernacular commands diff --git a/lib/flags.ml b/lib/flags.ml index e8763bc79f..b9965af5dd 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -36,7 +36,7 @@ let raw_print = ref false (* Compatibility mode *) -type compat_version = V8_2 +type compat_version = V8_2 | V8_3 let compat_version = ref None let version_strictly_greater v = match !compat_version with None -> true | Some v' -> v'>v diff --git a/lib/flags.mli b/lib/flags.mli index f7e3c17597..4fd042e225 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -25,7 +25,7 @@ val load_proofs : load_proofs ref val raw_print : bool ref -type compat_version = V8_2 +type compat_version = V8_2 | V8_3 val compat_version : compat_version option ref val version_strictly_greater : compat_version -> bool val version_less_or_equal : compat_version -> bool diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5a2dfead7c..79debed864 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -156,29 +156,71 @@ let _ = optread = (fun () -> !global_evars_pattern_unification_flag); optwrite = (:=) global_evars_pattern_unification_flag } +let _ = + declare_bool_option + { optsync = true; + optname = "pattern-unification for existential variables in tactics"; + optkey = ["Tactic";"Pattern";"Unification"]; + optread = (fun () -> !global_evars_pattern_unification_flag); + optwrite = (:=) global_evars_pattern_unification_flag } + type unify_flags = { modulo_conv_on_closed_terms : Names.transparent_state option; - use_metas_eagerly : bool; + (* What this flag controls was activated with all constants transparent, *) + (* even for auto, since Coq V5.10 *) + + use_metas_eagerly_in_conv_on_closed_terms : bool; + (* This refinement of the conversion on closed terms is activable *) + (* (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 *) + (* (but not simple apply) since Feb 2008 for 8.2 *) + modulo_delta_types : Names.transparent_state; + resolve_evars : bool; - use_evars_pattern_unification : bool; + (* This says if type classes instances resolution must be used to infer *) + (* the remaining evars *) + + use_pattern_unification : bool; + (* This says if type classes instances resolution must be used to infer *) + (* the remaining evars *) + + use_meta_bound_pattern_unification : bool; + (* This solves pattern "?n x1 ... xn = t" when the xi are distinct rels *) + (* This allows for instance to unify "forall x:A, B(x)" with "A' -> B'" *) + (* This was on for all tactics, including auto, since Sep 2006 for 8.1 *) + frozen_evars : ExistentialSet.t; + (* Evars of this set are considered axioms and never instantiated *) + (* Useful e.g. for autorewrite *) + restrict_conv_on_strict_subterms : bool; + (* No conversion at the root of the term; potentially useful for rewrite *) + modulo_betaiota : bool; + (* Support betaiota in the reduction *) + (* Note that zeta is always used *) + modulo_eta : bool; + (* Support eta in the reduction *) + allow_K_in_toplevel_higher_order_unification : bool + (* This is used only in second/higher order unification when looking for *) + (* subterms (rewrite and elim) *) } (* Default flag for unifying a type against a type (e.g. apply) *) (* We set all conversion flags *) let default_unify_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly = true; + use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = full_transparent_state; modulo_delta_types = full_transparent_state; resolve_evars = false; - use_evars_pattern_unification = true; + use_pattern_unification = true; + use_meta_bound_pattern_unification = true; frozen_evars = ExistentialSet.empty; restrict_conv_on_strict_subterms = false; modulo_betaiota = true; @@ -193,11 +235,12 @@ let default_unify_flags = { (* out of "simple apply" *) let default_no_delta_unify_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly = true; + use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; resolve_evars = false; - use_evars_pattern_unification = false; + use_pattern_unification = false; + use_meta_bound_pattern_unification = true; frozen_evars = ExistentialSet.empty; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; @@ -212,11 +255,12 @@ let default_no_delta_unify_flags = { (* 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 = true; + use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = full_transparent_state; modulo_delta_types = full_transparent_state; resolve_evars = false; - use_evars_pattern_unification = true; + use_pattern_unification = true; + use_meta_bound_pattern_unification = true; frozen_evars = ExistentialSet.empty; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; @@ -226,11 +270,12 @@ let elim_flags = { let elim_no_delta_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly = true; + use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; resolve_evars = false; - use_evars_pattern_unification = false; + use_pattern_unification = false; + use_meta_bound_pattern_unification = true; frozen_evars = ExistentialSet.empty; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; @@ -242,9 +287,15 @@ let set_no_head_reduction flags = { flags with restrict_conv_on_strict_subterms = true } let use_evars_pattern_unification flags = - !global_evars_pattern_unification_flag && flags.use_evars_pattern_unification + !global_evars_pattern_unification_flag && flags.use_pattern_unification && Flags.version_strictly_greater Flags.V8_2 +let use_metas_pattern_unification flags nb l = + !global_evars_pattern_unification_flag && flags.use_pattern_unification + || (Flags.version_less_or_equal Flags.V8_3 || + flags.use_meta_bound_pattern_unification) && + array_for_all (fun c -> isRel c && destRel c <= nb) l + let expand_key env = function | Some (ConstKey cst) -> constant_opt_value env cst | Some (VarKey id) -> (try named_body id env with Not_found -> None) @@ -355,15 +406,15 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag reduce curenvnb pb b substn cM cN) | App (f1,l1), _ when - (isMeta f1 || use_evars_pattern_unification flags && - isAllowedEvar flags f1) & + (isMeta f1 && use_metas_pattern_unification flags (snd curenvnb) l1 + || use_evars_pattern_unification flags && isAllowedEvar flags f1) & is_unification_pattern curenvnb f1 l1 cN & not (dependent f1 cN) -> solve_pattern_eqn_array curenvnb f1 l1 cN substn | _, App (f2,l2) when - (isMeta f2 || use_evars_pattern_unification flags && - isAllowedEvar flags f2) & + (isMeta f2 && use_metas_pattern_unification flags (snd curenvnb) l2 + || use_evars_pattern_unification flags && isAllowedEvar flags f2) & is_unification_pattern curenvnb f2 l2 cM & not (dependent f2 cM) -> solve_pattern_eqn_array curenvnb f2 l2 cM substn @@ -429,10 +480,11 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag (it is used by apply and rewrite); it might now be redundant with the support for delta-expansion (which is used essentially for apply)... *) + not (subterm_restriction b flags) && match flags.modulo_conv_on_closed_terms with | None -> false - | Some convflags when not (subterm_restriction b flags) -> - let subst = if flags.use_metas_eagerly then metasubst else ms in + | Some convflags -> + let subst = if flags.use_metas_eagerly_in_conv_on_closed_terms then metasubst else ms in match subst_defined_metas subst cM with | None -> (* some undefined Metas in cM *) false | Some m1 -> diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 44b1c3889c..37eaa58026 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -12,11 +12,12 @@ open Evd type unify_flags = { modulo_conv_on_closed_terms : Names.transparent_state option; - use_metas_eagerly : bool; + use_metas_eagerly_in_conv_on_closed_terms : bool; modulo_delta : Names.transparent_state; modulo_delta_types : Names.transparent_state; resolve_evars : bool; - use_evars_pattern_unification : bool; + use_pattern_unification : bool; + use_meta_bound_pattern_unification : bool; frozen_evars : ExistentialSet.t; restrict_conv_on_strict_subterms : bool; modulo_betaiota : bool; diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index a266405f7a..ec9aada73c 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -102,11 +102,12 @@ let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft let fail_quick_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly = false; + use_metas_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; resolve_evars = false; - use_evars_pattern_unification = false; + use_pattern_unification = false; + use_meta_bound_pattern_unification = true; (* ? *) frozen_evars = ExistentialSet.empty; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; diff --git a/tactics/auto.ml b/tactics/auto.ml index 18e71661ff..af9420a245 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -840,11 +840,12 @@ open Unification let auto_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly = false; + use_metas_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; resolve_evars = true; - use_evars_pattern_unification = false; + use_pattern_unification = false; + use_meta_bound_pattern_unification = true; frozen_evars = ExistentialSet.empty; restrict_conv_on_strict_subterms = false; (* Compat *) modulo_betaiota = false; @@ -971,7 +972,7 @@ and my_find_search mod_delta = else my_find_search_nodelta and my_find_search_delta db_list local_db hdc concl = - let flags = {auto_unif_flags with use_metas_eagerly = true} in + let flags = {auto_unif_flags with use_metas_eagerly_in_conv_on_closed_terms = true} in let f = hintmap_of hdc concl in if occur_existential concl then list_map_append diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index b460222b95..aed9f59857 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -74,11 +74,12 @@ open Unification let auto_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly = true; + use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = var_full_transparent_state; modulo_delta_types = full_transparent_state; resolve_evars = false; - use_evars_pattern_unification = true; + use_pattern_unification = true; + use_meta_bound_pattern_unification = true; frozen_evars = ExistentialSet.empty; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = true; diff --git a/tactics/equality.ml b/tactics/equality.ml index d2970603ea..3a40994f8c 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -82,11 +82,12 @@ type conditions = let rewrite_unif_flags = { Unification.modulo_conv_on_closed_terms = None; - Unification.use_metas_eagerly = true; + Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = empty_transparent_state; Unification.resolve_evars = true; - Unification.use_evars_pattern_unification = true; + Unification.use_pattern_unification = true; + Unification.use_meta_bound_pattern_unification = true; Unification.frozen_evars = ExistentialSet.empty; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; @@ -142,17 +143,19 @@ let rewrite_conv_closed_unif_flags = { (* We have this flag for historical reasons, it has e.g. the consequence *) (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *) - Unification.use_metas_eagerly = true; + Unification.use_metas_eagerly_in_conv_on_closed_terms = true; (* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *) (* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *) Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = full_transparent_state; Unification.resolve_evars = false; - Unification.use_evars_pattern_unification = true; + Unification.use_pattern_unification = true; (* To rewrite "?n x y" in "y+x=0" when ?n is *) (* a preexisting evar of the goal*) + Unification.use_meta_bound_pattern_unification = true; + Unification.frozen_evars = ExistentialSet.empty; (* This is set dynamically *) diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 821284ec7f..5400827bcf 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -302,11 +302,12 @@ let rewrite_transparent_state () = let rewrite_unif_flags = { Unification.modulo_conv_on_closed_terms = None; - Unification.use_metas_eagerly = true; + Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = full_transparent_state; Unification.resolve_evars = true; - Unification.use_evars_pattern_unification = true; + Unification.use_pattern_unification = true; + Unification.use_meta_bound_pattern_unification = true; Unification.frozen_evars = ExistentialSet.empty; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; @@ -316,11 +317,12 @@ let rewrite_unif_flags = { let rewrite2_unif_flags = { Unification.modulo_conv_on_closed_terms = Some conv_transparent_state; - Unification.use_metas_eagerly = true; + Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = conv_transparent_state; Unification.resolve_evars = true; - Unification.use_evars_pattern_unification = true; + Unification.use_pattern_unification = true; + Unification.use_meta_bound_pattern_unification = true; Unification.frozen_evars = ExistentialSet.empty; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = true; @@ -331,11 +333,12 @@ let rewrite2_unif_flags = let general_rewrite_unif_flags () = let ts = rewrite_transparent_state () in { Unification.modulo_conv_on_closed_terms = Some ts; - Unification.use_metas_eagerly = true; + Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = ts; Unification.modulo_delta_types = ts; Unification.resolve_evars = true; - Unification.use_evars_pattern_unification = true; + Unification.use_pattern_unification = true; + Unification.use_meta_bound_pattern_unification = true; Unification.frozen_evars = ExistentialSet.empty; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = true; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 060cd94a87..97928c87c2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -842,6 +842,7 @@ type conjunction_status = let make_projection sigma params cstr sign elim i n c = let elim = match elim with | NotADefinedRecordUseScheme elim -> + (* bugs: goes from right to left when i increases! *) let (na,b,t) = List.nth cstr.cs_args i in let b = match b with None -> mkRel (i+1) | Some b -> b in let branch = it_mkLambda_or_LetIn b cstr.cs_args in @@ -856,6 +857,7 @@ let make_projection sigma params cstr sign elim i n c = else None | DefinedRecord l -> + (* goes from left to right when i increases! *) match List.nth l i with | Some proj -> let t = Typeops.type_of_constant (Global.env()) proj in |