Implementing lazy matching over terms.

2 files changed, 39 insertions, 2 deletions

diff --git a/theories/Notations.v b/theories/Notations.v
index 411367eab1..93c9dd1798 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -7,7 +7,36 @@
 (************************************************************************)
 
 Require Import Ltac2.Init.
-Require Ltac2.Control Ltac2.Int Ltac2.Std.
+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 =>
+    match p with
+    | Pattern.ConstrMatchPattern pat f =>
+      Control.plus
+        (fun _ =>
+          let bind := Pattern.matches_vect pat t in
+          fun _ => f bind
+        )
+        (fun _ => interp m)
+    | Pattern.ConstrMatchContext pat f =>
+      Control.plus
+        (fun _ =>
+          let ((context, bind)) := Pattern.matches_subterm_vect pat t in
+          fun _ => f context bind
+        )
+        (fun _ => interp m)
+    end
+  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.
 
 (** Tacticals *)
 
diff --git a/theories/Pattern.v b/theories/Pattern.v
index ab3135f189..a672ad0fe7 100644
--- a/theories/Pattern.v
+++ b/theories/Pattern.v
@@ -14,7 +14,7 @@ Ltac2 Type context.
 
 Ltac2 Type 'a constr_match := [
 | ConstrMatchPattern (pattern, constr array -> 'a)
-| ConstrMatchContext (pattern, constr -> constr array -> 'a)
+| ConstrMatchContext (pattern, context -> constr array -> 'a)
 ].
 
 Ltac2 @ external matches : t -> constr -> (ident * constr) list :=
@@ -30,6 +30,14 @@ Ltac2 @ external matches_subterm : t -> constr -> context * ((ident * constr) li
     value compared to [matches] is the context of the match, to be filled with
     the instantiate function. *)
 
+Ltac2 @ external matches_vect : t -> constr -> constr array :=
+  "ltac2" "pattern_matches_vect".
+(** Internal version of [matches] that does not return the identifiers. *)
+
+Ltac2 @ external matches_subterm_vect : t -> constr -> context * constr array :=
+  "ltac2" "pattern_matches_subterm_vect".
+(** Internal version of [matches_subterms] that does not return the identifiers. *)
+
 Ltac2 @ external instantiate : context -> constr -> constr :=
   "ltac2" "pattern_instantiate".
 (** Fill the hole of a context with the given term. *)