http.bend
bend-kit-http@0.19.1.0 · 3,610 lines · 0 definitions
1# HTTP/1.1 client and server for http and https, with DNS and TLS. Source: https://github.com/paymog/bend-kit/tree/main/http
2import Base
3# By hash: bend-kit-wire@0.4.2.0, -url@0.4.1.0, -encoding@0.3.0.0, -json@0.5.0.1, -bytes@0.3.0.0, -dns@0.4.0.1, -zlib@0.1.5.0.
4import bend-kit-wire@0.4.2.0/wire.bend as Wire
5import bend-kit-url@0.4.1.0/url.bend as Url
6import bend-kit-encoding@0.3.0.0/encoding.bend as Enc
7import bend-kit-json@0.5.0.1/json.bend as Json
8import bend-kit-bytes@0.3.0.0/bytes.bend as Bytes
9import bend-kit-dns@0.4.0.1/dns.bend as Dns
10import bend-kit-zlib@0.1.5.0/zlib.bend as Zlib
11
12# HTTP/1.1 codec and client (RFC 9112) for http:// and https:// (OpenSSL 3 at run time).
13# parse: start-line → field lines → blank → body length (§6.3); chunked (§7.1).
14# Bodies are Bytes. The String parsers below are the spec: one Char per octet.
15# fetch reads until frame() says the response is whole. It returns Result, not Maybe.
16# Build with -o for big bodies: the `bend file.bend` runner overflows on ~30 KB strings; native binaries do not.
17# import bend-kit-http@0.15.0.0/http.bend as Http
18
19type Req is Type:
20 Req{method: String, path: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
21
22type Res is Type:
23 Res{status: U32, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
24
25# The body type and its conversions, so a caller needs no bytes import.
26def Body() -> Type:
27 Bytes.Bytes
28
29# A byte string (one Char per octet) to a body, and back.
30def from_string(+s: String) -> Bytes.Bytes:
31 Bytes.from_string(s)
32
33def to_string(b: Bytes.Bytes) -> String:
34 Bytes.to_string(b)
35
36def length(b: Bytes.Bytes) -> Bytes.Bytes & U32:
37 Bytes.length(b)
38
39# Why fetch failed. Wire errors keep the errno and the text the effect already had.
40# ponytail: 60 and 110 are ETIMEDOUT on macOS and Linux. Windows is out of scope.
41type Err is Data:
42 ErrUrl{}
43 ErrDns{}
44 ErrConnect{code: U32, why: String}
45 ErrTls{code: U32, why: String}
46 ErrRead{code: U32, why: String}
47 ErrWrite{code: U32, why: String}
48 ErrTimeout{}
49 ErrRedirect{}
50 ErrBad{}
51
52def err.late(+code: U32) -> Bool:
53 Bool.or(U32.is_eq(code, 60), U32.is_eq(code, 110))
54
55def err.pick(e: Err, late: Bool) -> Err:
56 match late:
57 case True{}:
58 ErrTimeout{}
59 case False{}:
60 e
61
62def err.or_late(code: U32, e: Err) -> Err:
63 err.pick(e, err.late(code))
64
65type Fields is Data:
66 FieldsBad{}
67 FieldsOk{m: Map<&2, List<&2, String>>}
68
69# One list per field name, in arrival order. header() is the first value.
70# Set-Cookie is never joined. Encode writes one line per value.
71def empty() -> Map<&2, List<&2, String>>:
72 Map.new(&2, List<&2, String>)
73
74def fields.of(r: Map<&2, List<&2, String>> & List<&2, String>) -> List<&2, String>:
75 (h, xs) = r
76 xs
77
78def fields(+h: Map<&2, List<&2, String>>, k: String) -> List<&2, String>:
79 fields.of(Map.get(List<&2, String>, Nil{}, h, k))
80
81def header.first(xs: List<&2, String>) -> String:
82 match xs:
83 case Nil{}:
84 ""
85 case Con{v, t}:
86 v
87
88def header(+h: Map<&2, List<&2, String>>, k: String) -> String:
89 header.first(fields(h, k))
90
91def field.last(xs: List<&2, String>) -> String:
92 match xs:
93 case Nil{}:
94 ""
95 case Con{v, Nil{}}:
96 v
97 case Con{v, t}:
98 field.last(t)
99
100# Transfer-Encoding is a list; chunked, when present, is the last coding.
101def header.last(+h: Map<&2, List<&2, String>>, k: String) -> String:
102 field.last(fields(h, k))
103
104def snoc(xs: List<&2, String>, v: String) -> List<&2, String>:
105 match xs:
106 case Nil{}:
107 [v]
108 case Con{h, t}:
109 Con{h, snoc(t, v)}
110
111def set(m: Map<&2, List<&2, String>>, k: String, v: String) -> Map<&2, List<&2, String>>:
112 Map.set(&2, List<&2, String>, m, k, [v])
113
114def add(+m: Map<&2, List<&2, String>>, +k: String, v: String) -> Map<&2, List<&2, String>>:
115 Map.set(&2, List<&2, String>, m, k, snoc(fields(m, k), v))
116
117def sanitize.cons(ch: Char, rest: String, drop: Bool) -> String:
118 match drop:
119 case True{}:
120 rest
121 case False{}:
122 SCon{ch, rest}
123
124def sanitize(s: String) -> String:
125 match s:
126 case SNil{}:
127 SNil{}
128 case SCon{Chr{+c}, t}:
129 sanitize.cons(Chr{c}, sanitize(t), Bool.or(U32.is_eq(c, 13), U32.is_eq(c, 10)))
130
131def drop_cr.last.if(cr: Bool, c: U32) -> String:
132 match cr:
133 case True{}:
134 SNil{}
135 case False{}:
136 SCon{Chr{c}, SNil{}}
137
138def drop_cr.last(+c: U32) -> String:
139 drop_cr.last.if(U32.is_eq(c, 13), c)
140
141# prev is the char before s; it is kept unless it is a final CR.
142def drop_cr.go(s: String, prev: U32) -> String:
143 match s:
144 case SNil{}:
145 drop_cr.last(prev)
146 case SCon{Chr{c}, t}:
147 SCon{Chr{prev}, drop_cr.go(t, c)}
148
149def drop_cr(s: String) -> String:
150 match s:
151 case SNil{}:
152 SNil{}
153 case SCon{Chr{c}, t}:
154 drop_cr.go(t, c)
155
156# w holds the last four octets; a char past 255 clears it.
157def blank_end.go(s: String, w: U32) -> Bool:
158 match s:
159 case SNil{}:
160 U32.is_eq(w, 218762506)
161 case SCon{Chr{+c}, t}:
162 blank_end.go(t, Bool.pick(U32, U32.is_lt(c, 256), (w * 256 + c : U32), 0))
163
164# String.ends_with(s, "\r\n\r\n") in one pass, with no reversed copy.
165def blank_end(s: String) -> Bool:
166 blank_end.go(s, 0)
167
168def trim_end.cons(h: Char, r: String, space: Bool) -> String:
169 match r:
170 case SNil{}:
171 match space:
172 case True{}:
173 SNil{}
174 case False{}:
175 SCon{h, SNil{}}
176 case SCon{a, t}:
177 SCon{h, SCon{a, t}}
178
179# String.trim_end without the two reversed copies.
180def trim_end(s: String) -> String:
181 match s:
182 case SNil{}:
183 SNil{}
184 case SCon{+h, t}:
185 trim_end.cons(h, trim_end(t), Char.is_space(h))
186
187def trim(s: String) -> String:
188 trim_end(String.trim_start(s))
189
190# Bool.pick evaluates both arms; a split that recursed inside it would reverse acc at every byte.
191def take.cut(acc: String, rest: String) -> String & String:
192 (String.reverse(String.drop(acc, 1n)), rest)
193
194# hit: the last char pushed onto acc was the stop char.
195def take_sp.go(s: String, acc: String, hit: Bool) -> String & String:
196 match s:
197 case SNil{}:
198 match hit:
199 case True{}:
200 take.cut(acc, SNil{})
201 case False{}:
202 (String.reverse(acc), SNil{})
203 case SCon{Chr{+c}, t}:
204 match hit:
205 case True{}:
206 take.cut(acc, SCon{Chr{c}, t})
207 case False{}:
208 take_sp.go(t, SCon{Chr{c}, acc}, U32.is_eq(c, 32))
209
210def take_sp(s: String) -> String & String:
211 take_sp.go(s, SNil{}, False{})
212
213def start_line.ver(m: String, pv: String & String) -> String & String & String:
214 (p, v) = pv
215 (m, p, drop_cr(v))
216
217def start_line.rest(mr: String & String) -> String & String & String:
218 (m, r) = mr
219 start_line.ver(m, take_sp(r))
220
221def start_line(s: String) -> String & String & String:
222 start_line.rest(take_sp(s))
223
224def split_at_blank.go(s: String, e: Bool, w: U32, acc: String) -> String & String:
225 match s:
226 case SNil{}:
227 (String.reverse(acc), SNil{})
228 case SCon{Chr{+a}, t}:
229 match e:
230 case True{}:
231 (String.reverse(acc), SCon{Chr{a}, t})
232 case False{}:
233 +w2 = (w * 256 + a : U32)
234 split_at_blank.go(t, U32.is_eq(w2, 218762506), w2, SCon{Chr{a}, acc})
235
236# split_at_blank, plus whether the head ends in the blank line.
237def split_at_blank.flag.go(+raw: String, s: String, off: Nat, w: U32, e: Bool) -> String & String & Bool:
238 match s:
239 case SNil{}:
240 (String.take(raw, off), SNil{}, e)
241 case SCon{Chr{+a}, t}:
242 match e:
243 case True{}:
244 (String.take(raw, off), SCon{Chr{a}, t}, True{})
245 case False{}:
246 +w2 = (w * 256 + a : U32)
247 +off1 = (1n + off : Nat)
248 split_at_blank.flag.go(raw, t, off1, w2, U32.is_eq(w2, 218762506))
249
250def split_at_blank.pair(r: String & String & Bool) -> String & String:
251 (head, rest, whole) = r
252 (head, rest)
253
254def split_at_blank(+s: String) -> String & String:
255 split_at_blank.pair(split_at_blank.flag.go(s, s, 0n, 0, False{}))
256
257def split_colon.go(s: String, acc: String, hit: Bool) -> String & String:
258 match s:
259 case SNil{}:
260 match hit:
261 case True{}:
262 take.cut(acc, SNil{})
263 case False{}:
264 (String.reverse(acc), SNil{})
265 case SCon{Chr{+c}, t}:
266 match hit:
267 case True{}:
268 take.cut(acc, SCon{Chr{c}, t})
269 case False{}:
270 split_colon.go(t, SCon{Char.to_lower(Chr{c}), acc}, U32.is_eq(c, 58))
271
272def split_colon(+s: String) -> String & String:
273 split_colon.go(s, SNil{}, False{})
274
275def has_header.of(r: Map<&2, List<&2, String>> & Bool) -> Bool:
276 (h, b) = r
277 b
278
279def has_header(+h: Map<&2, List<&2, String>>, k: String) -> Bool:
280 has_header.of(Map.has(&2, List<&2, String>, h, k))
281
282def folded(+line: String) -> Bool:
283 Bool.or(String.starts_with(line, " "), String.starts_with(line, "\t"))
284
285def tracked(+k: String) -> Bool:
286 Bool.or(String.eq(k, "host"), String.eq(k, "content-length"))
287
288def fields_put.dup(m: Map<&2, List<&2, String>>, k: String, v: String, bad: Bool) -> Fields:
289 match bad:
290 case True{}:
291 FieldsBad{}
292 case False{}:
293 FieldsOk{add(m, k, v)}
294
295def fields_put.tracked(+m: Map<&2, List<&2, String>>, +k: String, v: String, t: Bool) -> Fields:
296 match t:
297 case True{}:
298 fields_put.dup(m, k, v, has_header(m, k))
299 case False{}:
300 FieldsOk{add(m, k, v)}
301
302def fields_put.key(+m: Map<&2, List<&2, String>>, +k: String, v: String) -> Fields:
303 fields_put.tracked(m, k, v, tracked(k))
304
305def fields_put.kv(m: Map<&2, List<&2, String>>, kv: String & String) -> Fields:
306 (k, v) = kv
307 fields_put.key(m, k, trim(v))
308
309def fields_put.fold(m: Map<&2, List<&2, String>>, line: String, fold: Bool) -> Fields:
310 match fold:
311 case True{}:
312 FieldsBad{}
313 case False{}:
314 fields_put.kv(m, split_colon(line))
315
316def fields_put.empty(m: Map<&2, List<&2, String>>, +line: String, e: Bool) -> Fields:
317 match e:
318 case True{}:
319 FieldsOk{m}
320 case False{}:
321 fields_put.fold(m, line, folded(line))
322
323def fields_put.ok(m: Map<&2, List<&2, String>>, +line: String) -> Fields:
324 fields_put.empty(m, line, String.is_empty(line))
325
326def fields_put(acc: Fields, line: String) -> Fields:
327 match acc:
328 case FieldsBad{}:
329 FieldsBad{}
330 case FieldsOk{m}:
331 fields_put.ok(m, line)
332
333def parse.headers.done(acc: Fields) -> Maybe<&2, Map<&2, List<&2, String>>>:
334 match acc:
335 case FieldsBad{}:
336 None{}
337 case FieldsOk{m}:
338 Some{m}
339
340def parse.headers(xs: List<&2, String>, acc: Fields) -> Maybe<&2, Map<&2, List<&2, String>>>:
341 match xs:
342 case Nil{}:
343 parse.headers.done(acc)
344 case Con{line, rest}:
345 parse.headers(rest, fields_put(acc, drop_cr(line)))
346
347def parse_u32.digit(+c: U32) -> Bool:
348 Bool.and(U32.is_le(48, c), U32.is_le(c, 57))
349
350def parse_u32.add(acc: U32, c: U32) -> U32:
351 (acc * 10 + (c - 48 : U32) : U32)
352
353def parse_u32.done(acc: U32, bad: Bool) -> Maybe<&2, U32>:
354 match bad:
355 case True{}:
356 None{}
357 case False{}:
358 Some{acc}
359
360def parse_u32.go(s: String, acc: U32, bad: Bool) -> Maybe<&2, U32>:
361 match s:
362 case SNil{}:
363 parse_u32.done(acc, bad)
364 case SCon{Chr{+c}, t}:
365 parse_u32.go(t, parse_u32.add(acc, c), Bool.or(bad, Bool.not(parse_u32.digit(c))))
366
367def parse_u32(s: String) -> Maybe<&2, U32>:
368 match s:
369 case SNil{}:
370 None{}
371 case SCon{Chr{+c}, t}:
372 parse_u32.go(t, parse_u32.add(0, c), Bool.not(parse_u32.digit(c)))
373
374# More: a valid prefix. Bad: cannot become a body. Body: a whole chunked body.
375type Hold is Data:
376 HoldMore{}
377 HoldBad{}
378 HoldBody{b: String}
379 HoldUntil{b: String}
380
381def is_hex(+c: U32) -> Bool:
382 Bool.or(parse_u32.digit(c), Bool.or(Bool.and(U32.is_le(97, c), U32.is_le(c, 102)), Bool.and(U32.is_le(65, c), U32.is_le(c, 70))))
383
384def hexv(+c: U32) -> U32:
385 Bool.pick(U32, parse_u32.digit(c), (c - 48 : U32), Bool.pick(U32, U32.is_le(c, 70), (c - 55 : U32), (c - 87 : U32)))
386
387# A chunked body decoder that reads each byte once, so a body fed in pieces
388# costs O(bytes) in total. Tr{j}: j bytes of the closing CRLF CRLF matched.
389type Dc is Data:
390 DcSize{acc: U32, seen: Bool}
391 DcExt{n: U32}
392 DcSizeLf{n: U32}
393 DcData{k: U32}
394 DcDataCr{}
395 DcDataLf{}
396 DcTr{j: U32}
397 DcDone{}
398 DcBad{}
399
400# st: where the decoder is. racc: the body so far, reversed. rest: bytes after a Done body.
401type Dco is Data:
402 Dco{st: Dc, racc: String, rest: String}
403
404def dc.start() -> Dc:
405 DcSize{0, False{}}
406
407def dc.size.semi(+n: U32, semi: Bool) -> Dc:
408 match semi:
409 case True{}:
410 DcExt{n}
411 case False{}:
412 DcBad{}
413
414def dc.size.cr(+n: U32, +c: U32, cr: Bool) -> Dc:
415 match cr:
416 case True{}:
417 DcSizeLf{n}
418 case False{}:
419 dc.size.semi(n, U32.is_eq(c, 59))
420
421def dc.size.end(+n: U32, +c: U32, seen: Bool) -> Dc:
422 match seen:
423 case False{}:
424 DcBad{}
425 case True{}:
426 dc.size.cr(n, c, U32.is_eq(c, 13))
427
428# A size that would overflow 32 bits ends the digits, and size.end then refuses it.
429def dc.size(+acc: U32, seen: Bool, +c: U32, digit: Bool) -> Dc:
430 match digit:
431 case True{}:
432 DcSize{(acc * 16 + hexv(c) : U32), True{}}
433 case False{}:
434 dc.size.end(acc, c, seen)
435
436# RFC 9112 §7.1.1: recipients ignore unknown chunk extensions; a bare LF is not CRLF.
437def dc.ext.lf(+n: U32, lf: Bool) -> Dc:
438 match lf:
439 case True{}:
440 DcBad{}
441 case False{}:
442 DcExt{n}
443
444def dc.ext(+n: U32, +c: U32, cr: Bool) -> Dc:
445 match cr:
446 case True{}:
447 DcSizeLf{n}
448 case False{}:
449 dc.ext.lf(n, U32.is_eq(c, 10))
450
451def dc.sized(+n: U32, zero: Bool) -> Dc:
452 match zero:
453 case True{}:
454 DcTr{2}
455 case False{}:
456 DcData{n}
457
458def dc.size.lf(+n: U32, lf: Bool) -> Dc:
459 match lf:
460 case True{}:
461 dc.sized(n, U32.is_eq(n, 0))
462 case False{}:
463 DcBad{}
464
465# k data bytes are left and m of them were just read.
466def dc.data(+k: U32, +m: U32) -> Dc:
467 Bool.pick(Dc, U32.is_le(k, m), DcDataCr{}, DcData{(k - m : U32)})
468
469def dc.pick(ok: Bool, next: Dc) -> Dc:
470 match ok:
471 case True{}:
472 next
473 case False{}:
474 DcBad{}
475
476# ponytail: trailer fields are dropped unparsed (§7.1.2 allows discarding)
477def dc.tr.hit(+j: U32) -> Dc:
478 Bool.pick(Dc, U32.is_eq(j, 3), DcDone{}, DcTr{(j + 1 : U32)})
479
480def dc.tr(+j: U32, +c: U32, hit: Bool) -> Dc:
481 match hit:
482 case True{}:
483 dc.tr.hit(j)
484 case False{}:
485 Bool.pick(Dc, U32.is_eq(c, 13), DcTr{1}, DcTr{0})
486
487def dc.tr.want(+j: U32) -> U32:
488 Bool.pick(U32, U32.is_eq(U32.mod(j, 2), 0), 13, 10)
489
490def dc.byte(h: Char) -> U32:
491 Chr{c} = h
492 c
493
494# One byte c. Done and Bad never look at it, and a data byte is not inspected.
495def dc.step(st: Dc, +c: U32) -> Dc:
496 match st:
497 case DcBad{}:
498 DcBad{}
499 case DcSize{+acc, seen}:
500 dc.size(acc, seen, c, Bool.and(is_hex(c), U32.is_le(acc, 268435455)))
501 case DcExt{+n}:
502 dc.ext(n, c, U32.is_eq(c, 13))
503 case DcSizeLf{+n}:
504 dc.size.lf(n, U32.is_eq(c, 10))
505 case DcDataCr{}:
506 dc.pick(U32.is_eq(c, 13), DcDataLf{})
507 case DcDataLf{}:
508 dc.pick(U32.is_eq(c, 10), dc.start())
509 case DcTr{+j}:
510 dc.tr(j, c, U32.is_eq(c, dc.tr.want(j)))
511 case DcData{+k}:
512 dc.data(k, 1)
513 case DcDone{}:
514 DcDone{}
515
516def dc.live(st: Dc) -> Bool:
517 match st:
518 case DcDone{}:
519 False{}
520 case DcBad{}:
521 False{}
522 case DcSize{a, b}:
523 True{}
524 case DcExt{n}:
525 True{}
526 case DcSizeLf{n}:
527 True{}
528 case DcData{k}:
529 True{}
530 case DcDataCr{}:
531 True{}
532 case DcDataLf{}:
533 True{}
534 case DcTr{j}:
535 True{}
536
537def dc.feed(s: String, st: Dc, racc: String) -> Dco:
538 match s:
539 case SNil{}:
540 Dco{st, racc, ""}
541 case SCon{h, t}:
542 match st:
543 case DcBad{}:
544 Dco{DcBad{}, racc, ""}
545 case DcDone{}:
546 Dco{DcDone{}, racc, SCon{h, t}}
547 case DcData{+k}:
548 dc.feed(t, dc.data(k, 1), SCon{h, racc})
549 case DcSize{+acc, seen}:
550 dc.feed(t, dc.step(DcSize{acc, seen}, dc.byte(h)), racc)
551 case DcExt{+n}:
552 dc.feed(t, dc.step(DcExt{n}, dc.byte(h)), racc)
553 case DcSizeLf{+n}:
554 dc.feed(t, dc.step(DcSizeLf{n}, dc.byte(h)), racc)
555 case DcDataCr{}:
556 dc.feed(t, dc.step(DcDataCr{}, dc.byte(h)), racc)
557 case DcDataLf{}:
558 dc.feed(t, dc.step(DcDataLf{}, dc.byte(h)), racc)
559 case DcTr{+j}:
560 dc.feed(t, dc.step(DcTr{j}, dc.byte(h)), racc)
561
562def chunk.hold(o: Dco) -> Hold:
563 Dco{st, racc, rest} = o
564 match st:
565 case DcDone{}:
566 HoldBody{String.reverse(racc)}
567 case DcBad{}:
568 HoldBad{}
569 case DcSize{a, b}:
570 HoldMore{}
571 case DcExt{n}:
572 HoldMore{}
573 case DcSizeLf{n}:
574 HoldMore{}
575 case DcData{k}:
576 HoldMore{}
577 case DcDataCr{}:
578 HoldMore{}
579 case DcDataLf{}:
580 HoldMore{}
581 case DcTr{j}:
582 HoldMore{}
583
584def chunk.live(s: String) -> Hold:
585 chunk.hold(dc.feed(s, dc.start(), ""))
586
587def chunk.rest(o: Dco) -> Maybe<&2, String>:
588 Dco{st, racc, rest} = o
589 match st:
590 case DcDone{}:
591 Some{rest}
592 case DcBad{}:
593 None{}
594 case DcSize{a, b}:
595 None{}
596 case DcExt{n}:
597 None{}
598 case DcSizeLf{n}:
599 None{}
600 case DcData{k}:
601 None{}
602 case DcDataCr{}:
603 None{}
604 case DcDataLf{}:
605 None{}
606 case DcTr{j}:
607 None{}
608
609def chunk.suffix(s: String) -> Maybe<&2, String>:
610 chunk.rest(dc.feed(s, dc.start(), ""))
611
612def chunk.decode.hold(h: Hold) -> Maybe<&2, String>:
613 match h:
614 case HoldMore{}:
615 None{}
616 case HoldBad{}:
617 None{}
618 case HoldUntil{b}:
619 None{}
620 case HoldBody{b}:
621 Some{b}
622
623def chunk.decode(s: String) -> Maybe<&2, String>:
624 chunk.decode.hold(chunk.live(s))
625
626def bytes.snd(r: Bytes.Bytes & Bytes.Bytes) -> Bytes.Bytes:
627 (a, b) = r
628 b
629
630def found.at(+from: U32, m: Maybe<&2, U32>) -> Maybe<&2, U32>:
631 match m:
632 case None{}:
633 None{}
634 case Some{+j}:
635 Some{(from + j : U32)}
636
637# A chunked body decoded from piece[i..]: a data run is sliced whole, and every other byte steps dc.
638type Cs is Type:
639 Cs{piece: Bytes.Bytes, i: U32, st: Dc, parts: List<&1, Bytes.Bytes>}
640
641# st: where the decoder stopped. parts: the data so far, newest first. rest: the bytes after a Done body.
642type Ck is Type:
643 Ck{st: Dc, parts: List<&1, Bytes.Bytes>, rest: Bytes.Bytes}
644
645def ck.next(+len: U32, +i: U32, +st: Dc, piece: Bytes.Bytes, parts: List<&1, Bytes.Bytes>) -> Bool & Cs:
646 (Bool.and(U32.is_lt(i, len), dc.live(st)), Cs{piece, i, st, parts})
647
648def ck.data(+len: U32, +i: U32, +k: U32, +m: U32, parts: List<&1, Bytes.Bytes>, r: Bytes.Bytes & Bytes.Bytes) -> Bool & Cs:
649 (piece, run) = r
650 ck.next(len, (i + m : U32), dc.data(k, m), piece, Con{run, parts})
651
652def ck.byte(+len: U32, +i: U32, st: Dc, parts: List<&1, Bytes.Bytes>, r: Bytes.Bytes & Maybe<&2, U32>) -> Bool & Cs:
653 (piece, m) = r
654 match m:
655 case None{}:
656 ck.next(len, i, DcBad{}, piece, parts)
657 case Some{+c}:
658 ck.next(len, (i + 1 : U32), dc.step(st, c), piece, parts)
659
660def ck.step(+len: U32, cs: Cs) -> Bool & Cs:
661 Cs{piece, +i, st, parts} = cs
662 match st:
663 case DcData{+k}:
664 +m = U32.min(k, (len - i : U32))
665 ck.data(len, i, k, m, parts, Bytes.slice(piece, i, m))
666 case DcDone{}:
667 (False{}, Cs{piece, i, DcDone{}, parts})
668 case DcBad{}:
669 (False{}, Cs{piece, i, DcBad{}, parts})
670 case DcSize{+acc, seen}:
671 ck.byte(len, i, DcSize{acc, seen}, parts, Bytes.get(piece, i))
672 case DcExt{+n}:
673 ck.byte(len, i, DcExt{n}, parts, Bytes.get(piece, i))
674 case DcSizeLf{+n}:
675 ck.byte(len, i, DcSizeLf{n}, parts, Bytes.get(piece, i))
676 case DcDataCr{}:
677 ck.byte(len, i, DcDataCr{}, parts, Bytes.get(piece, i))
678 case DcDataLf{}:
679 ck.byte(len, i, DcDataLf{}, parts, Bytes.get(piece, i))
680 case DcTr{+j}:
681 ck.byte(len, i, DcTr{j}, parts, Bytes.get(piece, i))
682
683def ck.rest(st: Dc, parts: List<&1, Bytes.Bytes>, r: Bytes.Bytes & Bytes.Bytes) -> Ck:
684 (piece, rest) = r
685 Ck{st, parts, rest}
686
687def ck.end(+len: U32, cs: Cs) -> Ck:
688 Cs{piece, +i, st, parts} = cs
689 ck.rest(st, parts, Bytes.slice(piece, i, (len - i : U32)))
690
691# Each step reads at least one byte, so len steps are enough.
692def ck.feed(f: Nat, +len: U32, r: Bool & Cs) -> Ck:
693 match f:
694 case 0n:
695 (go, cs) = r
696 ck.end(len, cs)
697 case 1n+p:
698 (go, cs) = r
699 match go:
700 case False{}:
701 ck.end(len, cs)
702 case True{}:
703 ck.feed(p, len, ck.step(len, cs))
704
705def ck(piece: Bytes.Bytes, +st: Dc, parts: List<&1, Bytes.Bytes>) -> Ck:
706 Bytes.Bytes{+len, buf} = piece
707 ck.feed(U32.to_nat(len), len, ck.next(len, 0, st, Bytes.Bytes{len, buf}, parts))
708
709def parse.res.cl.have(+rest: String, +k: Nat, short: Bool) -> Hold:
710 match short:
711 case True{}:
712 HoldMore{}
713 case False{}:
714 HoldBody{String.take(rest, k)}
715
716def parse.res.cl.k(+rest: String, +k: Nat) -> Hold:
717 parse.res.cl.have(rest, k, Nat.is_lt(String.length(rest), k))
718
719def parse.res.cl.n(rest: String, n: Maybe<&2, U32>) -> Hold:
720 match n:
721 case None{}:
722 HoldBad{}
723 case Some{k}:
724 parse.res.cl.k(rest, U32.to_nat(k))
725
726def parse.body.cl(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
727 match hascl:
728 case False{}:
729 HoldBody{""}
730 case True{}:
731 parse.res.cl.n(rest, parse_u32(header(h, "content-length")))
732
733# RFC 9112 §6.3 (4): a request coding other than chunked cannot be framed.
734def parse.body.chunked.eq(rest: String, ok: Bool) -> Hold:
735 match ok:
736 case False{}:
737 HoldBad{}
738 case True{}:
739 chunk.live(rest)
740
741def parse.body.chunked.val(te: String, rest: String) -> Hold:
742 parse.body.chunked.eq(rest, String.eq(String.to_lower(te), "chunked"))
743
744def parse.body.chunked(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
745 match hascl:
746 case True{}:
747 HoldBad{}
748 case False{}:
749 parse.body.chunked.val(header.last(h, "transfer-encoding"), rest)
750
751def parse.body.te(+h: Map<&2, List<&2, String>>, rest: String, te: Bool) -> Hold:
752 match te:
753 case True{}:
754 parse.body.chunked(h, rest, has_header(h, "content-length"))
755 case False{}:
756 parse.body.cl(h, rest, has_header(h, "content-length"))
757
758def parse.body(+h: Map<&2, List<&2, String>>, rest: String) -> Hold:
759 parse.body.te(h, rest, has_header(h, "transfer-encoding"))
760
761# Bad: never a request. More: the head is not whole; read on. Head: the head is whole
762# and valid, and the body is still coming (req.body is empty). Req: a whole request.
763type Got is Type:
764 GotBad{}
765 GotMore{}
766 GotHead{req: Req}
767 GotReq{req: Req}
768
769def parse.finish(method: String, path: String, h: Map<&2, List<&2, String>>, body: Hold) -> Got:
770 match body:
771 case HoldBad{}:
772 GotBad{}
773 case HoldMore{}:
774 GotHead{Req{method, path, h, Bytes.new(0)}}
775 case HoldUntil{b}:
776 GotBad{}
777 case HoldBody{b}:
778 GotReq{Req{method, path, h, Bytes.from_string(b)}}
779
780def parse.host(method: String, path: String, +h: Map<&2, List<&2, String>>, rest: String, has: Bool) -> Got:
781 match has:
782 case False{}:
783 GotBad{}
784 case True{}:
785 parse.finish(method, path, h, parse.body(h, rest))
786
787# RFC 9112 §3.2: only HTTP/1.1 requires Host.
788def parse.fields(method: String, path: String, rest: String, v11: Bool, fs: Maybe<&2, Map<&2, List<&2, String>>>) -> Got:
789 match fs:
790 case None{}:
791 GotBad{}
792 case Some{+h}:
793 parse.host(method, path, h, rest, Bool.or(Bool.not(v11), has_header(h, "host")))
794
795def target_ok(+p: String) -> Bool:
796 Bool.or(String.starts_with(p, "/"), Bool.or(String.eq(p, "*"), String.starts_with(p, "http://")))
797
798def parse.target(method: String, +path: String, headers: List<&2, String>, rest: String, v11: Bool, ok: Bool) -> Got:
799 match ok:
800 case False{}:
801 GotBad{}
802 case True{}:
803 parse.fields(method, path, rest, v11, parse.headers(headers, FieldsOk{empty()}))
804
805def parse.ver(method: String, +path: String, +v: String, headers: List<&2, String>, rest: String, ok: Bool) -> Got:
806 match ok:
807 case False{}:
808 GotBad{}
809 case True{}:
810 parse.target(method, path, headers, rest, String.eq(v, "HTTP/1.1"), target_ok(path))
811
812def parse.empty_method(method: String, path: String, +v: String, headers: List<&2, String>, rest: String, empty: Bool) -> Got:
813 match empty:
814 case True{}:
815 GotBad{}
816 case False{}:
817 parse.ver(method, path, v, headers, rest, Bool.or(String.eq(v, "HTTP/1.1"), String.eq(v, "HTTP/1.0")))
818
819def parse.start3(mpv: String & String & String, headers: List<&2, String>, rest: String) -> Got:
820 (+method, path, v) = mpv
821 parse.empty_method(method, path, v, headers, rest, String.is_empty(method))
822
823def parse.lines(xs: List<&2, String>, rest: String) -> Got:
824 match xs:
825 case Nil{}:
826 GotBad{}
827 case Con{line, headers}:
828 parse.start3(start_line(line), headers, rest)
829
830
831def parse.head(+head: String, rest: String, whole: Bool) -> Got:
832 match whole:
833 case False{}:
834 GotMore{}
835 case True{}:
836 parse.lines(String.lines(head), rest)
837
838def parse.of(hb: String & String & Bool) -> Got:
839 (head, rest, whole) = hb
840 parse.head(head, rest, whole)
841
842# serve reads until this is not GotMore.
843def parse.got(+raw: String) -> Got:
844 parse.of(split_at_blank.flag.go(raw, raw, 0n, 0, False{}))
845
846
847def parse.req(g: Got) -> Maybe<&1, Req>:
848 match g:
849 case GotReq{req}:
850 Some{req}
851 case GotBad{}:
852 None{}
853 case GotMore{}:
854 None{}
855 case GotHead{req}:
856 None{}
857
858def parse(raw: String) -> Maybe<&1, Req>:
859 parse.req(parse.got(raw))
860
861def parse.res.cl(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
862 match hascl:
863 case False{}:
864 HoldBody{rest}
865 case True{}:
866 parse.res.cl.n(rest, parse_u32(header(h, "content-length")))
867
868def parse.res.chunked.eq(rest: String, ok: Bool) -> Hold:
869 match ok:
870 case False{}:
871 HoldUntil{rest}
872 case True{}:
873 chunk.live(rest)
874
875def parse.res.chunked.val(te: String, rest: String) -> Hold:
876 parse.res.chunked.eq(rest, String.eq(String.to_lower(te), "chunked"))
877
878def parse.res.chunked(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
879 match hascl:
880 case True{}:
881 HoldBad{}
882 case False{}:
883 parse.res.chunked.val(header.last(h, "transfer-encoding"), rest)
884
885def parse.res.te(+h: Map<&2, List<&2, String>>, rest: String, te: Bool) -> Hold:
886 match te:
887 case True{}:
888 parse.res.chunked(h, rest, has_header(h, "content-length"))
889 case False{}:
890 parse.res.cl(h, rest, has_header(h, "content-length"))
891
892def parse.res.body(+h: Map<&2, List<&2, String>>, rest: String) -> Hold:
893 parse.res.te(h, rest, has_header(h, "transfer-encoding"))
894
895# Bad: never a message. More: a valid prefix; read on. Done: a whole response.
896type Frame is Type:
897 FrameBad{}
898 FrameMore{}
899 FrameDone{res: Res}
900
901# RFC 9112 §8: a message cut short by close is incomplete, not valid.
902def frame.cut(closed: Bool) -> Frame:
903 match closed:
904 case True{}:
905 FrameBad{}
906 case False{}:
907 FrameMore{}
908
909def frame.wait(res: Res, wait: Bool) -> Frame:
910 match wait:
911 case True{}:
912 FrameMore{}
913 case False{}:
914 FrameDone{res}
915
916def frame.done(status: U32, h: Map<&2, List<&2, String>>, body: Hold, +closed: Bool, open: Bool) -> Frame:
917 match body:
918 case HoldBad{}:
919 FrameBad{}
920 case HoldMore{}:
921 frame.cut(closed)
922 case HoldUntil{b}:
923 frame.wait(Res{status, h, Bytes.from_string(b)}, Bool.not(closed))
924 case HoldBody{b}:
925 frame.wait(Res{status, h, Bytes.from_string(b)}, Bool.and(open, Bool.not(closed)))
926
927# RFC 9112 §6.3 (8): no TE and no CL ⇒ the body runs until the server closes.
928def frame.open(+h: Map<&2, List<&2, String>>) -> Bool:
929 Bool.not(Bool.or(has_header(h, "transfer-encoding"), has_header(h, "content-length")))
930
931# RFC 9112 §6.3 (1): HEAD, 1xx, 204 and 304 responses end at the blank line.
932def frame.nobody(+status: U32, head: Bool) -> Bool:
933 Bool.or(head, Bool.or(U32.is_lt(status, 200), Bool.or(U32.is_eq(status, 204), U32.is_eq(status, 304))))
934
935# 101 is the final response. Other 1xx are interim; a final response follows.
936def frame.interim(+status: U32) -> Bool:
937 Bool.and(U32.is_lt(status, 200), Bool.not(U32.is_eq(status, 101)))
938
939def frame.status(status: U32, +h: Map<&2, List<&2, String>>, rest: String, closed: Bool, nobody: Bool) -> Frame:
940 match nobody:
941 case True{}:
942 FrameDone{Res{status, h, Bytes.new(0)}}
943 case False{}:
944 frame.done(status, h, parse.res.body(h, rest), closed, frame.open(h))
945
946def parse.res.fields(+status: U32, rest: String, fs: Maybe<&2, Map<&2, List<&2, String>>>, closed: Bool, head: Bool) -> Frame:
947 match fs:
948 case None{}:
949 FrameBad{}
950 case Some{h}:
951 frame.status(status, h, rest, closed, frame.nobody(status, head))
952
953def parse.res.num(code: Maybe<&2, U32>, headers: List<&2, String>, rest: String, closed: Bool, head: Bool) -> Frame:
954 match code:
955 case None{}:
956 FrameBad{}
957 case Some{n}:
958 parse.res.fields(n, rest, parse.headers(headers, FieldsOk{empty()}), closed, head)
959
960def parse.res.ver(code: String, headers: List<&2, String>, rest: String, closed: Bool, head: Bool, ok: Bool) -> Frame:
961 match ok:
962 case False{}:
963 FrameBad{}
964 case True{}:
965 parse.res.num(parse_u32(code), headers, rest, closed, head)
966
967def parse.res.start3(mpv: String & String & String, headers: List<&2, String>, rest: String, closed: Bool, head: Bool) -> Frame:
968 (+ver, code, reason) = mpv
969 parse.res.ver(code, headers, rest, closed, head, Bool.or(String.eq(ver, "HTTP/1.1"), String.eq(ver, "HTTP/1.0")))
970
971def parse.res.lines(xs: List<&2, String>, rest: String, closed: Bool, head: Bool) -> Frame:
972 match xs:
973 case Nil{}:
974 FrameBad{}
975 case Con{line, headers}:
976 parse.res.start3(start_line(line), headers, rest, closed, head)
977
978def parse.res.blank(hd: String, rest: String, +closed: Bool, head: Bool, ok: Bool) -> Frame:
979 match ok:
980 case False{}:
981 frame.cut(closed)
982 case True{}:
983 parse.res.lines(String.lines(hd), rest, closed, head)
984
985def parse.res.of(hb: String & String, closed: Bool, head: Bool) -> Frame:
986 (+hd, rest) = hb
987 parse.res.blank(hd, rest, closed, head, blank_end(hd))
988
989type Lead is Data:
990 LeadCut{}
991 LeadFinal{}
992 LeadSkip{+rest: String}
993
994def frame.lead.if(rest: String, interim: Bool) -> Lead:
995 match interim:
996 case True{}:
997 LeadSkip{rest}
998 case False{}:
999 LeadFinal{}
1000
1001def frame.lead.num(n: Maybe<&2, U32>, rest: String) -> Lead:
1002 match n:
1003 case None{}:
1004 LeadFinal{}
1005 case Some{s}:
1006 frame.lead.if(rest, frame.interim(s))
1007
1008def frame.lead.code(mpv: String & String & String, rest: String) -> Lead:
1009 (ver, code, reason) = mpv
1010 frame.lead.num(parse_u32(code), rest)
1011
1012def frame.lead.lines(xs: List<&2, String>, rest: String) -> Lead:
1013 match xs:
1014 case Nil{}:
1015 LeadFinal{}
1016 case Con{line, headers}:
1017 frame.lead.code(start_line(line), rest)
1018
1019def frame.lead.blank(+hd: String, rest: String, ok: Bool) -> Lead:
1020 match ok:
1021 case False{}:
1022 LeadCut{}
1023 case True{}:
1024 frame.lead.lines(String.lines(hd), rest)
1025
1026def frame.lead(hb: String & String) -> Lead:
1027 (+hd, rest) = hb
1028 frame.lead.blank(hd, rest, blank_end(hd))
1029
1030def frame.at.cont(+raw: String, lead: Lead) -> String:
1031 match lead:
1032 case LeadCut{}:
1033 raw
1034 case LeadFinal{}:
1035 raw
1036 case LeadSkip{rest}:
1037 rest
1038
1039def frame.at.zero.go(+raw: String, closed: Bool, head: Bool, lead: Lead) -> Frame:
1040 match lead:
1041 case LeadCut{}:
1042 frame.cut(closed)
1043 case LeadFinal{}:
1044 parse.res.of(split_at_blank(raw), closed, head)
1045 case LeadSkip{rest}:
1046 FrameBad{}
1047
1048def frame.at.zero.of(+raw: String, closed: Bool, head: Bool) -> Frame:
1049 frame.at.zero.go(raw, closed, head, frame.lead(split_at_blank(raw)))
1050
1051def frame.at.pos.do(f: Nat, +raw: String, closed: Bool, head: Bool, hb: String & String, lead: Lead) -> Frame:
1052 match f:
1053 case 0n:
1054 match lead:
1055 case LeadCut{}:
1056 frame.cut(closed)
1057 case LeadFinal{}:
1058 parse.res.of(hb, closed, head)
1059 case LeadSkip{+rest}:
1060 frame.at.zero.of(rest, closed, head)
1061 case 1n+g:
1062 match lead:
1063 case LeadCut{}:
1064 frame.cut(closed)
1065 case LeadFinal{}:
1066 parse.res.of(hb, closed, head)
1067 case LeadSkip{+rest}:
1068 frame.at.pos.do(g, rest, closed, head, split_at_blank(rest), frame.lead(split_at_blank(rest)))
1069
1070def frame.at.zero(+raw: String, closed: Bool, head: Bool) -> Frame:
1071 frame.at.zero.of(raw, closed, head)
1072
1073# ponytail: 8 interim responses; raise the fuel if a server sends more
1074def frame.at(fuel: Nat, +raw: String, closed: Bool, head: Bool) -> Frame:
1075 match fuel:
1076 case 0n:
1077 frame.at.zero(raw, closed, head)
1078 case 1n+f:
1079 frame.at.pos.do(f, raw, closed, head, split_at_blank(raw), frame.lead(split_at_blank(raw)))
1080
1081# frame(bytes so far, server closed?, request was HEAD?)
1082def frame(raw: String, closed: Bool, head: Bool) -> Frame:
1083 frame.at(8n, raw, closed, head)
1084
1085def frame.res(f: Frame) -> Maybe<&1, Res>:
1086 match f:
1087 case FrameDone{res}:
1088 Some{res}
1089 case FrameBad{}:
1090 None{}
1091 case FrameMore{}:
1092 None{}
1093
1094def parse_res(raw: String) -> Maybe<&1, Res>:
1095 frame.res(frame(raw, True{}, False{}))
1096
1097def res_fields.res(res: Res, k: String) -> List<&2, String>:
1098 Res{status, headers, body} = res
1099 fields(headers, k)
1100
1101def res_fields(m: Maybe<&1, Res>, k: String) -> List<&2, String>:
1102 match m:
1103 case None{}:
1104 Nil{}
1105 case Some{res}:
1106 res_fields.res(res, k)
1107
1108# The response body as it arrives. Len: bytes left. Chunk: the decoder. Close: until the
1109# server closes. Done: the body is whole. Bad: it cannot become a body.
1110type Rb is Data:
1111 RbLen{left: U32}
1112 RbChunk{st: Dc}
1113 RbClose{}
1114 RbDone{}
1115 RbBad{}
1116
1117def rb.cl(n: Maybe<&2, U32>) -> Maybe<&2, Rb>:
1118 match n:
1119 case None{}:
1120 None{}
1121 case Some{+k}:
1122 Some{Bool.pick(Rb, U32.is_zero(k), RbDone{}, RbLen{k})}
1123
1124def rb.te(+h: Map<&2, List<&2, String>>, cl: Bool) -> Maybe<&2, Rb>:
1125 match cl:
1126 case True{}:
1127 None{}
1128 case False{}:
1129 Some{Bool.pick(Rb, String.eq(String.to_lower(header.last(h, "transfer-encoding")), "chunked"), RbChunk{dc.start()}, RbClose{})}
1130
1131def rb.len(+h: Map<&2, List<&2, String>>, te: Bool) -> Maybe<&2, Rb>:
1132 match te:
1133 case True{}:
1134 rb.te(h, has_header(h, "content-length"))
1135 case False{}:
1136 Bool.pick(Maybe<&2, Rb>, has_header(h, "content-length"), rb.cl(parse_u32(header(h, "content-length"))), Some{RbClose{}})
1137
1138# RFC 9112 §6.3: how the body of this response ends. None: it cannot be framed.
1139def rb.of(+h: Map<&2, List<&2, String>>, nobody: Bool) -> Maybe<&2, Rb>:
1140 match nobody:
1141 case True{}:
1142 Some{RbDone{}}
1143 case False{}:
1144 rb.len(h, has_header(h, "transfer-encoding"))
1145
1146# rb: how the body goes on. parts: body bytes so far, newest first. rest: bytes past a Done body.
1147type Bf is Type:
1148 Bf{rb: Rb, parts: List<&1, Bytes.Bytes>, rest: Bytes.Bytes}
1149
1150def rb.len.cut(parts: List<&1, Bytes.Bytes>, +len: U32, +left: U32, r: Bytes.Bytes & Bytes.Bytes) -> Bf:
1151 (piece, data) = r
1152 Bf{RbDone{}, Con{data, parts}, bytes.snd(Bytes.slice(piece, left, (len - left : U32)))}
1153
1154def rb.len.have(short: Bool, +left: U32, parts: List<&1, Bytes.Bytes>, +len: U32, piece: Bytes.Bytes) -> Bf:
1155 match short:
1156 case True{}:
1157 Bf{RbLen{(left - len : U32)}, Con{piece, parts}, Bytes.new(0)}
1158 case False{}:
1159 rb.len.cut(parts, len, left, Bytes.slice(piece, 0, left))
1160
1161def rb.chunk(c: Ck) -> Bf:
1162 Ck{st, parts, rest} = c
1163 match st:
1164 case DcDone{}:
1165 Bf{RbDone{}, parts, rest}
1166 case DcBad{}:
1167 Bf{RbBad{}, parts, rest}
1168 case DcSize{a, b}:
1169 Bf{RbChunk{DcSize{a, b}}, parts, rest}
1170 case DcExt{x}:
1171 Bf{RbChunk{DcExt{x}}, parts, rest}
1172 case DcSizeLf{x}:
1173 Bf{RbChunk{DcSizeLf{x}}, parts, rest}
1174 case DcData{k}:
1175 Bf{RbChunk{DcData{k}}, parts, rest}
1176 case DcDataCr{}:
1177 Bf{RbChunk{DcDataCr{}}, parts, rest}
1178 case DcDataLf{}:
1179 Bf{RbChunk{DcDataLf{}}, parts, rest}
1180 case DcTr{j}:
1181 Bf{RbChunk{DcTr{j}}, parts, rest}
1182
1183# The body bytes in piece, added to parts.
1184def rb.feed(rb: Rb, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Bf:
1185 match rb:
1186 case RbLen{+left}:
1187 Bytes.Bytes{+len, buf} = piece
1188 rb.len.have(U32.is_lt(len, left), left, parts, len, Bytes.Bytes{len, buf})
1189 case RbChunk{st}:
1190 rb.chunk(ck(piece, st, parts))
1191 case RbClose{}:
1192 Bf{RbClose{}, Con{piece, parts}, Bytes.new(0)}
1193 case RbDone{}:
1194 Bf{RbDone{}, parts, piece}
1195 case RbBad{}:
1196 Bf{RbBad{}, parts, piece}
1197
1198# RFC 9112 §8: only a close-delimited body may end at close.
1199def rb.eof(rb: Rb) -> Bool:
1200 match rb:
1201 case RbClose{}:
1202 True{}
1203 case RbDone{}:
1204 True{}
1205 case RbLen{n}:
1206 False{}
1207 case RbChunk{st}:
1208 False{}
1209 case RbBad{}:
1210 False{}
1211
1212def rb.body(parts: List<&1, Bytes.Bytes>) -> Bytes.Bytes:
1213 Bytes.concat(List.reverse(&1, Bytes.Bytes, parts))
1214
1215# The head scan. Seek: look for the blank line from byte from; k interim heads are behind.
1216# Wait: no blank line yet. Res: the final head, how its body ends, and the bytes after it.
1217type Hs is Type:
1218 HsSeek{buf: Bytes.Bytes, from: U32, k: U32}
1219 HsWait{buf: Bytes.Bytes, k: U32}
1220 HsBad{}
1221 HsRes{res: Res, rb: Rb, rest: Bytes.Bytes}
1222
1223def hs.final(+status: U32, +h: Map<&2, List<&2, String>>, rest: Bytes.Bytes, m: Maybe<&2, Rb>) -> Hs:
1224 match m:
1225 case None{}:
1226 HsBad{}
1227 case Some{rb}:
1228 HsRes{Res{status, h, Bytes.new(0)}, rb, rest}
1229
1230def hs.skip(more: Bool, +k: U32, rest: Bytes.Bytes) -> Hs:
1231 match more:
1232 case True{}:
1233 HsSeek{rest, 0, (k + 1 : U32)}
1234 case False{}:
1235 HsBad{}
1236
1237def hs.pick(interim: Bool, +head: Bool, +k: U32, +status: U32, +h: Map<&2, List<&2, String>>, rest: Bytes.Bytes) -> Hs:
1238 match interim:
1239 case True{}:
1240 hs.skip(U32.is_lt(k, 8), k, rest)
1241 case False{}:
1242 hs.final(status, h, rest, rb.of(h, frame.nobody(status, head)))
1243
1244def hs.res(+head: Bool, +k: U32, rest: Bytes.Bytes, res: Res) -> Hs:
1245 Res{+status, +h, body} = res
1246 hs.pick(frame.interim(status), head, k, status, h, rest)
1247
1248# The head alone, framed as a HEAD response so it stops at the blank line.
1249def hs.parsed(+head: Bool, +k: U32, rest: Bytes.Bytes, f: Frame) -> Hs:
1250 match f:
1251 case FrameDone{res}:
1252 hs.res(head, k, rest, res)
1253 case FrameBad{}:
1254 HsBad{}
1255 case FrameMore{}:
1256 HsBad{}
1257
1258def hs.split(+head: Bool, +k: U32, +hlen: U32, +len: U32, r: Bytes.Bytes & Bytes.Bytes) -> Hs:
1259 (buf, hb) = r
1260 hs.parsed(head, k, bytes.snd(Bytes.slice(buf, hlen, (len - hlen : U32))), parse.res.of(split_at_blank(Bytes.to_string(hb)), False{}, True{}))
1261
1262def hs.hit(+head: Bool, +k: U32, +len: U32, buf: Bytes.Bytes, at: Maybe<&2, U32>) -> Hs:
1263 match at:
1264 case None{}:
1265 HsWait{buf, k}
1266 case Some{+i}:
1267 +hlen = (i + 4 : U32)
1268 hs.split(head, k, hlen, len, Bytes.slice(buf, 0, hlen))
1269
1270def hs.seek.of(+head: Bool, +k: U32, +len: U32, +from: U32, buf: Bytes.Bytes, r: Bytes.Bytes & Maybe<&2, U32>) -> Hs:
1271 (tail, m) = r
1272 hs.hit(head, k, len, buf, found.at(from, m))
1273
1274def hs.seek(+head: Bool, +k: U32, +len: U32, +from: U32, r: Bytes.Bytes & Bytes.Bytes) -> Hs:
1275 (buf, tail) = r
1276 hs.seek.of(head, k, len, from, buf, Bytes.find(tail, "\r\n\r\n"))
1277
1278def hs.step(+head: Bool, st: Hs) -> Hs:
1279 match st:
1280 case HsSeek{buf, +from, +k}:
1281 Bytes.Bytes{+len, b} = buf
1282 hs.seek(head, k, len, from, Bytes.slice(Bytes.Bytes{len, b}, from, (len - from : U32)))
1283 case HsWait{buf, k}:
1284 HsWait{buf, k}
1285 case HsBad{}:
1286 HsBad{}
1287 case HsRes{res, rb, rest}:
1288 HsRes{res, rb, rest}
1289
1290# Each step ends the scan or passes one interim head, and at most 8 interim heads pass.
1291def hs.scan(fuel: Nat, +head: Bool, st: Hs) -> Hs:
1292 match fuel:
1293 case 0n:
1294 match st:
1295 case HsSeek{buf, from, k}:
1296 HsBad{}
1297 case HsWait{buf, k}:
1298 HsWait{buf, k}
1299 case HsBad{}:
1300 HsBad{}
1301 case HsRes{res, rb, rest}:
1302 HsRes{res, rb, rest}
1303 case 1n+f:
1304 hs.scan(f, head, hs.step(head, st))
1305
1306# piece joins buf; only the new bytes, and the 3 before them, can finish the blank line.
1307def hs.more(+head: Bool, +k: U32, buf: Bytes.Bytes, piece: Bytes.Bytes) -> Hs:
1308 Bytes.Bytes{+ol, ob} = buf
1309 hs.scan(10n, head, HsSeek{Bytes.append(Bytes.Bytes{ol, ob}, piece), Bool.pick(U32, U32.is_lt(ol, 3), 0, (ol - 3 : U32)), k})
1310
1311# Untrusted servers must not grow the buffer without bound.
1312def fetch.max() -> Nat:
1313 U32.to_nat(16777216)
1314
1315# A response read in pieces. Head: the head is not whole yet. Body: it is, and parts is the body so far.
1316# Len: a Content-Length body in one buffer of that size, with left bytes still to come.
1317type Rv is Type:
1318 RvHead{buf: Bytes.Bytes, k: U32}
1319 RvBody{res: Res, rb: Rb, parts: List<&1, Bytes.Bytes>}
1320 RvLen{res: Res, left: U32, body: Bytes.Bytes}
1321
1322# More: read on. Done: the response, and the bytes after it when the body is self-delimited.
1323type Rt is Type:
1324 RtMore{rv: Rv}
1325 RtBad{}
1326 RtDone{res: Res, rest: Maybe<&1, Bytes.Bytes>}
1327
1328def rv.start() -> Rv:
1329 RvHead{Bytes.new(0), 0}
1330
1331def rv.whole(res: Res, b: Bytes.Bytes, rest: Maybe<&1, Bytes.Bytes>) -> Rt:
1332 Res{status, headers, body} = res
1333 RtDone{Res{status, headers, b}, rest}
1334
1335def rv.done(res: Res, parts: List<&1, Bytes.Bytes>, rest: Maybe<&1, Bytes.Bytes>) -> Rt:
1336 rv.whole(res, rb.body(parts), rest)
1337
1338def rl.put.of(+total: U32, +len: U32, r: Array<U32> & Array<U32>) -> Bytes.Bytes & Bytes.Bytes:
1339 (src, dst) = r
1340 (Bytes.Bytes{total, dst}, Bytes.Bytes{len, src})
1341
1342# The first m bytes of piece, written into body after the total - left bytes already there.
1343def rl.put(+m: U32, +left: U32, body: Bytes.Bytes, piece: Bytes.Bytes) -> Bytes.Bytes & Bytes.Bytes:
1344 Bytes.Bytes{+total, dst} = body
1345 Bytes.Bytes{+len, src} = piece
1346 rl.put.of(total, len, Bytes.copy(m, src, dst, 0, (total - left : U32)))
1347
1348def rl.fed(short: Bool, res: Res, +left: U32, +len: U32, r: Bytes.Bytes & Bytes.Bytes) -> Rt:
1349 match short:
1350 case True{}:
1351 (body, piece) = r
1352 RtMore{RvLen{res, (left - len : U32), body}}
1353 case False{}:
1354 (body, piece) = r
1355 rv.whole(res, body, Some{bytes.snd(Bytes.slice(piece, left, (len - left : U32)))})
1356
1357def rl.feed(res: Res, +left: U32, body: Bytes.Bytes, piece: Bytes.Bytes) -> Rt:
1358 Bytes.Bytes{+len, buf} = piece
1359 rl.fed(U32.is_lt(len, left), res, left, len, rl.put(U32.min(len, left), left, body, Bytes.Bytes{len, buf}))
1360
1361def rv.fed(res: Res, bf: Bf) -> Rt:
1362 Bf{rb, parts, rest} = bf
1363 match rb:
1364 case RbDone{}:
1365 rv.done(res, parts, Some{rest})
1366 case RbBad{}:
1367 RtBad{}
1368 case RbLen{n}:
1369 RtMore{RvBody{res, RbLen{n}, parts}}
1370 case RbChunk{st}:
1371 RtMore{RvBody{res, RbChunk{st}, parts}}
1372 case RbClose{}:
1373 RtMore{RvBody{res, RbClose{}, parts}}
1374
1375# Some{left}: a Content-Length body small enough to allocate up front. Larger ones fail at the fetch cap.
1376def rb.buf(rb: Rb) -> Maybe<&2, U32>:
1377 match rb:
1378 case RbLen{+left}:
1379 Bool.pick(Maybe<&2, U32>, Nat.is_lt(fetch.max(), U32.to_nat(left)), None{}, Some{left})
1380 case RbChunk{st}:
1381 None{}
1382 case RbClose{}:
1383 None{}
1384 case RbDone{}:
1385 None{}
1386 case RbBad{}:
1387 None{}
1388
1389def rv.body(m: Maybe<&2, U32>, res: Res, rb: Rb, rest: Bytes.Bytes) -> Rt:
1390 match m:
1391 case None{}:
1392 rv.fed(res, rb.feed(rb, Nil{}, rest))
1393 case Some{+left}:
1394 rl.feed(res, left, Bytes.new(left), rest)
1395
1396def rv.head(hs: Hs) -> Rt:
1397 match hs:
1398 case HsWait{buf, k}:
1399 RtMore{RvHead{buf, k}}
1400 case HsBad{}:
1401 RtBad{}
1402 case HsSeek{buf, from, k}:
1403 RtBad{}
1404 case HsRes{res, +rb, rest}:
1405 rv.body(rb.buf(rb), res, rb, rest)
1406
1407def rv.eof(res: Res, parts: List<&1, Bytes.Bytes>, ok: Bool) -> Rt:
1408 match ok:
1409 case True{}:
1410 rv.done(res, parts, None{})
1411 case False{}:
1412 RtBad{}
1413
1414# One read: piece, or the server closed (RFC 9112 §8: a message cut short is not a message).
1415def rv.step(closed: Bool, +head: Bool, rv: Rv, piece: Bytes.Bytes) -> Rt:
1416 match closed:
1417 case True{}:
1418 match rv:
1419 case RvHead{buf, k}:
1420 RtBad{}
1421 case RvBody{res, rb, parts}:
1422 rv.eof(res, parts, rb.eof(rb))
1423 case RvLen{res, left, body}:
1424 RtBad{}
1425 case False{}:
1426 match rv:
1427 case RvHead{buf, +k}:
1428 rv.head(hs.more(head, k, buf, piece))
1429 case RvBody{res, rb, parts}:
1430 rv.fed(res, rb.feed(rb, parts, piece))
1431 case RvLen{res, +left, body}:
1432 rl.feed(res, left, body, piece)
1433
1434def rv.end(closed: Bool, +head: Bool, t: Rt) -> Rt:
1435 match closed:
1436 case False{}:
1437 t
1438 case True{}:
1439 match t:
1440 case RtMore{rv}:
1441 rv.step(True{}, head, rv, Bytes.new(0))
1442 case RtBad{}:
1443 RtBad{}
1444 case RtDone{res, rest}:
1445 RtDone{res, rest}
1446
1447def rv.go(xs: List<&2, String>, closed: Bool, +head: Bool, t: Rt) -> Rt:
1448 match xs:
1449 case Nil{}:
1450 rv.end(closed, head, t)
1451 case Con{+x, rest}:
1452 match t:
1453 case RtMore{rv}:
1454 rv.go(rest, closed, head, rv.step(False{}, head, rv, Bytes.from_string(x)))
1455 case RtBad{}:
1456 RtBad{}
1457 case RtDone{res, r}:
1458 RtDone{res, r}
1459
1460def rt.frame(t: Rt) -> Frame:
1461 match t:
1462 case RtMore{rv}:
1463 FrameMore{}
1464 case RtBad{}:
1465 FrameBad{}
1466 case RtDone{res, rest}:
1467 FrameDone{res}
1468
1469# What the read loop makes of these pieces, then a close when closed is set.
1470def res.frame(xs: List<&2, String>, closed: Bool, +head: Bool) -> Frame:
1471 rt.frame(rv.go(xs, closed, head, RtMore{rv.start()}))
1472
1473def rt.rest(t: Rt) -> Maybe<&1, Bytes.Bytes>:
1474 match t:
1475 case RtMore{rv}:
1476 None{}
1477 case RtBad{}:
1478 None{}
1479 case RtDone{res, rest}:
1480 rest
1481
1482def after.of(m: Maybe<&1, Bytes.Bytes>) -> Maybe<&2, String>:
1483 match m:
1484 case None{}:
1485 None{}
1486 case Some{b}:
1487 Some{Bytes.to_string(b)}
1488
1489# Bytes after a complete self-delimited message. None if it is not one yet.
1490def after(+raw: String, +head: Bool) -> Maybe<&2, String>:
1491 after.of(rt.rest(rv.go([raw], False{}, head, RtMore{rv.start()})))
1492
1493def req.v11.ver(mpv: String & String & String) -> Bool:
1494 (+method, path, v) = mpv
1495 String.eq(v, "HTTP/1.1")
1496
1497def req.v11.line(+line: String) -> Bool:
1498 req.v11.ver(start_line(line))
1499
1500def req.v11.lines(xs: List<&2, String>) -> Bool:
1501 match xs:
1502 case Nil{}:
1503 False{}
1504 case Con{line, headers}:
1505 req.v11.line(line)
1506
1507def req.v11.pick(+head: String, ok: Bool) -> Bool:
1508 match ok:
1509 case False{}:
1510 False{}
1511 case True{}:
1512 req.v11.lines(String.lines(head))
1513
1514def req.v11.of(hb: String & String) -> Bool:
1515 (+head, rest) = hb
1516 req.v11.pick(head, blank_end(head))
1517
1518def req.v11(+raw: String) -> Bool:
1519 req.v11.of(split_at_blank(raw))
1520
1521def req.conn_close(+headers: Map<&2, List<&2, String>>) -> Bool:
1522 String.eq(String.to_lower(header(headers, "connection")), "close")
1523
1524def res.conn_close(+headers: Map<&2, List<&2, String>>) -> Bool:
1525 String.eq(String.to_lower(header(headers, "connection")), "close")
1526
1527def serve.fail_close(+status: U32) -> Bool:
1528 Bool.or(U32.is_eq(status, 400), Bool.or(U32.is_eq(status, 413), U32.is_eq(status, 431)))
1529
1530def serve.keep.ok(fail: Bool, res_close: Bool) -> Bool:
1531 match fail:
1532 case True{}:
1533 False{}
1534 case False{}:
1535 Bool.not(res_close)
1536
1537def serve.keep.v11(v11: Bool, +req_close: Bool, +status: U32, res_close: Bool) -> Bool:
1538 match v11:
1539 case False{}:
1540 False{}
1541 case True{}:
1542 match req_close:
1543 case True{}:
1544 False{}
1545 case False{}:
1546 serve.keep.ok(serve.fail_close(status), res_close)
1547
1548def serve.keep(+headers: Map<&2, List<&2, String>>, v11: Bool, +status: U32, +res: Map<&2, List<&2, String>>) -> Bool:
1549 serve.keep.v11(v11, req.conn_close(headers), status, res.conn_close(res))
1550
1551
1552def again.keep(close: Bool, x: Bytes.Bytes) -> Maybe<&1, Bytes.Bytes>:
1553 match close:
1554 case True{}:
1555 None{}
1556 case False{}:
1557 Some{x}
1558
1559def again.rest(close: Bool, rest: Maybe<&1, Bytes.Bytes>) -> Maybe<&1, Bytes.Bytes>:
1560 match rest:
1561 case None{}:
1562 None{}
1563 case Some{x}:
1564 again.keep(close, x)
1565
1566# The bytes past the response when the socket can take another request: the request did not
1567# ask to close, the response is self-delimited, and the peer did not say close.
1568def again(close: Bool, +h: Map<&2, List<&2, String>>, rest: Maybe<&1, Bytes.Bytes>) -> Maybe<&1, Bytes.Bytes>:
1569 match close:
1570 case True{}:
1571 None{}
1572 case False{}:
1573 again.rest(String.eq(String.to_lower(header(h, "connection")), "close"), rest)
1574
1575def res_body.res(res: Res) -> Bytes.Bytes:
1576 Res{status, headers, body} = res
1577 body
1578
1579def res_body(m: Maybe<&1, Res>) -> Bytes.Bytes:
1580 match m:
1581 case None{}:
1582 Bytes.new(0)
1583 case Some{res}:
1584 res_body.res(res)
1585
1586def text(res: Res) -> String:
1587 Enc.utf8.decode(res_body.res(res))
1588
1589# UTF-8 is checked, not repaired: bad UTF-8 in a string gives None (RFC 8259 §8.1).
1590def json(res: Res) -> Maybe<&1, Json.Val>:
1591 Json.parse.bytes(res_body.res(res))
1592
1593def got_body.req(req: Req) -> Bytes.Bytes:
1594 Req{method, path, headers, body} = req
1595 body
1596
1597def got_body(m: Maybe<&1, Req>) -> Bytes.Bytes:
1598 match m:
1599 case None{}:
1600 Bytes.new(0)
1601 case Some{req}:
1602 got_body.req(req)
1603
1604def body.of(hb: String & String) -> String:
1605 (h, b) = hb
1606 b
1607
1608def body(s: String) -> String:
1609 body.of(split_at_blank.go(s, False{}, 0, SNil{}))
1610
1611def headers_lines(+k: String, vs: List<&2, String>, acc: String) -> String:
1612 match vs:
1613 case Nil{}:
1614 acc
1615 case Con{v, t}:
1616 headers_lines(k, t, acc ++ ("\r\n" ++ sanitize(k) ++ ": " ++ sanitize(v)))
1617
1618def headers_block.go(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>, acc: String) -> String:
1619 match xs:
1620 case Nil{}:
1621 acc
1622 case (k, vs) <> t:
1623 headers_block.go(t, headers_lines(k, vs, acc))
1624
1625def headers_block(h: Map<&2, List<&2, String>>) -> String:
1626 headers_block.go(Map.to_list(&2, List<&2, String>, h), "")
1627
1628# RFC 9110 §15. An unknown code gets an empty reason, which RFC 9112 §4 allows.
1629type Reason is Data:
1630 Reason{code: U32, text: String}
1631
1632def reasons() -> List<&2, Reason>:
1633 [Reason{100, "Continue"}, Reason{101, "Switching Protocols"}, Reason{103, "Early Hints"},
1634 Reason{200, "OK"}, Reason{201, "Created"}, Reason{202, "Accepted"}, Reason{203, "Non-Authoritative Information"}, Reason{204, "No Content"}, Reason{205, "Reset Content"}, Reason{206, "Partial Content"},
1635 Reason{300, "Multiple Choices"}, Reason{301, "Moved Permanently"}, Reason{302, "Found"}, Reason{303, "See Other"}, Reason{304, "Not Modified"}, Reason{307, "Temporary Redirect"}, Reason{308, "Permanent Redirect"},
1636 Reason{400, "Bad Request"}, Reason{401, "Unauthorized"}, Reason{402, "Payment Required"}, Reason{403, "Forbidden"}, Reason{404, "Not Found"}, Reason{405, "Method Not Allowed"}, Reason{406, "Not Acceptable"}, Reason{407, "Proxy Authentication Required"}, Reason{408, "Request Timeout"}, Reason{409, "Conflict"}, Reason{410, "Gone"}, Reason{411, "Length Required"}, Reason{412, "Precondition Failed"}, Reason{413, "Content Too Large"}, Reason{414, "URI Too Long"}, Reason{415, "Unsupported Media Type"}, Reason{416, "Range Not Satisfiable"}, Reason{417, "Expectation Failed"}, Reason{421, "Misdirected Request"}, Reason{422, "Unprocessable Content"}, Reason{426, "Upgrade Required"}, Reason{428, "Precondition Required"}, Reason{429, "Too Many Requests"}, Reason{431, "Request Header Fields Too Large"},
1637 Reason{500, "Internal Server Error"}, Reason{501, "Not Implemented"}, Reason{502, "Bad Gateway"}, Reason{503, "Service Unavailable"}, Reason{504, "Gateway Timeout"}, Reason{505, "HTTP Version Not Supported"}]
1638
1639def reason.go(xs: List<&2, Reason>, +status: U32) -> String:
1640 match xs:
1641 case Nil{}:
1642 ""
1643 case Con{Reason{k, v}, t}:
1644 Bool.pick(String, U32.is_eq(k, status), v, reason.go(t, status))
1645
1646def reason(+status: U32) -> String:
1647 reason.go(reasons(), status)
1648
1649def response(+status: U32, headers: Map<&2, List<&2, String>>, body: String) -> String:
1650 ("HTTP/1.1 " ++ U32.show(status) ++ " " ++ reason(status) ++ headers_block(headers)) ++ ("\r\n\r\n" ++ body)
1651
1652def encode.body(head: Bool, top: Bytes.Bytes, body: Bytes.Bytes) -> Bytes.Bytes:
1653 match head:
1654 case True{}:
1655 top
1656 case False{}:
1657 Bytes.append(top, body)
1658
1659def encode.len(+status: U32, headers: Map<&2, List<&2, String>>, head: Bool, body: Bytes.Bytes) -> Bytes.Bytes:
1660 Bytes.Bytes{+len, buf} = body
1661 encode.body(head, Bytes.from_string(response(status, set(headers, "content-length", U32.show(len)), "")), Bytes.Bytes{len, buf})
1662
1663# RFC 9110 §6.4.1, §8.6: 1xx, 204 and 304 have no body; HEAD gets the length but no body.
1664def encode.pick(+status: U32, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, head: Bool, nobody: Bool) -> Bytes.Bytes:
1665 match nobody:
1666 case True{}:
1667 Bytes.from_string(response(status, headers, ""))
1668 case False{}:
1669 encode.len(status, headers, head, body)
1670
1671def encode.on(r: Res, head: Bool) -> Bytes.Bytes:
1672 Res{+status, headers, body} = r
1673 encode.pick(status, headers, body, head, frame.nobody(status, False{}))
1674
1675def encode(r: Res) -> Bytes.Bytes:
1676 encode.on(r, False{})
1677
1678def request(method: String, path: String, headers: Map<&2, List<&2, String>>, body: String) -> String:
1679 (method ++ " " ++ path ++ " HTTP/1.1" ++ headers_block(headers)) ++ ("\r\n\r\n" ++ body)
1680
1681def req.reserved(+k: String) -> Bool:
1682 Bool.or(Bool.or(String.eq(k, "host"), String.eq(k, "connection")), Bool.or(String.eq(k, "content-length"), String.eq(k, "transfer-encoding")))
1683
1684def req.put.one(m: Map<&2, List<&2, String>>, +k: String, vs: List<&2, String>, skip: Bool) -> Map<&2, List<&2, String>>:
1685 match skip:
1686 case True{}:
1687 m
1688 case False{}:
1689 Map.set(&2, List<&2, String>, m, k, vs)
1690
1691def req.put(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>, m: Map<&2, List<&2, String>>) -> Map<&2, List<&2, String>>:
1692 match xs:
1693 case Nil{}:
1694 m
1695 case (k, vs) <> t:
1696 +lk = String.to_lower(k)
1697 req.put(t, req.put.one(m, lk, vs, req.reserved(lk)))
1698
1699# RFC 9110 §8.6: no Content-Length on a bodiless request whose method gives a body no meaning.
1700def req.cl(+m: Map<&2, List<&2, String>>, +method: String, +len: U32) -> Map<&2, List<&2, String>>:
1701 +bodied = Bool.or(Bool.not(U32.is_zero(len)), Bool.or(String.eq(method, "POST"), Bool.or(String.eq(method, "PUT"), String.eq(method, "PATCH"))))
1702 Bool.pick(Map<&2, List<&2, String>>, bodied, set(m, "content-length", U32.show(len)), m)
1703
1704# Caller headers are lowercased so they cannot duplicate ours; host, connection,
1705# content-length and transfer-encoding are always ours (no smuggling through them).
1706def encode_req.word(close: Bool) -> String:
1707 match close:
1708 case True{}:
1709 "close"
1710 case False{}:
1711 "keep-alive"
1712
1713def encode_req.on(+method: String, target: String, host: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, close: Bool) -> Bytes.Bytes:
1714 Bytes.Bytes{+len, buf} = body
1715 +h = set(set(req.put(Map.to_list(&2, List<&2, String>, headers), empty()), "host", host), "connection", encode_req.word(close))
1716 Bytes.append(Bytes.from_string(request(method, target, req.cl(h, method, len), "")), Bytes.Bytes{len, buf})
1717
1718def encode_req(+method: String, target: String, host: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> Bytes.Bytes:
1719 encode_req.on(method, target, host, headers, body, True{})
1720
1721# Redirects (RFC 9110 §15.4, as WHATWG fetch applies them)
1722# --------------------------------------------------------
1723
1724# One request to make: headers are already lowercased (see req.put).
1725type Hop is Type:
1726 Hop{method: String, url: Url.Abs, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
1727
1728def redirect.code(+s: U32) -> Bool:
1729 Bool.or(Bool.or(U32.is_eq(s, 301), U32.is_eq(s, 302)), Bool.or(U32.is_eq(s, 303), Bool.or(U32.is_eq(s, 307), U32.is_eq(s, 308))))
1730
1731def redirect.origin(a: Url.Abs) -> String:
1732 Url.Abs{scheme, host, port, target} = a
1733 scheme ++ "://" ++ host ++ ":" ++ U32.show(port)
1734
1735def redirect.del(ks: List<&2, String>, m: Map<&2, List<&2, String>>) -> Map<&2, List<&2, String>>:
1736 match ks:
1737 case Nil{}:
1738 m
1739 case Con{k, t}:
1740 redirect.del(t, Map.del(&2, List<&2, String>, m, k))
1741
1742def redirect.hdrs(+h: Map<&2, List<&2, String>>, drop: Bool, cross: Bool) -> Map<&2, List<&2, String>>:
1743 +h2 = Bool.pick(Map<&2, List<&2, String>>, drop, redirect.del(["content-type", "content-encoding", "content-language", "content-location"], h), h)
1744 Bool.pick(Map<&2, List<&2, String>>, cross, redirect.del(["authorization", "cookie", "proxy-authorization"], h2), h2)
1745
1746# 303 turns any method but HEAD into GET; 301 and 302 turn POST into GET;
1747# 307 and 308 keep method and body. A GET carries no body or body headers.
1748# Credentials do not follow a hop to another origin.
1749def redirect.body(drop: Bool, body: Bytes.Bytes) -> Bytes.Bytes:
1750 match drop:
1751 case True{}:
1752 Bytes.new(0)
1753 case False{}:
1754 body
1755
1756def redirect.to(+status: U32, +method: String, +from: Url.Abs, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, next: Maybe<&2, Url.Abs>) -> Maybe<&1, Hop>:
1757 match next:
1758 case None{}:
1759 None{}
1760 case Some{+to}:
1761 +drop = Bool.or(Bool.and(U32.is_eq(status, 303), Bool.not(String.eq(method, "HEAD"))), Bool.and(Bool.or(U32.is_eq(status, 301), U32.is_eq(status, 302)), String.eq(method, "POST")))
1762 Some{Hop{Bool.pick(String, drop, "GET", method), to, redirect.hdrs(headers, drop, Bool.not(String.eq(redirect.origin(from), redirect.origin(to)))), redirect.body(drop, body)}}
1763
1764def redirect.hop(status: U32, h: Hop, loc: String) -> Maybe<&1, Hop>:
1765 Hop{method, +url, headers, body} = h
1766 redirect.to(status, method, url, headers, body, Url.resolve(url, loc))
1767
1768def redirect.if(status: U32, h: Hop, loc: String, ok: Bool) -> Maybe<&1, Hop>:
1769 match ok:
1770 case False{}:
1771 None{}
1772 case True{}:
1773 redirect.hop(status, h, loc)
1774
1775# The next request after a response, or None when it is not a redirect we follow.
1776def redirect(+status: U32, +headers: Map<&2, List<&2, String>>, h: Hop) -> Maybe<&1, Hop>:
1777 redirect.if(status, h, header(headers, "location"), Bool.and(redirect.code(status), has_header(headers, "location")))
1778
1779def io.recv.words(tls: Bool, s: Socket, max: U32, ms: U32) -> IO(Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>):
1780 match tls:
1781 case True{}:
1782 Wire.tls.recv.words(s, max, ms)
1783 case False{}:
1784 Wire.recv.words(s, max, ms)
1785
1786def io.send(tls: Bool, s: Socket, data: String) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
1787 match tls:
1788 case True{}:
1789 Wire.tls.send(s, data)
1790 case False{}:
1791 Wire.send(s, data)
1792
1793def io.send.words(tls: Bool, s: Socket, +len: U32, buf: Array<U32>) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
1794 match tls:
1795 case True{}:
1796 Wire.tls.send.words(s, len, buf)
1797 case False{}:
1798 Wire.send.words(s, len, buf)
1799
1800def io.send.bytes(tls: Bool, s: Socket, b: Bytes.Bytes) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
1801 Bytes.Bytes{+len, buf} = b
1802 io.send.words(tls, s, len, buf)
1803
1804def io.close(tls: Bool, s: Socket) -> IO(Unit):
1805 match tls:
1806 case True{}:
1807 Wire.tls.close(s)
1808 case False{}:
1809 Socket.close(s)
1810
1811def fetch.close(tls: Bool, s: Socket, r: Result<&1, &1, Err, Res>) -> IO(Result<&1, &1, Err, Res>):
1812 do IO<Result<&1, &1, Err, Res>>:
1813 io.close(tls, s)
1814 return r
1815
1816# none: no response byte arrived, so an idempotent request may be retried (RFC 9112 §9.3.1).
1817# sock: the socket, when it can take another request.
1818type Out is Type:
1819 OutDone{res: Res, sock: Maybe<&1, Socket>, rest: Bytes.Bytes}
1820 OutFail{e: Err, none: Bool}
1821
1822def fetch.boxed(r: Result<&1, &1, Err, Res>, none: Bool) -> Out:
1823 match r:
1824 case Done{res}:
1825 OutDone{res, None{}, Bytes.new(0)}
1826 case Fail{e}:
1827 OutFail{e, none}
1828
1829def fetch.bad(tls: Bool, s: Socket, e: Maybe<&2, Err>) -> IO(Result<&1, &1, Err, Res>):
1830 match e:
1831 case None{}:
1832 fetch.close(tls, s, Fail{ErrBad{}})
1833 case Some{err}:
1834 fetch.close(tls, s, Fail{err})
1835
1836def fetch.shut(tls: Bool, s: Socket, r: Result<&1, &1, Err, Res>, none: Bool) -> IO(Out):
1837 do IO<Out>:
1838 x : Result<&1, &1, Err, Res> <- fetch.close(tls, s, r)
1839 return fetch.boxed(x, none)
1840
1841def fetch.hold.go(tls: Bool, s: Socket, res: Res, left: Maybe<&1, Bytes.Bytes>) -> IO(Out):
1842 match left:
1843 case Some{x}:
1844 IO.pure(Out, OutDone{res, Some{s}, x})
1845 case None{}:
1846 fetch.shut(tls, s, Done{res}, False{})
1847
1848def fetch.hold(tls: Bool, close: Bool, s: Socket, res: Res, left: Maybe<&1, Bytes.Bytes>) -> IO(Out):
1849 Res{status, +headers, body} = res
1850 fetch.hold.go(tls, s, Res{status, headers, body}, again(close, headers, left))
1851
1852def fetch.failout(tls: Bool, s: Socket, e: Maybe<&2, Err>, none: Bool) -> IO(Out):
1853 do IO<Out>:
1854 r : Result<&1, &1, Err, Res> <- fetch.bad(tls, s, e)
1855 return fetch.boxed(r, none)
1856
1857# Read state: the response so far and the bytes read, or how it ended.
1858# none: no byte arrived, so an idempotent request may be retried.
1859type Fl is Type:
1860 FlMore{rv: Rv, n: U32}
1861 FlBad{err: Maybe<&2, Err>, none: Bool}
1862 FlDone{res: Res, rest: Maybe<&1, Bytes.Bytes>}
1863
1864def fetch.rt(+n: U32, t: Rt) -> Fl:
1865 match t:
1866 case RtMore{rv}:
1867 FlMore{rv, n}
1868 case RtBad{}:
1869 FlBad{None{}, U32.is_zero(n)}
1870 case RtDone{res, rest}:
1871 FlDone{res, rest}
1872
1873# 64 KiB of head past the body cap, as serve allows.
1874def fetch.over(+n: U32) -> Bool:
1875 Nat.is_lt(Nat.add(fetch.max(), 65536n), U32.to_nat(n))
1876
1877def fetch.piece.cap(over: Bool, +head: Bool, rv: Rv, +n2: U32, +len: U32, buf: Array<U32>) -> Fl:
1878 match over:
1879 case True{}:
1880 FlBad{None{}, False{}}
1881 case False{}:
1882 fetch.rt(n2, rv.step(U32.is_zero(len), head, rv, Bytes.Bytes{len, buf}))
1883
1884def fetch.piece(+head: Bool, rv: Rv, +n: U32, p: U32 & Array<U32>) -> Fl:
1885 (+len, buf) = p
1886 +n2 = (n + len : U32)
1887 fetch.piece.cap(fetch.over(n2), head, rv, n2, len, buf)
1888
1889def fetch.next(+head: Bool, rv: Rv, +n: U32, m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Socket & Fl:
1890 (s, r) = m
1891 match r:
1892 case Fail{(+code, why)}:
1893 (s, FlBad{Some{err.or_late(code, ErrRead{code, why})}, U32.is_zero(n)})
1894 case Done{p}:
1895 (s, fetch.piece(head, rv, n, p))
1896
1897# Reads until the response is whole or cannot be; an empty read means the server closed.
1898@unsafe
1899def fetch.loop(+close: Bool, +head: Bool, +tls: Bool, +ms: U32, st: Socket & Fl) -> IO(Out):
1900 (s, fl) = st
1901 match fl:
1902 case FlMore{rv, +n}:
1903 do IO<Out>:
1904 m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv.words(tls, s, 65536, ms)
1905 fetch.loop(close, head, tls, ms, fetch.next(head, rv, n, m))
1906 case FlBad{err, none}:
1907 fetch.failout(tls, s, err, none)
1908 case FlDone{res, rest}:
1909 fetch.hold(tls, close, s, res, rest)
1910
1911def exchange.sent(+tls: Bool, +ms: U32, +close: Bool, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Out):
1912 (s, r) = m
1913 match r:
1914 case Fail{(+code, why)}:
1915 fetch.shut(tls, s, Fail{err.or_late(code, ErrWrite{code, why})}, True{})
1916 case Done{u}:
1917 fetch.loop(close, head, tls, ms, (s, FlMore{rv.start(), 0}))
1918
1919def exchange.go(+tls: Bool, +ms: U32, +close: Bool, +head: Bool, s: Socket, wire: Bytes.Bytes) -> IO(Out):
1920 do IO<Out>:
1921 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(tls, s, wire)
1922 exchange.sent(tls, ms, close, head, sent)
1923
1924def exchange.tup(o: Out) -> Maybe<&1, Socket> & Result<&1, &1, Err, Res> & Bytes.Bytes:
1925 match o:
1926 case OutFail{e, none}:
1927 (None{}, Fail{e}, Bytes.new(0))
1928 case OutDone{res, sock, rest}:
1929 (sock, Done{res}, rest)
1930
1931# One request on an open socket. Some{socket}: it can take another request.
1932def exchange(+tls: Bool, +ms: U32, +close: Bool, +head: Bool, s: Socket, wire: Bytes.Bytes) -> IO(Maybe<&1, Socket> & Result<&1, &1, Err, Res> & Bytes.Bytes):
1933 do IO<Maybe<&1, Socket> & Result<&1, &1, Err, Res> & Bytes.Bytes>:
1934 o : Out <- exchange.go(tls, ms, close, head, s, wire)
1935 return exchange.tup(o)
1936
1937# Paths to a PEM client chain and its private key for mutual TLS.
1938type Cert is Data:
1939 Cert{chain: String, key: String}
1940
1941# Connection pool: idle sockets by origin and client identity, newest first, at most cap per key.
1942# fetch uses a fresh pool per call.
1943
1944type Conn is Type:
1945 Conn{tls: Bool, s: Socket}
1946
1947type Pool is Type:
1948 Pool{cap: U32, idle: Map<&1, List<&1, Conn>>}
1949
1950def pool.new.with(+cap: U32) -> Pool:
1951 Pool{cap, Map.new(&1, List<&1, Conn>)}
1952
1953# Up to 8 idle sockets per origin.
1954def pool.new() -> Pool:
1955 pool.new.with(8)
1956
1957def pool.key(+scheme: String, +host: String, +port: U32) -> String:
1958 scheme ++ "://" ++ host ++ ":" ++ U32.show(port)
1959
1960def pool.key.cert(+base: String, cert: Maybe<&2, Cert>) -> String:
1961 match cert:
1962 case None{}:
1963 base
1964 case Some{Cert{+chain, +key}}:
1965 base ++ "|cert:" ++ Nat.show(String.length(chain)) ++ ":" ++ chain
1966 ++ Nat.show(String.length(key)) ++ ":" ++ key
1967
1968def pool.take.of(+cap: U32, +key: String, r: Map<&1, List<&1, Conn>> & Maybe<&1, List<&1, Conn>>) -> Pool & Maybe<&1, Conn>:
1969 (m, got) = r
1970 match got:
1971 case None{}:
1972 (Pool{cap, m}, None{})
1973 case Some{xs}:
1974 match xs:
1975 case Nil{}:
1976 (Pool{cap, m}, None{})
1977 case Con{c, t}:
1978 (Pool{cap, Map.set(&1, List<&1, Conn>, m, key, t)}, Some{c})
1979
1980# The socket given back last.
1981def pool.take(p: Pool, +key: String) -> Pool & Maybe<&1, Conn>:
1982 Pool{+cap, idle} = p
1983 pool.take.of(cap, key, Map.pop(&1, List<&1, Conn>, idle, key))
1984
1985def conn.close(c: Conn) -> IO(Unit):
1986 Conn{tls, s} = c
1987 io.close(tls, s)
1988
1989# The first n sockets; the rest are closed.
1990def conns.cut(xs: List<&1, Conn>, n: Nat) -> IO(List<&1, Conn>):
1991 match xs:
1992 case Nil{}:
1993 IO.pure(List<&1, Conn>, Nil{})
1994 case Con{c, t}:
1995 match n:
1996 case 0n:
1997 do IO<List<&1, Conn>>:
1998 conn.close(c)
1999 conns.cut(t, 0n)
2000 case 1n+k:
2001 do IO<List<&1, Conn>>:
2002 r : List<&1, Conn> <- conns.cut(t, k)
2003 return c <> r
2004
2005def pool.give.of(+cap: U32, +key: String, c: Conn, r: Map<&1, List<&1, Conn>> & Maybe<&1, List<&1, Conn>>) -> IO(Pool):
2006 (m, old) = r
2007 do IO<Pool>:
2008 xs : List<&1, Conn> <- conns.cut(c <> Maybe.default(&1, List<&1, Conn>, old, Nil{}), U32.to_nat(cap))
2009 return Pool{cap, Map.set(&1, List<&1, Conn>, m, key, xs)}
2010
2011# Past cap, the oldest idle socket of the origin is closed.
2012def pool.give(p: Pool, +key: String, c: Conn) -> IO(Pool):
2013 Pool{+cap, idle} = p
2014 pool.give.of(cap, key, c, Map.pop(&1, List<&1, Conn>, idle, key))
2015
2016def pool.close.go(xs: List<&1, List<&1, Conn>>) -> IO(Unit):
2017 match xs:
2018 case Nil{}:
2019 IO.pure(Unit, Unit{})
2020 case Con{cs, t}:
2021 do IO<Unit>:
2022 none : List<&1, Conn> <- conns.cut(cs, 0n)
2023 pool.close.go(t)
2024
2025def pool.close(p: Pool) -> IO(Unit):
2026 Pool{cap, idle} = p
2027 pool.close.go(Map.values(&1, List<&1, Conn>, idle))
2028
2029# RFC 9110 §9.2.2
2030def pool.idempotent(+method: String) -> Bool:
2031 Bool.or(String.eq(method, "GET"), Bool.or(String.eq(method, "HEAD"), Bool.or(String.eq(method, "OPTIONS"), Bool.or(String.eq(method, "TRACE"), Bool.or(String.eq(method, "PUT"), String.eq(method, "DELETE"))))))
2032
2033def conn.tls(m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Result<&1, &1, Err, Conn>):
2034 (s, r) = m
2035 match r:
2036 case Fail{(+code, why)}:
2037 do IO<Result<&1, &1, Err, Conn>>:
2038 Wire.tls.close(s)
2039 return Fail{err.or_late(code, ErrTls{code, why})}
2040 case Done{u}:
2041 IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{True{}, s}})
2042
2043def conn.handshake(cert: Maybe<&2, Cert>, s: Socket, host: String, +ms: U32) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
2044 match cert:
2045 case None{}:
2046 Wire.tls.connect(s, host, ms)
2047 case Some{Cert{chain, key}}:
2048 Wire.tls.connect.cert(s, host, ms, chain, key)
2049
2050# A failed handshake is an error, never plaintext.
2051def conn.secure(+ms: U32, sni: String, s: Socket, tls: Bool, cert: Maybe<&2, Cert>) -> IO(Result<&1, &1, Err, Conn>):
2052 match tls:
2053 case False{}:
2054 IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{False{}, s}})
2055 case True{}:
2056 do IO<Result<&1, &1, Err, Conn>>:
2057 hs : Socket & Result<&1, &1, U32 & String, Unit> <- conn.handshake(cert, s, sni, ms)
2058 conn.tls(hs)
2059
2060def conn.made(+ms: U32, sni: String, tls: Bool, cert: Maybe<&2, Cert>, r: Result<&1, &1, U32 & String, Socket>) -> IO(Result<&1, &1, Err, Conn>):
2061 match r:
2062 case Fail{(+code, why)}:
2063 IO.pure(Result<&1, &1, Err, Conn>, Fail{err.or_late(code, ErrConnect{code, why})})
2064 case Done{s}:
2065 conn.secure(ms, sni, s, tls, cert)
2066
2067def conn.open(+tls: Bool, +ms: U32, sni: String, ip: String, port: U32) -> IO(Result<&1, &1, Err, Conn>):
2068 do IO<Result<&1, &1, Err, Conn>>:
2069 c : Result<&1, &1, U32 & String, Socket> <- Wire.connect(ip, port, ms)
2070 conn.made(ms, sni, tls, None{}, c)
2071
2072# ponytail: addresses are tried in order, not raced; a broken first route can consume the step timeout.
2073type Dial is Type:
2074 Dial{port: U32, ms: U32, deadline: Nat, action: IO(Result<&1, &1, U32 & String, Socket>)}
2075
2076def conn.dial.time(+ip: String, +port: U32, +deadline: Nat, now: Nat, expired: Bool) ->
2077 IO(Result<&1, &1, U32 & String, Socket>):
2078 match expired:
2079 case True{}:
2080 IO.pure(Result<&1, &1, U32 & String, Socket>, Fail{(60, "connect timeout")})
2081 case False{}:
2082 Wire.connect(ip, port, U32.from_nat(Nat.sub(deadline, now)))
2083
2084def conn.dial.with(+ip: String, +port: U32, +ms: U32, +deadline: Nat, +now: Nat, unlimited: Bool) ->
2085 IO(Result<&1, &1, U32 & String, Socket>):
2086 match unlimited:
2087 case True{}:
2088 Wire.connect(ip, port, 0)
2089 case False{}:
2090 conn.dial.time(ip, port, deadline, now, Nat.is_le(deadline, now))
2091
2092def conn.dial.try(+ip: String, +port: U32, +ms: U32, +deadline: Nat) ->
2093 IO(Result<&1, &1, U32 & String, Socket>):
2094 do IO<Result<&1, &1, U32 & String, Socket>>:
2095 now : Nat <- IO.now()
2096 conn.dial.with(ip, port, ms, deadline, now, U32.is_zero(ms))
2097
2098def conn.dial.after(r: Result<&1, &1, U32 & String, Socket>, ip: String, +port: U32, +ms: U32, +deadline: Nat) ->
2099 IO(Result<&1, &1, U32 & String, Socket>):
2100 match r:
2101 case Done{s}:
2102 IO.pure(Result<&1, &1, U32 & String, Socket>, Done{s})
2103 case Fail{e}:
2104 conn.dial.try(ip, port, ms, deadline)
2105
2106def conn.dial.more(prev: IO(Result<&1, &1, U32 & String, Socket>), ip: String, +port: U32, +ms: U32, +deadline: Nat) ->
2107 IO(Result<&1, &1, U32 & String, Socket>):
2108 do IO<Result<&1, &1, U32 & String, Socket>>:
2109 r : Result<&1, &1, U32 & String, Socket> <- prev
2110 conn.dial.after(r, ip, port, ms, deadline)
2111
2112def conn.dial.fold(d: Dial, ip: String) -> Dial:
2113 Dial{+port, +ms, +deadline, action} = d
2114 Dial{port, ms, deadline, conn.dial.more(action, ip, port, ms, deadline)}
2115
2116def conn.dial.run(d: Dial) -> IO(Result<&1, &1, U32 & String, Socket>):
2117 Dial{port, ms, deadline, action} = d
2118 action
2119
2120def conn.dial.all(+port: U32, +ms: U32, +start: Nat, first: String, rest: List<&2, String>) ->
2121 IO(Result<&1, &1, U32 & String, Socket>):
2122 match rest:
2123 case Nil{}:
2124 Wire.connect(first, port, ms)
2125 case Con{ip, tail}:
2126 +deadline = Nat.add(start, U32.to_nat(ms))
2127 conn.dial.run(List.foldl(~&2, ~String, ~Dial, ~conn.dial.fold, Con{ip, tail},
2128 Dial{port, ms, deadline, Wire.connect(first, port, ms)}))
2129
2130def conn.open.all(+tls: Bool, +ms: U32, +host: String, +port: U32, ips: List<&2, String>, cert: Maybe<&2, Cert>) -> IO(Result<&1, &1, Err, Conn>):
2131 match ips:
2132 case Nil{}:
2133 IO.pure(Result<&1, &1, Err, Conn>, Fail{ErrDns{}})
2134 case Con{addr, rest}:
2135 do IO<Result<&1, &1, Err, Conn>>:
2136 start : Nat <- IO.now()
2137 r : Result<&1, &1, U32 & String, Socket> <- conn.dial.all(port, ms, start, addr, rest)
2138 conn.made(ms, host, tls, cert, r)
2139
2140def conn.ex(c: Conn, +ms: U32, +head: Bool, wire: Bytes.Bytes) -> IO(Out):
2141 Conn{+tls, s} = c
2142 exchange.go(tls, ms, False{}, head, s, wire)
2143
2144# A socket with bytes past the response is out of step with the server, so it is closed.
2145def pool.keep.s(p: Pool, +key: String, +tls: Bool, res: Res, s: Socket, clean: Bool) -> IO(Pool & Result<&1, &1, Err, Res>):
2146 match clean:
2147 case True{}:
2148 do IO<Pool & Result<&1, &1, Err, Res>>:
2149 p2 : Pool <- pool.give(p, key, Conn{tls, s})
2150 return (p2, Done{res})
2151 case False{}:
2152 do IO<Pool & Result<&1, &1, Err, Res>>:
2153 io.close(tls, s)
2154 return (p, Done{res})
2155
2156def pool.keep.m(p: Pool, +key: String, +tls: Bool, res: Res, +clean: Bool, sock: Maybe<&1, Socket>) -> IO(Pool & Result<&1, &1, Err, Res>):
2157 match sock:
2158 case None{}:
2159 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Done{res}))
2160 case Some{s}:
2161 pool.keep.s(p, key, tls, res, s, clean)
2162
2163def pool.keep(p: Pool, +key: String, +tls: Bool, res: Res, sock: Maybe<&1, Socket>, rest: Bytes.Bytes) -> IO(Pool & Result<&1, &1, Err, Res>):
2164 Bytes.Bytes{+len, buf} = rest
2165 pool.keep.m(p, key, tls, res, U32.is_zero(len), sock)
2166
2167def pool.after(p: Pool, +key: String, +tls: Bool, o: Out) -> IO(Pool & Result<&1, &1, Err, Res>):
2168 match o:
2169 case OutFail{e, none}:
2170 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
2171 case OutDone{res, sock, rest}:
2172 pool.keep(p, key, tls, res, sock, rest)
2173
2174def pool.fresh.conn(p: Pool, +key: String, +tls: Bool, +ms: U32, +head: Bool, wire: Bytes.Bytes, r: Result<&1, &1, Err, Conn>) -> IO(Pool & Result<&1, &1, Err, Res>):
2175 match r:
2176 case Fail{e}:
2177 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
2178 case Done{c}:
2179 do IO<Pool & Result<&1, &1, Err, Res>>:
2180 o : Out <- conn.ex(c, ms, head, wire)
2181 pool.after(p, key, tls, o)
2182
2183def pool.fresh(p: Pool, +key: String, +tls: Bool, +ms: U32, +head: Bool, +host: String, +port: U32, wire: Bytes.Bytes, cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res>):
2184 do IO<Pool & Result<&1, &1, Err, Res>>:
2185 ips : List<&2, String> <- Dns.resolve.all(host)
2186 c : Result<&1, &1, Err, Conn> <- conn.open.all(tls, ms, host, port, ips, cert)
2187 pool.fresh.conn(p, key, tls, ms, head, wire, c)
2188
2189# A reused socket the server already closed fails before any response byte.
2190def pool.retry(+none: Bool, +idem: Bool) -> Bool:
2191 Bool.and(none, idem)
2192
2193def pool.stale(p: Pool, +key: String, +tls: Bool, +ms: U32, +head: Bool, +host: String, +port: U32, wire: Bytes.Bytes, e: Err, again: Bool, cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res>):
2194 match again:
2195 case True{}:
2196 pool.fresh(p, key, tls, ms, head, host, port, wire, cert)
2197 case False{}:
2198 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
2199
2200def pool.reused(p: Pool, +key: String, +tls: Bool, +ms: U32, +head: Bool, +idem: Bool, +host: String, +port: U32, wire: Bytes.Bytes, o: Out, cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res>):
2201 match o:
2202 case OutFail{e, +none}:
2203 pool.stale(p, key, tls, ms, head, host, port, wire, e, pool.retry(none, idem), cert)
2204 case OutDone{res, sock, rest}:
2205 pool.keep(p, key, tls, res, sock, rest)
2206
2207# A spare copy of the request, for the retry after a stale socket.
2208def pool.idle.reuse(p: Pool, +key: String, +tls: Bool, +ms: U32, +head: Bool, +idem: Bool, +host: String, +port: U32, c: Conn, r: Bytes.Bytes & Bytes.Bytes, cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res>):
2209 (wire, spare) = r
2210 do IO<Pool & Result<&1, &1, Err, Res>>:
2211 o : Out <- conn.ex(c, ms, head, wire)
2212 pool.reused(p, key, tls, ms, head, idem, host, port, spare, o, cert)
2213
2214def pool.idle(taken: Pool & Maybe<&1, Conn>, +key: String, +tls: Bool, +ms: U32, +head: Bool, +idem: Bool, +host: String, +port: U32, wire: Bytes.Bytes, cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res>):
2215 (p, m) = taken
2216 match m:
2217 case None{}:
2218 pool.fresh(p, key, tls, ms, head, host, port, wire, cert)
2219 case Some{c}:
2220 pool.idle.reuse(p, key, tls, ms, head, idem, host, port, c, Bytes.slice(wire, 0, 4294967295), cert)
2221
2222def pool.origin(p: Pool, +method: String, +ms: U32, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, +hf: String, a: Url.Abs, known: Bool, +cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res>):
2223 Url.Abs{+scheme, +host, +port, target} = a
2224 match known:
2225 case False{}:
2226 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{ErrUrl{}}))
2227 case True{}:
2228 +key = pool.key.cert(pool.key(scheme, host, port), cert)
2229 pool.idle(pool.take(p, key), key, String.eq(scheme, "https"), ms, String.eq(method, "HEAD"), pool.idempotent(method), host, port, encode_req.on(method, target, hf, headers, body, False{}), cert)
2230
2231def pool.scheme.ok(a: Url.Abs) -> Bool:
2232 Url.Abs{+scheme, host, port, target} = a
2233 Bool.or(String.eq(scheme, "http"), String.eq(scheme, "https"))
2234
2235def pool.one.back(h: Hop, pr: Pool & Result<&1, &1, Err, Res>) -> Pool & Result<&1, &1, Err, Res> & Hop:
2236 (p, r) = pr
2237 (p, r, h)
2238
2239def pool.one.of(p: Pool, +method: String, +url: Url.Abs, +headers: Map<&2, List<&2, String>>, +ms: U32, r: Bytes.Bytes & Bytes.Bytes, cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res> & Hop):
2240 (body, wire) = r
2241 do IO<Pool & Result<&1, &1, Err, Res> & Hop>:
2242 pr : Pool & Result<&1, &1, Err, Res> <- pool.origin(p, method, ms, headers, wire, Url.host_field(url), url, pool.scheme.ok(url), cert)
2243 return pool.one.back(Hop{method, url, headers, body}, pr)
2244
2245# One request, on an idle socket to its origin when the pool has one. The hop comes back for the redirect.
2246def pool.one(p: Pool, h: Hop, +ms: U32, cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res> & Hop):
2247 Hop{+method, +url, +headers, body} = h
2248 pool.one.of(p, method, url, headers, ms, Bytes.slice(body, 0, 4294967295), cert)
2249
2250type Next is Type:
2251 NDone{res: Result<&1, &1, Err, Res>}
2252 NStop{}
2253 NGo{left: Nat, hop: Hop}
2254
2255type Mode is Data:
2256 ModeFollow{}
2257 ModeManual{}
2258 ModeError{}
2259
2260# left: redirects still allowed after the request we just finished.
2261def fetch.hop(left: Nat, h: Hop) -> Next:
2262 match left:
2263 case 0n:
2264 NStop{}
2265 case 1n+p:
2266 NGo{p, h}
2267
2268def fetch.decide.r(left: Nat, r: Res, next: Maybe<&1, Hop>) -> Next:
2269 match next:
2270 case None{}:
2271 NDone{Done{r}}
2272 case Some{h}:
2273 fetch.hop(left, h)
2274
2275def fetch.decide.res(left: Nat, h: Hop, r: Res) -> Next:
2276 Res{+status, +headers, body} = r
2277 fetch.decide.r(left, Res{status, headers, body}, redirect(status, headers, h))
2278
2279def fetch.decide(left: Nat, h: Hop, m: Result<&1, &1, Err, Res>) -> Next:
2280 match m:
2281 case Fail{e}:
2282 NDone{Fail{e}}
2283 case Done{r}:
2284 fetch.decide.res(left, h, r)
2285
2286def fetch.error.res(r: Res, bad: Bool) -> Next:
2287 match bad:
2288 case True{}:
2289 NDone{Fail{ErrRedirect{}}}
2290 case False{}:
2291 NDone{Done{r}}
2292
2293def fetch.error(h: Hop, m: Result<&1, &1, Err, Res>) -> Next:
2294 match m:
2295 case Fail{e}:
2296 NDone{Fail{e}}
2297 case Done{r}:
2298 Res{+status, +headers, body} = r
2299 fetch.error.res(Res{status, headers, body}, Bool.and(redirect.code(status), has_header(headers, "location")))
2300
2301def fetch.policy(mode: Mode, left: Nat, h: Hop, m: Result<&1, &1, Err, Res>) -> Next:
2302 match mode:
2303 case ModeFollow{}:
2304 fetch.decide(left, h, m)
2305 case ModeManual{}:
2306 NDone{m}
2307 case ModeError{}:
2308 fetch.error(h, m)
2309
2310# A caller's own Accept-Encoding wins; enc is the codings fetch can undo.
2311def accept.enc(+h: Map<&2, List<&2, String>>, +enc: String) -> Map<&2, List<&2, String>>:
2312 Bool.pick(Map<&2, List<&2, String>>, has_header(h, "accept-encoding"), h, set(h, "accept-encoding", enc))
2313
2314def fetch.start(method: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, u: Maybe<&2, Url.Abs>, +enc: String) -> Next:
2315 match u:
2316 case None{}:
2317 NDone{Fail{ErrUrl{}}}
2318 case Some{a}:
2319 NGo{20n, Hop{method, a, accept.enc(req.put(Map.to_list(&2, List<&2, String>, headers), empty()), enc), body}}
2320
2321def pool.next.move(p: Pool, +old: String, cert: Maybe<&2, Cert>, n: Next) -> Pool & Next & Maybe<&2, Cert>:
2322 match n:
2323 case NGo{left, h}:
2324 Hop{method, +url, headers, body} = h
2325 (p, NGo{left, Hop{method, url, headers, body}},
2326 Bool.pick(Maybe<&2, Cert>, String.eq(old, redirect.origin(url)), cert, None{}))
2327 case NDone{r}:
2328 (p, NDone{r}, None{})
2329 case NStop{}:
2330 (p, NStop{}, None{})
2331
2332def pool.next(+mode: Mode, left: Nat, cert: Maybe<&2, Cert>, x: Pool & Result<&1, &1, Err, Res> & Hop) -> Pool & Next & Maybe<&2, Cert>:
2333 (p, m, h) = x
2334 Hop{method, +url, headers, body} = h
2335 pool.next.move(p, redirect.origin(url), cert, fetch.policy(mode, left, Hop{method, url, headers, body}, m))
2336
2337def pool.hops.one(+mode: Mode, +ms: U32, +cert: Maybe<&2, Cert>, p: Pool, h: Hop, left: Nat) -> IO(Pool & Next & Maybe<&2, Cert>):
2338 do IO<Pool & Next & Maybe<&2, Cert>>:
2339 x : Pool & Result<&1, &1, Err, Res> & Hop <- pool.one(p, h, ms, cert)
2340 return pool.next(mode, left, cert, x)
2341
2342# NGo.left is how many redirects may follow this request. 20 is WHATWG's limit.
2343@unsafe
2344def pool.hops(+mode: Mode, +ms: U32, st: Pool & Next & Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res>):
2345 (p, n, cert) = st
2346 match n:
2347 case NDone{m}:
2348 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, m))
2349 case NStop{}:
2350 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{ErrRedirect{}}))
2351 case NGo{+left, h}:
2352 do IO<Pool & Result<&1, &1, Err, Res>>:
2353 next : Pool & Next & Maybe<&2, Cert> <- pool.hops.one(mode, ms, cert, p, h, left)
2354 pool.hops(mode, ms, next)
2355
2356# Content-Encoding (RFC 9110 §8.4): each value, trimmed and lowercased, in the order applied.
2357def ce.keep(+w: String, +rest: List<&2, String>) -> List<&2, String>:
2358 Bool.pick(List<&2, String>, String.is_empty(w), rest, Con{w, rest})
2359
2360def ce.norm(xs: List<&2, String>) -> List<&2, String>:
2361 match xs:
2362 case Nil{}:
2363 Nil{}
2364 case Con{v, t}:
2365 ce.keep(String.to_lower(trim(v)), ce.norm(t))
2366
2367def ce.split(xs: List<&2, String>) -> List<&2, String>:
2368 match xs:
2369 case Nil{}:
2370 Nil{}
2371 case Con{v, t}:
2372 List.append(&2, String, ce.norm(String.split(v, ',')), ce.split(t))
2373
2374# Ok: decoded so far. Bad: a coding failed. Skip: a coding we cannot decode, so the body stays as sent.
2375type Dec is Data:
2376 DecOk{b: String}
2377 DecBad{}
2378 DecSkip{}
2379
2380def ce.of(m: Maybe<&2, String>) -> Dec:
2381 match m:
2382 case None{}:
2383 DecBad{}
2384 case Some{b}:
2385 DecOk{b}
2386
2387# Servers send deflate both with and without the zlib wrapper.
2388def ce.deflate(+b: String, m: Maybe<&2, String>) -> Dec:
2389 match m:
2390 case Some{out}:
2391 DecOk{out}
2392 case None{}:
2393 ce.of(Zlib.inflate(b))
2394
2395def ce.apply(+c: String, +b: String) -> Dec:
2396 Bool.pick(Dec, Bool.or(String.eq(c, "gzip"), String.eq(c, "x-gzip")), ce.of(Zlib.gunzip(b)),
2397 Bool.pick(Dec, String.eq(c, "deflate"), ce.deflate(b, Zlib.unzlib(b)),
2398 Bool.pick(Dec, String.eq(c, "identity"), DecOk{b}, DecSkip{})))
2399
2400def ce.go(cs: List<&2, String>, d: Dec) -> Dec:
2401 match cs:
2402 case Nil{}:
2403 d
2404 case Con{+c, t}:
2405 match d:
2406 case DecOk{+b}:
2407 ce.go(t, ce.apply(c, b))
2408 case DecBad{}:
2409 DecBad{}
2410 case DecSkip{}:
2411 DecSkip{}
2412
2413def decoded.pick(d: Dec, +status: U32, headers: Map<&2, List<&2, String>>, body: String) -> Result<&1, &1, Err, Res>:
2414 match d:
2415 case DecOk{b}:
2416 Done{Res{status, headers, Bytes.from_string(b)}}
2417 case DecBad{}:
2418 Fail{ErrBad{}}
2419 case DecSkip{}:
2420 Done{Res{status, headers, Bytes.from_string(body)}}
2421
2422# ponytail: the codings run on a String copy of the body; give zlib a Bytes input if gzip bodies get big.
2423def decoded.cs(+status: U32, +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, cs: List<&2, String>) -> Result<&1, &1, Err, Res>:
2424 match cs:
2425 case Nil{}:
2426 Done{Res{status, headers, body}}
2427 case Con{c, t}:
2428 +s = Bytes.to_string(body)
2429 decoded.pick(ce.go(Con{c, t}, DecOk{s}), status, headers, s)
2430
2431def decoded.go(empty: Bool, +status: U32, +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> Result<&1, &1, Err, Res>:
2432 match empty:
2433 case True{}:
2434 Done{Res{status, headers, body}}
2435 case False{}:
2436 decoded.cs(status, headers, body, List.reverse(&2, String, ce.split(fields(headers, "content-encoding"))))
2437
2438# The body decoded per Content-Encoding; the headers stay as sent. A corrupt body is ErrBad.
2439def decoded(res: Res) -> Result<&1, &1, Err, Res>:
2440 Res{+status, +headers, body} = res
2441 Bytes.Bytes{+len, buf} = body
2442 decoded.go(U32.is_zero(len), status, headers, Bytes.Bytes{len, buf})
2443
2444def decoded.m(r: Result<&1, &1, Err, Res>) -> Maybe<&1, Res>:
2445 match r:
2446 case Done{x}:
2447 Some{x}
2448 case Fail{e}:
2449 None{}
2450
2451def decoded.some(res: Res) -> Maybe<&1, Res>:
2452 decoded.m(decoded(res))
2453
2454def ce.words(r: Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Maybe<&1, Bytes.Bytes>:
2455 match r:
2456 case Fail{e}:
2457 None{}
2458 case Done{(+len, buf)}:
2459 Some{Bytes.Bytes{len, buf}}
2460
2461# A decoded body stops at 16 MiB, like a received one.
2462def ce.eff(~eff: U32 -> U32 -> Array<U32> -> IO(Result<&1, &1, U32 & String, U32 & Array<U32>>), b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
2463 Bytes.Bytes{+len, buf} = b
2464 do IO<Maybe<&1, Bytes.Bytes>>:
2465 r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- eff(16777216, len, buf)
2466 return ce.words(r)
2467
2468def ce.dec(d: Dec) -> Maybe<&1, Bytes.Bytes>:
2469 match d:
2470 case DecOk{b}:
2471 Some{Bytes.from_string(b)}
2472 case DecBad{}:
2473 None{}
2474 case DecSkip{}:
2475 None{}
2476
2477# ponytail: deflate runs on the pure decoder, which also takes raw DEFLATE; servers rarely send it.
2478def ce.io.deflate(on: Bool, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
2479 match on:
2480 case True{}:
2481 +s = Bytes.to_string(b)
2482 IO.pure(Maybe<&1, Bytes.Bytes>, ce.dec(ce.deflate(s, Zlib.unzlib(s))))
2483 case False{}:
2484 IO.pure(Maybe<&1, Bytes.Bytes>, Some{b})
2485
2486def ce.io.zstd(on: Bool, +c: String, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
2487 match on:
2488 case True{}:
2489 ce.eff(~Zlib.zstd.words, b)
2490 case False{}:
2491 ce.io.deflate(String.eq(c, "deflate"), b)
2492
2493def ce.io.br(on: Bool, +c: String, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
2494 match on:
2495 case True{}:
2496 ce.eff(~Zlib.brotli.words, b)
2497 case False{}:
2498 ce.io.zstd(String.eq(c, "zstd"), c, b)
2499
2500# One known coding undone: gzip, x-gzip, br, zstd, deflate, or identity.
2501def ce.io.gz(on: Bool, +c: String, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
2502 match on:
2503 case True{}:
2504 ce.eff(~Zlib.inflate.words, b)
2505 case False{}:
2506 ce.io.br(String.eq(c, "br"), c, b)
2507
2508def ce.io.go(cs: List<&2, String>, m: Maybe<&1, Bytes.Bytes>) -> IO(Maybe<&1, Bytes.Bytes>):
2509 match cs:
2510 case Nil{}:
2511 match m:
2512 case None{}:
2513 IO.pure(Maybe<&1, Bytes.Bytes>, None{})
2514 case Some{b}:
2515 IO.pure(Maybe<&1, Bytes.Bytes>, Some{b})
2516 case Con{+c, t}:
2517 match m:
2518 case None{}:
2519 IO.pure(Maybe<&1, Bytes.Bytes>, None{})
2520 case Some{b}:
2521 do IO<Maybe<&1, Bytes.Bytes>>:
2522 n : Maybe<&1, Bytes.Bytes> <- ce.io.gz(Bool.or(String.eq(c, "gzip"), String.eq(c, "x-gzip")), c, b)
2523 ce.io.go(t, n)
2524
2525def ce.has(xs: List<&2, String>, +c: String) -> Bool:
2526 match xs:
2527 case Nil{}:
2528 False{}
2529 case Con{x, t}:
2530 Bool.or(String.eq(c, x), ce.has(t, c))
2531
2532def ce.known(cs: List<&2, String>, +ok: List<&2, String>) -> Bool:
2533 match cs:
2534 case Nil{}:
2535 True{}
2536 case Con{c, t}:
2537 Bool.and(ce.has(ok, c), ce.known(t, ok))
2538
2539def decoded.io.pick(m: Maybe<&1, Bytes.Bytes>, +status: U32, headers: Map<&2, List<&2, String>>) -> Result<&1, &1, Err, Res>:
2540 match m:
2541 case Some{b}:
2542 Done{Res{status, headers, b}}
2543 case None{}:
2544 Fail{ErrBad{}}
2545
2546def decoded.io.run(known: Bool, +status: U32, +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, cs: List<&2, String>) -> IO(Result<&1, &1, Err, Res>):
2547 match known:
2548 case True{}:
2549 do IO<Result<&1, &1, Err, Res>>:
2550 m : Maybe<&1, Bytes.Bytes> <- ce.io.go(cs, Some{body})
2551 return decoded.io.pick(m, status, headers)
2552 case False{}:
2553 IO.pure(Result<&1, &1, Err, Res>, Done{Res{status, headers, body}})
2554
2555def decoded.io.go(empty: Bool, +enc: String, +status: U32, +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Res>):
2556 match empty:
2557 case True{}:
2558 IO.pure(Result<&1, &1, Err, Res>, Done{Res{status, headers, body}})
2559 case False{}:
2560 +cs = List.reverse(&2, String, ce.split(fields(headers, "content-encoding")))
2561 decoded.io.run(ce.known(cs, Con{"identity", Con{"x-gzip", ce.split(Con{enc, Nil{}})}}), status, headers, body, cs)
2562
2563# decoded through the C libraries, for the codings in enc. A body with any other coding stays as sent.
2564def decoded.io(+enc: String, res: Res) -> IO(Result<&1, &1, Err, Res>):
2565 Res{+status, +headers, body} = res
2566 Bytes.Bytes{+len, buf} = body
2567 decoded.io.go(U32.is_zero(len), enc, status, headers, Bytes.Bytes{len, buf})
2568
2569# An effect on empty input fails with ENOENT only when its library does not load.
2570def codings.ok(r: Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Bool:
2571 match r:
2572 case Fail{(+c, why)}:
2573 Bool.not(U32.is_eq(c, 2))
2574 case Done{p}:
2575 True{}
2576
2577def codings.has(~eff: U32 -> U32 -> Array<U32> -> IO(Result<&1, &1, U32 & String, U32 & Array<U32>>), b: Bytes.Bytes) -> IO(Bool):
2578 Bytes.Bytes{+len, buf} = b
2579 do IO<Bool>:
2580 r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- eff(0, len, buf)
2581 return codings.ok(r)
2582
2583def codings.add(has: Bool, +enc: String, +c: String) -> String:
2584 Bool.pick(String, has, enc ++ ", " ++ c, enc)
2585
2586# gzip and deflate, then br and zstd when their C library loads.
2587def codings() -> IO(String):
2588 do IO<String>:
2589 b : Bool <- codings.has(~Zlib.brotli.words, Bytes.new(0))
2590 z : Bool <- codings.has(~Zlib.zstd.words, Bytes.new(0))
2591 return codings.add(z, codings.add(b, "gzip, deflate", "br"), "zstd")
2592
2593# The final response of a fetch, after redirects.
2594def fetch.final(+enc: String, r: Result<&1, &1, Err, Res>) -> IO(Result<&1, &1, Err, Res>):
2595 match r:
2596 case Done{res}:
2597 decoded.io(enc, res)
2598 case Fail{e}:
2599 IO.pure(Result<&1, &1, Err, Res>, Fail{e})
2600
2601def pool.final(+enc: String, pr: Pool & Result<&1, &1, Err, Res>) -> IO(Pool & Result<&1, &1, Err, Res>):
2602 (p, r) = pr
2603 do IO<Pool & Result<&1, &1, Err, Res>>:
2604 d : Result<&1, &1, Err, Res> <- fetch.final(enc, r)
2605 return (p, d)
2606
2607def pool.how.enc(+enc: String, p: Pool, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, ms: U32, mode: Mode, cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res>):
2608 do IO<Pool & Result<&1, &1, Err, Res>>:
2609 pr : Pool & Result<&1, &1, Err, Res> <- pool.hops(mode, ms, (p, fetch.start(method, headers, body, Url.absolute(url), enc), cert))
2610 pool.final(enc, pr)
2611
2612def pool.how.cert(p: Pool, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, ms: U32, mode: Mode, cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res>):
2613 do IO<Pool & Result<&1, &1, Err, Res>>:
2614 enc : String <- codings()
2615 pool.how.enc(enc, p, method, url, headers, body, ms, mode, cert)
2616
2617# pool.how(p, "GET", "https://example.com/x?y=1", headers, body, ms, mode) follows redirects
2618# on p's idle sockets. Fail is a bad URL, a failed lookup, connect, handshake, send, read,
2619# a malformed response, more than 20 redirects, or a step past ms. Bodies are bytes.
2620def pool.how(p: Pool, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, ms: U32, mode: Mode) -> IO(Pool & Result<&1, &1, Err, Res>):
2621 pool.how.cert(p, method, url, headers, body, ms, mode, None{})
2622
2623def pool.fetch.with(p: Pool, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, ms: U32) -> IO(Pool & Result<&1, &1, Err, Res>):
2624 pool.how(p, method, url, headers, body, ms, ModeFollow{})
2625
2626def pool.fetch(p: Pool, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Pool & Result<&1, &1, Err, Res>):
2627 pool.fetch.with(p, method, url, headers, body, 30000)
2628
2629def pool.fetch.cert.with(p: Pool, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, chain: String, key: String, ms: U32) -> IO(Pool & Result<&1, &1, Err, Res>):
2630 pool.how.cert(p, method, url, headers, body, ms, ModeFollow{}, Some{Cert{chain, key}})
2631
2632def pool.fetch.cert(p: Pool, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, chain: String, key: String) -> IO(Pool & Result<&1, &1, Err, Res>):
2633 pool.fetch.cert.with(p, method, url, headers, body, chain, key, 30000)
2634
2635def fetch.end(pr: Pool & Result<&1, &1, Err, Res>) -> IO(Result<&1, &1, Err, Res>):
2636 (p, r) = pr
2637 do IO<Result<&1, &1, Err, Res>>:
2638 pool.close(p)
2639 return r
2640
2641# fetch is pool.how on a fresh pool that closes afterwards.
2642def fetch.how(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, ms: U32, mode: Mode) -> IO(Result<&1, &1, Err, Res>):
2643 do IO<Result<&1, &1, Err, Res>>:
2644 pr : Pool & Result<&1, &1, Err, Res> <- pool.how(pool.new(), method, url, headers, body, ms, mode)
2645 fetch.end(pr)
2646
2647def fetch.with(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, ms: U32) -> IO(Result<&1, &1, Err, Res>):
2648 fetch.how(method, url, headers, body, ms, ModeFollow{})
2649
2650def fetch.cert.with(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, chain: String, key: String, ms: U32) -> IO(Result<&1, &1, Err, Res>):
2651 do IO<Result<&1, &1, Err, Res>>:
2652 pr : Pool & Result<&1, &1, Err, Res> <- pool.fetch.cert.with(pool.new(), method, url, headers, body, chain, key, ms)
2653 fetch.end(pr)
2654
2655def fetch.cert(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, chain: String, key: String) -> IO(Result<&1, &1, Err, Res>):
2656 fetch.cert.with(method, url, headers, body, chain, key, 30000)
2657
2658# fetch.with and a 30 s step timeout.
2659def fetch(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Res>):
2660 fetch.with(method, url, headers, body, 30000)
2661
2662def get(url: String) -> IO(Result<&1, &1, Err, Res>):
2663 fetch("GET", url, empty(), Bytes.new(0))
2664
2665# Streaming (a body read or sent in pieces). A decoded stream owns its decoders.
2666# What the next read returns: read more, a raw piece, a decoded piece, the end, or an error.
2667type Po is Type:
2668 PoNone{}
2669 PoPiece{b: Bytes.Bytes}
2670 PoReady{b: Bytes.Bytes}
2671 PoEnd{}
2672 PoBad{e: Err}
2673
2674type Stream is Type:
2675 Stream{tls: Bool, s: Socket, ms: U32, res: Res, rb: Rb, out: Po, decs: List<&1, Zlib.Decoder>}
2676
2677type Pc is Type:
2678 Pc{rb: Rb, out: Po}
2679
2680# A body piece, or none when empty: more reads the next piece, and not more is the end.
2681def pc.po(more: Bool, empty: Bool, b: Bytes.Bytes) -> Po:
2682 match empty:
2683 case True{}:
2684 Bool.pick(Po, more, PoNone{}, PoEnd{})
2685 case False{}:
2686 PoPiece{b}
2687
2688def pc.piece(more: Bool, +rb: Rb, b: Bytes.Bytes) -> Pc:
2689 Bytes.Bytes{+len, buf} = b
2690 Pc{rb, pc.po(more, U32.is_zero(len), Bytes.Bytes{len, buf})}
2691
2692def pc.fed.of(b: Bytes.Bytes, st: Rb) -> Pc:
2693 match st:
2694 case RbDone{}:
2695 pc.piece(False{}, RbDone{}, b)
2696 case RbBad{}:
2697 Pc{RbDone{}, PoBad{ErrBad{}}}
2698 case RbLen{n}:
2699 pc.piece(True{}, RbLen{n}, b)
2700 case RbChunk{st}:
2701 pc.piece(True{}, RbChunk{st}, b)
2702 case RbClose{}:
2703 pc.piece(True{}, RbClose{}, b)
2704
2705def pc.fed(bf: Bf) -> Pc:
2706 Bf{st, parts, rest} = bf
2707 pc.fed.of(rb.body(parts), st)
2708
2709# The body bytes that just arrived: what they add to the body, and how it ends.
2710def pc.of(rb: Rb, piece: Bytes.Bytes) -> Pc:
2711 pc.fed(rb.feed(rb, Nil{}, piece))
2712
2713# The server closed. Only a close-delimited body may end this way (RFC 9112 §8).
2714def pc.end(ok: Bool) -> Pc:
2715 match ok:
2716 case True{}:
2717 Pc{RbDone{}, PoEnd{}}
2718 case False{}:
2719 Pc{RbDone{}, PoBad{ErrBad{}}}
2720
2721def pc.eof(st: Rb) -> Pc:
2722 pc.end(rb.eof(st))
2723
2724def stream.mk(+tls: Bool, s: Socket, +ms: U32, res: Res, decs: List<&1, Zlib.Decoder>, pc: Pc) -> Stream:
2725 Pc{rb, out} = pc
2726 Stream{tls, s, ms, res, rb, out, decs}
2727
2728def stream.got.piece(+tls: Bool, s: Socket, +ms: U32, res: Res, decs: List<&1, Zlib.Decoder>, +rb: Rb, p: U32 & Array<U32>) -> Stream:
2729 (+len, buf) = p
2730 stream.mk(tls, s, ms, res, decs, Bool.pick(Pc, U32.is_zero(len), pc.eof(rb), pc.of(rb, Bytes.Bytes{len, buf})))
2731
2732def stream.got(+tls: Bool, +ms: U32, res: Res, decs: List<&1, Zlib.Decoder>, +rb: Rb, m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Stream:
2733 (s, r) = m
2734 match r:
2735 case Fail{(+code, why)}:
2736 Stream{tls, s, ms, res, RbDone{}, PoBad{err.or_late(code, ErrRead{code, why})}, decs}
2737 case Done{p}:
2738 stream.got.piece(tls, s, ms, res, decs, rb, p)
2739
2740def stream.after(+rb: Rb) -> Po:
2741 match rb:
2742 case RbDone{}:
2743 PoEnd{}
2744 case RbBad{}:
2745 PoEnd{}
2746 case RbLen{n}:
2747 PoNone{}
2748 case RbChunk{st}:
2749 PoNone{}
2750 case RbClose{}:
2751 PoNone{}
2752
2753type Fed is Type:
2754 Fed{decs: List<&1, Zlib.Decoder>, body: Result<&1, &1, Err, Bytes.Bytes>}
2755
2756def stream.feed.received(done: List<&1, Zlib.Decoder>, m: Zlib.Decoder & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Fed:
2757 (d, r) = m
2758 match r:
2759 case Fail{e}:
2760 Fed{d <> done, Fail{ErrBad{}}}
2761 case Done{(+len, buf)}:
2762 Fed{d <> done, Done{Bytes.Bytes{len, buf}}}
2763
2764def stream.feed.step(st: Fed, d: Zlib.Decoder) -> IO(Fed):
2765 Fed{done, body} = st
2766 match body:
2767 case Fail{e}:
2768 IO.pure(Fed, Fed{d <> done, Fail{e}})
2769 case Done{b}:
2770 Bytes.Bytes{+len, buf} = b
2771 do IO<Fed>:
2772 m : Zlib.Decoder & Result<&1, &1, U32 & String, U32 & Array<U32>> <-
2773 Zlib.dec.feed.words(d, 16777216, len, buf)
2774 return stream.feed.received(done, m)
2775
2776def stream.feed.one(prev: IO(Fed), d: Zlib.Decoder) -> IO(Fed):
2777 do IO<Fed>:
2778 st : Fed <- prev
2779 stream.feed.step(st, d)
2780
2781def stream.feed.reverse(st: Fed) -> Fed:
2782 Fed{done, body} = st
2783 Fed{List.reverse(&1, Zlib.Decoder, done), body}
2784
2785def stream.feed.all(decs: List<&1, Zlib.Decoder>, b: Bytes.Bytes) -> IO(Fed):
2786 do IO<Fed>:
2787 st : Fed <- List.foldl(~&1, ~Zlib.Decoder, ~IO(Fed), ~stream.feed.one, decs,
2788 IO.pure(Fed, Fed{Nil{}, Done{b}}))
2789 return stream.feed.reverse(st)
2790
2791def stream.ready(empty: Bool, +rb: Rb, b: Bytes.Bytes) -> Po:
2792 match empty:
2793 case True{}:
2794 stream.after(rb)
2795 case False{}:
2796 PoReady{b}
2797
2798def stream.feed.got(+tls: Bool, s: Socket, +ms: U32, res: Res, +rb: Rb, st: Fed) -> Stream:
2799 Fed{decs, body} = st
2800 match body:
2801 case Fail{e}:
2802 Stream{tls, s, ms, res, rb, PoBad{e}, decs}
2803 case Done{b}:
2804 Bytes.Bytes{+len, buf} = b
2805 Stream{tls, s, ms, res, rb, stream.ready(U32.is_zero(len), rb, Bytes.Bytes{len, buf}), decs}
2806
2807def stream.feed.st(st: Stream, b: Bytes.Bytes) -> IO(Stream):
2808 Stream{+tls, s, +ms, res, +rb, out, decs} = st
2809 match decs:
2810 case Nil{}:
2811 IO.pure(Stream, Stream{tls, s, ms, res, rb, PoReady{b}, Nil{}})
2812 case Con{d, rest}:
2813 do IO<Stream>:
2814 fed : Fed <- stream.feed.all(Con{d, rest}, b)
2815 return stream.feed.got(tls, s, ms, res, rb, fed)
2816
2817def stream.finish.ok(r: Result<&1, &1, U32 & String, Unit>) -> Bool:
2818 match r:
2819 case Fail{e}:
2820 False{}
2821 case Done{u}:
2822 True{}
2823
2824def stream.finish(decs: List<&1, Zlib.Decoder>) -> IO(Bool):
2825 match decs:
2826 case Nil{}:
2827 IO.pure(Bool, True{})
2828 case Con{d, rest}:
2829 do IO<Bool>:
2830 r : Result<&1, &1, U32 & String, Unit> <- Zlib.dec.finish(d)
2831 tail : Bool <- stream.finish(rest)
2832 return Bool.and(stream.finish.ok(r), tail)
2833
2834def stream.ended(good: Bool, +tls: Bool, s: Socket, +ms: U32, res: Res, +rb: Rb) ->
2835 Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>:
2836 match good:
2837 case True{}:
2838 (Stream{tls, s, ms, res, rb, PoEnd{}, Nil{}}, Done{None{}})
2839 case False{}:
2840 (Stream{tls, s, ms, res, rb, PoBad{ErrBad{}}, Nil{}}, Fail{ErrBad{}})
2841
2842# The next piece of the body; None at the end. A piece is never empty.
2843@unsafe
2844def stream.read(st: Stream) -> IO(Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>):
2845 Stream{+tls, s, +ms, res, +rb, out, decs} = st
2846 match out:
2847 case PoPiece{b}:
2848 do IO<Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>>:
2849 next : Stream <- stream.feed.st(Stream{tls, s, ms, res, rb, PoNone{}, decs}, b)
2850 stream.read(next)
2851 case PoReady{b}:
2852 IO.pure(Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>,
2853 (Stream{tls, s, ms, res, rb, stream.after(rb), decs}, Done{Some{b}}))
2854 case PoEnd{}:
2855 do IO<Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>>:
2856 good : Bool <- stream.finish(decs)
2857 return stream.ended(good, tls, s, ms, res, rb)
2858 case PoBad{+e}:
2859 IO.pure(Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>,
2860 (Stream{tls, s, ms, res, rb, PoBad{e}, decs}, Fail{e}))
2861 case PoNone{}:
2862 do IO<Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>>:
2863 m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv.words(tls, s, 65536, ms)
2864 stream.read(stream.got(tls, ms, res, decs, rb, m))
2865
2866# Status and headers. Its body is empty: read the body with stream.read.
2867def stream.res(st: Stream) -> Stream & Res:
2868 Stream{tls, s, ms, res, rb, out, decs} = st
2869 Res{+status, +headers, body} = res
2870 (Stream{tls, s, ms, Res{status, headers, body}, rb, out, decs}, Res{status, headers, Bytes.new(0)})
2871
2872def stream.close(st: Stream) -> IO(Unit):
2873 Stream{tls, s, ms, res, rb, out, decs} = st
2874 do IO<Unit>:
2875 good : Bool <- stream.finish(decs)
2876 io.close(tls, s)
2877
2878# Head read state: still scanning, cut short or bad, or the head with the bytes after it.
2879type Sh is Type:
2880 ShMore{buf: Bytes.Bytes, k: U32}
2881 ShBad{err: Maybe<&2, Err>}
2882 ShRes{res: Res, rb: Rb, rest: Bytes.Bytes}
2883
2884def sh.of(hs: Hs) -> Sh:
2885 match hs:
2886 case HsWait{buf, k}:
2887 ShMore{buf, k}
2888 case HsBad{}:
2889 ShBad{None{}}
2890 case HsSeek{buf, from, k}:
2891 ShBad{None{}}
2892 case HsRes{res, rb, rest}:
2893 ShRes{res, rb, rest}
2894
2895def sh.piece(+head: Bool, buf: Bytes.Bytes, +k: U32, p: U32 & Array<U32>) -> Sh:
2896 (+len, b) = p
2897 Bool.pick(Sh, U32.is_zero(len), ShBad{None{}}, sh.of(hs.more(head, k, buf, Bytes.Bytes{len, b})))
2898
2899def sh.next(+head: Bool, buf: Bytes.Bytes, +k: U32, m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Socket & Sh:
2900 (s, r) = m
2901 match r:
2902 case Fail{(+code, why)}:
2903 (s, ShBad{Some{err.or_late(code, ErrRead{code, why})}})
2904 case Done{p}:
2905 (s, sh.piece(head, buf, k, p))
2906
2907def fetch.fail.of(r: Result<&1, &1, Err, Res>) -> Result<&1, &1, Err, Stream>:
2908 match r:
2909 case Fail{e}:
2910 Fail{e}
2911 case Done{res}:
2912 Fail{ErrBad{}}
2913
2914# Reads until the final head is in; the body bytes that came with it are the first piece.
2915@unsafe
2916def stream.head(+tls: Bool, +ms: U32, +head: Bool, st: Socket & Sh) -> IO(Result<&1, &1, Err, Stream>):
2917 (s, sh) = st
2918 match sh:
2919 case ShMore{buf, +k}:
2920 do IO<Result<&1, &1, Err, Stream>>:
2921 m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv.words(tls, s, 65536, ms)
2922 stream.head(tls, ms, head, sh.next(head, buf, k, m))
2923 case ShBad{err}:
2924 do IO<Result<&1, &1, Err, Stream>>:
2925 r : Result<&1, &1, Err, Res> <- fetch.bad(tls, s, err)
2926 return fetch.fail.of(r)
2927 case ShRes{res, rb, rest}:
2928 IO.pure(Result<&1, &1, Err, Stream>, Done{stream.mk(tls, s, ms, res, Nil{}, pc.of(rb, rest))})
2929
2930def stream.sent(+tls: Bool, +ms: U32, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Result<&1, &1, Err, Stream>):
2931 (s, r) = m
2932 match r:
2933 case Fail{(+code, why)}:
2934 do IO<Result<&1, &1, Err, Stream>>:
2935 io.close(tls, s)
2936 return Fail{err.or_late(code, ErrWrite{code, why})}
2937 case Done{u}:
2938 stream.head(tls, ms, head, (s, ShMore{Bytes.new(0), 0}))
2939
2940def stream.conn(r: Result<&1, &1, Err, Conn>, +ms: U32, +head: Bool, wire: Bytes.Bytes) -> IO(Result<&1, &1, Err, Stream>):
2941 match r:
2942 case Fail{e}:
2943 IO.pure(Result<&1, &1, Err, Stream>, Fail{e})
2944 case Done{c}:
2945 Conn{+tls, s} = c
2946 do IO<Result<&1, &1, Err, Stream>>:
2947 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(tls, s, wire)
2948 stream.sent(tls, ms, head, sent)
2949
2950# One connection per stream; the request says close.
2951def stream.origin(+ms: U32, +head: Bool, wire: Bytes.Bytes, a: Url.Abs, known: Bool) -> IO(Result<&1, &1, Err, Stream>):
2952 Url.Abs{+scheme, +host, +port, target} = a
2953 match known:
2954 case False{}:
2955 IO.pure(Result<&1, &1, Err, Stream>, Fail{ErrUrl{}})
2956 case True{}:
2957 do IO<Result<&1, &1, Err, Stream>>:
2958 ips : List<&2, String> <- Dns.resolve.all(host)
2959 c : Result<&1, &1, Err, Conn> <- conn.open.all(String.eq(scheme, "https"), ms, host, port, ips, None{})
2960 stream.conn(c, ms, head, wire)
2961
2962def stream.one.of(+method: String, +url: Url.Abs, +headers: Map<&2, List<&2, String>>, +ms: U32, r: Bytes.Bytes & Bytes.Bytes) -> IO(Hop & Result<&1, &1, Err, Stream>):
2963 Url.Abs{scheme, host, port, +target} = url
2964 (body, wire) = r
2965 do IO<Hop & Result<&1, &1, Err, Stream>>:
2966 got : Result<&1, &1, Err, Stream> <- stream.origin(ms, String.eq(method, "HEAD"), encode_req.on(method, target, Url.host_field(url), headers, wire, True{}), url, pool.scheme.ok(url))
2967 return (Hop{method, url, headers, body}, got)
2968
2969# One request on its own connection. The hop comes back for the redirect.
2970def stream.one(h: Hop, +ms: U32) -> IO(Hop & Result<&1, &1, Err, Stream>):
2971 Hop{+method, +url, +headers, body} = h
2972 stream.one.of(method, url, headers, ms, Bytes.slice(body, 0, 4294967295))
2973
2974# Go: the next request. Drop: close this stream, then go on. Done: the answer.
2975type Sn is Type:
2976 SnGo{left: Nat, hop: Hop}
2977 SnDrop{st: Stream, next: Next}
2978 SnDone{r: Result<&1, &1, Err, Stream>}
2979
2980def sn.of(n: Next) -> Sn:
2981 match n:
2982 case NGo{l, h}:
2983 SnGo{l, h}
2984 case NStop{}:
2985 SnDone{Fail{ErrRedirect{}}}
2986 case NDone{m}:
2987 match m:
2988 case Fail{e}:
2989 SnDone{Fail{e}}
2990 case Done{r}:
2991 SnDone{Fail{ErrBad{}}}
2992
2993def stream.decide.n(st: Stream, n: Next) -> Sn:
2994 match n:
2995 case NDone{m}:
2996 SnDone{Done{st}}
2997 case NGo{l, h}:
2998 SnDrop{st, NGo{l, h}}
2999 case NStop{}:
3000 SnDrop{st, NStop{}}
3001
3002def stream.decide.of(+left: Nat, hop: Hop, sr: Stream & Res) -> Sn:
3003 (st, res) = sr
3004 stream.decide.n(st, fetch.decide(left, hop, Done{res}))
3005
3006def stream.decide(+left: Nat, x: Hop & Result<&1, &1, Err, Stream>) -> Sn:
3007 (hop, r) = x
3008 match r:
3009 case Fail{e}:
3010 SnDone{Fail{e}}
3011 case Done{st}:
3012 stream.decide.of(left, hop, stream.res(st))
3013
3014@unsafe
3015def stream.hops(+ms: U32, sn: Sn) -> IO(Result<&1, &1, Err, Stream>):
3016 match sn:
3017 case SnDone{r}:
3018 IO.pure(Result<&1, &1, Err, Stream>, r)
3019 case SnGo{+left, hop}:
3020 do IO<Result<&1, &1, Err, Stream>>:
3021 x : Hop & Result<&1, &1, Err, Stream> <- stream.one(hop, ms)
3022 stream.hops(ms, stream.decide(left, x))
3023 case SnDrop{st, next}:
3024 do IO<Result<&1, &1, Err, Stream>>:
3025 stream.close(st)
3026 stream.hops(ms, sn.of(next))
3027
3028type Opened is Type:
3029 Opened{decs: List<&1, Zlib.Decoder>, bad: Bool}
3030
3031def stream.open.got(st: Opened, r: Result<&1, &1, U32 & String, Zlib.Decoder>) -> Opened:
3032 Opened{decs, bad} = st
3033 match r:
3034 case Fail{e}:
3035 Opened{decs, True{}}
3036 case Done{d}:
3037 Opened{d <> decs, bad}
3038
3039def stream.open.add(st: Opened, m: IO(Result<&1, &1, U32 & String, Zlib.Decoder>)) -> IO(Opened):
3040 do IO<Opened>:
3041 r : Result<&1, &1, U32 & String, Zlib.Decoder> <- m
3042 return stream.open.got(st, r)
3043
3044def stream.open.zstd(zstd: Bool, st: Opened) -> IO(Opened):
3045 match zstd:
3046 case True{}:
3047 stream.open.add(st, Zlib.zstd.new())
3048 case False{}:
3049 IO.pure(Opened, st)
3050
3051def stream.open.br(br: Bool, +c: String, st: Opened) -> IO(Opened):
3052 match br:
3053 case True{}:
3054 stream.open.add(st, Zlib.brotli.new())
3055 case False{}:
3056 stream.open.zstd(String.eq(c, "zstd"), st)
3057
3058def stream.open.gz(gz: Bool, +c: String, st: Opened) -> IO(Opened):
3059 match gz:
3060 case True{}:
3061 stream.open.add(st, Zlib.inflate.new())
3062 case False{}:
3063 stream.open.br(String.eq(c, "br"), c, st)
3064
3065def stream.open.step(+c: String, st: Opened) -> IO(Opened):
3066 Opened{decs, bad} = st
3067 match bad:
3068 case True{}:
3069 IO.pure(Opened, Opened{decs, True{}})
3070 case False{}:
3071 stream.open.gz(Bool.or(String.eq(c, "gzip"), Bool.or(String.eq(c, "x-gzip"), String.eq(c, "deflate"))),
3072 c, Opened{decs, False{}})
3073
3074def stream.open.one(prev: IO(Opened), c: String) -> IO(Opened):
3075 do IO<Opened>:
3076 st : Opened <- prev
3077 stream.open.step(c, st)
3078
3079def stream.open.all(cs: List<&2, String>) -> IO(Opened):
3080 List.foldl(~&2, ~String, ~IO(Opened), ~stream.open.one, cs, IO.pure(Opened, Opened{Nil{}, False{}}))
3081
3082def stream.put.decs(st: Stream, decs: List<&1, Zlib.Decoder>) -> Stream:
3083 Stream{tls, s, ms, res, rb, out, old} = st
3084 Stream{tls, s, ms, res, rb, out, decs}
3085
3086def stream.init.opened(st: Stream, opened: Opened) -> IO(Result<&1, &1, Err, Stream>):
3087 Opened{decs, bad} = opened
3088 match bad:
3089 case True{}:
3090 do IO<Result<&1, &1, Err, Stream>>:
3091 stream.close(stream.put.decs(st, decs))
3092 return Fail{ErrBad{}}
3093 case False{}:
3094 IO.pure(Result<&1, &1, Err, Stream>, Done{stream.put.decs(st, List.reverse(&1, Zlib.Decoder, decs))})
3095
3096def stream.init.known(known: Bool, st: Stream, cs: List<&2, String>) -> IO(Result<&1, &1, Err, Stream>):
3097 match known:
3098 case False{}:
3099 IO.pure(Result<&1, &1, Err, Stream>, Done{st})
3100 case True{}:
3101 do IO<Result<&1, &1, Err, Stream>>:
3102 opened : Opened <- stream.open.all(cs)
3103 stream.init.opened(st, opened)
3104
3105def stream.init.st(+enc: String, st: Stream) -> IO(Result<&1, &1, Err, Stream>):
3106 Stream{tls, s, ms, res, rb, out, decs} = st
3107 Res{+status, +headers, body} = res
3108 +cs = List.reverse(&2, String, ce.split(fields(headers, "content-encoding")))
3109 stream.init.known(ce.known(cs, Con{"identity", Con{"x-gzip", ce.split(Con{enc, Nil{}})}}),
3110 Stream{tls, s, ms, Res{status, headers, body}, rb, out, decs}, cs)
3111
3112def stream.init(+enc: String, r: Result<&1, &1, Err, Stream>) -> IO(Result<&1, &1, Err, Stream>):
3113 match r:
3114 case Fail{e}:
3115 IO.pure(Result<&1, &1, Err, Stream>, Fail{e})
3116 case Done{st}:
3117 stream.init.st(enc, st)
3118
3119def stream.start(method: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, u: Maybe<&2, Url.Abs>) -> Sn:
3120 match u:
3121 case None{}:
3122 SnDone{Fail{ErrUrl{}}}
3123 case Some{a}:
3124 SnGo{20n, Hop{method, a, req.put(Map.to_list(&2, List<&2, String>, headers), empty()), body}}
3125
3126# Open a raw stream. Its body bytes and headers remain as sent.
3127def open.raw.with(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, +ms: U32) -> IO(Result<&1, &1, Err, Stream>):
3128 stream.hops(ms, stream.start(method, headers, body, Url.absolute(url)))
3129
3130def open.raw(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Stream>):
3131 open.raw.with(method, url, headers, body, 30000)
3132
3133def open.with.enc(+enc: String, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, +ms: U32) -> IO(Result<&1, &1, Err, Stream>):
3134 do IO<Result<&1, &1, Err, Stream>>:
3135 r : Result<&1, &1, Err, Stream> <-
3136 stream.hops(ms, stream.start(method, accept.enc(headers, enc), body, Url.absolute(url)))
3137 stream.init(enc, r)
3138
3139# Follow redirects, then decode each body piece by Content-Encoding. Unknown codings stay raw.
3140def open.with(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, +ms: U32) -> IO(Result<&1, &1, Err, Stream>):
3141 do IO<Result<&1, &1, Err, Stream>>:
3142 enc : String <- codings()
3143 open.with.enc(enc, method, url, headers, body, ms)
3144
3145def open(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Stream>):
3146 open.with(method, url, headers, body, 30000)
3147
3148# Upload: the request body sent in chunks (RFC 9112 §7.1). err: the first failed write.
3149type Up is Type:
3150 Up{tls: Bool, s: Socket, ms: U32, head: Bool, err: Maybe<&2, Err>}
3151
3152def hex.digit(+n: U32) -> Char:
3153 Chr{Bool.pick(U32, U32.is_lt(n, 10), (48 + n : U32), (87 + n : U32))}
3154
3155def hex.go(k: Nat, +n: U32, acc: String) -> String:
3156 match k:
3157 case 0n:
3158 acc
3159 case 1n+p:
3160 hex.go(p, U32.shrn(n, 4n), SCon{hex.digit(U32.and(n, 15)), acc})
3161
3162def hex.trim(+s: String) -> String:
3163 match s:
3164 case SNil{}:
3165 SNil{}
3166 case SCon{Chr{+c}, +t}:
3167 Bool.pick(String, Bool.and(U32.is_eq(c, 48), Bool.not(String.is_empty(t))), hex.trim(t), SCon{Chr{c}, t})
3168
3169def hex(+n: U32) -> String:
3170 hex.trim(hex.go(8n, n, ""))
3171
3172def up.sent(+tls: Bool, +ms: U32, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> Up:
3173 (s, r) = m
3174 match r:
3175 case Fail{(+code, why)}:
3176 Up{tls, s, ms, head, Some{err.or_late(code, ErrWrite{code, why})}}
3177 case Done{u}:
3178 Up{tls, s, ms, head, None{}}
3179
3180def up.conn(r: Result<&1, &1, Err, Conn>, +ms: U32, +head: Bool, wire: String) -> IO(Result<&1, &1, Err, Up>):
3181 match r:
3182 case Fail{e}:
3183 IO.pure(Result<&1, &1, Err, Up>, Fail{e})
3184 case Done{c}:
3185 Conn{+tls, s} = c
3186 do IO<Result<&1, &1, Err, Up>>:
3187 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send(tls, s, wire)
3188 return Done{up.sent(tls, ms, head, sent)}
3189
3190def up.head(+method: String, +target: String, +hf: String, +headers: Map<&2, List<&2, String>>) -> String:
3191 request(method, target, set(set(set(req.put(Map.to_list(&2, List<&2, String>, headers), empty()), "host", hf), "connection", "close"), "transfer-encoding", "chunked"), "")
3192
3193def up.origin(+method: String, +ms: U32, headers: Map<&2, List<&2, String>>, a: Url.Abs, known: Bool) -> IO(Result<&1, &1, Err, Up>):
3194 Url.Abs{+scheme, +host, +port, +target} = a
3195 match known:
3196 case False{}:
3197 IO.pure(Result<&1, &1, Err, Up>, Fail{ErrUrl{}})
3198 case True{}:
3199 do IO<Result<&1, &1, Err, Up>>:
3200 ips : List<&2, String> <- Dns.resolve.all(host)
3201 c : Result<&1, &1, Err, Conn> <- conn.open.all(String.eq(scheme, "https"), ms, host, port, ips, None{})
3202 up.conn(c, ms, String.eq(method, "HEAD"), up.head(method, target, Url.host_field(a), headers))
3203
3204def up.url(+method: String, +ms: U32, headers: Map<&2, List<&2, String>>, u: Maybe<&2, Url.Abs>) -> IO(Result<&1, &1, Err, Up>):
3205 match u:
3206 case None{}:
3207 IO.pure(Result<&1, &1, Err, Up>, Fail{ErrUrl{}})
3208 case Some{+a}:
3209 up.origin(method, ms, headers, a, pool.scheme.ok(a))
3210
3211# Http.upload(method, url, headers) sends the head. A streamed body cannot be replayed, so redirects are not followed.
3212def upload.with(+method: String, url: String, headers: Map<&2, List<&2, String>>, +ms: U32) -> IO(Result<&1, &1, Err, Up>):
3213 up.url(method, ms, headers, Url.absolute(url))
3214
3215def upload(+method: String, url: String, headers: Map<&2, List<&2, String>>) -> IO(Result<&1, &1, Err, Up>):
3216 upload.with(method, url, headers, 30000)
3217
3218def up.wrote(+tls: Bool, +ms: U32, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> Up & Result<&2, &2, Err, Unit>:
3219 (s, r) = m
3220 match r:
3221 case Fail{(+code, why)}:
3222 +e = err.or_late(code, ErrWrite{code, why})
3223 (Up{tls, s, ms, head, Some{e}}, Fail{e})
3224 case Done{u}:
3225 (Up{tls, s, ms, head, None{}}, Done{Unit{}})
3226
3227# One write per chunk, so the size line and the data do not wait on each other (Nagle).
3228def up.put(+tls: Bool, s: Socket, +ms: U32, +head: Bool, +len: U32, piece: Bytes.Bytes, skip: Bool) -> IO(Up & Result<&2, &2, Err, Unit>):
3229 match skip:
3230 case True{}:
3231 IO.pure(Up & Result<&2, &2, Err, Unit>, (Up{tls, s, ms, head, None{}}, Done{Unit{}}))
3232 case False{}:
3233 do IO<Up & Result<&2, &2, Err, Unit>>:
3234 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(tls, s, Bytes.concat(Con{Bytes.from_string(hex(len) ++ "\r\n"), Con{piece, Con{Bytes.from_string("\r\n"), Nil{}}}}))
3235 return up.wrote(tls, ms, head, sent)
3236
3237def up.chunk(+tls: Bool, s: Socket, +ms: U32, +head: Bool, piece: Bytes.Bytes) -> IO(Up & Result<&2, &2, Err, Unit>):
3238 Bytes.Bytes{+len, buf} = piece
3239 up.put(tls, s, ms, head, len, Bytes.Bytes{len, buf}, U32.is_zero(len))
3240
3241# One chunk. An empty piece sends nothing, since an empty chunk would end the body.
3242def upload.write(up: Up, piece: Bytes.Bytes) -> IO(Up & Result<&2, &2, Err, Unit>):
3243 Up{+tls, s, +ms, +head, err} = up
3244 match err:
3245 case Some{+e}:
3246 IO.pure(Up & Result<&2, &2, Err, Unit>, (Up{tls, s, ms, head, Some{e}}, Fail{e}))
3247 case None{}:
3248 up.chunk(tls, s, ms, head, piece)
3249
3250# Ends the body and returns the response as a stream.
3251def upload.finish(up: Up) -> IO(Result<&1, &1, Err, Stream>):
3252 Up{+tls, s, +ms, +head, err} = up
3253 match err:
3254 case Some{e}:
3255 do IO<Result<&1, &1, Err, Stream>>:
3256 io.close(tls, s)
3257 return Fail{e}
3258 case None{}:
3259 do IO<Result<&1, &1, Err, Stream>>:
3260 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send(tls, s, "0\r\n\r\n")
3261 stream.sent(tls, ms, head, sent)
3262
3263def reply.bytes(res: Res, head: Bool, close: Bool) -> Bytes.Bytes:
3264 Res{+status, +headers, body} = res
3265 encode.on(Res{status, Bool.pick(Map<&2, List<&2, String>>, close, set(headers, "connection", "close"), headers), body}, head)
3266
3267def reply.fail.bytes(+status: U32) -> Res:
3268 Res{status, empty(), Bytes.from_string(reason(status))}
3269
3270def reply.sent.close(m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Unit):
3271 (s, r) = m
3272 Socket.close(s)
3273
3274def reply_fail(s: Socket, +status: U32) -> IO(Unit):
3275 do IO<Unit>:
3276 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(False{}, s, encode(reply.fail.bytes(status)))
3277 reply.sent.close(sent)
3278
3279
3280# The head is parsed once, when it is whole. Body pieces are kept as they come and joined once.
3281type Sv is Type:
3282 SvHead{buf: Bytes.Bytes}
3283 SvLen{req: Req, v11: Bool, left: U32, parts: List<&1, Bytes.Bytes>}
3284 SvChunk{req: Req, v11: Bool, n: U32, st: Dc, parts: List<&1, Bytes.Bytes>}
3285
3286# More: read on, first answering 100 Continue when cont is set.
3287type Turn is Type:
3288 TurnClose{}
3289 TurnFail{status: U32}
3290 TurnReq{req: Req, rest: Bytes.Bytes, v11: Bool}
3291 TurnMore{sv: Sv, cont: Bool}
3292
3293def serve.max() -> Nat:
3294 fetch.max()
3295
3296def sv.none() -> Sv:
3297 SvHead{Bytes.new(0)}
3298
3299def sv.body(req: Req, +v11: Bool, parts: List<&1, Bytes.Bytes>, rest: Bytes.Bytes) -> Turn:
3300 Req{method, path, headers, body} = req
3301 TurnReq{Req{method, path, headers, rb.body(parts)}, rest, v11}
3302
3303def sv.len.cut(req: Req, +v11: Bool, parts: List<&1, Bytes.Bytes>, +len: U32, +left: U32, r: Bytes.Bytes & Bytes.Bytes) -> Turn:
3304 (piece, last) = r
3305 sv.body(req, v11, Con{last, parts}, bytes.snd(Bytes.slice(piece, left, (len - left : U32))))
3306
3307def sv.len.have(short: Bool, req: Req, +v11: Bool, +left: U32, parts: List<&1, Bytes.Bytes>, +len: U32, piece: Bytes.Bytes) -> Turn:
3308 match short:
3309 case True{}:
3310 TurnMore{SvLen{req, v11, (left - len : U32), Con{piece, parts}}, False{}}
3311 case False{}:
3312 sv.len.cut(req, v11, parts, len, left, Bytes.slice(piece, 0, left))
3313
3314def sv.len(req: Req, +v11: Bool, +left: U32, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Turn:
3315 Bytes.Bytes{+len, buf} = piece
3316 sv.len.have(U32.is_lt(len, left), req, v11, left, parts, len, Bytes.Bytes{len, buf})
3317
3318def sv.chunk.of(req: Req, +v11: Bool, +n: U32, c: Ck) -> Turn:
3319 Ck{st, parts, rest} = c
3320 match st:
3321 case DcDone{}:
3322 sv.body(req, v11, parts, rest)
3323 case DcBad{}:
3324 TurnFail{400}
3325 case DcSize{a, b}:
3326 TurnMore{SvChunk{req, v11, n, DcSize{a, b}, parts}, False{}}
3327 case DcExt{x}:
3328 TurnMore{SvChunk{req, v11, n, DcExt{x}, parts}, False{}}
3329 case DcSizeLf{x}:
3330 TurnMore{SvChunk{req, v11, n, DcSizeLf{x}, parts}, False{}}
3331 case DcData{k}:
3332 TurnMore{SvChunk{req, v11, n, DcData{k}, parts}, False{}}
3333 case DcDataCr{}:
3334 TurnMore{SvChunk{req, v11, n, DcDataCr{}, parts}, False{}}
3335 case DcDataLf{}:
3336 TurnMore{SvChunk{req, v11, n, DcDataLf{}, parts}, False{}}
3337 case DcTr{j}:
3338 TurnMore{SvChunk{req, v11, n, DcTr{j}, parts}, False{}}
3339
3340def sv.chunk.cap(big: Bool, req: Req, +v11: Bool, +n: U32, st: Dc, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Turn:
3341 match big:
3342 case True{}:
3343 TurnFail{413}
3344 case False{}:
3345 sv.chunk.of(req, v11, n, ck(piece, st, parts))
3346
3347def sv.chunk(+max: Nat, req: Req, +v11: Bool, +n: U32, st: Dc, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Turn:
3348 Bytes.Bytes{+len, buf} = piece
3349 +n2 = (n + len : U32)
3350 sv.chunk.cap(Bool.or(U32.is_lt(n2, n), Nat.is_lt(max, U32.to_nat(n2))), req, v11, n2, st, parts, Bytes.Bytes{len, buf})
3351
3352# RFC 9110 §10.1.1: answer 100 Continue only when the body is still to come.
3353def sv.cont(want: Bool, t: Turn) -> Turn:
3354 match t:
3355 case TurnMore{sv, c}:
3356 TurnMore{sv, want}
3357 case TurnClose{}:
3358 TurnClose{}
3359 case TurnFail{s}:
3360 TurnFail{s}
3361 case TurnReq{req, rest, v11}:
3362 TurnReq{req, rest, v11}
3363
3364def sv.cl.k(big: Bool, req: Req, +v11: Bool, +k: U32, rest: Bytes.Bytes) -> Turn:
3365 match big:
3366 case True{}:
3367 TurnFail{413}
3368 case False{}:
3369 sv.len(req, v11, k, Nil{}, rest)
3370
3371def sv.cl(+max: Nat, req: Req, +v11: Bool, rest: Bytes.Bytes, n: Maybe<&2, U32>) -> Turn:
3372 match n:
3373 case None{}:
3374 TurnFail{400}
3375 case Some{+k}:
3376 sv.cl.k(Nat.is_lt(max, U32.to_nat(k)), req, v11, k, rest)
3377
3378def sv.frame(+max: Nat, req: Req, +v11: Bool, rest: Bytes.Bytes, te: Bool) -> Turn:
3379 Req{method, path, +headers, body} = req
3380 match te:
3381 case True{}:
3382 sv.chunk(max, Req{method, path, headers, body}, v11, 0, dc.start(), Nil{}, rest)
3383 case False{}:
3384 sv.cl(max, Req{method, path, headers, body}, v11, rest, parse_u32(header(headers, "content-length")))
3385
3386def sv.expects(+v11: Bool, +headers: Map<&2, List<&2, String>>) -> Bool:
3387 Bool.and(v11, String.eq(String.to_lower(header(headers, "expect")), "100-continue"))
3388
3389def sv.got.head(+max: Nat, +v11: Bool, rest: Bytes.Bytes, req: Req) -> Turn:
3390 Req{method, path, +headers, body} = req
3391 sv.cont(sv.expects(v11, headers), sv.frame(max, Req{method, path, headers, body}, v11, rest, has_header(headers, "transfer-encoding")))
3392
3393def sv.parsed(+max: Nat, +v11: Bool, rest: Bytes.Bytes, g: Got) -> Turn:
3394 match g:
3395 case GotBad{}:
3396 TurnFail{400}
3397 case GotMore{}:
3398 TurnFail{400}
3399 case GotReq{req}:
3400 TurnReq{req, rest, v11}
3401 case GotHead{req}:
3402 sv.got.head(max, v11, rest, req)
3403
3404def sv.split(+max: Nat, +hlen: U32, +len: U32, r: Bytes.Bytes & Bytes.Bytes) -> Turn:
3405 (buf, hb) = r
3406 +head = Bytes.to_string(hb)
3407 sv.parsed(max, req.v11(head), bytes.snd(Bytes.slice(buf, hlen, (len - hlen : U32))), parse.got(head))
3408
3409def sv.hit.none(big: Bool, buf: Bytes.Bytes) -> Turn:
3410 match big:
3411 case True{}:
3412 TurnFail{431}
3413 case False{}:
3414 TurnMore{SvHead{buf}, False{}}
3415
3416def sv.hit.some(big: Bool, +max: Nat, +hlen: U32, +len: U32, buf: Bytes.Bytes) -> Turn:
3417 match big:
3418 case True{}:
3419 TurnFail{431}
3420 case False{}:
3421 sv.split(max, hlen, len, Bytes.slice(buf, 0, hlen))
3422
3423# RFC 6585 §5: a head over 64 KiB is refused.
3424def sv.hit(+max: Nat, +len: U32, buf: Bytes.Bytes, at: Maybe<&2, U32>) -> Turn:
3425 match at:
3426 case None{}:
3427 sv.hit.none(U32.is_lt(65536, len), buf)
3428 case Some{+i}:
3429 +hlen = (i + 4 : U32)
3430 sv.hit.some(U32.is_lt(65536, hlen), max, hlen, len, buf)
3431
3432def sv.seek.of(+max: Nat, +len: U32, +from: U32, buf: Bytes.Bytes, r: Bytes.Bytes & Maybe<&2, U32>) -> Turn:
3433 (tail, m) = r
3434 sv.hit(max, len, buf, found.at(from, m))
3435
3436def sv.seek(+max: Nat, +len: U32, +from: U32, r: Bytes.Bytes & Bytes.Bytes) -> Turn:
3437 (buf, tail) = r
3438 sv.seek.of(max, len, from, buf, Bytes.find(tail, "\r\n\r\n"))
3439
3440# Only the new bytes, and the 3 before them, can finish the blank line.
3441def sv.head.at(+max: Nat, +from: U32, buf: Bytes.Bytes) -> Turn:
3442 Bytes.Bytes{+len, b} = buf
3443 sv.seek(max, len, from, Bytes.slice(Bytes.Bytes{len, b}, from, (len - from : U32)))
3444
3445def sv.head(+max: Nat, buf: Bytes.Bytes, piece: Bytes.Bytes) -> Turn:
3446 Bytes.Bytes{+ol, ob} = buf
3447 sv.head.at(max, Bool.pick(U32, U32.is_lt(ol, 3), 0, (ol - 3 : U32)), Bytes.append(Bytes.Bytes{ol, ob}, piece))
3448
3449def sv.closed.pick(empty: Bool) -> Turn:
3450 match empty:
3451 case True{}:
3452 TurnClose{}
3453 case False{}:
3454 TurnFail{400}
3455
3456def sv.closed.head(buf: Bytes.Bytes) -> Turn:
3457 Bytes.Bytes{+len, b} = buf
3458 sv.closed.pick(U32.is_eq(len, 0))
3459
3460# A close mid-request is a request cut short (RFC 9112 §8).
3461def sv.step(closed: Bool, +max: Nat, sv: Sv, piece: Bytes.Bytes) -> Turn:
3462 match closed:
3463 case True{}:
3464 match sv:
3465 case SvHead{buf}:
3466 sv.closed.head(buf)
3467 case SvLen{req, v11, left, parts}:
3468 TurnFail{400}
3469 case SvChunk{req, v11, n, st, parts}:
3470 TurnFail{400}
3471 case False{}:
3472 match sv:
3473 case SvHead{buf}:
3474 sv.head(max, buf, piece)
3475 case SvLen{req, +v11, +left, parts}:
3476 sv.len(req, v11, left, parts, piece)
3477 case SvChunk{req, +v11, +n, st, parts}:
3478 sv.chunk(max, req, v11, n, st, parts, piece)
3479
3480def sv.frame.req(t: Turn) -> Maybe<&1, String & String>:
3481 match t:
3482 case TurnReq{req, rest, v11}:
3483 Req{method, path, headers, body} = req
3484 Some{(Bytes.to_string(body), Bytes.to_string(rest))}
3485 case TurnMore{sv, c}:
3486 None{}
3487 case TurnFail{s}:
3488 None{}
3489 case TurnClose{}:
3490 None{}
3491
3492def sv.frame.go(xs: List<&2, String>, t: Turn) -> Maybe<&1, String & String>:
3493 match xs:
3494 case Nil{}:
3495 sv.frame.req(t)
3496 case Con{+x, rest}:
3497 match t:
3498 case TurnMore{sv, c}:
3499 sv.frame.go(rest, sv.step(False{}, serve.max(), sv, Bytes.from_string(x)))
3500 case TurnReq{req, r, v11}:
3501 sv.frame.req(TurnReq{req, r, v11})
3502 case TurnFail{s}:
3503 None{}
3504 case TurnClose{}:
3505 None{}
3506
3507# The body and the bytes after it, once the pieces make a whole request; None otherwise.
3508def serve.frame(xs: List<&2, String>) -> Maybe<&1, String & String>:
3509 sv.frame.go(xs, TurnMore{sv.none(), False{}})
3510
3511def talk.piece(+max: Nat, sv: Sv, p: U32 & Array<U32>) -> Turn:
3512 (+len, buf) = p
3513 sv.step(U32.is_eq(len, 0), max, sv, Bytes.Bytes{len, buf})
3514
3515def talk.next(+max: Nat, sv: Sv, m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Socket & Turn:
3516 (s, r) = m
3517 match r:
3518 case Fail{e}:
3519 (s, TurnClose{})
3520 case Done{p}:
3521 (s, talk.piece(max, sv, p))
3522
3523def talk.after.pick(empty: Bool, +max: Nat, rest: Bytes.Bytes) -> Turn:
3524 match empty:
3525 case True{}:
3526 TurnMore{sv.none(), False{}}
3527 case False{}:
3528 sv.step(False{}, max, sv.none(), rest)
3529
3530def talk.after.rest(+max: Nat, rest: Bytes.Bytes, s: Socket) -> Socket & Turn:
3531 Bytes.Bytes{+len, buf} = rest
3532 (s, talk.after.pick(U32.is_eq(len, 0), max, Bytes.Bytes{len, buf}))
3533
3534def talk.after.keep(keep: Bool, +max: Nat, rest: Bytes.Bytes, s: Socket) -> Socket & Turn:
3535 match keep:
3536 case False{}:
3537 (s, TurnClose{})
3538 case True{}:
3539 talk.after.rest(max, rest, s)
3540
3541def talk.after(+max: Nat, keep: Bool, rest: Bytes.Bytes, m: Socket & Result<&1, &1, U32 & String, Unit>) -> Socket & Turn:
3542 (s, r) = m
3543 match r:
3544 case Fail{e}:
3545 (s, TurnClose{})
3546 case Done{u}:
3547 talk.after.keep(keep, max, rest, s)
3548
3549def talk.send(+max: Nat, s: Socket, rest: Bytes.Bytes, +headers: Map<&2, List<&2, String>>, v11: Bool, +head: Bool, res: Res) -> IO(Socket & Turn):
3550 Res{+status, +rh, body} = res
3551 +keep = serve.keep(headers, v11, status, rh)
3552 do IO<Socket & Turn>:
3553 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(False{}, s, reply.bytes(Res{status, rh, body}, head, Bool.not(keep)))
3554 return talk.after(max, keep, rest, sent)
3555
3556def talk.cont.sent(m: Socket & Result<&1, &1, U32 & String, Unit>) -> Socket:
3557 (s, r) = m
3558 s
3559
3560def talk.cont(cont: Bool, s: Socket) -> IO(Socket):
3561 match cont:
3562 case False{}:
3563 IO.pure(Socket, s)
3564 case True{}:
3565 do IO<Socket>:
3566 sent : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.send(s, "HTTP/1.1 100 Continue\r\n\r\n")
3567 return talk.cont.sent(sent)
3568
3569@unsafe
3570def talk(~h: Req -> IO(Res), +max: Nat, st: Socket & Turn) -> IO(Unit):
3571 (s, t) = st
3572 match t:
3573 case TurnMore{sv, cont}:
3574 do IO<Unit>:
3575 s2 : Socket <- talk.cont(cont, s)
3576 m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- Wire.recv.words(s2, 65536, 30000)
3577 talk(~h, max, talk.next(max, sv, m))
3578 case TurnReq{req, rest, v11}:
3579 Req{+method, path, +headers, body} = req
3580 do IO<Unit>:
3581 res : Res <- h(Req{method, path, headers, body})
3582 next : Socket & Turn <- talk.send(max, s, rest, headers, v11, String.eq(method, "HEAD"), res)
3583 talk(~h, max, next)
3584 case TurnFail{status}:
3585 reply_fail(s, status)
3586 case TurnClose{}:
3587 Socket.close(s)
3588
3589def conn(~h: Req -> IO(Res), +max: Nat, m: Listener & Result<&1, &1, U32 & String, Socket>) -> IO(Listener):
3590 (l, r) = m
3591 do IO<Listener>:
3592 s : Socket <- IO.pass(Socket, r)
3593 IO.spawn(Unit, talk(~h, max, (s, TurnMore{sv.none(), False{}})))
3594 return l
3595
3596@unsafe
3597def loop(~h: Req -> IO(Res), +max: Nat, l: Listener) -> IO(Unit):
3598 do IO<Unit>:
3599 m : Listener & Result<&1, &1, U32 & String, Socket> <- TCP.accept(l)
3600 l2 : Listener <- conn(~h, max, m)
3601 loop(~h, max, l2)
3602
3603def serve.with(~h: Req -> IO(Res), +port: U32, +max: Nat) -> IO(Unit):
3604 do IO<Unit>:
3605 l : Listener <- IO.try(Listener, TCP.listen(port))
3606 IO.print("http://127.0.0.1:" ++ U32.show(port))
3607 loop(~h, max, l)
3608
3609def serve(~h: Req -> IO(Res), +port: U32) -> IO(Unit):
3610 serve.with(~h, port, serve.max())