bytes.bend

bend-encoding@0.2.0.0 · 40 lines · 0 definitions

1import Base
2
3type Bytes.Error is Data:
4  InvalidByte{index: Nat, value: U32}
5
6type Bytes is Data:
7  Bytes{data: List<&2, U32>}
8
9def Bytes.ok_byte(x: U32) -> Bool:
10  U32.is_le(x, 255)
11
12def Bytes.from_u32_list.go(
13  xs: List<&2, U32>, acc: List<&2, U32>, i: Nat, ok: Bool, +h: U32
14) -> Result<&2, &2, Bytes.Error, Bytes>:
15  match xs ok:
16    case _ False{}:
17      Fail{InvalidByte{i, h}}
18    case Nil{} True{}:
19      Done{Bytes{List.reverse(&2, U32, Con{h, acc})}}
20    case Con{+hh, t} True{}:
21      Bytes.from_u32_list.go(t, Con{h, acc}, 1n+i, Bytes.ok_byte(hh), hh)
22
23def Bytes.from_u32_list.start(
24  xs: List<&2, U32>
25) -> Result<&2, &2, Bytes.Error, Bytes>:
26  match xs:
27    case Nil{}:
28      Done{Bytes{Nil{}}}
29    case Con{+h, t}:
30      Bytes.from_u32_list.go(t, Nil{}, 0n, Bytes.ok_byte(h), h)
31
32def Bytes.from_u32_list(
33  values: List<&2, U32>
34) -> Result<&2, &2, Bytes.Error, Bytes>:
35  Bytes.from_u32_list.start(values)
36
37def Bytes.to_u32_list(b: Bytes) -> List<&2, U32>:
38  match b:
39    case Bytes{data}:
40      data