diff options
| author | Pierre-Marie Pédrot | 2014-07-24 15:11:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-07-24 15:13:12 +0200 |
| commit | ae5ea0c9d5c0e9a39a50a2348b2b8f08938d5f5c (patch) | |
| tree | 2ba9b3c26e3627fe70bf095bdf650c8d375e9176 | |
| parent | fb4187a6d475719bada0a7fe1b7902a36e06d658 (diff) | |
Adding a tail-rec tclONCE.
| -rw-r--r-- | proofs/proofview.ml | 7 | ||||
| -rw-r--r-- | proofs/proofview_gen.ml | 4 | ||||
| -rw-r--r-- | proofs/proofview_monad.mli | 1 |
3 files changed, 6 insertions, 6 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 1797f38f0f..52d8b7d7ca 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -283,12 +283,7 @@ let tclIFCATCH a s f = (* [tclONCE t] fails if [t] fails, otherwise it has exactly one success. *) -let tclONCE t = - (* spiwack: convenience notations, waiting for ocaml 3.12 *) - let (>>=) = Proof.bind in - Proof.split t >>= function - | Nil e -> tclZERO e - | Cons (x,_) -> tclUNIT x +let tclONCE = Proof.once exception MoreThanOneSuccess let _ = Errors.register_handler begin function diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml index 04c3c267d3..9ed3f4bd02 100644 --- a/proofs/proofview_gen.ml +++ b/proofs/proofview_gen.ml @@ -138,6 +138,10 @@ module Logical = (** List observation *) + let once (m : 'a tactic) : 'a tactic = (); fun s -> + let m = m s in + { iolist = fun nil cons -> m.iolist nil (fun x _ -> cons x nil) } + 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 4d4e4470c0..7a86c79698 100644 --- a/proofs/proofview_monad.mli +++ b/proofs/proofview_monad.mli @@ -65,6 +65,7 @@ module Logical : sig val zero : exn -> 'a t 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 lift : 'a NonLogical.t -> 'a t |