bytes.bend
gralha-bytes@0.1.0.1 · 431 lines · 80 definitions
1
2import Base
3import gralha-text-scan@0.1.0.1/scan.bend as U
4
5
6
7
8
9
10type ByteTree is Data:
11 ByteFlat{value: U32}
12 ByteWord{value: U32}
13 ByteNode{left: ByteTree, right: ByteTree}
14
15def bytes.lane(+index: U32) -> U32:
16 +k = U32.mod(index, 4)
17 U.choose(U32, U32.is_eq(k, 0), 1, U.choose(U32, U32.is_eq(k, 1), 256, U.choose(U32, U32.is_eq(k, 2), 65536, 16777216)))
18
19def bytes.word.get(+word: U32, +index: U32) -> U32:
20 U32.mod(U32.div(word, bytes.lane(index)), 256)
21
22def bytes.word.put(+word: U32, +index: U32, +v: U32) -> U32:
23 +lane = bytes.lane(index)
24 (word - U32.mod(U32.div(word, lane), 256) * lane + v * lane : U32)
25
26type Bytes is Data:
27 Bytes{bufTree: ByteTree, size: U32, capacity: U32}
28
29def bytes.empty() -> Bytes:
30 Bytes{ByteFlat{0}, 0, 1}
31
32@unsafe
33def bytes.tree.get(bufTree: ByteTree, +capacity: U32, +index: U32) -> U32:
34 match bufTree:
35 case ByteFlat{v}: v
36 case ByteWord{v}: bytes.word.get(v, index)
37 case ByteNode{left, right}:
38 +half = (capacity / 2 : U32)
39 bytes.tree.get(U.choose(ByteTree, U32.is_lt(index, half), left, right), half, U32.mod(index, half))
40
41@unsafe
42def bytes.tree.set(+bufTree: ByteTree, +capacity: U32, +index: U32, +v: U32) -> ByteTree:
43 match bufTree:
44 case ByteFlat{old}:
45 U.branch(ByteTree, U32.is_le(capacity, 1), _ => ByteFlat{v}, _ => bytes.tree.set(ByteNode{ByteFlat{old}, ByteFlat{old}}, capacity, index, v))
46 case ByteWord{old}:
47 U.branch(ByteTree, U32.is_le(capacity, 4), _ => ByteWord{bytes.word.put(old, index, v)}, _ => bytes.tree.set(ByteNode{ByteWord{old}, ByteWord{old}}, capacity, index, v))
48 case ByteNode{left, right}:
49 +half = (capacity / 2 : U32)
50 U.branch(ByteTree, U32.is_lt(index, half), _ => ByteNode{bytes.tree.set(left, half, index, v), right}, _ => ByteNode{left, bytes.tree.set(right, half, (index - half : U32), v)})
51
52def bytes.get(bytes: Bytes, +index: U32) -> U32:
53 Bytes{bufTree, size, capacity} = bytes
54 U.branch(U32, U32.is_lt(index, size), _ => bytes.tree.get(bufTree, capacity, index), _ => 0)
55
56def bytes.size(bytes: Bytes) -> U32:
57 Bytes{bufTree, size, capacity} = bytes
58 size
59
60def bytes.set(+bytes: Bytes, +index: U32, v: U32) -> Bytes:
61 Bytes{bufTree, size, capacity} = bytes
62 Bytes{bytes.tree.set(bufTree, capacity, index, v), size, capacity}
63
64def bytes.push(bytes: Bytes, +v: U32) -> Bytes:
65 Bytes{bufTree, size, capacity} = bytes
66 +data = bufTree
67 +n = size
68 +cap = capacity
69 +grow = U32.is_eq(n, cap)
70 +newcap = U.choose(U32, grow, (cap * 2 : U32), cap)
71 Bytes{bytes.tree.set(U.choose(ByteTree, grow, ByteNode{data, ByteFlat{0}}, data), newcap, n, v), U32.inc(n), newcap}
72
73def bytes.string(s: String, acc: Bytes) -> Bytes:
74 match s:
75 case SNil{}: acc
76 case SCon{Chr{c}, t}: bytes.string(t, bytes.push(acc, c))
77
78def bytes.slice(n: Nat, +source: Bytes, +start: U32, target: Bytes) -> Bytes:
79 match n:
80 case 0n: target
81 case 1n+d: bytes.slice(d, source, U32.inc(start), bytes.push(target, bytes.get(source, start)))
82
83@unsafe
84def bytes.be(+bytes: Bytes, +at: U32, count: Nat, acc: U32) -> U32:
85 match count:
86 case 0n: acc
87 case 1n+d: bytes.be(bytes, U32.inc(at), d, (acc * 256 + bytes.get(bytes, at) : U32))
88
89def base64.digit(+c: U32) -> U32:
90 U.choose(U32, U32.is_ge(c, 65) && U32.is_le(c, 90), (c - 65 : U32),
91 U.choose(U32, U32.is_ge(c, 97) && U32.is_le(c, 122), (c - 71 : U32),
92 U.choose(U32, U32.is_ge(c, 48) && U32.is_le(c, 57), (c + 4 : U32), U.choose(U32, U32.is_eq(c, 43), 62, U.choose(U32, U32.is_eq(c, 47), 63, 64)))))
93
94def base64.read(+s: String, +bits: U32, +count: U32, +out: Bytes) -> Bytes:
95 match s:
96 case SNil{}: out
97 case SCon{Chr{c}, t}:
98 +v = base64.digit(c)
99 +n = (count + 6 : U32)
100 +word = (bits * 64 + v : U32)
101 U.branch(Bytes, U32.is_eq(c, 61), _ => out,
102 _ => U.branch(Bytes, U.space(c), _ => base64.read(t, bits, count, out),
103 _ => U.branch(Bytes, U32.is_lt(v, 64), _ => U.branch(Bytes, U32.is_ge(n, 8),
104 _ => base64.read(t, U32.mod(word, U32.shln(1, U32.to_nat((n - 8 : U32)))), (n - 8 : U32), bytes.push(out, U32.shrn(word, U32.to_nat((n - 8 : U32))))),
105 _ => base64.read(t, word, n, out)), _ => bytes.empty())))
106
107def base64(s: String) -> Bytes:
108 base64.read(s, 0, 0, bytes.empty())
109
110type BitStream is Data:
111 BitStream{data: Bytes, position: U32, limit: U32, valid: Bool}
112
113type BitRead is Data:
114 BitRead{value: U32, stream: BitStream}
115
116def bits.read(stream: BitStream, +count: U32) -> BitRead:
117 BitStream{data, position, limit, valid} = stream
118 +src = data
119 +pos = position
120 +end = limit
121 +at = (pos / 8 : U32)
122 +word = (bytes.get(src, at) + bytes.get(src, U32.inc(at)) * 256 + bytes.get(src, (at + 2 : U32)) * 65536 : U32)
123 BitRead{U32.and(U32.shrn(word, U32.to_nat(U32.mod(pos, 8))), (U32.shln(1, U32.to_nat(count)) - 1 : U32)), BitStream{src, (pos + count : U32), end, valid && U32.is_le((pos + count : U32), end)}}
124
125def bits.valid(stream: BitStream) -> Bool:
126 BitStream{data, position, limit, valid} = stream
127 valid && U32.is_le(position, limit)
128
129def bits.invalid(stream: BitStream) -> BitStream:
130 BitStream{data, position, limit, valid} = stream
131 BitStream{data, position, limit, False{}}
132
133def bits.align(+stream: BitStream) -> BitStream:
134 BitStream{data, position, limit, valid} = stream
135 +pos = (((position + 7) / 8) * 8 : U32)
136 BitStream{data, pos, limit, valid && U32.is_le(pos, limit)}
137
138type Huffman is Data:
139 HuffEmpty{}
140 HuffBad{}
141 HuffLeaf{symbol: U32}
142 HuffNode{zero: Huffman, one: Huffman}
143
144@unsafe
145def huff.insert(+node: Huffman, +depth: Nat, +codeword: U32, +symbol: U32) -> Huffman:
146 match node:
147 case HuffBad{}: HuffBad{}
148 case HuffLeaf{old}: HuffBad{}
149 case HuffEmpty{}:
150 match depth:
151 case 0n: HuffLeaf{symbol}
152 case 1n+d: huff.insert(HuffNode{HuffEmpty{}, HuffEmpty{}}, 1n+d, codeword, symbol)
153 case HuffNode{zero, one}:
154 match depth:
155 case 0n: HuffBad{}
156 case 1n+d:
157 +dd = d
158 U.branch(Huffman, U32.is_eq(U32.and(codeword, U32.shln(1, dd)), 0), _ => HuffNode{huff.insert(zero, dd, codeword, symbol), one}, _ => HuffNode{zero, huff.insert(one, dd, codeword, symbol)})
159
160def huff.counts(n: Nat, +lengths: Bytes, +index: U32, +counts: Bytes) -> Bytes:
161 match n:
162 case 0n: counts
163 case 1n+d:
164 +len = bytes.get(lengths, index)
165 huff.counts(d, lengths, U32.inc(index), U.choose(Bytes, U32.is_gt(len, 0) && U32.is_le(len, 15), bytes.set(counts, len, U32.inc(bytes.get(counts, len))), counts))
166
167def huff.codes(n: Nat, +counts: Bytes, +length: U32, codeword: U32, codes: Bytes) -> Bytes:
168 match n:
169 case 0n: codes
170 case 1n+d:
171 +next = ((codeword + bytes.get(counts, (length - 1 : U32))) * 2 : U32)
172 huff.codes(d, counts, U32.inc(length), next, bytes.push(codes, next))
173
174def huff.build.loop(+n: Nat, +lengths: Bytes, +index: U32, +codes: Bytes, +node: Huffman) -> Huffman:
175 match n:
176 case 0n: node
177 case 1n+d:
178 +len = bytes.get(lengths, index)
179 +word = bytes.get(codes, len)
180 U.branch(Huffman, U32.is_eq(len, 0), _ => huff.build.loop(d, lengths, U32.inc(index), codes, node),
181 _ => U.branch(Huffman, U32.is_le(len, 15) && U32.is_lt(word, U32.shln(1, U32.to_nat(len))), _ => huff.build.loop(d, lengths, U32.inc(index), bytes.set(codes, len, U32.inc(word)), huff.insert(node, U32.to_nat(len), word, index)), _ => HuffBad{}))
182
183def huff.build(+lengths: Bytes) -> Huffman:
184 +n = U32.to_nat(bytes.size(lengths))
185 +counts = huff.counts(n, lengths, 0, Bytes{ByteFlat{0}, 16, 16})
186 huff.build.loop(n, lengths, 0, huff.codes(15n, counts, 1, 0, bytes.push(bytes.empty(), 0)), HuffEmpty{})
187
188def huff.read.next(read: BitRead, zero: Huffman, one: Huffman, next: Huffman -> BitStream -> BitRead) -> BitRead:
189 BitRead{bit, stream} = read
190 next(U.choose(Huffman, U32.is_eq(bit, 0), zero, one))(stream)
191
192@unsafe
193def huff.read(node: Huffman, +stream: BitStream) -> BitRead:
194 match node:
195 case HuffEmpty{}: BitRead{0, bits.invalid(stream)}
196 case HuffBad{}: BitRead{0, bits.invalid(stream)}
197 case HuffLeaf{symbol}: BitRead{symbol, stream}
198 case HuffNode{zero, one}: huff.read.next(bits.read(stream, 1), zero, one, node => input => huff.read(node, input))
199
200def huff.fixed.lengths(n: Nat, +index: U32, out: Bytes) -> Bytes:
201 match n:
202 case 0n: out
203 case 1n+d: huff.fixed.lengths(d, U32.inc(index), bytes.push(out, U.choose(U32, U32.is_lt(index, 144), 8, U.choose(U32, U32.is_lt(index, 256), 9, U.choose(U32, U32.is_lt(index, 280), 7, 8)))))
204
205def bytes.repeat(n: Nat, +v: U32, out: Bytes) -> Bytes:
206 match n:
207 case 0n: out
208 case 1n+d: bytes.repeat(d, v, bytes.push(out, v))
209
210def inflate.length.base(index: U32) -> U32:
211 U.uints.nth(Con{3, Con{4, Con{5, Con{6, Con{7, Con{8, Con{9, Con{10, Con{11, Con{13, Con{15, Con{17, Con{19, Con{23, Con{27, Con{31, Con{35, Con{43, Con{51, Con{59, Con{67, Con{83, Con{99, Con{115, Con{131, Con{163, Con{195, Con{227, Con{258, Nil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32.to_nat(index), 0)
212
213def inflate.length.bits(index: U32) -> U32:
214 U.uints.nth(Con{0, Con{0, Con{0, Con{0, Con{0, Con{0, Con{0, Con{0, Con{1, Con{1, Con{1, Con{1, Con{2, Con{2, Con{2, Con{2, Con{3, Con{3, Con{3, Con{3, Con{4, Con{4, Con{4, Con{4, Con{5, Con{5, Con{5, Con{5, Con{0, Nil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32.to_nat(index), 0)
215
216def inflate.distance.base(index: U32) -> U32:
217 U.uints.nth(Con{1, Con{2, Con{3, Con{4, Con{5, Con{7, Con{9, Con{13, Con{17, Con{25, Con{33, Con{49, Con{65, Con{97, Con{129, Con{193, Con{257, Con{385, Con{513, Con{769, Con{1025, Con{1537, Con{2049, Con{3073, Con{4097, Con{6145, Con{8193, Con{12289, Con{16385, Con{24577, Nil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32.to_nat(index), 0)
218
219def inflate.distance.bits(index: U32) -> U32:
220 U.uints.nth(Con{0, Con{0, Con{0, Con{0, Con{1, Con{1, Con{2, Con{2, Con{3, Con{3, Con{4, Con{4, Con{5, Con{5, Con{6, Con{6, Con{7, Con{7, Con{8, Con{8, Con{9, Con{9, Con{10, Con{10, Con{11, Con{11, Con{12, Con{12, Con{13, Con{13, Nil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32.to_nat(index), 0)
221
222def inflate.code.order(index: U32) -> U32:
223 U.uints.nth(Con{16, Con{17, Con{18, Con{0, Con{8, Con{7, Con{9, Con{6, Con{10, Con{5, Con{11, Con{4, Con{12, Con{3, Con{13, Con{2, Con{14, Con{1, Con{15, Nil{}}}}}}}}}}}}}}}}}}}}, U32.to_nat(index), 0)
224
225type Inflate is Data:
226 Inflate{stream: BitStream, output: Bytes}
227
228def inflate.copy(n: Nat, +distance: U32, +out: Bytes) -> Bytes:
229 match n:
230 case 0n: out
231 case 1n+d: inflate.copy(d, distance, bytes.push(out, bytes.get(out, (bytes.size(out) - distance : U32))))
232
233def inflate.distance.extra(read: BitRead, +length: U32, +base: U32, +out: Bytes, limit: U32) -> Inflate:
234 BitRead{extra, stream} = read
235 +input = stream
236 +distance = (base + extra : U32)
237 U.branch(Inflate, bits.valid(input) && U32.is_gt(distance, 0) && U32.is_le(distance, bytes.size(out)) && U32.is_le(length, (limit - bytes.size(out) : U32)),
238 _ => Inflate{input, inflate.copy(U32.to_nat(length), distance, out)}, _ => Inflate{bits.invalid(input), out})
239
240def inflate.distance(read: BitRead, length: U32, out: Bytes, limit: U32) -> Inflate:
241 BitRead{symbol, stream} = read
242 +codeword = symbol
243 +input = stream
244 inflate.distance.extra(bits.read(U.choose(BitStream, U32.is_lt(codeword, 30), input, bits.invalid(input)), inflate.distance.bits(codeword)), length, inflate.distance.base(codeword), out, limit)
245
246def inflate.length.extra(read: BitRead, base: U32, distance: Huffman, out: Bytes, limit: U32) -> Inflate:
247 BitRead{extra, stream} = read
248 inflate.distance(huff.read(distance, stream), (base + extra : U32), out, limit)
249
250def inflate.symbol(read: BitRead, distance: Huffman, +out: Bytes, +limit: U32) -> Inflate:
251 BitRead{symbol, stream} = read
252 +codeword = symbol
253 +input = stream
254 U.branch(Inflate, Bool.not(bits.valid(input)) || U32.is_gt(codeword, 285), _ => Inflate{bits.invalid(input), out},
255 _ => U.branch(Inflate, U32.is_lt(codeword, 256), _ => U.branch(Inflate, U32.is_lt(bytes.size(out), limit), _ => Inflate{input, bytes.push(out, codeword)}, _ => Inflate{bits.invalid(input), out}),
256 _ => inflate.length.extra(bits.read(input, inflate.length.bits((codeword - 257 : U32))), inflate.length.base((codeword - 257 : U32)), distance, out, limit)))
257
258def inflate.codes.next(+result: Inflate, next: BitStream -> Bytes -> Inflate) -> Inflate:
259 Inflate{stream, output} = result
260 U.branch(Inflate, bits.valid(stream), _ => next(stream)(output), _ => result)
261
262def inflate.codes.step(+read: BitRead, distance: Huffman, +out: Bytes, limit: U32, next: BitStream -> Bytes -> Inflate) -> Inflate:
263 BitRead{symbol, stream} = read
264 U.branch(Inflate, U32.is_eq(symbol, 256), _ => Inflate{stream, out}, _ => inflate.codes.next(inflate.symbol(read, distance, out, limit), next))
265
266@unsafe
267def inflate.codes(+literal: Huffman, +distance: Huffman, stream: BitStream, out: Bytes, +limit: U32) -> Inflate:
268 inflate.codes.step(huff.read(literal, stream), distance, out, limit, input => output => inflate.codes(literal, distance, input, output, limit))
269
270def inflate.stored.byte(read: BitRead, out: Bytes, next: BitStream -> Bytes -> Inflate) -> Inflate:
271 BitRead{v, stream} = read
272 next(stream)(bytes.push(out, v))
273
274@unsafe
275def inflate.stored.copy(n: Nat, stream: BitStream, out: Bytes) -> Inflate:
276 match n:
277 case 0n: Inflate{stream, out}
278 case 1n+d: inflate.stored.byte(bits.read(stream, 8), out, input => output => inflate.stored.copy(d, input, output))
279
280def inflate.stored.nlen(read: BitRead, +length: U32, +out: Bytes, limit: U32) -> Inflate:
281 BitRead{inverse, stream} = read
282 +input = stream
283 U.branch(Inflate, bits.valid(input) && U32.is_eq(U32.xor(length, inverse), 65535) && U32.is_le(length, (limit - bytes.size(out) : U32)),
284 _ => inflate.stored.copy(U32.to_nat(length), input, out), _ => Inflate{bits.invalid(input), out})
285
286def inflate.stored.len(read: BitRead, out: Bytes, limit: U32) -> Inflate:
287 BitRead{len, stream} = read
288 inflate.stored.nlen(bits.read(stream, 16), len, out, limit)
289
290type DeflateTrees is Data:
291 DeflateTrees{literal: Huffman, distance: Huffman, stream: BitStream}
292
293def inflate.cl.byte(read: BitRead, codes: Bytes, index: U32, next: BitStream -> Bytes -> Inflate) -> Inflate:
294 BitRead{len, stream} = read
295 next(stream)(bytes.set(codes, inflate.code.order(index), len))
296
297@unsafe
298def inflate.cl(n: Nat, +index: U32, stream: BitStream, codes: Bytes) -> Inflate:
299 match n:
300 case 0n: Inflate{stream, codes}
301 case 1n+d: inflate.cl.byte(bits.read(stream, 3), codes, index, input => output => inflate.cl(d, U32.inc(index), input, output))
302
303def inflate.length.repeat(read: BitRead, +base: U32, +value: U32, +remaining: U32, +lengths: Bytes) -> Inflate:
304 BitRead{extra, stream} = read
305 +count = (base + extra : U32)
306 +input = stream
307 U.branch(Inflate, bits.valid(input) && U32.is_le(count, remaining), _ => Inflate{input, bytes.repeat(U32.to_nat(count), value, lengths)}, _ => Inflate{bits.invalid(input), lengths})
308
309def inflate.length.code(read: BitRead, +remaining: U32, +lengths: Bytes) -> Inflate:
310 BitRead{symbol, stream} = read
311 +codeword = symbol
312 +input = stream
313 U.branch(Inflate, Bool.not(bits.valid(input)) || U32.is_gt(codeword, 18), _ => Inflate{bits.invalid(input), lengths},
314 _ => U.branch(Inflate, U32.is_lt(codeword, 16), _ => Inflate{input, bytes.push(lengths, codeword)},
315 _ => U.branch(Inflate, U32.is_eq(codeword, 16) && U32.is_eq(bytes.size(lengths), 0), _ => Inflate{bits.invalid(input), lengths},
316 _ => inflate.length.repeat(bits.read(input, U.choose(U32, U32.is_eq(codeword, 16), 2, U.choose(U32, U32.is_eq(codeword, 17), 3, 7))), U.choose(U32, U32.is_eq(codeword, 18), 11, 3), U.choose(U32, U32.is_eq(codeword, 16), bytes.get(lengths, (bytes.size(lengths) - 1 : U32)), 0), remaining, lengths))))
317
318def inflate.lengths.next(+result: Inflate, remaining: U32, oldSize: U32, next: U32 -> BitStream -> Bytes -> Inflate) -> Inflate:
319 Inflate{stream, lengths} = result
320 U.branch(Inflate, bits.valid(stream), _ => next((remaining - bytes.size(lengths) + oldSize : U32))(stream)(lengths), _ => result)
321
322@unsafe
323def inflate.lengths(+remaining: U32, +codes: Huffman, +stream: BitStream, +lengths: Bytes) -> Inflate:
324 U.branch(Inflate, U32.is_eq(remaining, 0), _ => Inflate{stream, lengths},
325 _ => inflate.lengths.next(inflate.length.code(huff.read(codes, stream), remaining, lengths), remaining, bytes.size(lengths), n => input => output => inflate.lengths(n, codes, input, output)))
326
327def inflate.trees(result: Inflate, +litCount: U32, distCount: U32) -> DeflateTrees:
328 Inflate{stream, lengths} = result
329 +ls = lengths
330 +input = stream
331 DeflateTrees{huff.build(bytes.slice(U32.to_nat(litCount), ls, 0, bytes.empty())), huff.build(bytes.slice(U32.to_nat(distCount), ls, litCount, bytes.empty())), U.choose(BitStream, U32.is_gt(bytes.get(ls, 256), 0), input, bits.invalid(input))}
332
333def inflate.dynamic.codes(result: Inflate, +litCount: U32, +distCount: U32) -> DeflateTrees:
334 Inflate{stream, codes} = result
335 inflate.trees(inflate.lengths((litCount + distCount : U32), huff.build(codes), stream, bytes.empty()), litCount, distCount)
336
337def inflate.dynamic.header(read: BitRead) -> DeflateTrees:
338 BitRead{header, stream} = read
339 +word = header
340 +litCount = (U32.and(word, 31) + 257 : U32)
341 +distCount = (U32.and(U32.shrn(word, 5n), 31) + 1 : U32)
342 inflate.dynamic.codes(inflate.cl(U32.to_nat((U32.and(U32.shrn(word, 10n), 15) + 4 : U32)), 0, stream, Bytes{ByteFlat{0}, 19, 32}), litCount, distCount)
343
344def inflate.dynamic(trees: DeflateTrees, out: Bytes, limit: U32) -> Inflate:
345 DeflateTrees{literal, distance, stream} = trees
346 inflate.codes(literal, distance, stream, out, limit)
347
348def inflate.block(+kind: U32, +stream: BitStream, +out: Bytes, +limit: U32) -> Inflate:
349 U.branch(Inflate, U32.is_eq(kind, 0), _ => inflate.stored.len(bits.read(bits.align(stream), 16), out, limit),
350 _ => U.branch(Inflate, U32.is_eq(kind, 1), _ => inflate.codes(huff.build(huff.fixed.lengths(288n, 0, bytes.empty())), huff.build(bytes.repeat(32n, 5, bytes.empty())), stream, out, limit),
351 _ => U.branch(Inflate, U32.is_eq(kind, 2), _ => inflate.dynamic(inflate.dynamic.header(bits.read(stream, 14)), out, limit), _ => Inflate{bits.invalid(stream), out})))
352
353def inflate.block.done(+result: Inflate, last: Bool, next: BitStream -> Bytes -> Inflate) -> Inflate:
354 Inflate{stream, output} = result
355 U.branch(Inflate, last || Bool.not(bits.valid(stream)), _ => result, _ => next(stream)(output))
356
357def inflate.header(read: BitRead, out: Bytes, limit: U32, next: BitStream -> Bytes -> Inflate) -> Inflate:
358 BitRead{header, stream} = read
359 +word = header
360 inflate.block.done(inflate.block(U32.shr(word), stream, out, limit), U32.is_eq(U32.and(word, 1), 1), next)
361
362@unsafe
363def inflate.blocks(stream: BitStream, out: Bytes, +limit: U32) -> Inflate:
364 inflate.header(bits.read(stream, 3), out, limit, input => output => inflate.blocks(input, output, limit))
365
366def checksum.adler.loop(n: Nat, +src: Bytes, +index: U32, +a: U32, b: U32) -> U32:
367 match n:
368 case 0n: (b * 65536 + a : U32)
369 case 1n+d:
370 +aa = ((a + bytes.get(src, index)) % 65521 : U32)
371 checksum.adler.loop(d, src, U32.inc(index), aa, ((b + aa) % 65521 : U32))
372
373def checksum.adler(+src: Bytes) -> U32:
374 checksum.adler.loop(U32.to_nat(bytes.size(src)), src, 0, 1, 0)
375
376def checksum.crc.word(n: Nat, +word: U32) -> U32:
377 match n:
378 case 0n: word
379 case 1n+d: checksum.crc.word(d, U32.xor(U32.shr(word), U.choose(U32, U32.is_eq(U32.and(word, 1), 1), 3988292384, 0)))
380
381def checksum.crc.table(n: Nat, +index: U32, out: Bytes) -> Bytes:
382 match n:
383 case 0n: out
384 case 1n+d: checksum.crc.table(d, U32.inc(index), bytes.push(out, checksum.crc.word(8n, index)))
385
386def checksum.crc.loop(n: Nat, +src: Bytes, +index: U32, +table: Bytes, +crc: U32) -> U32:
387 match n:
388 case 0n: U32.xor(crc, 4294967295)
389 case 1n+d: checksum.crc.loop(d, src, U32.inc(index), table, U32.xor(U32.shrn(crc, 8n), bytes.get(table, U32.and(U32.xor(crc, bytes.get(src, index)), 255))))
390
391def zlib.result(result: Inflate, +expected: U32, checksum: U32) -> Maybe<&2, Bytes>:
392 Inflate{stream, output} = result
393 +out = output
394 U.choose(Maybe<&2, Bytes>, bits.valid(stream) && U32.is_eq(bytes.size(out), expected) && U32.is_eq(checksum.adler(out), checksum), Some{out}, None{})
395
396def zlib(+src: Bytes, +expected: U32) -> Maybe<&2, Bytes>:
397 +n = bytes.size(src)
398 +cmf = bytes.get(src, 0)
399 +flg = bytes.get(src, 1)
400 U.branch(Maybe<&2, Bytes>, U32.is_ge(n, 6) && U32.is_eq(U32.and(cmf, 15), 8) && U32.is_le(U32.shrn(cmf, 4n), 7) && U32.is_eq(U32.and(flg, 32), 0) && U32.is_eq(((cmf * 256 + flg) % 31 : U32), 0),
401 _ => zlib.result(inflate.blocks(BitStream{src, 16, ((n - 4) * 8 : U32), True{}}, bytes.empty(), expected), expected, bytes.be(src, (n - 4 : U32), 4n, 0)), _ => None{})
402
403def uri.hex.valid(+c: U32) -> Bool:
404 U.digit(c) || (U32.is_ge(c, 65) && U32.is_le(c, 70)) || (U32.is_ge(c, 97) && U32.is_le(c, 102))
405
406def uri.bytes(+s: String, +out: Bytes) -> Bytes:
407 match s:
408 case SNil{}: out
409 case SCon{Chr{37}, SCon{Chr{a}, SCon{Chr{b}, rest}}}:
410 U.branch(Bytes, uri.hex.valid(a) && uri.hex.valid(b), _ => uri.bytes(rest, bytes.push(out, (U.hex.digit(a) * 16 + U.hex.digit(b) : U32))), _ => bytes.empty())
411 case SCon{Chr{c}, rest}:
412 U.branch(Bytes, U32.is_lt(c, 128) && Bool.not(U32.is_eq(c, 37)), _ => uri.bytes(rest, bytes.push(out, c)), _ => bytes.empty())
413
414@unsafe
415def bytes.depth(+size: U32, +side: U32, +depth: Nat) -> Nat:
416 U.branch(Nat, U32.is_ge(side, size), _ => depth, _ => bytes.depth(size, (side * 2 : U32), 1n+depth))
417
418def bytes.zero(+size: U32) -> Bytes:
419 Bytes{ByteFlat{0}, size, U32.shln(1, bytes.depth(size, 1, 0n))}
420
421
422
423
424
425
426def bytes.read.raw(path: String) -> IO(Result<&1, &1, U32 & String, Bytes>):
427 import "./effs/bytes_read.c"
428 import "./effs/bytes_read.js"
429
430def bytes.read(path: String) -> IO(Result<&1, &1, U32 & String, Bytes>):
431 bytes.read.raw(path)