Add a backtracking version of Ltac's [match].

[multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well.

5 files changed, 40 insertions, 19 deletions

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 1a11b00282..e3d910f321 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -289,6 +289,11 @@ let mlexpr_of_pattern_ast = mlexpr_of_constr
 let mlexpr_of_entry_type = function
     _ -> failwith "mlexpr_of_entry_type: TODO"
 
+let mlexpr_of_match_lazy_flag = function
+  | Tacexpr.General -> <:expr<Tacexpr.General>>
+  | Tacexpr.Lazy    -> <:expr<Tacexpr.Lazy>>
+  | Tacexpr.Once    -> <:expr<Tacexpr.Once>>
+
 let mlexpr_of_match_pattern = function
   | Tacexpr.Term t -> <:expr< Tacexpr.Term $mlexpr_of_pattern_ast t$ >>
   | Tacexpr.Subterm (b,ido,t) ->
@@ -479,12 +484,12 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
       <:expr< Tacexpr.TacLetIn $mlexpr_of_bool isrec$ $mlexpr_of_list f l$ $mlexpr_of_tactic t$ >>
   | Tacexpr.TacMatch (lz,t,l) ->
       <:expr< Tacexpr.TacMatch
-        $mlexpr_of_bool lz$
+        $mlexpr_of_match_lazy_flag lz$
         $mlexpr_of_tactic t$
         $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>>
   | Tacexpr.TacMatchGoal (lz,lr,l) ->
       <:expr< Tacexpr.TacMatchGoal
-        $mlexpr_of_bool lz$
+        $mlexpr_of_match_lazy_flag lz$
         $mlexpr_of_bool lr$
         $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>>
 
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 0c2b754788..7c898b75eb 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -20,7 +20,11 @@ open Misctypes
 open Locus
 
 type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
-type lazy_flag = bool      (* true = lazy             false = eager *)
+type lazy_flag =
+  | General (* returns all possible successes *)
+  | Lazy    (* returns all successes of the first matching branch *)
+  | Once    (* returns the first success in a maching branch
+               (not necessarily the first) *)
 type evars_flag = bool     (* true = pose evars       false = fail on evars *)
 type rec_flag = bool       (* true = recursive        false = not recursive *)
 type advanced_flag = bool  (* true = advanced         false = basic *)
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index b2b1d5adea..fa2c111a68 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -172,7 +172,9 @@ GEXTEND Gram
       | "()" -> TacGeneric (genarg_of_unit ()) ] ]
   ;
   match_key:
-    [ [ "match" -> false | "lazymatch" -> true ] ]
+    [ [ "match" -> Once
+      | "lazymatch" -> Lazy
+      | "multimatch" -> General ] ]
   ;
   input_fun:
     [ [ "_" -> None
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index d43b94ec4b..ddb85a3626 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -621,7 +621,10 @@ module Make
     | FullInversion -> primitive "inversion"
     | FullInversionClear -> primitive "inversion_clear"
 
-  let pr_lazy lz = if lz then keyword "lazy" else mt ()
+  let pr_lazy = function
+    | General -> keyword "multi"
+    | Lazy -> keyword "lazy"
+    | Once -> mt ()
 
   let pr_match_pattern pr_pat = function
     | Term a -> pr_pat a
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index bbeb23c781..a8da8c81f5 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1547,20 +1547,27 @@ and interp_match_success ist { TacticMatching.subst ; context ; terms ; lhs } =
     matching of successes [s]. If [lz] is set to true, then only the
     first success is considered, otherwise further successes are tried
     if the left-hand side fails. *)
-and interp_match_successes lz ist tac =
-    if lz then
-      (** Only keep the first matching result, we don't backtrack on it *)
-      let tac = Proofview.tclONCE tac in
-      tac >>= fun ans -> interp_match_success ist ans
-    else
-      let break (e, info) = match e with
-      | FailError (0, _) -> None
-      | FailError (n, s) -> Some (FailError (pred n, s), info)
-      | _ -> None
-      in
-      let tac = Proofview.tclBREAK break tac >>= fun ans -> interp_match_success ist ans in
-      (** Once a tactic has succeeded, do not backtrack anymore *)
-      Proofview.tclONCE tac
+and interp_match_successes lz ist s =
+   let general =
+     let break (e, info) = match e with
+       | FailError (0, _) -> None
+       | FailError (n, s) -> Some (FailError (pred n, s), info)
+       | _ -> None
+     in
+     Proofview.tclBREAK break s >>= fun ans -> interp_match_success ist ans
+   in
+    match lz with
+    | General ->
+        general
+    | Lazy ->
+      begin
+        (** Only keep the first matching result, we don't backtrack on it *)
+        let s = Proofview.tclONCE s in
+        s >>= fun ans -> interp_match_success ist ans
+      end
+    | Once ->
+        (** Once a tactic has succeeded, do not backtrack anymore *)
+        Proofview.tclONCE general
 
 (* Interprets the Match expressions *)
 and interp_match ist lz constr lmr =