TraceContext.Drive.read: def of bend-trace-context@0.2.0.0
Import: import bend-trace-context@0.2.0.0/trace_context.bend as TraceContext
Lines 982-998 of bend-trace-context@0.2.0.0/trace_context.bend: https://jend.leeeet.dev/read.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&start_line=982&end_line=998

import Base

# Drive a machine from any source, one word at a time. `read` returns the
# source's next state with each word, and the driver stops as soon as the
# machine's step has ended; the final source state is handed back, so a
# caller can see what was read. `fuel` bounds the words read, as in
# Drive.run. Templates keep this driver free of any host effect: the effect,
# if any, lives in the source.
def Drive.read(~T: Data, ~D: Data, ~waiting: T -> Maybe<&2, D>, ~feed: Result<&1, &1, U32 & String, U32> -> D -> T,
  ~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), fuel: Nat, current: S & (T & Maybe<&2, D>)) ->
  IO(S & T):
  match fuel current:
    case _ Tuple{state, Tuple{step, None{}}}:
      IO.pure(S & T, (state, step))
    case 0n Tuple{state, Tuple{step, Some{draw}}}:
      IO.pure(S & T, (state, step))
    case 1n+p Tuple{state, Tuple{step, Some{draw}}}:
      IO.bind(S & Result<&1, &1, U32 & String, U32>, S & T, read(state),
        got => Drive.read(~T, ~D, ~waiting, ~feed, ~S, ~read, p, Drive.fed(~T, ~D, ~waiting, ~feed, S, got, draw)))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO.bind
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO.pure
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Drive.fed