From 9dec278bb1af17f30021bf0bb04f21682d1f0a3c Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 6 Jul 2007 16:35:07 +0000 Subject: Adding a syntax for "n-ary" rewrite: rewrite H, H' means: rewrite H; rewrite H'. This should still be compatible with other "features" of rewrite: like orientation, implicit arguments (t:=...), and "in" clause. Concerning the "in" clause, for the moment only one is allowed at the very end of the tactic, and it applies to all the different rewrites that are done. For instance, if someone _really_ wants to use all features at the same time: rewrite H1 with (t:=u), <-H2, H3 in * means: rewrite H1 with (t:=u) in *; rewrite <- H2 in *; rewrite H3 in * git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9954 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/interface/xlate.ml | 5 +++-- doc/refman/RefMan-tac.tex | 10 ++++++++++ parsing/g_tactic.ml4 | 11 +++++++---- parsing/pptactic.ml | 10 +++++++--- proofs/tacexpr.ml | 2 +- tactics/equality.ml | 6 ++++++ tactics/equality.mli | 2 ++ tactics/tacinterp.ml | 20 ++++++++++++-------- 8 files changed, 48 insertions(+), 18 deletions(-) diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 068110d74..9c81a1c3a 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1012,13 +1012,14 @@ and xlate_tac = CT_coerce_TACTIC_COM_to_TACTIC_OPT tac in CT_replace_with (c1, c2,cl,tac_opt) - | TacRewrite(b,false,cbindl,cl) -> + | TacRewrite(false,[b,cbindl],cl) -> let cl = xlate_clause cl and c = xlate_formula (fst cbindl) and bindl = xlate_bindings (snd cbindl) in if b then CT_rewrite_lr (c, bindl, cl) else CT_rewrite_rl (c, bindl, cl) - | TacRewrite(b,true,cbindl,cl) -> xlate_error "TODO: erewrite" + | TacRewrite(false,_,cl) -> xlate_error "TODO: rewrite of several hyps at once" + | TacRewrite(true,_,cl) -> xlate_error "TODO: erewrite" | TacExtend (_,"conditional_rewrite", [t; b; cbindl]) -> let t = out_gen rawwit_main_tactic t in let b = out_gen Extraargs.rawwit_orient b in diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 0ba9553ce..8dd168aad 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1728,6 +1728,16 @@ This happens if \term$_1$ does not occur in the goal. \tacindex{rewrite <- \dots\ in} Uses the equality \term$_1${\tt=}\term$_2$ from right to left to rewrite in \textit{clause} as explained above. + +\item {\tt rewrite $\term_1$, \ldots, $term_n$}\\ + Is equivalent to {\tt rewrite $\term_1$; \ldots; rewrite $\term_n$}. + Orientation {\tt ->} or {\tt <-} can be inserted before each term. + +\item {\tt rewrite $\term_1$, \ldots, $term_n$ in \textit{clause}}\\ + Is equivalent to {\tt rewrite $\term_1$ in \textit{clause}; \ldots; + rewrite $\term_n$ in \textit{clause}}. + Orientation {\tt ->} or {\tt <-} can be inserted before each term. + \end{Variants} diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 3853a6d51..9d0cd28ff 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -317,6 +317,9 @@ GEXTEND Gram rename : [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ] ; + rewriter : + [ [ b = orient; c = constr_with_bindings -> (b,c) ] ] + ; simple_tactic: [ [ (* Basic tactics *) @@ -436,10 +439,10 @@ GEXTEND Gram | IDENT "transitivity"; c = constr -> TacTransitivity c (* Equality and inversion *) - | IDENT "rewrite"; b = orient; c = constr_with_bindings ; cl = clause -> - TacRewrite (b,false,c,cl) - | IDENT "erewrite"; b = orient; c = constr_with_bindings ; cl = clause -> - TacRewrite (b,true,c,cl) + | IDENT "rewrite"; l = LIST1 rewriter SEP ","; cl = clause -> + TacRewrite (false,l,cl) + | IDENT "erewrite"; l = LIST1 rewriter SEP ","; cl = clause -> + TacRewrite (true,l,cl) | IDENT "dependent"; k = [ IDENT "simple"; IDENT "inversion" -> SimpleInversion | IDENT "inversion" -> FullInversion diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index b07213fe9..52b2e5f64 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -824,9 +824,13 @@ and pr_atom1 = function | TacTransitivity c -> str "transitivity" ++ pr_constrarg c (* Equality and inversion *) - | TacRewrite (b,ev,c,cl) -> - hov 1 (str (if ev then "erewrite" else "rewrite") ++ pr_orient b ++ - spc() ++ pr_with_bindings c ++ pr_clauses pr_ident cl) + | TacRewrite (ev,l,cl) -> + hov 1 (str (if ev then "erewrite" else "rewrite") ++ + prlist_with_sep + (fun () -> str ","++spc()) + (fun (b,c) -> pr_orient b ++ spc() ++ pr_with_bindings c) + l + ++ pr_clauses pr_ident cl) | TacInversion (DepInversion (k,c,ids),hyp) -> hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++ pr_quantified_hypothesis hyp ++ diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 8c45d95b3..f99ce1a88 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -185,7 +185,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacTransitivity of 'constr (* Equality and inversion *) - | TacRewrite of bool * evars_flag * 'constr with_bindings * 'id gclause + | TacRewrite of evars_flag * (bool * 'constr with_bindings) list * 'id gclause | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis (* For ML extensions *) diff --git a/tactics/equality.ml b/tactics/equality.ml index c5b7aeedf..4f94ba595 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -166,6 +166,12 @@ let general_multi_rewrite l2r with_evars c cl = (general_rewrite_ebindings l2r c with_evars) do_hyps +let rec general_multi_multi_rewrite with_evars l cl = match l with + | [] -> tclIDTAC + | (l2r,c)::l -> + tclTHEN (general_multi_rewrite l2r with_evars c cl) + (general_multi_multi_rewrite with_evars l cl) + (* Conditional rewriting, the success of a rewriting is related to the resolution of the conditions by a given tactic *) diff --git a/tactics/equality.mli b/tactics/equality.mli index 36fc99594..772f9cdc8 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -48,6 +48,8 @@ val general_rewrite_in : val general_multi_rewrite : bool -> evars_flag -> constr with_ebindings -> clause -> tactic +val general_multi_multi_rewrite : + evars_flag -> (bool * constr with_ebindings) list -> clause -> tactic val conditional_rewrite : bool -> tactic -> constr with_ebindings -> tactic val conditional_rewrite_in : diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 944b7710a..dc4b3822f 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -744,9 +744,11 @@ let rec intern_atomic lf ist x = | TacTransitivity c -> TacTransitivity (intern_constr ist c) (* Equality and inversion *) - | TacRewrite (b,ev,c,cl) -> - TacRewrite (b,ev,intern_constr_with_bindings ist c, - clause_app (intern_hyp_location ist) cl) + | TacRewrite (ev,l,cl) -> + TacRewrite + (ev, + List.map (fun (b,c) -> (b,intern_constr_with_bindings ist c)) l, + clause_app (intern_hyp_location ist) cl) | TacInversion (inv,hyp) -> TacInversion (intern_inversion_strength lf ist inv, intern_quantified_hypothesis ist hyp) @@ -2158,9 +2160,9 @@ and interp_atomic ist gl = function | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c) (* Equality and inversion *) - | TacRewrite (b,ev,c,cl) -> - Equality.general_multi_rewrite b ev - (interp_constr_with_bindings ist gl c) + | TacRewrite (ev,l,cl) -> + Equality.general_multi_multi_rewrite ev + (List.map (fun (b,c) -> (b, interp_constr_with_bindings ist gl c)) l) (interp_clause ist gl cl) | TacInversion (DepInversion (k,c,ids),hyp) -> Inv.dinv k (option_map (pf_interp_constr ist gl) c) @@ -2451,8 +2453,10 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacTransitivity c -> TacTransitivity (subst_rawconstr subst c) (* Equality and inversion *) - | TacRewrite (b,ev,c,cl) -> - TacRewrite (b,ev,subst_raw_with_bindings subst c,cl) + | TacRewrite (ev,l,cl) -> + TacRewrite (ev, + List.map (fun (b,c) ->b,subst_raw_with_bindings subst c) l, + cl) | TacInversion (DepInversion (k,c,l),hyp) -> TacInversion (DepInversion (k,option_map (subst_rawconstr subst) c,l),hyp) | TacInversion (NonDepInversion _,_) as x -> x -- cgit v1.2.3