def Drive.run

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

import Base

967# Drive a machine from a tape, stopping as soon as its step has ended; unread
968# words stay on the tape. `fuel` bounds the steps, which Bend requires for
969# termination; the laws show the budgets suffice.
970def Drive.run(~T: Data, ~D: Data, ~waiting: T -> Maybe<&2, D>, ~feed: Result<&1, &1, U32 & String, U32> -> D -> T,
971  fuel: Nat, current: List<&1, Result<&1, &1, U32 & String, U32>> & (T & Maybe<&2, D>)) ->
972  List<&1, Result<&1, &1, U32 & String, U32>> & T:
973  match fuel current:
974    case _ Tuple{tape, Tuple{step, None{}}}:
975      (tape, step)
976    case 0n Tuple{tape, Tuple{step, Some{draw}}}:
977      (tape, step)
978    case 1n+p Tuple{tape, Tuple{step, Some{draw}}}:
979      Drive.run(~T, ~D, ~waiting, ~feed, p, Drive.fed(~T, ~D, ~waiting, ~feed,
980        List<&1, Result<&1, &1, U32 & String, U32>>, Tape.next(tape), draw))