lean4
lean4 copied to clipboard
feat: `modifyM`/`modifyGetM` for `IO.Ref`
Adds IO.Ref.modfyM
/ IO.Ref.modifyGetM
which are monadic variants of IO.Ref.modify
(ST.Prim.Ref.modify
) / IO.Ref.modifyGet
(ST.Prim.Ref.modifyGet
). Like them, it uses ST.Prim.Ref.take
to atomically modify the reference via busy-waiting, but allow users to perform BaseIO
actions within the critical section. This is safe because BaseIO
/ ST σ α
actions do not throw exceptions. Without these utilities, to modify a reference while preforming I/O, one needs to use IO.Mutex
. Thus, this provides a lightweight alternative for users.
The outstanding question here is whether this is good idea or if users should be expected to use IO.Mutex
if they wish to modify a reference while performing I/O.