def cut.go

lawful-fields@0.1.1.0 · fields.bend:22

import Base
import lawful-bytes@0.1.1.0/defs.bend as D

22# n counts the pieces still wanted, this one included; more says the previous
23# piece ended at a separator; r holds this piece's end.
24def cut.go(+n: Nat, more: Bool, r: D.Bytes & U32, +to: U32, +sep: U32) -> D.Bytes & List<&2, U32>:
25  match n more:
26    case 0n _:
27      (b, e) = r
28      (b, Nil{})
29    case 1n+m False{}:
30      (b, e) = r
31      (b, Nil{})
32    case 1n+m True{}:
33      (b, +e) = r
34      +go = U32.is_lt(e, to)
35      cut.cons(e, cut.go(m, go, cut.next(go && Bool.not(Nat.is_eq(m, 0n)), b, (e + 1 : U32), to, sep), to, sep))