Skip to content

Collapse NonLogical thunks in the logic monad. #21247

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
coqbot-app merged 2 commits into from
Jan 27, 2026
Merged

Collapse NonLogical thunks in the logic monad. #21247

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
982b082
Bake the NonLogical run in Logic_monad.run.
ppedrot Oct 29, 2025
dd3766e
Collapse NonLogical thunks in the logic monad.
ppedrot Oct 29, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
55 changes: 34 additions & 21 deletions engine/logic_monad.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

@silene silene Dec 2, 2025

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is another possibility: tuples.

Indeed, as far as the OCaml compiler is concerned, there is no difference between a function taking a single tuple argument and a function taking several arguments. For example, the same machine code is generated for f and g below. (Said otherwise, f actually receives 4 separate arguments, in the same order as g.)

let f (a,b,c,d) = a + b + c + d
let g a b c d = a + b + c + d

So, there is no runtime overhead when using tuples. (Obviously, there is some overhead whenever the caller of f needs to destruct the tuple argument on the fly. But it only happens if the argument comes from outside the caller of f. If the tuple is created before the call to f, the compiler recognizes it and optimizes it away.)

In case you wonder how it can even work when f is used as a closure, that is where the infamous caml_tuplify function comes into play. And since caml_tuplify is generally faster than caml_curry (because the resulting closure cannot be partially applied), there is no runtime overhead either when using closures.

@ppedrot ppedrot Dec 2, 2025

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I checked on return and the OCaml compiler doesn't seem to be able to perform this analysis. It does allocate a tuple and performs projections here and there. It's not so surprising either, all these functions are only known at runtime and there is no way it is going to inline all of them... So maybe it helps in some cases, but most of the combinators defined in this file are not going to be optimized.

We discussed the matter with OCaml experts recently, and it seems that OxCaml lets you write such "pure functions" in a way that is tracked by the type system. Basically you have to write a tuplified function and annotate the type with unboxed to achieve this.

@silene silene Dec 2, 2025

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I do not understand. Are you talking about this kind of code?

type ('a, 'i, 'o, 'e) t = { iolist : 'r. 'i * ('e -> 'r) * ('a -> 'o -> ('e -> 'r) -> 'r) -> 'r }

let return x = { iolist = fun (s, nil, cons) -> cons x s nil }

The OCaml compiler does not perform any projection inside the closure stored in iolist. As I explained, it produces the exact same code as if fun s nil cons -> cons x s nil had been written.

@ppedrot ppedrot Dec 2, 2025

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, I also turned the inner arrow type into tuples.

type ('a, 'i, 'o, 'e) t =
  { iolist : 'r. ('i * ('e -> 'r) * ('a * 'o * ('e -> 'r) -> 'r)) -> 'r }

let return x =
  { iolist = fun (s, nil, cons) -> cons (x, s, nil) }

@silene silene Dec 2, 2025

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see. In that case, there will indeed be some overhead. But do you actually need to turn the inner arrow type into a tuple? You should have complete control over all the callers of this inner function since the type of iolist is not exported. So, you can make sure that it is never partially applied.


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 }
Expand All @@ -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 *)

Expand Down Expand Up @@ -243,35 +257,34 @@ 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
type ('a, 'e) reified = ('a, ('a, 'e) reified_, 'e) list_view_
and ('a, 'e) reified_ = {r : 'e -> ('a, 'e) reified} [@@unboxed]

let rec reflect (m : ('a * 'o, 'e) reified) =
{ 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

Expand Down Expand Up @@ -380,10 +393,10 @@ 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

Expand Down
4 changes: 2 additions & 2 deletions engine/logic_monad.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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

Expand Down
16 changes: 8 additions & 8 deletions engine/proofview.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -245,15 +245,15 @@ type +'a tactic = 'a Proof.t
(** Applies a tactic to the current proofview. *)
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
NewProfile.profile "Proofview.apply" begin fun () ->
match Proof.repr (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)
()

r, state, env, status, Trace.to_tree info
| exception (Exception e as src) ->
let (src, info) = Exninfo.capture src in
Exninfo.iraise (e, info)
end ()

(** {7 Monadic primitives} *)

Expand Down Expand Up @@ -1022,7 +1022,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
| Error info -> return (Util.Inr (Logic_monad.Tac_Timeout, info))
| Ok (Logic_monad.Nil e) -> return (Util.Inr e)
Expand Down