Adding a tclBREAK primitive to the tactic monad.

4 files changed, 15 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 9f2ab30b65..aba7691cd4 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -285,6 +285,8 @@ let tclIFCATCH a s f =
    success. *)
 let tclONCE = Proof.once
 
+let tclBREAK = Proof.break
+
 exception MoreThanOneSuccess
 let _ = Errors.register_handler begin function
   | MoreThanOneSuccess -> Errors.error "This tactic has more than one success."
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 5d093b43b5..6e73e6cc76 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -179,6 +179,12 @@ val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (exn -> 'b tactic) -> 'b tact
    success. *)
 val tclONCE : 'a tactic -> 'a tactic
 
+(* [tclBREAK f t] is a generalization of [tclONCE t]. Instead of stopping at the
+  first element encountered, it waits for the tactic to return an exception
+  satisfying [f], and drop the remaining results. [tclONCE t] is equivalent to
+  [tclBREAK (fun _ -> true) t]. *)
+val tclBREAK : (exn -> bool) -> 'a tactic -> 'a tactic
+
 (* [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one
    success. Otherwise it fails.  It may behave differently than [t] as
    there may be extra non-logical effects used to discover that [t]
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index 9ed3f4bd02..90b730198b 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -142,6 +142,12 @@ module Logical =
     let m = m s in
     { iolist = fun nil cons -> m.iolist nil (fun x _ -> cons x nil) }
 
+  let break (f : exn -> bool) (m : 'a tactic) : 'a tactic = (); fun s ->
+    let m = m s in
+    { iolist = fun nil cons ->
+      m.iolist nil (fun x next -> cons x (fun e -> if f e then nil e else next e))
+    }
+
   type 'a reified = ('a, exn -> 'a reified) list_view IO.t
 
   let rec reflect (m : 'a reified) : 'a iolist =
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index 7a86c79698..6b6f216b0a 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -66,6 +66,7 @@ module Logical : sig
   val plus : 'a t -> (exn -> 'a t) -> 'a t
   val split : 'a t -> (('a,(exn->'a t)) list_view) t
   val once : 'a t -> 'a t
+  val break : (exn -> bool) -> 'a t -> 'a t
 
   val lift : 'a NonLogical.t -> 'a t