cross_handler_reversibility.007

-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
--
-- Example: cross-handler reversibility (Layer 10 rung 3b, static half).
--
-- A `reversible as <name>` block in one handler binds an echo residue that a
-- `reverse <name>` in ANOTHER handler of the same agent can replay — the
-- residue is carried through agent state. This is the cross-handler counterpart
-- to the within-body named residues of rung 3a (see named_reversibility.007).
--
-- The type checker accepts the cross-handler `reverse undo` by PRESENCE: some
-- handler of this agent declares `reversible as undo`. The once-only / linear
-- discipline across handlers is a RUNTIME property — handler firing order is
-- not statically known (cf. `takeForReverse : Maybe` in EchoResidueLinear.idr).

agent ReversibleWorker {
    control {
        -- The happy path binds an undo capability under the name `undo`.
        on receive(amount: Int) {
            reversible as undo {
                let snapshot = amount
            }
        }

        -- On failure, a DIFFERENT handler replays it by name.
        on error(reason: String) {
            reverse undo
        }
    }
}