From 2e613c10f3f332d5b7c506138eb0267ecdd5cc51 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 29 Oct 2025 17:53:22 +0100 Subject: [PATCH 1/2] Bake the NonLogical run in Logic_monad.run. There is no real point in exposing this implementation detail, all callers immediately evaluate the resulting thunk. --- engine/logic_monad.ml | 10 +++++----- engine/logic_monad.mli | 4 ++-- engine/proofview.ml | 3 +-- 3 files changed, 8 insertions(+), 9 deletions(-) diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 1b7f2799e241..7d664a41ead8 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -243,10 +243,10 @@ struct (** For [reflect] and [split] see the "Backtracking, Interleaving, and Terminating Monad Transformers" paper. *) - type ('a, 'e) reified = ('a, ('a, 'e) reified_, 'e) list_view_ NonLogical.t - and ('a, 'e) reified_ = {r : 'e -> ('a, 'e) reified} [@@unboxed] + type ('a, 'e) reified = ('a, ('a, 'e) reified_, 'e) list_view_ + and ('a, 'e) reified_ = {r : 'e -> ('a, 'e) reified NonLogical.t} [@@unboxed] - let rec reflect (m : ('a * 'o, 'e) reified) = + let rec reflect (m : ('a * 'o, 'e) reified NonLogical.t) = { iolist = fun s0 nil cons -> let next = function | Nil e -> nil e @@ -273,7 +273,7 @@ struct let p = (x, s) in NonLogical.return (Cons (p, {r=l})) in - m.iolist s rnil rcons + m.iolist s rnil rcons () let repr x = x end @@ -385,6 +385,6 @@ struct let p = (x, s.sstate, s.wstate, s.ustate) in NonLogical.return (Cons (p, {r=l})) in - m.iolist s rnil rcons + m.iolist s rnil rcons () end diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index 91e6d3e22d88..0f72c2422651 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -148,7 +148,7 @@ module BackState : sig type ('a, 'e) reified type ('a, 'e) reified_ - val repr : ('a, 'e) reified -> ('a, ('a, 'e) reified_, 'e) list_view_ NonLogical.t + val repr : ('a, 'e) reified -> ('a, ('a, 'e) reified_, 'e) list_view_ val run : ('a, 'i, 'o, 'e) t -> 'i -> ('a * 'o, 'e) reified @@ -204,7 +204,7 @@ module Logical (P:Param) : sig type 'a reified = ('a, Exninfo.iexn) BackState.reified type 'a reified_ = ('a, Exninfo.iexn) BackState.reified_ - val repr : 'a reified -> ('a, 'a reified_, Exninfo.iexn) list_view_ NonLogical.t + val repr : 'a reified -> ('a, 'a reified_, Exninfo.iexn) list_view_ val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w * P.u) reified diff --git a/engine/proofview.ml b/engine/proofview.ml index 164f3a70b648..e95bd32e6374 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -247,7 +247,6 @@ let apply ~name ~poly env t sp = let open Logic_monad in NewProfile.profile "Proofview.apply" (fun () -> let ans = Proof.repr (Proof.run t P.{trace=false; name; poly} (sp,env)) in - let ans = Logic_monad.NonLogical.run ans in match ans with | Nil (e, info) -> Exninfo.iraise (TacticFailure e, info) | Cons ((r, (state, env), status, info), _) -> @@ -1032,7 +1031,7 @@ let tclTIMEOUTF n t = Proof.current >>= fun envvar -> Proof.lift begin let open Logic_monad.NonLogical in - timeout n (Proof.repr (Proof.run t envvar initial)) >>= fun r -> + timeout n (make (fun () -> Proof.repr (Proof.run t envvar initial))) >>= fun r -> match r with | None -> return (Util.Inr (Logic_monad.Tac_Timeout, Exninfo.null)) | Some (Logic_monad.Nil e) -> return (Util.Inr e) From 5d4456c037e92d408663d71a71de213af72a821a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 29 Oct 2025 18:13:53 +0100 Subject: [PATCH 2/2] Collapse NonLogical thunks in the logic monad. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We leverage the fact that a ~> unit -> b ≅ a -> b where ~> stands for a hypothetical pure arrow type. This allows replacing all instances of the NonLogical.t monad in the logic monad type with basically nothing, leaving effects implicits in the rightmost arrow type. Since all clients evaluate the thunk directly, the new code should be equivalent to the previous one. Actually, it may even be more correct given that we already implicitly use the function space in the monadic bind operator to perform side-effects. --- engine/logic_monad.ml | 59 ++++++++++++++++++++++++++----------------- 1 file changed, 36 insertions(+), 23 deletions(-) diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 7d664a41ead8..bcaac2194299 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -182,9 +182,23 @@ struct [split] is pattern-matching. *) type ('a, 'i, 'o, 'e) t = - { iolist : 'r. 'i -> ('e -> 'r NonLogical.t) -> - ('a -> 'o -> ('e -> 'r NonLogical.t) -> 'r NonLogical.t) -> - 'r NonLogical.t } + { iolist : 'r. 'i -> ('e -> 'r) -> ('a -> 'o -> ('e -> 'r) -> 'r) -> 'r } + (* IMPORTANT: to play well with side-effects, all functions involved in the + above type must have AT LEAST the same arity as the one implied by their + type. This is to ensure that applying them to the expected arguments only + triggers side-effects once fully applied. If OCaml had a type for pure + functions a ~> b ⊆ a -> b, we could write this type instead as + + type ('a, 'i, 'o, 'e) t = + { iolist : 'r. 'i ~> ('e -> 'r) ~> ('a ~> 'o ~> ('e -> 'r) -> 'r) -> 'r } + + Alternatively we could use records but then it would incur a runtime + overhead. + + An easy way to ensure that is to eta-expand the functions on sight. + + Since the type is abstract in the API, this means we must locally enforce + this property only in this module. *) let return x = { iolist = fun s nil cons -> cons x s nil } @@ -210,7 +224,7 @@ struct { iolist = fun s nil cons -> m.iolist s nil (fun _ s next -> cons () s next) } let lift m = - { iolist = fun s nil cons -> NonLogical.(m >>= fun x -> cons x s nil) } + { iolist = fun s nil cons -> cons (m ()) s nil } (** State related *) @@ -244,36 +258,35 @@ struct (** For [reflect] and [split] see the "Backtracking, Interleaving, and Terminating Monad Transformers" paper. *) type ('a, 'e) reified = ('a, ('a, 'e) reified_, 'e) list_view_ - and ('a, 'e) reified_ = {r : 'e -> ('a, 'e) reified NonLogical.t} [@@unboxed] + and ('a, 'e) reified_ = {r : 'e -> ('a, 'e) reified} [@@unboxed] - let rec reflect (m : ('a * 'o, 'e) reified NonLogical.t) = - { iolist = fun s0 nil cons -> - let next = function + let rec reflect0 : type r. _ -> _ -> _ -> (_ -> r) -> (_ -> _ -> (_ -> r) -> r) -> r = + fun e m s0 nil cons -> + match m e with | Nil e -> nil e - | Cons ((x, s), {r=l}) -> cons x s (fun e -> (reflect (l e)).iolist s0 nil cons) - in - NonLogical.(m >>= next) - } + | Cons ((x, s), {r=l}) -> cons x s (fun e -> reflect0 e l s0 nil cons) + + let reflect (e : 'e) (m : 'e -> ('a * 'o, 'e) reified) = + { iolist = fun s0 nil cons -> reflect0 e m s0 nil cons } let split m : (_ list_view, _, _, _) t = - let rnil e = NonLogical.return (Nil e) in - let rcons p s l = NonLogical.return (Cons ((p, s), {r=l})) in + let rnil e = Nil e in + let rcons p s l = Cons ((p, s), {r=l}) in { iolist = fun s nil cons -> - let open NonLogical in - m.iolist s rnil rcons >>= begin function + begin match m.iolist s rnil rcons with | Nil e -> cons (Nil e) s nil | Cons ((x, s), {r=l}) -> - let l e = reflect (l e) in + let l e = reflect e l in cons (Cons (x, l)) s nil end } let run m s = - let rnil e = NonLogical.return (Nil e) in + let rnil e = Nil e in let rcons x s l = let p = (x, s) in - NonLogical.return (Cons (p, {r=l})) + Cons (p, {r=l}) in - m.iolist s rnil rcons () + m.iolist s rnil rcons let repr x = x end @@ -380,11 +393,11 @@ struct let run m r s = let s = { wstate = P.wunit; ustate = P.uunit; rstate = r; sstate = s } in - let rnil e = NonLogical.return (Nil e) in + let rnil e = Nil e in let rcons x s l = let p = (x, s.sstate, s.wstate, s.ustate) in - NonLogical.return (Cons (p, {r=l})) + Cons (p, {r=l}) in - m.iolist s rnil rcons () + m.iolist s rnil rcons end