Adding a notation for match goal.

3 files changed, 127 insertions, 48 deletions

diff --git a/tests/matching.v b/tests/matching.v
index f43e0121ef..6bc5706da7 100644
--- a/tests/matching.v
+++ b/tests/matching.v
@@ -1,5 +1,12 @@
 Require Import Ltac2.Ltac2 Ltac2.Notations.
 
+Ltac2 Type exn ::= [ Nope ].
+
+Ltac2 check_id id id' := match Ident.equal id id' with
+| true => ()
+| false => Control.throw Nope
+end.
+
 Goal True -> False.
 Proof.
 Fail
@@ -25,3 +32,21 @@ let f c :=
 in
 match! '(nat -> bool) with context [?a] => f a end.
 Abort.
+
+Goal forall (i j : unit) (x y : nat) (b : bool), True.
+Proof.
+Fail match! goal with
+| [ h : ?t, h' : ?t |- _ ] => ()
+end.
+intros i j x y b.
+match! goal with
+| [ h : ?t, h' : ?t |- _ ] =>
+  check_id h @x;
+  check_id h' @y
+end.
+match! reverse goal with
+| [ h : ?t, h' : ?t |- _ ] =>
+  check_id h @j;
+  check_id h' @i
+end.
+Abort.
diff --git a/theories/Notations.v b/theories/Notations.v
index 8523c0f524..48f3ca0587 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -11,59 +11,34 @@ Require Ltac2.Control Ltac2.Pattern Ltac2.Array Ltac2.Int Ltac2.Std.
 
 (** Constr matching *)
 
-Ltac2 lazy_match0 t pats :=
-  let rec interp m := match m with
-  | [] => Control.zero Match_failure
-  | p :: m =>
-    let next _ := interp m in
-    let ((knd, pat, f)) := p in
-    let p := match knd with
-    | Pattern.MatchPattern =>
-      (fun _ =>
-        let context := Pattern.empty_context () in
-        let bind := Pattern.matches_vect pat t in
-        fun _ => f context bind)
-    | Pattern.MatchContext =>
-      (fun _ =>
-        let ((context, bind)) := Pattern.matches_subterm_vect pat t in
-        fun _ => f context bind)
-    end in
-    Control.plus p next
-  end in
-  let ans := Control.once (fun () => interp pats) in
-  ans ().
-
 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 =>
-    let next _ := interp m in
-    let ((knd, pat, f)) := p in
-    let p := match knd with
-    | Pattern.MatchPattern =>
-      (fun _ =>
-        let context := Pattern.empty_context () in
-        let bind := Pattern.matches_vect pat t in
-        f context bind)
-    | Pattern.MatchContext =>
-      (fun _ =>
-        let ((context, bind)) := Pattern.matches_subterm_vect pat t in
-        f context bind)
-    end in
-    Control.plus p next
-  end in
-  interp pats.
+  Pattern.lazy_match0 t m.
 
 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).
+  Pattern.multi_match0 t m.
 
 Ltac2 Notation "match!" t(tactic(6)) "with" m(constr_matching) "end" :=
-  one_match0 t m.
+  Pattern.one_match0 t m.
+
+(** Goal matching *)
+
+Ltac2 Notation "lazy_match!" "goal" "with" m(goal_matching) "end" :=
+  Pattern.lazy_goal_match0 false m.
+
+Ltac2 Notation "multi_match!" "goal" "with" m(goal_matching) "end" :=
+  Pattern.multi_goal_match0 false m.
+
+Ltac2 Notation "match!" "goal" "with" m(goal_matching) "end" :=
+  Pattern.one_goal_match0 false m.
+
+Ltac2 Notation "lazy_match!" "reverse" "goal" "with" m(goal_matching) "end" :=
+  Pattern.lazy_goal_match0 true m.
+
+Ltac2 Notation "multi_match!" "reverse" "goal" "with" m(goal_matching) "end" :=
+  Pattern.multi_goal_match0 true m.
+
+Ltac2 Notation "match!" "reverse" "goal" "with" m(goal_matching) "end" :=
+  Pattern.one_goal_match0 true m.
 
 (** Tacticals *)
 
diff --git a/theories/Pattern.v b/theories/Pattern.v
index fb450d9dfa..2c93918aee 100644
--- a/theories/Pattern.v
+++ b/theories/Pattern.v
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 Require Import Ltac2.Init.
+Require Ltac2.Control.
 
 Ltac2 Type t := pattern.
 
@@ -64,3 +65,81 @@ Ltac2 @ external matches_goal : bool -> (match_kind * t) list -> (match_kind * t
 Ltac2 @ external instantiate : context -> constr -> constr :=
   "ltac2" "pattern_instantiate".
 (** Fill the hole of a context with the given term. *)
+
+(** Implementation of Ltac matching over terms and goals *)
+
+Ltac2 lazy_match0 t pats :=
+  let rec interp m := match m with
+  | [] => Control.zero Match_failure
+  | p :: m =>
+    let next _ := interp m in
+    let ((knd, pat, f)) := p in
+    let p := match knd with
+    | MatchPattern =>
+      (fun _ =>
+        let context := empty_context () in
+        let bind := matches_vect pat t in
+        fun _ => f context bind)
+    | MatchContext =>
+      (fun _ =>
+        let ((context, bind)) := matches_subterm_vect pat t in
+        fun _ => f context bind)
+    end in
+    Control.plus p next
+  end in
+  Control.once (fun () => interp pats) ().
+
+Ltac2 multi_match0 t pats :=
+  let rec interp m := match m with
+  | [] => Control.zero Match_failure
+  | p :: m =>
+    let next _ := interp m in
+    let ((knd, pat, f)) := p in
+    let p := match knd with
+    | MatchPattern =>
+      (fun _ =>
+        let context := empty_context () in
+        let bind := matches_vect pat t in
+        f context bind)
+    | MatchContext =>
+      (fun _ =>
+        let ((context, bind)) := matches_subterm_vect pat t in
+        f context bind)
+    end in
+    Control.plus p next
+  end in
+  interp pats.
+
+Ltac2 one_match0 t m := Control.once (fun _ => multi_match0 t m).
+
+Ltac2 lazy_goal_match0 rev pats :=
+  let rec interp m := match m with
+  | [] => Control.zero Match_failure
+  | p :: m =>
+    let next _ := interp m in
+    let ((pat, f)) := p in
+    let ((phyps, pconcl)) := pat in
+    let cur _ :=
+      let ((hids, hctx, subst, cctx)) := matches_goal rev phyps pconcl in
+      fun _ => f hids hctx subst cctx
+    in
+    Control.plus cur next
+  end in
+  interp pats ().
+
+Ltac2 multi_goal_match0 rev pats :=
+  let rec interp m := match m with
+  | [] => Control.zero Match_failure
+  | p :: m =>
+    let next _ := interp m in
+    let ((pat, f)) := p in
+    let ((phyps, pconcl)) := pat in
+    let cur _ :=
+      let ((hids, hctx, subst, cctx)) := matches_goal rev phyps pconcl in
+      f hids hctx subst cctx
+    in
+    Control.plus cur next
+  end in
+  interp pats.
+
+Ltac2 one_goal_match0 rev pats := Control.once (fun _ => multi_goal_match0 rev pats).