hpack.bend
bend-kit-http2@0.3.0.0 · 651 lines · 0 definitions
1# RFC 7541 HPACK header blocks with a bounded dynamic table.
2import Base
3import bend-kit-bytes@0.3.2.0/bytes.bend as Bytes
4import bend-kit-http2@0.3.0.0/huffman.bend as Huff
5
6# mode: 0 permits indexing, 1 is without indexing, 2 is never indexed.
7type Field is Data:
8 Field{name: String, value: String, mode: U32}
9
10type State is Data:
11 State{entries: List<&2, Field>, size: U32, capacity: U32, allowed: U32, pending: Maybe<&2, U32>, minimum: Maybe<&2, U32>}
12
13def new(+max: U32) -> State:
14 State{Nil{}, 0, max, max, None{}, None{}}
15
16# RFC 7541 Appendix A, indexed from 1 to 61.
17def static(+index: U32) -> Field:
18 match index:
19 case 1:
20 Field{":authority", "", 0}
21 case 2:
22 Field{":method", "GET", 0}
23 case 3:
24 Field{":method", "POST", 0}
25 case 4:
26 Field{":path", "/", 0}
27 case 5:
28 Field{":path", "/index.html", 0}
29 case 6:
30 Field{":scheme", "http", 0}
31 case 7:
32 Field{":scheme", "https", 0}
33 case 8:
34 Field{":status", "200", 0}
35 case 9:
36 Field{":status", "204", 0}
37 case 10:
38 Field{":status", "206", 0}
39 case 11:
40 Field{":status", "304", 0}
41 case 12:
42 Field{":status", "400", 0}
43 case 13:
44 Field{":status", "404", 0}
45 case 14:
46 Field{":status", "500", 0}
47 case 15:
48 Field{"accept-charset", "", 0}
49 case 16:
50 Field{"accept-encoding", "gzip, deflate", 0}
51 case 17:
52 Field{"accept-language", "", 0}
53 case 18:
54 Field{"accept-ranges", "", 0}
55 case 19:
56 Field{"accept", "", 0}
57 case 20:
58 Field{"access-control-allow-origin", "", 0}
59 case 21:
60 Field{"age", "", 0}
61 case 22:
62 Field{"allow", "", 0}
63 case 23:
64 Field{"authorization", "", 0}
65 case 24:
66 Field{"cache-control", "", 0}
67 case 25:
68 Field{"content-disposition", "", 0}
69 case 26:
70 Field{"content-encoding", "", 0}
71 case 27:
72 Field{"content-language", "", 0}
73 case 28:
74 Field{"content-length", "", 0}
75 case 29:
76 Field{"content-location", "", 0}
77 case 30:
78 Field{"content-range", "", 0}
79 case 31:
80 Field{"content-type", "", 0}
81 case 32:
82 Field{"cookie", "", 0}
83 case 33:
84 Field{"date", "", 0}
85 case 34:
86 Field{"etag", "", 0}
87 case 35:
88 Field{"expect", "", 0}
89 case 36:
90 Field{"expires", "", 0}
91 case 37:
92 Field{"from", "", 0}
93 case 38:
94 Field{"host", "", 0}
95 case 39:
96 Field{"if-match", "", 0}
97 case 40:
98 Field{"if-modified-since", "", 0}
99 case 41:
100 Field{"if-none-match", "", 0}
101 case 42:
102 Field{"if-range", "", 0}
103 case 43:
104 Field{"if-unmodified-since", "", 0}
105 case 44:
106 Field{"last-modified", "", 0}
107 case 45:
108 Field{"link", "", 0}
109 case 46:
110 Field{"location", "", 0}
111 case 47:
112 Field{"max-forwards", "", 0}
113 case 48:
114 Field{"proxy-authenticate", "", 0}
115 case 49:
116 Field{"proxy-authorization", "", 0}
117 case 50:
118 Field{"range", "", 0}
119 case 51:
120 Field{"referer", "", 0}
121 case 52:
122 Field{"refresh", "", 0}
123 case 53:
124 Field{"retry-after", "", 0}
125 case 54:
126 Field{"server", "", 0}
127 case 55:
128 Field{"set-cookie", "", 0}
129 case 56:
130 Field{"strict-transport-security", "", 0}
131 case 57:
132 Field{"transfer-encoding", "", 0}
133 case 58:
134 Field{"user-agent", "", 0}
135 case 59:
136 Field{"vary", "", 0}
137 case 60:
138 Field{"via", "", 0}
139 case 61:
140 Field{"www-authenticate", "", 0}
141 case _:
142 Field{"", "", 0}
143
144type Cursor is Type:
145 Cursor{bytes: Bytes.Bytes, at: U32, length: U32}
146
147def take.of(r: Bytes.Bytes & Maybe<&2, U32>, +at: U32, +length: U32) -> Maybe<&1, Cursor & U32>:
148 (b, m) = r
149 match m:
150 case None{}:
151 None{}
152 case Some{value}:
153 Some{(Cursor{b, (at + 1 : U32), length}, value)}
154
155def take(c: Cursor) -> Maybe<&1, Cursor & U32>:
156 Cursor{b, +at, +length} = c
157 take.of(Bytes.get(b, at), at, length)
158
159def with_pair(-R: Type, r: Cursor & U32, k: Cursor -> U32 -> R) -> R:
160 (cursor, value) = r
161 k(cursor, value)
162
163def with_taken(-R: Type, m: Maybe<&1, Cursor & U32>, k: Cursor -> U32 -> Maybe<&1, R>) -> Maybe<&1, R>:
164 match m:
165 case None{}:
166 None{}
167 case Some{pair}:
168 with_pair(Maybe<&1, R>, pair, k)
169
170def within(ok: Bool) -> Maybe<&1, Unit>:
171 match ok:
172 case True{}:
173 Some{Unit{}}
174 case False{}:
175 None{}
176
177def integer.done(n: Nat, cont: Bool, c: Cursor, +shift: U32, +value: U32) -> Maybe<&1, Cursor & U32>:
178 match n cont:
179 case 0n False{}:
180 Some{(c, value)}
181 case 0n True{}:
182 None{}
183 case 1n+p False{}:
184 Some{(c, value)}
185 case 1n+p True{}:
186 with_taken(Cursor & U32, take(c), cursor => +byte =>
187 do Maybe<&1, Cursor & U32>:
188 +part: U32 = (byte .&. 127 : U32)
189 unused: Unit <- within(U32.is_le(part, ((4294967295 - value : U32) >> U32.to_nat(shift) : U32)))
190 integer.done(p, U32.is_ne((byte .&. 128 : U32), 0), cursor, (shift + 7 : U32), (value + (part << U32.to_nat(shift) : U32) : U32)))
191
192def integer.more(full: Bool, c: Cursor, +value: U32) -> Maybe<&1, Cursor & U32>:
193 match full:
194 case True{}:
195 integer.done(5n, True{}, c, 0, value)
196 case False{}:
197 Some{(c, value)}
198
199def integer.after(+byte: U32, +mask: U32, c: Cursor) -> Maybe<&1, Cursor & U32>:
200 +v = (byte .&. mask : U32)
201 integer.more(U32.is_eq(v, mask), c, v)
202
203def table.at(xs: List<&2, Field>, n: Nat) -> Maybe<&2, Field>:
204 match xs n:
205 case Nil{} _:
206 None{}
207 case Con{+field, tail} 0n:
208 Some{field}
209 case Con{field, tail} 1n+p:
210 table.at(tail, p)
211
212
213def indexed.static(valid: Bool, +i: U32) -> Maybe<&2, Field>:
214 match valid:
215 case True{}:
216 Some{static(i)}
217 case False{}:
218 None{}
219def indexed.choose(s: Bool, +i: U32, xs: List<&2, Field>) -> Maybe<&2, Field>:
220 match s:
221 case True{}:
222 indexed.static(U32.is_ne(i, 0), i)
223 case False{}:
224 table.at(xs, U32.to_nat((i - 62 : U32)))
225def indexed(+i: U32, st: State) -> Maybe<&2, Field>:
226 State{entries, size, capacity, allowed, pending, minimum} = st
227 indexed.choose(U32.is_le(i, 61), i, entries)
228
229def literal.decoded(huff: Bool, b: Bytes.Bytes) -> Maybe<&2, String>:
230 match huff:
231 case True{}:
232 Huff.decode(b)
233 case False{}:
234 Some{Bytes.to_string(b)}
235
236def literal.result(m: Maybe<&2, String>, b: Bytes.Bytes, +at: U32, +count: U32, +length: U32) -> Maybe<&1, Cursor & String>:
237 match m:
238 case None{}:
239 None{}
240 case Some{text}:
241 Some{(Cursor{b, (at + count : U32), length}, text)}
242
243def literal.slice(r: Bytes.Bytes & Bytes.Bytes, huff: Bool, +at: U32, +count: U32, +length: U32) -> Maybe<&1, Cursor & String>:
244 (b, part) = r
245 literal.result(literal.decoded(huff, part), b, at, count, length)
246
247def literal.fits(ok: Bool, huff: Bool, b: Bytes.Bytes, +at: U32, +count: U32, +length: U32) -> Maybe<&1, Cursor & String>:
248 match ok:
249 case False{}:
250 None{}
251 case True{}:
252 literal.slice(Bytes.slice(b, at, count), huff, at, count, length)
253
254def literal.bytes(huff: Bool, c: Cursor, +count: U32) -> Maybe<&1, Cursor & String>:
255 Cursor{b, +at, +length} = c
256 literal.fits(Bytes.fits(length, at, count), huff, b, at, count, length)
257
258def literal(c: Cursor) -> Maybe<&1, Cursor & String>:
259 with_taken(Cursor & String, take(c), cursor => +first =>
260 with_taken(Cursor & String, integer.after(first, 127, cursor), cursor => count =>
261 literal.bytes(U32.is_ne((first .&. 128 : U32), 0), cursor, count)))
262
263def field.size(f: Field) -> U32:
264 Field{+name, +value, mode} = f
265 (U32.from_nat(String.length(name)) + U32.from_nat(String.length(value)) + 32 : U32)
266
267def table.trim.go(xs: List<&2, Field>, +room: U32, keep: Bool, +acc: List<&2, Field>, +used: U32) -> List<&2, Field> & U32:
268 match xs keep:
269 case Nil{} _:
270 (List.reverse(&2, Field, acc), used)
271 case Con{field, tail} False{}:
272 (List.reverse(&2, Field, acc), used)
273 case Con{+field, tail} True{}:
274 +cost = field.size(field)
275 +fits = U32.is_le(cost, room)
276 table.trim.go(tail, Bool.pick(U32, fits, (room - cost : U32), 0), fits,
277 Bool.pick(List<&2, Field>, fits, Con{field, acc}, acc),
278 Bool.pick(U32, fits, (used + cost : U32), used))
279
280def table.trim(xs: List<&2, Field>, +capacity: U32) -> List<&2, Field> & U32:
281 table.trim.go(xs, capacity, True{}, Nil{}, 0)
282
283def table.trimmed(r: List<&2, Field> & U32, +capacity: U32, +allowed: U32, pending: Maybe<&2, U32>, minimum: Maybe<&2, U32>) -> State:
284 (entries, size) = r
285 State{entries, size, capacity, allowed, pending, minimum}
286
287def table.add(room: Bool, +field: Field, xs: List<&2, Field>, +used: U32, +capacity: U32, +allowed: U32, pending: Maybe<&2, U32>, minimum: Maybe<&2, U32>) -> State:
288 match room:
289 case True{}:
290 State{Con{field, xs}, (used + field.size(field) : U32), capacity, allowed, pending, minimum}
291 case False{}:
292 table.trimmed(table.trim(Con{field, xs}, capacity), capacity, allowed, pending, minimum)
293
294def table.oversize(too_big: Bool, +field: Field, xs: List<&2, Field>, +used: U32, +capacity: U32, +allowed: U32, pending: Maybe<&2, U32>, minimum: Maybe<&2, U32>) -> State:
295 match too_big:
296 case True{}:
297 State{Nil{}, 0, capacity, allowed, pending, minimum}
298 case False{}:
299 table.add(U32.is_le(used, (capacity - field.size(field) : U32)), field, xs, used, capacity, allowed, pending, minimum)
300def table.insert(+field: Field, st: State) -> State:
301 State{xs, +used, +capacity, +allowed, pending, minimum} = st
302 +cost = field.size(field)
303 table.oversize(U32.is_gt(cost, capacity), field, xs, used, capacity, allowed, pending, minimum)
304
305def field.matches(exact: Bool, f: Field, +name: String, +value: String) -> Bool:
306 match exact:
307 case True{}:
308 Field{n, v, mode} = f
309 Bool.and(String.eq(n, name), String.eq(v, value))
310 case False{}:
311 Field{n, v, mode} = f
312 String.eq(n, name)
313
314def find.static(+exact: Bool, n: Nat, +i: U32, +name: String, +value: String, found: U32) -> U32:
315 match n found:
316 case 0n result:
317 result
318 case 1n+p 0:
319 find.static(exact, p, (i + 1 : U32), name, value,
320 Bool.pick(U32, field.matches(exact, static(i), name, value), i, 0))
321 case 1n+p result:
322 result
323
324def find.dynamic(+exact: Bool, xs: List<&2, Field>, +i: U32, +name: String, +value: String, found: U32) -> U32:
325 match xs found:
326 case Nil{} result:
327 result
328 case Con{+field, tail} 0:
329 find.dynamic(exact, tail, (i + 1 : U32), name, value,
330 Bool.pick(U32, field.matches(exact, field, name, value), i, 0))
331 case Con{field, tail} result:
332 result
333
334def find.in_dynamic(exact: Bool, st: State, +name: String, +value: String, found: U32) -> U32:
335 State{entries, size, capacity, allowed, pending, minimum} = st
336 find.dynamic(exact, entries, 62, name, value, found)
337
338def find.index(+exact: Bool, st: State, +name: String, +value: String) -> U32:
339 find.in_dynamic(exact, st, name, value, find.static(exact, 61n, 1, name, value, 0))
340
341def limit.min(m: Maybe<&2, U32>, +n: U32) -> U32:
342 match m:
343 case None{}:
344 n
345 case Some{+old}:
346 Bool.pick(U32, U32.is_lt(n, old), n, old)
347
348def set_limit(+n: U32, st: State) -> State:
349 State{entries, size, capacity, allowed, pending, minimum} = st
350 State{entries, size, capacity, n, Some{n}, Some{limit.min(minimum, n)}}
351
352def table.resize(+n: U32, st: State) -> State:
353 State{entries, size, capacity, allowed, pending, minimum} = st
354 table.trimmed(table.trim(entries, n), n, allowed, pending, minimum)
355
356type Step is Type:
357 Step{state: State, cursor: Cursor, field: Maybe<&2, Field>}
358
359def with_text.pair(-R: Type, r: Cursor & String, k: Cursor -> String -> R) -> R:
360 (cursor, text) = r
361 k(cursor, text)
362
363def with_text(-R: Type, m: Maybe<&1, Cursor & String>, k: Cursor -> String -> Maybe<&1, R>) -> Maybe<&1, R>:
364 match m:
365 case None{}:
366 None{}
367 case Some{pair}:
368 with_text.pair(Maybe<&1, R>, pair, k)
369
370def name.indexed(m: Maybe<&2, Field>, c: Cursor) -> Maybe<&1, Cursor & String>:
371 match m:
372 case None{}:
373 None{}
374 case Some{Field{name, value, mode}}:
375 Some{(c, name)}
376
377def name.read(+i: U32, st: State, c: Cursor) -> Maybe<&1, Cursor & String>:
378 match i:
379 case 0:
380 literal(c)
381 case _:
382 name.indexed(indexed(i, st), c)
383
384def decode.indexed.field(m: Maybe<&2, Field>, st: State, c: Cursor) -> Maybe<&1, Step>:
385 match m:
386 case None{}:
387 None{}
388 case Some{field}:
389 Some{Step{st, c, Some{field}}}
390
391def decode.indexed(+first: U32, +st: State, c: Cursor) -> Maybe<&1, Step>:
392 with_taken(Step, integer.after(first, 127, c), cursor => index =>
393 decode.indexed.field(indexed(index, st), st, cursor))
394
395def decode.literal.finish(insert: Bool, +field: Field, st: State, c: Cursor) -> Maybe<&1, Step>:
396 match insert:
397 case True{}:
398 Some{Step{table.insert(field, st), c, Some{field}}}
399 case False{}:
400 Some{Step{st, c, Some{field}}}
401
402def decode.literal(+first: U32, +mask: U32, +mode: U32, +st: State, c: Cursor) -> Maybe<&1, Step>:
403 with_taken(Step, integer.after(first, mask, c), cursor => index =>
404 with_text(Step, name.read(index, st, cursor), cursor => +name =>
405 with_text(Step, literal(cursor), cursor => value =>
406 decode.literal.finish(U32.is_eq(mode, 0), Field{name, value, mode}, st, cursor))))
407
408def decode.min(m: Maybe<&2, U32>, +n: U32) -> Bool:
409 match m:
410 case None{}:
411 True{}
412 case Some{minimum}:
413 U32.is_le(n, minimum)
414
415def decode.updated.from(st: State, c: Cursor) -> Maybe<&1, Step>:
416 State{entries, size, capacity, allowed, pending, minimum} = st
417 Some{Step{State{entries, size, capacity, allowed, None{}, None{}}, c, None{}}}
418
419def decode.updated(n: U32, st: State, c: Cursor) -> Maybe<&1, Step>:
420 decode.updated.from(table.resize(n, st), c)
421
422def decode.update.valid(valid: Bool, +n: U32, st: State, c: Cursor) -> Maybe<&1, Step>:
423 match valid:
424 case True{}:
425 decode.updated(n, st, c)
426 case False{}:
427 None{}
428
429def decode.update.value(+n: U32, st: State, c: Cursor) -> Maybe<&1, Step>:
430 State{entries, size, capacity, +allowed, pending, +minimum} = st
431 decode.update.valid(Bool.and(U32.is_le(n, allowed), decode.min(minimum, n)), n,
432 State{entries, size, capacity, allowed, pending, minimum}, c)
433
434def decode.update(+first: U32, st: State, c: Cursor, seen: Bool) -> Maybe<&1, Step>:
435 do Maybe<&1, Step>:
436 unused: Unit <- within(Bool.not(seen))
437 with_taken(Step, integer.after(first, 31, c), cursor => size =>
438 decode.update.value(size, st, cursor))
439
440def decode.ready(st: State) -> Bool:
441 State{entries, size, capacity, allowed, pending, minimum} = st
442 Maybe.is_none(&2, U32, pending)
443
444def decode.kind(+first: U32) -> U32:
445 Bool.pick(U32, U32.is_ne((first .&. 128 : U32), 0), 0,
446 Bool.pick(U32, U32.is_ne((first .&. 64 : U32), 0), 1,
447 Bool.pick(U32, U32.is_ne((first .&. 32 : U32), 0), 2, 3)))
448
449def decode.representation(kind: U32, +first: U32, c: Cursor, +st: State, seen: Bool) -> Maybe<&1, Step>:
450 match kind:
451 case 0:
452 do Maybe<&1, Step>:
453 unused: Unit <- within(decode.ready(st))
454 decode.indexed(first, st, c)
455 case 1:
456 do Maybe<&1, Step>:
457 unused: Unit <- within(decode.ready(st))
458 decode.literal(first, 63, 0, st, c)
459 case 2:
460 decode.update(first, st, c, seen)
461 case _:
462 do Maybe<&1, Step>:
463 unused: Unit <- within(decode.ready(st))
464 decode.literal(first, 15, Bool.pick(U32, U32.is_ne((first .&. 16 : U32), 0), 2, 1), st, c)
465
466def decode.one(c: Cursor, +st: State, seen: Bool) -> Maybe<&1, Step>:
467 with_taken(Step, take(c), cursor => +first =>
468 decode.representation(decode.kind(first), first, cursor, st, seen))
469
470def decode.add(m: Maybe<&2, Field>, acc: List<&2, Field>, seen: Bool) -> List<&2, Field> & Bool:
471 match m:
472 case None{}:
473 (acc, seen)
474 case Some{field}:
475 (Con{field, acc}, True{})
476
477def with_step(-R: Type, step: Step, k: State -> Cursor -> Maybe<&2, Field> -> R) -> R:
478 Step{state, cursor, field} = step
479 k(state, cursor, field)
480
481def with_end(-R: Type, c: Cursor, k: Cursor -> Bool -> R) -> R:
482 Cursor{bytes, +at, +length} = c
483 k(Cursor{bytes, at, length}, U32.is_eq(at, length))
484
485def with_fields(-R: Type, r: List<&2, Field> & Bool, k: List<&2, Field> -> Bool -> R) -> R:
486 (fields, seen) = r
487 k(fields, seen)
488
489def decode.go(fuel: Nat, ended: Bool, c: Cursor, st: State, acc: List<&2, Field>, +seen: Bool) -> Maybe<&1, State & List<&2, Field>>:
490 match fuel ended:
491 case 0n False{}:
492 None{}
493 case 0n True{}:
494 Some{(st, List.reverse(&2, Field, acc))}
495 case 1n+p True{}:
496 Some{(st, List.reverse(&2, Field, acc))}
497 case 1n+p False{}:
498 Maybe.bind(&1, Step, State & List<&2, Field>, decode.one(c, st, seen), step =>
499 with_step(Maybe<&1, State & List<&2, Field>>, step, state => cursor => field =>
500 with_end(Maybe<&1, State & List<&2, Field>>, cursor, cursor => ended =>
501 with_fields(Maybe<&1, State & List<&2, Field>>, decode.add(field, acc, seen), fields => was_field =>
502 decode.go(p, ended, cursor, state, fields, was_field)))))
503
504def decode(block: Bytes.Bytes, st: State) -> Maybe<&1, State & List<&2, Field>>:
505 Bytes.Bytes{+length, buf} = block
506 decode.go(1n+U32.to_nat(length), U32.is_eq(length, 0),
507 Cursor{Bytes.Bytes{length, buf}, 0, length}, st, Nil{}, False{})
508
509def integer.tail(n: Nat, +value: U32, active: Bool) -> String:
510 match n active:
511 case 0n _:
512 SNil{}
513 case 1n+p False{}:
514 SNil{}
515 case 1n+p True{}:
516 SCon{Chr{((value .&. 127 : U32) .|. Bool.pick(U32, U32.is_ge(value, 128), 128, 0) : U32)},
517 integer.tail(p, (value >> 7n : U32), U32.is_ge(value, 128))}
518
519def integer.encoded(small: Bool, +prefix: U32, +mask: U32, +value: U32) -> Bytes.Bytes:
520 match small:
521 case True{}:
522 Bytes.from_string(SCon{Chr{(prefix .|. value : U32)}, SNil{}})
523 case False{}:
524 Bytes.from_string(SCon{Chr{(prefix .|. mask : U32)},
525 integer.tail(5n, (value - mask : U32), True{})})
526
527def integer.encode(+prefix: U32, +mask: U32, +value: U32) -> Bytes.Bytes:
528 integer.encoded(U32.is_lt(value, mask), prefix, mask, value)
529
530def octets.valid(s: String) -> Bool:
531 match s:
532 case SNil{}:
533 True{}
534 case SCon{Chr{+octet}, tail}:
535 Bool.and(U32.is_le(octet, 255), octets.valid(tail))
536
537def literal.raw(+s: String) -> Maybe<&1, Bytes.Bytes>:
538 do Maybe<&1, Bytes.Bytes>:
539 unused: Unit <- within(octets.valid(s))
540 return Bytes.from_string(s)
541
542def literal.pack(b: Bytes.Bytes, huff: Bool) -> Bytes.Bytes:
543 Bytes.Bytes{+length, buf} = b
544 Bytes.concat([integer.encode(Bool.pick(U32, huff, 128, 0), 127, length), Bytes.Bytes{length, buf}])
545
546def literal.encode(huff: Bool, s: String) -> Maybe<&1, Bytes.Bytes>:
547 match huff:
548 case True{}:
549 Maybe.map(&1, Bytes.Bytes, Bytes.Bytes, b => literal.pack(b, True{}), Huff.encode(s))
550 case False{}:
551 Maybe.map(&1, Bytes.Bytes, Bytes.Bytes, b => literal.pack(b, False{}), literal.raw(s))
552
553def name.parts(+index: U32, huff: Bool, name: String) -> Maybe<&1, List<&1, Bytes.Bytes>>:
554 match index:
555 case 0:
556 Maybe.map(&1, Bytes.Bytes, List<&1, Bytes.Bytes>, b => [b], literal.encode(huff, name))
557 case _:
558 Some{Nil{}}
559
560def encode.literal.bytes(+index: U32, +prefix: U32, +mask: U32, +huff: Bool, name: String, value: String) -> Maybe<&1, Bytes.Bytes>:
561 do Maybe<&1, Bytes.Bytes>:
562 parts: List<&1, Bytes.Bytes> <- name.parts(index, huff, name)
563 encoded: Bytes.Bytes <- literal.encode(huff, value)
564 return Bytes.concat(Con{integer.encode(prefix, mask, index),
565 List.append(&1, Bytes.Bytes, parts, [encoded])})
566
567def encode.literal.done(insert: Bool, field: Field, st: State, b: Bytes.Bytes) -> Maybe<&1, State & Bytes.Bytes>:
568 match insert:
569 case True{}:
570 Some{(table.insert(field, st), b)}
571 case False{}:
572 Some{(st, b)}
573
574def encode.literal(+mode: U32, +name: String, +value: String, huff: Bool, +st: State) -> Maybe<&1, State & Bytes.Bytes>:
575 +index = find.index(False{}, st, name, value)
576 +prefix = Bool.pick(U32, U32.is_eq(mode, 0), 64, Bool.pick(U32, U32.is_eq(mode, 2), 16, 0))
577 +mask = Bool.pick(U32, U32.is_eq(mode, 0), 63, 15)
578 Maybe.bind(&1, Bytes.Bytes, State & Bytes.Bytes,
579 encode.literal.bytes(index, prefix, mask, huff, name, value), b =>
580 encode.literal.done(U32.is_eq(mode, 0), Field{name, value, mode}, st, b))
581
582def encode.exact(found: Bool, +index: U32, +name: String, +value: String, huff: Bool, st: State) -> Maybe<&1, State & Bytes.Bytes>:
583 match found:
584 case True{}:
585 Some{(st, integer.encode(128, 127, index))}
586 case False{}:
587 encode.literal(0, name, value, huff, st)
588
589def encode.field(f: Field, huff: Bool, +st: State) -> Maybe<&1, State & Bytes.Bytes>:
590 Field{+name, +value, mode} = f
591 match mode:
592 case 0:
593 +index = find.index(True{}, st, name, value)
594 encode.exact(U32.is_ne(index, 0), index, name, value, huff, st)
595 case 1:
596 encode.literal(1, name, value, huff, st)
597 case 2:
598 encode.literal(2, name, value, huff, st)
599 case _:
600 None{}
601
602
603def encode.cleared(st: State, pieces: List<&1, Bytes.Bytes>) -> State & List<&1, Bytes.Bytes>:
604 State{entries, size, capacity, allowed, pending, minimum} = st
605 (State{entries, size, capacity, allowed, None{}, None{}}, pieces)
606
607def encode.emit(smaller: Bool, +minimum: U32, +final: U32, st: State) -> State & List<&1, Bytes.Bytes>:
608 match smaller:
609 case True{}:
610 encode.cleared(table.resize(final, table.resize(minimum, st)),
611 [integer.encode(32, 31, minimum), integer.encode(32, 31, final)])
612 case False{}:
613 encode.cleared(table.resize(final, st), [integer.encode(32, 31, final)])
614
615def encode.pending(m: Maybe<&2, U32>, minimum: Maybe<&2, U32>, st: State) -> State & List<&1, Bytes.Bytes>:
616 match m:
617 case None{}:
618 (st, Nil{})
619 case Some{+final}:
620 +smallest = limit.min(minimum, final)
621 encode.emit(U32.is_lt(smallest, final), smallest, final, st)
622
623def encode.prepare(st: State) -> State & List<&1, Bytes.Bytes>:
624 State{entries, size, capacity, allowed, +pending, +minimum} = st
625 encode.pending(pending, minimum, State{entries, size, capacity, allowed, pending, minimum})
626
627def with_encoded(-R: Type, r: State & Bytes.Bytes, k: State -> Bytes.Bytes -> R) -> R:
628 (st, bytes) = r
629 k(st, bytes)
630
631def encode.go(xs: List<&2, Field>, +huff: Bool, st: State, acc: List<&1, Bytes.Bytes>) -> Maybe<&1, State & List<&1, Bytes.Bytes>>:
632 match xs:
633 case Nil{}:
634 Some{(st, acc)}
635 case Con{field, tail}:
636 Maybe.bind(&1, State & Bytes.Bytes, State & List<&1, Bytes.Bytes>, encode.field(field, huff, st), pair =>
637 with_encoded(Maybe<&1, State & List<&1, Bytes.Bytes>>, pair, state => bytes =>
638 encode.go(tail, huff, state, Con{bytes, acc})))
639
640def encode.finish(r: State & List<&1, Bytes.Bytes>) -> State & Bytes.Bytes:
641 (st, pieces) = r
642 (st, Bytes.concat(List.reverse(&1, Bytes.Bytes, pieces)))
643
644def encode.from(r: State & List<&1, Bytes.Bytes>, fields: List<&2, Field>, huff: Bool) -> Maybe<&1, State & Bytes.Bytes>:
645 (st, updates) = r
646 Maybe.map(&1, State & List<&1, Bytes.Bytes>, State & Bytes.Bytes, encode.finish,
647 encode.go(fields, huff, st, List.reverse(&1, Bytes.Bytes, updates)))
648
649def encode(fields: List<&2, Field>, huff: Bool, st: State) -> Maybe<&1, State & Bytes.Bytes>:
650 encode.from(encode.prepare(st), fields, huff)
651