def run

stelliferous@0.0.2.0 · proofs/traversal_witness.bend:43

import Base
import stelliferous@0.0.2.0/traversal_array.bend as Traversal

43def run(~Reader: Type,~Element: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
44  ~read: Reader -> Context -> U32 -> Reader & Element,~destination: Context -> U32 -> U32,
45  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
46    Sample<Reader,Element,reader,read(reader,context,index)>,
47  +depth: Nat,count: Nat,-reader: Reader,-state: Traversal.State<&1,&1,Reader,Array<Element>,Context>,
48  +reader_evidence: ReaderEvidence(reader),evidence: StateEvidence<Reader,Element,Context,reader,depth,state>) ->
49  StateEvidence<Reader,Element,Context,reader,depth,Traversal.run(~Reader,~Element,~Context,~read,~destination,count,state)>:
50  match count:
51    case 0n: evidence
52    case 1n+rest:
53      run(~Reader,~Element,~Context,~ReaderEvidence,~read,~destination,~read_preserves,depth,rest,reader,
54        Traversal.step(~Reader,~Element,~Context,~read,~destination,state),reader_evidence,
55        step(~Reader,~Element,~Context,~ReaderEvidence,~read,~destination,~read_preserves,depth,reader,state,reader_evidence,evidence))