def Parse.bytes

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

import bend-trace-context@0.2.0.0/trace_context.bend as TraceContext
import Base
import bend-trace-context@0.2.0.0/src/digits.bend as Digits

833# Consume exactly n cells as bytes, keeping the cells after them. As in
834# Parse.digits, the recursion decreases n, so the result's type has the 2n
835# digits of n bytes.
836def Parse.bytes(n: Nat, bytes: List<&2, U32>, offset: Nat) -> Result<&2, &2, Error, ParsedBytes<n>>:
837  match n:
838    case 0n:
839      Done{ParsedBytes{Digits.DNil{}, bytes}}
840    case 1n+p:
841      match bytes:
842        case Nil{}:
843          Fail{UnexpectedEnd{offset}}
844        case Con{cell, tail}:
845          +at = offset
846          do Result<&2, &2, Error, ParsedBytes<1n+p>>:
847            digits : Digits.Digits(2n) <- Parse.byte(cell, at)
848            parsed : ParsedBytes<p> <- Parse.bytes(p, tail, 1n+at)
849            return ParsedBytes.prepend(p, digits, parsed)

Uses (12)

Used by (1)