Per-node monad decorations

MonadDecoration spec assigns a BundledMonad to each internal node. Strategy.withMonads generalizes Strategy so continuations live in the monad recorded at each node; runWithMonads lifts everything into a single ambient monad.

@[reducible, inline]

abbrev Interaction.Spec.MonadDecoration : Spec → Type (max u (u_1 + 1) (u_2 + 1))

Node-wise choice of monad, as a Decoration valued in BundledMonad.

def Interaction.Spec.Strategy.withMonads (spec : Spec) : spec.MonadDecoration → (spec.Transcript → Type u) → Type u

Strategy type where each node's continuation uses the monad from MonadDecoration.

def Interaction.Spec.Strategy.runWithMonads {m : Type u → Type u} [Monad m] (liftM : (bm : BundledMonad) → {α : Type u} → bm.M α → m α) (spec : Spec) (deco : spec.MonadDecoration) {Output : spec.Transcript → Type u} : withMonads spec deco Output → m ((tr : spec.Transcript) × Output tr)

Execute a withMonads strategy, lifting each node's bundled monad into m.