Insn.bpf_decode.go: def of bend-osdev-bpf@0.1.0.0
Import: import bend-osdev-bpf@0.1.0.0/insn.bend as Insn
Lines 349-364 of bend-osdev-bpf@0.1.0.0/insn.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&start_line=349&end_line=364

import Base

# a: the instructions before pc, last first, or the first failure; the loop
# stops at the instruction after a failure
def bpf_decode.go(rs: List<&2, BpfRaw>, +pc: Nat, a: Result<&2, &2, BpfError, List<&2, BpfOp>>) -> Result<&2, &2, BpfError, List<&2, BpfOp>>:
  match rs:
    case Nil{}:
      match a:
        case Fail{e}:
          Fail{e}
        case Done{acc}:
          Done{List.reverse(&2, BpfOp, acc)}
    case Con{+r, t}:
      match a:
        case Fail{e}:
          Fail{e}
        case Done{acc}:
          bpf_decode.go(t, 1n+pc, bpf_decode.push(BpfRaw.decode(r), BpfErrBadCode{pc, BpfRaw.code(r)}, acc))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.reverse
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfError
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfOp
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfRaw
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfRaw.code
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfRaw.decode
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=bpf_decode.push