Replay

Record/replay handlers for the capability effects.

record runs an action against the real world, logging each observation into a trace; replay re-runs the same action against a trace, performing no real IO. The trace and its entry type stay private to this module: a caller only ever threads the opaque trace record returns back into replay.

Functions and Values

record

record : forall e0 a. ((Unit) -> a ! {IO, e0}) -> (a, List(Replay@TraceEntry)) ! {IO, e0}

Run action against the real world, logging every capability observation (console, file, random, and environment reads) into a trace. Returns (result, trace); feed the trace to replay to reproduce the run without IO.

replay

replay : forall e0 a. (List(Replay@TraceEntry), (Unit) -> a ! {Fail, e0}) -> a ! {Fail, e0}

Re-run action against a recorded trace, performing no real IO: each capability read is served from the trace and output is dropped, reproducing the original result. Fails if the trace does not match the action.

serialize

serialize : (List(Replay@TraceEntry)) -> String

Encode a trace to a self-delimiting string for durable storage, read back with deserialize.

deserialize

deserialize : (String) -> List(Replay@TraceEntry)

Decode a trace produced by serialize; deserialize(serialize(t)) is t.

durable

durable : forall e0 a. (String, (Unit) -> a ! {Fail, IO, e0}) -> a ! {Fail, IO, e0}

Durable record/replay against a persisted log at path: replay the recorded prefix with no real IO, then perform each new observation for real, appending a frame per observation so an interrupted run resumes where it left off, exactly once at the crash boundary.