From 1177da32723fd46a82b66ca7ffe4d13d93480da6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 31 Oct 2014 17:29:49 +0100 Subject: Reorganization of the test for generic selection of occurrences in clause; extended it so that an induction over "x" is considered generic when the clause has the form "in H |-" (w/o the conclusion) and x does not occur in the conclusion. --- parsing/g_tactic.ml4 | 18 ++---------------- pretyping/locusops.ml | 14 ++++++++++---- pretyping/locusops.mli | 2 +- pretyping/unification.ml | 4 ++-- tactics/tactics.ml | 8 +++++++- 5 files changed, 22 insertions(+), 24 deletions(-) diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index fb09a3108..a57720755 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -174,23 +174,9 @@ let map_int_or_var f = function let all_concl_occs_clause = { onhyps=Some[]; concl_occs=AllOccurrences } -let has_no_specified_occs cl = - let forall ((occs, _), _) = match occs with - | AllOccurrences -> true - | _ -> false - in - let hyps = match cl.onhyps with - | None -> true - | Some hyps -> List.for_all forall hyps in - let concl = match cl.concl_occs with - | AllOccurrences | NoOccurrences -> true - | _ -> false - in - hyps && concl - let merge_occurrences loc cl = function | None -> - if has_no_specified_occs cl then (None, cl) + if Locusops.clause_with_generic_occurrences cl then (None, cl) else user_err_loc (loc,"",str "Found an \"at\" clause without \"with\" clause.") | Some (occs, p) -> @@ -203,7 +189,7 @@ let merge_occurrences loc cl = function | { onhyps = Some [(AllOccurrences, id), l]; concl_occs = NoOccurrences } -> { cl with onhyps = Some [(occs, id), l] } | _ -> - if has_no_specified_occs cl then + if Locusops.clause_with_generic_occurrences cl then user_err_loc (loc,"",str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.") else user_err_loc (loc,"",str "Cannot use clause \"at\" twice.") diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 7e825b6c2..cc19f01f8 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -102,7 +102,13 @@ let occurrences_of_goal cls = let in_every_hyp cls = Option.is_empty cls.onhyps -let has_selected_occurrences cls = - cls.concl_occs != AllOccurrences || - not (Option.is_empty cls.onhyps) && List.exists (fun ((occs,_),hl) -> - occs != AllOccurrences || hl != InHyp) (Option.get cls.onhyps) +let clause_with_generic_occurrences cls = + let hyps = match cls.onhyps with + | None -> true + | Some hyps -> + List.for_all + (function ((AllOccurrences,_),InHyp) -> true | _ -> false) hyps in + let concl = match cls.concl_occs with + | AllOccurrences | NoOccurrences -> true + | _ -> false in + hyps && concl diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index c1bf2d9ea..1d7c6b72e 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -42,4 +42,4 @@ val occurrences_of_hyp : Id.t -> clause -> (occurrences * hyp_location_flag) val occurrences_of_goal : clause -> occurrences val in_every_hyp : clause -> bool -val has_selected_occurrences : clause -> bool +val clause_with_generic_occurrences : 'a clause_expr -> bool diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 3f2963bfe..3f6a4e307 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1468,7 +1468,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = else x in - let likefirst = not (has_selected_occurrences occs) in + let likefirst = clause_with_generic_occurrences occs in let mkvarid () = mkVar id in let compute_dependency _ (hyp,_,_ as d) (sign,depdecls) = match occurrences_of_hyp hyp occs with @@ -1508,7 +1508,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = in let lastlhyp = if List.is_empty depdecls then None else Some (pi1(List.last depdecls)) in - (id,sign,depdecls,lastlhyp,ccl,out test) + (id,sign,depdecls,lastlhyp,ccl,out test) with SubtermUnificationError e -> raise (PretypeError (env,sigma,CannotUnifyOccurrences e)) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f315f4445..4d8c97870 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3876,6 +3876,11 @@ let pose_induction_arg clear_flag isrec with_evars info_arg elim end end +let has_generic_occurrences_but_goal cls id env ccl = + clause_with_generic_occurrences cls && + (* TODO: whd_evar of goal *) + (cls.concl_occs != NoOccurrences || not (occur_var env id ccl)) + let induction_gen clear_flag isrec with_evars elim ((_pending,(c,lbind)),(eqname,names) as arg) cls = let inhyps = match cls with @@ -3884,11 +3889,12 @@ let induction_gen clear_flag isrec with_evars elim Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in + let ccl = Proofview.Goal.raw_concl gl in let cls = Option.default allHypsAndConcl cls in let t = typ_of env sigma c in let is_arg_pure_hyp = isVar c && lbind == NoBindings && not with_evars && Option.is_empty eqname - && not (has_selected_occurrences cls) in + && has_generic_occurrences_but_goal cls (destVar c) env ccl in let enough_applied = check_enough_applied env sigma elim t in if is_arg_pure_hyp && enough_applied then (* First case: induction on a variable already in an inductive type and -- cgit v1.2.3