Implementing lazy matching over terms.

4 files changed, 92 insertions, 2 deletions

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 39fcff0c73..bbf95c7056 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -544,6 +544,42 @@ let () = define2 "pattern_matches_subterm" begin fun pat c ->
   end
 end
 
+let () = define2 "pattern_matches_vect" begin fun pat c ->
+  let pat = Value.to_pattern pat in
+  let c = Value.to_constr c in
+  pf_apply begin fun env sigma ->
+    let ans =
+      try Some (Constr_matching.matches env sigma pat c)
+      with Constr_matching.PatternMatchingFailure -> None
+    in
+    begin match ans with
+    | None -> Proofview.tclZERO err_matchfailure
+    | Some ans ->
+      let ans = Id.Map.bindings ans in
+      let ans = Array.map_of_list snd ans in
+      return (Value.of_array Value.of_constr ans)
+    end
+  end
+end
+
+let () = define2 "pattern_matches_subterm_vect" begin fun pat c ->
+  let pat = Value.to_pattern pat in
+  let c = Value.to_constr c in
+  let open Constr_matching in
+  let rec of_ans s = match IStream.peek s with
+  | IStream.Nil -> Proofview.tclZERO err_matchfailure
+  | IStream.Cons ({ m_sub = (_, sub); m_ctx }, s) ->
+    let ans = Id.Map.bindings sub in
+    let ans = Array.map_of_list snd ans in
+    let ans = Value.of_tuple [| Value.of_constr m_ctx; Value.of_array Value.of_constr ans |] in
+    Proofview.tclOR (return ans) (fun _ -> of_ans s)
+  in
+  pf_apply begin fun env sigma ->
+    let ans = Constr_matching.match_appsubterm env sigma pat c in
+    of_ans ans
+  end
+end
+
 let () = define2 "pattern_instantiate" begin fun ctx c ->
   let ctx = EConstr.Unsafe.to_constr (Value.to_constr ctx) in
   let c = EConstr.Unsafe.to_constr (Value.to_constr c) in
diff --git a/tests/matching.v b/tests/matching.v
new file mode 100644
index 0000000000..d21c505cdf
--- /dev/null
+++ b/tests/matching.v
@@ -0,0 +1,17 @@
+Require Import Ltac2.Ltac2 Ltac2.Notations.
+
+Goal True -> False.
+Proof.
+Fail
+let b := { contents := true } in
+let f c :=
+  match b.(contents) with
+  | true => Message.print (Message.of_constr c); b.(contents) := false; fail
+  | false => ()
+  end
+in
+(** This fails because the matching is not allowed to backtrack once
+    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.
+Abort.
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. *)