diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-10 19:35:23 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-10 19:35:23 +0000 |
| commit | 5d8d8e858e56c0d12cb262d5ff8e733ae7afc102 (patch) | |
| tree | 90c20481422f774db9d25e70f98713a907e8894f | |
| parent | 0039bf5442d91443f9ef3e2a83afdbd65524de84 (diff) | |
- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)
- Changement au passage de la convention "at -n1 ... -n2" en
"at - n1 ... n2" qui me paraît plus clair à partir du moment où on peut
pas mélanger des positifs et des négatifs.
- Au passage:
- simplification de gclause avec fusion de onconcl et concl_occs,
- généralisation de l'utilisation de la désignation des occurrences par la
négative aux cas de setoid_rewrite, clrewrite et rewrite at,
- correction d'un bug de "rewrite in at" qui utilisait le at de la
conclusion dans les hyps.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11094 85f007b7-540e-0410-9357-904b9bb8a0f7
45 files changed, 474 insertions, 425 deletions
diff --git a/contrib/firstorder/rules.ml b/contrib/firstorder/rules.ml index b6112e653..813e951cf 100644 --- a/contrib/firstorder/rules.ml +++ b/contrib/firstorder/rules.ml @@ -204,8 +204,8 @@ let ll_forall_tac prod backtrack id continue seq= let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str let defined_connectives=lazy - [[],EvalConstRef (destConst (constant "not")); - [],EvalConstRef (destConst (constant "iff"))] + [all_occurrences,EvalConstRef (destConst (constant "not")); + all_occurrences,EvalConstRef (destConst (constant "iff"))] let normalize_evaluables= onAllClauses @@ -213,4 +213,4 @@ let normalize_evaluables= None->unfold_in_concl (Lazy.force defined_connectives) | Some ((_,id),_)-> unfold_in_hyp (Lazy.force defined_connectives) - (([],id),Tacexpr.InHypTypeOnly)) + ((Rawterm.all_occurrences_expr,id),Tacexpr.InHypTypeOnly)) diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 558ca6c21..3d80bd004 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -637,7 +637,7 @@ let build_proof [ h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); thin dyn_infos.rec_hyps; - pattern_option [[-1],t] None; + pattern_option [(false,[1]),t] None; h_simplest_case t; (fun g' -> let g'_nb_prod = nb_prod (pf_concl g') in @@ -1246,7 +1246,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in tclTHENSEQ - [unfold_in_concl [([],Names.EvalConstRef fname)]; + [unfold_in_concl [(all_occurrences,Names.EvalConstRef fname)]; let do_prove = build_proof interactive_proof @@ -1347,11 +1347,10 @@ let build_clause eqs = { Tacexpr.onhyps = Some (List.map - (fun id -> ([],id),Tacexpr.InHyp) + (fun id -> (Rawterm.all_occurrences_expr,id),Tacexpr.InHyp) eqs ); - Tacexpr.onconcl = false; - Tacexpr.concl_occs = [] + Tacexpr.concl_occs = Rawterm.no_occurrences_expr } let rec rewrite_eqs_in_eqs eqs = @@ -1364,7 +1363,7 @@ let rec rewrite_eqs_in_eqs eqs = (fun id gl -> observe_tac (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id)) - (tclTRY (Equality.general_rewrite_in true [] id (mkVar eq) false)) + (tclTRY (Equality.general_rewrite_in true all_occurrences id (mkVar eq) false)) gl ) eqs @@ -1386,7 +1385,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = (fun g -> if is_mes then - unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] g + unfold_in_concl [(all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g else tclIDTAC g ); observe_tac "rew_and_finish" diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index a5bd519e2..0160c290f 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -16,6 +16,7 @@ open Tacticals open Tactics open Indfun_common open Tacmach +open Termops open Sign open Hiddentac @@ -314,7 +315,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem | None -> (id::pre_args,pre_tac) | Some b -> (pre_args, - tclTHEN (h_reduce (Rawterm.Unfold([[],EvalVarRef id])) allHyps) pre_tac + tclTHEN (h_reduce (Rawterm.Unfold([Rawterm.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac ) else (pre_args,pre_tac) @@ -687,7 +688,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = h_generalize (List.map mkVar ids); thin ids ] - else unfold_in_concl [([],Names.EvalConstRef (destConst f))] + else unfold_in_concl [(all_occurrences,Names.EvalConstRef (destConst f))] in (* The proof of each branche itself *) let ind_number = ref 0 in diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml index f4f852d36..13989f03b 100644 --- a/contrib/funind/recdef.ml +++ b/contrib/funind/recdef.ml @@ -296,7 +296,7 @@ let mkCaseEq a : tactic = [h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]; (fun g2 -> change_in_concl None - (pattern_occs [([-1], a)] (pf_env g2) Evd.empty (pf_concl g2)) + (pattern_occs [((false,[1]), a)] (pf_env g2) Evd.empty (pf_concl g2)) g2); simplest_case a] g);; @@ -323,7 +323,7 @@ let mkDestructEq : [h_generalize new_hyps; (fun g2 -> change_in_concl None - (pattern_occs [([-1], expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2); + (pattern_occs [((false,[1]), expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2); simplest_case expr], to_revert let rec mk_intros_and_continue thin_intros (extra_eqn:bool) @@ -336,7 +336,7 @@ let rec mk_intros_and_continue thin_intros (extra_eqn:bool) h_intros thin_intros; tclMAP - (fun eq -> tclTRY (Equality.general_rewrite_in true [] teq eq false)) + (fun eq -> tclTRY (Equality.general_rewrite_in true all_occurrences teq eq false)) (List.rev eqs); (fun g1 -> let ty_teq = pf_type_of g1 (mkVar teq) in @@ -397,7 +397,7 @@ let tclUSER tac is_mes l g = clear_tac; if is_mes then tclTHEN - (unfold_in_concl [([], evaluable_of_global_reference + (unfold_in_concl [(all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))]) tac else tac @@ -496,7 +496,7 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs = Nameops.out_name k_na,Nameops.out_name def_na in tclTHENS - (general_rewrite_bindings false [] + (general_rewrite_bindings false all_occurrences (mkVar eq, ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k; dummy_loc, NamedHyp def_id, mkVar def]) false) @@ -531,7 +531,7 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs observe_tac "intros k h' def" (h_intros [k;h';def]); observe_tac "simple_iter" (simpl_iter onConcl); observe_tac "unfold functional" - (unfold_in_concl[([1],evaluable_of_global_reference func)]); + (unfold_in_concl[((true,[1]),evaluable_of_global_reference func)]); observe_tac "rewriting equations" (list_rewrite true eqs); observe_tac ("cond rewrite "^(string_of_id k)) (list_cond_rewrite k def bound cond_eqs le_proofs); @@ -1120,7 +1120,7 @@ let start_equation (f:global_reference) (term_f:global_reference) let x = n_x_id ids nargs in tclTHENLIST [ h_intros x; - unfold_in_concl [([], evaluable_of_global_reference f)]; + unfold_in_concl [(all_occurrences, evaluable_of_global_reference f)]; observe_tac "simplest_case" (simplest_case (mkApp (terminate_constr, Array.of_list (List.map mkVar x)))); @@ -1144,7 +1144,7 @@ let base_leaf_eq func eqs f_id g = [|mkApp (delayed_force coq_S, [|mkVar p|]); mkApp(delayed_force lt_n_Sn, [|mkVar p|]); f_id|]))); simpl_iter onConcl; - tclTRY (unfold_in_concl [([1], evaluable_of_global_reference func)]); + tclTRY (unfold_in_concl [((true,[1]), evaluable_of_global_reference func)]); list_rewrite true eqs; apply (delayed_force refl_equal)] g;; @@ -1160,9 +1160,9 @@ let rec introduce_all_values_eq cont_tac functional termine [forward None (IntroIdentifier heq2) (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|])); simpl_iter (onHyp heq2); - unfold_in_hyp [([1], evaluable_of_global_reference + unfold_in_hyp [((true,[1]), evaluable_of_global_reference (global_of_constr functional))] - (([], heq2), Tacexpr.InHyp); + ((all_occurrences_expr, heq2), Tacexpr.InHyp); tclTHENS (fun gls -> let t_eq = compute_renamed_type gls (mkVar heq2) in @@ -1170,7 +1170,7 @@ let rec introduce_all_values_eq cont_tac functional termine let _,_,t = destProd t_eq in let def_na,_,_ = destProd t in Nameops.out_name def_na in - observe_tac "rewrite heq" (general_rewrite_bindings false [] + observe_tac "rewrite heq" (general_rewrite_bindings false all_occurrences (mkVar heq2, ExplicitBindings[dummy_loc,NamedHyp def_id, f]) false) gls) @@ -1226,7 +1226,7 @@ let rec introduce_all_values_eq cont_tac functional termine f_S(mkVar pmax'); dummy_loc, NamedHyp def_id, f]) in - observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false [] + observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false all_occurrences c_b false)) g ) diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 10fafaefc..6ec0fac42 100644 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -188,7 +188,7 @@ and e_my_find_search db_list local_db hdc concl = | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (unify_e_resolve (term,cl)) (e_trivial_fail_db db_list local_db) - | Unfold_nth c -> unfold_in_concl [[],c] + | Unfold_nth c -> unfold_in_concl [all_occurrences,c] | Extern tacast -> Auto.conclPattern concl (Option.get p) tacast in @@ -403,7 +403,7 @@ and my_find_search db_list local_db hdc concl = tclTHEN (unify_resolve st (term,cl)) (trivial_fail_db db_list local_db) - | Unfold_nth c -> unfold_in_concl [[],c] + | Unfold_nth c -> unfold_in_concl [all_occurrences,c] | Extern tacast -> conclPattern concl (Option.get p) tacast)) tacl diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index ac152f906..06b957d9c 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -166,7 +166,7 @@ let make_pbp_atomic_tactic = function TacAtom (zz, TacSplit (false,true,ImplicitBindings [make_pbp_pattern x])) | PbpGeneralize (h,args) -> let l = List.map make_pbp_pattern args in - TacAtom (zz, TacGeneralize [([],make_app (make_var h) l),Anonymous]) + TacAtom (zz, TacGeneralize [((true,[]),make_app (make_var h) l),Anonymous]) | PbpLeft -> TacAtom (zz, TacLeft (false,NoBindings)) | PbpRight -> TacAtom (zz, TacRight (false,NoBindings)) | PbpIntros l -> TacAtom (zz, TacIntroPattern l) diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index a2a504fb4..953fb5e79 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -1612,7 +1612,7 @@ and natural_fix ig lh g gs narg ltree = | _ -> assert false and natural_reduce ig lh g gs ge mode la ltree = match la with - {onhyps=Some[];onconcl=true} -> + {onhyps=Some[]} when la.concl_occs <> no_occurrences_expr -> spv [ (natural_lhyp lh ig.ihsg); (show_goal2 lh ig g gs ""); @@ -1620,7 +1620,7 @@ and natural_reduce ig lh g gs ge mode la ltree = {ihsg=All_subgoals_hyp;isgintro="simpl"}) ltree) ] - | {onhyps=Some[hyp]; onconcl=false} -> + | {onhyps=Some[hyp]} when la.concl_occs = no_occurrences_expr -> spv [ (natural_lhyp lh ig.ihsg); (show_goal2 lh ig g gs ""); diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index b041272c1..fa8f05713 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -464,24 +464,31 @@ let (xlate_ident_or_metaid: AI (_, x) -> xlate_ident x | MetaId(_, x) -> CT_metaid x;; +let nums_of_occs (b,nums) = + if b then nums + else List.map (function ArgArg x -> ArgArg (-x) | y -> y) nums + let xlate_hyp = function | AI (_,id) -> xlate_ident id | MetaId _ -> xlate_error "MetaId should occur only in quotations" let xlate_hyp_location = function - | (nums, AI (_,id)), InHypTypeOnly -> - CT_intype(xlate_ident id, nums_or_var_to_int_list nums) - | (nums, AI (_,id)), InHypValueOnly -> - CT_invalue(xlate_ident id, nums_or_var_to_int_list nums) - | ([], AI (_,id)), InHyp -> + | (occs, AI (_,id)), InHypTypeOnly -> + CT_intype(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs)) + | (occs, AI (_,id)), InHypValueOnly -> + CT_invalue(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs)) + | ((true,[]), AI (_,id)), InHyp -> CT_coerce_UNFOLD_to_HYP_LOCATION (CT_coerce_ID_to_UNFOLD (xlate_ident id)) - | (a::l, AI (_,id)), InHyp -> + | ((_,a::l as occs), AI (_,id)), InHyp -> + let nums = nums_of_occs occs in + let a = List.hd nums and l = List.tl nums in CT_coerce_UNFOLD_to_HYP_LOCATION (CT_unfold_occ (xlate_ident id, CT_int_ne_list(num_or_var_to_int a, nums_or_var_to_int_list_aux l))) + | ((false,[]), AI (_,id)), InHyp -> xlate_error "Unused" | (_, MetaId _),_ -> xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)" @@ -494,7 +501,7 @@ let xlate_clause cls = | Some l -> CT_hyp_location_list(List.map xlate_hyp_location l) in CT_clause (hyps_info, - if cls.onconcl then + if cls.concl_occs <> no_occurrences_expr then CT_coerce_STAR_to_STAR_OPT CT_star else CT_coerce_NONE_to_STAR_OPT CT_none) @@ -667,11 +674,13 @@ let xlate_using = function | Some (c2,sl2) -> CT_using (xlate_formula c2, xlate_bindings sl2);; let xlate_one_unfold_block = function - ([],qid) -> + ((true,[]),qid) -> CT_coerce_ID_to_UNFOLD(apply_or_by_notation tac_qualid_to_ct_ID qid) - | (n::nums, qid) -> + | (((_,_::_) as occs), qid) -> + let l = nums_of_occs occs in CT_unfold_occ(apply_or_by_notation tac_qualid_to_ct_ID qid, - nums_or_var_to_int_ne_list n nums) + nums_or_var_to_int_ne_list (List.hd l) (List.tl l)) + | ((false,[]), qid) -> xlate_error "Unused" ;; let xlate_with_names = function @@ -732,7 +741,8 @@ and xlate_red_tactic = | CbvVm -> CT_cbvvm | Hnf -> CT_hnf | Simpl None -> CT_simpl ctv_PATTERN_OPT_NONE - | Simpl (Some (l,c)) -> + | Simpl (Some (occs,c)) -> + let l = nums_of_occs occs in CT_simpl (CT_coerce_PATTERN_to_PATTERN_OPT (CT_pattern_occ @@ -751,9 +761,9 @@ and xlate_red_tactic = | Fold formula_list -> CT_fold(CT_formula_list(List.map xlate_formula formula_list)) | Pattern l -> - let pat_list = List.map (fun (nums,c) -> + let pat_list = List.map (fun (occs,c) -> CT_pattern_occ - (CT_int_list (nums_or_var_to_int_list_aux nums), + (CT_int_list (nums_or_var_to_int_list_aux (nums_of_occs occs)), xlate_formula c)) l in (match pat_list with | first :: others -> CT_pattern (CT_pattern_ne_list (first, others)) @@ -907,6 +917,7 @@ and xlate_tac = | TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b) | TacChange (Some(l,c), f, b) -> (* TODO LATER: combine with other constructions of pattern_occ *) + let l = nums_of_occs l in CT_change_local( CT_pattern_occ(CT_int_list(nums_or_var_to_int_list_aux l), xlate_formula c), @@ -1151,8 +1162,9 @@ and xlate_tac = | TacSpecialize (nopt, (c,sl)) -> CT_specialize (xlate_int_opt nopt, xlate_formula c, xlate_bindings sl) | TacGeneralize [] -> xlate_error "" - | TacGeneralize ((([],first),Anonymous) :: cl) - when List.for_all (fun ((o,_),na) -> o = [] & na = Anonymous) cl -> + | TacGeneralize ((((true,[]),first),Anonymous) :: cl) + when List.for_all (fun ((o,_),na) -> o = all_occurrences_expr + & na = Anonymous) cl -> CT_generalize (CT_formula_ne_list (xlate_formula first, List.map (fun ((_,c),_) -> xlate_formula c) cl)) diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index b96b57d5b..0bb18b3b0 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -133,7 +133,7 @@ let exists_tac c = constructor_tac false (Some 1) 1 (Rawterm.ImplicitBindings [c let generalize_tac t = generalize_time (generalize t) let elim t = elim_time (simplest_elim t) let exact t = exact_time (Tactics.refine t) -let unfold s = Tactics.unfold_in_concl [[], Lazy.force s] +let unfold s = Tactics.unfold_in_concl [all_occurrences, Lazy.force s] let rev_assoc k = let rec loop = function diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 66246faf5..92f74d1d9 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -826,9 +826,11 @@ let raw_polynom th op lc gl = c'''i; ci; c'i_eq_c''i |])))) (tclTHENS (tclORELSE - (Setoid_replace.general_s_rewrite true [] c'i_eq_c''i + (Setoid_replace.general_s_rewrite true + Termops.all_occurrences c'i_eq_c''i ~new_goals:[]) - (Setoid_replace.general_s_rewrite false [] c'i_eq_c''i + (Setoid_replace.general_s_rewrite false + Termops.all_occurrences c'i_eq_c''i ~new_goals:[])) [tac])) else diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index c3caa403e..474b3616a 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -104,7 +104,8 @@ let protect_tac map = Tactics.reduct_option (protect_red map,DEFAULTcast) None ;; let protect_tac_in map id = - Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(([],id),InHyp));; + Tactics.reduct_option (protect_red map,DEFAULTcast) + (Some((all_occurrences_expr,id),InHyp));; TACTIC EXTEND protect_fv diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 1c4fa7e1f..b464a9622 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -127,7 +127,9 @@ \newcommand{\ifitem}{\nterm{dep\_ret\_type}} \newcommand{\convclause}{\nterm{conversion\_clause}} \newcommand{\occclause}{\nterm{occurrence\_clause}} -\newcommand{\occset}{\nterm{occurrence\_set}} +\newcommand{\occgoalset}{\nterm{goal\_occurrences}} +\newcommand{\atoccurrences}{\nterm{at\_occurrences}} +\newcommand{\occlist}{\nterm{occurrences}} \newcommand{\params}{\nterm{params}} % vernac \newcommand{\returntype}{\nterm{return\_type}} \newcommand{\idparams}{\nterm{ident\_with\_params}} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 9589963fe..f71d66319 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -447,10 +447,10 @@ replacement only in the conclusion. \begin{Variants} -\item {\tt set (} {\ident} {\tt :=} {\term} {\tt ) in {\occset}} +\item {\tt set (} {\ident} {\tt :=} {\term} {\tt ) in {\occgoalset}} This notation allows to specify which occurrences of {\term} have to -be substituted in the context. The {\tt in {\occset}} clause is an +be substituted in the context. The {\tt in {\occgoalset}} clause is an occurrence clause whose syntax and behavior is described in Section~\ref{Occurrences clauses}. @@ -465,8 +465,8 @@ Section~\ref{Occurrences clauses}. is generated by {\Coq}. This variant also supports an occurrence clause. \item {\tt set (} {\ident$_0$} \nelist{\binder}{} {\tt :=} {\term} - {\tt ) in {\occset}}\\ - {\tt set {\term} in {\occset}} + {\tt ) in {\occgoalset}}\\ + {\tt set {\term} in {\occgoalset}} These are the general forms which combine the previous possibilities. @@ -475,7 +475,7 @@ Section~\ref{Occurrences clauses}. This behaves as {\tt set (} {\ident} := {\term} {\tt ) in *} and using a logical (Leibniz's) equality instead of a local definition. -\item {\tt remember {\term} {\tt as} {\ident} in {\occset}} +\item {\tt remember {\term} {\tt as} {\ident} in {\occgoalset}} This is a more general form of {\tt remember} that remembers the occurrences of {\term} specified by an occurrences set. @@ -900,18 +900,18 @@ An occurrences clause is a modifier to some tactics that obeys the following syntax: $\!\!\!$\begin{tabular}{lcl} -{\occclause} & ::= & {\tt in} {\occset} \\ -{\occset} & ::= & - \zeroone{{\ident$_1$} \zeroone{{\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}} {\tt ,} {\dots} {\tt ,} - {\ident$_m$} \zeroone{{\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$}}}\\ -& & - \zeroone{{\tt |-} - \zeroone{{\tt *} \zeroone{{\tt at} {\num$'_1$} \dots\ {\num$'_n$}}}}\\ +{\occclause} & ::= & {\tt in} {\occgoalset} \\ +{\occgoalset} & ::= & + \zeroone{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\ +& & {\dots} {\tt ,}\\ +& & {\ident$_m$} \zeroone{\atoccurrences}}\\ +& & \zeroone{{\tt |-} \zeroone{{\tt *} \zeroone{\atoccurrences}}}\\ & | & - {\tt *} {\tt |-} - \zeroone{{\tt *} \zeroone{{\tt at} {\num$'_1$} \dots\ {\num$'_n$}}}\\ + {\tt *} {\tt |-} \zeroone{{\tt *} \zeroone{\atoccurrences}}\\ & | & {\tt *}\\ +{\atoccurrences} & ::= & {\tt at} {\occlist}\\ +{\occlist} & ::= & \zeroone{\tt -} {\num$_1$} \dots\ {\num$_n$} \end{tabular} The role of an occurrence clause is to select a set of occurrences of @@ -927,10 +927,13 @@ particular, occurrences of {\term} in implicit arguments (see Section~\ref{Implicit Arguments}) or coercions (see Section~\ref{Coercions}) are counted. -A negative occurrence number means an occurrence which should not be -substituted. As an exception to the left-to-right order, the -occurrences in the {\tt return} subexpression of a {\tt match} are -considered {\em before} the occurrences in the matched term. +If a minus sign is given between {\tt at} and the list of occurrences, +it negates the condition so that the clause denotes all the occurrences except +the ones explicitly mentioned after the minus sign. + +As an exception to the left-to-right order, the occurrences in the +{\tt return} subexpression of a {\tt match} are considered {\em +before} the occurrences in the matched term. In the second case, the {\tt *} on the left of {\tt |-} means that all occurrences of {\term} are selected in every hypothesis. @@ -1290,10 +1293,16 @@ x}$)$) $t$}. This command can be used, for instance, when the tactic \begin{Variants} \item {\tt pattern {\term} at {\num$_1$} \dots\ {\num$_n$}} - Only the occurrences {\num$_1$} \dots\ {\num$_n$} of {\term} will be + Only the occurrences {\num$_1$} \dots\ {\num$_n$} of {\term} are considered for $\beta$-expansion. Occurrences are located from left to right. +\item {\tt pattern {\term} at - {\num$_1$} \dots\ {\num$_n$}} + + All occurrences except the occurrences of indexes {\num$_1$} \dots\ + {\num$_n$} of {\term} are considered for + $\beta$-expansion. Occurrences are located from left to right. + \item {\tt pattern {\term$_1$}, \dots, {\term$_m$}} Starting from a goal $\phi(t_1 \dots\ t_m)$, the tactic @@ -1310,6 +1319,11 @@ x}$)$) $t$}. This command can be used, for instance, when the tactic \dots, \num$_i^1$ of \term$_1$, \dots, \num$_1^m$, \dots, \num$_j^m$ of \term$_m$ starting from \term$_m$. +\item {\tt pattern} {\term$_1$} \zeroone{{\tt at \zeroone{-}} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}} {\tt ,} \dots {\tt ,} + {\term$_m$} \zeroone{{\tt at \zeroone{-}} {\num$_1^m$} \dots\ {\num$_{n_m}^m$}} + + This is the most general syntax that combines the different variants. + \end{Variants} \subsection{Conversion tactics applied to hypotheses} @@ -1524,10 +1538,10 @@ induction n. This syntax tells to keep an equation between {\term} and the value it gets in each case of the induction. -\item \texttt{induction {\term} in {\occset}} +\item \texttt{induction {\term} in {\occgoalset}} This syntax is used for selecting which occurrences of {\term} the - induction has to be carried on. The {\tt in {\occset}} clause is an + induction has to be carried on. The {\tt in {\atoccurrences}} clause is an occurrence clause whose syntax and behavior is described in Section~\ref{Occurrences clause}. @@ -1535,8 +1549,8 @@ induction n. the value it gets in each case of the induction is added to the context of the subgoals corresponding to the induction cases. -\item{\tt induction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}}\\ - {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}} +\item{\tt induction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\ + {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}} This is the most general form of {\tt induction} and {\tt einduction}. It combines the effects of the {\tt with}, {\tt as}, @@ -1700,10 +1714,10 @@ last introduced hypothesis. This syntax tells to keep an equation between {\term} and the value it gets in each cases of the analysis. -\item \texttt{destruct {\term} in {\occset}} +\item \texttt{destruct {\term} in {\occgoalset}} This syntax is used for selecting which occurrences of {\term} the - case analysis has to be done on. The {\tt in {\occset}} clause is an + case analysis has to be done on. The {\tt in {\occgoalset}} clause is an occurrence clause whose syntax and behavior is described in Section~\ref{Occurrences clauses}. @@ -1711,8 +1725,8 @@ last introduced hypothesis. the value it gets in each cases of the analysis is added to the context of the subgoals corresponding to the cases. -\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}}\\ - {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}} +\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\ + {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}} This is the most general form of {\tt destruct} and {\tt edestruct}. It combines the effects of the {\tt with}, {\tt as}, {\tt using}, @@ -2146,8 +2160,8 @@ This happens if \term$_1$ does not occur in the goal. \begin{itemize} \item \texttt{rewrite H in H1} will rewrites \texttt{H} in the hypothesis \texttt{H1} instead of the current goal. - \item \texttt{rewrite H in H1,H2 |- *} means \texttt{rewrite H; rewrite H in H1; - rewrite H in H2}. In particular a failure will happen if any of + \item \texttt{rewrite H in H1 at 1, H2 at - 2 |- *} means \texttt{rewrite H; rewrite H in H1 at 1; + rewrite H in H2 at - 2}. In particular a failure will happen if any of these three simpler tactics fails. \item \texttt{rewrite H in * |- } will do \texttt{rewrite H in H$_i$} for all hypothesis \texttt{H$_i$ <> H}. A success will happen @@ -2159,7 +2173,7 @@ This happens if \term$_1$ does not occur in the goal. Orientation {\tt ->} or {\tt <-} can be inserted before the term to rewrite. -\item {\tt rewrite {\term} at \textit{occurrences}} +\item {\tt rewrite {\term} at {\occlist}} \tacindex{rewrite \dots\ at} Rewrite only the given occurrences of \term$_1'$. Occurrences are diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 5ab401550..bea3929df 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -162,6 +162,10 @@ let mkCLambdaN_simple bl c = let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (constr_loc c) in mkCLambdaN_simple_loc loc bl c +let map_int_or_var f = function + | Rawterm.ArgArg x -> Rawterm.ArgArg (f x) + | Rawterm.ArgVar _ as y -> y + (* Auxiliary grammar rules *) GEXTEND Gram @@ -173,6 +177,10 @@ GEXTEND Gram [ [ n = integer -> Rawterm.ArgArg n | id = identref -> Rawterm.ArgVar id ] ] ; + nat_or_var: + [ [ n = natural -> Rawterm.ArgArg n + | id = identref -> Rawterm.ArgVar id ] ] + ; (* An identifier or a quotation meta-variable *) id_or_meta: [ [ id = identref -> AI id @@ -203,18 +211,22 @@ GEXTEND Gram ; conversion: [ [ c = constr -> (None, c) - | c1 = constr; "with"; c2 = constr -> (Some ([],c1), c2) - | c1 = constr; "at"; nl = LIST1 int_or_var; "with"; c2 = constr -> - (Some (nl,c1), c2) ] ] + | c1 = constr; "with"; c2 = constr -> (Some (all_occurrences_expr,c1),c2) + | c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr -> + (Some (occs,c1), c2) ] ] ; smart_global: [ [ c = global -> AN c | s = ne_string -> ByNotation (loc,s) ] ] ; + occs_nums: + [ [ nl = LIST1 nat_or_var -> no_occurrences_expr_but nl + | "-"; n = nat_or_var; nl = LIST0 int_or_var -> + (* have used int_or_var instead of nat_or_var for compatibility *) + all_occurrences_expr_but (List.map (map_int_or_var abs) (n::nl)) ] ] + ; occs: - [ [ "at"; nl = LIST1 integer -> List.map (fun x -> Rawterm.ArgArg x) nl - | "at"; id = identref -> [Rawterm.ArgVar id] - | -> [] ] ] + [ [ "at"; occs = occs_nums -> occs | -> all_occurrences_expr_but [] ] ] ; pattern_occ: [ [ c = constr; nl = occs -> (nl,c) ] ] @@ -323,29 +335,29 @@ GEXTEND Gram ; in_clause: [ [ "*"; occs=occs -> - {onhyps=None; onconcl=true; concl_occs=occs} - | "*"; "|-"; (b,occs)=concl_occ -> - {onhyps=None; onconcl=b; concl_occs=occs} - | hl=LIST0 hypident_occ SEP","; "|-"; (b,occs)=concl_occ -> - {onhyps=Some hl; onconcl=b; concl_occs=occs} + {onhyps=None; concl_occs=occs} + | "*"; "|-"; occs=concl_occ -> + {onhyps=None; concl_occs=occs} + | hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ -> + {onhyps=Some hl; concl_occs=occs} | hl=LIST0 hypident_occ SEP"," -> - {onhyps=Some hl; onconcl=false; concl_occs=[]} ] ] + {onhyps=Some hl; concl_occs=no_occurrences_expr} ] ] ; clause_dft_concl: [ [ "in"; cl = in_clause -> cl - | occs=occs -> {onhyps=Some[]; onconcl=true; concl_occs=occs} - | -> {onhyps=Some[]; onconcl=true; concl_occs=[]} ] ] + | occs=occs -> {onhyps=Some[]; concl_occs=occs} + | -> {onhyps=Some[]; concl_occs=all_occurrences_expr} ] ] ; clause_dft_all: [ [ "in"; cl = in_clause -> cl - | -> {onhyps=None; onconcl=true; concl_occs=[]} ] ] + | -> {onhyps=None; concl_occs=all_occurrences_expr} ] ] ; opt_clause: [ [ "in"; cl = in_clause -> Some cl | -> None ] ] ; concl_occ: - [ [ "*"; occs = occs -> (true,occs) - | -> (false, []) ] ] + [ [ "*"; occs = occs -> occs + | -> no_occurrences_expr ] ] ; simple_clause: [ [ "in"; idl = LIST1 id_or_meta -> idl @@ -493,9 +505,10 @@ GEXTEND Gram | IDENT "cut"; c = constr -> TacCut c | IDENT "generalize"; c = constr -> - TacGeneralize [(([],c),Names.Anonymous)] + TacGeneralize [((all_occurrences_expr,c),Names.Anonymous)] | IDENT "generalize"; c = constr; l = LIST1 constr -> - TacGeneralize (List.map (fun c -> (([],c),Names.Anonymous)) (c::l)) + let gen_everywhere c = ((all_occurrences_expr,c),Names.Anonymous) in + TacGeneralize (List.map gen_everywhere (c::l)) | IDENT "generalize"; c = constr; lookup_at_as_coma; nl = occs; na = as_name; l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] -> diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 0f0c38adc..04b700236 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -674,10 +674,16 @@ let pr_cases_pattern_expr = pr_patt ltop let pr_binders = pr_undelimited_binders (pr ltop) -let pr_with_occurrences pr = function - ([],c) -> pr c - | (nl,c) -> hov 1 (pr c ++ spc() ++ str"at " ++ - hov 0 (prlist_with_sep spc (pr_or_var int) nl)) +let pr_with_occurrences_with_trailer pr occs trailer = + match occs with + ((false,[]),c) -> pr c ++ trailer + | ((nowhere_except_in,nl),c) -> + hov 1 (pr c ++ spc() ++ str"at " ++ + (if nowhere_except_in then mt() else str "- ") ++ + hov 0 (prlist_with_sep spc (pr_or_var int) nl) ++ trailer) + +let pr_with_occurrences pr occs = + pr_with_occurrences_with_trailer pr occs (mt()) let pr_red_flag pr r = (if r.rBeta then pr_arg str "beta" else mt ()) ++ diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index f351144dc..83339ee2f 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -55,6 +55,8 @@ val pr_qualid : qualid -> std_ppcmds val pr_with_occurrences : ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds +val pr_with_occurrences_with_trailer : + ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds -> std_ppcmds val pr_red_expr : ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) -> ('a,'b) red_expr_gen -> std_ppcmds diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index c0dbc0eff..e59df48aa 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -417,14 +417,14 @@ let pr_simple_clause pr_id = function | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l) let pr_clauses pr_id = function - { onhyps=None; onconcl=true; concl_occs=nl } -> - pr_in (pr_with_occurrences (fun () -> str " *") (nl,())) - | { onhyps=None; onconcl=false } -> pr_in (str " * |-") - | { onhyps=Some l; onconcl=true; concl_occs=nl } -> - pr_in (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l - ++ pr_with_occurrences (fun () -> str" |- *") (nl,())) - | { onhyps=Some l; onconcl=false } -> - pr_in (prlist_with_sep (fun()->str",") (pr_hyp_location pr_id) l) + | { onhyps=None; concl_occs=occs } -> + if occs = no_occurrences_expr then pr_in (str " * |-") + else pr_in (pr_with_occurrences (fun () -> str " *") (occs,())) + | { onhyps=Some l; concl_occs=occs } -> + pr_in + (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l ++ + (if occs = no_occurrences_expr then mt () + else pr_with_occurrences (fun () -> str" |- *") (occs,()))) let pr_clause_pattern pr_id = function | (None, []) -> mt () @@ -829,12 +829,9 @@ and pr_atom1 = function hov 1 (str "change" ++ brk (1,1) ++ (match occ with None -> mt() - | Some([],c1) -> hov 1 (pr_constr c1 ++ spc() ++ str "with ") - | Some(ocl,c1) -> - hov 1 (pr_constr c1 ++ spc() ++ - str "at " ++ prlist_with_sep spc (pr_or_var int) ocl) ++ - spc() ++ - str "with ") ++ + | Some occlc -> + pr_with_occurrences_with_trailer pr_constr occlc + (spc () ++ str "with ")) ++ pr_constr c ++ pr_clauses pr_ident h) (* Equivalence relations *) diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 5c31fcee6..4b52772b5 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -95,7 +95,9 @@ let mlexpr_of_or_var f = function let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident) -let mlexpr_of_occs = mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) +let mlexpr_of_occs = + mlexpr_of_pair + mlexpr_of_bool (mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int)) let mlexpr_of_occurrences f = mlexpr_of_pair mlexpr_of_occs f @@ -111,7 +113,6 @@ let mlexpr_of_clause cl = <:expr< {Tacexpr.onhyps= $mlexpr_of_option (mlexpr_of_list mlexpr_of_hyp_location) cl.Tacexpr.onhyps$; - Tacexpr.onconcl= $mlexpr_of_bool cl.Tacexpr.onconcl$; Tacexpr.concl_occs= $mlexpr_of_occs cl.Tacexpr.concl_occs$} >> let mlexpr_of_red_flags { @@ -165,8 +166,7 @@ let rec mlexpr_of_constr = function | _ -> failwith "mlexpr_of_constr: TODO" let mlexpr_of_occ_constr = - mlexpr_of_pair (mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int)) - mlexpr_of_constr + mlexpr_of_occurrences mlexpr_of_constr let mlexpr_of_red_expr = function | Rawterm.Red b -> <:expr< Rawterm.Red $mlexpr_of_bool b$ >> @@ -177,9 +177,8 @@ let mlexpr_of_red_expr = function | Rawterm.Lazy f -> <:expr< Rawterm.Lazy $mlexpr_of_red_flags f$ >> | Rawterm.Unfold l -> - let f1 = mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) in - let f2 = mlexpr_of_by_notation mlexpr_of_reference in - let f = mlexpr_of_list (mlexpr_of_pair f1 f2) in + let f1 = mlexpr_of_by_notation mlexpr_of_reference in + let f = mlexpr_of_list (mlexpr_of_occurrences f1) in <:expr< Rawterm.Unfold $f l$ >> | Rawterm.Fold l -> <:expr< Rawterm.Fold $mlexpr_of_list mlexpr_of_constr l$ >> diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index fe48cd4fa..79708e9fb 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -335,7 +335,14 @@ let all_flags = type 'a or_var = ArgArg of 'a | ArgVar of identifier located -type 'a with_occurrences = int or_var list * 'a +type occurrences_expr = bool * int or_var list + +let all_occurrences_expr_but l = (false,l) +let no_occurrences_expr_but l = (true,l) +let all_occurrences_expr = (false,[]) +let no_occurrences_expr = (true,[]) + +type 'a with_occurrences = occurrences_expr * 'a type ('a,'b) red_expr_gen = | Red of bool diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index ab67a0922..0eee3e73a 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -146,7 +146,14 @@ val all_flags : 'a raw_red_flag type 'a or_var = ArgArg of 'a | ArgVar of identifier located -type 'a with_occurrences = int or_var list * 'a +type occurrences_expr = bool * int or_var list + +val all_occurrences_expr_but : int or_var list -> occurrences_expr +val no_occurrences_expr_but : int or_var list -> occurrences_expr +val all_occurrences_expr : occurrences_expr +val no_occurrences_expr : occurrences_expr + +type 'a with_occurrences = occurrences_expr * 'a type ('a,'b) red_expr_gen = | Red of bool diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 05d108673..47bc132ac 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -35,16 +35,23 @@ exception ReductionTacticError of reduction_tactic_error exception Elimconst exception Redelimination -let is_evaluable env ref = - match ref with - EvalConstRef kn -> - is_transparent (ConstKey kn) && - let cb = Environ.lookup_constant kn env in - cb.const_body <> None & not cb.const_opaque - | EvalVarRef id -> - is_transparent (VarKey id) && - let (_,value,_) = Environ.lookup_named id env in - value <> None +let is_evaluable env = function + | EvalConstRef kn -> + is_transparent (ConstKey kn) && + let cb = Environ.lookup_constant kn env in + cb.const_body <> None & not cb.const_opaque + | EvalVarRef id -> + is_transparent (VarKey id) && + let (_,value,_) = Environ.lookup_named id env in + value <> None + +let value_of_evaluable_ref env = function + | EvalConstRef con -> constant_value env con + | EvalVarRef id -> Option.get (pi2 (lookup_named id env)) + +let constr_of_evaluable_ref = function + | EvalConstRef con -> mkConst con + | EvalVarRef id -> mkVar id type evaluable_reference = | EvalConst of constant @@ -627,20 +634,16 @@ let is_head c t = | App (f,_) -> f = c | _ -> false -let contextually byhead (locs,c) f env sigma t = +let contextually byhead ((nowhere_except_in,locs),c) f env sigma t = let maxocc = List.fold_right max locs 0 in let pos = ref 1 in - let except = List.exists (fun n -> n<0) locs in - if except & (List.exists (fun n -> n>=0) locs) - then error "mixing of positive and negative occurences" - else - let rec traverse (env,c as envc) t = - if locs <> [] & (not except) & (!pos > maxocc) then t + let rec traverse (env,c as envc) t = + if nowhere_except_in & (!pos > maxocc) then t else if (not byhead & eq_constr c t) or (byhead & is_head c t) then let ok = - if except then not (List.mem (- !pos) locs) - else (locs = [] or List.mem !pos locs) in + if nowhere_except_in then List.mem !pos locs + else not (List.mem !pos locs) in incr pos; if ok then f env sigma t @@ -656,112 +659,34 @@ let contextually byhead (locs,c) f env sigma t = traverse envc t in let t' = traverse (env,c) t in - if locs <> [] & List.exists (fun o -> o >= !pos or o <= - !pos) locs then - error_invalid_occurrence locs; + if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs; t' (* linear bindings (following pretty-printer) of the value of name in c. * n is the number of the next occurence of name. * ol is the occurence list to find. *) -let rec substlin env name n ol c = - match kind_of_term c with - | Const kn when EvalConstRef kn = name -> - if List.hd ol = n then - try - (n+1, List.tl ol, constant_value env kn) - with - NotEvaluableConst _ -> - errorlabstrm "substlin" - (pr_con kn ++ str " is not a defined constant") - else - ((n+1), ol, c) - - | Var id when EvalVarRef id = name -> - if List.hd ol = n then - match lookup_named id env with - | (_,Some c,_) -> (n+1, List.tl ol, c) - | _ -> - errorlabstrm "substlin" - (pr_id id ++ str " is not a defined constant") - else - ((n+1), ol, c) - - (* INEFFICIENT: OPTIMIZE *) - | App (c1,cl) -> - Array.fold_left - (fun (n1,ol1,c1') c2 -> - (match ol1 with - | [] -> (n1,[],applist(c1',[c2])) - | _ -> - let (n2,ol2,c2') = substlin env name n1 ol1 c2 in - (n2,ol2,applist(c1',[c2'])))) - (substlin env name n ol c1) cl - - | Lambda (na,c1,c2) -> - let (n1,ol1,c1') = substlin env name n ol c1 in - (match ol1 with - | [] -> (n1,[],mkLambda (na,c1',c2)) - | _ -> - let (n2,ol2,c2') = substlin env name n1 ol1 c2 in - (n2,ol2,mkLambda (na,c1',c2'))) - - | LetIn (na,c1,t,c2) -> - let (n1,ol1,c1') = substlin env name n ol c1 in - (match ol1 with - | [] -> (n1,[],mkLetIn (na,c1',t,c2)) - | _ -> - let (n2,ol2,c2') = substlin env name n1 ol1 c2 in - (n2,ol2,mkLetIn (na,c1',t,c2'))) - - | Prod (na,c1,c2) -> - let (n1,ol1,c1') = substlin env name n ol c1 in - (match ol1 with - | [] -> (n1,[],mkProd (na,c1',c2)) - | _ -> - let (n2,ol2,c2') = substlin env name n1 ol1 c2 in - (n2,ol2,mkProd (na,c1',c2'))) - - | Case (ci,p,d,llf) -> - let rec substlist nn oll = function - | [] -> (nn,oll,[]) - | f::lfe -> - let (nn1,oll1,f') = substlin env name nn oll f in - (match oll1 with - | [] -> (nn1,[],f'::lfe) - | _ -> - let (nn2,oll2,lfe') = substlist nn1 oll1 lfe in - (nn2,oll2,f'::lfe')) - in - (* p is printed after d in v8 syntax *) - let (n1,ol1,d') = substlin env name n ol d in - (match ol1 with - | [] -> (n1,[],mkCase (ci, p, d', llf)) - | _ -> - let (n2,ol2,p') = substlin env name n1 ol1 p in - (match ol2 with - | [] -> (n2,[],mkCase (ci, p', d', llf)) - | _ -> - let (n3,ol3,lf') = substlist n2 ol2 (Array.to_list llf) - in (n3,ol3,mkCase (ci, p', d', Array.of_list lf')))) - - | Cast (c1,k,c2) -> - let (n1,ol1,c1') = substlin env name n ol c1 in - (match ol1 with - | [] -> (n1,[],mkCast (c1',k,c2)) - | _ -> - let (n2,ol2,c2') = substlin env name n1 ol1 c2 in - (n2,ol2,mkCast (c1',k,c2'))) - - | Fix _ -> - (Flags.if_verbose - warning "do not consider occurrences inside fixpoints"; (n,ol,c)) - - | CoFix _ -> - (Flags.if_verbose - warning "do not consider occurrences inside cofixpoints"; (n,ol,c)) - | (Rel _|Meta _|Var _|Sort _ - |Evar _|Const _|Ind _|Construct _) -> (n,ol,c) +let substlin env evalref n (nowhere_except_in,locs) c = + let maxocc = List.fold_right max locs 0 in + let pos = ref n in + assert (List.for_all (fun x -> x >= 0) locs); + let value = value_of_evaluable_ref env evalref in + let term = constr_of_evaluable_ref evalref in + let rec substrec () c = + if nowhere_except_in & !pos > maxocc then c + else if c = term then + let ok = + if nowhere_except_in then List.mem !pos locs + else not (List.mem !pos locs) in + incr pos; + if ok then value else c + else + map_constr_with_binders_left_to_right + (fun _ () -> ()) + substrec () c + in + let t' = substrec () c in + (!pos, t') let string_of_evaluable_ref env = function | EvalVarRef id -> string_of_id id @@ -779,16 +704,15 @@ let unfold env sigma name = * Unfolds the constant name in a term c following a list of occurrences occl. * at the occurrences of occ_list. If occ_list is empty, unfold all occurences. * Performs a betaiota reduction after unfolding. *) -let unfoldoccs env sigma (occl,name) c = - match occl with - | [] -> unfold env sigma name c - | l -> - match substlin env name 1 (Sort.list (<) l) c with - | (_,[],uc) -> nf_betaiota uc - | (1,_,_) -> - error ((string_of_evaluable_ref env name)^" does not occur") - | (_,l,_) -> - error_invalid_occurrence l +let unfoldoccs env sigma ((nowhere_except_in,locs as plocs),name) c = + if locs = [] then if nowhere_except_in then c else unfold env sigma name c + else + let (nbocc,uc) = substlin env name 1 plocs c in + if nbocc = 1 then + error ((string_of_evaluable_ref env name)^" does not occur"); + let rest = List.filter (fun o -> o >= nbocc) locs in + if rest <> [] then error_invalid_occurrence rest; + nf_betaiota uc (* Unfold reduction tactic: *) let unfoldn loccname env sigma c = diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 0ff5154f6..1516a2bd6 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -16,6 +16,7 @@ open Evd open Reductionops open Closure open Rawterm +open Termops (*i*) type reduction_tactic_error = @@ -47,13 +48,13 @@ val hnf_constr : reduction_function (* Unfold *) val unfoldn : - (int list * evaluable_global_reference) list -> reduction_function + (occurrences * evaluable_global_reference) list -> reduction_function (* Fold *) val fold_commands : constr list -> reduction_function (* Pattern *) -val pattern_occs : (int list * constr) list -> reduction_function +val pattern_occs : (occurrences * constr) list -> reduction_function (* Rem: Lazy strategies are defined in Reduction *) (* Call by value strategy (uses Closures) *) @@ -81,7 +82,7 @@ val reduce_to_quantified_ref : val reduce_to_atomic_ref : env -> evar_map -> Libnames.global_reference -> types -> types -val contextually : bool -> int list * constr -> reduction_function +val contextually : bool -> occurrences * constr -> reduction_function -> reduction_function (* Compatibility *) diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 9a9e25c59..aa6c37491 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -621,32 +621,33 @@ let subst_term = subst_term_gen eq_constr let replace_term = replace_term_gen eq_constr -(* Substitute only a list of locations locs, the empty list is - interpreted as substitute all, if 0 is in the list then no - bindings is done. The list may contain only negative occurrences - that will not be substituted. *) +(* Substitute only at a list of locations or excluding a list of + locations; in the occurrences list (b,l), b=true means no + occurrence except the ones in l and b=false, means all occurrences + except the ones in l *) + +type occurrences = bool * int list +let all_occurrences = (false,[]) +let no_occurrences_in_set = (true,[]) let error_invalid_occurrence l = errorlabstrm "" (str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++ prlist_with_sep spc int l) -let subst_term_occ_gen locs occ c t = +let subst_term_occ_gen (nowhere_except_in,locs) occ c t = let maxocc = List.fold_right max locs 0 in let pos = ref occ in - let except = List.exists (fun n -> n<0) locs in - if except & (List.exists (fun n -> n>=0) locs) - then error "mixing of positive and negative occurences" - else - let rec substrec (k,c as kc) t = - if (not except) & (!pos > maxocc) then t + assert (List.for_all (fun x -> x >= 0) locs); + let rec substrec (k,c as kc) t = + if nowhere_except_in & !pos > maxocc then t else if eq_constr c t then let r = - if except then - if List.mem (- !pos) locs then t else (mkRel k) - else + if nowhere_except_in then if List.mem !pos locs then (mkRel k) else t + else + if List.mem !pos locs then t else (mkRel k) in incr pos; r else map_constr_with_binders_left_to_right @@ -656,28 +657,27 @@ let subst_term_occ_gen locs occ c t = let t' = substrec (1,c) t in (!pos, t') -let subst_term_occ locs c t = - if locs = [] then subst_term c t - else if List.mem 0 locs then - t +let subst_term_occ (nowhere_except_in,locs as plocs) c t = + if locs = [] then if nowhere_except_in then t else subst_term c t else - let (nbocc,t') = subst_term_occ_gen locs 1 c t in - let rest = List.filter (fun o -> o >= nbocc or o <= -nbocc) locs in + let (nbocc,t') = subst_term_occ_gen plocs 1 c t in + let rest = List.filter (fun o -> o >= nbocc) locs in if rest <> [] then error_invalid_occurrence rest; t' -let subst_term_occ_decl locs c (id,bodyopt,typ as d) = +let subst_term_occ_decl (nowhere_except_in,locs as plocs) c (id,bodyopt,typ as d) = match bodyopt with - | None -> (id,None,subst_term_occ locs c typ) + | None -> (id,None,subst_term_occ plocs c typ) | Some body -> if locs = [] then - (id,Some (subst_term c body),subst_term c typ) - else if List.mem 0 locs then - d + if nowhere_except_in then + (id,Some (subst_term c body),subst_term c typ) + else + d else - let (nbocc,body') = subst_term_occ_gen locs 1 c body in - let (nbocc',t') = subst_term_occ_gen locs nbocc c typ in - let rest = List.filter (fun o -> o >= nbocc' or o <= -nbocc') locs in + let (nbocc,body') = subst_term_occ_gen plocs 1 c body in + let (nbocc',t') = subst_term_occ_gen plocs nbocc c typ in + let rest = List.filter (fun o -> o >= nbocc') locs in if rest <> [] then error_invalid_occurrence rest; (id,Some body',t') diff --git a/pretyping/termops.mli b/pretyping/termops.mli index bc483cfc3..f80deab10 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -131,18 +131,24 @@ val subst_term : constr -> constr -> constr (* [replace_term d e c] replaces [d] by [e] in [c] *) val replace_term : constr -> constr -> constr -> constr +(* In occurrences sets, false = everywhere except and true = nowhere except *) +type occurrences = bool * int list +val all_occurrences : occurrences +val no_occurrences_in_set : occurrences + (* [subst_term_occ_gen occl n c d] replaces occurrences of [c] at positions [occl], counting from [n], by [Rel 1] in [d] *) -val subst_term_occ_gen : int list -> int -> constr -> types -> int * types +val subst_term_occ_gen : + occurrences -> int -> constr -> types -> int * types (* [subst_term_occ occl c d] replaces occurrences of [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC) *) -val subst_term_occ : int list -> constr -> constr -> constr +val subst_term_occ : occurrences -> constr -> constr -> constr (* [subst_term_occ_decl occl c decl] replaces occurrences of [c] at positions [occl] by [Rel 1] in [decl] *) val subst_term_occ_decl : - int list -> constr -> named_declaration -> named_declaration + occurrences -> constr -> named_declaration -> named_declaration val error_invalid_occurrence : int list -> 'a diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ca1be55bb..41d6ff4c1 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -44,7 +44,8 @@ let abstract_scheme env c l lname_typ = let abstract_list_all env evd typ c l = let ctxt,_ = decomp_n_prod env (evars_of evd) (List.length l) typ in - let p = abstract_scheme env c (List.map (function a -> [],a) l) ctxt in + let l_with_all_occs = List.map (function a -> (all_occurrences,a)) l in + let p = abstract_scheme env c l_with_all_occs ctxt in try if is_conv_leq env (evars_of evd) (Typing.mtype_of env evd p) typ then p else error "abstract_list_all" diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 27db71755..71e7cdc21 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -154,8 +154,8 @@ let out_arg = function | ArgVar _ -> anomaly "Unevaluated or_var variable" | ArgArg x -> x -let out_with_occurrences (l,c) = - (List.map out_arg l, c) +let out_with_occurrences ((b,l),c) = + ((b,List.map out_arg l), c) let reduction_of_red_expr = function | Red internal -> diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index 68c1fd669..70db56c48 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -13,11 +13,12 @@ open Term open Closure open Rawterm open Reductionops +open Termops type red_expr = (constr, evaluable_global_reference) red_expr_gen -val out_with_occurrences : 'a with_occurrences -> int list * 'a +val out_with_occurrences : 'a with_occurrences -> occurrences * 'a val reduction_of_red_expr : red_expr -> reduction_function * cast_kind (* [true] if we should use the vm to verify the reduction *) diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index d0b015552..17961fd42 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -94,15 +94,17 @@ type 'id gsimple_clause = ('id raw_hyp_location) option [Some l] means on hypothesis belonging to l *) type 'id gclause = { onhyps : 'id raw_hyp_location list option; - onconcl : bool; - concl_occs : int or_var list } + concl_occs : bool * int or_var list } -let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]} +let nowhere = {onhyps=Some[]; concl_occs=(false,[])} let simple_clause_of = function - { onhyps = Some[scl]; onconcl = false } -> Some scl - | { onhyps = Some []; onconcl = true; concl_occs=[] } -> None - | _ -> error "not a simple clause (one hypothesis or conclusion)" +| { onhyps = Some [scl]; concl_occs = occs } when occs = no_occurrences_expr -> + Some scl +| { onhyps = Some []; concl_occs = occs } when occs = all_occurrences_expr -> + None +| _ -> + error "not a simple clause (one hypothesis or conclusion)" type multi = | Precisely of int diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 6b6305a17..2b007112f 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -79,7 +79,7 @@ val pf_nf_betaiota : goal sigma -> constr -> constr val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types val pf_reduce_to_atomic_ind : goal sigma -> types -> inductive * types val pf_compute : goal sigma -> constr -> constr -val pf_unfoldn : (int list * evaluable_global_reference) list +val pf_unfoldn : (Termops.occurrences * evaluable_global_reference) list -> goal sigma -> constr -> constr val pf_const_value : goal sigma -> constant -> constr diff --git a/tactics/auto.ml b/tactics/auto.ml index e41bebea1..a4933a896 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -677,7 +677,7 @@ and my_find_search_nodelta db_list local_db hdc concl = tclTHEN (unify_resolve_nodelta (term,cl)) (trivial_fail_db false db_list local_db) - | Unfold_nth c -> unfold_in_concl [[],c] + | Unfold_nth c -> unfold_in_concl [all_occurrences,c] | Extern tacast -> conclPattern concl (Option.get p) tacast)) tacl @@ -717,7 +717,7 @@ and my_find_search_delta db_list local_db hdc concl = tclTHEN (unify_resolve st (term,cl)) (trivial_fail_db true db_list local_db) - | Unfold_nth c -> unfold_in_concl [[],c] + | Unfold_nth c -> unfold_in_concl [all_occurrences,c] | Extern tacast -> conclPattern concl (Option.get p) tacast)) tacl diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index e3e90c7ca..3be1e45de 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -17,7 +17,9 @@ open Tacticals open Tacinterp open Tactics open Term +open Termops open Util +open Rawterm open Vernacinterp open Tacexpr open Mod_subst @@ -80,7 +82,10 @@ let one_base general_rewrite_maybe_in tac_main bas = let autorewrite tac_main lbas = tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac bas -> - tclTHEN tac (one_base (fun dir -> general_rewrite dir []) tac_main bas)) tclIDTAC lbas)) + tclTHEN tac + (one_base (fun dir -> general_rewrite dir all_occurrences) + tac_main bas)) + tclIDTAC lbas)) let autorewrite_multi_in idl tac_main lbas : tactic = fun gl -> @@ -96,7 +101,7 @@ let autorewrite_multi_in idl tac_main lbas : tactic = | _ -> (* even the hypothesis id is missing *) error ("No such hypothesis : " ^ (string_of_id !id)) in - let gl' = general_rewrite_in dir [] !id cstr false gl in + let gl' = general_rewrite_in dir all_occurrences !id cstr false gl in let gls = (fst gl').Evd.it in match gls with g::_ -> @@ -132,7 +137,9 @@ let gen_auto_multi_rewrite tac_main lbas cl = let try_do_hyps treat_id l = autorewrite_multi_in (List.map treat_id l) tac_main lbas in - if cl.concl_occs <> [] then + if cl.concl_occs <> all_occurrences_expr & + cl.concl_occs <> no_occurrences_expr + then error "The \"at\" syntax isn't available yet for the autorewrite tactic" else let compose_tac t1 t2 = @@ -141,7 +148,7 @@ let gen_auto_multi_rewrite tac_main lbas cl = | _ -> tclTHENFIRST t1 t2 in compose_tac - (if cl.onconcl then autorewrite tac_main lbas else tclIDTAC) + (if cl.concl_occs <> no_occurrences_expr then autorewrite tac_main lbas else tclIDTAC) (match cl.onhyps with | Some l -> try_do_hyps (fun ((_,id),_) -> id) l | None -> @@ -153,11 +160,12 @@ let gen_auto_multi_rewrite tac_main lbas cl = let auto_multi_rewrite = gen_auto_multi_rewrite Refiner.tclIDTAC -let auto_multi_rewrite_with tac_main lbas cl gl = - match cl.Tacexpr.onconcl,cl.Tacexpr.onhyps with +let auto_multi_rewrite_with tac_main lbas cl gl = + let onconcl = cl.Tacexpr.concl_occs <> no_occurrences_expr in + match onconcl,cl.Tacexpr.onhyps with | false,Some [_] | true,Some [] | false,Some [] -> (* autorewrite with .... in clause using tac n'est sur que - si clause reprensente soit le but soit UNE hypothse + si clause represente soit le but soit UNE hypothese *) gen_auto_multi_rewrite tac_main lbas cl gl | _ -> diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index bbeeb4e03..37fe7c3c8 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -125,7 +125,7 @@ and e_my_find_search db_list local_db hdc concl = | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (unify_e_resolve st (term,cl)) (e_trivial_fail_db db_list local_db) - | Unfold_nth c -> unfold_in_concl [[],c] + | Unfold_nth c -> unfold_in_concl [all_occurrences,c] | Extern tacast -> conclPattern concl (Option.get p) tacast in @@ -793,8 +793,10 @@ type rewrite_flags = { under_lambdas : bool; on_morphisms : bool } let default_flags = { under_lambdas = true; on_morphisms = true; } -let build_new gl env sigma flags occs hypinfo concl cstr evars = - let is_occ occ = occs = [] || List.mem occ occs in +let build_new gl env sigma flags loccs hypinfo concl cstr evars = + let (nowhere_except_in,occs) = loccs in + let is_occ occ = + if nowhere_except_in then List.mem occ occs else not (List.mem occ occs) in let rec aux env t occ cstr = let unif = unify_eqn env sigma hypinfo t in let occ = if unif = None then occ else succ occ in @@ -899,7 +901,11 @@ let build_new gl env sigma flags occs hypinfo concl cstr evars = Some (prf', (car', rel', c1', c2')) in res, occ | _ -> None, occ - in aux env concl 0 cstr + in + let eq,nbocc_min_1 = aux env concl 0 cstr in + let rest = List.filter (fun o -> o > nbocc_min_1) occs in + if rest <> [] then error_invalid_occurrence rest; + eq let resolve_typeclass_evars d p env evd onlyargs = let pred = @@ -924,7 +930,7 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g let evars = ref (Evd.create_evar_defs Evd.empty) in let env = pf_env gl in let sigma = project gl in - let eq, _ = build_new gl env sigma flags occs hypinfo concl (Some (Lazy.lazy_from_val cstr)) evars + let eq = build_new gl env sigma flags occs hypinfo concl (Some (Lazy.lazy_from_val cstr)) evars in match eq with | Some (p, (_, _, oldt, newt)) -> @@ -993,12 +999,19 @@ let cl_rewrite_clause c left2right occs clause gl = open Genarg open Extraargs +let occurrences_of = function + | n::_ as nl when n < 0 -> (false,List.map abs nl) + | nl -> + if List.exists (fun n -> n < 0) nl then + error "Illegal negative occurrence number"; + (true,nl) + TACTIC EXTEND class_rewrite -| [ "clrewrite" orient(o) constr(c) "in" hyp(id) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ] -| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ] -| [ "clrewrite" orient(o) constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o [] (Some (([],id), [])) ] -| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o occ None ] -| [ "clrewrite" orient(o) constr(c) ] -> [ cl_rewrite_clause c o [] None ] +| [ "clrewrite" orient(o) constr(c) "in" hyp(id) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), [])) ] +| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), [])) ] +| [ "clrewrite" orient(o) constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o all_occurrences (Some (([],id), [])) ] +| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) None ] +| [ "clrewrite" orient(o) constr(c) ] -> [ cl_rewrite_clause c o all_occurrences None ] END @@ -1008,7 +1021,7 @@ let clsubstitute o c = (fun cl -> match cl with | Some ((_,id),_) when is_tac id -> tclIDTAC - | _ -> tclTRY (cl_rewrite_clause c o [] cl)) + | _ -> tclTRY (cl_rewrite_clause c o all_occurrences cl)) TACTIC EXTEND substitute | [ "substitute" orient(o) constr(c) ] -> [ clsubstitute o c ] @@ -1098,15 +1111,15 @@ let _ = TACTIC EXTEND setoid_rewrite [ "setoid_rewrite" orient(o) constr(c) ] - -> [ cl_rewrite_clause c o [] None ] + -> [ cl_rewrite_clause c o all_occurrences None ] | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) ] -> - [ cl_rewrite_clause c o [] (Some (([],id), []))] + [ cl_rewrite_clause c o all_occurrences (Some (([],id), []))] | [ "setoid_rewrite" orient(o) constr(c) "at" occurrences(occ) ] -> - [ cl_rewrite_clause c o occ None] + [ cl_rewrite_clause c o (occurrences_of occ) None] | [ "setoid_rewrite" orient(o) constr(c) "at" occurrences(occ) "in" hyp(id)] -> - [ cl_rewrite_clause c o occ (Some (([],id), []))] + [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), []))] | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) "at" occurrences(occ)] -> - [ cl_rewrite_clause c o occ (Some (([],id), []))] + [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), []))] END (* let solve_obligation lemma = *) diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 843554bae..7d2ccbe21 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -261,11 +261,13 @@ let add_destructor_hint local na loc pat pri code = (inDD (local,na,{ d_pat = pat; d_pri=pri; d_code=code })) let match_dpat dp cls gls = + let onconcl = cls.concl_occs <> no_occurrences_expr in match (cls,dp) with - | ({onhyps=lo;onconcl=false},HypLocation(_,hypd,concld)) -> + | ({onhyps=lo},HypLocation(_,hypd,concld)) when not onconcl -> let hl = match lo with Some l -> l - | None -> List.map (fun id -> (([],id),InHyp)) (pf_ids_of_hyps gls) in + | None -> List.map (fun id -> ((all_occurrences_expr,id),InHyp)) + (pf_ids_of_hyps gls) in if not (List.for_all (fun ((_,id),hl) -> @@ -278,7 +280,7 @@ let match_dpat dp cls gls = (is_matching concld.d_sort (pf_type_of gls cl))) hl) then error "No match" - | ({onhyps=Some[];onconcl=true},ConclLocation concld) -> + | ({onhyps=Some[]},ConclLocation concld) when onconcl -> let cl = pf_concl gls in if not ((is_matching concld.d_typ cl) & diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index c6804329b..3b982b4c0 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -140,7 +140,7 @@ and e_my_find_search_nodelta db_list local_db hdc concl = | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (unify_e_resolve_nodelta (term,cl)) (e_trivial_fail_db false db_list local_db) - | Unfold_nth c -> unfold_in_concl [[],c] + | Unfold_nth c -> unfold_in_concl [all_occurrences,c] | Extern tacast -> conclPattern concl (Option.get p) tacast in @@ -179,7 +179,7 @@ and e_my_find_search_delta db_list local_db hdc concl = | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (unify_e_resolve st (term,cl)) (e_trivial_fail_db true db_list local_db) - | Unfold_nth c -> unfold_in_concl [[],c] + | Unfold_nth c -> unfold_in_concl [all_occurrences,c] | Extern tacast -> conclPattern concl (Option.get p) tacast in @@ -448,7 +448,7 @@ END let autosimpl db cl = let unfold_of_elts constr (b, elts) = if not b then - List.map (fun c -> [], constr c) elts + List.map (fun c -> all_occurrences, constr c) elts else [] in let unfolds = List.concat (List.map (fun dbname -> diff --git a/tactics/equality.ml b/tactics/equality.ml index b0c5a29eb..f907b1fd7 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -109,7 +109,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs (c,l) with_evars gl = then !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl else error "The term provided does not end with an equation" | Some (hdcncl,_) -> - if occs <> [] then ( + if occs <> all_occurrences then ( !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl) else let hdcncls = string_of_inductive hdcncl in @@ -145,10 +145,10 @@ let general_rewrite_in l2r occs id c = general_rewrite_ebindings_clause (Some id) l2r occs (c,NoBindings) let general_multi_rewrite l2r with_evars c cl = - let occs = List.fold_left + let occs_of = on_snd (List.fold_left (fun acc -> function ArgArg x -> x :: acc | ArgVar _ -> acc) - [] cl.concl_occs + []) in match cl.onhyps with | Some l -> @@ -156,24 +156,24 @@ let general_multi_rewrite l2r with_evars c cl = each of these locations. *) let rec do_hyps = function | [] -> tclIDTAC - | ((_,id),_) :: l -> - tclTHENFIRST - (general_rewrite_ebindings_in l2r occs id c with_evars) - (do_hyps l) + | ((occs,id),_) :: l -> + tclTHENFIRST + (general_rewrite_ebindings_in l2r (occs_of occs) id c with_evars) + (do_hyps l) in - if not cl.onconcl then do_hyps l else + if cl.concl_occs = no_occurrences_expr then do_hyps l else tclTHENFIRST - (general_rewrite_ebindings l2r occs c with_evars) - (do_hyps l) + (general_rewrite_ebindings l2r (occs_of cl.concl_occs) c with_evars) + (do_hyps l) | None -> (* Otherwise, if we are told to rewrite in all hypothesis via the syntax "* |-", we fail iff all the different rewrites fail *) let rec do_hyps_atleastonce = function | [] -> (fun gl -> error "Nothing to rewrite.") | id :: l -> - tclIFTHENTRYELSEMUST - (general_rewrite_ebindings_in l2r occs id c with_evars) - (do_hyps_atleastonce l) + tclIFTHENTRYELSEMUST + (general_rewrite_ebindings_in l2r all_occurrences id c with_evars) + (do_hyps_atleastonce l) in let do_hyps gl = (* If the term to rewrite uses an hypothesis H, don't rewrite in H *) @@ -182,10 +182,10 @@ let general_multi_rewrite l2r with_evars c cl = Idset.fold (fun id l -> list_remove id l) ids_in_c (pf_ids_of_hyps gl) in do_hyps_atleastonce ids gl in - if not cl.onconcl then do_hyps else - tclIFTHENTRYELSEMUST - (general_rewrite_ebindings l2r occs c with_evars) - do_hyps + if cl.concl_occs = no_occurrences_expr then do_hyps else + tclIFTHENTRYELSEMUST + (general_rewrite_ebindings l2r (occs_of cl.concl_occs) c with_evars) + do_hyps let general_multi_multi_rewrite with_evars l cl tac = let do1 l2r c = @@ -212,20 +212,22 @@ let general_multi_multi_rewrite with_evars l cl tac = to the resolution of the conditions by a given tactic *) let conditional_rewrite lft2rgt tac (c,bl) = - tclTHENSFIRSTn (general_rewrite_ebindings lft2rgt [] (c,bl) false) + tclTHENSFIRSTn + (general_rewrite_ebindings lft2rgt all_occurrences (c,bl) false) [|tclIDTAC|] (tclCOMPLETE tac) -let rewriteLR_bindings = general_rewrite_bindings true [] -let rewriteRL_bindings = general_rewrite_bindings false [] +let rewriteLR_bindings = general_rewrite_bindings true all_occurrences +let rewriteRL_bindings = general_rewrite_bindings false all_occurrences -let rewriteLR = general_rewrite true [] -let rewriteRL = general_rewrite false [] +let rewriteLR = general_rewrite true all_occurrences +let rewriteRL = general_rewrite false all_occurrences -let rewriteLRin_bindings = general_rewrite_bindings_in true [] -let rewriteRLin_bindings = general_rewrite_bindings_in false [] +let rewriteLRin_bindings = general_rewrite_bindings_in true all_occurrences +let rewriteRLin_bindings = general_rewrite_bindings_in false all_occurrences let conditional_rewrite_in lft2rgt id tac (c,bl) = - tclTHENSFIRSTn (general_rewrite_ebindings_in lft2rgt [] id (c,bl) false) + tclTHENSFIRSTn + (general_rewrite_ebindings_in lft2rgt all_occurrences id (c,bl) false) [|tclIDTAC|] (tclCOMPLETE tac) let rewriteRL_clause = function @@ -1124,7 +1126,8 @@ let unfold_body x gl = | _ -> errorlabstrm "unfold_body" (pr_id x ++ str" is not a defined hypothesis") in let aft = afterHyp x gl in - let hl = List.fold_right (fun (y,yval,_) cl -> (([],y),InHyp) :: cl) aft [] in + let hl = List.fold_right + (fun (y,yval,_) cl -> ((all_occurrences_expr,y),InHyp) :: cl) aft [] in let xvar = mkVar x in let rfun _ _ c = replace_term xvar xval c in tclTHENLIST diff --git a/tactics/equality.mli b/tactics/equality.mli index 19cf1ed56..acbaca235 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -21,14 +21,15 @@ open Pattern open Tacticals open Tactics open Tacexpr +open Termops open Rawterm open Genarg (*i*) val general_rewrite_bindings : - bool -> int list -> constr with_bindings -> evars_flag -> tactic + bool -> occurrences -> constr with_bindings -> evars_flag -> tactic val general_rewrite : - bool -> int list -> constr -> tactic + bool -> occurrences -> constr -> tactic (* Obsolete, use [general_rewrite_bindings l2r] [val rewriteLR_bindings : constr with_bindings -> tactic] @@ -42,13 +43,13 @@ val rewriteRL : constr -> tactic (* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *) val register_general_setoid_rewrite_clause : - (identifier option -> - bool -> int list -> constr -> new_goals:constr list -> tactic) -> unit + (identifier option -> bool -> + occurrences -> constr -> new_goals:constr list -> tactic) -> unit val general_rewrite_bindings_in : - bool -> int list -> identifier -> constr with_bindings -> evars_flag -> tactic + bool -> occurrences -> identifier -> constr with_bindings -> evars_flag -> tactic val general_rewrite_in : - bool -> int list -> identifier -> constr -> evars_flag -> tactic + bool -> occurrences -> identifier -> constr -> evars_flag -> tactic val general_multi_rewrite : bool -> evars_flag -> constr with_ebindings -> clause -> tactic diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index f768e98e4..158cecfc7 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -288,12 +288,11 @@ let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : Tacticals.clause = Option.map (fun l -> List.map - (fun id -> ( ([],trad_id id) ,Tacexpr.InHyp)) + (fun id -> ( (all_occurrences_expr,trad_id id) ,Tacexpr.InHyp)) l ) hyps; - Tacexpr.onconcl=concl; - Tacexpr.concl_occs = []} + Tacexpr.concl_occs = if concl then all_occurrences_expr else no_occurrences_expr} let raw_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause snd diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 0a9ed111f..11ace2abb 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -65,7 +65,8 @@ let h_generalize_gen cl = abstract_tactic (TacGeneralize (List.map (on_fst inj_occ) cl)) (generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl)) let h_generalize cl = - h_generalize_gen (List.map (fun c -> (([],c),Names.Anonymous)) cl) + h_generalize_gen (List.map (fun c -> ((all_occurrences_expr,c),Names.Anonymous)) + cl) let h_generalize_dep c = abstract_tactic (TacGeneralizeDep (inj_open c))(generalize_dep c) let h_let_tac b na c cl = diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index dc8ff2b9c..98c0c1104 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -1806,7 +1806,7 @@ let relation_rewrite_no_unif c1 c2 hyp ~new_goals sigma gl = if_output_relation_is_if gl with Optimize -> - !general_rewrite (fst hyp = Left2Right) [] (snd hyp) gl + !general_rewrite (fst hyp = Left2Right) all_occurrences (snd hyp) gl let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl = let (sigma,cl,c1,c2) = unification_rewrite c1 c2 cl (pf_concl gl) gl in @@ -1825,6 +1825,8 @@ let analyse_hypothesis gl c = eqclause,mkApp (equiv, Array.of_list others),c1,c2 let general_s_rewrite lft2rgt occs c ~new_goals gl = + if occs <> all_occurrences then + warning "Rewriting at selected occurrences not supported"; let eqclause,_,c1,c2 = analyse_hypothesis gl c in if lft2rgt then relation_rewrite c1 c2 (Left2Right,eqclause) ~new_goals gl @@ -1862,6 +1864,8 @@ let relation_rewrite_in id c1 c2 (direction,eqclause) ~new_goals gl = gl let general_s_rewrite_in id lft2rgt occs c ~new_goals gl = + if occs <> all_occurrences then + warning "Rewriting at selected occurrences not supported"; let eqclause,_,c1,c2 = analyse_hypothesis gl c in if lft2rgt then relation_rewrite_in id c1 c2 (Left2Right,eqclause) ~new_goals gl @@ -1916,7 +1920,7 @@ let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_ tclTHENS (assert_tac false Anonymous eq) [onLastHyp (fun id -> tclTHEN - (rewrite_tac dir [] (mkVar id) ~new_goals) + (rewrite_tac dir all_occurrences (mkVar id) ~new_goals) (clear [id])); try_prove_eq_tac] in @@ -1928,7 +1932,7 @@ let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_ tclTHENS (assert_tac false Anonymous eq) [onLastHyp (fun id -> tclTHEN - (rewrite_tac false [] (mkVar id) ~new_goals) + (rewrite_tac false all_occurrences (mkVar id) ~new_goals) (clear [id])); try_prove_eq_tac] gl diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index 1eb0141c6..244e02dd4 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -12,6 +12,7 @@ open Term open Proof_type open Topconstr open Names +open Termops type relation = { rel_a: constr ; @@ -40,7 +41,7 @@ type morphism_signature = (bool option * constr_expr) list * constr_expr val pr_morphism_signature : morphism_signature -> Pp.std_ppcmds val register_replace : (tactic option -> constr -> constr -> tactic) -> unit -val register_general_rewrite : (bool -> int list -> constr -> tactic) -> unit +val register_general_rewrite : (bool -> occurrences -> constr -> tactic) -> unit val print_setoids : unit -> unit @@ -58,9 +59,10 @@ val setoid_replace_in : identifier -> constr option -> constr -> constr -> new_goals:constr list -> tactic -val general_s_rewrite : bool -> int list -> constr -> new_goals:constr list -> tactic +val general_s_rewrite : + bool -> occurrences -> constr -> new_goals:constr list -> tactic val general_s_rewrite_in : - identifier -> bool -> int list -> constr -> new_goals:constr list -> tactic + identifier -> bool -> occurrences -> constr -> new_goals:constr list -> tactic val setoid_reflexivity : tactic val setoid_symmetry : tactic diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 20b4abf8a..2fc6692a8 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -204,7 +204,7 @@ let add_primitive_tactic s tac = atomic_mactab := Idmap.add id tac !atomic_mactab let _ = - let nocl = {onhyps=Some[];onconcl=true; concl_occs=[]} in + let nocl = {onhyps=Some[];concl_occs=all_occurrences_expr} in List.iter (fun (s,t) -> add_primitive_tactic s (TacAtom(dloc,t))) [ "red", TacReduce(Red false,nocl); @@ -610,8 +610,8 @@ let intern_inversion_strength lf ist = function InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl) (* Interprets an hypothesis name *) -let intern_hyp_location ist ((occs,id),hl) = - ((List.map (intern_or_var ist) occs,intern_hyp ist (skip_metaid id)), hl) +let intern_hyp_location ist (((b,occs),id),hl) = + (((b,List.map (intern_or_var ist) occs),intern_hyp ist (skip_metaid id)), hl) let interp_constrpattern_gen sigma env ?(as_type=false) ltacvar c = let c = intern_gen as_type ~allow_patvar:true ~ltacvars:(ltacvar,[]) @@ -672,10 +672,10 @@ let extract_let_names lrc = lrc [] let clause_app f = function - { onhyps=None; onconcl=b;concl_occs=nl } -> - { onhyps=None; onconcl=b; concl_occs=nl } - | { onhyps=Some l; onconcl=b;concl_occs=nl } -> - { onhyps=Some(List.map f l); onconcl=b;concl_occs=nl} + { onhyps=None; concl_occs=nl } -> + { onhyps=None; concl_occs=nl } + | { onhyps=Some l; concl_occs=nl } -> + { onhyps=Some(List.map f l); concl_occs=nl} (* Globalizes tactics : raw_tactic_expr -> glob_tactic_expr *) let rec intern_atomic lf ist x = @@ -783,7 +783,9 @@ let rec intern_atomic lf ist x = TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl) | TacChange (occl,c,cl) -> TacChange (Option.map (intern_constr_with_occurrences ist) occl, - (if occl = None & cl.onhyps = None & cl.concl_occs = [] + (if occl = None & (cl.onhyps = None or cl.onhyps = Some []) & + (cl.concl_occs = all_occurrences_expr or + cl.concl_occs = no_occurrences_expr) then intern_type ist c else intern_constr ist c), clause_app (intern_hyp_location ist) cl) @@ -1279,13 +1281,15 @@ let interp_evaluable ist env = function interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) locid (* Interprets an hypothesis name *) +let interp_occurrences ist (b,occs) = + (b,interp_int_or_var_list ist occs) + let interp_hyp_location ist gl ((occs,id),hl) = - ((interp_int_or_var_list ist occs,interp_hyp ist gl id),hl) + ((interp_occurrences ist occs,interp_hyp ist gl id),hl) -let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } = +let interp_clause ist gl { onhyps=ol; concl_occs=occs } = { onhyps=Option.map(List.map (interp_hyp_location ist gl)) ol; - onconcl=b; - concl_occs= interp_int_or_var_list ist occs } + concl_occs=interp_occurrences ist occs } (* Interpretation of constructions *) @@ -1483,22 +1487,23 @@ let pf_interp_type ist gl = interp_type ist (project gl) (pf_env gl) (* Interprets a reduction expression *) -let interp_unfold ist env (l,qid) = - (interp_int_or_var_list ist l,interp_evaluable ist env qid) +let interp_unfold ist env (occs,qid) = + (interp_occurrences ist occs,interp_evaluable ist env qid) let interp_flag ist env red = { red with rConst = List.map (interp_evaluable ist env) red.rConst } -let interp_pattern ist sigma env (l,c) = - (interp_int_or_var_list ist l, interp_constr ist sigma env c) +let interp_pattern ist sigma env (occs,c) = + (interp_occurrences ist occs, interp_constr ist sigma env c) let pf_interp_constr_with_occurrences ist gl = interp_pattern ist (project gl) (pf_env gl) let pf_interp_constr_with_occurrences_and_name_as_list = pf_interp_constr_in_compound_list - (fun c -> (([],c),Anonymous)) - (function (([],c),Anonymous) -> c | _ -> raise Not_found) + (fun c -> ((all_occurrences_expr,c),Anonymous)) + (function ((occs,c),Anonymous) when occs = all_occurrences_expr -> c + | _ -> raise Not_found) (fun ist gl (occ_c,na) -> (interp_pattern ist (project gl) (pf_env gl) occ_c, interp_fresh_name ist gl na)) @@ -2189,7 +2194,9 @@ and interp_atomic ist gl = function h_reduce (pf_interp_red_expr ist gl r) (interp_clause ist gl cl) | TacChange (occl,c,cl) -> h_change (Option.map (pf_interp_constr_with_occurrences ist gl) occl) - (if occl = None & cl.onhyps = None & cl.concl_occs = [] + (if occl = None & (cl.onhyps = None or cl.onhyps = Some []) & + (cl.concl_occs = all_occurrences_expr or + cl.concl_occs = no_occurrences_expr) then pf_interp_type ist gl c else pf_interp_constr ist gl c) (interp_clause ist gl cl) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index dd8aa1294..577ef0c6f 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -23,6 +23,7 @@ open Refiner open Tacmach open Clenv open Clenvtac +open Rawterm open Pattern open Matching open Evar_refiner @@ -123,17 +124,21 @@ let tclTRY_HYPS (tac : constr->tactic) gl = type simple_clause = identifier gsimple_clause type clause = identifier gclause -let allClauses = { onhyps=None; onconcl=true; concl_occs=[] } -let allHyps = { onhyps=None; onconcl=false; concl_occs=[] } -let onHyp id = { onhyps=Some[(([],id),InHyp)]; onconcl=false; concl_occs=[] } -let onConcl = { onhyps=Some[]; onconcl=true; concl_occs=[] } +let allClauses = { onhyps=None; concl_occs=all_occurrences_expr } +let allHyps = { onhyps=None; concl_occs=no_occurrences_expr } +let onConcl = { onhyps=Some[]; concl_occs=all_occurrences_expr } +let onHyp id = + { onhyps=Some[((all_occurrences_expr,id),InHyp)]; concl_occs=no_occurrences_expr } let simple_clause_list_of cl gls = let hyps = match cl.onhyps with - None -> List.map (fun id -> Some(([],id),InHyp)) (pf_ids_of_hyps gls) - | Some l -> List.map (fun h -> Some h) l in - if cl.onconcl then None::hyps else hyps + | None -> + let f id = Some((all_occurrences_expr,id),InHyp) in + List.map f (pf_ids_of_hyps gls) + | Some l -> + List.map (fun h -> Some h) l in + if cl.concl_occs = all_occurrences_expr then None::hyps else hyps (* OR-branch *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 905511b12..4ec8ee0ae 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -56,6 +56,8 @@ let rec nb_prod x = | _ -> n in count 0 x +let inj_with_occurrences e = (all_occurrences_expr,e) + let inj_open c = (Evd.empty,c) let inj_occ (occ,c) = (occ,inj_open c) @@ -214,7 +216,8 @@ let change_option occl t = function let change occl c cls = (match cls, occl with - ({onhyps=(Some(_::_::_)|None)}|{onhyps=Some(_::_);onconcl=true}), + ({onhyps=(Some(_::_::_)|None)} + |{onhyps=Some(_::_);concl_occs=((false,_)|(true,_::_))}), Some _ -> error "No occurrences expected when changing several hypotheses" | _ -> ()); @@ -256,8 +259,8 @@ let reduce redexp cl goal = (* Unfolding occurrences of a constant *) let unfold_constr = function - | ConstRef sp -> unfold_in_concl [[],EvalConstRef sp] - | VarRef id -> unfold_in_concl [[],EvalVarRef id] + | ConstRef sp -> unfold_in_concl [all_occurrences,EvalConstRef sp] + | VarRef id -> unfold_in_concl [all_occurrences,EvalVarRef id] | _ -> errorlabstrm "unfold_constr" (str "Cannot unfold a non-constant.") (*******************************************) @@ -1175,7 +1178,7 @@ let generalize_dep c gl = | _ -> tothin in let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in - let cl'' = generalize_goal gl 0 (([],c),Anonymous) cl' in + let cl'' = generalize_goal gl 0 ((all_occurrences,c),Anonymous) cl' in let args = Array.to_list (instance_from_named_context to_quantify_rev) in tclTHEN (apply_type cl'' (c::args)) @@ -1187,7 +1190,8 @@ let generalize_gen lconstr gl = list_fold_right_i (generalize_goal gl) 0 lconstr (pf_concl gl) in apply_type newcl (List.map (fun ((_,c),_) -> c) lconstr) gl -let generalize l = generalize_gen (List.map (fun c -> (([],c),Anonymous)) l) +let generalize l = + generalize_gen (List.map (fun c -> ((all_occurrences,c),Anonymous)) l) let revert hyps gl = tclTHEN (generalize (List.map mkVar hyps)) (clear hyps) gl @@ -1235,14 +1239,15 @@ let out_arg = function let occurrences_of_hyp id cls = let rec hyp_occ = function [] -> None - | ((occs,id'),hl)::_ when id=id' -> Some (List.map out_arg occs) + | (((b,occs),id'),hl)::_ when id=id' -> Some (b,List.map out_arg occs) | _::l -> hyp_occ l in match cls.onhyps with - None -> Some [] + None -> Some (all_occurrences) | Some l -> hyp_occ l let occurrences_of_goal cls = - if cls.onconcl then Some (List.map out_arg cls.concl_occs) else None + if cls.concl_occs = no_occurrences_expr then None + else Some (on_snd (List.map out_arg) cls.concl_occs) let in_every_hyp cls = (cls.onhyps=None) @@ -1311,7 +1316,7 @@ let letin_abstract id c occs gl = | None -> depdecls | Some occ -> let newdecl = subst_term_occ_decl occ c d in - if occ = [] & d = newdecl then + if occ = all_occurrences & d = newdecl then if not (in_every_hyp occs) then raise (RefinerError (DoesNotOccurIn (c,hyp))) else depdecls @@ -2297,8 +2302,6 @@ let recolle_clenv scheme lid elimclause gl = (List.rev clauses) elimclause - - (* Unification of the goal and the principle applied to meta variables: (elimc ?i ?j ?k...?l). This solves partly meta variables (and may produce new ones). Then refine with the resulting term with holes. @@ -2364,7 +2367,7 @@ let induction_from_context_l isrec with_evars elim_info lid names gl = if deps = [] then tclIDTAC else apply_type tmpcl deps_cstr; thin dephyps; (* clear dependent hyps *) (* pattern to make the predicate appear. *) - reduce (Pattern (List.map (fun e -> ([],e)) lidcstr)) onConcl; + reduce (Pattern (List.map inj_with_occurrences lidcstr)) onConcl; (* FIXME: Tester ca avec un principe dependant et non-dependant *) (if isrec then tclTHENFIRSTn else tclTHENLASTn) (tclTHENLIST [ diff --git a/tactics/tactics.mli b/tactics/tactics.mli index bfb49cba7..0492e296f 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -26,6 +26,7 @@ open Genarg open Tacexpr open Nametab open Rawterm +open Termops (*i*) val inj_open : constr -> open_constr @@ -121,9 +122,9 @@ type tactic_reduction = env -> evar_map -> constr -> constr val reduct_in_hyp : tactic_reduction -> hyp_location -> tactic val reduct_option : tactic_reduction * cast_kind -> simple_clause -> tactic val reduct_in_concl : tactic_reduction * cast_kind -> tactic -val change_in_concl : (int list * constr) option -> constr -> tactic -val change_in_hyp : (int list * constr) option -> constr -> hyp_location -> - tactic +val change_in_concl : (occurrences * constr) option -> constr -> tactic +val change_in_hyp : (occurrences * constr) option -> constr -> + hyp_location -> tactic val red_in_concl : tactic val red_in_hyp : hyp_location -> tactic val red_option : simple_clause -> tactic @@ -137,18 +138,19 @@ val normalise_in_concl : tactic val normalise_in_hyp : hyp_location -> tactic val normalise_option : simple_clause -> tactic val normalise_vm_in_concl : tactic -val unfold_in_concl : (int list * evaluable_global_reference) list -> tactic +val unfold_in_concl : + (occurrences * evaluable_global_reference) list -> tactic val unfold_in_hyp : - (int list * evaluable_global_reference) list -> hyp_location -> tactic + (occurrences * evaluable_global_reference) list -> hyp_location -> tactic val unfold_option : - (int list * evaluable_global_reference) list -> simple_clause + (occurrences * evaluable_global_reference) list -> simple_clause -> tactic -val reduce : red_expr -> clause -> tactic val change : - (int list * constr) option -> constr -> clause -> tactic - + (occurrences * constr) option -> constr -> clause -> tactic +val pattern_option : + (occurrences * constr) list -> simple_clause -> tactic +val reduce : red_expr -> clause -> tactic val unfold_constr : global_reference -> tactic -val pattern_option : (int list * constr) list -> simple_clause -> tactic (*s Modification of the local context. *) @@ -326,9 +328,9 @@ val forward : tactic option -> intro_pattern_expr -> constr -> tactic val letin_tac : bool option -> name -> constr -> clause -> tactic val true_cut : name -> constr -> tactic val assert_tac : bool -> name -> constr -> tactic -val generalize : constr list -> tactic -val generalize_gen : ((int list * constr) * name) list -> tactic -val generalize_dep : constr -> tactic +val generalize : constr list -> tactic +val generalize_gen : ((occurrences * constr) * name) list -> tactic +val generalize_dep : constr -> tactic val tclABSTRACT : identifier option -> tactic -> tactic diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index a6ae7240c..0ef835689 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -527,7 +527,8 @@ let compute_bl_tact ind lnamesparrec nparrec = tclTRY ( tclORELSE reflexivity (Equality.discr_tac None) ); - simpl_in_hyp (([],freshz),Tacexpr.InHyp); + simpl_in_hyp + ((Rawterm.all_occurrences_expr,freshz),Tacexpr.InHyp); (* repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). *) @@ -798,7 +799,8 @@ let compute_dec_tact ind lnamesparrec nparrec = (tclTHENSEQ [apply (mkApp(lbI,Array.map (fun x->mkVar x) xargs)); Auto.default_auto ]); - Pfedit.by (Equality.general_rewrite_bindings_in true [] + Pfedit.by (Equality.general_rewrite_bindings_in true + all_occurrences (List.hd !avoid) ((mkVar (List.hd (List.tl !avoid))), Rawterm.NoBindings |