Introducing quotations for the rewrite tactic.

7 files changed, 98 insertions, 28 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index b10f8d66bd..48a593df28 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -308,7 +308,8 @@ open Tac2entries.Pltac
 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;
+  GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause
+          q_rewriting;
   anti:
     [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
   ;
@@ -503,6 +504,39 @@ GEXTEND Gram
   q_induction_clause:
     [ [ cl = induction_clause -> Tac2quote.of_induction_clause cl ] ]
   ;
+  orient:
+    [ [ "->" -> Loc.tag ~loc:!@loc (Some true)
+      | "<-" -> Loc.tag ~loc:!@loc (Some false)
+      | -> Loc.tag ~loc:!@loc None
+    ]]
+  ;
+  rewriter:
+    [ [ "!"; c = constr_with_bindings ->
+        (Loc.tag ~loc:!@loc @@ QRepeatPlus,c)
+      | ["?"| LEFTQMARK]; c = constr_with_bindings ->
+        (Loc.tag ~loc:!@loc @@ QRepeatStar,c)
+      | n = lnatural; "!"; c = constr_with_bindings ->
+        (Loc.tag ~loc:!@loc @@ QPrecisely n,c)
+      |	n = lnatural; ["?" | LEFTQMARK]; c = constr_with_bindings ->
+        (Loc.tag ~loc:!@loc @@ QUpTo n,c)
+      | n = lnatural; c = constr_with_bindings ->
+        (Loc.tag ~loc:!@loc @@ QPrecisely n,c)
+      | c = constr_with_bindings ->
+        (Loc.tag ~loc:!@loc @@ QPrecisely (Loc.tag 1), c)
+      ] ]
+  ;
+  oriented_rewriter:
+    [ [ b = orient; (m, c) = rewriter ->
+      Loc.tag ~loc:!@loc @@ {
+        rew_orient = b;
+        rew_repeat = m;
+        rew_equatn = c;
+      }
+    ] ]
+  ;
+  q_rewriting:
+    [ [ r = oriented_rewriter -> Tac2quote.of_rewriting r ] ]
+  ;
 END
 
 (** Extension of constr syntax *)
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 45fa52ff9b..72b4dbfe97 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -883,29 +883,16 @@ let () = add_scope "bindings" begin function
 | _ -> scope_fail ()
 end
 
-let () = add_scope "intropattern" begin function
-| [] ->
-  let scope = Extend.Aentry Tac2entries.Pltac.q_intropattern in
-  let act tac = tac in
-  Tac2entries.ScopeRule (scope, act)
-| _ -> scope_fail ()
-end
-
-let () = add_scope "intropatterns" begin function
-| [] ->
-  let scope = Extend.Aentry Tac2entries.Pltac.q_intropatterns in
-  let act tac = tac in
-  Tac2entries.ScopeRule (scope, act)
-| _ -> scope_fail ()
-end
+let add_expr_scope name entry =
+  add_scope name begin function
+  | [] -> Tac2entries.ScopeRule (Extend.Aentry entry, (fun e -> e))
+  | _ -> scope_fail ()
+  end
 
-let () = add_scope "induction_clause" begin function
-| [] ->
-  let scope = Extend.Aentry Tac2entries.Pltac.q_induction_clause in
-  let act tac = tac in
-  Tac2entries.ScopeRule (scope, act)
-| _ -> scope_fail ()
-end
+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_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 ce86e8aa33..3aa1ee23b7 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -29,6 +29,7 @@ let q_bindings = Pcoq.Gram.entry_create "tactic:q_bindings"
 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"
 end
 
 (** Tactic definition *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 1567551246..f5c5a479c4 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -62,4 +62,5 @@ val q_bindings : raw_tacexpr Pcoq.Gram.entry
 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
 end
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 0eb9e9f4b5..f6b8c2c19b 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -63,8 +63,10 @@ type hyp_location = (occurrences * Id.t located or_anti) * Locus.hyp_location_fl
 type clause =
   { q_onhyps : hyp_location list option; q_concl_occs : occurrences; }
 
+type constr_with_bindings = (Constrexpr.constr_expr * bindings) located
+
 type destruction_arg =
-| QElimOnConstr of (Constrexpr.constr_expr * bindings) located
+| QElimOnConstr of constr_with_bindings
 | QElimOnIdent of Id.t located
 | QElimOnAnonHyp of int located
 
@@ -76,3 +78,19 @@ type induction_clause_r = {
 }
 
 type induction_clause = induction_clause_r located
+
+type multi_r =
+| QPrecisely of int located
+| QUpTo of int located
+| QRepeatStar
+| QRepeatPlus
+
+type multi = multi_r located
+
+type rewriting_r = {
+  rew_orient : bool option located;
+  rew_repeat : multi;
+  rew_equatn : constr_with_bindings;
+}
+
+type rewriting = rewriting_r located
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 1cba488768..7d9c01f3f0 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -109,6 +109,11 @@ let of_bindings (loc, b) = match b with
   let tl = List.map map tl in
   std_constructor ?loc "ExplicitBindings" [of_list ?loc tl]
 
+let of_constr_with_bindings (loc, (c, bnd)) =
+  let c = of_open_constr c in
+  let bnd = of_bindings bnd in
+  of_pair ?loc (c, bnd)
+
 let rec of_intro_pattern (loc, pat) = match pat with
 | QIntroForthcoming b ->
   std_constructor ?loc "IntroForthcoming" [of_bool b]
@@ -179,10 +184,8 @@ let of_clause ?loc cl =
   ])
 
 let of_destruction_arg ?loc = function
-| QElimOnConstr (loc, (c, bnd)) ->
-  let c = of_open_constr c in
-  let bnd = of_bindings bnd in
-  let arg = thunk (of_pair ?loc (c, bnd)) in
+| QElimOnConstr c ->
+  let arg = thunk (of_constr_with_bindings c) in
   std_constructor ?loc "ElimOnConstr" [arg]
 | QElimOnIdent id -> std_constructor ?loc "ElimOnIdent" [of_ident id]
 | QElimOnAnonHyp n -> std_constructor ?loc "ElimOnAnonHyp" [of_int n]
@@ -200,6 +203,30 @@ let of_induction_clause (loc, cl) =
     std_proj "indcl_in", in_;
   ])
 
+let of_repeat (loc, r) = match r with
+| QPrecisely n -> std_constructor ?loc "Precisely" [of_int n]
+| QUpTo n -> std_constructor ?loc "UpTo" [of_int n]
+| QRepeatStar -> std_constructor ?loc "RepeatStar" []
+| QRepeatPlus -> std_constructor ?loc "RepeatPlus" []
+
+let of_orient loc b =
+  if b then std_constructor ?loc "LTR" []
+  else std_constructor ?loc "RTL" []
+
+let of_rewriting (loc, rew) =
+  let orient =
+    let (loc, orient) = rew.rew_orient in
+    of_option ?loc (Option.map (fun b -> of_orient loc b) orient)
+  in
+  let repeat = of_repeat rew.rew_repeat in
+  let equatn = thunk (of_constr_with_bindings rew.rew_equatn) in
+  let loc = Option.default dummy_loc loc in
+  CTacRec (loc, [
+    std_proj "rew_orient", orient;
+    std_proj "rew_repeat", repeat;
+    std_proj "rew_equatn", equatn;
+  ])
+
 let of_hyp ?loc id =
   let loc = Option.default dummy_loc loc in
   let hyp = CTacRef (AbsKn (control_core "hyp")) in
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 404e9378e0..cb2e406571 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -43,6 +43,8 @@ val of_intro_patterns : intro_pattern list located -> raw_tacexpr
 
 val of_induction_clause : induction_clause -> raw_tacexpr
 
+val of_rewriting : rewriting -> raw_tacexpr
+
 val of_hyp : ?loc:Loc.t -> Id.t located -> raw_tacexpr
 (** id ↦ 'Control.hyp @id' *)