def Drive.read

bend-trace-context@0.2.0.0 · trace_context.bend:982

import Base

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