http.bend
bend-kit-http@0.21.0.0 · 4,617 lines · 0 definitions
1# HTTP/1.1 and HTTP/2 client, with an HTTP/1.1 server. Source: https://github.com/paymog/bend-kit/tree/main/http
2import Base
3# By hash: bend-kit-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-http2@0.1.2.0/http2.bend as H2
6import bend-kit-http2@0.1.2.0/hpack.bend as Hpack
7import bend-kit-bytes@0.3.1.0/bytes.bend as HBytes
8import bend-kit-time@0.1.0.0/time.bend as Time
9import bend-kit-int@0.2.0.0/int.bend as Int
10import bend-kit-url@0.4.1.0/url.bend as Url
11import bend-kit-encoding@0.3.0.0/encoding.bend as Enc
12import bend-kit-json@0.5.0.1/json.bend as Json
13import bend-kit-bytes@0.3.0.0/bytes.bend as Bytes
14import bend-kit-dns@0.4.0.1/dns.bend as Dns
15import bend-kit-zlib@0.1.5.0/zlib.bend as Zlib
16
17# HTTP/1.1 codec and client (RFC 9112) for http:// and https:// (OpenSSL 3 at run time).
18# parse: start-line → field lines → blank → body length (§6.3); chunked (§7.1).
19# Bodies are Bytes. The String parsers below are the spec: one Char per octet.
20# fetch reads until frame() says the response is whole. It returns Result, not Maybe.
21# Build with -o for big bodies: the `bend file.bend` runner overflows on ~30 KB strings; native binaries do not.
22# import bend-kit-http@0.20.1.0/http.bend as Http
23
24type Req is Type:
25 Req{method: String, path: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
26
27type Res is Type:
28 Res{status: U32, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
29
30# The body type and its conversions, so a caller needs no bytes import.
31def Body() -> Type:
32 Bytes.Bytes
33
34# A byte string (one Char per octet) to a body, and back.
35def from_string(+s: String) -> Bytes.Bytes:
36 Bytes.from_string(s)
37
38def to_string(b: Bytes.Bytes) -> String:
39 Bytes.to_string(b)
40
41def length(b: Bytes.Bytes) -> Bytes.Bytes & U32:
42 Bytes.length(b)
43
44# Why fetch failed. Wire errors keep the errno and the text the effect already had.
45# ponytail: 60 and 110 are ETIMEDOUT on macOS and Linux. Windows is out of scope.
46type Err is Data:
47 ErrUrl{}
48 ErrDns{}
49 ErrConnect{code: U32, why: String}
50 ErrTls{code: U32, why: String}
51 ErrRead{code: U32, why: String}
52 ErrWrite{code: U32, why: String}
53 ErrTimeout{}
54 ErrRedirect{}
55 ErrBad{}
56
57def err.late(+code: U32) -> Bool:
58 Bool.or(U32.is_eq(code, 60), U32.is_eq(code, 110))
59
60def err.pick(e: Err, late: Bool) -> Err:
61 match late:
62 case True{}:
63 ErrTimeout{}
64 case False{}:
65 e
66
67def err.or_late(code: U32, e: Err) -> Err:
68 err.pick(e, err.late(code))
69
70type Fields is Data:
71 FieldsBad{}
72 FieldsOk{m: Map<&2, List<&2, String>>}
73
74# One list per field name, in arrival order. header() is the first value.
75# Set-Cookie is never joined. Encode writes one line per value.
76def empty() -> Map<&2, List<&2, String>>:
77 Map.new(&2, List<&2, String>)
78
79def fields.of(r: Map<&2, List<&2, String>> & List<&2, String>) -> List<&2, String>:
80 (h, xs) = r
81 xs
82
83def fields(+h: Map<&2, List<&2, String>>, k: String) -> List<&2, String>:
84 fields.of(Map.get(List<&2, String>, Nil{}, h, k))
85
86def header.first(xs: List<&2, String>) -> String:
87 match xs:
88 case Nil{}:
89 ""
90 case Con{v, t}:
91 v
92
93def header(+h: Map<&2, List<&2, String>>, k: String) -> String:
94 header.first(fields(h, k))
95
96def field.last(xs: List<&2, String>) -> String:
97 match xs:
98 case Nil{}:
99 ""
100 case Con{v, Nil{}}:
101 v
102 case Con{v, t}:
103 field.last(t)
104
105# Transfer-Encoding is a list; chunked, when present, is the last coding.
106def header.last(+h: Map<&2, List<&2, String>>, k: String) -> String:
107 field.last(fields(h, k))
108
109def snoc(xs: List<&2, String>, v: String) -> List<&2, String>:
110 match xs:
111 case Nil{}:
112 [v]
113 case Con{h, t}:
114 Con{h, snoc(t, v)}
115
116def set(m: Map<&2, List<&2, String>>, k: String, v: String) -> Map<&2, List<&2, String>>:
117 Map.set(&2, List<&2, String>, m, k, [v])
118
119def add(+m: Map<&2, List<&2, String>>, +k: String, v: String) -> Map<&2, List<&2, String>>:
120 Map.set(&2, List<&2, String>, m, k, snoc(fields(m, k), v))
121
122def sanitize.cons(ch: Char, rest: String, drop: Bool) -> String:
123 match drop:
124 case True{}:
125 rest
126 case False{}:
127 SCon{ch, rest}
128
129def sanitize(s: String) -> String:
130 match s:
131 case SNil{}:
132 SNil{}
133 case SCon{Chr{+c}, t}:
134 sanitize.cons(Chr{c}, sanitize(t), Bool.or(U32.is_eq(c, 13), U32.is_eq(c, 10)))
135
136def drop_cr.last.if(cr: Bool, c: U32) -> String:
137 match cr:
138 case True{}:
139 SNil{}
140 case False{}:
141 SCon{Chr{c}, SNil{}}
142
143def drop_cr.last(+c: U32) -> String:
144 drop_cr.last.if(U32.is_eq(c, 13), c)
145
146# prev is the char before s; it is kept unless it is a final CR.
147def drop_cr.go(s: String, prev: U32) -> String:
148 match s:
149 case SNil{}:
150 drop_cr.last(prev)
151 case SCon{Chr{c}, t}:
152 SCon{Chr{prev}, drop_cr.go(t, c)}
153
154def drop_cr(s: String) -> String:
155 match s:
156 case SNil{}:
157 SNil{}
158 case SCon{Chr{c}, t}:
159 drop_cr.go(t, c)
160
161# w holds the last four octets; a char past 255 clears it.
162def blank_end.go(s: String, w: U32) -> Bool:
163 match s:
164 case SNil{}:
165 U32.is_eq(w, 218762506)
166 case SCon{Chr{+c}, t}:
167 blank_end.go(t, Bool.pick(U32, U32.is_lt(c, 256), (w * 256 + c : U32), 0))
168
169# String.ends_with(s, "\r\n\r\n") in one pass, with no reversed copy.
170def blank_end(s: String) -> Bool:
171 blank_end.go(s, 0)
172
173def trim_end.cons(h: Char, r: String, space: Bool) -> String:
174 match r:
175 case SNil{}:
176 match space:
177 case True{}:
178 SNil{}
179 case False{}:
180 SCon{h, SNil{}}
181 case SCon{a, t}:
182 SCon{h, SCon{a, t}}
183
184# String.trim_end without the two reversed copies.
185def trim_end(s: String) -> String:
186 match s:
187 case SNil{}:
188 SNil{}
189 case SCon{+h, t}:
190 trim_end.cons(h, trim_end(t), Char.is_space(h))
191
192def trim(s: String) -> String:
193 trim_end(String.trim_start(s))
194
195# Bool.pick evaluates both arms; a split that recursed inside it would reverse acc at every byte.
196def take.cut(acc: String, rest: String) -> String & String:
197 (String.reverse(String.drop(acc, 1n)), rest)
198
199# hit: the last char pushed onto acc was the stop char.
200def take_sp.go(s: String, acc: String, hit: Bool) -> String & String:
201 match s:
202 case SNil{}:
203 match hit:
204 case True{}:
205 take.cut(acc, SNil{})
206 case False{}:
207 (String.reverse(acc), SNil{})
208 case SCon{Chr{+c}, t}:
209 match hit:
210 case True{}:
211 take.cut(acc, SCon{Chr{c}, t})
212 case False{}:
213 take_sp.go(t, SCon{Chr{c}, acc}, U32.is_eq(c, 32))
214
215def take_sp(s: String) -> String & String:
216 take_sp.go(s, SNil{}, False{})
217
218def start_line.ver(m: String, pv: String & String) -> String & String & String:
219 (p, v) = pv
220 (m, p, drop_cr(v))
221
222def start_line.rest(mr: String & String) -> String & String & String:
223 (m, r) = mr
224 start_line.ver(m, take_sp(r))
225
226def start_line(s: String) -> String & String & String:
227 start_line.rest(take_sp(s))
228
229def split_at_blank.go(s: String, e: Bool, w: U32, acc: String) -> String & String:
230 match s:
231 case SNil{}:
232 (String.reverse(acc), SNil{})
233 case SCon{Chr{+a}, t}:
234 match e:
235 case True{}:
236 (String.reverse(acc), SCon{Chr{a}, t})
237 case False{}:
238 +w2 = (w * 256 + a : U32)
239 split_at_blank.go(t, U32.is_eq(w2, 218762506), w2, SCon{Chr{a}, acc})
240
241# split_at_blank, plus whether the head ends in the blank line.
242def split_at_blank.flag.go(+raw: String, s: String, off: Nat, w: U32, e: Bool) -> String & String & Bool:
243 match s:
244 case SNil{}:
245 (String.take(raw, off), SNil{}, e)
246 case SCon{Chr{+a}, t}:
247 match e:
248 case True{}:
249 (String.take(raw, off), SCon{Chr{a}, t}, True{})
250 case False{}:
251 +w2 = (w * 256 + a : U32)
252 +off1 = (1n + off : Nat)
253 split_at_blank.flag.go(raw, t, off1, w2, U32.is_eq(w2, 218762506))
254
255def split_at_blank.pair(r: String & String & Bool) -> String & String:
256 (head, rest, whole) = r
257 (head, rest)
258
259def split_at_blank(+s: String) -> String & String:
260 split_at_blank.pair(split_at_blank.flag.go(s, s, 0n, 0, False{}))
261
262def split_colon.go(s: String, acc: String, hit: Bool) -> String & String:
263 match s:
264 case SNil{}:
265 match hit:
266 case True{}:
267 take.cut(acc, SNil{})
268 case False{}:
269 (String.reverse(acc), SNil{})
270 case SCon{Chr{+c}, t}:
271 match hit:
272 case True{}:
273 take.cut(acc, SCon{Chr{c}, t})
274 case False{}:
275 split_colon.go(t, SCon{Char.to_lower(Chr{c}), acc}, U32.is_eq(c, 58))
276
277def split_colon(+s: String) -> String & String:
278 split_colon.go(s, SNil{}, False{})
279
280def has_header.of(r: Map<&2, List<&2, String>> & Bool) -> Bool:
281 (h, b) = r
282 b
283
284def has_header(+h: Map<&2, List<&2, String>>, k: String) -> Bool:
285 has_header.of(Map.has(&2, List<&2, String>, h, k))
286
287def folded(+line: String) -> Bool:
288 Bool.or(String.starts_with(line, " "), String.starts_with(line, "\t"))
289
290def tracked(+k: String) -> Bool:
291 Bool.or(String.eq(k, "host"), String.eq(k, "content-length"))
292
293def fields_put.dup(m: Map<&2, List<&2, String>>, k: String, v: String, bad: Bool) -> Fields:
294 match bad:
295 case True{}:
296 FieldsBad{}
297 case False{}:
298 FieldsOk{add(m, k, v)}
299
300def fields_put.tracked(+m: Map<&2, List<&2, String>>, +k: String, v: String, t: Bool) -> Fields:
301 match t:
302 case True{}:
303 fields_put.dup(m, k, v, has_header(m, k))
304 case False{}:
305 FieldsOk{add(m, k, v)}
306
307def fields_put.key(+m: Map<&2, List<&2, String>>, +k: String, v: String) -> Fields:
308 fields_put.tracked(m, k, v, tracked(k))
309
310def fields_put.kv(m: Map<&2, List<&2, String>>, kv: String & String) -> Fields:
311 (k, v) = kv
312 fields_put.key(m, k, trim(v))
313
314def fields_put.fold(m: Map<&2, List<&2, String>>, line: String, fold: Bool) -> Fields:
315 match fold:
316 case True{}:
317 FieldsBad{}
318 case False{}:
319 fields_put.kv(m, split_colon(line))
320
321def fields_put.empty(m: Map<&2, List<&2, String>>, +line: String, e: Bool) -> Fields:
322 match e:
323 case True{}:
324 FieldsOk{m}
325 case False{}:
326 fields_put.fold(m, line, folded(line))
327
328def fields_put.ok(m: Map<&2, List<&2, String>>, +line: String) -> Fields:
329 fields_put.empty(m, line, String.is_empty(line))
330
331def fields_put(acc: Fields, line: String) -> Fields:
332 match acc:
333 case FieldsBad{}:
334 FieldsBad{}
335 case FieldsOk{m}:
336 fields_put.ok(m, line)
337
338def parse.headers.done(acc: Fields) -> Maybe<&2, Map<&2, List<&2, String>>>:
339 match acc:
340 case FieldsBad{}:
341 None{}
342 case FieldsOk{m}:
343 Some{m}
344
345def parse.headers(xs: List<&2, String>, acc: Fields) -> Maybe<&2, Map<&2, List<&2, String>>>:
346 match xs:
347 case Nil{}:
348 parse.headers.done(acc)
349 case Con{line, rest}:
350 parse.headers(rest, fields_put(acc, drop_cr(line)))
351
352def parse_u32.digit(+c: U32) -> Bool:
353 Bool.and(U32.is_le(48, c), U32.is_le(c, 57))
354
355def parse_u32.add(acc: U32, c: U32) -> U32:
356 (acc * 10 + (c - 48 : U32) : U32)
357
358def parse_u32.done(acc: U32, bad: Bool) -> Maybe<&2, U32>:
359 match bad:
360 case True{}:
361 None{}
362 case False{}:
363 Some{acc}
364
365def parse_u32.go(s: String, acc: U32, bad: Bool) -> Maybe<&2, U32>:
366 match s:
367 case SNil{}:
368 parse_u32.done(acc, bad)
369 case SCon{Chr{+c}, t}:
370 parse_u32.go(t, parse_u32.add(acc, c), Bool.or(bad, Bool.not(parse_u32.digit(c))))
371
372def parse_u32(s: String) -> Maybe<&2, U32>:
373 match s:
374 case SNil{}:
375 None{}
376 case SCon{Chr{+c}, t}:
377 parse_u32.go(t, parse_u32.add(0, c), Bool.not(parse_u32.digit(c)))
378
379# More: a valid prefix. Bad: cannot become a body. Body: a whole chunked body.
380type Hold is Data:
381 HoldMore{}
382 HoldBad{}
383 HoldBody{b: String}
384 HoldUntil{b: String}
385
386def is_hex(+c: U32) -> Bool:
387 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))))
388
389def hexv(+c: U32) -> U32:
390 Bool.pick(U32, parse_u32.digit(c), (c - 48 : U32), Bool.pick(U32, U32.is_le(c, 70), (c - 55 : U32), (c - 87 : U32)))
391
392# A chunked body decoder that reads each byte once, so a body fed in pieces
393# costs O(bytes) in total. Tr{j}: j bytes of the closing CRLF CRLF matched.
394type Dc is Data:
395 DcSize{acc: U32, seen: Bool}
396 DcExt{n: U32}
397 DcSizeLf{n: U32}
398 DcData{k: U32}
399 DcDataCr{}
400 DcDataLf{}
401 DcTr{j: U32}
402 DcDone{}
403 DcBad{}
404
405# st: where the decoder is. racc: the body so far, reversed. rest: bytes after a Done body.
406type Dco is Data:
407 Dco{st: Dc, racc: String, rest: String}
408
409def dc.start() -> Dc:
410 DcSize{0, False{}}
411
412def dc.size.semi(+n: U32, semi: Bool) -> Dc:
413 match semi:
414 case True{}:
415 DcExt{n}
416 case False{}:
417 DcBad{}
418
419def dc.size.cr(+n: U32, +c: U32, cr: Bool) -> Dc:
420 match cr:
421 case True{}:
422 DcSizeLf{n}
423 case False{}:
424 dc.size.semi(n, U32.is_eq(c, 59))
425
426def dc.size.end(+n: U32, +c: U32, seen: Bool) -> Dc:
427 match seen:
428 case False{}:
429 DcBad{}
430 case True{}:
431 dc.size.cr(n, c, U32.is_eq(c, 13))
432
433# A size that would overflow 32 bits ends the digits, and size.end then refuses it.
434def dc.size(+acc: U32, seen: Bool, +c: U32, digit: Bool) -> Dc:
435 match digit:
436 case True{}:
437 DcSize{(acc * 16 + hexv(c) : U32), True{}}
438 case False{}:
439 dc.size.end(acc, c, seen)
440
441# RFC 9112 §7.1.1: recipients ignore unknown chunk extensions; a bare LF is not CRLF.
442def dc.ext.lf(+n: U32, lf: Bool) -> Dc:
443 match lf:
444 case True{}:
445 DcBad{}
446 case False{}:
447 DcExt{n}
448
449def dc.ext(+n: U32, +c: U32, cr: Bool) -> Dc:
450 match cr:
451 case True{}:
452 DcSizeLf{n}
453 case False{}:
454 dc.ext.lf(n, U32.is_eq(c, 10))
455
456def dc.sized(+n: U32, zero: Bool) -> Dc:
457 match zero:
458 case True{}:
459 DcTr{2}
460 case False{}:
461 DcData{n}
462
463def dc.size.lf(+n: U32, lf: Bool) -> Dc:
464 match lf:
465 case True{}:
466 dc.sized(n, U32.is_eq(n, 0))
467 case False{}:
468 DcBad{}
469
470# k data bytes are left and m of them were just read.
471def dc.data(+k: U32, +m: U32) -> Dc:
472 Bool.pick(Dc, U32.is_le(k, m), DcDataCr{}, DcData{(k - m : U32)})
473
474def dc.pick(ok: Bool, next: Dc) -> Dc:
475 match ok:
476 case True{}:
477 next
478 case False{}:
479 DcBad{}
480
481# ponytail: trailer fields are dropped unparsed (§7.1.2 allows discarding)
482def dc.tr.hit(+j: U32) -> Dc:
483 Bool.pick(Dc, U32.is_eq(j, 3), DcDone{}, DcTr{(j + 1 : U32)})
484
485def dc.tr(+j: U32, +c: U32, hit: Bool) -> Dc:
486 match hit:
487 case True{}:
488 dc.tr.hit(j)
489 case False{}:
490 Bool.pick(Dc, U32.is_eq(c, 13), DcTr{1}, DcTr{0})
491
492def dc.tr.want(+j: U32) -> U32:
493 Bool.pick(U32, U32.is_eq(U32.mod(j, 2), 0), 13, 10)
494
495def dc.byte(h: Char) -> U32:
496 Chr{c} = h
497 c
498
499# One byte c. Done and Bad never look at it, and a data byte is not inspected.
500def dc.step(st: Dc, +c: U32) -> Dc:
501 match st:
502 case DcBad{}:
503 DcBad{}
504 case DcSize{+acc, seen}:
505 dc.size(acc, seen, c, Bool.and(is_hex(c), U32.is_le(acc, 268435455)))
506 case DcExt{+n}:
507 dc.ext(n, c, U32.is_eq(c, 13))
508 case DcSizeLf{+n}:
509 dc.size.lf(n, U32.is_eq(c, 10))
510 case DcDataCr{}:
511 dc.pick(U32.is_eq(c, 13), DcDataLf{})
512 case DcDataLf{}:
513 dc.pick(U32.is_eq(c, 10), dc.start())
514 case DcTr{+j}:
515 dc.tr(j, c, U32.is_eq(c, dc.tr.want(j)))
516 case DcData{+k}:
517 dc.data(k, 1)
518 case DcDone{}:
519 DcDone{}
520
521def dc.live(st: Dc) -> Bool:
522 match st:
523 case DcDone{}:
524 False{}
525 case DcBad{}:
526 False{}
527 case DcSize{a, b}:
528 True{}
529 case DcExt{n}:
530 True{}
531 case DcSizeLf{n}:
532 True{}
533 case DcData{k}:
534 True{}
535 case DcDataCr{}:
536 True{}
537 case DcDataLf{}:
538 True{}
539 case DcTr{j}:
540 True{}
541
542def dc.feed(s: String, st: Dc, racc: String) -> Dco:
543 match s:
544 case SNil{}:
545 Dco{st, racc, ""}
546 case SCon{h, t}:
547 match st:
548 case DcBad{}:
549 Dco{DcBad{}, racc, ""}
550 case DcDone{}:
551 Dco{DcDone{}, racc, SCon{h, t}}
552 case DcData{+k}:
553 dc.feed(t, dc.data(k, 1), SCon{h, racc})
554 case DcSize{+acc, seen}:
555 dc.feed(t, dc.step(DcSize{acc, seen}, dc.byte(h)), racc)
556 case DcExt{+n}:
557 dc.feed(t, dc.step(DcExt{n}, dc.byte(h)), racc)
558 case DcSizeLf{+n}:
559 dc.feed(t, dc.step(DcSizeLf{n}, dc.byte(h)), racc)
560 case DcDataCr{}:
561 dc.feed(t, dc.step(DcDataCr{}, dc.byte(h)), racc)
562 case DcDataLf{}:
563 dc.feed(t, dc.step(DcDataLf{}, dc.byte(h)), racc)
564 case DcTr{+j}:
565 dc.feed(t, dc.step(DcTr{j}, dc.byte(h)), racc)
566
567def chunk.hold(o: Dco) -> Hold:
568 Dco{st, racc, rest} = o
569 match st:
570 case DcDone{}:
571 HoldBody{String.reverse(racc)}
572 case DcBad{}:
573 HoldBad{}
574 case DcSize{a, b}:
575 HoldMore{}
576 case DcExt{n}:
577 HoldMore{}
578 case DcSizeLf{n}:
579 HoldMore{}
580 case DcData{k}:
581 HoldMore{}
582 case DcDataCr{}:
583 HoldMore{}
584 case DcDataLf{}:
585 HoldMore{}
586 case DcTr{j}:
587 HoldMore{}
588
589def chunk.live(s: String) -> Hold:
590 chunk.hold(dc.feed(s, dc.start(), ""))
591
592def chunk.rest(o: Dco) -> Maybe<&2, String>:
593 Dco{st, racc, rest} = o
594 match st:
595 case DcDone{}:
596 Some{rest}
597 case DcBad{}:
598 None{}
599 case DcSize{a, b}:
600 None{}
601 case DcExt{n}:
602 None{}
603 case DcSizeLf{n}:
604 None{}
605 case DcData{k}:
606 None{}
607 case DcDataCr{}:
608 None{}
609 case DcDataLf{}:
610 None{}
611 case DcTr{j}:
612 None{}
613
614def chunk.suffix(s: String) -> Maybe<&2, String>:
615 chunk.rest(dc.feed(s, dc.start(), ""))
616
617def chunk.decode.hold(h: Hold) -> Maybe<&2, String>:
618 match h:
619 case HoldMore{}:
620 None{}
621 case HoldBad{}:
622 None{}
623 case HoldUntil{b}:
624 None{}
625 case HoldBody{b}:
626 Some{b}
627
628def chunk.decode(s: String) -> Maybe<&2, String>:
629 chunk.decode.hold(chunk.live(s))
630
631def bytes.snd(r: Bytes.Bytes & Bytes.Bytes) -> Bytes.Bytes:
632 (a, b) = r
633 b
634
635def found.at(+from: U32, m: Maybe<&2, U32>) -> Maybe<&2, U32>:
636 match m:
637 case None{}:
638 None{}
639 case Some{+j}:
640 Some{(from + j : U32)}
641
642# A chunked body decoded from piece[i..]: a data run is sliced whole, and every other byte steps dc.
643type Cs is Type:
644 Cs{piece: Bytes.Bytes, i: U32, st: Dc, parts: List<&1, Bytes.Bytes>}
645
646# st: where the decoder stopped. parts: the data so far, newest first. rest: the bytes after a Done body.
647type Ck is Type:
648 Ck{st: Dc, parts: List<&1, Bytes.Bytes>, rest: Bytes.Bytes}
649
650def ck.next(+len: U32, +i: U32, +st: Dc, piece: Bytes.Bytes, parts: List<&1, Bytes.Bytes>) -> Bool & Cs:
651 (Bool.and(U32.is_lt(i, len), dc.live(st)), Cs{piece, i, st, parts})
652
653def ck.data(+len: U32, +i: U32, +k: U32, +m: U32, parts: List<&1, Bytes.Bytes>, r: Bytes.Bytes & Bytes.Bytes) -> Bool & Cs:
654 (piece, run) = r
655 ck.next(len, (i + m : U32), dc.data(k, m), piece, Con{run, parts})
656
657def ck.byte(+len: U32, +i: U32, st: Dc, parts: List<&1, Bytes.Bytes>, r: Bytes.Bytes & Maybe<&2, U32>) -> Bool & Cs:
658 (piece, m) = r
659 match m:
660 case None{}:
661 ck.next(len, i, DcBad{}, piece, parts)
662 case Some{+c}:
663 ck.next(len, (i + 1 : U32), dc.step(st, c), piece, parts)
664
665def ck.step(+len: U32, cs: Cs) -> Bool & Cs:
666 Cs{piece, +i, st, parts} = cs
667 match st:
668 case DcData{+k}:
669 +m = U32.min(k, (len - i : U32))
670 ck.data(len, i, k, m, parts, Bytes.slice(piece, i, m))
671 case DcDone{}:
672 (False{}, Cs{piece, i, DcDone{}, parts})
673 case DcBad{}:
674 (False{}, Cs{piece, i, DcBad{}, parts})
675 case DcSize{+acc, seen}:
676 ck.byte(len, i, DcSize{acc, seen}, parts, Bytes.get(piece, i))
677 case DcExt{+n}:
678 ck.byte(len, i, DcExt{n}, parts, Bytes.get(piece, i))
679 case DcSizeLf{+n}:
680 ck.byte(len, i, DcSizeLf{n}, parts, Bytes.get(piece, i))
681 case DcDataCr{}:
682 ck.byte(len, i, DcDataCr{}, parts, Bytes.get(piece, i))
683 case DcDataLf{}:
684 ck.byte(len, i, DcDataLf{}, parts, Bytes.get(piece, i))
685 case DcTr{+j}:
686 ck.byte(len, i, DcTr{j}, parts, Bytes.get(piece, i))
687
688def ck.rest(st: Dc, parts: List<&1, Bytes.Bytes>, r: Bytes.Bytes & Bytes.Bytes) -> Ck:
689 (piece, rest) = r
690 Ck{st, parts, rest}
691
692def ck.end(+len: U32, cs: Cs) -> Ck:
693 Cs{piece, +i, st, parts} = cs
694 ck.rest(st, parts, Bytes.slice(piece, i, (len - i : U32)))
695
696# Each step reads at least one byte, so len steps are enough.
697def ck.feed(f: Nat, +len: U32, r: Bool & Cs) -> Ck:
698 match f:
699 case 0n:
700 (go, cs) = r
701 ck.end(len, cs)
702 case 1n+p:
703 (go, cs) = r
704 match go:
705 case False{}:
706 ck.end(len, cs)
707 case True{}:
708 ck.feed(p, len, ck.step(len, cs))
709
710def ck(piece: Bytes.Bytes, +st: Dc, parts: List<&1, Bytes.Bytes>) -> Ck:
711 Bytes.Bytes{+len, buf} = piece
712 ck.feed(U32.to_nat(len), len, ck.next(len, 0, st, Bytes.Bytes{len, buf}, parts))
713
714def parse.res.cl.have(+rest: String, +k: Nat, short: Bool) -> Hold:
715 match short:
716 case True{}:
717 HoldMore{}
718 case False{}:
719 HoldBody{String.take(rest, k)}
720
721def parse.res.cl.k(+rest: String, +k: Nat) -> Hold:
722 parse.res.cl.have(rest, k, Nat.is_lt(String.length(rest), k))
723
724def parse.res.cl.n(rest: String, n: Maybe<&2, U32>) -> Hold:
725 match n:
726 case None{}:
727 HoldBad{}
728 case Some{k}:
729 parse.res.cl.k(rest, U32.to_nat(k))
730
731def parse.body.cl(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
732 match hascl:
733 case False{}:
734 HoldBody{""}
735 case True{}:
736 parse.res.cl.n(rest, parse_u32(header(h, "content-length")))
737
738# RFC 9112 §6.3 (4): a request coding other than chunked cannot be framed.
739def parse.body.chunked.eq(rest: String, ok: Bool) -> Hold:
740 match ok:
741 case False{}:
742 HoldBad{}
743 case True{}:
744 chunk.live(rest)
745
746def parse.body.chunked.val(te: String, rest: String) -> Hold:
747 parse.body.chunked.eq(rest, String.eq(String.to_lower(te), "chunked"))
748
749def parse.body.chunked(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
750 match hascl:
751 case True{}:
752 HoldBad{}
753 case False{}:
754 parse.body.chunked.val(header.last(h, "transfer-encoding"), rest)
755
756def parse.body.te(+h: Map<&2, List<&2, String>>, rest: String, te: Bool) -> Hold:
757 match te:
758 case True{}:
759 parse.body.chunked(h, rest, has_header(h, "content-length"))
760 case False{}:
761 parse.body.cl(h, rest, has_header(h, "content-length"))
762
763def parse.body(+h: Map<&2, List<&2, String>>, rest: String) -> Hold:
764 parse.body.te(h, rest, has_header(h, "transfer-encoding"))
765
766# Bad: never a request. More: the head is not whole; read on. Head: the head is whole
767# and valid, and the body is still coming (req.body is empty). Req: a whole request.
768type Got is Type:
769 GotBad{}
770 GotMore{}
771 GotHead{req: Req}
772 GotReq{req: Req}
773
774def parse.finish(method: String, path: String, h: Map<&2, List<&2, String>>, body: Hold) -> Got:
775 match body:
776 case HoldBad{}:
777 GotBad{}
778 case HoldMore{}:
779 GotHead{Req{method, path, h, Bytes.new(0)}}
780 case HoldUntil{b}:
781 GotBad{}
782 case HoldBody{b}:
783 GotReq{Req{method, path, h, Bytes.from_string(b)}}
784
785def parse.host(method: String, path: String, +h: Map<&2, List<&2, String>>, rest: String, has: Bool) -> Got:
786 match has:
787 case False{}:
788 GotBad{}
789 case True{}:
790 parse.finish(method, path, h, parse.body(h, rest))
791
792# RFC 9112 §3.2: only HTTP/1.1 requires Host.
793def parse.fields(method: String, path: String, rest: String, v11: Bool, fs: Maybe<&2, Map<&2, List<&2, String>>>) -> Got:
794 match fs:
795 case None{}:
796 GotBad{}
797 case Some{+h}:
798 parse.host(method, path, h, rest, Bool.or(Bool.not(v11), has_header(h, "host")))
799
800def target_ok(+p: String) -> Bool:
801 Bool.or(String.starts_with(p, "/"), Bool.or(String.eq(p, "*"), String.starts_with(p, "http://")))
802
803def parse.target(method: String, +path: String, headers: List<&2, String>, rest: String, v11: Bool, ok: Bool) -> Got:
804 match ok:
805 case False{}:
806 GotBad{}
807 case True{}:
808 parse.fields(method, path, rest, v11, parse.headers(headers, FieldsOk{empty()}))
809
810def parse.ver(method: String, +path: String, +v: String, headers: List<&2, String>, rest: String, ok: Bool) -> Got:
811 match ok:
812 case False{}:
813 GotBad{}
814 case True{}:
815 parse.target(method, path, headers, rest, String.eq(v, "HTTP/1.1"), target_ok(path))
816
817def parse.empty_method(method: String, path: String, +v: String, headers: List<&2, String>, rest: String, empty: Bool) -> Got:
818 match empty:
819 case True{}:
820 GotBad{}
821 case False{}:
822 parse.ver(method, path, v, headers, rest, Bool.or(String.eq(v, "HTTP/1.1"), String.eq(v, "HTTP/1.0")))
823
824def parse.start3(mpv: String & String & String, headers: List<&2, String>, rest: String) -> Got:
825 (+method, path, v) = mpv
826 parse.empty_method(method, path, v, headers, rest, String.is_empty(method))
827
828def parse.lines(xs: List<&2, String>, rest: String) -> Got:
829 match xs:
830 case Nil{}:
831 GotBad{}
832 case Con{line, headers}:
833 parse.start3(start_line(line), headers, rest)
834
835
836def parse.head(+head: String, rest: String, whole: Bool) -> Got:
837 match whole:
838 case False{}:
839 GotMore{}
840 case True{}:
841 parse.lines(String.lines(head), rest)
842
843def parse.of(hb: String & String & Bool) -> Got:
844 (head, rest, whole) = hb
845 parse.head(head, rest, whole)
846
847# serve reads until this is not GotMore.
848def parse.got(+raw: String) -> Got:
849 parse.of(split_at_blank.flag.go(raw, raw, 0n, 0, False{}))
850
851
852def parse.req(g: Got) -> Maybe<&1, Req>:
853 match g:
854 case GotReq{req}:
855 Some{req}
856 case GotBad{}:
857 None{}
858 case GotMore{}:
859 None{}
860 case GotHead{req}:
861 None{}
862
863def parse(raw: String) -> Maybe<&1, Req>:
864 parse.req(parse.got(raw))
865
866def parse.res.cl(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
867 match hascl:
868 case False{}:
869 HoldBody{rest}
870 case True{}:
871 parse.res.cl.n(rest, parse_u32(header(h, "content-length")))
872
873def parse.res.chunked.eq(rest: String, ok: Bool) -> Hold:
874 match ok:
875 case False{}:
876 HoldUntil{rest}
877 case True{}:
878 chunk.live(rest)
879
880def parse.res.chunked.val(te: String, rest: String) -> Hold:
881 parse.res.chunked.eq(rest, String.eq(String.to_lower(te), "chunked"))
882
883def parse.res.chunked(+h: Map<&2, List<&2, String>>, rest: String, hascl: Bool) -> Hold:
884 match hascl:
885 case True{}:
886 HoldBad{}
887 case False{}:
888 parse.res.chunked.val(header.last(h, "transfer-encoding"), rest)
889
890def parse.res.te(+h: Map<&2, List<&2, String>>, rest: String, te: Bool) -> Hold:
891 match te:
892 case True{}:
893 parse.res.chunked(h, rest, has_header(h, "content-length"))
894 case False{}:
895 parse.res.cl(h, rest, has_header(h, "content-length"))
896
897def parse.res.body(+h: Map<&2, List<&2, String>>, rest: String) -> Hold:
898 parse.res.te(h, rest, has_header(h, "transfer-encoding"))
899
900# Bad: never a message. More: a valid prefix; read on. Done: a whole response.
901type Frame is Type:
902 FrameBad{}
903 FrameMore{}
904 FrameDone{res: Res}
905
906# RFC 9112 §8: a message cut short by close is incomplete, not valid.
907def frame.cut(closed: Bool) -> Frame:
908 match closed:
909 case True{}:
910 FrameBad{}
911 case False{}:
912 FrameMore{}
913
914def frame.wait(res: Res, wait: Bool) -> Frame:
915 match wait:
916 case True{}:
917 FrameMore{}
918 case False{}:
919 FrameDone{res}
920
921def frame.done(status: U32, h: Map<&2, List<&2, String>>, body: Hold, +closed: Bool, open: Bool) -> Frame:
922 match body:
923 case HoldBad{}:
924 FrameBad{}
925 case HoldMore{}:
926 frame.cut(closed)
927 case HoldUntil{b}:
928 frame.wait(Res{status, h, Bytes.from_string(b)}, Bool.not(closed))
929 case HoldBody{b}:
930 frame.wait(Res{status, h, Bytes.from_string(b)}, Bool.and(open, Bool.not(closed)))
931
932# RFC 9112 §6.3 (8): no TE and no CL ⇒ the body runs until the server closes.
933def frame.open(+h: Map<&2, List<&2, String>>) -> Bool:
934 Bool.not(Bool.or(has_header(h, "transfer-encoding"), has_header(h, "content-length")))
935
936# RFC 9112 §6.3 (1): HEAD, 1xx, 204 and 304 responses end at the blank line.
937def frame.nobody(+status: U32, head: Bool) -> Bool:
938 Bool.or(head, Bool.or(U32.is_lt(status, 200), Bool.or(U32.is_eq(status, 204), U32.is_eq(status, 304))))
939
940# 101 is the final response. Other 1xx are interim; a final response follows.
941def frame.interim(+status: U32) -> Bool:
942 Bool.and(U32.is_lt(status, 200), Bool.not(U32.is_eq(status, 101)))
943
944def frame.status(status: U32, +h: Map<&2, List<&2, String>>, rest: String, closed: Bool, nobody: Bool) -> Frame:
945 match nobody:
946 case True{}:
947 FrameDone{Res{status, h, Bytes.new(0)}}
948 case False{}:
949 frame.done(status, h, parse.res.body(h, rest), closed, frame.open(h))
950
951def parse.res.fields(+status: U32, rest: String, fs: Maybe<&2, Map<&2, List<&2, String>>>, closed: Bool, head: Bool) -> Frame:
952 match fs:
953 case None{}:
954 FrameBad{}
955 case Some{h}:
956 frame.status(status, h, rest, closed, frame.nobody(status, head))
957
958def parse.res.num(code: Maybe<&2, U32>, headers: List<&2, String>, rest: String, closed: Bool, head: Bool) -> Frame:
959 match code:
960 case None{}:
961 FrameBad{}
962 case Some{n}:
963 parse.res.fields(n, rest, parse.headers(headers, FieldsOk{empty()}), closed, head)
964
965def parse.res.ver(code: String, headers: List<&2, String>, rest: String, closed: Bool, head: Bool, ok: Bool) -> Frame:
966 match ok:
967 case False{}:
968 FrameBad{}
969 case True{}:
970 parse.res.num(parse_u32(code), headers, rest, closed, head)
971
972def parse.res.start3(mpv: String & String & String, headers: List<&2, String>, rest: String, closed: Bool, head: Bool) -> Frame:
973 (+ver, code, reason) = mpv
974 parse.res.ver(code, headers, rest, closed, head, Bool.or(String.eq(ver, "HTTP/1.1"), String.eq(ver, "HTTP/1.0")))
975
976def parse.res.lines(xs: List<&2, String>, rest: String, closed: Bool, head: Bool) -> Frame:
977 match xs:
978 case Nil{}:
979 FrameBad{}
980 case Con{line, headers}:
981 parse.res.start3(start_line(line), headers, rest, closed, head)
982
983def parse.res.blank(hd: String, rest: String, +closed: Bool, head: Bool, ok: Bool) -> Frame:
984 match ok:
985 case False{}:
986 frame.cut(closed)
987 case True{}:
988 parse.res.lines(String.lines(hd), rest, closed, head)
989
990def parse.res.of(hb: String & String, closed: Bool, head: Bool) -> Frame:
991 (+hd, rest) = hb
992 parse.res.blank(hd, rest, closed, head, blank_end(hd))
993
994type Lead is Data:
995 LeadCut{}
996 LeadFinal{}
997 LeadSkip{+rest: String}
998
999def frame.lead.if(rest: String, interim: Bool) -> Lead:
1000 match interim:
1001 case True{}:
1002 LeadSkip{rest}
1003 case False{}:
1004 LeadFinal{}
1005
1006def frame.lead.num(n: Maybe<&2, U32>, rest: String) -> Lead:
1007 match n:
1008 case None{}:
1009 LeadFinal{}
1010 case Some{s}:
1011 frame.lead.if(rest, frame.interim(s))
1012
1013def frame.lead.code(mpv: String & String & String, rest: String) -> Lead:
1014 (ver, code, reason) = mpv
1015 frame.lead.num(parse_u32(code), rest)
1016
1017def frame.lead.lines(xs: List<&2, String>, rest: String) -> Lead:
1018 match xs:
1019 case Nil{}:
1020 LeadFinal{}
1021 case Con{line, headers}:
1022 frame.lead.code(start_line(line), rest)
1023
1024def frame.lead.blank(+hd: String, rest: String, ok: Bool) -> Lead:
1025 match ok:
1026 case False{}:
1027 LeadCut{}
1028 case True{}:
1029 frame.lead.lines(String.lines(hd), rest)
1030
1031def frame.lead(hb: String & String) -> Lead:
1032 (+hd, rest) = hb
1033 frame.lead.blank(hd, rest, blank_end(hd))
1034
1035def frame.at.cont(+raw: String, lead: Lead) -> String:
1036 match lead:
1037 case LeadCut{}:
1038 raw
1039 case LeadFinal{}:
1040 raw
1041 case LeadSkip{rest}:
1042 rest
1043
1044def frame.at.zero.go(+raw: String, closed: Bool, head: Bool, lead: Lead) -> Frame:
1045 match lead:
1046 case LeadCut{}:
1047 frame.cut(closed)
1048 case LeadFinal{}:
1049 parse.res.of(split_at_blank(raw), closed, head)
1050 case LeadSkip{rest}:
1051 FrameBad{}
1052
1053def frame.at.zero.of(+raw: String, closed: Bool, head: Bool) -> Frame:
1054 frame.at.zero.go(raw, closed, head, frame.lead(split_at_blank(raw)))
1055
1056def frame.at.pos.do(f: Nat, +raw: String, closed: Bool, head: Bool, hb: String & String, lead: Lead) -> Frame:
1057 match f:
1058 case 0n:
1059 match lead:
1060 case LeadCut{}:
1061 frame.cut(closed)
1062 case LeadFinal{}:
1063 parse.res.of(hb, closed, head)
1064 case LeadSkip{+rest}:
1065 frame.at.zero.of(rest, closed, head)
1066 case 1n+g:
1067 match lead:
1068 case LeadCut{}:
1069 frame.cut(closed)
1070 case LeadFinal{}:
1071 parse.res.of(hb, closed, head)
1072 case LeadSkip{+rest}:
1073 frame.at.pos.do(g, rest, closed, head, split_at_blank(rest), frame.lead(split_at_blank(rest)))
1074
1075def frame.at.zero(+raw: String, closed: Bool, head: Bool) -> Frame:
1076 frame.at.zero.of(raw, closed, head)
1077
1078# ponytail: 8 interim responses; raise the fuel if a server sends more
1079def frame.at(fuel: Nat, +raw: String, closed: Bool, head: Bool) -> Frame:
1080 match fuel:
1081 case 0n:
1082 frame.at.zero(raw, closed, head)
1083 case 1n+f:
1084 frame.at.pos.do(f, raw, closed, head, split_at_blank(raw), frame.lead(split_at_blank(raw)))
1085
1086# frame(bytes so far, server closed?, request was HEAD?)
1087def frame(raw: String, closed: Bool, head: Bool) -> Frame:
1088 frame.at(8n, raw, closed, head)
1089
1090def frame.res(f: Frame) -> Maybe<&1, Res>:
1091 match f:
1092 case FrameDone{res}:
1093 Some{res}
1094 case FrameBad{}:
1095 None{}
1096 case FrameMore{}:
1097 None{}
1098
1099def parse_res(raw: String) -> Maybe<&1, Res>:
1100 frame.res(frame(raw, True{}, False{}))
1101
1102def res_fields.res(res: Res, k: String) -> List<&2, String>:
1103 Res{status, headers, body} = res
1104 fields(headers, k)
1105
1106def res_fields(m: Maybe<&1, Res>, k: String) -> List<&2, String>:
1107 match m:
1108 case None{}:
1109 Nil{}
1110 case Some{res}:
1111 res_fields.res(res, k)
1112
1113# The response body as it arrives. Len: bytes left. Chunk: the decoder. Close: until the
1114# server closes. Done: the body is whole. Bad: it cannot become a body.
1115type Rb is Data:
1116 RbLen{left: U32}
1117 RbChunk{st: Dc}
1118 RbClose{}
1119 RbDone{}
1120 RbBad{}
1121
1122def rb.cl(n: Maybe<&2, U32>) -> Maybe<&2, Rb>:
1123 match n:
1124 case None{}:
1125 None{}
1126 case Some{+k}:
1127 Some{Bool.pick(Rb, U32.is_zero(k), RbDone{}, RbLen{k})}
1128
1129def rb.te(+h: Map<&2, List<&2, String>>, cl: Bool) -> Maybe<&2, Rb>:
1130 match cl:
1131 case True{}:
1132 None{}
1133 case False{}:
1134 Some{Bool.pick(Rb, String.eq(String.to_lower(header.last(h, "transfer-encoding")), "chunked"), RbChunk{dc.start()}, RbClose{})}
1135
1136def rb.len(+h: Map<&2, List<&2, String>>, te: Bool) -> Maybe<&2, Rb>:
1137 match te:
1138 case True{}:
1139 rb.te(h, has_header(h, "content-length"))
1140 case False{}:
1141 Bool.pick(Maybe<&2, Rb>, has_header(h, "content-length"), rb.cl(parse_u32(header(h, "content-length"))), Some{RbClose{}})
1142
1143# RFC 9112 §6.3: how the body of this response ends. None: it cannot be framed.
1144def rb.of(+h: Map<&2, List<&2, String>>, nobody: Bool) -> Maybe<&2, Rb>:
1145 match nobody:
1146 case True{}:
1147 Some{RbDone{}}
1148 case False{}:
1149 rb.len(h, has_header(h, "transfer-encoding"))
1150
1151# rb: how the body goes on. parts: body bytes so far, newest first. rest: bytes past a Done body.
1152type Bf is Type:
1153 Bf{rb: Rb, parts: List<&1, Bytes.Bytes>, rest: Bytes.Bytes}
1154
1155def rb.len.cut(parts: List<&1, Bytes.Bytes>, +len: U32, +left: U32, r: Bytes.Bytes & Bytes.Bytes) -> Bf:
1156 (piece, data) = r
1157 Bf{RbDone{}, Con{data, parts}, bytes.snd(Bytes.slice(piece, left, (len - left : U32)))}
1158
1159def rb.len.have(short: Bool, +left: U32, parts: List<&1, Bytes.Bytes>, +len: U32, piece: Bytes.Bytes) -> Bf:
1160 match short:
1161 case True{}:
1162 Bf{RbLen{(left - len : U32)}, Con{piece, parts}, Bytes.new(0)}
1163 case False{}:
1164 rb.len.cut(parts, len, left, Bytes.slice(piece, 0, left))
1165
1166def rb.chunk(c: Ck) -> Bf:
1167 Ck{st, parts, rest} = c
1168 match st:
1169 case DcDone{}:
1170 Bf{RbDone{}, parts, rest}
1171 case DcBad{}:
1172 Bf{RbBad{}, parts, rest}
1173 case DcSize{a, b}:
1174 Bf{RbChunk{DcSize{a, b}}, parts, rest}
1175 case DcExt{x}:
1176 Bf{RbChunk{DcExt{x}}, parts, rest}
1177 case DcSizeLf{x}:
1178 Bf{RbChunk{DcSizeLf{x}}, parts, rest}
1179 case DcData{k}:
1180 Bf{RbChunk{DcData{k}}, parts, rest}
1181 case DcDataCr{}:
1182 Bf{RbChunk{DcDataCr{}}, parts, rest}
1183 case DcDataLf{}:
1184 Bf{RbChunk{DcDataLf{}}, parts, rest}
1185 case DcTr{j}:
1186 Bf{RbChunk{DcTr{j}}, parts, rest}
1187
1188# The body bytes in piece, added to parts.
1189def rb.feed(rb: Rb, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Bf:
1190 match rb:
1191 case RbLen{+left}:
1192 Bytes.Bytes{+len, buf} = piece
1193 rb.len.have(U32.is_lt(len, left), left, parts, len, Bytes.Bytes{len, buf})
1194 case RbChunk{st}:
1195 rb.chunk(ck(piece, st, parts))
1196 case RbClose{}:
1197 Bf{RbClose{}, Con{piece, parts}, Bytes.new(0)}
1198 case RbDone{}:
1199 Bf{RbDone{}, parts, piece}
1200 case RbBad{}:
1201 Bf{RbBad{}, parts, piece}
1202
1203# RFC 9112 §8: only a close-delimited body may end at close.
1204def rb.eof(rb: Rb) -> Bool:
1205 match rb:
1206 case RbClose{}:
1207 True{}
1208 case RbDone{}:
1209 True{}
1210 case RbLen{n}:
1211 False{}
1212 case RbChunk{st}:
1213 False{}
1214 case RbBad{}:
1215 False{}
1216
1217def rb.body(parts: List<&1, Bytes.Bytes>) -> Bytes.Bytes:
1218 Bytes.concat(List.reverse(&1, Bytes.Bytes, parts))
1219
1220# The head scan. Seek: look for the blank line from byte from; k interim heads are behind.
1221# Wait: no blank line yet. Res: the final head, how its body ends, and the bytes after it.
1222type Hs is Type:
1223 HsSeek{buf: Bytes.Bytes, from: U32, k: U32}
1224 HsWait{buf: Bytes.Bytes, k: U32}
1225 HsBad{}
1226 HsRes{res: Res, rb: Rb, rest: Bytes.Bytes}
1227
1228def hs.final(+status: U32, +h: Map<&2, List<&2, String>>, rest: Bytes.Bytes, m: Maybe<&2, Rb>) -> Hs:
1229 match m:
1230 case None{}:
1231 HsBad{}
1232 case Some{rb}:
1233 HsRes{Res{status, h, Bytes.new(0)}, rb, rest}
1234
1235def hs.skip(more: Bool, +k: U32, rest: Bytes.Bytes) -> Hs:
1236 match more:
1237 case True{}:
1238 HsSeek{rest, 0, (k + 1 : U32)}
1239 case False{}:
1240 HsBad{}
1241
1242def hs.pick(interim: Bool, +head: Bool, +k: U32, +status: U32, +h: Map<&2, List<&2, String>>, rest: Bytes.Bytes) -> Hs:
1243 match interim:
1244 case True{}:
1245 hs.skip(U32.is_lt(k, 8), k, rest)
1246 case False{}:
1247 hs.final(status, h, rest, rb.of(h, frame.nobody(status, head)))
1248
1249def hs.res(+head: Bool, +k: U32, rest: Bytes.Bytes, res: Res) -> Hs:
1250 Res{+status, +h, body} = res
1251 hs.pick(frame.interim(status), head, k, status, h, rest)
1252
1253# The head alone, framed as a HEAD response so it stops at the blank line.
1254def hs.parsed(+head: Bool, +k: U32, rest: Bytes.Bytes, f: Frame) -> Hs:
1255 match f:
1256 case FrameDone{res}:
1257 hs.res(head, k, rest, res)
1258 case FrameBad{}:
1259 HsBad{}
1260 case FrameMore{}:
1261 HsBad{}
1262
1263def hs.split(+head: Bool, +k: U32, +hlen: U32, +len: U32, r: Bytes.Bytes & Bytes.Bytes) -> Hs:
1264 (buf, hb) = r
1265 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{}))
1266
1267def hs.hit(+head: Bool, +k: U32, +len: U32, buf: Bytes.Bytes, at: Maybe<&2, U32>) -> Hs:
1268 match at:
1269 case None{}:
1270 HsWait{buf, k}
1271 case Some{+i}:
1272 +hlen = (i + 4 : U32)
1273 hs.split(head, k, hlen, len, Bytes.slice(buf, 0, hlen))
1274
1275def hs.seek.of(+head: Bool, +k: U32, +len: U32, +from: U32, buf: Bytes.Bytes, r: Bytes.Bytes & Maybe<&2, U32>) -> Hs:
1276 (tail, m) = r
1277 hs.hit(head, k, len, buf, found.at(from, m))
1278
1279def hs.seek(+head: Bool, +k: U32, +len: U32, +from: U32, r: Bytes.Bytes & Bytes.Bytes) -> Hs:
1280 (buf, tail) = r
1281 hs.seek.of(head, k, len, from, buf, Bytes.find(tail, "\r\n\r\n"))
1282
1283def hs.step(+head: Bool, st: Hs) -> Hs:
1284 match st:
1285 case HsSeek{buf, +from, +k}:
1286 Bytes.Bytes{+len, b} = buf
1287 hs.seek(head, k, len, from, Bytes.slice(Bytes.Bytes{len, b}, from, (len - from : U32)))
1288 case HsWait{buf, k}:
1289 HsWait{buf, k}
1290 case HsBad{}:
1291 HsBad{}
1292 case HsRes{res, rb, rest}:
1293 HsRes{res, rb, rest}
1294
1295# Each step ends the scan or passes one interim head, and at most 8 interim heads pass.
1296def hs.scan(fuel: Nat, +head: Bool, st: Hs) -> Hs:
1297 match fuel:
1298 case 0n:
1299 match st:
1300 case HsSeek{buf, from, k}:
1301 HsBad{}
1302 case HsWait{buf, k}:
1303 HsWait{buf, k}
1304 case HsBad{}:
1305 HsBad{}
1306 case HsRes{res, rb, rest}:
1307 HsRes{res, rb, rest}
1308 case 1n+f:
1309 hs.scan(f, head, hs.step(head, st))
1310
1311# piece joins buf; only the new bytes, and the 3 before them, can finish the blank line.
1312def hs.more(+head: Bool, +k: U32, buf: Bytes.Bytes, piece: Bytes.Bytes) -> Hs:
1313 Bytes.Bytes{+ol, ob} = buf
1314 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})
1315
1316# Untrusted servers must not grow the buffer without bound.
1317def fetch.max() -> Nat:
1318 U32.to_nat(16777216)
1319
1320# A response read in pieces. Head: the head is not whole yet. Body: it is, and parts is the body so far.
1321# Len: a Content-Length body in one buffer of that size, with left bytes still to come.
1322type Rv is Type:
1323 RvHead{buf: Bytes.Bytes, k: U32}
1324 RvBody{res: Res, rb: Rb, parts: List<&1, Bytes.Bytes>}
1325 RvLen{res: Res, left: U32, body: Bytes.Bytes}
1326
1327# More: read on. Done: the response, and the bytes after it when the body is self-delimited.
1328type Rt is Type:
1329 RtMore{rv: Rv}
1330 RtBad{}
1331 RtDone{res: Res, rest: Maybe<&1, Bytes.Bytes>}
1332
1333def rv.start() -> Rv:
1334 RvHead{Bytes.new(0), 0}
1335
1336def rv.whole(res: Res, b: Bytes.Bytes, rest: Maybe<&1, Bytes.Bytes>) -> Rt:
1337 Res{status, headers, body} = res
1338 RtDone{Res{status, headers, b}, rest}
1339
1340def rv.done(res: Res, parts: List<&1, Bytes.Bytes>, rest: Maybe<&1, Bytes.Bytes>) -> Rt:
1341 rv.whole(res, rb.body(parts), rest)
1342
1343def rl.put.of(+total: U32, +len: U32, r: Array<U32> & Array<U32>) -> Bytes.Bytes & Bytes.Bytes:
1344 (src, dst) = r
1345 (Bytes.Bytes{total, dst}, Bytes.Bytes{len, src})
1346
1347# The first m bytes of piece, written into body after the total - left bytes already there.
1348def rl.put(+m: U32, +left: U32, body: Bytes.Bytes, piece: Bytes.Bytes) -> Bytes.Bytes & Bytes.Bytes:
1349 Bytes.Bytes{+total, dst} = body
1350 Bytes.Bytes{+len, src} = piece
1351 rl.put.of(total, len, Bytes.copy(m, src, dst, 0, (total - left : U32)))
1352
1353def rl.fed(short: Bool, res: Res, +left: U32, +len: U32, r: Bytes.Bytes & Bytes.Bytes) -> Rt:
1354 match short:
1355 case True{}:
1356 (body, piece) = r
1357 RtMore{RvLen{res, (left - len : U32), body}}
1358 case False{}:
1359 (body, piece) = r
1360 rv.whole(res, body, Some{bytes.snd(Bytes.slice(piece, left, (len - left : U32)))})
1361
1362def rl.feed(res: Res, +left: U32, body: Bytes.Bytes, piece: Bytes.Bytes) -> Rt:
1363 Bytes.Bytes{+len, buf} = piece
1364 rl.fed(U32.is_lt(len, left), res, left, len, rl.put(U32.min(len, left), left, body, Bytes.Bytes{len, buf}))
1365
1366def rv.fed(res: Res, bf: Bf) -> Rt:
1367 Bf{rb, parts, rest} = bf
1368 match rb:
1369 case RbDone{}:
1370 rv.done(res, parts, Some{rest})
1371 case RbBad{}:
1372 RtBad{}
1373 case RbLen{n}:
1374 RtMore{RvBody{res, RbLen{n}, parts}}
1375 case RbChunk{st}:
1376 RtMore{RvBody{res, RbChunk{st}, parts}}
1377 case RbClose{}:
1378 RtMore{RvBody{res, RbClose{}, parts}}
1379
1380# Some{left}: a Content-Length body small enough to allocate up front. Larger ones fail at the fetch cap.
1381def rb.buf(rb: Rb) -> Maybe<&2, U32>:
1382 match rb:
1383 case RbLen{+left}:
1384 Bool.pick(Maybe<&2, U32>, Nat.is_lt(fetch.max(), U32.to_nat(left)), None{}, Some{left})
1385 case RbChunk{st}:
1386 None{}
1387 case RbClose{}:
1388 None{}
1389 case RbDone{}:
1390 None{}
1391 case RbBad{}:
1392 None{}
1393
1394def rv.body(m: Maybe<&2, U32>, res: Res, rb: Rb, rest: Bytes.Bytes) -> Rt:
1395 match m:
1396 case None{}:
1397 rv.fed(res, rb.feed(rb, Nil{}, rest))
1398 case Some{+left}:
1399 rl.feed(res, left, Bytes.new(left), rest)
1400
1401def rv.head(hs: Hs) -> Rt:
1402 match hs:
1403 case HsWait{buf, k}:
1404 RtMore{RvHead{buf, k}}
1405 case HsBad{}:
1406 RtBad{}
1407 case HsSeek{buf, from, k}:
1408 RtBad{}
1409 case HsRes{res, +rb, rest}:
1410 rv.body(rb.buf(rb), res, rb, rest)
1411
1412def rv.eof(res: Res, parts: List<&1, Bytes.Bytes>, ok: Bool) -> Rt:
1413 match ok:
1414 case True{}:
1415 rv.done(res, parts, None{})
1416 case False{}:
1417 RtBad{}
1418
1419# One read: piece, or the server closed (RFC 9112 §8: a message cut short is not a message).
1420def rv.step(closed: Bool, +head: Bool, rv: Rv, piece: Bytes.Bytes) -> Rt:
1421 match closed:
1422 case True{}:
1423 match rv:
1424 case RvHead{buf, k}:
1425 RtBad{}
1426 case RvBody{res, rb, parts}:
1427 rv.eof(res, parts, rb.eof(rb))
1428 case RvLen{res, left, body}:
1429 RtBad{}
1430 case False{}:
1431 match rv:
1432 case RvHead{buf, +k}:
1433 rv.head(hs.more(head, k, buf, piece))
1434 case RvBody{res, rb, parts}:
1435 rv.fed(res, rb.feed(rb, parts, piece))
1436 case RvLen{res, +left, body}:
1437 rl.feed(res, left, body, piece)
1438
1439def rv.end(closed: Bool, +head: Bool, t: Rt) -> Rt:
1440 match closed:
1441 case False{}:
1442 t
1443 case True{}:
1444 match t:
1445 case RtMore{rv}:
1446 rv.step(True{}, head, rv, Bytes.new(0))
1447 case RtBad{}:
1448 RtBad{}
1449 case RtDone{res, rest}:
1450 RtDone{res, rest}
1451
1452def rv.go(xs: List<&2, String>, closed: Bool, +head: Bool, t: Rt) -> Rt:
1453 match xs:
1454 case Nil{}:
1455 rv.end(closed, head, t)
1456 case Con{+x, rest}:
1457 match t:
1458 case RtMore{rv}:
1459 rv.go(rest, closed, head, rv.step(False{}, head, rv, Bytes.from_string(x)))
1460 case RtBad{}:
1461 RtBad{}
1462 case RtDone{res, r}:
1463 RtDone{res, r}
1464
1465def rt.frame(t: Rt) -> Frame:
1466 match t:
1467 case RtMore{rv}:
1468 FrameMore{}
1469 case RtBad{}:
1470 FrameBad{}
1471 case RtDone{res, rest}:
1472 FrameDone{res}
1473
1474# What the read loop makes of these pieces, then a close when closed is set.
1475def res.frame(xs: List<&2, String>, closed: Bool, +head: Bool) -> Frame:
1476 rt.frame(rv.go(xs, closed, head, RtMore{rv.start()}))
1477
1478def rt.rest(t: Rt) -> Maybe<&1, Bytes.Bytes>:
1479 match t:
1480 case RtMore{rv}:
1481 None{}
1482 case RtBad{}:
1483 None{}
1484 case RtDone{res, rest}:
1485 rest
1486
1487def after.of(m: Maybe<&1, Bytes.Bytes>) -> Maybe<&2, String>:
1488 match m:
1489 case None{}:
1490 None{}
1491 case Some{b}:
1492 Some{Bytes.to_string(b)}
1493
1494# Bytes after a complete self-delimited message. None if it is not one yet.
1495def after(+raw: String, +head: Bool) -> Maybe<&2, String>:
1496 after.of(rt.rest(rv.go([raw], False{}, head, RtMore{rv.start()})))
1497
1498def req.v11.ver(mpv: String & String & String) -> Bool:
1499 (+method, path, v) = mpv
1500 String.eq(v, "HTTP/1.1")
1501
1502def req.v11.line(+line: String) -> Bool:
1503 req.v11.ver(start_line(line))
1504
1505def req.v11.lines(xs: List<&2, String>) -> Bool:
1506 match xs:
1507 case Nil{}:
1508 False{}
1509 case Con{line, headers}:
1510 req.v11.line(line)
1511
1512def req.v11.pick(+head: String, ok: Bool) -> Bool:
1513 match ok:
1514 case False{}:
1515 False{}
1516 case True{}:
1517 req.v11.lines(String.lines(head))
1518
1519def req.v11.of(hb: String & String) -> Bool:
1520 (+head, rest) = hb
1521 req.v11.pick(head, blank_end(head))
1522
1523def req.v11(+raw: String) -> Bool:
1524 req.v11.of(split_at_blank(raw))
1525
1526def req.conn_close(+headers: Map<&2, List<&2, String>>) -> Bool:
1527 String.eq(String.to_lower(header(headers, "connection")), "close")
1528
1529def res.conn_close(+headers: Map<&2, List<&2, String>>) -> Bool:
1530 String.eq(String.to_lower(header(headers, "connection")), "close")
1531
1532def serve.fail_close(+status: U32) -> Bool:
1533 Bool.or(U32.is_eq(status, 400), Bool.or(U32.is_eq(status, 413), U32.is_eq(status, 431)))
1534
1535def serve.keep.ok(fail: Bool, res_close: Bool) -> Bool:
1536 match fail:
1537 case True{}:
1538 False{}
1539 case False{}:
1540 Bool.not(res_close)
1541
1542def serve.keep.v11(v11: Bool, +req_close: Bool, +status: U32, res_close: Bool) -> Bool:
1543 match v11:
1544 case False{}:
1545 False{}
1546 case True{}:
1547 match req_close:
1548 case True{}:
1549 False{}
1550 case False{}:
1551 serve.keep.ok(serve.fail_close(status), res_close)
1552
1553def serve.keep(+headers: Map<&2, List<&2, String>>, v11: Bool, +status: U32, +res: Map<&2, List<&2, String>>) -> Bool:
1554 serve.keep.v11(v11, req.conn_close(headers), status, res.conn_close(res))
1555
1556
1557def again.keep(close: Bool, x: Bytes.Bytes) -> Maybe<&1, Bytes.Bytes>:
1558 match close:
1559 case True{}:
1560 None{}
1561 case False{}:
1562 Some{x}
1563
1564def again.rest(close: Bool, rest: Maybe<&1, Bytes.Bytes>) -> Maybe<&1, Bytes.Bytes>:
1565 match rest:
1566 case None{}:
1567 None{}
1568 case Some{x}:
1569 again.keep(close, x)
1570
1571# The bytes past the response when the socket can take another request: the request did not
1572# ask to close, the response is self-delimited, and the peer did not say close.
1573def again(close: Bool, +h: Map<&2, List<&2, String>>, rest: Maybe<&1, Bytes.Bytes>) -> Maybe<&1, Bytes.Bytes>:
1574 match close:
1575 case True{}:
1576 None{}
1577 case False{}:
1578 again.rest(String.eq(String.to_lower(header(h, "connection")), "close"), rest)
1579
1580def res_body.res(res: Res) -> Bytes.Bytes:
1581 Res{status, headers, body} = res
1582 body
1583
1584def res_body(m: Maybe<&1, Res>) -> Bytes.Bytes:
1585 match m:
1586 case None{}:
1587 Bytes.new(0)
1588 case Some{res}:
1589 res_body.res(res)
1590
1591def text(res: Res) -> String:
1592 Enc.utf8.decode(res_body.res(res))
1593
1594# UTF-8 is checked, not repaired: bad UTF-8 in a string gives None (RFC 8259 §8.1).
1595def json(res: Res) -> Maybe<&1, Json.Val>:
1596 Json.parse.bytes(res_body.res(res))
1597
1598def got_body.req(req: Req) -> Bytes.Bytes:
1599 Req{method, path, headers, body} = req
1600 body
1601
1602def got_body(m: Maybe<&1, Req>) -> Bytes.Bytes:
1603 match m:
1604 case None{}:
1605 Bytes.new(0)
1606 case Some{req}:
1607 got_body.req(req)
1608
1609def body.of(hb: String & String) -> String:
1610 (h, b) = hb
1611 b
1612
1613def body(s: String) -> String:
1614 body.of(split_at_blank.go(s, False{}, 0, SNil{}))
1615
1616def headers_lines(+k: String, vs: List<&2, String>, acc: String) -> String:
1617 match vs:
1618 case Nil{}:
1619 acc
1620 case Con{v, t}:
1621 headers_lines(k, t, acc ++ ("\r\n" ++ sanitize(k) ++ ": " ++ sanitize(v)))
1622
1623def headers_block.go(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>, acc: String) -> String:
1624 match xs:
1625 case Nil{}:
1626 acc
1627 case (k, vs) <> t:
1628 headers_block.go(t, headers_lines(k, vs, acc))
1629
1630def headers_block(h: Map<&2, List<&2, String>>) -> String:
1631 headers_block.go(Map.to_list(&2, List<&2, String>, h), "")
1632
1633# RFC 9110 §15. An unknown code gets an empty reason, which RFC 9112 §4 allows.
1634type Reason is Data:
1635 Reason{code: U32, text: String}
1636
1637def reasons() -> List<&2, Reason>:
1638 [Reason{100, "Continue"}, Reason{101, "Switching Protocols"}, Reason{103, "Early Hints"},
1639 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"},
1640 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"},
1641 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"},
1642 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"}]
1643
1644def reason.go(xs: List<&2, Reason>, +status: U32) -> String:
1645 match xs:
1646 case Nil{}:
1647 ""
1648 case Con{Reason{k, v}, t}:
1649 Bool.pick(String, U32.is_eq(k, status), v, reason.go(t, status))
1650
1651def reason(+status: U32) -> String:
1652 reason.go(reasons(), status)
1653
1654def response(+status: U32, headers: Map<&2, List<&2, String>>, body: String) -> String:
1655 ("HTTP/1.1 " ++ U32.show(status) ++ " " ++ reason(status) ++ headers_block(headers)) ++ ("\r\n\r\n" ++ body)
1656
1657def encode.body(head: Bool, top: Bytes.Bytes, body: Bytes.Bytes) -> Bytes.Bytes:
1658 match head:
1659 case True{}:
1660 top
1661 case False{}:
1662 Bytes.append(top, body)
1663
1664def encode.len(+status: U32, headers: Map<&2, List<&2, String>>, head: Bool, body: Bytes.Bytes) -> Bytes.Bytes:
1665 Bytes.Bytes{+len, buf} = body
1666 encode.body(head, Bytes.from_string(response(status, set(headers, "content-length", U32.show(len)), "")), Bytes.Bytes{len, buf})
1667
1668# RFC 9110 §6.4.1, §8.6: 1xx, 204 and 304 have no body; HEAD gets the length but no body.
1669def encode.pick(+status: U32, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, head: Bool, nobody: Bool) -> Bytes.Bytes:
1670 match nobody:
1671 case True{}:
1672 Bytes.from_string(response(status, headers, ""))
1673 case False{}:
1674 encode.len(status, headers, head, body)
1675
1676def encode.on(r: Res, head: Bool) -> Bytes.Bytes:
1677 Res{+status, headers, body} = r
1678 encode.pick(status, headers, body, head, frame.nobody(status, False{}))
1679
1680def encode(r: Res) -> Bytes.Bytes:
1681 encode.on(r, False{})
1682
1683def request(method: String, path: String, headers: Map<&2, List<&2, String>>, body: String) -> String:
1684 (method ++ " " ++ path ++ " HTTP/1.1" ++ headers_block(headers)) ++ ("\r\n\r\n" ++ body)
1685
1686def req.reserved(+k: String) -> Bool:
1687 Bool.or(Bool.or(String.eq(k, "host"), String.eq(k, "connection")), Bool.or(String.eq(k, "content-length"), String.eq(k, "transfer-encoding")))
1688
1689def req.put.one(m: Map<&2, List<&2, String>>, +k: String, vs: List<&2, String>, skip: Bool) -> Map<&2, List<&2, String>>:
1690 match skip:
1691 case True{}:
1692 m
1693 case False{}:
1694 Map.set(&2, List<&2, String>, m, k, vs)
1695
1696def req.put(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>, m: Map<&2, List<&2, String>>) -> Map<&2, List<&2, String>>:
1697 match xs:
1698 case Nil{}:
1699 m
1700 case (k, vs) <> t:
1701 +lk = String.to_lower(k)
1702 req.put(t, req.put.one(m, lk, vs, req.reserved(lk)))
1703
1704# RFC 9110 §8.6: no Content-Length on a bodiless request whose method gives a body no meaning.
1705def req.cl(+m: Map<&2, List<&2, String>>, +method: String, +len: U32) -> Map<&2, List<&2, String>>:
1706 +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"))))
1707 Bool.pick(Map<&2, List<&2, String>>, bodied, set(m, "content-length", U32.show(len)), m)
1708
1709# Caller headers are lowercased so they cannot duplicate ours; host, connection,
1710# content-length and transfer-encoding are always ours (no smuggling through them).
1711def encode_req.word(close: Bool) -> String:
1712 match close:
1713 case True{}:
1714 "close"
1715 case False{}:
1716 "keep-alive"
1717
1718def encode_req.on(+method: String, target: String, host: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, close: Bool) -> Bytes.Bytes:
1719 Bytes.Bytes{+len, buf} = body
1720 +h = set(set(req.put(Map.to_list(&2, List<&2, String>, headers), empty()), "host", host), "connection", encode_req.word(close))
1721 Bytes.append(Bytes.from_string(request(method, target, req.cl(h, method, len), "")), Bytes.Bytes{len, buf})
1722
1723def encode_req(+method: String, target: String, host: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> Bytes.Bytes:
1724 encode_req.on(method, target, host, headers, body, True{})
1725
1726# Redirects (RFC 9110 §15.4, as WHATWG fetch applies them)
1727# --------------------------------------------------------
1728
1729# One request to make: headers are already lowercased (see req.put).
1730type Hop is Type:
1731 Hop{method: String, url: Url.Abs, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
1732
1733def redirect.code(+s: U32) -> Bool:
1734 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))))
1735
1736def redirect.origin(a: Url.Abs) -> String:
1737 Url.Abs{scheme, host, port, target} = a
1738 scheme ++ "://" ++ host ++ ":" ++ U32.show(port)
1739
1740def redirect.del(ks: List<&2, String>, m: Map<&2, List<&2, String>>) -> Map<&2, List<&2, String>>:
1741 match ks:
1742 case Nil{}:
1743 m
1744 case Con{k, t}:
1745 redirect.del(t, Map.del(&2, List<&2, String>, m, k))
1746
1747def redirect.hdrs(+h: Map<&2, List<&2, String>>, drop: Bool, cross: Bool) -> Map<&2, List<&2, String>>:
1748 +h2 = Bool.pick(Map<&2, List<&2, String>>, drop, redirect.del(["content-type", "content-encoding", "content-language", "content-location"], h), h)
1749 Bool.pick(Map<&2, List<&2, String>>, cross, redirect.del(["authorization", "cookie", "proxy-authorization"], h2), h2)
1750
1751# 303 turns any method but HEAD into GET; 301 and 302 turn POST into GET;
1752# 307 and 308 keep method and body. A GET carries no body or body headers.
1753# Credentials do not follow a hop to another origin.
1754def redirect.body(drop: Bool, body: Bytes.Bytes) -> Bytes.Bytes:
1755 match drop:
1756 case True{}:
1757 Bytes.new(0)
1758 case False{}:
1759 body
1760
1761def 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>:
1762 match next:
1763 case None{}:
1764 None{}
1765 case Some{+to}:
1766 +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")))
1767 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)}}
1768
1769def redirect.hop(status: U32, h: Hop, loc: String) -> Maybe<&1, Hop>:
1770 Hop{method, +url, headers, body} = h
1771 redirect.to(status, method, url, headers, body, Url.resolve(url, loc))
1772
1773def redirect.if(status: U32, h: Hop, loc: String, ok: Bool) -> Maybe<&1, Hop>:
1774 match ok:
1775 case False{}:
1776 None{}
1777 case True{}:
1778 redirect.hop(status, h, loc)
1779
1780# The next request after a response, or None when it is not a redirect we follow.
1781def redirect(+status: U32, +headers: Map<&2, List<&2, String>>, h: Hop) -> Maybe<&1, Hop>:
1782 redirect.if(status, h, header(headers, "location"), Bool.and(redirect.code(status), has_header(headers, "location")))
1783
1784def io.recv.words(tls: Bool, s: Socket, max: U32, ms: U32) -> IO(Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>):
1785 match tls:
1786 case True{}:
1787 Wire.tls.recv.words(s, max, ms)
1788 case False{}:
1789 Wire.recv.words(s, max, ms)
1790
1791def io.send(tls: Bool, s: Socket, data: String) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
1792 match tls:
1793 case True{}:
1794 Wire.tls.send(s, data)
1795 case False{}:
1796 Wire.send(s, data)
1797
1798def io.send.words(tls: Bool, s: Socket, +len: U32, buf: Array<U32>) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
1799 match tls:
1800 case True{}:
1801 Wire.tls.send.words(s, len, buf)
1802 case False{}:
1803 Wire.send.words(s, len, buf)
1804
1805def io.send.bytes(tls: Bool, s: Socket, b: Bytes.Bytes) -> IO(Socket & Result<&1, &1, U32 & String, Unit>):
1806 Bytes.Bytes{+len, buf} = b
1807 io.send.words(tls, s, len, buf)
1808
1809def io.close(tls: Bool, s: Socket) -> IO(Unit):
1810 match tls:
1811 case True{}:
1812 Wire.tls.close(s)
1813 case False{}:
1814 Socket.close(s)
1815
1816def fetch.close(tls: Bool, s: Socket, r: Result<&1, &1, Err, Res>) -> IO(Result<&1, &1, Err, Res>):
1817 do IO<Result<&1, &1, Err, Res>>:
1818 io.close(tls, s)
1819 return r
1820
1821# none: no response byte arrived, so an idempotent request may be retried (RFC 9112 §9.3.1).
1822# sock: the socket, when it can take another request.
1823type Out is Type:
1824 OutDone{res: Res, sock: Maybe<&1, Socket>, rest: Bytes.Bytes}
1825 OutFail{e: Err, none: Bool}
1826
1827def fetch.boxed(r: Result<&1, &1, Err, Res>, none: Bool) -> Out:
1828 match r:
1829 case Done{res}:
1830 OutDone{res, None{}, Bytes.new(0)}
1831 case Fail{e}:
1832 OutFail{e, none}
1833
1834def fetch.bad(tls: Bool, s: Socket, e: Maybe<&2, Err>) -> IO(Result<&1, &1, Err, Res>):
1835 match e:
1836 case None{}:
1837 fetch.close(tls, s, Fail{ErrBad{}})
1838 case Some{err}:
1839 fetch.close(tls, s, Fail{err})
1840
1841def fetch.shut(tls: Bool, s: Socket, r: Result<&1, &1, Err, Res>, none: Bool) -> IO(Out):
1842 do IO<Out>:
1843 x : Result<&1, &1, Err, Res> <- fetch.close(tls, s, r)
1844 return fetch.boxed(x, none)
1845
1846def fetch.hold.go(tls: Bool, s: Socket, res: Res, left: Maybe<&1, Bytes.Bytes>) -> IO(Out):
1847 match left:
1848 case Some{x}:
1849 IO.pure(Out, OutDone{res, Some{s}, x})
1850 case None{}:
1851 fetch.shut(tls, s, Done{res}, False{})
1852
1853def fetch.hold(tls: Bool, close: Bool, s: Socket, res: Res, left: Maybe<&1, Bytes.Bytes>) -> IO(Out):
1854 Res{status, +headers, body} = res
1855 fetch.hold.go(tls, s, Res{status, headers, body}, again(close, headers, left))
1856
1857def fetch.failout(tls: Bool, s: Socket, e: Maybe<&2, Err>, none: Bool) -> IO(Out):
1858 do IO<Out>:
1859 r : Result<&1, &1, Err, Res> <- fetch.bad(tls, s, e)
1860 return fetch.boxed(r, none)
1861
1862# Read state: the response so far and the bytes read, or how it ended.
1863# none: no byte arrived, so an idempotent request may be retried.
1864type Fl is Type:
1865 FlMore{rv: Rv, n: U32}
1866 FlBad{err: Maybe<&2, Err>, none: Bool}
1867 FlDone{res: Res, rest: Maybe<&1, Bytes.Bytes>}
1868
1869def fetch.rt(+n: U32, t: Rt) -> Fl:
1870 match t:
1871 case RtMore{rv}:
1872 FlMore{rv, n}
1873 case RtBad{}:
1874 FlBad{None{}, U32.is_zero(n)}
1875 case RtDone{res, rest}:
1876 FlDone{res, rest}
1877
1878# 64 KiB of head past the body cap, as serve allows.
1879def fetch.over(+n: U32) -> Bool:
1880 Nat.is_lt(Nat.add(fetch.max(), 65536n), U32.to_nat(n))
1881
1882def fetch.piece.cap(over: Bool, +head: Bool, rv: Rv, +n2: U32, +len: U32, buf: Array<U32>) -> Fl:
1883 match over:
1884 case True{}:
1885 FlBad{None{}, False{}}
1886 case False{}:
1887 fetch.rt(n2, rv.step(U32.is_zero(len), head, rv, Bytes.Bytes{len, buf}))
1888
1889def fetch.piece(+head: Bool, rv: Rv, +n: U32, p: U32 & Array<U32>) -> Fl:
1890 (+len, buf) = p
1891 +n2 = (n + len : U32)
1892 fetch.piece.cap(fetch.over(n2), head, rv, n2, len, buf)
1893
1894def fetch.next(+head: Bool, rv: Rv, +n: U32, m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Socket & Fl:
1895 (s, r) = m
1896 match r:
1897 case Fail{(+code, why)}:
1898 (s, FlBad{Some{err.or_late(code, ErrRead{code, why})}, U32.is_zero(n)})
1899 case Done{p}:
1900 (s, fetch.piece(head, rv, n, p))
1901
1902# Reads until the response is whole or cannot be; an empty read means the server closed.
1903@unsafe
1904def fetch.loop(+close: Bool, +head: Bool, +tls: Bool, +ms: U32, st: Socket & Fl) -> IO(Out):
1905 (s, fl) = st
1906 match fl:
1907 case FlMore{rv, +n}:
1908 do IO<Out>:
1909 m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv.words(tls, s, 65536, ms)
1910 fetch.loop(close, head, tls, ms, fetch.next(head, rv, n, m))
1911 case FlBad{err, none}:
1912 fetch.failout(tls, s, err, none)
1913 case FlDone{res, rest}:
1914 fetch.hold(tls, close, s, res, rest)
1915
1916def exchange.sent(+tls: Bool, +ms: U32, +close: Bool, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Out):
1917 (s, r) = m
1918 match r:
1919 case Fail{(+code, why)}:
1920 fetch.shut(tls, s, Fail{err.or_late(code, ErrWrite{code, why})}, True{})
1921 case Done{u}:
1922 fetch.loop(close, head, tls, ms, (s, FlMore{rv.start(), 0}))
1923
1924def exchange.go(+tls: Bool, +ms: U32, +close: Bool, +head: Bool, s: Socket, wire: Bytes.Bytes) -> IO(Out):
1925 do IO<Out>:
1926 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(tls, s, wire)
1927 exchange.sent(tls, ms, close, head, sent)
1928
1929def exchange.tup(o: Out) -> Maybe<&1, Socket> & Result<&1, &1, Err, Res> & Bytes.Bytes:
1930 match o:
1931 case OutFail{e, none}:
1932 (None{}, Fail{e}, Bytes.new(0))
1933 case OutDone{res, sock, rest}:
1934 (sock, Done{res}, rest)
1935
1936# One request on an open socket. Some{socket}: it can take another request.
1937def 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):
1938 do IO<Maybe<&1, Socket> & Result<&1, &1, Err, Res> & Bytes.Bytes>:
1939 o : Out <- exchange.go(tls, ms, close, head, s, wire)
1940 return exchange.tup(o)
1941
1942# Paths to a PEM client chain and its private key for mutual TLS.
1943type Cert is Data:
1944 Cert{chain: String, key: String}
1945
1946type Proxy is Data:
1947 ProxyDirect{}
1948 ProxyVia{host: String, port: U32, authorization: String}
1949
1950type Route is Data:
1951 RouteDirect{tls: Bool, host: String, port: U32, cert: Maybe<&2, Cert>}
1952 RouteProxy{tls: Bool, host: String, port: U32, sni: String,
1953 authority: String, authorization: String, cert: Maybe<&2, Cert>}
1954
1955# Connection pool: idle sockets by origin and client identity, newest first, at most cap per key.
1956# fetch uses a fresh pool per call.
1957
1958type Conn is Type:
1959 Conn{tls: Bool, s: Socket}
1960 ConnH2{s: Socket, client: H2.Client}
1961
1962type Send is Type:
1963 Send{method: String, target: String, authority: String,
1964 headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
1965
1966type H2Step is Type:
1967 H2Reply{s: Socket, reply: H2.Reply}
1968 H2Sent{client: H2.Client, events: List<&1, H2.ClientEvent>,
1969 sent: Result<&1, &1, Err, Socket>}
1970 H2Events{s: Socket, client: H2.Client, result: Result<&1, &1, Err, Maybe<&1, Res>>}
1971 H2Received{client: H2.Client,
1972 answer: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>}
1973
1974type TunnelStep is Type:
1975 TunnelRead{s: Socket, raw: String}
1976 TunnelHead{s: Socket, raw: String, frame: Frame}
1977 TunnelGot{raw: String,
1978 answer: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>}
1979
1980type Pool is Type:
1981 Pool{cap: U32, idle: Map<&1, List<&1, Conn>>}
1982
1983def pool.new.with(+cap: U32) -> Pool:
1984 Pool{cap, Map.new(&1, List<&1, Conn>)}
1985
1986# Up to 8 idle sockets per origin.
1987def pool.new() -> Pool:
1988 pool.new.with(8)
1989
1990def pool.key(+scheme: String, +host: String, +port: U32) -> String:
1991 scheme ++ "://" ++ host ++ ":" ++ U32.show(port)
1992
1993def pool.key.cert(+base: String, cert: Maybe<&2, Cert>) -> String:
1994 match cert:
1995 case None{}:
1996 base
1997 case Some{Cert{+chain, +key}}:
1998 base ++ "|cert:" ++ Nat.show(String.length(chain)) ++ ":" ++ chain
1999 ++ Nat.show(String.length(key)) ++ ":" ++ key
2000
2001def pool.take.of(+cap: U32, +key: String, r: Map<&1, List<&1, Conn>> & Maybe<&1, List<&1, Conn>>) -> Pool & Maybe<&1, Conn>:
2002 (m, got) = r
2003 match got:
2004 case None{}:
2005 (Pool{cap, m}, None{})
2006 case Some{xs}:
2007 match xs:
2008 case Nil{}:
2009 (Pool{cap, m}, None{})
2010 case Con{c, t}:
2011 (Pool{cap, Map.set(&1, List<&1, Conn>, m, key, t)}, Some{c})
2012
2013# The socket given back last.
2014def pool.take(p: Pool, +key: String) -> Pool & Maybe<&1, Conn>:
2015 Pool{+cap, idle} = p
2016 pool.take.of(cap, key, Map.pop(&1, List<&1, Conn>, idle, key))
2017
2018def conn.close(c: Conn) -> IO(Unit):
2019 match c:
2020 case Conn{tls, s}:
2021 io.close(tls, s)
2022 case ConnH2{s, client}:
2023 Wire.tls.close(s)
2024
2025# The first n sockets; the rest are closed.
2026def conns.cut(xs: List<&1, Conn>, n: Nat) -> IO(List<&1, Conn>):
2027 match xs:
2028 case Nil{}:
2029 IO.pure(List<&1, Conn>, Nil{})
2030 case Con{c, t}:
2031 match n:
2032 case 0n:
2033 do IO<List<&1, Conn>>:
2034 conn.close(c)
2035 conns.cut(t, 0n)
2036 case 1n+k:
2037 do IO<List<&1, Conn>>:
2038 r : List<&1, Conn> <- conns.cut(t, k)
2039 return c <> r
2040
2041def pool.give.of(+cap: U32, +key: String, c: Conn, limit: Nat,
2042 r: Map<&1, List<&1, Conn>> & Maybe<&1, List<&1, Conn>>) -> IO(Pool):
2043 (m, old) = r
2044 do IO<Pool>:
2045 xs : List<&1, Conn> <- conns.cut(c <> Maybe.default(&1, List<&1, Conn>, old, Nil{}), limit)
2046 return Pool{cap, Map.set(&1, List<&1, Conn>, m, key, xs)}
2047
2048# Past the limit (cap for HTTP/1.1, one session for HTTP/2), close the oldest idle connection.
2049def pool.give(p: Pool, +key: String, c: Conn) -> IO(Pool):
2050 Pool{+cap, idle} = p
2051 match c:
2052 case Conn{tls, s}:
2053 pool.give.of(cap, key, Conn{tls, s}, U32.to_nat(cap), Map.pop(&1, List<&1, Conn>, idle, key))
2054 case ConnH2{s, client}:
2055 pool.give.of(cap, key, ConnH2{s, client}, Bool.pick(Nat, U32.is_zero(cap), 0n, 1n),
2056 Map.pop(&1, List<&1, Conn>, idle, key))
2057
2058def pool.close.go(xs: List<&1, List<&1, Conn>>) -> IO(Unit):
2059 match xs:
2060 case Nil{}:
2061 IO.pure(Unit, Unit{})
2062 case Con{cs, t}:
2063 do IO<Unit>:
2064 none : List<&1, Conn> <- conns.cut(cs, 0n)
2065 pool.close.go(t)
2066
2067def pool.close(p: Pool) -> IO(Unit):
2068 Pool{cap, idle} = p
2069 pool.close.go(Map.values(&1, List<&1, Conn>, idle))
2070
2071# RFC 9110 §9.2.2
2072def pool.idempotent(+method: String) -> Bool:
2073 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"))))))
2074
2075def conn.tls(m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Result<&1, &1, Err, Conn>):
2076 (s, r) = m
2077 match r:
2078 case Fail{(+code, why)}:
2079 do IO<Result<&1, &1, Err, Conn>>:
2080 Wire.tls.close(s)
2081 return Fail{err.or_late(code, ErrTls{code, why})}
2082 case Done{u}:
2083 IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{True{}, s}})
2084
2085def conn.h2.sent(client: H2.Client, r: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Result<&1, &1, Err, Conn>):
2086 (s, sent) = r
2087 match sent:
2088 case Fail{(+code, why)}:
2089 do IO<Result<&1, &1, Err, Conn>>:
2090 Wire.tls.close(s)
2091 return Fail{err.or_late(code, ErrWrite{code, why})}
2092 case Done{u}:
2093 IO.pure(Result<&1, &1, Err, Conn>, Done{ConnH2{s, client}})
2094
2095def conn.h2.start(s: Socket, r: H2.Client & HBytes.Bytes) -> IO(Result<&1, &1, Err, Conn>):
2096 (client, HBytes.Bytes{len, buf}) = r
2097 do IO<Result<&1, &1, Err, Conn>>:
2098 sent : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.tls.send.words(s, len, buf)
2099 conn.h2.sent(client, sent)
2100
2101def conn.tls.protocol(proto: String, s: Socket) -> IO(Result<&1, &1, Err, Conn>):
2102 match proto:
2103 case "h2":
2104 conn.h2.start(s, H2.client.start())
2105 case "http/1.1":
2106 IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{True{}, s}})
2107 case "":
2108 IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{True{}, s}})
2109 case other:
2110 do IO<Result<&1, &1, Err, Conn>>:
2111 Wire.tls.close(s)
2112 return Fail{ErrTls{71, "unsupported ALPN: " ++ other}}
2113
2114def conn.tls.alpn(m: Socket & Result<&1, &1, U32 & String, String>) -> IO(Result<&1, &1, Err, Conn>):
2115 (s, r) = m
2116 match r:
2117 case Fail{(+code, why)}:
2118 do IO<Result<&1, &1, Err, Conn>>:
2119 Wire.tls.close(s)
2120 return Fail{err.or_late(code, ErrTls{code, why})}
2121 case Done{proto}:
2122 conn.tls.protocol(proto, s)
2123
2124def conn.secure.no.cert(offer: Bool, s: Socket, host: String, +ms: U32) ->
2125 IO(Result<&1, &1, Err, Conn>):
2126 match offer:
2127 case True{}:
2128 do IO<Result<&1, &1, Err, Conn>>:
2129 hs : Socket & Result<&1, &1, U32 & String, String> <-
2130 Wire.tls.connect.alpn(s, host, ms, "h2,http/1.1")
2131 conn.tls.alpn(hs)
2132 case False{}:
2133 do IO<Result<&1, &1, Err, Conn>>:
2134 hs : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.tls.connect(s, host, ms)
2135 conn.tls(hs)
2136
2137def conn.secure.tls(cert: Maybe<&2, Cert>, s: Socket, host: String, +ms: U32,
2138 offer: Bool) -> IO(Result<&1, &1, Err, Conn>):
2139 match cert:
2140 case None{}:
2141 conn.secure.no.cert(offer, s, host, ms)
2142 case Some{Cert{chain, key}}:
2143 do IO<Result<&1, &1, Err, Conn>>:
2144 hs : Socket & Result<&1, &1, U32 & String, Unit> <-
2145 Wire.tls.connect.cert(s, host, ms, chain, key)
2146 conn.tls(hs)
2147
2148# A failed handshake is an error, never plaintext.
2149def conn.secure(+ms: U32, sni: String, s: Socket, tls: Bool,
2150 cert: Maybe<&2, Cert>, offer: Bool) -> IO(Result<&1, &1, Err, Conn>):
2151 match tls:
2152 case False{}:
2153 IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{False{}, s}})
2154 case True{}:
2155 conn.secure.tls(cert, s, sni, ms, offer)
2156
2157def conn.made(+ms: U32, sni: String, tls: Bool, cert: Maybe<&2, Cert>,
2158 offer: Bool, r: Result<&1, &1, U32 & String, Socket>) ->
2159 IO(Result<&1, &1, Err, Conn>):
2160 match r:
2161 case Fail{(+code, why)}:
2162 IO.pure(Result<&1, &1, Err, Conn>, Fail{err.or_late(code, ErrConnect{code, why})})
2163 case Done{s}:
2164 conn.secure(ms, sni, s, tls, cert, offer)
2165
2166def conn.open(+tls: Bool, +ms: U32, sni: String, ip: String, port: U32) ->
2167 IO(Result<&1, &1, Err, Conn>):
2168 do IO<Result<&1, &1, Err, Conn>>:
2169 c : Result<&1, &1, U32 & String, Socket> <- Wire.connect(ip, port, ms)
2170 conn.made(ms, sni, tls, None{}, False{}, c)
2171
2172# ponytail: addresses are tried in order, not raced; a broken first route can consume the step timeout.
2173type Dial is Type:
2174 Dial{port: U32, ms: U32, deadline: Nat, action: IO(Result<&1, &1, U32 & String, Socket>)}
2175
2176def conn.dial.time(+ip: String, +port: U32, +deadline: Nat, now: Nat, expired: Bool) ->
2177 IO(Result<&1, &1, U32 & String, Socket>):
2178 match expired:
2179 case True{}:
2180 IO.pure(Result<&1, &1, U32 & String, Socket>, Fail{(60, "connect timeout")})
2181 case False{}:
2182 Wire.connect(ip, port, U32.from_nat(Nat.sub(deadline, now)))
2183
2184def conn.dial.with(+ip: String, +port: U32, +ms: U32, +deadline: Nat, +now: Nat, unlimited: Bool) ->
2185 IO(Result<&1, &1, U32 & String, Socket>):
2186 match unlimited:
2187 case True{}:
2188 Wire.connect(ip, port, 0)
2189 case False{}:
2190 conn.dial.time(ip, port, deadline, now, Nat.is_le(deadline, now))
2191
2192def conn.dial.try(+ip: String, +port: U32, +ms: U32, +deadline: Nat) ->
2193 IO(Result<&1, &1, U32 & String, Socket>):
2194 do IO<Result<&1, &1, U32 & String, Socket>>:
2195 now : Nat <- IO.now()
2196 conn.dial.with(ip, port, ms, deadline, now, U32.is_zero(ms))
2197
2198def conn.dial.after(r: Result<&1, &1, U32 & String, Socket>, ip: String, +port: U32, +ms: U32, +deadline: Nat) ->
2199 IO(Result<&1, &1, U32 & String, Socket>):
2200 match r:
2201 case Done{s}:
2202 IO.pure(Result<&1, &1, U32 & String, Socket>, Done{s})
2203 case Fail{e}:
2204 conn.dial.try(ip, port, ms, deadline)
2205
2206def conn.dial.more(prev: IO(Result<&1, &1, U32 & String, Socket>), ip: String, +port: U32, +ms: U32, +deadline: Nat) ->
2207 IO(Result<&1, &1, U32 & String, Socket>):
2208 do IO<Result<&1, &1, U32 & String, Socket>>:
2209 r : Result<&1, &1, U32 & String, Socket> <- prev
2210 conn.dial.after(r, ip, port, ms, deadline)
2211
2212def conn.dial.fold(d: Dial, ip: String) -> Dial:
2213 Dial{+port, +ms, +deadline, action} = d
2214 Dial{port, ms, deadline, conn.dial.more(action, ip, port, ms, deadline)}
2215
2216def conn.dial.run(d: Dial) -> IO(Result<&1, &1, U32 & String, Socket>):
2217 Dial{port, ms, deadline, action} = d
2218 action
2219
2220def conn.dial.all(+port: U32, +ms: U32, +start: Nat, first: String, rest: List<&2, String>) ->
2221 IO(Result<&1, &1, U32 & String, Socket>):
2222 match rest:
2223 case Nil{}:
2224 Wire.connect(first, port, ms)
2225 case Con{ip, tail}:
2226 +deadline = Nat.add(start, U32.to_nat(ms))
2227 conn.dial.run(List.foldl(~&2, ~String, ~Dial, ~conn.dial.fold, Con{ip, tail},
2228 Dial{port, ms, deadline, Wire.connect(first, port, ms)}))
2229
2230def conn.open.all(+tls: Bool, +ms: U32, +host: String, +port: U32,
2231 ips: List<&2, String>, cert: Maybe<&2, Cert>, offer: Bool) ->
2232 IO(Result<&1, &1, Err, Conn>):
2233 match ips:
2234 case Nil{}:
2235 IO.pure(Result<&1, &1, Err, Conn>, Fail{ErrDns{}})
2236 case Con{addr, rest}:
2237 do IO<Result<&1, &1, Err, Conn>>:
2238 start : Nat <- IO.now()
2239 r : Result<&1, &1, U32 & String, Socket> <- conn.dial.all(port, ms, start, addr, rest)
2240 conn.made(ms, host, tls, cert, offer, r)
2241
2242def proxy.auth.safe(s: String) -> Bool:
2243 match s:
2244 case SNil{}:
2245 True{}
2246 case SCon{Chr{+c}, rest}:
2247 Bool.and(U32.is_ge(c, 32), Bool.and(U32.is_ne(c, 127), proxy.auth.safe(rest)))
2248
2249def proxy.auth.checked(+decoded: String, valid: Bool) -> Maybe<&2, String>:
2250 match valid:
2251 case False{}:
2252 None{}
2253 case True{}:
2254 Some{"Basic " ++ Bytes.to_base64(Bytes.from_string(decoded))}
2255
2256def proxy.auth.value(m: Maybe<&2, String>) -> Maybe<&2, String>:
2257 match m:
2258 case None{}:
2259 None{}
2260 case Some{+decoded}:
2261 proxy.auth.checked(decoded, Bool.and(Url.has(decoded, 58), proxy.auth.safe(decoded)))
2262
2263def proxy.from.abs(authorization: String, m: Maybe<&2, Url.Abs>) -> Maybe<&2, Proxy>:
2264 match m:
2265 case None{}:
2266 None{}
2267 case Some{Url.Abs{scheme, host, port, target}}:
2268 Some{ProxyVia{host, port, authorization}}
2269
2270def proxy.from.user(user: String, host: String) -> Maybe<&2, Proxy>:
2271 do Maybe<&2, Proxy>:
2272 authorization : String <- proxy.auth.value(Url.pct.decode(user))
2273 proxy.from.abs(authorization, Url.absolute("http://" ++ host))
2274
2275def proxy.from.authority(has_user: Bool, authority: String, split: String & String) ->
2276 Maybe<&2, Proxy>:
2277 match has_user:
2278 case False{}:
2279 proxy.from.abs("", Url.absolute("http://" ++ authority))
2280 case True{}:
2281 (user, host) = split
2282 proxy.from.user(user, host)
2283
2284def proxy.from.parts(parts: String & String) -> Maybe<&2, Proxy>:
2285 (+authority, path) = parts
2286 match path:
2287 case SNil{}:
2288 proxy.from.authority(Url.has(authority, 64), authority, Url.take_to(authority, 64))
2289 case other:
2290 None{}
2291
2292def proxy.from.url.if(valid: Bool, raw: String) -> Maybe<&2, Proxy>:
2293 match valid:
2294 case False{}:
2295 None{}
2296 case True{}:
2297 proxy.from.parts(Url.take_to(String.drop(raw, 7n), 47))
2298
2299def proxy.from.url(+raw: String) -> Maybe<&2, Proxy>:
2300 proxy.from.url.if(String.starts_with(String.to_lower(raw), "http://"), raw)
2301
2302def proxy.no.domain(+host: String, +suffix: String) -> Bool:
2303 Bool.or(String.eq(host, suffix), String.ends_with(host, "." ++ suffix))
2304
2305def proxy.no.suffix(+host: String, +raw: String) -> Bool:
2306 match raw:
2307 case SCon{Chr{46}, +suffix}:
2308 proxy.no.domain(host, suffix)
2309 case other:
2310 proxy.no.domain(host, raw)
2311
2312def proxy.no.port(valid: Bool, +host: String, suffix: String) -> Bool:
2313 match valid:
2314 case False{}:
2315 False{}
2316 case True{}:
2317 proxy.no.suffix(host, suffix)
2318
2319def proxy.no.named(+host: String, +port: U32, parts: String & String) -> Bool:
2320 (suffix, port_text) = parts
2321 match port_text:
2322 case SNil{}:
2323 proxy.no.suffix(host, suffix)
2324 case other:
2325 proxy.no.port(String.eq(port_text, U32.show(port)), host, suffix)
2326
2327def proxy.no.literal(+host: String, +port: U32, +name: String) -> Bool:
2328 Bool.or(String.eq(name, host), Bool.or(String.eq(name, "[" ++ host ++ "]"),
2329 Bool.or(String.eq(name, host ++ ":" ++ U32.show(port)),
2330 String.eq(name, "[" ++ host ++ "]:" ++ U32.show(port)))))
2331
2332def proxy.no.token(+host: String, +port: U32, token: String) -> Bool:
2333 +name = String.to_lower(trim(token))
2334 Bool.or(String.eq(name, "*"),
2335 Bool.or(proxy.no.literal(host, port, name),
2336 Bool.and(Bool.not(Url.has(host, 58)),
2337 proxy.no.named(host, port, Url.take_to(name, 58)))))
2338
2339def proxy.no.list(xs: List<&2, String>, +host: String, +port: U32) -> Bool:
2340 match xs:
2341 case Nil{}:
2342 False{}
2343 case Con{token, rest}:
2344 Bool.or(proxy.no.token(host, port, token), proxy.no.list(rest, host, port))
2345
2346def proxy.no_match(+host: String, +port: U32, no_proxy: String) -> Bool:
2347 proxy.no.list(String.split(no_proxy, ','), String.to_lower(host), port)
2348
2349def proxy.env.value(r: Result<&1, &1, U32 & String, String>) -> String:
2350 match r:
2351 case Fail{e}:
2352 ""
2353 case Done{value}:
2354 value
2355
2356def proxy.env.lower(r: Result<&1, &1, U32 & String, String>, upper: String) ->
2357 IO(String):
2358 match r:
2359 case Done{value}:
2360 IO.pure(String, value)
2361 case Fail{e}:
2362 do IO<String>:
2363 got : Result<&1, &1, U32 & String, String> <- IO.get_env(upper)
2364 return proxy.env.value(got)
2365
2366def proxy.env(lower: String, upper: String) -> IO(String):
2367 do IO<String>:
2368 got : Result<&1, &1, U32 & String, String> <- IO.get_env(lower)
2369 proxy.env.lower(got, upper)
2370
2371def proxy.from.env(value: String) -> Maybe<&2, Proxy>:
2372 match value:
2373 case SNil{}:
2374 Some{ProxyDirect{}}
2375 case other:
2376 proxy.from.url(value)
2377
2378def proxy.choose(bypass: Bool, value: String) -> Maybe<&2, Proxy>:
2379 match bypass:
2380 case True{}:
2381 Some{ProxyDirect{}}
2382 case False{}:
2383 proxy.from.env(value)
2384
2385def proxy.select(+scheme: String, +host: String, +port: U32) ->
2386 IO(Maybe<&2, Proxy>):
2387 +secure = String.eq(scheme, "https")
2388 do IO<Maybe<&2, Proxy>>:
2389 bypass : String <- proxy.env("no_proxy", "NO_PROXY")
2390 value : String <- proxy.env(Bool.pick(String, secure, "https_proxy", "http_proxy"),
2391 Bool.pick(String, secure, "HTTPS_PROXY", "HTTP_PROXY"))
2392 return proxy.choose(proxy.no_match(host, port, bypass), value)
2393
2394def h2.header.skip(+name: String) -> Bool:
2395 match name:
2396 case SCon{Chr{58}, rest}:
2397 True{}
2398 case other:
2399 Bool.or(req.reserved(name),
2400 Bool.or(String.eq(name, "keep-alive"),
2401 Bool.or(String.eq(name, "proxy-connection"),
2402 Bool.or(String.eq(name, "upgrade"), String.eq(name, "te")))))
2403
2404def h2.header.mode(+name: String) -> U32:
2405 Bool.pick(U32,
2406 Bool.or(String.eq(name, "authorization"),
2407 Bool.or(String.eq(name, "cookie"), String.eq(name, "proxy-authorization"))),
2408 2, 0)
2409
2410def h2.header.values(+name: String, +mode: U32, vs: List<&2, String>) -> List<&2, Hpack.Field>:
2411 match vs:
2412 case Nil{}:
2413 Nil{}
2414 case Con{v, tail}:
2415 Hpack.Field{name, sanitize(v), mode} <> h2.header.values(name, mode, tail)
2416
2417def h2.header.tokens(vs: List<&2, String>) -> List<&2, String>:
2418 match vs:
2419 case Nil{}:
2420 Nil{}
2421 case Con{value, rest}:
2422 List.append(&2, String, String.split(value, ','), h2.header.tokens(rest))
2423
2424def h2.header.nominated.one(enabled: Bool, vs: List<&2, String>,
2425 rest: List<&2, String>) -> List<&2, String>:
2426 match enabled:
2427 case True{}:
2428 List.append(&2, String, h2.header.tokens(vs), rest)
2429 case False{}:
2430 rest
2431
2432def h2.header.nominated(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>) ->
2433 List<&2, String>:
2434 match xs:
2435 case Nil{}:
2436 Nil{}
2437 case (name, values) <> tail:
2438 h2.header.nominated.one(String.eq(String.to_lower(name), "connection"),
2439 values, h2.header.nominated(tail))
2440
2441def h2.header.has(xs: List<&2, String>, +key: String) -> Bool:
2442 match xs:
2443 case Nil{}:
2444 False{}
2445 case Con{value, rest}:
2446 Bool.or(String.eq(String.to_lower(trim(value)), key), h2.header.has(rest, key))
2447
2448def h2.header.item(skip: Bool, +name: String, vs: List<&2, String>,
2449 tail: List<&2, Hpack.Field>) -> List<&2, Hpack.Field>:
2450 match skip:
2451 case True{}:
2452 tail
2453 case False{}:
2454 List.append(&2, Hpack.Field, h2.header.values(name, h2.header.mode(name), vs), tail)
2455
2456def h2.header.items(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>,
2457 +nominated: List<&2, String>) -> List<&2, Hpack.Field>:
2458 match xs:
2459 case Nil{}:
2460 Nil{}
2461 case (name, values) <> tail:
2462 +key = String.to_lower(name)
2463 h2.header.item(Bool.or(h2.header.skip(key), h2.header.has(nominated, key)),
2464 key, values, h2.header.items(tail, nominated))
2465
2466def h2.request.fields(+method: String, target: String, authority: String,
2467 headers: Map<&2, List<&2, String>>) -> List<&2, Hpack.Field>:
2468 +xs = Map.to_list(&2, List<&2, String>, headers)
2469 List.append(&2, Hpack.Field,
2470 [Hpack.Field{":method", method, 0}, Hpack.Field{":scheme", "https", 0},
2471 Hpack.Field{":authority", authority, 0}, Hpack.Field{":path", target, 0}],
2472 h2.header.items(xs, h2.header.nominated(xs)))
2473
2474def h2.response.status.value(+value: String, valid: Bool) -> Maybe<&2, U32>:
2475 match valid:
2476 case False{}:
2477 None{}
2478 case True{}:
2479 parse_u32(value)
2480
2481def h2.response.status(xs: List<&2, Hpack.Field>) -> Maybe<&2, U32>:
2482 match xs:
2483 case Nil{}:
2484 None{}
2485 case Con{Hpack.Field{name, +value, mode}, tail}:
2486 match name:
2487 case ":status":
2488 h2.response.status.value(value, Nat.is_eq(String.length(value), 3n))
2489 case other:
2490 h2.response.status(tail)
2491
2492def h2.response.headers(xs: List<&2, Hpack.Field>, acc: Map<&2, List<&2, String>>) ->
2493 Map<&2, List<&2, String>>:
2494 match xs:
2495 case Nil{}:
2496 acc
2497 case Con{Hpack.Field{name, value, mode}, tail}:
2498 match name:
2499 case SCon{Chr{58}, rest}:
2500 h2.response.headers(tail, acc)
2501 case other:
2502 h2.response.headers(tail, add(acc, String.to_lower(name), value))
2503
2504def h2.response.final(interim: Bool, +status: U32, headers: List<&2, Hpack.Field>,
2505 body: HBytes.Bytes) -> Result<&1, &1, Err, Maybe<&1, Res>>:
2506 match interim:
2507 case True{}:
2508 Done{None{}}
2509 case False{}:
2510 HBytes.Bytes{len, buf} = body
2511 Done{Some{Res{status, h2.response.headers(headers, empty()), Bytes.Bytes{len, buf}}}}
2512
2513def h2.response.valid(valid: Bool, +status: U32, headers: List<&2, Hpack.Field>,
2514 body: HBytes.Bytes) -> Result<&1, &1, Err, Maybe<&1, Res>>:
2515 match valid:
2516 case False{}:
2517 Fail{ErrBad{}}
2518 case True{}:
2519 h2.response.final(U32.is_lt(status, 200), status, headers, body)
2520
2521def h2.response.parsed(m: Maybe<&2, U32>, headers: List<&2, Hpack.Field>,
2522 body: HBytes.Bytes) -> Result<&1, &1, Err, Maybe<&1, Res>>:
2523 match m:
2524 case None{}:
2525 Fail{ErrBad{}}
2526 case Some{+status}:
2527 h2.response.valid(Bool.and(U32.is_ge(status, 100), U32.is_lt(status, 600)),
2528 status, headers, body)
2529
2530def h2.response(+fields: List<&2, Hpack.Field>, body: HBytes.Bytes) ->
2531 Result<&1, &1, Err, Maybe<&1, Res>>:
2532 h2.response.parsed(h2.response.status(fields), fields, body)
2533
2534def h2.event.fold(acc: Result<&1, &1, Err, Maybe<&1, Res>>,
2535 event: H2.ClientEvent) -> Result<&1, &1, Err, Maybe<&1, Res>>:
2536 match acc:
2537 case Fail{e}:
2538 Fail{e}
2539 case Done{Some{res}}:
2540 Done{Some{res}}
2541 case Done{None{}}:
2542 match event:
2543 case H2.Response{id, headers, body}:
2544 h2.response(headers, body)
2545 case H2.Reset{id, code}:
2546 Fail{ErrBad{}}
2547 case H2.Shutdown{last, code}:
2548 Done{None{}}
2549 case H2.Pong{data}:
2550 Done{None{}}
2551
2552def h2.send.report(r: Socket & Result<&1, &1, U32 & String, Unit>) ->
2553 IO(Result<&1, &1, Err, Socket>):
2554 (s, sent) = r
2555 match sent:
2556 case Fail{(+code, why)}:
2557 do IO<Result<&1, &1, Err, Socket>>:
2558 Wire.tls.close(s)
2559 return Fail{err.or_late(code, ErrWrite{code, why})}
2560 case Done{unit}:
2561 IO.pure(Result<&1, &1, Err, Socket>, Done{s})
2562
2563def h2.send.one(prev: Result<&1, &1, Err, Socket>, b: HBytes.Bytes) ->
2564 IO(Result<&1, &1, Err, Socket>):
2565 match prev:
2566 case Fail{e}:
2567 IO.pure(Result<&1, &1, Err, Socket>, Fail{e})
2568 case Done{s}:
2569 HBytes.Bytes{len, buf} = b
2570 do IO<Result<&1, &1, Err, Socket>>:
2571 sent : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.tls.send.words(s, len, buf)
2572 h2.send.report(sent)
2573
2574def h2.send.fold(prev: IO(Result<&1, &1, Err, Socket>), b: HBytes.Bytes) ->
2575 IO(Result<&1, &1, Err, Socket>):
2576 do IO<Result<&1, &1, Err, Socket>>:
2577 r : Result<&1, &1, Err, Socket> <- prev
2578 h2.send.one(r, b)
2579
2580def h2.send(xs: List<&1, HBytes.Bytes>, s: Socket) -> IO(Result<&1, &1, Err, Socket>):
2581 List.foldl(~&1, ~HBytes.Bytes, ~IO(Result<&1, &1, Err, Socket>), ~h2.send.fold,
2582 xs, IO.pure(Result<&1, &1, Err, Socket>, Done{s}))
2583
2584def h2.received.step(over: Bool, s: Socket, client: H2.Client,
2585 +len: U32, buf: Array<U32>) -> H2Step:
2586 match over:
2587 case True{}:
2588 H2Reply{s, H2.Failed{H2.Error{1, True{}, 0}}}
2589 case False{}:
2590 H2Reply{s, H2.client.receive(client, HBytes.Bytes{len, buf})}
2591
2592def h2.fail(s: Socket, e: Err) -> IO(Result<&1, &1, Err, Conn & Res>):
2593 do IO<Result<&1, &1, Err, Conn & Res>>:
2594 Wire.tls.close(s)
2595 return Fail{e}
2596
2597def h2.loop(n: Nat, step: H2Step, +ms: U32, +used: U32) ->
2598 IO(Result<&1, &1, Err, Conn & Res>):
2599 match n:
2600 case 0n:
2601 match step:
2602 case H2Reply{s, reply}:
2603 h2.fail(s, ErrBad{})
2604 case H2Sent{client, events, sent}:
2605 match sent:
2606 case Fail{e}:
2607 IO.pure(Result<&1, &1, Err, Conn & Res>, Fail{e})
2608 case Done{s}:
2609 h2.fail(s, ErrBad{})
2610 case H2Events{s, client, result}:
2611 h2.fail(s, ErrBad{})
2612 case H2Received{client, answer}:
2613 (s, r) = answer
2614 h2.fail(s, ErrBad{})
2615 case 1n+p:
2616 match step:
2617 case H2Reply{s, reply}:
2618 match reply:
2619 case H2.Failed{error}:
2620 h2.fail(s, ErrBad{})
2621 case H2.Ready{client, writes, events}:
2622 do IO<Result<&1, &1, Err, Conn & Res>>:
2623 sent : Result<&1, &1, Err, Socket> <- h2.send(writes, s)
2624 h2.loop(p, H2Sent{client, events, sent}, ms, used)
2625 case H2Sent{client, events, sent}:
2626 match sent:
2627 case Fail{e}:
2628 IO.pure(Result<&1, &1, Err, Conn & Res>, Fail{e})
2629 case Done{s}:
2630 h2.loop(p, H2Events{s, client,
2631 List.foldl(~&1, ~H2.ClientEvent,
2632 ~Result<&1, &1, Err, Maybe<&1, Res>>, ~h2.event.fold,
2633 events, Done{None{}})}, ms, used)
2634 case H2Events{s, client, result}:
2635 match result:
2636 case Fail{e}:
2637 h2.fail(s, e)
2638 case Done{Some{res}}:
2639 IO.pure(Result<&1, &1, Err, Conn & Res>,
2640 Done{(ConnH2{s, client}, res)})
2641 case Done{None{}}:
2642 do IO<Result<&1, &1, Err, Conn & Res>>:
2643 r : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <-
2644 Wire.tls.recv.words(s, 16384, ms)
2645 h2.loop(p, H2Received{client, r}, ms, used)
2646 case H2Received{client, answer}:
2647 match answer:
2648 case (s, Fail{(+code, why)}):
2649 h2.fail(s, err.or_late(code, ErrRead{code, why}))
2650 case (s, Done{(0, buf)}):
2651 h2.fail(s, ErrBad{})
2652 case (s, Done{(+len, buf)}):
2653 +total = (used + len : U32)
2654 h2.loop(p, h2.received.step(fetch.over(total), s, client, len, buf), ms, total)
2655
2656def h2.exchange(s: Socket, client: H2.Client, +ms: U32, request: Send) ->
2657 IO(Result<&1, &1, Err, Conn & Res>):
2658 Send{method, target, authority, headers, Bytes.Bytes{len, buf}} = request
2659 h2.loop(Nat.mul(4n, Nat.add(fetch.max(), 65536n)),
2660 H2Reply{s, H2.client.request(client,
2661 h2.request.fields(method, target, authority, headers), HBytes.Bytes{len, buf})},
2662 ms, 0)
2663
2664def proxy.connect.fail(s: Socket, e: Err) -> IO(Result<&1, &1, Err, Conn>):
2665 do IO<Result<&1, &1, Err, Conn>>:
2666 io.close(False{}, s)
2667 return Fail{e}
2668
2669def proxy.connect.extra(m: Maybe<&2, String>, s: Socket, +ms: U32,
2670 sni: String, cert: Maybe<&2, Cert>) -> IO(Result<&1, &1, Err, Conn>):
2671 match m:
2672 case None{}:
2673 proxy.connect.fail(s, ErrBad{})
2674 case Some{rest}:
2675 match rest:
2676 case SNil{}:
2677 conn.secure(ms, sni, s, True{}, cert, True{})
2678 case other:
2679 proxy.connect.fail(s, ErrBad{})
2680
2681def proxy.connect.status(ok: Bool, +status: U32, raw: String, s: Socket,
2682 +ms: U32, sni: String, cert: Maybe<&2, Cert>) ->
2683 IO(Result<&1, &1, Err, Conn>):
2684 match ok:
2685 case False{}:
2686 proxy.connect.fail(s, ErrConnect{status, "proxy CONNECT refused"})
2687 case True{}:
2688 proxy.connect.extra(after(raw, True{}), s, ms, sni, cert)
2689
2690def proxy.connect.finish(res: Res, raw: String, s: Socket, +ms: U32,
2691 sni: String, cert: Maybe<&2, Cert>) -> IO(Result<&1, &1, Err, Conn>):
2692 Res{+status, headers, body} = res
2693 proxy.connect.status(Bool.and(U32.is_ge(status, 200), U32.is_lt(status, 300)),
2694 status, raw, s, ms, sni, cert)
2695
2696def proxy.connect.frame(raw: String, over: Bool) -> Frame:
2697 match over:
2698 case True{}:
2699 FrameBad{}
2700 case False{}:
2701 frame(raw, False{}, True{})
2702
2703def proxy.connect.chunk(empty: Bool, s: Socket, raw: String,
2704 +len: U32, buf: Array<U32>) -> TunnelStep:
2705 match empty:
2706 case True{}:
2707 TunnelHead{s, raw, FrameBad{}}
2708 case False{}:
2709 TunnelRead{s, raw ++ Bytes.to_string(Bytes.Bytes{len, buf})}
2710
2711def proxy.connect.loop(n: Nat, step: TunnelStep, +ms: U32, +sni: String,
2712 +cert: Maybe<&2, Cert>) -> IO(Result<&1, &1, Err, Conn>):
2713 match n:
2714 case 0n:
2715 match step:
2716 case TunnelRead{s, raw}:
2717 proxy.connect.fail(s, ErrBad{})
2718 case TunnelHead{s, raw, result}:
2719 proxy.connect.fail(s, ErrBad{})
2720 case TunnelGot{raw, answer}:
2721 (s, result) = answer
2722 proxy.connect.fail(s, ErrBad{})
2723 case 1n+p:
2724 match step:
2725 case TunnelRead{s, +raw}:
2726 proxy.connect.loop(p, TunnelHead{s, raw,
2727 proxy.connect.frame(raw, Nat.is_gt(String.length(raw), 65536n))},
2728 ms, sni, cert)
2729 case TunnelHead{s, raw, result}:
2730 match result:
2731 case FrameBad{}:
2732 proxy.connect.fail(s, ErrBad{})
2733 case FrameMore{}:
2734 do IO<Result<&1, &1, Err, Conn>>:
2735 answer : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <-
2736 io.recv.words(False{}, s, 4096, ms)
2737 proxy.connect.loop(p, TunnelGot{raw, answer}, ms, sni, cert)
2738 case FrameDone{res}:
2739 proxy.connect.finish(res, raw, s, ms, sni, cert)
2740 case TunnelGot{raw, answer}:
2741 match answer:
2742 case (s, Fail{(+code, why)}):
2743 proxy.connect.fail(s, err.or_late(code, ErrRead{code, why}))
2744 case (s, Done{(+len, buf)}):
2745 proxy.connect.loop(p,
2746 proxy.connect.chunk(U32.is_zero(len), s, raw, len, buf),
2747 ms, sni, cert)
2748
2749def proxy.connect.header(+authority: String, authorization: String) -> String:
2750 match authorization:
2751 case SNil{}:
2752 "CONNECT " ++ authority ++ " HTTP/1.1\r\nHost: " ++ authority ++ "\r\n\r\n"
2753 case other:
2754 "CONNECT " ++ authority ++ " HTTP/1.1\r\nHost: " ++ authority
2755 ++ "\r\nProxy-Authorization: " ++ authorization ++ "\r\n\r\n"
2756
2757def proxy.connect.sent(r: Socket & Result<&1, &1, U32 & String, Unit>,
2758 +ms: U32, sni: String, cert: Maybe<&2, Cert>) ->
2759 IO(Result<&1, &1, Err, Conn>):
2760 (s, sent) = r
2761 match sent:
2762 case Fail{(+code, why)}:
2763 proxy.connect.fail(s, err.or_late(code, ErrWrite{code, why}))
2764 case Done{unit}:
2765 proxy.connect.loop(Nat.mul(3n, 65536n), TunnelRead{s, ""}, ms, sni, cert)
2766
2767def proxy.connect(s: Socket, +ms: U32, sni: String, authority: String,
2768 authorization: String, cert: Maybe<&2, Cert>) ->
2769 IO(Result<&1, &1, Err, Conn>):
2770 do IO<Result<&1, &1, Err, Conn>>:
2771 sent : Socket & Result<&1, &1, U32 & String, Unit> <-
2772 io.send(False{}, s, proxy.connect.header(authority, authorization))
2773 proxy.connect.sent(sent, ms, sni, cert)
2774
2775def proxy.route.tls(tls: Bool, s: Socket, +ms: U32, sni: String,
2776 authority: String, authorization: String, cert: Maybe<&2, Cert>) ->
2777 IO(Result<&1, &1, Err, Conn>):
2778 match tls:
2779 case False{}:
2780 IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{False{}, s}})
2781 case True{}:
2782 proxy.connect(s, ms, sni, authority, authorization, cert)
2783
2784def proxy.route.connected(tls: Bool, +ms: U32, sni: String, authority: String,
2785 authorization: String, cert: Maybe<&2, Cert>,
2786 r: Result<&1, &1, Err, Conn>) -> IO(Result<&1, &1, Err, Conn>):
2787 match r:
2788 case Fail{e}:
2789 IO.pure(Result<&1, &1, Err, Conn>, Fail{e})
2790 case Done{c}:
2791 match c:
2792 case Conn{plain, s}:
2793 proxy.route.tls(tls, s, ms, sni, authority, authorization, cert)
2794 case ConnH2{s, client}:
2795 do IO<Result<&1, &1, Err, Conn>>:
2796 Wire.tls.close(s)
2797 return Fail{ErrBad{}}
2798
2799def proxy.route.open(+ms: U32, +tls: Bool, +host: String, +port: U32,
2800 +sni: String, +authority: String, +authorization: String,
2801 cert: Maybe<&2, Cert>) -> IO(Result<&1, &1, Err, Conn>):
2802 do IO<Result<&1, &1, Err, Conn>>:
2803 ips : List<&2, String> <- Dns.resolve.all(host)
2804 conn : Result<&1, &1, Err, Conn> <-
2805 conn.open.all(False{}, ms, host, port, ips, None{}, False{})
2806 proxy.route.connected(tls, ms, sni, authority, authorization, cert, conn)
2807
2808def route.open(+ms: U32, route: Route) -> IO(Result<&1, &1, Err, Conn>):
2809 match route:
2810 case RouteDirect{tls, +host, port, cert}:
2811 do IO<Result<&1, &1, Err, Conn>>:
2812 ips : List<&2, String> <- Dns.resolve.all(host)
2813 conn.open.all(tls, ms, host, port, ips, cert, True{})
2814 case RouteProxy{tls, host, port, sni, authority, authorization, cert}:
2815 proxy.route.open(ms, tls, host, port, sni, authority, authorization, cert)
2816
2817def conn.ex.h1(+tls: Bool, s: Socket, +ms: U32, request: Send) -> IO(Out):
2818 Send{+method, target, authority, headers, body} = request
2819 exchange.go(tls, ms, False{}, String.eq(method, "HEAD"), s,
2820 encode_req.on(method, target, authority, headers, body, False{}))
2821
2822# A socket with bytes past the response is out of step with the server, so it is closed.
2823def pool.keep.s(p: Pool, +key: String, +tls: Bool, res: Res, s: Socket, clean: Bool) -> IO(Pool & Result<&1, &1, Err, Res>):
2824 match clean:
2825 case True{}:
2826 do IO<Pool & Result<&1, &1, Err, Res>>:
2827 p2 : Pool <- pool.give(p, key, Conn{tls, s})
2828 return (p2, Done{res})
2829 case False{}:
2830 do IO<Pool & Result<&1, &1, Err, Res>>:
2831 io.close(tls, s)
2832 return (p, Done{res})
2833
2834def pool.keep.m(p: Pool, +key: String, +tls: Bool, res: Res, +clean: Bool, sock: Maybe<&1, Socket>) -> IO(Pool & Result<&1, &1, Err, Res>):
2835 match sock:
2836 case None{}:
2837 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Done{res}))
2838 case Some{s}:
2839 pool.keep.s(p, key, tls, res, s, clean)
2840
2841def pool.keep(p: Pool, +key: String, +tls: Bool, res: Res, sock: Maybe<&1, Socket>, rest: Bytes.Bytes) -> IO(Pool & Result<&1, &1, Err, Res>):
2842 Bytes.Bytes{+len, buf} = rest
2843 pool.keep.m(p, key, tls, res, U32.is_zero(len), sock)
2844
2845def pool.after(p: Pool, +key: String, +tls: Bool, o: Out) -> IO(Pool & Result<&1, &1, Err, Res>):
2846 match o:
2847 case OutFail{e, none}:
2848 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
2849 case OutDone{res, sock, rest}:
2850 pool.keep(p, key, tls, res, sock, rest)
2851
2852def pool.h2.reusable(c: Conn) -> Bool & Conn:
2853 match c:
2854 case Conn{tls, s}:
2855 (True{}, Conn{tls, s})
2856 case ConnH2{s, H2.Client{input, streams, encoder, decoder, +control}}:
2857 H2.Control{next, active, frame_max, initial, max_streams, send_window,
2858 recv_window, first, ack, continuation, +goaway} = control
2859 (Maybe.is_none(&2, U32, goaway),
2860 ConnH2{s, H2.Client{input, streams, encoder, decoder, control}})
2861
2862def pool.h2.keep(p: Pool, +key: String, res: Res, state: Bool & Conn) ->
2863 IO(Pool & Result<&1, &1, Err, Res>):
2864 (reusable, c) = state
2865 match reusable:
2866 case True{}:
2867 do IO<Pool & Result<&1, &1, Err, Res>>:
2868 next : Pool <- pool.give(p, key, c)
2869 return (next, Done{res})
2870 case False{}:
2871 do IO<Pool & Result<&1, &1, Err, Res>>:
2872 conn.close(c)
2873 return (p, Done{res})
2874
2875def pool.h2.result(p: Pool, +key: String, r: Result<&1, &1, Err, Conn & Res>) ->
2876 IO(Pool & Result<&1, &1, Err, Res>):
2877 match r:
2878 case Fail{e}:
2879 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
2880 case Done{(c, res)}:
2881 pool.h2.keep(p, key, res, pool.h2.reusable(c))
2882
2883def pool.h2.ex(p: Pool, +key: String, +ms: U32, request: Send,
2884 s: Socket, client: H2.Client) -> IO(Pool & Result<&1, &1, Err, Res>):
2885 do IO<Pool & Result<&1, &1, Err, Res>>:
2886 r : Result<&1, &1, Err, Conn & Res> <- h2.exchange(s, client, ms, request)
2887 pool.h2.result(p, key, r)
2888
2889def pool.fresh.conn(p: Pool, +key: String, +ms: U32, request: Send,
2890 r: Result<&1, &1, Err, Conn>) -> IO(Pool & Result<&1, &1, Err, Res>):
2891 match r:
2892 case Fail{e}:
2893 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
2894 case Done{c}:
2895 match c:
2896 case Conn{+tls, s}:
2897 do IO<Pool & Result<&1, &1, Err, Res>>:
2898 o : Out <- conn.ex.h1(tls, s, ms, request)
2899 pool.after(p, key, tls, o)
2900 case ConnH2{s, client}:
2901 pool.h2.ex(p, key, ms, request, s, client)
2902
2903def pool.fresh(p: Pool, +key: String, +ms: U32, request: Send, route: Route) ->
2904 IO(Pool & Result<&1, &1, Err, Res>):
2905 do IO<Pool & Result<&1, &1, Err, Res>>:
2906 c : Result<&1, &1, Err, Conn> <- route.open(ms, route)
2907 pool.fresh.conn(p, key, ms, request, c)
2908
2909# A reused socket the server already closed fails before any response byte.
2910def pool.retry(+none: Bool, +idem: Bool) -> Bool:
2911 Bool.and(none, idem)
2912
2913def pool.stale(p: Pool, +key: String, +ms: U32, request: Send,
2914 e: Err, again: Bool, route: Route) ->
2915 IO(Pool & Result<&1, &1, Err, Res>):
2916 match again:
2917 case True{}:
2918 pool.fresh(p, key, ms, request, route)
2919 case False{}:
2920 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
2921
2922def pool.reused(p: Pool, +key: String, +tls: Bool, +ms: U32, +idem: Bool,
2923 spare: Send, o: Out, route: Route) ->
2924 IO(Pool & Result<&1, &1, Err, Res>):
2925 match o:
2926 case OutFail{e, +none}:
2927 pool.stale(p, key, ms, spare, e, pool.retry(none, idem), route)
2928 case OutDone{res, sock, rest}:
2929 pool.keep(p, key, tls, res, sock, rest)
2930
2931# Copy only the reused HTTP/1.1 request body, for a stale-socket retry.
2932def pool.idle.h1.bodies(p: Pool, +key: String, +tls: Bool, +ms: U32, +idem: Bool,
2933 s: Socket, +method: String, +target: String, +authority: String,
2934 +headers: Map<&2, List<&2, String>>, r: Bytes.Bytes & Bytes.Bytes,
2935 route: Route) -> IO(Pool & Result<&1, &1, Err, Res>):
2936 (wire, spare) = r
2937 do IO<Pool & Result<&1, &1, Err, Res>>:
2938 o : Out <- conn.ex.h1(tls, s, ms, Send{method, target, authority, headers, wire})
2939 pool.reused(p, key, tls, ms, idem,
2940 Send{method, target, authority, headers, spare}, o, route)
2941
2942def pool.idle.h1(p: Pool, +key: String, +tls: Bool, +ms: U32, +idem: Bool,
2943 s: Socket, request: Send, route: Route) ->
2944 IO(Pool & Result<&1, &1, Err, Res>):
2945 Send{+method, +target, +authority, +headers, body} = request
2946 pool.idle.h1.bodies(p, key, tls, ms, idem, s, method, target,
2947 authority, headers, Bytes.slice(body, 0, 4294967295), route)
2948
2949def pool.idle.reuse(p: Pool, +key: String, +ms: U32, +idem: Bool,
2950 c: Conn, request: Send, route: Route) ->
2951 IO(Pool & Result<&1, &1, Err, Res>):
2952 match c:
2953 case Conn{tls, s}:
2954 pool.idle.h1(p, key, tls, ms, idem, s, request, route)
2955 case ConnH2{s, client}:
2956 pool.h2.ex(p, key, ms, request, s, client)
2957
2958def pool.idle(taken: Pool & Maybe<&1, Conn>, +key: String, +ms: U32,
2959 +idem: Bool, request: Send, route: Route) ->
2960 IO(Pool & Result<&1, &1, Err, Res>):
2961 (p, m) = taken
2962 match m:
2963 case None{}:
2964 pool.fresh(p, key, ms, request, route)
2965 case Some{c}:
2966 pool.idle.reuse(p, key, ms, idem, c, request, route)
2967
2968def proxy.http.headers(headers: Map<&2, List<&2, String>>,
2969 authorization: String) -> Map<&2, List<&2, String>>:
2970 match authorization:
2971 case SNil{}:
2972 headers
2973 case other:
2974 set(headers, "proxy-authorization", authorization)
2975
2976def proxy.absolute(scheme: String, host_field: String, target: String) -> String:
2977 scheme ++ "://" ++ host_field ++ target
2978
2979def proxy.request(secure: Bool, +scheme: String, method: String,
2980 +target: String, +hf: String, headers: Map<&2, List<&2, String>>,
2981 body: Bytes.Bytes, authorization: String) -> Send:
2982 match secure:
2983 case True{}:
2984 Send{method, target, hf, Map.del(&2, List<&2, String>, headers,
2985 "proxy-authorization"), body}
2986 case False{}:
2987 Send{method, proxy.absolute(scheme, hf, target), hf,
2988 proxy.http.headers(headers, authorization), body}
2989
2990def pool.origin.proxy(p: Pool, +method: String, +ms: U32,
2991 headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, +hf: String,
2992 +scheme: String, +host: String, +port: U32, +target: String,
2993 +cert: Maybe<&2, Cert>, proxy: Proxy) ->
2994 IO(Pool & Result<&1, &1, Err, Res>):
2995 match proxy:
2996 case ProxyDirect{}:
2997 +key = pool.key.cert(pool.key(scheme, host, port), cert)
2998 pool.idle(pool.take(p, key), key, ms, pool.idempotent(method),
2999 Send{method, target, hf, headers, body},
3000 RouteDirect{String.eq(scheme, "https"), host, port, cert})
3001 case ProxyVia{+proxy_host, +proxy_port, +authorization}:
3002 +secure = String.eq(scheme, "https")
3003 +key = pool.key.cert(pool.key(scheme, host, port)
3004 ++ "|proxy:" ++ proxy_host ++ ":" ++ U32.show(proxy_port)
3005 ++ "|auth:" ++ authorization, cert)
3006 pool.idle(pool.take(p, key), key, ms, pool.idempotent(method),
3007 proxy.request(secure, scheme, method, target, hf, headers, body, authorization),
3008 RouteProxy{secure, proxy_host, proxy_port, host,
3009 Url.host_field.wrap(host, Url.has(host, 58)) ++ ":" ++ U32.show(port),
3010 authorization, cert})
3011
3012def pool.origin.choice(p: Pool, method: String, ms: U32,
3013 headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, hf: String,
3014 scheme: String, host: String, port: U32, target: String,
3015 cert: Maybe<&2, Cert>, choice: Maybe<&2, Proxy>) ->
3016 IO(Pool & Result<&1, &1, Err, Res>):
3017 match choice:
3018 case None{}:
3019 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{ErrUrl{}}))
3020 case Some{proxy}:
3021 pool.origin.proxy(p, method, ms, headers, body, hf, scheme, host, port,
3022 target, cert, proxy)
3023
3024def pool.origin(p: Pool, method: String, ms: U32,
3025 headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, hf: String,
3026 a: Url.Abs, known: Bool, cert: Maybe<&2, Cert>,
3027 choice: Maybe<&2, Proxy>) ->
3028 IO(Pool & Result<&1, &1, Err, Res>):
3029 Url.Abs{scheme, host, port, target} = a
3030 match known:
3031 case False{}:
3032 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{ErrUrl{}}))
3033 case True{}:
3034 pool.origin.choice(p, method, ms, headers, body, hf, scheme, host,
3035 port, target, cert, choice)
3036
3037def pool.scheme.ok(a: Url.Abs) -> Bool:
3038 Url.Abs{+scheme, host, port, target} = a
3039 Bool.or(String.eq(scheme, "http"), String.eq(scheme, "https"))
3040
3041def pool.one.back(h: Hop, pr: Pool & Result<&1, &1, Err, Res>) -> Pool & Result<&1, &1, Err, Res> & Hop:
3042 (p, r) = pr
3043 (p, r, h)
3044
3045def pool.one.of(p: Pool, +method: String, +url: Url.Abs,
3046 +headers: Map<&2, List<&2, String>>, +ms: U32, r: Bytes.Bytes & Bytes.Bytes,
3047 cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res> & Hop):
3048 Url.Abs{+scheme, +host, +port, target} = url
3049 (body, wire) = r
3050 do IO<Pool & Result<&1, &1, Err, Res> & Hop>:
3051 choice : Maybe<&2, Proxy> <- proxy.select(scheme, host, port)
3052 pr : Pool & Result<&1, &1, Err, Res> <-
3053 pool.origin(p, method, ms, headers, wire, Url.host_field(url),
3054 url, pool.scheme.ok(url), cert, choice)
3055 return pool.one.back(Hop{method, url, headers, body}, pr)
3056
3057# One request, on an idle socket to its origin when the pool has one. The hop comes back for the redirect.
3058def pool.one(p: Pool, h: Hop, +ms: U32, cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res> & Hop):
3059 Hop{+method, +url, +headers, body} = h
3060 pool.one.of(p, method, url, headers, ms, Bytes.slice(body, 0, 4294967295), cert)
3061
3062type Next is Type:
3063 NDone{res: Result<&1, &1, Err, Res>}
3064 NStop{}
3065 NGo{left: Nat, hop: Hop}
3066
3067type Mode is Data:
3068 ModeFollow{}
3069 ModeManual{}
3070 ModeError{}
3071
3072# left: redirects still allowed after the request we just finished.
3073def fetch.hop(left: Nat, h: Hop) -> Next:
3074 match left:
3075 case 0n:
3076 NStop{}
3077 case 1n+p:
3078 NGo{p, h}
3079
3080def fetch.decide.r(left: Nat, r: Res, next: Maybe<&1, Hop>) -> Next:
3081 match next:
3082 case None{}:
3083 NDone{Done{r}}
3084 case Some{h}:
3085 fetch.hop(left, h)
3086
3087def fetch.decide.res(left: Nat, h: Hop, r: Res) -> Next:
3088 Res{+status, +headers, body} = r
3089 fetch.decide.r(left, Res{status, headers, body}, redirect(status, headers, h))
3090
3091def fetch.decide(left: Nat, h: Hop, m: Result<&1, &1, Err, Res>) -> Next:
3092 match m:
3093 case Fail{e}:
3094 NDone{Fail{e}}
3095 case Done{r}:
3096 fetch.decide.res(left, h, r)
3097
3098def fetch.error.res(r: Res, bad: Bool) -> Next:
3099 match bad:
3100 case True{}:
3101 NDone{Fail{ErrRedirect{}}}
3102 case False{}:
3103 NDone{Done{r}}
3104
3105def fetch.error(h: Hop, m: Result<&1, &1, Err, Res>) -> Next:
3106 match m:
3107 case Fail{e}:
3108 NDone{Fail{e}}
3109 case Done{r}:
3110 Res{+status, +headers, body} = r
3111 fetch.error.res(Res{status, headers, body}, Bool.and(redirect.code(status), has_header(headers, "location")))
3112
3113def fetch.policy(mode: Mode, left: Nat, h: Hop, m: Result<&1, &1, Err, Res>) -> Next:
3114 match mode:
3115 case ModeFollow{}:
3116 fetch.decide(left, h, m)
3117 case ModeManual{}:
3118 NDone{m}
3119 case ModeError{}:
3120 fetch.error(h, m)
3121
3122# A caller's own Accept-Encoding wins; enc is the codings fetch can undo.
3123def accept.enc(+h: Map<&2, List<&2, String>>, +enc: String) -> Map<&2, List<&2, String>>:
3124 Bool.pick(Map<&2, List<&2, String>>, has_header(h, "accept-encoding"), h, set(h, "accept-encoding", enc))
3125
3126def fetch.start(method: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, u: Maybe<&2, Url.Abs>, +enc: String) -> Next:
3127 match u:
3128 case None{}:
3129 NDone{Fail{ErrUrl{}}}
3130 case Some{a}:
3131 NGo{20n, Hop{method, a, accept.enc(req.put(Map.to_list(&2, List<&2, String>, headers), empty()), enc), body}}
3132
3133def pool.next.move(p: Pool, +old: String, cert: Maybe<&2, Cert>, n: Next) -> Pool & Next & Maybe<&2, Cert>:
3134 match n:
3135 case NGo{left, h}:
3136 Hop{method, +url, headers, body} = h
3137 (p, NGo{left, Hop{method, url, headers, body}},
3138 Bool.pick(Maybe<&2, Cert>, String.eq(old, redirect.origin(url)), cert, None{}))
3139 case NDone{r}:
3140 (p, NDone{r}, None{})
3141 case NStop{}:
3142 (p, NStop{}, None{})
3143
3144def pool.next(+mode: Mode, left: Nat, cert: Maybe<&2, Cert>, x: Pool & Result<&1, &1, Err, Res> & Hop) -> Pool & Next & Maybe<&2, Cert>:
3145 (p, m, h) = x
3146 Hop{method, +url, headers, body} = h
3147 pool.next.move(p, redirect.origin(url), cert, fetch.policy(mode, left, Hop{method, url, headers, body}, m))
3148
3149def pool.hops.one(+mode: Mode, +ms: U32, +cert: Maybe<&2, Cert>, p: Pool, h: Hop, left: Nat) -> IO(Pool & Next & Maybe<&2, Cert>):
3150 do IO<Pool & Next & Maybe<&2, Cert>>:
3151 x : Pool & Result<&1, &1, Err, Res> & Hop <- pool.one(p, h, ms, cert)
3152 return pool.next(mode, left, cert, x)
3153
3154# NGo.left is how many redirects may follow this request. 20 is WHATWG's limit.
3155@unsafe
3156def pool.hops(+mode: Mode, +ms: U32, st: Pool & Next & Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res>):
3157 (p, n, cert) = st
3158 match n:
3159 case NDone{m}:
3160 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, m))
3161 case NStop{}:
3162 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{ErrRedirect{}}))
3163 case NGo{+left, h}:
3164 do IO<Pool & Result<&1, &1, Err, Res>>:
3165 next : Pool & Next & Maybe<&2, Cert> <- pool.hops.one(mode, ms, cert, p, h, left)
3166 pool.hops(mode, ms, next)
3167
3168# Content-Encoding (RFC 9110 §8.4): each value, trimmed and lowercased, in the order applied.
3169def ce.keep(+w: String, +rest: List<&2, String>) -> List<&2, String>:
3170 Bool.pick(List<&2, String>, String.is_empty(w), rest, Con{w, rest})
3171
3172def ce.norm(xs: List<&2, String>) -> List<&2, String>:
3173 match xs:
3174 case Nil{}:
3175 Nil{}
3176 case Con{v, t}:
3177 ce.keep(String.to_lower(trim(v)), ce.norm(t))
3178
3179def ce.split(xs: List<&2, String>) -> List<&2, String>:
3180 match xs:
3181 case Nil{}:
3182 Nil{}
3183 case Con{v, t}:
3184 List.append(&2, String, ce.norm(String.split(v, ',')), ce.split(t))
3185
3186# Ok: decoded so far. Bad: a coding failed. Skip: a coding we cannot decode, so the body stays as sent.
3187type Dec is Data:
3188 DecOk{b: String}
3189 DecBad{}
3190 DecSkip{}
3191
3192def ce.of(m: Maybe<&2, String>) -> Dec:
3193 match m:
3194 case None{}:
3195 DecBad{}
3196 case Some{b}:
3197 DecOk{b}
3198
3199# Servers send deflate both with and without the zlib wrapper.
3200def ce.deflate(+b: String, m: Maybe<&2, String>) -> Dec:
3201 match m:
3202 case Some{out}:
3203 DecOk{out}
3204 case None{}:
3205 ce.of(Zlib.inflate(b))
3206
3207def ce.apply(+c: String, +b: String) -> Dec:
3208 Bool.pick(Dec, Bool.or(String.eq(c, "gzip"), String.eq(c, "x-gzip")), ce.of(Zlib.gunzip(b)),
3209 Bool.pick(Dec, String.eq(c, "deflate"), ce.deflate(b, Zlib.unzlib(b)),
3210 Bool.pick(Dec, String.eq(c, "identity"), DecOk{b}, DecSkip{})))
3211
3212def ce.go(cs: List<&2, String>, d: Dec) -> Dec:
3213 match cs:
3214 case Nil{}:
3215 d
3216 case Con{+c, t}:
3217 match d:
3218 case DecOk{+b}:
3219 ce.go(t, ce.apply(c, b))
3220 case DecBad{}:
3221 DecBad{}
3222 case DecSkip{}:
3223 DecSkip{}
3224
3225def decoded.pick(d: Dec, +status: U32, headers: Map<&2, List<&2, String>>, body: String) -> Result<&1, &1, Err, Res>:
3226 match d:
3227 case DecOk{b}:
3228 Done{Res{status, headers, Bytes.from_string(b)}}
3229 case DecBad{}:
3230 Fail{ErrBad{}}
3231 case DecSkip{}:
3232 Done{Res{status, headers, Bytes.from_string(body)}}
3233
3234# ponytail: the codings run on a String copy of the body; give zlib a Bytes input if gzip bodies get big.
3235def decoded.cs(+status: U32, +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, cs: List<&2, String>) -> Result<&1, &1, Err, Res>:
3236 match cs:
3237 case Nil{}:
3238 Done{Res{status, headers, body}}
3239 case Con{c, t}:
3240 +s = Bytes.to_string(body)
3241 decoded.pick(ce.go(Con{c, t}, DecOk{s}), status, headers, s)
3242
3243def decoded.go(empty: Bool, +status: U32, +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> Result<&1, &1, Err, Res>:
3244 match empty:
3245 case True{}:
3246 Done{Res{status, headers, body}}
3247 case False{}:
3248 decoded.cs(status, headers, body, List.reverse(&2, String, ce.split(fields(headers, "content-encoding"))))
3249
3250# The body decoded per Content-Encoding; the headers stay as sent. A corrupt body is ErrBad.
3251def decoded(res: Res) -> Result<&1, &1, Err, Res>:
3252 Res{+status, +headers, body} = res
3253 Bytes.Bytes{+len, buf} = body
3254 decoded.go(U32.is_zero(len), status, headers, Bytes.Bytes{len, buf})
3255
3256def decoded.m(r: Result<&1, &1, Err, Res>) -> Maybe<&1, Res>:
3257 match r:
3258 case Done{x}:
3259 Some{x}
3260 case Fail{e}:
3261 None{}
3262
3263def decoded.some(res: Res) -> Maybe<&1, Res>:
3264 decoded.m(decoded(res))
3265
3266def ce.words(r: Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Maybe<&1, Bytes.Bytes>:
3267 match r:
3268 case Fail{e}:
3269 None{}
3270 case Done{(+len, buf)}:
3271 Some{Bytes.Bytes{len, buf}}
3272
3273# A decoded body stops at 16 MiB, like a received one.
3274def ce.eff(~eff: U32 -> U32 -> Array<U32> -> IO(Result<&1, &1, U32 & String, U32 & Array<U32>>), b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
3275 Bytes.Bytes{+len, buf} = b
3276 do IO<Maybe<&1, Bytes.Bytes>>:
3277 r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- eff(16777216, len, buf)
3278 return ce.words(r)
3279
3280def ce.dec(d: Dec) -> Maybe<&1, Bytes.Bytes>:
3281 match d:
3282 case DecOk{b}:
3283 Some{Bytes.from_string(b)}
3284 case DecBad{}:
3285 None{}
3286 case DecSkip{}:
3287 None{}
3288
3289# ponytail: deflate runs on the pure decoder, which also takes raw DEFLATE; servers rarely send it.
3290def ce.io.deflate(on: Bool, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
3291 match on:
3292 case True{}:
3293 +s = Bytes.to_string(b)
3294 IO.pure(Maybe<&1, Bytes.Bytes>, ce.dec(ce.deflate(s, Zlib.unzlib(s))))
3295 case False{}:
3296 IO.pure(Maybe<&1, Bytes.Bytes>, Some{b})
3297
3298def ce.io.zstd(on: Bool, +c: String, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
3299 match on:
3300 case True{}:
3301 ce.eff(~Zlib.zstd.words, b)
3302 case False{}:
3303 ce.io.deflate(String.eq(c, "deflate"), b)
3304
3305def ce.io.br(on: Bool, +c: String, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
3306 match on:
3307 case True{}:
3308 ce.eff(~Zlib.brotli.words, b)
3309 case False{}:
3310 ce.io.zstd(String.eq(c, "zstd"), c, b)
3311
3312# One known coding undone: gzip, x-gzip, br, zstd, deflate, or identity.
3313def ce.io.gz(on: Bool, +c: String, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
3314 match on:
3315 case True{}:
3316 ce.eff(~Zlib.inflate.words, b)
3317 case False{}:
3318 ce.io.br(String.eq(c, "br"), c, b)
3319
3320def ce.io.go(cs: List<&2, String>, m: Maybe<&1, Bytes.Bytes>) -> IO(Maybe<&1, Bytes.Bytes>):
3321 match cs:
3322 case Nil{}:
3323 match m:
3324 case None{}:
3325 IO.pure(Maybe<&1, Bytes.Bytes>, None{})
3326 case Some{b}:
3327 IO.pure(Maybe<&1, Bytes.Bytes>, Some{b})
3328 case Con{+c, t}:
3329 match m:
3330 case None{}:
3331 IO.pure(Maybe<&1, Bytes.Bytes>, None{})
3332 case Some{b}:
3333 do IO<Maybe<&1, Bytes.Bytes>>:
3334 n : Maybe<&1, Bytes.Bytes> <- ce.io.gz(Bool.or(String.eq(c, "gzip"), String.eq(c, "x-gzip")), c, b)
3335 ce.io.go(t, n)
3336
3337def ce.has(xs: List<&2, String>, +c: String) -> Bool:
3338 match xs:
3339 case Nil{}:
3340 False{}
3341 case Con{x, t}:
3342 Bool.or(String.eq(c, x), ce.has(t, c))
3343
3344def ce.known(cs: List<&2, String>, +ok: List<&2, String>) -> Bool:
3345 match cs:
3346 case Nil{}:
3347 True{}
3348 case Con{c, t}:
3349 Bool.and(ce.has(ok, c), ce.known(t, ok))
3350
3351def decoded.io.pick(m: Maybe<&1, Bytes.Bytes>, +status: U32, headers: Map<&2, List<&2, String>>) -> Result<&1, &1, Err, Res>:
3352 match m:
3353 case Some{b}:
3354 Done{Res{status, headers, b}}
3355 case None{}:
3356 Fail{ErrBad{}}
3357
3358def 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>):
3359 match known:
3360 case True{}:
3361 do IO<Result<&1, &1, Err, Res>>:
3362 m : Maybe<&1, Bytes.Bytes> <- ce.io.go(cs, Some{body})
3363 return decoded.io.pick(m, status, headers)
3364 case False{}:
3365 IO.pure(Result<&1, &1, Err, Res>, Done{Res{status, headers, body}})
3366
3367def decoded.io.go(empty: Bool, +enc: String, +status: U32, +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Res>):
3368 match empty:
3369 case True{}:
3370 IO.pure(Result<&1, &1, Err, Res>, Done{Res{status, headers, body}})
3371 case False{}:
3372 +cs = List.reverse(&2, String, ce.split(fields(headers, "content-encoding")))
3373 decoded.io.run(ce.known(cs, Con{"identity", Con{"x-gzip", ce.split(Con{enc, Nil{}})}}), status, headers, body, cs)
3374
3375# decoded through the C libraries, for the codings in enc. A body with any other coding stays as sent.
3376def decoded.io(+enc: String, res: Res) -> IO(Result<&1, &1, Err, Res>):
3377 Res{+status, +headers, body} = res
3378 Bytes.Bytes{+len, buf} = body
3379 decoded.io.go(U32.is_zero(len), enc, status, headers, Bytes.Bytes{len, buf})
3380
3381# An effect on empty input fails with ENOENT only when its library does not load.
3382def codings.ok(r: Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Bool:
3383 match r:
3384 case Fail{(+c, why)}:
3385 Bool.not(U32.is_eq(c, 2))
3386 case Done{p}:
3387 True{}
3388
3389def codings.has(~eff: U32 -> U32 -> Array<U32> -> IO(Result<&1, &1, U32 & String, U32 & Array<U32>>), b: Bytes.Bytes) -> IO(Bool):
3390 Bytes.Bytes{+len, buf} = b
3391 do IO<Bool>:
3392 r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- eff(0, len, buf)
3393 return codings.ok(r)
3394
3395def codings.add(has: Bool, +enc: String, +c: String) -> String:
3396 Bool.pick(String, has, enc ++ ", " ++ c, enc)
3397
3398# gzip and deflate, then br and zstd when their C library loads.
3399def codings() -> IO(String):
3400 do IO<String>:
3401 b : Bool <- codings.has(~Zlib.brotli.words, Bytes.new(0))
3402 z : Bool <- codings.has(~Zlib.zstd.words, Bytes.new(0))
3403 return codings.add(z, codings.add(b, "gzip, deflate", "br"), "zstd")
3404
3405# The final response of a fetch, after redirects.
3406def fetch.final(+enc: String, r: Result<&1, &1, Err, Res>) -> IO(Result<&1, &1, Err, Res>):
3407 match r:
3408 case Done{res}:
3409 decoded.io(enc, res)
3410 case Fail{e}:
3411 IO.pure(Result<&1, &1, Err, Res>, Fail{e})
3412
3413def pool.final(+enc: String, pr: Pool & Result<&1, &1, Err, Res>) -> IO(Pool & Result<&1, &1, Err, Res>):
3414 (p, r) = pr
3415 do IO<Pool & Result<&1, &1, Err, Res>>:
3416 d : Result<&1, &1, Err, Res> <- fetch.final(enc, r)
3417 return (p, d)
3418
3419def 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>):
3420 do IO<Pool & Result<&1, &1, Err, Res>>:
3421 pr : Pool & Result<&1, &1, Err, Res> <- pool.hops(mode, ms, (p, fetch.start(method, headers, body, Url.absolute(url), enc), cert))
3422 pool.final(enc, pr)
3423
3424def 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>):
3425 do IO<Pool & Result<&1, &1, Err, Res>>:
3426 enc : String <- codings()
3427 pool.how.enc(enc, p, method, url, headers, body, ms, mode, cert)
3428
3429# pool.how(p, "GET", "https://example.com/x?y=1", headers, body, ms, mode) follows redirects
3430# on p's idle sockets. Fail is a bad URL, a failed lookup, connect, handshake, send, read,
3431# a malformed response, more than 20 redirects, or a step past ms. Bodies are bytes.
3432def 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>):
3433 pool.how.cert(p, method, url, headers, body, ms, mode, None{})
3434
3435def 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>):
3436 pool.how(p, method, url, headers, body, ms, ModeFollow{})
3437
3438def pool.fetch(p: Pool, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Pool & Result<&1, &1, Err, Res>):
3439 pool.fetch.with(p, method, url, headers, body, 30000)
3440
3441def 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>):
3442 pool.how.cert(p, method, url, headers, body, ms, ModeFollow{}, Some{Cert{chain, key}})
3443
3444def 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>):
3445 pool.fetch.cert.with(p, method, url, headers, body, chain, key, 30000)
3446
3447def fetch.end(pr: Pool & Result<&1, &1, Err, Res>) -> IO(Result<&1, &1, Err, Res>):
3448 (p, r) = pr
3449 do IO<Result<&1, &1, Err, Res>>:
3450 pool.close(p)
3451 return r
3452
3453# fetch is pool.how on a fresh pool that closes afterwards.
3454def 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>):
3455 do IO<Result<&1, &1, Err, Res>>:
3456 pr : Pool & Result<&1, &1, Err, Res> <- pool.how(pool.new(), method, url, headers, body, ms, mode)
3457 fetch.end(pr)
3458
3459def fetch.with(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, ms: U32) -> IO(Result<&1, &1, Err, Res>):
3460 fetch.how(method, url, headers, body, ms, ModeFollow{})
3461
3462def 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>):
3463 do IO<Result<&1, &1, Err, Res>>:
3464 pr : Pool & Result<&1, &1, Err, Res> <- pool.fetch.cert.with(pool.new(), method, url, headers, body, chain, key, ms)
3465 fetch.end(pr)
3466
3467def 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>):
3468 fetch.cert.with(method, url, headers, body, chain, key, 30000)
3469
3470# fetch.with and a 30 s step timeout.
3471def fetch(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Res>):
3472 fetch.with(method, url, headers, body, 30000)
3473
3474def get(url: String) -> IO(Result<&1, &1, Err, Res>):
3475 fetch("GET", url, empty(), Bytes.new(0))
3476
3477# POST v as compact JSON, with content-type: application/json.
3478def post.json(url: String, v: Json.Val) -> IO(Result<&1, &1, Err, Res>):
3479 fetch("POST", url, set(empty(), "content-type", "application/json"), Json.encode.bytes(v))
3480
3481# Base URLs: resolve(base, ref) is ref against the absolute http(s) URL base (RFC 3986 §5.2),
3482# written back as a URL for fetch. None when base is not absolute or ref has another scheme.
3483def resolve.show(a: Url.Abs) -> String:
3484 Url.Abs{+scheme, host, port, +target} = a
3485 scheme ++ "://" ++ Url.host_field(Url.Abs{scheme, host, port, target}) ++ target
3486
3487def resolve.to(m: Maybe<&2, Url.Abs>) -> Maybe<&2, String>:
3488 match m:
3489 case None{}:
3490 None{}
3491 case Some{a}:
3492 Some{resolve.show(a)}
3493
3494def resolve.base(m: Maybe<&2, Url.Abs>, +ref: String) -> Maybe<&2, String>:
3495 match m:
3496 case None{}:
3497 None{}
3498 case Some{b}:
3499 resolve.to(Url.resolve(b, ref))
3500
3501def resolve(base: String, +ref: String) -> Maybe<&2, String>:
3502 resolve.base(Url.absolute(base), ref)
3503
3504# Retry. The wait before retry n (0 first) is 500 ms doubled n times, at most 30 s;
3505# its upper half is jitter r: backoff(n, r) = half + r mod (half + 1).
3506def retry.cap() -> U32:
3507 30000
3508
3509def retry.base(n: Nat) -> U32:
3510 match n:
3511 case 0n:
3512 500
3513 case 1n+p:
3514 U32.min((retry.base(p) * 2 : U32), retry.cap())
3515
3516def retry.backoff.half(+half: U32, +r: U32) -> U32:
3517 (half + (r % (half + 1)) : U32)
3518
3519def retry.backoff(n: Nat, +r: U32) -> U32:
3520 retry.backoff.half((retry.base(n) / 2 : U32), r)
3521
3522# ms clamped to 0 .. retry.cap().
3523def retry.after.ms(+ms: Int.I64) -> U32:
3524 Bool.pick(U32, Int.I64.is_neg(ms), 0,
3525 Bool.pick(U32, Int.I64.is_lt(ms, Int.I64.from_u32(retry.cap())), Int.I64.to_u32(ms), retry.cap()))
3526
3527def retry.after.date(m: Maybe<&2, Time.Instant>, now: Time.Instant) -> Maybe<&2, U32>:
3528 match m:
3529 case None{}:
3530 None{}
3531 case Some{date}:
3532 Some{retry.after.ms(Time.Duration.to_ms(Time.Instant.since(date, now)))}
3533
3534# More than 5 digits is past the cap, and would overflow parse_u32.
3535def retry.after.secs(+v: String, now: Time.Instant, n: Maybe<&2, U32>) -> Maybe<&2, U32>:
3536 match n:
3537 case None{}:
3538 retry.after.date(Time.http_date.parse(v), now)
3539 case Some{s}:
3540 Some{Bool.pick(U32, Nat.is_lt(5n, String.length(v)), retry.cap(), U32.min((s * 1000 : U32), retry.cap()))}
3541
3542# Retry-After (RFC 9110 §10.2.3) as ms from now, at most retry.cap(): delay-seconds, or an
3543# HTTP-date (a past date is 0). None when v is empty or neither form.
3544def retry.after(+v: String, now: Time.Instant) -> Maybe<&2, U32>:
3545 retry.after.secs(v, now, parse_u32(v))
3546
3547def retry.wait(m: Maybe<&2, U32>, n: Nat, +r: U32) -> U32:
3548 match m:
3549 case None{}:
3550 retry.backoff(n, r)
3551 case Some{ms}:
3552 ms
3553
3554# The wait before retry n: Retry-After v when it reads as a delay, else backoff with jitter r.
3555def retry.delay(+v: String, now: Time.Instant, n: Nat, +r: U32) -> U32:
3556 retry.wait(retry.after(v, now), n, r)
3557
3558# Statuses a later try may clear.
3559def retry.status(+s: U32) -> Bool:
3560 Bool.or(Bool.or(U32.is_eq(s, 408), U32.is_eq(s, 429)),
3561 Bool.or(Bool.or(U32.is_eq(s, 500), U32.is_eq(s, 502)), Bool.or(U32.is_eq(s, 503), U32.is_eq(s, 504))))
3562
3563# A refused connect or a timeout may clear; any other error would repeat.
3564def retry.fail(e: Err) -> Result<&1, &1, Err, Res> & Maybe<&2, String>:
3565 match e:
3566 case ErrConnect{code, why}:
3567 (Fail{ErrConnect{code, why}}, Some{""})
3568 case ErrTimeout{}:
3569 (Fail{ErrTimeout{}}, Some{""})
3570 case other:
3571 (Fail{other}, None{})
3572
3573def retry.res(res: Res) -> Result<&1, &1, Err, Res> & Maybe<&2, String>:
3574 Res{+status, +headers, body} = res
3575 (Done{Res{status, headers, body}}, Bool.pick(Maybe<&2, String>, retry.status(status), Some{header(headers, "retry-after")}, None{}))
3576
3577def retry.judge.try(r: Result<&1, &1, Err, Res>) -> Result<&1, &1, Err, Res> & Maybe<&2, String>:
3578 match r:
3579 case Fail{e}:
3580 retry.fail(e)
3581 case Done{res}:
3582 retry.res(res)
3583
3584# One try, judged: the result as it came, and Some{Retry-After value} ("" when absent)
3585# when an idempotent request may try again.
3586def retry.judge(idem: Bool, r: Result<&1, &1, Err, Res>) -> Result<&1, &1, Err, Res> & Maybe<&2, String>:
3587 match idem:
3588 case False{}:
3589 (r, None{})
3590 case True{}:
3591 retry.judge.try(r)
3592
3593# ponytail: a failed random source gives jitter 0, so the wait is the lower half.
3594def retry.jitter(r: Result<&1, &1, U32 & String, U32>) -> U32:
3595 match r:
3596 case Fail{e}:
3597 0
3598 case Done{x}:
3599 x
3600
3601def retry.sleep(+v: String, n: Nat) -> IO(Unit):
3602 do IO<Unit>:
3603 now : Time.Instant <- Time.now()
3604 rnd : Result<&1, &1, U32 & String, U32> <- IO.random_u32()
3605 IO.sleep(retry.delay(v, now, n, retry.jitter(rnd)))
3606
3607def retry.kept(body: Bytes.Bytes, j: Result<&1, &1, Err, Res> & Maybe<&2, String>) -> Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String>:
3608 (r, m) = j
3609 (body, r, m)
3610
3611# One fetch of the copy; the body comes back for the next try.
3612def retry.one(+idem: Bool, +method: String, +url: String, +headers: Map<&2, List<&2, String>>,
3613 r: Bytes.Bytes & Bytes.Bytes) -> IO(Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String>):
3614 (body, spare) = r
3615 do IO<Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String>>:
3616 got : Result<&1, &1, Err, Res> <- fetch(method, url, headers, spare)
3617 return retry.kept(body, retry.judge(idem, got))
3618
3619# left: retries still allowed. n: the retry to wait for next, 0 first.
3620def retry.go(left: Nat, +n: Nat, +idem: Bool, +method: String, +url: String,
3621 +headers: Map<&2, List<&2, String>>,
3622 t: Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String>) -> IO(Result<&1, &1, Err, Res>):
3623 match left:
3624 case 0n:
3625 (body, r, m) = t
3626 IO.pure(Result<&1, &1, Err, Res>, r)
3627 case 1n+p:
3628 (body, r, m) = t
3629 match m:
3630 case None{}:
3631 IO.pure(Result<&1, &1, Err, Res>, r)
3632 case Some{v}:
3633 do IO<Result<&1, &1, Err, Res>>:
3634 retry.sleep(v, n)
3635 tried : Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String> <-
3636 retry.one(idem, method, url, headers, Bytes.slice(body, 0, 4294967295))
3637 retry.go(p, 1n+n, idem, method, url, headers, tried)
3638
3639# fetch.retry(n, method, url, headers, body) is fetch, tried again up to n times while an
3640# idempotent method (GET, HEAD, OPTIONS, TRACE, PUT, DELETE) gets a connect error, a timeout,
3641# or 408, 429, 500, 502, 503, or 504. POST, PATCH and other methods get one try. It waits
3642# Retry-After (seconds or HTTP-date, at most 30 s) when given, else the backoff. When retries
3643# run out, the last response or error comes back as it was.
3644def retry.start(enabled: Bool, n: U32, +method: String, +url: String,
3645 +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) ->
3646 IO(Result<&1, &1, Err, Res>):
3647 match enabled:
3648 case False{}:
3649 fetch(method, url, headers, body)
3650 case True{}:
3651 do IO<Result<&1, &1, Err, Res>>:
3652 first : Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String> <-
3653 retry.one(True{}, method, url, headers, Bytes.slice(body, 0, 4294967295))
3654 retry.go(U32.to_nat(n), 0n, True{}, method, url, headers, first)
3655
3656def fetch.retry(+n: U32, +method: String, +url: String,
3657 +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) ->
3658 IO(Result<&1, &1, Err, Res>):
3659 retry.start(Bool.and(U32.is_ne(n, 0), pool.idempotent(method)),
3660 n, method, url, headers, body)
3661
3662# Streaming (a body read or sent in pieces). A decoded stream owns its decoders.
3663# What the next read returns: read more, a raw piece, a decoded piece, the end, or an error.
3664type Po is Type:
3665 PoNone{}
3666 PoPiece{b: Bytes.Bytes}
3667 PoReady{b: Bytes.Bytes}
3668 PoEnd{}
3669 PoBad{e: Err}
3670
3671type Stream is Type:
3672 Stream{tls: Bool, s: Socket, ms: U32, res: Res, rb: Rb, out: Po, decs: List<&1, Zlib.Decoder>}
3673
3674type Pc is Type:
3675 Pc{rb: Rb, out: Po}
3676
3677# A body piece, or none when empty: more reads the next piece, and not more is the end.
3678def pc.po(more: Bool, empty: Bool, b: Bytes.Bytes) -> Po:
3679 match empty:
3680 case True{}:
3681 Bool.pick(Po, more, PoNone{}, PoEnd{})
3682 case False{}:
3683 PoPiece{b}
3684
3685def pc.piece(more: Bool, +rb: Rb, b: Bytes.Bytes) -> Pc:
3686 Bytes.Bytes{+len, buf} = b
3687 Pc{rb, pc.po(more, U32.is_zero(len), Bytes.Bytes{len, buf})}
3688
3689def pc.fed.of(b: Bytes.Bytes, st: Rb) -> Pc:
3690 match st:
3691 case RbDone{}:
3692 pc.piece(False{}, RbDone{}, b)
3693 case RbBad{}:
3694 Pc{RbDone{}, PoBad{ErrBad{}}}
3695 case RbLen{n}:
3696 pc.piece(True{}, RbLen{n}, b)
3697 case RbChunk{st}:
3698 pc.piece(True{}, RbChunk{st}, b)
3699 case RbClose{}:
3700 pc.piece(True{}, RbClose{}, b)
3701
3702def pc.fed(bf: Bf) -> Pc:
3703 Bf{st, parts, rest} = bf
3704 pc.fed.of(rb.body(parts), st)
3705
3706# The body bytes that just arrived: what they add to the body, and how it ends.
3707def pc.of(rb: Rb, piece: Bytes.Bytes) -> Pc:
3708 pc.fed(rb.feed(rb, Nil{}, piece))
3709
3710# The server closed. Only a close-delimited body may end this way (RFC 9112 §8).
3711def pc.end(ok: Bool) -> Pc:
3712 match ok:
3713 case True{}:
3714 Pc{RbDone{}, PoEnd{}}
3715 case False{}:
3716 Pc{RbDone{}, PoBad{ErrBad{}}}
3717
3718def pc.eof(st: Rb) -> Pc:
3719 pc.end(rb.eof(st))
3720
3721def stream.mk(+tls: Bool, s: Socket, +ms: U32, res: Res, decs: List<&1, Zlib.Decoder>, pc: Pc) -> Stream:
3722 Pc{rb, out} = pc
3723 Stream{tls, s, ms, res, rb, out, decs}
3724
3725def stream.got.piece(+tls: Bool, s: Socket, +ms: U32, res: Res, decs: List<&1, Zlib.Decoder>, +rb: Rb, p: U32 & Array<U32>) -> Stream:
3726 (+len, buf) = p
3727 stream.mk(tls, s, ms, res, decs, Bool.pick(Pc, U32.is_zero(len), pc.eof(rb), pc.of(rb, Bytes.Bytes{len, buf})))
3728
3729def 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:
3730 (s, r) = m
3731 match r:
3732 case Fail{(+code, why)}:
3733 Stream{tls, s, ms, res, RbDone{}, PoBad{err.or_late(code, ErrRead{code, why})}, decs}
3734 case Done{p}:
3735 stream.got.piece(tls, s, ms, res, decs, rb, p)
3736
3737def stream.after(+rb: Rb) -> Po:
3738 match rb:
3739 case RbDone{}:
3740 PoEnd{}
3741 case RbBad{}:
3742 PoEnd{}
3743 case RbLen{n}:
3744 PoNone{}
3745 case RbChunk{st}:
3746 PoNone{}
3747 case RbClose{}:
3748 PoNone{}
3749
3750type Fed is Type:
3751 Fed{decs: List<&1, Zlib.Decoder>, body: Result<&1, &1, Err, Bytes.Bytes>}
3752
3753def stream.feed.received(done: List<&1, Zlib.Decoder>, m: Zlib.Decoder & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Fed:
3754 (d, r) = m
3755 match r:
3756 case Fail{e}:
3757 Fed{d <> done, Fail{ErrBad{}}}
3758 case Done{(+len, buf)}:
3759 Fed{d <> done, Done{Bytes.Bytes{len, buf}}}
3760
3761def stream.feed.step(st: Fed, d: Zlib.Decoder) -> IO(Fed):
3762 Fed{done, body} = st
3763 match body:
3764 case Fail{e}:
3765 IO.pure(Fed, Fed{d <> done, Fail{e}})
3766 case Done{b}:
3767 Bytes.Bytes{+len, buf} = b
3768 do IO<Fed>:
3769 m : Zlib.Decoder & Result<&1, &1, U32 & String, U32 & Array<U32>> <-
3770 Zlib.dec.feed.words(d, 16777216, len, buf)
3771 return stream.feed.received(done, m)
3772
3773def stream.feed.one(prev: IO(Fed), d: Zlib.Decoder) -> IO(Fed):
3774 do IO<Fed>:
3775 st : Fed <- prev
3776 stream.feed.step(st, d)
3777
3778def stream.feed.reverse(st: Fed) -> Fed:
3779 Fed{done, body} = st
3780 Fed{List.reverse(&1, Zlib.Decoder, done), body}
3781
3782def stream.feed.all(decs: List<&1, Zlib.Decoder>, b: Bytes.Bytes) -> IO(Fed):
3783 do IO<Fed>:
3784 st : Fed <- List.foldl(~&1, ~Zlib.Decoder, ~IO(Fed), ~stream.feed.one, decs,
3785 IO.pure(Fed, Fed{Nil{}, Done{b}}))
3786 return stream.feed.reverse(st)
3787
3788def stream.ready(empty: Bool, +rb: Rb, b: Bytes.Bytes) -> Po:
3789 match empty:
3790 case True{}:
3791 stream.after(rb)
3792 case False{}:
3793 PoReady{b}
3794
3795def stream.feed.got(+tls: Bool, s: Socket, +ms: U32, res: Res, +rb: Rb, st: Fed) -> Stream:
3796 Fed{decs, body} = st
3797 match body:
3798 case Fail{e}:
3799 Stream{tls, s, ms, res, rb, PoBad{e}, decs}
3800 case Done{b}:
3801 Bytes.Bytes{+len, buf} = b
3802 Stream{tls, s, ms, res, rb, stream.ready(U32.is_zero(len), rb, Bytes.Bytes{len, buf}), decs}
3803
3804def stream.feed.st(st: Stream, b: Bytes.Bytes) -> IO(Stream):
3805 Stream{+tls, s, +ms, res, +rb, out, decs} = st
3806 match decs:
3807 case Nil{}:
3808 IO.pure(Stream, Stream{tls, s, ms, res, rb, PoReady{b}, Nil{}})
3809 case Con{d, rest}:
3810 do IO<Stream>:
3811 fed : Fed <- stream.feed.all(Con{d, rest}, b)
3812 return stream.feed.got(tls, s, ms, res, rb, fed)
3813
3814def stream.finish.ok(r: Result<&1, &1, U32 & String, Unit>) -> Bool:
3815 match r:
3816 case Fail{e}:
3817 False{}
3818 case Done{u}:
3819 True{}
3820
3821def stream.finish(decs: List<&1, Zlib.Decoder>) -> IO(Bool):
3822 match decs:
3823 case Nil{}:
3824 IO.pure(Bool, True{})
3825 case Con{d, rest}:
3826 do IO<Bool>:
3827 r : Result<&1, &1, U32 & String, Unit> <- Zlib.dec.finish(d)
3828 tail : Bool <- stream.finish(rest)
3829 return Bool.and(stream.finish.ok(r), tail)
3830
3831def stream.ended(good: Bool, +tls: Bool, s: Socket, +ms: U32, res: Res, +rb: Rb) ->
3832 Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>:
3833 match good:
3834 case True{}:
3835 (Stream{tls, s, ms, res, rb, PoEnd{}, Nil{}}, Done{None{}})
3836 case False{}:
3837 (Stream{tls, s, ms, res, rb, PoBad{ErrBad{}}, Nil{}}, Fail{ErrBad{}})
3838
3839# The next piece of the body; None at the end. A piece is never empty.
3840@unsafe
3841def stream.read(st: Stream) -> IO(Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>):
3842 Stream{+tls, s, +ms, res, +rb, out, decs} = st
3843 match out:
3844 case PoPiece{b}:
3845 do IO<Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>>:
3846 next : Stream <- stream.feed.st(Stream{tls, s, ms, res, rb, PoNone{}, decs}, b)
3847 stream.read(next)
3848 case PoReady{b}:
3849 IO.pure(Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>,
3850 (Stream{tls, s, ms, res, rb, stream.after(rb), decs}, Done{Some{b}}))
3851 case PoEnd{}:
3852 do IO<Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>>:
3853 good : Bool <- stream.finish(decs)
3854 return stream.ended(good, tls, s, ms, res, rb)
3855 case PoBad{+e}:
3856 IO.pure(Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>,
3857 (Stream{tls, s, ms, res, rb, PoBad{e}, decs}, Fail{e}))
3858 case PoNone{}:
3859 do IO<Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>>:
3860 m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv.words(tls, s, 65536, ms)
3861 stream.read(stream.got(tls, ms, res, decs, rb, m))
3862
3863# Status and headers. Its body is empty: read the body with stream.read.
3864def stream.res(st: Stream) -> Stream & Res:
3865 Stream{tls, s, ms, res, rb, out, decs} = st
3866 Res{+status, +headers, body} = res
3867 (Stream{tls, s, ms, Res{status, headers, body}, rb, out, decs}, Res{status, headers, Bytes.new(0)})
3868
3869def stream.close(st: Stream) -> IO(Unit):
3870 Stream{tls, s, ms, res, rb, out, decs} = st
3871 do IO<Unit>:
3872 good : Bool <- stream.finish(decs)
3873 io.close(tls, s)
3874
3875# Head read state: still scanning, cut short or bad, or the head with the bytes after it.
3876type Sh is Type:
3877 ShMore{buf: Bytes.Bytes, k: U32}
3878 ShBad{err: Maybe<&2, Err>}
3879 ShRes{res: Res, rb: Rb, rest: Bytes.Bytes}
3880
3881def sh.of(hs: Hs) -> Sh:
3882 match hs:
3883 case HsWait{buf, k}:
3884 ShMore{buf, k}
3885 case HsBad{}:
3886 ShBad{None{}}
3887 case HsSeek{buf, from, k}:
3888 ShBad{None{}}
3889 case HsRes{res, rb, rest}:
3890 ShRes{res, rb, rest}
3891
3892def sh.piece(+head: Bool, buf: Bytes.Bytes, +k: U32, p: U32 & Array<U32>) -> Sh:
3893 (+len, b) = p
3894 Bool.pick(Sh, U32.is_zero(len), ShBad{None{}}, sh.of(hs.more(head, k, buf, Bytes.Bytes{len, b})))
3895
3896def sh.next(+head: Bool, buf: Bytes.Bytes, +k: U32, m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Socket & Sh:
3897 (s, r) = m
3898 match r:
3899 case Fail{(+code, why)}:
3900 (s, ShBad{Some{err.or_late(code, ErrRead{code, why})}})
3901 case Done{p}:
3902 (s, sh.piece(head, buf, k, p))
3903
3904def fetch.fail.of(r: Result<&1, &1, Err, Res>) -> Result<&1, &1, Err, Stream>:
3905 match r:
3906 case Fail{e}:
3907 Fail{e}
3908 case Done{res}:
3909 Fail{ErrBad{}}
3910
3911# Reads until the final head is in; the body bytes that came with it are the first piece.
3912@unsafe
3913def stream.head(+tls: Bool, +ms: U32, +head: Bool, st: Socket & Sh) -> IO(Result<&1, &1, Err, Stream>):
3914 (s, sh) = st
3915 match sh:
3916 case ShMore{buf, +k}:
3917 do IO<Result<&1, &1, Err, Stream>>:
3918 m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv.words(tls, s, 65536, ms)
3919 stream.head(tls, ms, head, sh.next(head, buf, k, m))
3920 case ShBad{err}:
3921 do IO<Result<&1, &1, Err, Stream>>:
3922 r : Result<&1, &1, Err, Res> <- fetch.bad(tls, s, err)
3923 return fetch.fail.of(r)
3924 case ShRes{res, rb, rest}:
3925 IO.pure(Result<&1, &1, Err, Stream>, Done{stream.mk(tls, s, ms, res, Nil{}, pc.of(rb, rest))})
3926
3927def stream.sent(+tls: Bool, +ms: U32, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Result<&1, &1, Err, Stream>):
3928 (s, r) = m
3929 match r:
3930 case Fail{(+code, why)}:
3931 do IO<Result<&1, &1, Err, Stream>>:
3932 io.close(tls, s)
3933 return Fail{err.or_late(code, ErrWrite{code, why})}
3934 case Done{u}:
3935 stream.head(tls, ms, head, (s, ShMore{Bytes.new(0), 0}))
3936
3937def stream.conn(r: Result<&1, &1, Err, Conn>, +ms: U32, +head: Bool, wire: Bytes.Bytes) -> IO(Result<&1, &1, Err, Stream>):
3938 match r:
3939 case Fail{e}:
3940 IO.pure(Result<&1, &1, Err, Stream>, Fail{e})
3941 case Done{c}:
3942 match c:
3943 case Conn{+tls, s}:
3944 do IO<Result<&1, &1, Err, Stream>>:
3945 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(tls, s, wire)
3946 stream.sent(tls, ms, head, sent)
3947 case ConnH2{s, client}:
3948 do IO<Result<&1, &1, Err, Stream>>:
3949 Wire.tls.close(s)
3950 return Fail{ErrBad{}}
3951
3952# One connection per stream; the request says close.
3953def stream.origin(+ms: U32, +head: Bool, wire: Bytes.Bytes, a: Url.Abs, known: Bool) -> IO(Result<&1, &1, Err, Stream>):
3954 Url.Abs{+scheme, +host, +port, target} = a
3955 match known:
3956 case False{}:
3957 IO.pure(Result<&1, &1, Err, Stream>, Fail{ErrUrl{}})
3958 case True{}:
3959 do IO<Result<&1, &1, Err, Stream>>:
3960 ips : List<&2, String> <- Dns.resolve.all(host)
3961 c : Result<&1, &1, Err, Conn> <- conn.open.all(String.eq(scheme, "https"), ms, host, port, ips, None{}, False{})
3962 stream.conn(c, ms, head, wire)
3963
3964def 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>):
3965 Url.Abs{scheme, host, port, +target} = url
3966 (body, wire) = r
3967 do IO<Hop & Result<&1, &1, Err, Stream>>:
3968 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))
3969 return (Hop{method, url, headers, body}, got)
3970
3971# One request on its own connection. The hop comes back for the redirect.
3972def stream.one(h: Hop, +ms: U32) -> IO(Hop & Result<&1, &1, Err, Stream>):
3973 Hop{+method, +url, +headers, body} = h
3974 stream.one.of(method, url, headers, ms, Bytes.slice(body, 0, 4294967295))
3975
3976# Go: the next request. Drop: close this stream, then go on. Done: the answer.
3977type Sn is Type:
3978 SnGo{left: Nat, hop: Hop}
3979 SnDrop{st: Stream, next: Next}
3980 SnDone{r: Result<&1, &1, Err, Stream>}
3981
3982def sn.of(n: Next) -> Sn:
3983 match n:
3984 case NGo{l, h}:
3985 SnGo{l, h}
3986 case NStop{}:
3987 SnDone{Fail{ErrRedirect{}}}
3988 case NDone{m}:
3989 match m:
3990 case Fail{e}:
3991 SnDone{Fail{e}}
3992 case Done{r}:
3993 SnDone{Fail{ErrBad{}}}
3994
3995def stream.decide.n(st: Stream, n: Next) -> Sn:
3996 match n:
3997 case NDone{m}:
3998 SnDone{Done{st}}
3999 case NGo{l, h}:
4000 SnDrop{st, NGo{l, h}}
4001 case NStop{}:
4002 SnDrop{st, NStop{}}
4003
4004def stream.decide.of(+left: Nat, hop: Hop, sr: Stream & Res) -> Sn:
4005 (st, res) = sr
4006 stream.decide.n(st, fetch.decide(left, hop, Done{res}))
4007
4008def stream.decide(+left: Nat, x: Hop & Result<&1, &1, Err, Stream>) -> Sn:
4009 (hop, r) = x
4010 match r:
4011 case Fail{e}:
4012 SnDone{Fail{e}}
4013 case Done{st}:
4014 stream.decide.of(left, hop, stream.res(st))
4015
4016@unsafe
4017def stream.hops(+ms: U32, sn: Sn) -> IO(Result<&1, &1, Err, Stream>):
4018 match sn:
4019 case SnDone{r}:
4020 IO.pure(Result<&1, &1, Err, Stream>, r)
4021 case SnGo{+left, hop}:
4022 do IO<Result<&1, &1, Err, Stream>>:
4023 x : Hop & Result<&1, &1, Err, Stream> <- stream.one(hop, ms)
4024 stream.hops(ms, stream.decide(left, x))
4025 case SnDrop{st, next}:
4026 do IO<Result<&1, &1, Err, Stream>>:
4027 stream.close(st)
4028 stream.hops(ms, sn.of(next))
4029
4030type Opened is Type:
4031 Opened{decs: List<&1, Zlib.Decoder>, bad: Bool}
4032
4033def stream.open.got(st: Opened, r: Result<&1, &1, U32 & String, Zlib.Decoder>) -> Opened:
4034 Opened{decs, bad} = st
4035 match r:
4036 case Fail{e}:
4037 Opened{decs, True{}}
4038 case Done{d}:
4039 Opened{d <> decs, bad}
4040
4041def stream.open.add(st: Opened, m: IO(Result<&1, &1, U32 & String, Zlib.Decoder>)) -> IO(Opened):
4042 do IO<Opened>:
4043 r : Result<&1, &1, U32 & String, Zlib.Decoder> <- m
4044 return stream.open.got(st, r)
4045
4046def stream.open.zstd(zstd: Bool, st: Opened) -> IO(Opened):
4047 match zstd:
4048 case True{}:
4049 stream.open.add(st, Zlib.zstd.new())
4050 case False{}:
4051 IO.pure(Opened, st)
4052
4053def stream.open.br(br: Bool, +c: String, st: Opened) -> IO(Opened):
4054 match br:
4055 case True{}:
4056 stream.open.add(st, Zlib.brotli.new())
4057 case False{}:
4058 stream.open.zstd(String.eq(c, "zstd"), st)
4059
4060def stream.open.gz(gz: Bool, +c: String, st: Opened) -> IO(Opened):
4061 match gz:
4062 case True{}:
4063 stream.open.add(st, Zlib.inflate.new())
4064 case False{}:
4065 stream.open.br(String.eq(c, "br"), c, st)
4066
4067def stream.open.step(+c: String, st: Opened) -> IO(Opened):
4068 Opened{decs, bad} = st
4069 match bad:
4070 case True{}:
4071 IO.pure(Opened, Opened{decs, True{}})
4072 case False{}:
4073 stream.open.gz(Bool.or(String.eq(c, "gzip"), Bool.or(String.eq(c, "x-gzip"), String.eq(c, "deflate"))),
4074 c, Opened{decs, False{}})
4075
4076def stream.open.one(prev: IO(Opened), c: String) -> IO(Opened):
4077 do IO<Opened>:
4078 st : Opened <- prev
4079 stream.open.step(c, st)
4080
4081def stream.open.all(cs: List<&2, String>) -> IO(Opened):
4082 List.foldl(~&2, ~String, ~IO(Opened), ~stream.open.one, cs, IO.pure(Opened, Opened{Nil{}, False{}}))
4083
4084def stream.put.decs(st: Stream, decs: List<&1, Zlib.Decoder>) -> Stream:
4085 Stream{tls, s, ms, res, rb, out, old} = st
4086 Stream{tls, s, ms, res, rb, out, decs}
4087
4088def stream.init.opened(st: Stream, opened: Opened) -> IO(Result<&1, &1, Err, Stream>):
4089 Opened{decs, bad} = opened
4090 match bad:
4091 case True{}:
4092 do IO<Result<&1, &1, Err, Stream>>:
4093 stream.close(stream.put.decs(st, decs))
4094 return Fail{ErrBad{}}
4095 case False{}:
4096 IO.pure(Result<&1, &1, Err, Stream>, Done{stream.put.decs(st, List.reverse(&1, Zlib.Decoder, decs))})
4097
4098def stream.init.known(known: Bool, st: Stream, cs: List<&2, String>) -> IO(Result<&1, &1, Err, Stream>):
4099 match known:
4100 case False{}:
4101 IO.pure(Result<&1, &1, Err, Stream>, Done{st})
4102 case True{}:
4103 do IO<Result<&1, &1, Err, Stream>>:
4104 opened : Opened <- stream.open.all(cs)
4105 stream.init.opened(st, opened)
4106
4107def stream.init.st(+enc: String, st: Stream) -> IO(Result<&1, &1, Err, Stream>):
4108 Stream{tls, s, ms, res, rb, out, decs} = st
4109 Res{+status, +headers, body} = res
4110 +cs = List.reverse(&2, String, ce.split(fields(headers, "content-encoding")))
4111 stream.init.known(ce.known(cs, Con{"identity", Con{"x-gzip", ce.split(Con{enc, Nil{}})}}),
4112 Stream{tls, s, ms, Res{status, headers, body}, rb, out, decs}, cs)
4113
4114def stream.init(+enc: String, r: Result<&1, &1, Err, Stream>) -> IO(Result<&1, &1, Err, Stream>):
4115 match r:
4116 case Fail{e}:
4117 IO.pure(Result<&1, &1, Err, Stream>, Fail{e})
4118 case Done{st}:
4119 stream.init.st(enc, st)
4120
4121def stream.start(method: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, u: Maybe<&2, Url.Abs>) -> Sn:
4122 match u:
4123 case None{}:
4124 SnDone{Fail{ErrUrl{}}}
4125 case Some{a}:
4126 SnGo{20n, Hop{method, a, req.put(Map.to_list(&2, List<&2, String>, headers), empty()), body}}
4127
4128# Open a raw stream. Its body bytes and headers remain as sent.
4129def open.raw.with(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, +ms: U32) -> IO(Result<&1, &1, Err, Stream>):
4130 stream.hops(ms, stream.start(method, headers, body, Url.absolute(url)))
4131
4132def open.raw(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Stream>):
4133 open.raw.with(method, url, headers, body, 30000)
4134
4135def 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>):
4136 do IO<Result<&1, &1, Err, Stream>>:
4137 r : Result<&1, &1, Err, Stream> <-
4138 stream.hops(ms, stream.start(method, accept.enc(headers, enc), body, Url.absolute(url)))
4139 stream.init(enc, r)
4140
4141# Follow redirects, then decode each body piece by Content-Encoding. Unknown codings stay raw.
4142def open.with(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, +ms: U32) -> IO(Result<&1, &1, Err, Stream>):
4143 do IO<Result<&1, &1, Err, Stream>>:
4144 enc : String <- codings()
4145 open.with.enc(enc, method, url, headers, body, ms)
4146
4147def open(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Stream>):
4148 open.with(method, url, headers, body, 30000)
4149
4150# Upload: the request body sent in chunks (RFC 9112 §7.1). err: the first failed write.
4151type Up is Type:
4152 Up{tls: Bool, s: Socket, ms: U32, head: Bool, err: Maybe<&2, Err>}
4153
4154def hex.digit(+n: U32) -> Char:
4155 Chr{Bool.pick(U32, U32.is_lt(n, 10), (48 + n : U32), (87 + n : U32))}
4156
4157def hex.go(k: Nat, +n: U32, acc: String) -> String:
4158 match k:
4159 case 0n:
4160 acc
4161 case 1n+p:
4162 hex.go(p, U32.shrn(n, 4n), SCon{hex.digit(U32.and(n, 15)), acc})
4163
4164def hex.trim(+s: String) -> String:
4165 match s:
4166 case SNil{}:
4167 SNil{}
4168 case SCon{Chr{+c}, +t}:
4169 Bool.pick(String, Bool.and(U32.is_eq(c, 48), Bool.not(String.is_empty(t))), hex.trim(t), SCon{Chr{c}, t})
4170
4171def hex(+n: U32) -> String:
4172 hex.trim(hex.go(8n, n, ""))
4173
4174def up.sent(+tls: Bool, +ms: U32, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> Up:
4175 (s, r) = m
4176 match r:
4177 case Fail{(+code, why)}:
4178 Up{tls, s, ms, head, Some{err.or_late(code, ErrWrite{code, why})}}
4179 case Done{u}:
4180 Up{tls, s, ms, head, None{}}
4181
4182def up.conn(r: Result<&1, &1, Err, Conn>, +ms: U32, +head: Bool, wire: String) -> IO(Result<&1, &1, Err, Up>):
4183 match r:
4184 case Fail{e}:
4185 IO.pure(Result<&1, &1, Err, Up>, Fail{e})
4186 case Done{c}:
4187 match c:
4188 case Conn{+tls, s}:
4189 do IO<Result<&1, &1, Err, Up>>:
4190 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send(tls, s, wire)
4191 return Done{up.sent(tls, ms, head, sent)}
4192 case ConnH2{s, client}:
4193 do IO<Result<&1, &1, Err, Up>>:
4194 Wire.tls.close(s)
4195 return Fail{ErrBad{}}
4196
4197def up.head(+method: String, +target: String, +hf: String, +headers: Map<&2, List<&2, String>>) -> String:
4198 request(method, target, set(set(set(req.put(Map.to_list(&2, List<&2, String>, headers), empty()), "host", hf), "connection", "close"), "transfer-encoding", "chunked"), "")
4199
4200def up.origin(+method: String, +ms: U32, headers: Map<&2, List<&2, String>>, a: Url.Abs, known: Bool) -> IO(Result<&1, &1, Err, Up>):
4201 Url.Abs{+scheme, +host, +port, +target} = a
4202 match known:
4203 case False{}:
4204 IO.pure(Result<&1, &1, Err, Up>, Fail{ErrUrl{}})
4205 case True{}:
4206 do IO<Result<&1, &1, Err, Up>>:
4207 ips : List<&2, String> <- Dns.resolve.all(host)
4208 c : Result<&1, &1, Err, Conn> <- conn.open.all(String.eq(scheme, "https"), ms, host, port, ips, None{}, False{})
4209 up.conn(c, ms, String.eq(method, "HEAD"), up.head(method, target, Url.host_field(a), headers))
4210
4211def up.url(+method: String, +ms: U32, headers: Map<&2, List<&2, String>>, u: Maybe<&2, Url.Abs>) -> IO(Result<&1, &1, Err, Up>):
4212 match u:
4213 case None{}:
4214 IO.pure(Result<&1, &1, Err, Up>, Fail{ErrUrl{}})
4215 case Some{+a}:
4216 up.origin(method, ms, headers, a, pool.scheme.ok(a))
4217
4218# Http.upload(method, url, headers) sends the head. A streamed body cannot be replayed, so redirects are not followed.
4219def upload.with(+method: String, url: String, headers: Map<&2, List<&2, String>>, +ms: U32) -> IO(Result<&1, &1, Err, Up>):
4220 up.url(method, ms, headers, Url.absolute(url))
4221
4222def upload(+method: String, url: String, headers: Map<&2, List<&2, String>>) -> IO(Result<&1, &1, Err, Up>):
4223 upload.with(method, url, headers, 30000)
4224
4225def up.wrote(+tls: Bool, +ms: U32, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> Up & Result<&2, &2, Err, Unit>:
4226 (s, r) = m
4227 match r:
4228 case Fail{(+code, why)}:
4229 +e = err.or_late(code, ErrWrite{code, why})
4230 (Up{tls, s, ms, head, Some{e}}, Fail{e})
4231 case Done{u}:
4232 (Up{tls, s, ms, head, None{}}, Done{Unit{}})
4233
4234# One write per chunk, so the size line and the data do not wait on each other (Nagle).
4235def up.put(+tls: Bool, s: Socket, +ms: U32, +head: Bool, +len: U32, piece: Bytes.Bytes, skip: Bool) -> IO(Up & Result<&2, &2, Err, Unit>):
4236 match skip:
4237 case True{}:
4238 IO.pure(Up & Result<&2, &2, Err, Unit>, (Up{tls, s, ms, head, None{}}, Done{Unit{}}))
4239 case False{}:
4240 do IO<Up & Result<&2, &2, Err, Unit>>:
4241 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{}}}}))
4242 return up.wrote(tls, ms, head, sent)
4243
4244def up.chunk(+tls: Bool, s: Socket, +ms: U32, +head: Bool, piece: Bytes.Bytes) -> IO(Up & Result<&2, &2, Err, Unit>):
4245 Bytes.Bytes{+len, buf} = piece
4246 up.put(tls, s, ms, head, len, Bytes.Bytes{len, buf}, U32.is_zero(len))
4247
4248# One chunk. An empty piece sends nothing, since an empty chunk would end the body.
4249def upload.write(up: Up, piece: Bytes.Bytes) -> IO(Up & Result<&2, &2, Err, Unit>):
4250 Up{+tls, s, +ms, +head, err} = up
4251 match err:
4252 case Some{+e}:
4253 IO.pure(Up & Result<&2, &2, Err, Unit>, (Up{tls, s, ms, head, Some{e}}, Fail{e}))
4254 case None{}:
4255 up.chunk(tls, s, ms, head, piece)
4256
4257# Ends the body and returns the response as a stream.
4258def upload.finish(up: Up) -> IO(Result<&1, &1, Err, Stream>):
4259 Up{+tls, s, +ms, +head, err} = up
4260 match err:
4261 case Some{e}:
4262 do IO<Result<&1, &1, Err, Stream>>:
4263 io.close(tls, s)
4264 return Fail{e}
4265 case None{}:
4266 do IO<Result<&1, &1, Err, Stream>>:
4267 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send(tls, s, "0\r\n\r\n")
4268 stream.sent(tls, ms, head, sent)
4269
4270def reply.bytes(res: Res, head: Bool, close: Bool) -> Bytes.Bytes:
4271 Res{+status, +headers, body} = res
4272 encode.on(Res{status, Bool.pick(Map<&2, List<&2, String>>, close, set(headers, "connection", "close"), headers), body}, head)
4273
4274def reply.fail.bytes(+status: U32) -> Res:
4275 Res{status, empty(), Bytes.from_string(reason(status))}
4276
4277def reply.sent.close(m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Unit):
4278 (s, r) = m
4279 Socket.close(s)
4280
4281def reply_fail(s: Socket, +status: U32) -> IO(Unit):
4282 do IO<Unit>:
4283 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(False{}, s, encode(reply.fail.bytes(status)))
4284 reply.sent.close(sent)
4285
4286
4287# The head is parsed once, when it is whole. Body pieces are kept as they come and joined once.
4288type Sv is Type:
4289 SvHead{buf: Bytes.Bytes}
4290 SvLen{req: Req, v11: Bool, left: U32, parts: List<&1, Bytes.Bytes>}
4291 SvChunk{req: Req, v11: Bool, n: U32, st: Dc, parts: List<&1, Bytes.Bytes>}
4292
4293# More: read on, first answering 100 Continue when cont is set.
4294type Turn is Type:
4295 TurnClose{}
4296 TurnFail{status: U32}
4297 TurnReq{req: Req, rest: Bytes.Bytes, v11: Bool}
4298 TurnMore{sv: Sv, cont: Bool}
4299
4300def serve.max() -> Nat:
4301 fetch.max()
4302
4303def sv.none() -> Sv:
4304 SvHead{Bytes.new(0)}
4305
4306def sv.body(req: Req, +v11: Bool, parts: List<&1, Bytes.Bytes>, rest: Bytes.Bytes) -> Turn:
4307 Req{method, path, headers, body} = req
4308 TurnReq{Req{method, path, headers, rb.body(parts)}, rest, v11}
4309
4310def sv.len.cut(req: Req, +v11: Bool, parts: List<&1, Bytes.Bytes>, +len: U32, +left: U32, r: Bytes.Bytes & Bytes.Bytes) -> Turn:
4311 (piece, last) = r
4312 sv.body(req, v11, Con{last, parts}, bytes.snd(Bytes.slice(piece, left, (len - left : U32))))
4313
4314def sv.len.have(short: Bool, req: Req, +v11: Bool, +left: U32, parts: List<&1, Bytes.Bytes>, +len: U32, piece: Bytes.Bytes) -> Turn:
4315 match short:
4316 case True{}:
4317 TurnMore{SvLen{req, v11, (left - len : U32), Con{piece, parts}}, False{}}
4318 case False{}:
4319 sv.len.cut(req, v11, parts, len, left, Bytes.slice(piece, 0, left))
4320
4321def sv.len(req: Req, +v11: Bool, +left: U32, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Turn:
4322 Bytes.Bytes{+len, buf} = piece
4323 sv.len.have(U32.is_lt(len, left), req, v11, left, parts, len, Bytes.Bytes{len, buf})
4324
4325def sv.chunk.of(req: Req, +v11: Bool, +n: U32, c: Ck) -> Turn:
4326 Ck{st, parts, rest} = c
4327 match st:
4328 case DcDone{}:
4329 sv.body(req, v11, parts, rest)
4330 case DcBad{}:
4331 TurnFail{400}
4332 case DcSize{a, b}:
4333 TurnMore{SvChunk{req, v11, n, DcSize{a, b}, parts}, False{}}
4334 case DcExt{x}:
4335 TurnMore{SvChunk{req, v11, n, DcExt{x}, parts}, False{}}
4336 case DcSizeLf{x}:
4337 TurnMore{SvChunk{req, v11, n, DcSizeLf{x}, parts}, False{}}
4338 case DcData{k}:
4339 TurnMore{SvChunk{req, v11, n, DcData{k}, parts}, False{}}
4340 case DcDataCr{}:
4341 TurnMore{SvChunk{req, v11, n, DcDataCr{}, parts}, False{}}
4342 case DcDataLf{}:
4343 TurnMore{SvChunk{req, v11, n, DcDataLf{}, parts}, False{}}
4344 case DcTr{j}:
4345 TurnMore{SvChunk{req, v11, n, DcTr{j}, parts}, False{}}
4346
4347def sv.chunk.cap(big: Bool, req: Req, +v11: Bool, +n: U32, st: Dc, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Turn:
4348 match big:
4349 case True{}:
4350 TurnFail{413}
4351 case False{}:
4352 sv.chunk.of(req, v11, n, ck(piece, st, parts))
4353
4354def sv.chunk(+max: Nat, req: Req, +v11: Bool, +n: U32, st: Dc, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Turn:
4355 Bytes.Bytes{+len, buf} = piece
4356 +n2 = (n + len : U32)
4357 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})
4358
4359# RFC 9110 §10.1.1: answer 100 Continue only when the body is still to come.
4360def sv.cont(want: Bool, t: Turn) -> Turn:
4361 match t:
4362 case TurnMore{sv, c}:
4363 TurnMore{sv, want}
4364 case TurnClose{}:
4365 TurnClose{}
4366 case TurnFail{s}:
4367 TurnFail{s}
4368 case TurnReq{req, rest, v11}:
4369 TurnReq{req, rest, v11}
4370
4371def sv.cl.k(big: Bool, req: Req, +v11: Bool, +k: U32, rest: Bytes.Bytes) -> Turn:
4372 match big:
4373 case True{}:
4374 TurnFail{413}
4375 case False{}:
4376 sv.len(req, v11, k, Nil{}, rest)
4377
4378def sv.cl(+max: Nat, req: Req, +v11: Bool, rest: Bytes.Bytes, n: Maybe<&2, U32>) -> Turn:
4379 match n:
4380 case None{}:
4381 TurnFail{400}
4382 case Some{+k}:
4383 sv.cl.k(Nat.is_lt(max, U32.to_nat(k)), req, v11, k, rest)
4384
4385def sv.frame(+max: Nat, req: Req, +v11: Bool, rest: Bytes.Bytes, te: Bool) -> Turn:
4386 Req{method, path, +headers, body} = req
4387 match te:
4388 case True{}:
4389 sv.chunk(max, Req{method, path, headers, body}, v11, 0, dc.start(), Nil{}, rest)
4390 case False{}:
4391 sv.cl(max, Req{method, path, headers, body}, v11, rest, parse_u32(header(headers, "content-length")))
4392
4393def sv.expects(+v11: Bool, +headers: Map<&2, List<&2, String>>) -> Bool:
4394 Bool.and(v11, String.eq(String.to_lower(header(headers, "expect")), "100-continue"))
4395
4396def sv.got.head(+max: Nat, +v11: Bool, rest: Bytes.Bytes, req: Req) -> Turn:
4397 Req{method, path, +headers, body} = req
4398 sv.cont(sv.expects(v11, headers), sv.frame(max, Req{method, path, headers, body}, v11, rest, has_header(headers, "transfer-encoding")))
4399
4400def sv.parsed(+max: Nat, +v11: Bool, rest: Bytes.Bytes, g: Got) -> Turn:
4401 match g:
4402 case GotBad{}:
4403 TurnFail{400}
4404 case GotMore{}:
4405 TurnFail{400}
4406 case GotReq{req}:
4407 TurnReq{req, rest, v11}
4408 case GotHead{req}:
4409 sv.got.head(max, v11, rest, req)
4410
4411def sv.split(+max: Nat, +hlen: U32, +len: U32, r: Bytes.Bytes & Bytes.Bytes) -> Turn:
4412 (buf, hb) = r
4413 +head = Bytes.to_string(hb)
4414 sv.parsed(max, req.v11(head), bytes.snd(Bytes.slice(buf, hlen, (len - hlen : U32))), parse.got(head))
4415
4416def sv.hit.none(big: Bool, buf: Bytes.Bytes) -> Turn:
4417 match big:
4418 case True{}:
4419 TurnFail{431}
4420 case False{}:
4421 TurnMore{SvHead{buf}, False{}}
4422
4423def sv.hit.some(big: Bool, +max: Nat, +hlen: U32, +len: U32, buf: Bytes.Bytes) -> Turn:
4424 match big:
4425 case True{}:
4426 TurnFail{431}
4427 case False{}:
4428 sv.split(max, hlen, len, Bytes.slice(buf, 0, hlen))
4429
4430# RFC 6585 §5: a head over 64 KiB is refused.
4431def sv.hit(+max: Nat, +len: U32, buf: Bytes.Bytes, at: Maybe<&2, U32>) -> Turn:
4432 match at:
4433 case None{}:
4434 sv.hit.none(U32.is_lt(65536, len), buf)
4435 case Some{+i}:
4436 +hlen = (i + 4 : U32)
4437 sv.hit.some(U32.is_lt(65536, hlen), max, hlen, len, buf)
4438
4439def sv.seek.of(+max: Nat, +len: U32, +from: U32, buf: Bytes.Bytes, r: Bytes.Bytes & Maybe<&2, U32>) -> Turn:
4440 (tail, m) = r
4441 sv.hit(max, len, buf, found.at(from, m))
4442
4443def sv.seek(+max: Nat, +len: U32, +from: U32, r: Bytes.Bytes & Bytes.Bytes) -> Turn:
4444 (buf, tail) = r
4445 sv.seek.of(max, len, from, buf, Bytes.find(tail, "\r\n\r\n"))
4446
4447# Only the new bytes, and the 3 before them, can finish the blank line.
4448def sv.head.at(+max: Nat, +from: U32, buf: Bytes.Bytes) -> Turn:
4449 Bytes.Bytes{+len, b} = buf
4450 sv.seek(max, len, from, Bytes.slice(Bytes.Bytes{len, b}, from, (len - from : U32)))
4451
4452def sv.head(+max: Nat, buf: Bytes.Bytes, piece: Bytes.Bytes) -> Turn:
4453 Bytes.Bytes{+ol, ob} = buf
4454 sv.head.at(max, Bool.pick(U32, U32.is_lt(ol, 3), 0, (ol - 3 : U32)), Bytes.append(Bytes.Bytes{ol, ob}, piece))
4455
4456def sv.closed.pick(empty: Bool) -> Turn:
4457 match empty:
4458 case True{}:
4459 TurnClose{}
4460 case False{}:
4461 TurnFail{400}
4462
4463def sv.closed.head(buf: Bytes.Bytes) -> Turn:
4464 Bytes.Bytes{+len, b} = buf
4465 sv.closed.pick(U32.is_eq(len, 0))
4466
4467# A close mid-request is a request cut short (RFC 9112 §8).
4468def sv.step(closed: Bool, +max: Nat, sv: Sv, piece: Bytes.Bytes) -> Turn:
4469 match closed:
4470 case True{}:
4471 match sv:
4472 case SvHead{buf}:
4473 sv.closed.head(buf)
4474 case SvLen{req, v11, left, parts}:
4475 TurnFail{400}
4476 case SvChunk{req, v11, n, st, parts}:
4477 TurnFail{400}
4478 case False{}:
4479 match sv:
4480 case SvHead{buf}:
4481 sv.head(max, buf, piece)
4482 case SvLen{req, +v11, +left, parts}:
4483 sv.len(req, v11, left, parts, piece)
4484 case SvChunk{req, +v11, +n, st, parts}:
4485 sv.chunk(max, req, v11, n, st, parts, piece)
4486
4487def sv.frame.req(t: Turn) -> Maybe<&1, String & String>:
4488 match t:
4489 case TurnReq{req, rest, v11}:
4490 Req{method, path, headers, body} = req
4491 Some{(Bytes.to_string(body), Bytes.to_string(rest))}
4492 case TurnMore{sv, c}:
4493 None{}
4494 case TurnFail{s}:
4495 None{}
4496 case TurnClose{}:
4497 None{}
4498
4499def sv.frame.go(xs: List<&2, String>, t: Turn) -> Maybe<&1, String & String>:
4500 match xs:
4501 case Nil{}:
4502 sv.frame.req(t)
4503 case Con{+x, rest}:
4504 match t:
4505 case TurnMore{sv, c}:
4506 sv.frame.go(rest, sv.step(False{}, serve.max(), sv, Bytes.from_string(x)))
4507 case TurnReq{req, r, v11}:
4508 sv.frame.req(TurnReq{req, r, v11})
4509 case TurnFail{s}:
4510 None{}
4511 case TurnClose{}:
4512 None{}
4513
4514# The body and the bytes after it, once the pieces make a whole request; None otherwise.
4515def serve.frame(xs: List<&2, String>) -> Maybe<&1, String & String>:
4516 sv.frame.go(xs, TurnMore{sv.none(), False{}})
4517
4518def talk.piece(+max: Nat, sv: Sv, p: U32 & Array<U32>) -> Turn:
4519 (+len, buf) = p
4520 sv.step(U32.is_eq(len, 0), max, sv, Bytes.Bytes{len, buf})
4521
4522def talk.next(+max: Nat, sv: Sv, m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Socket & Turn:
4523 (s, r) = m
4524 match r:
4525 case Fail{e}:
4526 (s, TurnClose{})
4527 case Done{p}:
4528 (s, talk.piece(max, sv, p))
4529
4530def talk.after.pick(empty: Bool, +max: Nat, rest: Bytes.Bytes) -> Turn:
4531 match empty:
4532 case True{}:
4533 TurnMore{sv.none(), False{}}
4534 case False{}:
4535 sv.step(False{}, max, sv.none(), rest)
4536
4537def talk.after.rest(+max: Nat, rest: Bytes.Bytes, s: Socket) -> Socket & Turn:
4538 Bytes.Bytes{+len, buf} = rest
4539 (s, talk.after.pick(U32.is_eq(len, 0), max, Bytes.Bytes{len, buf}))
4540
4541def talk.after.keep(keep: Bool, +max: Nat, rest: Bytes.Bytes, s: Socket) -> Socket & Turn:
4542 match keep:
4543 case False{}:
4544 (s, TurnClose{})
4545 case True{}:
4546 talk.after.rest(max, rest, s)
4547
4548def talk.after(+max: Nat, keep: Bool, rest: Bytes.Bytes, m: Socket & Result<&1, &1, U32 & String, Unit>) -> Socket & Turn:
4549 (s, r) = m
4550 match r:
4551 case Fail{e}:
4552 (s, TurnClose{})
4553 case Done{u}:
4554 talk.after.keep(keep, max, rest, s)
4555
4556def talk.send(+max: Nat, s: Socket, rest: Bytes.Bytes, +headers: Map<&2, List<&2, String>>, v11: Bool, +head: Bool, res: Res) -> IO(Socket & Turn):
4557 Res{+status, +rh, body} = res
4558 +keep = serve.keep(headers, v11, status, rh)
4559 do IO<Socket & Turn>:
4560 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(False{}, s, reply.bytes(Res{status, rh, body}, head, Bool.not(keep)))
4561 return talk.after(max, keep, rest, sent)
4562
4563def talk.cont.sent(m: Socket & Result<&1, &1, U32 & String, Unit>) -> Socket:
4564 (s, r) = m
4565 s
4566
4567def talk.cont(cont: Bool, s: Socket) -> IO(Socket):
4568 match cont:
4569 case False{}:
4570 IO.pure(Socket, s)
4571 case True{}:
4572 do IO<Socket>:
4573 sent : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.send(s, "HTTP/1.1 100 Continue\r\n\r\n")
4574 return talk.cont.sent(sent)
4575
4576@unsafe
4577def talk(~h: Req -> IO(Res), +max: Nat, st: Socket & Turn) -> IO(Unit):
4578 (s, t) = st
4579 match t:
4580 case TurnMore{sv, cont}:
4581 do IO<Unit>:
4582 s2 : Socket <- talk.cont(cont, s)
4583 m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- Wire.recv.words(s2, 65536, 30000)
4584 talk(~h, max, talk.next(max, sv, m))
4585 case TurnReq{req, rest, v11}:
4586 Req{+method, path, +headers, body} = req
4587 do IO<Unit>:
4588 res : Res <- h(Req{method, path, headers, body})
4589 next : Socket & Turn <- talk.send(max, s, rest, headers, v11, String.eq(method, "HEAD"), res)
4590 talk(~h, max, next)
4591 case TurnFail{status}:
4592 reply_fail(s, status)
4593 case TurnClose{}:
4594 Socket.close(s)
4595
4596def conn(~h: Req -> IO(Res), +max: Nat, m: Listener & Result<&1, &1, U32 & String, Socket>) -> IO(Listener):
4597 (l, r) = m
4598 do IO<Listener>:
4599 s : Socket <- IO.pass(Socket, r)
4600 IO.spawn(Unit, talk(~h, max, (s, TurnMore{sv.none(), False{}})))
4601 return l
4602
4603@unsafe
4604def loop(~h: Req -> IO(Res), +max: Nat, l: Listener) -> IO(Unit):
4605 do IO<Unit>:
4606 m : Listener & Result<&1, &1, U32 & String, Socket> <- TCP.accept(l)
4607 l2 : Listener <- conn(~h, max, m)
4608 loop(~h, max, l2)
4609
4610def serve.with(~h: Req -> IO(Res), +port: U32, +max: Nat) -> IO(Unit):
4611 do IO<Unit>:
4612 l : Listener <- IO.try(Listener, TCP.listen(port))
4613 IO.print("http://127.0.0.1:" ++ U32.show(port))
4614 loop(~h, max, l)
4615
4616def serve(~h: Req -> IO(Res), +port: U32) -> IO(Unit):
4617 serve.with(~h, port, serve.max())