Exporting the rewrite tactic.

11 files changed, 109 insertions, 8 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 48a593df28..8b373647f3 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -309,7 +309,7 @@ let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
 
 GEXTEND Gram
   GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause
-          q_rewriting;
+          q_rewriting q_clause;
   anti:
     [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
   ;
@@ -479,12 +479,14 @@ GEXTEND Gram
         { q_onhyps = Some hl; q_concl_occs = QNoOccurrences }
     ] ]
   ;
-  opt_clause:
-    [ [ "in"; cl = in_clause -> Some cl
-      | "at"; occs = occs_nums -> Some { q_onhyps = Some []; q_concl_occs = occs }
-      | -> None
+  clause:
+    [ [ "in"; cl = in_clause -> cl
+      | "at"; occs = occs_nums -> { q_onhyps = Some []; q_concl_occs = occs }
     ] ]
   ;
+  q_clause:
+    [ [ cl = clause -> Tac2quote.of_clause cl ] ]
+  ;
   concl_occ:
     [ [ "*"; occs = occs -> occs
       | -> QNoOccurrences
@@ -492,7 +494,7 @@ GEXTEND Gram
   ;
   induction_clause:
     [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
-        cl = opt_clause ->
+        cl = OPT clause ->
         Loc.tag ~loc:!@loc @@ {
           indcl_arg = c;
           indcl_eqn = eq;
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 72b4dbfe97..7539e1b697 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -893,6 +893,7 @@ let () = add_expr_scope "intropattern" Tac2entries.Pltac.q_intropattern
 let () = add_expr_scope "intropatterns" Tac2entries.Pltac.q_intropatterns
 let () = add_expr_scope "induction_clause" Tac2entries.Pltac.q_induction_clause
 let () = add_expr_scope "rewriting" Tac2entries.Pltac.q_rewriting
+let () = add_expr_scope "clause" Tac2entries.Pltac.q_clause
 
 let () = add_generic_scope "constr" Pcoq.Constr.constr Stdarg.wit_constr
 let () = add_generic_scope "open_constr" Pcoq.Constr.constr Stdarg.wit_open_constr
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 3aa1ee23b7..40d8ff078e 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -30,6 +30,7 @@ let q_intropattern = Pcoq.Gram.entry_create "tactic:q_intropattern"
 let q_intropatterns = Pcoq.Gram.entry_create "tactic:q_intropatterns"
 let q_induction_clause = Pcoq.Gram.entry_create "tactic:q_induction_clause"
 let q_rewriting = Pcoq.Gram.entry_create "tactic:q_rewriting"
+let q_clause = Pcoq.Gram.entry_create "tactic:q_clause"
 end
 
 (** Tactic definition *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index f5c5a479c4..1fe13cda17 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -63,4 +63,5 @@ val q_intropattern : raw_tacexpr Pcoq.Gram.entry
 val q_intropatterns : raw_tacexpr Pcoq.Gram.entry
 val q_induction_clause : raw_tacexpr Pcoq.Gram.entry
 val q_rewriting : raw_tacexpr Pcoq.Gram.entry
+val q_clause : raw_tacexpr Pcoq.Gram.entry
 end
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index cb2e406571..ddb39326d1 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -41,6 +41,8 @@ val of_intro_pattern : intro_pattern -> raw_tacexpr
 
 val of_intro_patterns : intro_pattern list located -> raw_tacexpr
 
+val of_clause : ?loc:Loc.t -> clause -> raw_tacexpr
+
 val of_induction_clause : induction_clause -> raw_tacexpr
 
 val of_rewriting : rewriting -> raw_tacexpr
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 7e421c8577..e8e63f520c 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -141,6 +141,21 @@ let to_induction_clause = function
 | _ ->
   assert false
 
+let to_multi = function
+| ValBlk (0, [| n |]) -> Precisely (Value.to_int n)
+| ValBlk (1, [| n |]) -> UpTo (Value.to_int n)
+| ValInt 0 -> RepeatStar
+| ValInt 1 -> RepeatPlus
+| _ -> assert false
+
+let to_rewriting = function
+| ValBlk (0, [| orient; repeat; c |]) ->
+  let orient = Value.to_option Value.to_bool orient in
+  let repeat = to_multi repeat in
+  let c = thaw c >>= fun c -> return (to_constr_with_bindings c) in
+  (orient, repeat, c)
+| _ -> assert false
+
 (** Standard tactics sharing their implementation with Ltac1 *)
 
 let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
@@ -304,6 +319,15 @@ let () = define_prim2 "tac_lazy" begin fun flags cl ->
   Tactics.reduce (Lazy flags) cl
 end
 
+let () = define_prim4 "tac_rewrite" begin fun ev rw cl by ->
+  let ev = Value.to_bool ev in
+  let rw = Value.to_list to_rewriting rw in
+  let cl = to_clause cl in
+  let to_tac t = Proofview.tclIGNORE (thaw t) in
+  let by = Value.to_option to_tac by in
+  Tac2tactics.rewrite ev rw cl by
+end
+
 (** Tactics from coretactics *)
 
 let () = define_prim0 "tac_reflexivity" Tactics.intros_reflexivity
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 439250db78..e7e15544af 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -44,3 +44,16 @@ let map_induction_clause ((clear, arg), eqn, as_, occ) =
 let induction_destruct isrec ev ic using =
   let ic = List.map map_induction_clause ic in
   Tactics.induction_destruct isrec ev (ic, using)
+
+type rewriting =
+  bool option *
+  multi *
+  EConstr.constr with_bindings tactic
+
+let rewrite ev rw cl by =
+  let map_rw (orient, repeat, c) =
+    (Option.default true orient, repeat, None, delayed_of_tactic c)
+  in
+  let rw = List.map map_rw rw in
+  let by = Option.map (fun tac -> Tacticals.New.tclCOMPLETE tac, Equality.Naive) by in
+  Equality.general_multi_rewrite ev rw cl by
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index f29793411a..93cc6ecd68 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Names
+open Locus
 open Misctypes
 open Tactypes
 open Proofview
@@ -21,7 +22,15 @@ type induction_clause =
   EConstr.constr with_bindings tactic destruction_arg *
   intro_pattern_naming option *
   or_and_intro_pattern option *
-  Locus.clause option
+  clause option
 
 val induction_destruct : rec_flag -> evars_flag ->
-  induction_clause list -> EConstr.constr with_bindings option -> unit Proofview.tactic
+  induction_clause list -> EConstr.constr with_bindings option -> unit tactic
+
+type rewriting =
+  bool option *
+  multi *
+  EConstr.constr with_bindings tactic
+
+val rewrite :
+  evars_flag -> rewriting list -> clause -> unit tactic option -> unit tactic
diff --git a/tests/example2.v b/tests/example2.v
index 812f9172c9..526cbc39f5 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -95,3 +95,24 @@ Proof.
 intros b1 b2.
 destruct &b1 as [|], &b2 as [|]; split.
 Qed.
+
+Goal forall n m, n = 0 -> n + m = m.
+Proof.
+intros n m Hn.
+rewrite &Hn; split.
+Qed.
+
+Goal forall n m p, n = m -> p = m -> 0 = n -> p = 0.
+Proof.
+intros n m p He He' Hn.
+rewrite &He, <- &He' in Hn.
+rewrite &Hn.
+split.
+Qed.
+
+Goal forall n m, (m = n -> n = m) -> m = n -> n = 0 -> m = 0.
+Proof.
+intros n m He He' He''.
+rewrite <- &He by Std.assumption ().
+Control.refine (fun () => &He'').
+Qed.
diff --git a/theories/Notations.v b/theories/Notations.v
index 20f01c3b48..4ce9fc0dbd 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -138,3 +138,28 @@ Ltac2 Notation "edestruct"
   ic(list1(induction_clause, ","))
   use(thunk(opt(seq("using", constr, bindings)))) :=
   destruct0 true ic use.
+
+Ltac2 rewrite0 ev rw cl tac :=
+  let tac := match tac with
+  | None => None
+  | Some p =>
+    let ((_, tac)) := p in
+    Some tac
+  end in
+  let cl := match cl with
+  | None => { Std.on_hyps := Some []; Std.on_concl := Std.AllOccurrences }
+  | Some cl => cl
+  end in
+  Std.rewrite ev rw cl tac.
+
+Ltac2 Notation "rewrite"
+  rw(list1(rewriting, ","))
+  cl(opt(clause))
+  tac(opt(seq("by", thunk(tactic)))) :=
+  rewrite0 false rw cl tac.
+
+Ltac2 Notation "erewrite"
+  rw(list1(rewriting, ","))
+  cl(opt(clause))
+  tac(opt(seq("by", thunk(tactic)))) :=
+  rewrite0 true rw cl tac.
diff --git a/theories/Std.v b/theories/Std.v
index 09cb3ca0c2..695ea26444 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -134,6 +134,8 @@ Ltac2 @ external cbv : red_flags -> clause -> unit := "ltac2" "tac_cbv".
 Ltac2 @ external cbn : red_flags -> clause -> unit := "ltac2" "tac_cbn".
 Ltac2 @ external lazy : red_flags -> clause -> unit := "ltac2" "tac_lazy".
 
+Ltac2 @ external rewrite : evar_flag -> rewriting list -> clause -> (unit -> unit) option -> unit := "ltac2" "tac_rewrite".
+
 Ltac2 @ external reflexivity : unit -> unit := "ltac2" "tac_reflexivity".
 
 Ltac2 @ external assumption : unit -> unit := "ltac2" "tac_assumption".