bytes.bend
bend-kit-bytes@0.3.2.0 · 891 lines · 0 definitions
1# Byte buffers packed four bytes to a U32, with bounds-checked access. Source: https://github.com/paymog/bend-kit/tree/main/bytes
2import Base
3# bend-kit-int@0.2.0.0
4import bend-kit-int@0.2.0.0/int.bend as Int
5
6# Bytes{len, buf}: byte i is bits 8*(i%4) of buf[i/4]. buf has the fewest 2^d words
7# that hold len bytes. Every byte at or past len is 0, so equal buffers have equal words.
8# Out-of-range reads answer None and out-of-range writes do nothing; Array alone would wrap.
9# import ./bytes/bytes.bend as Bytes
10
11type Bytes is Type:
12 Bytes{len: U32, buf: Array<U32>}
13
14def b8(+x: U32) -> U32:
15 (x .&. 255 : U32)
16
17def shift(+i: U32) -> Nat:
18 U32.to_nat(((i .&. 3 : U32) * 8 : U32))
19
20def words(+n: U32) -> U32:
21 ((n + 3 : U32) >> 2n : U32)
22
23# The fewest d with 2^d >= w.
24def depth.go(f: Nat, more: Bool, +w: U32, +d: Nat, +cap: U32) -> Nat:
25 match f:
26 case 0n:
27 d
28 case 1n+p:
29 match more:
30 case False{}:
31 d
32 case True{}:
33 depth.go(p, U32.is_lt((cap * 2 : U32), w), w, 1n+d, (cap * 2 : U32))
34
35def depth(+w: U32) -> Nat:
36 depth.go(32n, U32.is_lt(1, w), w, 0n, 1)
37
38def alloc(+n: U32) -> Array<U32>:
39 Array.new(U32, depth(words(n)), 0)
40
41# Unchecked byte read and write. Callers keep i below len.
42def peek.of(+sh: Nat, r: Array<U32> & U32) -> Array<U32> & U32:
43 (a, w) = r
44 (a, b8(U32.shrn(w, sh)))
45
46def peek(a: Array<U32>, +i: U32) -> Array<U32> & U32:
47 peek.of(shift(i), Array.get(U32, a, (i >> 2n : U32)))
48
49def poke.of(+i: U32, +v: U32, r: Array<U32> & U32) -> Array<U32>:
50 (a, w) = r
51 +sh = shift(i)
52 Array.set(U32, a, (i >> 2n : U32), ((w .&. ((255 << sh) .^. 4294967295)) .|. (b8(v) << sh) : U32))
53
54def poke(a: Array<U32>, +i: U32, +v: U32) -> Array<U32>:
55 poke.of(i, v, Array.get(U32, a, (i >> 2n : U32)))
56
57# n bytes from src[s..] to dst[d..], one byte at a time.
58def copy.go(n: Nat, r: Array<U32> & U32, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
59 match n:
60 case 0n:
61 (a, v) = r
62 (a, dst)
63 case 1n+p:
64 (a, v) = r
65 copy.go(p, peek(a, (s + 1 : U32)), poke(dst, d, v), (s + 1 : U32), (d + 1 : U32))
66
67def copy.bytes(+m: U32, src: Array<U32>, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
68 copy.go(U32.to_nat(m), peek(src, s), dst, s, d)
69
70# n words from src[s..] to dst[d..] (word indexes).
71def copy.words(n: Nat, r: Array<U32> & U32, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
72 match n:
73 case 0n:
74 (a, w) = r
75 (a, dst)
76 case 1n+p:
77 (a, +w) = r
78 copy.words(p, Array.get(U32, a, (s + 1 : U32)), Array.set(U32, dst, d, w), (s + 1 : U32), (d + 1 : U32))
79
80# m bytes to a word-aligned d from an unaligned s: each out word joins two source words.
81# lo = 8*(s%4) and hi = 32 - lo; r holds source word k, prev the word before it.
82def copy.shift(n: Nat, +lo: Nat, +hi: Nat, +prev: U32, r: Array<U32> & U32, dst: Array<U32>, +k: U32, +d: U32) -> Array<U32> & Array<U32>:
83 match n:
84 case 0n:
85 (a, w) = r
86 (a, dst)
87 case 1n+p:
88 (a, +w) = r
89 copy.shift(p, lo, hi, w, Array.get(U32, a, (k + 1 : U32)), Array.set(U32, dst, d, (U32.shrn(prev, lo) .|. U32.shln(w, hi) : U32)), (k + 1 : U32), (d + 1 : U32))
90
91def copy.shift.at(+w: U32, +lo: U32, +k: U32, +d: U32, r: Array<U32> & U32, dst: Array<U32>) -> Array<U32> & Array<U32>:
92 (a, prev) = r
93 copy.shift(U32.to_nat(w), U32.to_nat(lo), U32.to_nat((32 - lo : U32)), prev, Array.get(U32, a, (k + 1 : U32)), dst, (k + 1 : U32), d)
94
95def copy.tail(+m: U32, +s: U32, +d: U32, r: Array<U32> & Array<U32>) -> Array<U32> & Array<U32>:
96 (a, b) = r
97 copy.bytes(m, a, b, s, d)
98
99def copy.pick(aligned: Bool, +m: U32, src: Array<U32>, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
100 match aligned:
101 case True{}:
102 +w = (m >> 2n : U32)
103 +k = (w * 4 : U32)
104 copy.tail((m - k : U32), (s + k : U32), (d + k : U32), copy.words(U32.to_nat(w), Array.get(U32, src, (s >> 2n : U32)), dst, (s >> 2n : U32), (d >> 2n : U32)))
105 case False{}:
106 +w = (m >> 2n : U32)
107 +k = (w * 4 : U32)
108 copy.tail((m - k : U32), (s + k : U32), (d + k : U32), copy.shift.at(w, ((s .&. 3 : U32) * 8 : U32), (s >> 2n : U32), (d >> 2n : U32), Array.get(U32, src, (s >> 2n : U32)), dst))
109
110def copy.dst(daligned: Bool, +m: U32, src: Array<U32>, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
111 match daligned:
112 case False{}:
113 copy.bytes(m, src, dst, s, d)
114 case True{}:
115 copy.pick(U32.is_eq((s .&. 3 : U32), 0), m, src, dst, s, d)
116
117# m bytes from src[s..] to dst[d..]. Whole words when d is word-aligned, shifted when s is not.
118# ponytail: an unaligned d (append after an odd length) copies bytes; merge into d's first word if that gets hot.
119def copy(+m: U32, src: Array<U32>, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
120 copy.dst(U32.is_eq((d .&. 3 : U32), 0), m, src, dst, s, d)
121
122# n zero bytes.
123def new(+n: U32) -> Bytes:
124 Bytes{n, alloc(n)}
125
126def length(b: Bytes) -> Bytes & U32:
127 Bytes{+len, buf} = b
128 (Bytes{len, buf}, len)
129
130def get.some(+len: U32, r: Array<U32> & U32) -> Bytes & Maybe<&2, U32>:
131 (a, v) = r
132 (Bytes{len, a}, Some{v})
133
134def get.if(ok: Bool, +len: U32, buf: Array<U32>, +i: U32) -> Bytes & Maybe<&2, U32>:
135 match ok:
136 case True{}:
137 get.some(len, peek(buf, i))
138 case False{}:
139 (Bytes{len, buf}, None{})
140
141# Byte i, or None when i >= len.
142def get(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>:
143 Bytes{+len, buf} = b
144 get.if(U32.is_lt(i, len), len, buf, i)
145
146def set.if(ok: Bool, +len: U32, buf: Array<U32>, +i: U32, +v: U32) -> Bytes:
147 match ok:
148 case True{}:
149 Bytes{len, poke(buf, i, v)}
150 case False{}:
151 Bytes{len, buf}
152
153# Byte i becomes v & 255. Nothing changes when i >= len.
154def set(b: Bytes, +i: U32, +v: U32) -> Bytes:
155 Bytes{+len, buf} = b
156 set.if(U32.is_lt(i, len), len, buf, i, v)
157
158# The next index: one forward when up, one back when not.
159def step(+up: Bool, +i: U32) -> U32:
160 Bool.pick(U32, up, (i + 1 : U32), (i - 1 : U32))
161
162# Do n bytes from i fit in len?
163def fits(+len: U32, +i: U32, +n: U32) -> Bool:
164 Bool.and(U32.is_le(n, len), U32.is_le(i, (len - n : U32)))
165
166# n bytes from j, each shifted in below the ones before: the first byte read is the most significant.
167def uint.go(n: Nat, r: Array<U32> & U32, +j: U32, +up: Bool, +acc: U32) -> Array<U32> & U32:
168 match n:
169 case 0n:
170 (a, v) = r
171 (a, acc)
172 case 1n+p:
173 (a, +v) = r
174 uint.go(p, peek(a, step(up, j)), step(up, j), up, ((acc << 8n) .|. v : U32))
175
176# Big-endian reads forward from i; little-endian reads back from the last byte.
177def uint.if(ok: Bool, +len: U32, buf: Array<U32>, +i: U32, +n: U32, +be: Bool) -> Bytes & Maybe<&2, U32>:
178 match ok:
179 case True{}:
180 +j = Bool.pick(U32, be, i, (i + n - 1 : U32))
181 get.some(len, uint.go(U32.to_nat(n), peek(buf, j), j, be, 0))
182 case False{}:
183 (Bytes{len, buf}, None{})
184
185def uint(b: Bytes, +i: U32, +n: U32, +be: Bool) -> Bytes & Maybe<&2, U32>:
186 Bytes{+len, buf} = b
187 uint.if(fits(len, i, n), len, buf, i, n, be)
188
189# Unsigned integers at byte i, or None when they run past len.
190# be: most significant byte first (network order); le: least significant first.
191def get.u16be(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>:
192 uint(b, i, 2, True{})
193
194def get.u16le(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>:
195 uint(b, i, 2, False{})
196
197def get.u32be(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>:
198 uint(b, i, 4, True{})
199
200def get.u32le(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>:
201 uint(b, i, 4, False{})
202
203# n bytes of v from j, least significant first.
204def put.go(n: Nat, a: Array<U32>, +j: U32, +up: Bool, +v: U32) -> Array<U32>:
205 match n:
206 case 0n:
207 a
208 case 1n+p:
209 put.go(p, poke(a, j, v), step(up, j), up, U32.shrn(v, 8n))
210
211# Little-endian writes forward from i; big-endian writes back from the last byte.
212def put.if(ok: Bool, +len: U32, buf: Array<U32>, +i: U32, +n: U32, +be: Bool, +v: U32) -> Bytes:
213 match ok:
214 case True{}:
215 Bytes{len, put.go(U32.to_nat(n), buf, Bool.pick(U32, be, (i + n - 1 : U32), i), Bool.not(be), v)}
216 case False{}:
217 Bytes{len, buf}
218
219def put(b: Bytes, +i: U32, +n: U32, +be: Bool, +v: U32) -> Bytes:
220 Bytes{+len, buf} = b
221 put.if(fits(len, i, n), len, buf, i, n, be, v)
222
223# v's low 16 or 32 bits at byte i. Nothing changes when they would run past len.
224def set.u16be(b: Bytes, +i: U32, +v: U32) -> Bytes:
225 put(b, i, 2, True{}, v)
226
227def set.u16le(b: Bytes, +i: U32, +v: U32) -> Bytes:
228 put(b, i, 2, False{}, v)
229
230def set.u32be(b: Bytes, +i: U32, +v: U32) -> Bytes:
231 put(b, i, 4, True{}, v)
232
233def set.u32le(b: Bytes, +i: U32, +v: U32) -> Bytes:
234 put(b, i, 4, False{}, v)
235
236# The U64 whose words, in byte order, are x then y.
237def u64.of(be: Bool, +x: U32, +y: U32) -> Int.U64:
238 match be:
239 case True{}:
240 Int.U64.or(Int.U64.shl(Int.U64.from_u32(x), 32n), Int.U64.from_u32(y))
241 case False{}:
242 Int.U64.or(Int.U64.shl(Int.U64.from_u32(y), 32n), Int.U64.from_u32(x))
243
244def u64.join(+be: Bool, x: Maybe<&2, U32>, y: Maybe<&2, U32>) -> Maybe<&2, Int.U64>:
245 match x y:
246 case Some{a} Some{c}:
247 Some{u64.of(be, a, c)}
248 case _ _:
249 None{}
250
251def u64.lo(+be: Bool, x: Maybe<&2, U32>, r: Bytes & Maybe<&2, U32>) -> Bytes & Maybe<&2, Int.U64>:
252 (b, y) = r
253 (b, u64.join(be, x, y))
254
255def u64.hi(+i: U32, +be: Bool, r: Bytes & Maybe<&2, U32>) -> Bytes & Maybe<&2, Int.U64>:
256 (b, x) = r
257 u64.lo(be, x, uint(b, (i + 4 : U32), 4, be))
258
259def u64(b: Bytes, +i: U32, +be: Bool) -> Bytes & Maybe<&2, Int.U64>:
260 u64.hi(i, be, uint(b, i, 4, be))
261
262# A U64 at byte i, or None when its 8 bytes run past len.
263def get.u64be(b: Bytes, +i: U32) -> Bytes & Maybe<&2, Int.U64>:
264 u64(b, i, True{})
265
266def get.u64le(b: Bytes, +i: U32) -> Bytes & Maybe<&2, Int.U64>:
267 u64(b, i, False{})
268
269# Writes words x then y at byte i, both in the same byte order.
270def put64.if(ok: Bool, +len: U32, buf: Array<U32>, +i: U32, +be: Bool, +x: U32, +y: U32) -> Bytes:
271 match ok:
272 case True{}:
273 put(put(Bytes{len, buf}, i, 4, be, x), (i + 4 : U32), 4, be, y)
274 case False{}:
275 Bytes{len, buf}
276
277def put64(b: Bytes, +i: U32, +be: Bool, +v: Int.U64) -> Bytes:
278 Bytes{+len, buf} = b
279 +hi = Int.U64.to_u32(Int.U64.shr(v, 32n))
280 +lo = Int.U64.to_u32(v)
281 put64.if(fits(len, i, 8), len, buf, i, be, Bool.pick(U32, be, hi, lo), Bool.pick(U32, be, lo, hi))
282
283# v at byte i. Nothing changes when its 8 bytes would run past len.
284def set.u64be(b: Bytes, +i: U32, +v: Int.U64) -> Bytes:
285 put64(b, i, True{}, v)
286
287def set.u64le(b: Bytes, +i: U32, +v: Int.U64) -> Bytes:
288 put64(b, i, False{}, v)
289
290# String.length counts in Nat, which costs more than the walk itself.
291def count(s: String, +n: U32) -> U32:
292 match s:
293 case SNil{}:
294 n
295 case SCon{c, t}:
296 count(t, (n + 1 : U32))
297
298# Bytes enter at the top of w and shift down, so a full word has byte 0 lowest.
299def flush(full: Bool, a: Array<U32>, +k: U32, +w: U32) -> Array<U32>:
300 match full:
301 case True{}:
302 Array.set(U32, a, k, w)
303 case False{}:
304 a
305
306def from.go(s: String, a: Array<U32>, +i: U32, +w: U32) -> Array<U32>:
307 match s:
308 case SNil{}:
309 +r = (i .&. 3 : U32)
310 flush(U32.is_ne(r, 0), a, (i >> 2n : U32), U32.shrn(w, U32.to_nat((((4 - r) .&. 3) * 8 : U32))))
311 case SCon{Chr{+c}, t}:
312 +w2 = ((w >> 8n) .|. (b8(c) << 24n) : U32)
313 +full = U32.is_eq((i .&. 3 : U32), 3)
314 from.go(t, flush(full, a, (i >> 2n : U32), w2), (i + 1 : U32), Bool.pick(U32, full, 0, w2))
315
316# A byte string (one Char per octet, as Wire and Http use) to Bytes. Each Char keeps its low 8 bits.
317def from_string(+s: String) -> Bytes:
318 +n = count(s, 0)
319 Bytes{n, from.go(s, alloc(n), 0, 0)}
320
321def to.go(n: Nat, r: Array<U32> & U32, +i: U32, acc: String) -> String:
322 match n:
323 case 0n:
324 acc
325 case 1n+p:
326 (a, v) = r
327 to.go(p, peek(a, (i - 1 : U32)), (i - 1 : U32), SCon{Chr{v}, acc})
328
329# Bytes to a byte string, one Char per octet.
330def to_string(b: Bytes) -> String:
331 Bytes{+len, buf} = b
332 to.go(U32.to_nat(len), peek(buf, (len - 1 : U32)), (len - 1 : U32), SNil{})
333
334def slice.fin(+len: U32, +m: U32, r: Array<U32> & Array<U32>) -> Bytes & Bytes:
335 (a, c) = r
336 (Bytes{len, a}, Bytes{m, c})
337
338def slice.at(+len: U32, buf: Array<U32>, +s: U32, +m: U32) -> Bytes & Bytes:
339 slice.fin(len, m, copy(m, buf, alloc(m), s, 0))
340
341# The buffer back, and a copy of up to n bytes from start. Both ends are clamped to len.
342def slice(b: Bytes, +start: U32, +n: U32) -> Bytes & Bytes:
343 Bytes{+len, buf} = b
344 +s = U32.min(start, len)
345 slice.at(len, buf, s, U32.min(n, (len - s : U32)))
346
347def dst(r: Array<U32> & Array<U32>) -> Array<U32>:
348 (src, out) = r
349 out
350
351# Does a buffer holding len bytes have room for n? Its 2^d words fit the fewest that hold len.
352def room(+len: U32, +n: U32) -> Bool:
353 U32.is_le(words(n), U32.shln(1, depth(words(len))))
354
355def grow.if(fits: Bool, +len: U32, buf: Array<U32>, +n: U32) -> Array<U32>:
356 match fits:
357 case True{}:
358 buf
359 case False{}:
360 dst(copy(len, buf, alloc(n), 0, 0))
361
362# buf, or a copy of its first len bytes in the fewest 2^d words that hold n.
363def grow(+len: U32, buf: Array<U32>, +n: U32) -> Array<U32>:
364 grow.if(room(len, n), len, buf, n)
365
366# a then b. b is written into a's buffer while it has room, and the buffer at least
367# doubles when it runs out, so building a buffer one piece at a time is O(total).
368def append(a: Bytes, b: Bytes) -> Bytes:
369 Bytes{+la, ba} = a
370 Bytes{+lb, bb} = b
371 +n = (la + lb : U32)
372 Bytes{n, dst(copy(lb, bb, grow(la, ba, n), 0, la))}
373
374def concat.total.con(x: Bytes, r: List<&1, Bytes> & U32) -> List<&1, Bytes> & U32:
375 (t, n) = r
376 (Con{x, t}, n)
377
378def concat.total(xs: List<&1, Bytes>, +n: U32) -> List<&1, Bytes> & U32:
379 match xs:
380 case Nil{}:
381 (Nil{}, n)
382 case Con{x, t}:
383 Bytes{+l, buf} = x
384 concat.total.con(Bytes{l, buf}, concat.total(t, (n + l : U32)))
385
386def concat.go(xs: List<&1, Bytes>, out: Array<U32>, +at: U32) -> Array<U32>:
387 match xs:
388 case Nil{}:
389 out
390 case Con{x, t}:
391 Bytes{+l, buf} = x
392 concat.go(t, dst(copy(l, buf, out, 0, at)), (at + l : U32))
393
394def concat.of(r: List<&1, Bytes> & U32) -> Bytes:
395 (xs, +n) = r
396 Bytes{n, concat.go(xs, alloc(n), 0)}
397
398# The pieces in order, in one new buffer: one copy per byte, however many pieces.
399def concat(xs: List<&1, Bytes>) -> Bytes:
400 concat.of(concat.total(xs, 0))
401
402# Does needle match at j? ok is the previous byte's result; the first mismatch stops the walk.
403def at.go(needle: String, ok: Bool, r: Array<U32> & U32, +j: U32) -> Array<U32> & Bool:
404 match needle:
405 case SNil{}:
406 (a, v) = r
407 (a, ok)
408 case SCon{Chr{+c}, t}:
409 match ok:
410 case False{}:
411 (a, v) = r
412 (a, False{})
413 case True{}:
414 (a, +v) = r
415 at.go(t, U32.is_eq(v, c), peek(a, (j + 1 : U32)), (j + 1 : U32))
416
417def at(a: Array<U32>, +needle: String, +j: U32) -> Array<U32> & Bool:
418 at.go(needle, True{}, peek(a, j), j)
419
420# ponytail: naive search; a mismatch costs one byte read per position, but a repetitive needle is O(len * needle). Add a SWAR scan or two-way search if find gets hot.
421# f counts the positions left after i.
422def find.go(f: Nat, r: Array<U32> & Bool, +needle: String, +i: U32, +up: Bool) -> Array<U32> & Maybe<&2, U32>:
423 match f:
424 case 0n:
425 (a, hit) = r
426 (a, Bool.pick(Maybe<&2, U32>, hit, Some{i}, None{}))
427 case 1n+p:
428 (a, hit) = r
429 match hit:
430 case True{}:
431 (a, Some{i})
432 case False{}:
433 find.go(p, at(a, needle, step(up, i)), needle, step(up, i), up)
434
435def find.fin(+len: U32, r: Array<U32> & Maybe<&2, U32>) -> Bytes & Maybe<&2, U32>:
436 (a, x) = r
437 (Bytes{len, a}, x)
438
439def find.at(none: Bool, +len: U32, buf: Array<U32>, +needle: String, +i: U32, +f: U32, +up: Bool) -> Bytes & Maybe<&2, U32>:
440 match none:
441 case True{}:
442 (Bytes{len, buf}, None{})
443 case False{}:
444 find.fin(len, find.go(U32.to_nat(f), at(buf, needle, i), needle, i, up))
445
446# Index of the first match of needle (a byte string) at or after start, or None.
447# An empty needle matches at start when start <= len.
448def find.from(b: Bytes, +needle: String, +start: U32) -> Bytes & Maybe<&2, U32>:
449 Bytes{+len, buf} = b
450 +m = count(needle, 0)
451 find.at(Bool.or(U32.is_lt(len, m), U32.is_lt((len - m : U32), start)), len, buf, needle, start, (len - m - start : U32), True{})
452
453# Index of the first match of needle (a byte string), or None. An empty needle matches at 0.
454def find(b: Bytes, +needle: String) -> Bytes & Maybe<&2, U32>:
455 find.from(b, needle, 0)
456
457# Index of the last match of needle, or None. An empty needle matches at len.
458def rfind(b: Bytes, +needle: String) -> Bytes & Maybe<&2, U32>:
459 Bytes{+len, buf} = b
460 +m = count(needle, 0)
461 find.at(U32.is_lt(len, m), len, buf, needle, (len - m : U32), (len - m : U32), False{})
462
463def at.fin(+len: U32, r: Array<U32> & Bool) -> Bytes & Bool:
464 (a, ok) = r
465 (Bytes{len, a}, ok)
466
467def at.if(fits: Bool, +len: U32, buf: Array<U32>, +needle: String, +j: U32) -> Bytes & Bool:
468 match fits:
469 case True{}:
470 at.fin(len, at(buf, needle, j))
471 case False{}:
472 (Bytes{len, buf}, False{})
473
474# Does b begin with prefix (a byte string)?
475def starts_with(b: Bytes, +prefix: String) -> Bytes & Bool:
476 Bytes{+len, buf} = b
477 +m = count(prefix, 0)
478 at.if(U32.is_le(m, len), len, buf, prefix, 0)
479
480# Does b end with suffix (a byte string)?
481def ends_with(b: Bytes, +suffix: String) -> Bytes & Bool:
482 Bytes{+len, buf} = b
483 +m = count(suffix, 0)
484 at.if(U32.is_le(m, len), len, buf, suffix, (len - m : U32))
485
486# Match positions of sep, latest first, that do not overlap an earlier match.
487# f counts the positions left; skip counts the bytes still inside the last match.
488def split.scan(f: Nat, r: Array<U32> & Bool, +sep: String, +m: U32, +i: U32, +skip: U32, +cuts: List<&2, U32>) -> Array<U32> & List<&2, U32>:
489 match f:
490 case 0n:
491 (a, hit) = r
492 (a, cuts)
493 case 1n+p:
494 (a, +hit) = r
495 +take = Bool.and(hit, U32.is_eq(skip, 0))
496 +next = Bool.pick(U32, take, (m - 1 : U32), Bool.pick(U32, U32.is_eq(skip, 0), 0, (skip - 1 : U32)))
497 split.scan(p, at(a, sep, (i + 1 : U32)), sep, m, (i + 1 : U32), next, Bool.pick(List<&2, U32>, take, Con{i, cuts}, cuts))
498
499def snd(r: Bytes & Bytes) -> Bytes:
500 (a, b) = r
501 b
502
503# r holds the buffer and the piece that ends at end; each earlier cut j starts one at j + m.
504def split.cut(cuts: List<&2, U32>, r: Bytes & Bytes, +end: U32, +m: U32, acc: List<&1, Bytes>) -> List<&1, Bytes>:
505 match cuts:
506 case Nil{}:
507 (b, piece) = r
508 Con{snd(slice(b, 0, end)), Con{piece, acc}}
509 case Con{+j, t}:
510 (b, piece) = r
511 split.cut(t, slice(b, (j + m : U32), (end - j - m : U32)), j, m, Con{piece, acc})
512
513def split.of(cuts: List<&2, U32>, b: Bytes, +len: U32, +m: U32) -> List<&1, Bytes>:
514 match cuts:
515 case Nil{}:
516 Con{b, Nil{}}
517 case Con{+j, t}:
518 split.cut(t, slice(b, (j + m : U32), (len - j - m : U32)), j, m, Nil{})
519
520def split.run(+len: U32, +m: U32, r: Array<U32> & List<&2, U32>) -> List<&1, Bytes>:
521 (a, cuts) = r
522 split.of(cuts, Bytes{len, a}, len, m)
523
524def split.if(whole: Bool, +len: U32, buf: Array<U32>, +sep: String, +m: U32) -> List<&1, Bytes>:
525 match whole:
526 case True{}:
527 Con{Bytes{len, buf}, Nil{}}
528 case False{}:
529 split.run(len, m, split.scan(U32.to_nat((len - m + 1 : U32)), at(buf, sep, 0), sep, m, 0, 0, Nil{}))
530
531# The pieces between matches of sep (a byte string), left to right. n matches give n + 1
532# pieces, so a match at either end gives an empty piece. An empty sep gives b whole.
533def split(b: Bytes, +sep: String) -> List<&1, Bytes>:
534 Bytes{+len, buf} = b
535 +m = count(sep, 0)
536 split.if(Bool.or(U32.is_eq(m, 0), U32.is_lt(len, m)), len, buf, sep, m)
537
538# Compares whole words; same tells whether the previous pair matched.
539def eq.go(n: Nat, same: Bool, r: Array<U32> & U32, s: Array<U32> & U32, +i: U32) -> Array<U32> & Array<U32> & Bool:
540 match n:
541 case 0n:
542 (x, v) = r
543 (y, w) = s
544 (x, y, same)
545 case 1n+p:
546 match same:
547 case False{}:
548 (x, v) = r
549 (y, w) = s
550 (x, y, False{})
551 case True{}:
552 (x, +v) = r
553 (y, +w) = s
554 eq.go(p, U32.is_eq(v, w), Array.get(U32, x, (i + 1 : U32)), Array.get(U32, y, (i + 1 : U32)), (i + 1 : U32))
555
556def eq.fin(+la: U32, +lb: U32, r: Array<U32> & Array<U32> & Bool) -> Bytes & Bytes & Bool:
557 (x, y, ok) = r
558 (Bytes{la, x}, Bytes{lb, y}, ok)
559
560def eq.len(same: Bool, +la: U32, xa: Array<U32>, +lb: U32, ya: Array<U32>) -> Bytes & Bytes & Bool:
561 match same:
562 case False{}:
563 (Bytes{la, xa}, Bytes{lb, ya}, False{})
564 case True{}:
565 eq.fin(la, lb, eq.go(U32.to_nat(words(la)), True{}, Array.get(U32, xa, 0), Array.get(U32, ya, 0), 0))
566
567# Both buffers back, and whether they hold the same bytes.
568def eq(a: Bytes, b: Bytes) -> Bytes & Bytes & Bool:
569 Bytes{+la, xa} = a
570 Bytes{+lb, ya} = b
571 eq.len(U32.is_eq(la, lb), la, xa, lb, ya)
572
573# Byte 0 of w becomes the most significant, so words compare in byte order.
574def bswap(+w: U32) -> U32:
575 ((b8(w) << 24n) .|. (b8(U32.shrn(w, 8n)) << 16n) .|. (b8(U32.shrn(w, 16n)) << 8n) .|. U32.shrn(w, 24n) : U32)
576
577# Compares whole words; c is the previous pair's order.
578def cmp.go(n: Nat, c: Cmp, r: Array<U32> & U32, s: Array<U32> & U32, +i: U32) -> Array<U32> & Array<U32> & Cmp:
579 match n:
580 case 0n:
581 (x, v) = r
582 (y, w) = s
583 (x, y, c)
584 case 1n+p:
585 match c:
586 case LT{}:
587 (x, v) = r
588 (y, w) = s
589 (x, y, LT{})
590 case GT{}:
591 (x, v) = r
592 (y, w) = s
593 (x, y, GT{})
594 case EQ{}:
595 (x, +v) = r
596 (y, +w) = s
597 cmp.go(p, U32.cmp(bswap(v), bswap(w)), Array.get(U32, x, (i + 1 : U32)), Array.get(U32, y, (i + 1 : U32)), (i + 1 : U32))
598
599def cmp.len(c: Cmp, +la: U32, +lb: U32) -> Cmp:
600 match c:
601 case EQ{}:
602 U32.cmp(la, lb)
603 case LT{}:
604 LT{}
605 case GT{}:
606 GT{}
607
608def cmp.fin(+la: U32, +lb: U32, r: Array<U32> & Array<U32> & Cmp) -> Bytes & Bytes & Cmp:
609 (x, y, c) = r
610 (Bytes{la, x}, Bytes{lb, y}, cmp.len(c, la, lb))
611
612# Both buffers back, and their order byte by byte; a prefix sorts first.
613# The shorter buffer's bytes past its len are 0, so its last word compares low when only the longer one goes on.
614def cmp(a: Bytes, b: Bytes) -> Bytes & Bytes & Cmp:
615 Bytes{+la, xa} = a
616 Bytes{+lb, ya} = b
617 cmp.fin(la, lb, cmp.go(U32.to_nat(words(U32.min(la, lb))), EQ{}, Array.get(U32, xa, 0), Array.get(U32, ya, 0), 0))
618
619def nibble(+n: U32) -> Char:
620 Chr{Bool.pick(U32, U32.is_lt(n, 10), (48 + n : U32), (87 + n : U32))}
621
622def hex.go(n: Nat, r: Array<U32> & U32, +i: U32, acc: String) -> String:
623 match n:
624 case 0n:
625 acc
626 case 1n+p:
627 (a, +v) = r
628 hex.go(p, peek(a, (i - 1 : U32)), (i - 1 : U32), SCon{nibble(U32.shrn(v, 4n)), SCon{nibble((v .&. 15 : U32)), acc}})
629
630# Two lowercase hex digits per byte.
631def to_hex(b: Bytes) -> String:
632 Bytes{+len, buf} = b
633 hex.go(U32.to_nat(len), peek(buf, (len - 1 : U32)), (len - 1 : U32), SNil{})
634
635def in(+lo: U32, +c: U32, +hi: U32) -> Bool:
636 Bool.and(U32.is_le(lo, c), U32.is_le(c, hi))
637
638# A hex digit's value, or 16.
639def unnibble(+c: U32) -> U32:
640 Bool.pick(U32, in(48, c, 57), (c - 48 : U32), Bool.pick(U32, in(97, c, 102), (c - 87 : U32), Bool.pick(U32, in(65, c, 70), (c - 55 : U32), 16)))
641
642def poke.when(write: Bool, a: Array<U32>, +i: U32, +v: U32) -> Array<U32>:
643 match write:
644 case True{}:
645 poke(a, i, v)
646 case False{}:
647 a
648
649# hi is the previous digit; an odd i completes a byte.
650def unhex.go(s: String, a: Array<U32>, +i: U32, +hi: U32, +ok: Bool) -> Array<U32> & Bool:
651 match s:
652 case SNil{}:
653 (a, ok)
654 case SCon{Chr{+c}, t}:
655 +d = unnibble(c)
656 unhex.go(t, poke.when(U32.is_eq((i .&. 1 : U32), 1), a, (i >> 1n : U32), ((hi << 4n) .|. d : U32)), (i + 1 : U32), d, Bool.and(ok, U32.is_lt(d, 16)))
657
658def decoded(+n: U32, r: Array<U32> & Bool) -> Maybe<&1, Bytes>:
659 (a, ok) = r
660 match ok:
661 case True{}:
662 Some{Bytes{n, a}}
663 case False{}:
664 None{}
665
666def unhex.if(even: Bool, +s: String, +n: U32) -> Maybe<&1, Bytes>:
667 match even:
668 case True{}:
669 decoded((n >> 1n : U32), unhex.go(s, alloc((n >> 1n : U32)), 0, 0, True{}))
670 case False{}:
671 None{}
672
673# Hex digits, either case, to bytes. None for an odd count or a non-hex char.
674def from_hex(+s: String) -> Maybe<&1, Bytes>:
675 +n = count(s, 0)
676 unhex.if(U32.is_eq((n .&. 1 : U32), 0), s, n)
677
678# RFC 4648 §4: the standard alphabet, padded with '='.
679def b64.char(+i: U32) -> U32:
680 Bool.pick(U32, U32.is_lt(i, 26), (65 + i : U32), Bool.pick(U32, U32.is_lt(i, 52), (71 + i : U32), Bool.pick(U32, U32.is_lt(i, 62), (i - 4 : U32), Bool.pick(U32, U32.is_eq(i, 62), 43, 47))))
681
682# The six bits of v at k as a base64 char.
683def b64.at(+v: U32, +k: Nat) -> Char:
684 Chr{b64.char((U32.shrn(v, k) .&. 63 : U32))}
685
686# Groups of three bytes, last first; r holds the 24 bits of the group at i.
687def b64.go(n: Nat, r: Array<U32> & U32, +i: U32, acc: String) -> String:
688 match n:
689 case 0n:
690 acc
691 case 1n+p:
692 (a, +v) = r
693 +j = (i - 3 : U32)
694 b64.go(p, uint.go(3n, peek(a, j), j, True{}, 0), j, SCon{b64.at(v, 18n), SCon{b64.at(v, 12n), SCon{b64.at(v, 6n), SCon{b64.at(v, 0n), acc}}}})
695
696# The rem < 3 bytes after the last whole group, then the groups before them.
697def b64.tail(+rem: U32, +t: U32, +q: U32, r: Array<U32> & U32) -> String:
698 (a, +v0) = r
699 +v = U32.shln(v0, U32.to_nat(((3 - rem) * 8 : U32)))
700 +end = Bool.pick(String, U32.is_eq(rem, 0), "", Bool.pick(String, U32.is_eq(rem, 1), SCon{b64.at(v, 18n), SCon{b64.at(v, 12n), "=="}}, SCon{b64.at(v, 18n), SCon{b64.at(v, 12n), SCon{b64.at(v, 6n), "="}}}))
701 +j = (t - 3 : U32)
702 b64.go(U32.to_nat(q), uint.go(3n, peek(a, j), j, True{}, 0), j, end)
703
704# Base64 (RFC 4648 §4) with '=' padding.
705def to_base64(b: Bytes) -> String:
706 Bytes{+len, buf} = b
707 +q = (len / 3 : U32)
708 +t = (q * 3 : U32)
709 b64.tail((len - t : U32), t, q, uint.go(U32.to_nat((len - t : U32)), peek(buf, t), t, True{}, 0))
710
711# A base64 char's value, 64 for '=', or 65.
712def b64.val(+c: U32) -> U32:
713 Bool.pick(U32, in(65, c, 90), (c - 65 : U32), Bool.pick(U32, in(97, c, 122), (c - 71 : U32), Bool.pick(U32, in(48, c, 57), (c + 4 : U32), Bool.pick(U32, U32.is_eq(c, 43), 62, Bool.pick(U32, U32.is_eq(c, 47), 63, Bool.pick(U32, U32.is_eq(c, 61), 64, 65))))))
714
715# The count of '=' at the end of s.
716def b64.pads(s: String, +run: U32) -> U32:
717 match s:
718 case SNil{}:
719 run
720 case SCon{Chr{+c}, t}:
721 b64.pads(t, Bool.pick(U32, U32.is_eq(c, 61), (run + 1 : U32), 0))
722
723# A whole group of four chars writes its bytes at o, as many as fit before len.
724def b64.put(full: Bool, a: Array<U32>, +o: U32, +w: U32, +v: U32) -> Array<U32>:
725 match full:
726 case True{}:
727 put.go(U32.to_nat(w), a, (o + w - 1 : U32), False{}, U32.shrn(v, U32.to_nat(((3 - w) * 8 : U32))))
728 case False{}:
729 a
730
731# v collects six bits per char. '=' is allowed only at body and after.
732def unb64.go(s: String, a: Array<U32>, +i: U32, +v: U32, +ok: Bool, +len: U32, +body: U32) -> Array<U32> & Bool:
733 match s:
734 case SNil{}:
735 (a, ok)
736 case SCon{Chr{+c}, t}:
737 +d = b64.val(c)
738 +v2 = ((v << 6n) .|. (d .&. 63) : U32)
739 +o = ((i >> 2n) * 3 : U32)
740 +good = Bool.pick(Bool, U32.is_lt(i, body), U32.is_lt(d, 64), U32.is_eq(d, 64))
741 unb64.go(t, b64.put(U32.is_eq((i .&. 3 : U32), 3), a, o, U32.min(3, (len - o : U32)), v2), (i + 1 : U32), v2, Bool.and(ok, good), len, body)
742
743def unb64.if(ok: Bool, +s: String, +n: U32, +pads: U32) -> Maybe<&1, Bytes>:
744 match ok:
745 case True{}:
746 +len = ((n >> 2n) * 3 - pads : U32)
747 decoded(len, unb64.go(s, alloc(len), 0, 0, True{}, len, (n - pads : U32)))
748 case False{}:
749 None{}
750
751# Padded base64 (RFC 4648 §4) to bytes. None for a length that is not a multiple of 4,
752# more than two '=', '=' before the end, or a char outside the alphabet.
753def from_base64(+s: String) -> Maybe<&1, Bytes>:
754 +n = count(s, 0)
755 +pads = b64.pads(s, 0)
756 unb64.if(Bool.and(U32.is_eq((n .&. 3 : U32), 0), U32.is_le(pads, 2)), s, n, pads)
757
758# A cursor owns the same packed buffer; start and end bound a region without slicing it.
759type Cursor is Type:
760 Cursor{bytes: Bytes, pos: U32, start: U32, end: U32}
761
762type CursorLimit is Type:
763 CursorLimit{resume: U32, start: U32, end: U32}
764
765def Cursor.new(b: Bytes) -> Cursor:
766 Bytes{+len, buf} = b
767 Cursor{Bytes{len, buf}, 0, 0, len}
768
769def Cursor.finish(c: Cursor) -> Bytes & U32:
770 Cursor{b, pos, start, end} = c
771 (b, pos)
772
773def Cursor.position(c: Cursor) -> Cursor & U32:
774 Cursor{b, +pos, start, end} = c
775 (Cursor{b, pos, start, end}, pos)
776
777def Cursor.remaining(c: Cursor) -> Cursor & U32:
778 Cursor{b, +pos, start, +end} = c
779 (Cursor{b, pos, start, end}, (end - U32.min(pos, end) : U32))
780
781def Cursor.fits(+len: U32, +pos: U32, +start: U32, +end: U32, +n: U32) -> Bool:
782 U32.is_le(start, pos) && U32.is_le(end, len) && fits(end, pos, n)
783
784def Cursor.seek.if(ok: Bool, c: Cursor, +pos: U32) -> Cursor & Bool:
785 match ok:
786 case False{}:
787 (c, False{})
788 case True{}:
789 Cursor{b, old, start, end} = c
790 (Cursor{b, pos, start, end}, True{})
791
792def Cursor.seek(c: Cursor, +pos: U32) -> Cursor & Bool:
793 Cursor{Bytes{+len, buf}, old, +start, +end} = c
794 Cursor.seek.if(Cursor.fits(len, pos, start, end, 0), Cursor{Bytes{len, buf}, old, start, end}, pos)
795
796def Cursor.skip(c: Cursor, +n: U32) -> Cursor & Bool:
797 Cursor{Bytes{+len, buf}, +pos, +start, +end} = c
798 Cursor.seek.if(Cursor.fits(len, pos, start, end, n), Cursor{Bytes{len, buf}, pos, start, end}, (pos + n : U32))
799
800# On success, read inside the region, then leave with the returned affine limit.
801def Cursor.region.if(ok: Bool, c: Cursor, +n: U32) -> Cursor & Maybe<&1, CursorLimit>:
802 match ok:
803 case False{}:
804 (c, None{})
805 case True{}:
806 Cursor{b, +pos, start, end} = c
807 +resume = (pos + n : U32)
808 (Cursor{b, pos, pos, resume}, Some{CursorLimit{resume, start, end}})
809
810def Cursor.region(c: Cursor, +n: U32) -> Cursor & Maybe<&1, CursorLimit>:
811 Cursor{Bytes{+len, buf}, +pos, +start, +end} = c
812 Cursor.region.if(Cursor.fits(len, pos, start, end, n), Cursor{Bytes{len, buf}, pos, start, end}, n)
813
814def Cursor.leave(c: Cursor, limit: CursorLimit) -> Cursor:
815 Cursor{b, pos, start, end} = c
816 CursorLimit{resume, outer_start, outer_end} = limit
817 Cursor{b, resume, outer_start, outer_end}
818
819def Cursor.read.done(~T: Data, +pos: U32, start: U32, end: U32, +n: U32, r: Bytes & Maybe<&2, T>) -> Cursor & Maybe<&2, T>:
820 (b, m) = r
821 match m:
822 case None{}:
823 (Cursor{b, pos, start, end}, None{})
824 case Some{v}:
825 (Cursor{b, (pos + n : U32), start, end}, Some{v})
826
827def Cursor.read.if(~T: Data, ~read: Bytes -> @+i:U32 -> Bytes & Maybe<&2, T>, ok: Bool, c: Cursor, +n: U32) -> Cursor & Maybe<&2, T>:
828 match ok:
829 case False{}:
830 (c, None{})
831 case True{}:
832 Cursor{b, +pos, start, end} = c
833 Cursor.read.done(~T, pos, start, end, n, read(b, pos))
834
835def Cursor.read(~T: Data, ~read: Bytes -> @+i:U32 -> Bytes & Maybe<&2, T>, c: Cursor, +n: U32) -> Cursor & Maybe<&2, T>:
836 Cursor{Bytes{+len, buf}, +pos, +start, +end} = c
837 Cursor.read.if(~T, ~read, Cursor.fits(len, pos, start, end, n), Cursor{Bytes{len, buf}, pos, start, end}, n)
838
839def Cursor.u8(c: Cursor) -> Cursor & Maybe<&2, U32>:
840 Cursor.read(~U32, ~get, c, 1)
841
842def Cursor.u16be(c: Cursor) -> Cursor & Maybe<&2, U32>:
843 Cursor.read(~U32, ~get.u16be, c, 2)
844
845def Cursor.u16le(c: Cursor) -> Cursor & Maybe<&2, U32>:
846 Cursor.read(~U32, ~get.u16le, c, 2)
847
848def Cursor.u32be(c: Cursor) -> Cursor & Maybe<&2, U32>:
849 Cursor.read(~U32, ~get.u32be, c, 4)
850
851def Cursor.u32le(c: Cursor) -> Cursor & Maybe<&2, U32>:
852 Cursor.read(~U32, ~get.u32le, c, 4)
853
854def Cursor.u64be(c: Cursor) -> Cursor & Maybe<&2, Int.U64>:
855 Cursor.read(~Int.U64, ~get.u64be, c, 8)
856
857def Cursor.u64le(c: Cursor) -> Cursor & Maybe<&2, Int.U64>:
858 Cursor.read(~Int.U64, ~get.u64le, c, 8)
859
860def Cursor.write.if(~T: Data, ~write: Bytes -> @+i:U32 -> @+v:T -> Bytes, ok: Bool, c: Cursor, +n: U32, v: T) -> Cursor & Bool:
861 match ok:
862 case False{}:
863 (c, False{})
864 case True{}:
865 Cursor{b, +pos, start, end} = c
866 (Cursor{write(b, pos, v), (pos + n : U32), start, end}, True{})
867
868def Cursor.write(~T: Data, ~write: Bytes -> @+i:U32 -> @+v:T -> Bytes, c: Cursor, +n: U32, v: T) -> Cursor & Bool:
869 Cursor{Bytes{+len, buf}, +pos, +start, +end} = c
870 Cursor.write.if(~T, ~write, Cursor.fits(len, pos, start, end, n), Cursor{Bytes{len, buf}, pos, start, end}, n, v)
871
872def Cursor.put.u8(c: Cursor, v: U32) -> Cursor & Bool:
873 Cursor.write(~U32, ~set, c, 1, v)
874
875def Cursor.put.u16be(c: Cursor, v: U32) -> Cursor & Bool:
876 Cursor.write(~U32, ~set.u16be, c, 2, v)
877
878def Cursor.put.u16le(c: Cursor, v: U32) -> Cursor & Bool:
879 Cursor.write(~U32, ~set.u16le, c, 2, v)
880
881def Cursor.put.u32be(c: Cursor, v: U32) -> Cursor & Bool:
882 Cursor.write(~U32, ~set.u32be, c, 4, v)
883
884def Cursor.put.u32le(c: Cursor, v: U32) -> Cursor & Bool:
885 Cursor.write(~U32, ~set.u32le, c, 4, v)
886
887def Cursor.put.u64be(c: Cursor, v: Int.U64) -> Cursor & Bool:
888 Cursor.write(~Int.U64, ~set.u64be, c, 8, v)
889
890def Cursor.put.u64le(c: Cursor, v: Int.U64) -> Cursor & Bool:
891 Cursor.write(~Int.U64, ~set.u64le, c, 8, v)