diff options
| -rw-r--r-- | proofs/clenv.ml | 105 | ||||
| -rw-r--r-- | proofs/clenv.mli | 2 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 10 | ||||
| -rw-r--r-- | test-suite/success/auto.v | 18 |
6 files changed, 100 insertions, 41 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index a8b13e8456..12b734e563 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -197,24 +197,58 @@ let clenv_assign mv rhs clenv = (* [clenv_dependent hyps_only clenv] * returns a list of the metavars which appear in the template of clenv, - * and which are dependent, This is computed by taking the metavars in cval, - * in right-to-left order, and collecting the metavars which appear + * and which are dependent, This is computed by taking the metavars of the + * template in right-to-left order, and collecting the metavars which appear * in their types, and adding in all the metavars appearing in the * type of clenv. - * If [hyps_only] then metavariables occurring in the type are _excluded_ *) + * If [hyps_only] then metavariables occurring in the concl are _excluded_ + * If [iter] is also set then all metavariables *recursively* occurring + * in the concl are _excluded_ -(* [clenv_metavars clenv mv] - * returns a list of the metavars which appear in the type of - * the metavar mv. The list is unordered. *) + Details of the strategies used for computing the set of unresolved + dependent metavariables -let clenv_metavars evd mv = + We typically have a clause of the form + + lem(?T:Type,?T,?U:Type,?V:Type,?x:?T,?y:?U,?z:?V,?H:hyp(?x,?z)) :concl(?y,?z) + + Then, we compute: + A = the set of all unresolved metas + C = the set of metas occurring in concl (here ?y, ?z) + C* = the recursive closure of C wrt types (here ?y, ?z, ?U, ?V) + D = the set of metas occurring in a type of meta (here ?x, ?T, ?z, ?U, ?V) + NL = the set of duplicated metas even if non dependent (here ?T) + (we make the assumption that duplicated metas have internal dependencies) + + Then, for the "apply"-style tactic (hyps_only), missing metas are + A inter ((D minus C) union NL) + + for the optimized "apply"-style tactic (taking in care, f_equal style + lemma, from 2/8/10, Coq > 8.3), missing metas are + A inter (( D minus C* ) union NL) + + for the "elim"-style tactic, missing metas are + A inter (D union C union NL) + + In any case, we respect the order given in A. +*) + +let clenv_metas_in_type_of_meta evd mv = (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas -let dependent_metas clenv mvs conclmetas = +let dependent_in_type_of_metas clenv mvs = List.fold_right - (fun mv deps -> - Metaset.union deps (clenv_metavars clenv.evd mv)) - mvs conclmetas + (fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv.evd mv)) + mvs Metaset.empty + +let dependent_closure clenv mvs = + let rec aux mvs acc = + Metaset.fold + (fun mv deps -> + let metas_of_meta_type = clenv_metas_in_type_of_meta clenv.evd mv in + aux metas_of_meta_type (Metaset.union deps metas_of_meta_type)) + mvs acc in + aux mvs mvs let duplicated_metas c = let rec collrec (one,more as acc) c = @@ -224,20 +258,24 @@ let duplicated_metas c = in snd (collrec ([],[]) c) -let clenv_dependent hyps_only clenv = - let mvs = undefined_metas clenv.evd in - let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in - let deps = dependent_metas clenv mvs ctyp_mvs in - let nonlinear = duplicated_metas (clenv_value clenv) in - let ctyp_mvs = dependent_metas clenv (Metaset.elements ctyp_mvs) ctyp_mvs in - (* Make the assumption that duplicated metas have internal dependencies *) +let clenv_dependent_gen hyps_only ?(iter=true) clenv = + let all_undefined = undefined_metas clenv.evd in + let deps_in_concl = (mk_freelisted (clenv_type clenv)).freemetas in + let deps_in_hyps = dependent_in_type_of_metas clenv all_undefined in + let non_linear = duplicated_metas (clenv_value clenv) in + let deps_in_concl = + if hyps_only && iter then dependent_closure clenv deps_in_concl + else deps_in_concl in List.filter - (fun mv -> if Metaset.mem mv deps - then not (hyps_only && Metaset.mem mv ctyp_mvs) - else List.mem mv nonlinear) - mvs + (fun mv -> + Metaset.mem mv deps_in_hyps && + not (hyps_only && Metaset.mem mv deps_in_concl) + || not hyps_only && Metaset.mem mv deps_in_concl + || List.mem mv non_linear) + all_undefined -let clenv_missing ce = clenv_dependent true ce +let clenv_missing ce = clenv_dependent_gen true ce +let clenv_dependent ce = clenv_dependent_gen false ce (******************************************************************) @@ -373,7 +411,7 @@ type arg_bindings = constr explicit_bindings let clenv_independent clenv = let mvs = collect_metas (clenv_value clenv) in let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in - let deps = dependent_metas clenv mvs ctyp_mvs in + let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in List.filter (fun mv -> not (Metaset.mem mv deps)) mvs let check_bindings bl = @@ -448,17 +486,28 @@ let clenv_constrain_last_binding c clenv = let k = try list_last all_mvs with Failure _ -> raise NoSuchBinding in clenv_assign_binding clenv k c +let error_not_right_number_missing_arguments n = + errorlabstrm "" + (strbrk "Not the right number of missing arguments (expected " ++ + int n ++ str ").") + let clenv_constrain_dep_args hyps_only bl clenv = if bl = [] then clenv else - let occlist = clenv_dependent hyps_only clenv in + let occlist = clenv_dependent_gen hyps_only clenv in if List.length occlist = List.length bl then List.fold_left2 clenv_assign_binding clenv occlist bl else - errorlabstrm "" - (strbrk "Not the right number of missing arguments (expected " ++ - int (List.length occlist) ++ str ").") + if hyps_only then + (* Tolerance for compatibility <= 8.3 *) + let occlist' = clenv_dependent_gen hyps_only ~iter:false clenv in + if List.length occlist' = List.length bl then + List.fold_left2 clenv_assign_binding clenv occlist' bl + else + error_not_right_number_missing_arguments (List.length occlist) + else + error_not_right_number_missing_arguments (List.length occlist) (****************************************************************) (* Clausal environment for an application *) diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 1b4b0514b0..363cf423b0 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -71,7 +71,7 @@ val clenv_unique_resolver : val evar_clenv_unique_resolver : bool -> ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv -val clenv_dependent : bool -> clausenv -> metavariable list +val clenv_dependent : clausenv -> metavariable list val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 272eead6c4..85e4580c86 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -61,7 +61,7 @@ let clenv_value_cast_meta clenv = clenv_cast_meta clenv (clenv_value clenv) let clenv_pose_dependent_evars with_evars clenv = - let dep_mvs = clenv_dependent false clenv in + let dep_mvs = clenv_dependent clenv in if dep_mvs <> [] & not with_evars then raise (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); diff --git a/tactics/equality.ml b/tactics/equality.ml index 9e716aae51..a4e2b510fd 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -103,9 +103,7 @@ let instantiate_lemma_all env sigma gl c ty l l2r concl = | _ -> error "The term provided is not an applied relation." in let others,(c1,c2) = split_last_two args in let try_occ (evd', c') = - let cl' = {eqclause with evd = evd'} in - let mvs = clenv_dependent false cl' in - clenv_pose_metas_as_evars cl' mvs + clenv_pose_dependent_evars true {eqclause with evd = evd'} in let occs = Unification.w_unify_to_subterm_all ~flags:rewrite_unif_flags env diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 0e9281a21d..4524cf0dae 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -349,10 +349,7 @@ let unify_eqn env sigma hypinfo t = (* For Ring essentially, only when doing setoid_rewrite *) clenv_unify allowK ~flags:rewrite2_unif_flags CONV left t cl in - let env' = - let mvs = clenv_dependent false env' in - clenv_pose_metas_as_evars env' mvs - in + let env' = Clenvtac.clenv_pose_dependent_evars true env' in let evd' = Typeclasses.resolve_typeclasses ~fail:true env'.env env'.evd in let env' = { env' with evd = evd' } in let nf c = Evarutil.nf_evar evd' (Clenv.clenv_nf_meta env' c) in @@ -1552,10 +1549,7 @@ let unification_rewrite l2r c1 c2 cl car rel but gl = in let evd' = Typeclasses.resolve_typeclasses ~fail:false env evd' in let cl' = {cl with evd = evd'} in - let cl' = - let mvs = clenv_dependent false cl' in - clenv_pose_metas_as_evars cl' mvs - in + let cl' = Clenvtac.clenv_pose_dependent_evars true cl' in let nf c = Evarutil.nf_evar ( cl'.evd) (Clenv.clenv_nf_meta cl' c) in let c1 = if l2r then nf c' else nf c1 and c2 = if l2r then nf c2 else nf c' diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v new file mode 100644 index 0000000000..a2701f8bbe --- /dev/null +++ b/test-suite/success/auto.v @@ -0,0 +1,18 @@ +(* Wish #2154 by E. van der Weegen *) + +(* auto was not using f_equal-style lemmas with metavariables occuring + only in the type of an evar of the concl, but not directly in the + concl itself *) + +Parameters + (F: Prop -> Prop) + (G: forall T, (T -> Prop) -> Type) + (L: forall A (P: A -> Prop), G A P -> forall x, F (P x)) + (Q: unit -> Prop). + +Hint Resolve L. + +Goal G unit Q -> F (Q tt). + intro. + auto. +Qed. |