Implementing multi-match and simple match over constrs.

2 files changed, 41 insertions, 0 deletions

diff --git a/tests/matching.v b/tests/matching.v
index d21c505cdf..f43e0121ef 100644
--- a/tests/matching.v
+++ b/tests/matching.v
@@ -14,4 +14,14 @@ in
     it commits to a branch*)
 lazy_match! '(nat -> bool) with context [?a] => f a end.
 lazy_match! Control.goal () with ?a -> ?b => Message.print (Message.of_constr b) end.
+
+(** This one works by taking the second match context, i.e. ?a := nat *)
+let b := { contents := true } in
+let f c :=
+  match b.(contents) with
+  | true => b.(contents) := false; fail
+  | false => Message.print (Message.of_constr c)
+  end
+in
+match! '(nat -> bool) with context [?a] => f a end.
 Abort.
diff --git a/theories/Notations.v b/theories/Notations.v
index 93c9dd1798..5ed47336ad 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -38,6 +38,37 @@ Ltac2 lazy_match0 t pats :=
 Ltac2 Notation "lazy_match!" t(tactic(6)) "with" m(constr_matching) "end" :=
   lazy_match0 t m.
 
+Ltac2 multi_match0 t pats :=
+  let rec interp m := match m with
+  | [] => Control.zero Match_failure
+  | p :: m =>
+    match p with
+    | Pattern.ConstrMatchPattern pat f =>
+      Control.plus
+        (fun _ =>
+          let bind := Pattern.matches_vect pat t in
+          f bind
+        )
+        (fun _ => interp m)
+    | Pattern.ConstrMatchContext pat f =>
+      Control.plus
+        (fun _ =>
+          let ((context, bind)) := Pattern.matches_subterm_vect pat t in
+          f context bind
+        )
+        (fun _ => interp m)
+    end
+  end in
+  interp pats.
+
+Ltac2 Notation "multi_match!" t(tactic(6)) "with" m(constr_matching) "end" :=
+  multi_match0 t m.
+
+Ltac2 one_match0 t m := Control.once (fun _ => multi_match0 t m).
+
+Ltac2 Notation "match!" t(tactic(6)) "with" m(constr_matching) "end" :=
+  one_match0 t m.
+
 (** Tacticals *)
 
 Ltac2 orelse t f :=