Update operational semantics to impose one-shot continuations
The operational semantics is modified so that the continuation captured by a TryWith
construct can be called at most once by the handler. The idea for accomplishing this is to extend the continuation with a piece of mutable state, which is initialised to true
and updated to false
after the first call. Moreover, in order to resume a continuation, the state must be true
.
Effectively, this is done by extending the continuation constructor ContV
with an extra argument l : loc
, which represents a memory location. So, to recapitulate, now a continuation ContV k l
is the given of a evaluation context k
and a memory location l
. Furthermore, we modify the reduction rules for both the resumption of a continuation and the capture of a raising effect. Indeed, now, when an effect is captured, the handler is called with a continuation built with a newly allocated memory location initialised to true
:
(TryWith (Eff v k) h r); σ → (h v (ContV k l)); σ[l ↦ true]
and a continuation can only be called when this location points to true
:
((ContV k l) w); σ[l ↦ true] → (k[w]); σ[l ↦ false]
Finally, we have also adapted some of the proofs to work with this new semantics, but all of the previous definitions and statements remain valid.