Introducing a syntax for goal dispatch.

9 files changed, 59 insertions, 1 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 695fc7d430..e9d2eb1ca3 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -107,6 +107,7 @@ GEXTEND Gram
       | "match"; e = tac2expr LEVEL "5"; "with"; bl = branches; "end" ->
          CTacCse (!@loc, e, bl)
       ]
+    | "4" LEFTA [ ]
     | "::" RIGHTA
       [ e1 = tac2expr; "::"; e2 = tac2expr ->
         CTacApp (!@loc, CTacCst (!@loc, AbsKn (Other Tac2core.Core.c_cons)), [e1; e2])
@@ -309,7 +310,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_clause;
+          q_rewriting q_clause q_dispatch;
   anti:
     [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
   ;
@@ -540,6 +541,23 @@ GEXTEND Gram
   q_rewriting:
     [ [ r = oriented_rewriter -> Tac2quote.of_rewriting r ] ]
   ;
+  tactic_then_last:
+    [ [ "|"; lta = LIST0 OPT tac2expr LEVEL "6" SEP "|" -> lta
+      | -> []
+    ] ]
+  ;
+  tactic_then_gen:
+    [ [ ta = tac2expr; "|"; (first,last) = tactic_then_gen -> (Some ta :: first, last)
+      | ta = tac2expr; ".."; l = tactic_then_last -> ([], Some (Some ta, l))
+      | ".."; l = tactic_then_last -> ([], Some (None, l))
+      | ta = tac2expr -> ([Some ta], None)
+      | "|"; (first,last) = tactic_then_gen -> (None :: first, last)
+      | -> ([None], None)
+    ] ]
+  ;
+  q_dispatch:
+    [ [ d = tactic_then_gen -> Tac2quote.of_dispatch (Loc.tag ~loc:!@loc d) ] ]
+  ;
 END
 
 (** Extension of constr syntax *)
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 1c03cc410d..b8e50ad1df 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -919,6 +919,7 @@ 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_expr_scope "dispatch" Tac2entries.Pltac.q_dispatch
 
 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 1dd8410d2a..729779aef2 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -31,6 +31,7 @@ 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"
+let q_dispatch = Pcoq.Gram.entry_create "tactic:q_dispatch"
 end
 
 (** Tactic definition *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 1fe13cda17..0dd1d5a113 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -64,4 +64,5 @@ 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
+val q_dispatch : raw_tacexpr Pcoq.Gram.entry
 end
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index d5520c54ee..e2bf10f4e2 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -96,3 +96,7 @@ type rewriting_r = {
 }
 
 type rewriting = rewriting_r located
+
+type dispatch_r = raw_tacexpr option list * (raw_tacexpr option * raw_tacexpr option list) option
+
+type dispatch = dispatch_r located
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 57c8a4bbed..73fd7c29c3 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -230,3 +230,12 @@ let of_exact_hyp ?loc id =
   let loc = Option.default dummy_loc loc in
   let refine = CTacRef (AbsKn (TacConstant (control_core "refine"))) in
   CTacApp (loc, refine, [thunk (of_hyp ~loc id)])
+
+let of_dispatch tacs =
+  let loc = Option.default dummy_loc (fst tacs) in
+  let default = function
+  | Some e -> thunk e
+  | None -> thunk (CTacCst (loc, AbsKn (Tuple 0)))
+  in
+  let map e = of_pair default (fun l -> of_list ~loc default l) (Loc.tag ~loc e) in
+  of_pair (fun l -> of_list ~loc default l) (fun r -> of_option ~loc map r) tacs
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index dba3c82715..c02493c554 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -52,3 +52,5 @@ val of_hyp : ?loc:Loc.t -> Id.t located -> raw_tacexpr
 
 val of_exact_hyp : ?loc:Loc.t -> Id.t located -> raw_tacexpr
 (** id ↦ 'Control.refine (fun () => Control.hyp @id') *)
+
+val of_dispatch : dispatch -> raw_tacexpr
diff --git a/tests/tacticals.v b/tests/tacticals.v
index 73f9c03b87..1a2fbcbb37 100644
--- a/tests/tacticals.v
+++ b/tests/tacticals.v
@@ -20,3 +20,15 @@ first [
 | Message.print (Message.of_string "I won't be printed")
 ].
 Qed.
+
+Goal True /\ True.
+Proof.
+Fail split > [ split | |].
+split > [split | split].
+Qed.
+
+Goal True /\ (True -> True) /\ True.
+Proof.
+split > [ | split] > [split | .. | split].
+intros H; refine &H.
+Qed.
diff --git a/theories/Notations.v b/theories/Notations.v
index 97f3042d2b..910b6d5463 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -42,6 +42,16 @@ Ltac2 rec repeat0 (t : unit -> unit) :=
 
 Ltac2 Notation repeat := repeat0.
 
+Ltac2 dispatch0 t ((head, tail)) :=
+  match tail with
+  | None => Control.enter (fun _ => t (); Control.dispatch head)
+  | Some tacs =>
+    let ((def, rem)) := tacs in
+    Control.enter (fun _ => t (); Control.extend head def rem)
+  end.
+
+Ltac2 Notation t(thunk(self)) ">" "[" l(dispatch) "]" : 4 := dispatch0 t l.
+
 Ltac2 do0 n t :=
   let rec aux n t := match Int.equal n 0 with
   | true => ()