Simplifications in logic_monad

engine/logic_monad.ml

@@ -37,7 +37,7 @@ exception Tac_Timeout
     interrupts). *)
 exception TacticFailure of exn
 
-let _ = CErrors.register_handler begin function
+let () = CErrors.register_handler begin function
   | Exception e -> Some (CErrors.print e)
   | TacticFailure e -> Some (CErrors.print e)
   | _ -> None
@@ -143,11 +143,9 @@ end
 
 (** A view type for the logical monad, which is a form of list, hence
     we can decompose it with as a list. *)
-type ('a, 'b, 'e) list_view_ =
-  | Nil of 'e
-  | Cons of 'a * 'b
-
-type ('a, 'b, 'e) list_view = ('a, 'e -> 'b, 'e) list_view_
+type ('a, 'e) list_view =
+| Nil of 'e
+| Cons of 'a * ('e -> ('a, 'e) list_view)
 
 module BackState =
 struct
@@ -257,39 +255,29 @@ struct
       m.iolist s nil (fun x s next -> cons x s (fun e -> match f e with None -> next e | Some e -> nil e))
     }
 
-  (** For [reflect] and [split] see the "Backtracking, Interleaving,
-      and Terminating Monad Transformers" paper.  *)
-  type ('a, 'e) reified = { r : ('a, ('a, 'e) reified, 'e) list_view } [@@unboxed]
-
+  (** For [reflect] and [split] see the
+      "Backtracking, Interleaving, and Terminating Monad Transformers" paper.  *)
   let rec reflect0 : type r. _ -> (_ -> r) -> (_ -> _ -> (_ -> r) -> r) -> r =
     fun m nil cons ->
-      match m.r with
+      match m with
       | Nil e -> nil e
       | Cons ((x, s), l) -> cons x s (fun e -> reflect0 (l e) nil cons)
 
-  let reflect (m : ('a * 'o, 'e) reified) =
+  let reflect (m : ('a * 'o, 'e) list_view) =
     { iolist = fun s0 nil cons -> reflect0 m nil cons }
 
-  let split m : (_ list_view, _, _, _) t =
-    let rnil e = Nil e in
-    let rcons p s l = Cons ((p, s), (fun e -> {r=l e})) in
-    { iolist = fun s nil cons ->
-      begin match m.iolist s rnil rcons with
-      | Nil e -> cons (Nil e) s nil
-      | Cons ((x, s), l) ->
-        let l e = reflect (l e) in
-        cons (Cons (x, l)) s nil
-      end }
-
   let run m s =
-    let rnil e = {r=Nil e} in
-    let rcons x s l =
-      let p = (x, s) in
-      {r=Cons (p, l)}
-    in
+    let rnil e = Nil e in
+    let rcons x s l = Cons ((x, s), l) in
     m.iolist s rnil rcons
 
-  let repr x = x.r
+  let split m : (_ result, _, _, _) t =
+    get >>= fun s -> match run m s with
+    | Nil e -> return (Error e)
+    | Cons ((x, s), l) ->
+      let l e = reflect (l e) in
+      set s >> return (Ok (x, l))
+
 end
 
 module type Param = sig
@@ -340,7 +328,7 @@ struct
 
   type iexn = Exninfo.iexn
 
-  type 'a reified = ('a, iexn) BackState.reified
+  type 'a reified = ('a, iexn) list_view
 
   (** Inherited from Backstate *)
 
@@ -361,7 +349,6 @@ struct
   let once = BackState.once
   let break = BackState.break
   let split = BackState.split
-  let repr = BackState.repr
 
   (** State related. We specialize them here to ensure soundness (for reader and
       writer) and efficiency. *)
@@ -393,10 +380,10 @@ struct
 
   let run m r s =
     let s = { wstate = P.wunit; ustate = P.uunit; rstate = r; sstate = s } in
-    let rnil e = {r=Nil e} in
+    let rnil e = Nil e in
     let rcons x s l =
       let p = (x, s.sstate, s.wstate, s.ustate) in
-      {r=Cons (p, l)}
+      Cons (p, l)
     in
     m.iolist s rnil rcons
 

engine/logic_monad.mli

@@ -109,11 +109,9 @@ end
 
 (** A view type for the logical monad, which is a form of list, hence
     we can decompose it with as a list. *)
-type ('a, 'b, 'e) list_view_ =
+type ('a, 'e) list_view =
 | Nil of 'e
-| Cons of 'a * 'b
-
-type ('a, 'b, 'e) list_view = ('a, 'e -> 'b, 'e) list_view_
+| Cons of 'a * ('e -> ('a, 'e) list_view)
 
 module BackState : sig
 
@@ -140,17 +138,13 @@ module BackState : sig
   val plus : ('a, 'i, 'o, 'e) t -> ('e -> ('a, 'i, 'o, 'e) t) -> ('a, 'i, 'o, 'e) t
 
   val split : ('a, 's, 's, 'e) t ->
-    (('a, ('a, 'i, 's, 'e) t, 'e) list_view, 's, 's, 'e) t
+    (('a * ('e -> ('a, 'i, 's, 'e) t), 'e) result, 's, 's, 'e) t
 
   val once : ('a, 'i, 'o, 'e) t -> ('a, 'i, 'o, 'e) t
   val break : ('e -> 'e option) -> ('a, 'i, 'o, 'e) t -> ('a, 'i, 'o, 'e) t
   val lift : 'a NonLogical.t -> ('a, 's, 's, 'e) t
 
-  type ('a, 'e) reified
-
-  val repr : ('a, 'e) reified -> ('a, ('a, 'e) reified, 'e) list_view
-
-  val run : ('a, 'i, 'o, 'e) t -> 'i -> ('a * 'o, 'e) reified
+  val run : ('a, 'i, 'o, 'e) t -> 'i -> ('a * 'o, 'e) list_view
 
 end
 
@@ -195,15 +189,13 @@ module Logical (P:Param) : sig
 
   val zero : Exninfo.iexn -> 'a t
   val plus : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
-  val split : 'a t -> ('a, 'a t, Exninfo.iexn) list_view t
+  val split : 'a t -> ('a * (Exninfo.iexn -> 'a t), Exninfo.iexn) result t
   val once : 'a t -> 'a t
   val break : (Exninfo.iexn -> Exninfo.iexn option) -> 'a t -> 'a t
 
   val lift : 'a NonLogical.t -> 'a t
 
-  type 'a reified = ('a, Exninfo.iexn) BackState.reified
-
-  val repr : 'a reified -> ('a, 'a reified, Exninfo.iexn) list_view
+  type 'a reified = ('a, Exninfo.iexn) list_view
 
   val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w * P.u) reified
 

engine/profile_tactic.ml

@@ -379,8 +379,8 @@ let rec tclWRAPFINALLY before tac finally =
   let open Proofview in
   let open Proofview.Notations in
   before >>= fun v -> tclCASE tac >>= function
-  | Fail (e, info) -> finally v >>= fun () -> tclZERO ~info e
-  | Next (ret, tac') -> tclOR
+  | Error (e, info) -> finally v >>= fun () -> tclZERO ~info e
+  | Ok (ret, tac') -> tclOR
                           (finally v >>= fun () -> tclUNIT ret)
                           (fun e -> tclWRAPFINALLY before (tac' e) finally)
 

engine/proofview.ml

@@ -246,7 +246,7 @@ type +'a tactic = 'a Proof.t
 let apply ~name ~poly env t sp =
   let open Logic_monad in
   NewProfile.profile "Proofview.apply" begin fun () ->
-  match Proof.repr (Proof.run t P.{trace=false; name; poly} (sp,env)) with
+  match Proof.run t P.{trace=false; name; poly} (sp,env) with
   | Nil (e, info) -> Exninfo.iraise (TacticFailure e, info)
   | Cons ((r, (state, env), status, info), _) ->
     r, state, env, status, Trace.to_tree info
@@ -295,29 +295,27 @@ let tclOR = Proof.plus
     [try/with] handler of exception in that it is not a backtracking
     point. *)
 let tclORELSE t1 t2 =
-  let open Logic_monad in
   let open Proof in
   split t1 >>= function
-    | Nil e -> t2 e
-    | Cons (a,t1') -> plus (return a) t1'
+    | Error e -> t2 e
+    | Ok (a,t1') -> plus (return a) t1'
 
 (** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a]
     succeeds at least once then it behaves as [tclBIND a s] otherwise,
     if [a] fails with [e], then it behaves as [f e]. *)
 let tclIFCATCH a s f =
-  let open Logic_monad in
   let open Proof in
   split a >>= function
-    | Nil e -> f e
-    | Cons (x,a') -> plus (s x) (fun e -> (a' e) >>= fun x' -> (s x'))
+    | Error e -> f e
+    | Ok (x,a') -> plus (s x) (fun e -> a' e >>= fun x' -> s x')
 
 (** [tclONCE t] behave like [t] except it has at most one success:
     [tclONCE t] stops after the first success of [t]. If [t] fails
     with [e], [tclONCE t] also fails with [e]. *)
 let tclONCE = Proof.once
 
 exception MoreThanOneSuccess
-let _ = CErrors.register_handler begin function
+let () = CErrors.register_handler begin function
   | MoreThanOneSuccess ->
     Some (Pp.str "This tactic has more than one success.")
   | _ -> None
@@ -332,28 +330,19 @@ end
     [t]. Notice that the choice of [e] is relevant, as the presence of
     further successes may depend on [e] (see {!tclOR}). *)
 let tclEXACTLY_ONCE e t =
-  let open Logic_monad in
   let open Proof in
   split t >>= function
-    | Nil (e, info) -> tclZERO ~info e
-    | Cons (x,k) ->
+    | Error (e, info) -> tclZERO ~info e
+    | Ok (x,k) ->
       let info = Exninfo.null in
       Proof.split (k (e, Exninfo.null)) >>= function
-      | Nil _ -> tclUNIT x
+      | Error _ -> tclUNIT x
       | _ -> tclZERO ~info MoreThanOneSuccess
 
 
 (** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *)
-type 'a case =
-| Fail of Exninfo.iexn
-| Next of 'a * (Exninfo.iexn -> 'a tactic)
-let tclCASE t =
-  let open Logic_monad in
-  let map = function
-  | Nil e -> Fail e
-  | Cons (x, t) -> Next (x, t)
-  in
-  Proof.map map (Proof.split t)
+type 'a case = ('a * (Exninfo.iexn -> 'a tactic), Exninfo.iexn) result
+let tclCASE = Proof.split
 
 let tclBREAK = Proof.break
 
@@ -1022,7 +1011,7 @@ let tclTIMEOUTF n t =
   Proof.current >>= fun envvar ->
   Proof.lift begin
     let open Logic_monad.NonLogical in
-    timeout n (make (fun () -> Proof.repr (Proof.run t envvar initial))) >>= fun r ->
+    timeout n (make (fun () -> Proof.run t envvar initial)) >>= fun r ->
     match r with
     | Error info -> return (Util.Inr (Logic_monad.Tac_Timeout, info))
     | Ok (Logic_monad.Nil e) -> return (Util.Inr e)
@@ -1049,7 +1038,7 @@ let tclALLOCLIMIT n t =
   let t = Proof.lift (Logic_monad.NonLogical.return ()) >> t in
   Proof.get >>= fun initial ->
   Proof.current >>= fun envvar ->
-  let r = Control.alloc_limit n (fun () -> Proof.repr (Proof.run t envvar initial)) () in
+  let r = Control.alloc_limit n (fun () -> Proof.run t envvar initial) () in
   let () = match r with
     | Error _ -> ()
     | Ok (_, {kilowords=n}) ->
@@ -1082,14 +1071,14 @@ let tclTIME s t =
     let open Proof in
     tclUNIT () >>= fun () ->
     let tstart = System.get_time() in
-    Proof.split t >>= let open Logic_monad in function
-    | Nil (e, info) ->
+    Proof.split t >>= function
+    | Error (e, info) ->
       begin
         let tend = System.get_time() in
         pr_time tstart tend n "failure";
         tclZERO ~info e
       end
-    | Cons (x,k) ->
+    | Ok (x,k) ->
         let tend = System.get_time() in
         pr_time tstart tend n "success";
         tclOR (tclUNIT x) (fun e -> aux (n+1) (k e))

engine/proofview.mli

@@ -229,9 +229,7 @@ val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic
 (** [tclCASE t] splits [t] into its first success and a
     continuation. It is the most general primitive to control
     backtracking. *)
-type 'a case =
-  | Fail of Exninfo.iexn
-  | Next of 'a * (Exninfo.iexn -> 'a tactic)
+type 'a case = ('a * (Exninfo.iexn -> 'a tactic), Exninfo.iexn) result
 val tclCASE : 'a tactic -> 'a case tactic
 
 (** [tclBREAK p t] is a generalization of [tclONCE t]. Instead of

plugins/ltac2/tac2core.ml

@@ -1022,10 +1022,10 @@ let () =
 let () =
   define "case" (thunk valexpr @-> tac (result (pair valexpr (fun1 exn valexpr)))) @@ fun f ->
   Proofview.tclCASE (thaw f) >>= begin function
-  | Proofview.Next (x, k) ->
+  | Ok (x, k) ->
     let k (e,info) = set_bt info >>= fun info -> k (e,info) in
     return (Ok (x, k))
-  | Proofview.Fail e -> return (Error e)
+  | Error _ as e -> return e
   end
 
 let () =

tactics/class_tactics.ml

@@ -604,7 +604,7 @@ module Search = struct
             str " of status " ++ pr_goal_status status)
         in
         let rec kont = function
-          | Fail ((NonStuckFailure | StuckGoal as exn), info) when allow_out_of_order ->
+          | Error ((NonStuckFailure | StuckGoal as exn), info) when allow_out_of_order ->
             let () = ppdebug 1 (fun () ->
                 str "Goal " ++ int glid ++
                 str" is stuck or failed without being stuck, trying other tactics.")
@@ -617,13 +617,13 @@ module Search = struct
             in
             cycle 1 (* Puts the first goal last *) <*>
             fixpoint progress tacs ((glid, ev, status, tac) :: stuck) fk (* Launches the search on the rest of the goals *)
-          | Fail ie ->
+          | Error ie ->
             let () = ppdebug 1 (fun () ->
                 str "Goal " ++ int glid ++ str" has no more solutions, returning exception: "
                 ++ pr_internal_exception ie)
             in
             fk ie
-          | Next (res, fk') ->
+          | Ok (res, fk') ->
             let () = ppdebug 1 (fun () ->
                 str "Goal " ++ int glid ++ str" has a success, continuing resolution")
             in