Exporting a primitive allowing to run completely the tactic monad.

3 files changed, 25 insertions, 10 deletions

diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
index 4df5ab507a..55eb434d38 100644
--- a/proofs/logic_monad.ml
+++ b/proofs/logic_monad.ml
@@ -312,8 +312,13 @@ struct
   let run m r s =
     let s = { wstate = P.wunit; ustate = P.uunit; rstate = r; sstate = s } in
     let m = m s in
-    let nil e = NonLogical.raise (TacticFailure e) in
-    let cons (x, s) _ = NonLogical.return (x, s.sstate, s.wstate, s.ustate) in
-    m.iolist nil cons
+    let rnil e = NonLogical.return (Nil e) in
+    let rcons (x, s) l =
+      let p = (x, s.sstate, s.wstate, s.ustate) in
+      NonLogical.return (Cons (p, l))
+    in
+    m.iolist rnil rcons
+
+  let repr x = x
 
  end
diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli
index a36b017fb0..46cab18d25 100644
--- a/proofs/logic_monad.mli
+++ b/proofs/logic_monad.mli
@@ -148,5 +148,10 @@ module Logical (P:Param) : sig
 
   val lift : 'a NonLogical.t -> 'a t
 
-  val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w * P.u) NonLogical.t
+  type 'a reified
+
+  val repr : 'a reified -> ('a, exn -> 'a reified) list_view NonLogical.t
+
+  val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w * P.u) reified
+
 end
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index e2b92f5649..c850211387 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -223,10 +223,13 @@ type +'a tactic = 'a Proof.t
 
 (** Applies a tactic to the current proofview. *)
 let apply env t sp =
-  let (next_r,(next_state,_),status,info) =
-    Logic_monad.NonLogical.run (Proof.run t false (sp,env))
-  in
-  next_r,next_state,status,Trace.to_tree info
+  let open Logic_monad in
+  let ans = Proof.repr (Proof.run t false (sp,env)) in
+  let ans = Logic_monad.NonLogical.run ans in
+  match ans with
+  | Nil e -> raise (TacticFailure e)
+  | Cons ((r, (state, _), status, info), _) ->
+    r, state, status, Trace.to_tree info
 
 
 
@@ -732,8 +735,10 @@ let tclTIMEOUT n t =
     Logic_monad.NonLogical.catch
       begin
         let open Logic_monad.NonLogical in
-        timeout n (Proof.run t envvar initial) >>= fun r ->
-        return (Util.Inl r)
+        timeout n (Proof.repr (Proof.run t envvar initial)) >>= fun r ->
+        match r with
+        | Logic_monad.Nil e -> return (Util.Inr e)
+        | Logic_monad.Cons (r, _) -> return (Util.Inl r)
       end
       begin let open Logic_monad.NonLogical in function
         | Logic_monad.Timeout -> return (Util.Inr Timeout)