http.bend
bend-kit-http@0.20.1.0 · 4,238 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
1946# Connection pool: idle sockets by origin and client identity, newest first, at most cap per key.
1947# fetch uses a fresh pool per call.
1948
1949type Conn is Type:
1950 Conn{tls: Bool, s: Socket}
1951 ConnH2{s: Socket, client: H2.Client}
1952
1953type Send is Type:
1954 Send{method: String, target: String, authority: String,
1955 headers: Map<&2, List<&2, String>>, body: Bytes.Bytes}
1956
1957type H2Step is Type:
1958 H2Reply{s: Socket, reply: H2.Reply}
1959 H2Sent{client: H2.Client, events: List<&1, H2.ClientEvent>,
1960 sent: Result<&1, &1, Err, Socket>}
1961 H2Events{s: Socket, client: H2.Client, result: Result<&1, &1, Err, Maybe<&1, Res>>}
1962 H2Received{client: H2.Client,
1963 answer: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>}
1964
1965type Pool is Type:
1966 Pool{cap: U32, idle: Map<&1, List<&1, Conn>>}
1967
1968def pool.new.with(+cap: U32) -> Pool:
1969 Pool{cap, Map.new(&1, List<&1, Conn>)}
1970
1971# Up to 8 idle sockets per origin.
1972def pool.new() -> Pool:
1973 pool.new.with(8)
1974
1975def pool.key(+scheme: String, +host: String, +port: U32) -> String:
1976 scheme ++ "://" ++ host ++ ":" ++ U32.show(port)
1977
1978def pool.key.cert(+base: String, cert: Maybe<&2, Cert>) -> String:
1979 match cert:
1980 case None{}:
1981 base
1982 case Some{Cert{+chain, +key}}:
1983 base ++ "|cert:" ++ Nat.show(String.length(chain)) ++ ":" ++ chain
1984 ++ Nat.show(String.length(key)) ++ ":" ++ key
1985
1986def pool.take.of(+cap: U32, +key: String, r: Map<&1, List<&1, Conn>> & Maybe<&1, List<&1, Conn>>) -> Pool & Maybe<&1, Conn>:
1987 (m, got) = r
1988 match got:
1989 case None{}:
1990 (Pool{cap, m}, None{})
1991 case Some{xs}:
1992 match xs:
1993 case Nil{}:
1994 (Pool{cap, m}, None{})
1995 case Con{c, t}:
1996 (Pool{cap, Map.set(&1, List<&1, Conn>, m, key, t)}, Some{c})
1997
1998# The socket given back last.
1999def pool.take(p: Pool, +key: String) -> Pool & Maybe<&1, Conn>:
2000 Pool{+cap, idle} = p
2001 pool.take.of(cap, key, Map.pop(&1, List<&1, Conn>, idle, key))
2002
2003def conn.close(c: Conn) -> IO(Unit):
2004 match c:
2005 case Conn{tls, s}:
2006 io.close(tls, s)
2007 case ConnH2{s, client}:
2008 Wire.tls.close(s)
2009
2010# The first n sockets; the rest are closed.
2011def conns.cut(xs: List<&1, Conn>, n: Nat) -> IO(List<&1, Conn>):
2012 match xs:
2013 case Nil{}:
2014 IO.pure(List<&1, Conn>, Nil{})
2015 case Con{c, t}:
2016 match n:
2017 case 0n:
2018 do IO<List<&1, Conn>>:
2019 conn.close(c)
2020 conns.cut(t, 0n)
2021 case 1n+k:
2022 do IO<List<&1, Conn>>:
2023 r : List<&1, Conn> <- conns.cut(t, k)
2024 return c <> r
2025
2026def pool.give.of(+cap: U32, +key: String, c: Conn, limit: Nat,
2027 r: Map<&1, List<&1, Conn>> & Maybe<&1, List<&1, Conn>>) -> IO(Pool):
2028 (m, old) = r
2029 do IO<Pool>:
2030 xs : List<&1, Conn> <- conns.cut(c <> Maybe.default(&1, List<&1, Conn>, old, Nil{}), limit)
2031 return Pool{cap, Map.set(&1, List<&1, Conn>, m, key, xs)}
2032
2033# Past the limit (cap for HTTP/1.1, one session for HTTP/2), close the oldest idle connection.
2034def pool.give(p: Pool, +key: String, c: Conn) -> IO(Pool):
2035 Pool{+cap, idle} = p
2036 match c:
2037 case Conn{tls, s}:
2038 pool.give.of(cap, key, Conn{tls, s}, U32.to_nat(cap), Map.pop(&1, List<&1, Conn>, idle, key))
2039 case ConnH2{s, client}:
2040 pool.give.of(cap, key, ConnH2{s, client}, Bool.pick(Nat, U32.is_zero(cap), 0n, 1n),
2041 Map.pop(&1, List<&1, Conn>, idle, key))
2042
2043def pool.close.go(xs: List<&1, List<&1, Conn>>) -> IO(Unit):
2044 match xs:
2045 case Nil{}:
2046 IO.pure(Unit, Unit{})
2047 case Con{cs, t}:
2048 do IO<Unit>:
2049 none : List<&1, Conn> <- conns.cut(cs, 0n)
2050 pool.close.go(t)
2051
2052def pool.close(p: Pool) -> IO(Unit):
2053 Pool{cap, idle} = p
2054 pool.close.go(Map.values(&1, List<&1, Conn>, idle))
2055
2056# RFC 9110 §9.2.2
2057def pool.idempotent(+method: String) -> Bool:
2058 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"))))))
2059
2060def conn.tls(m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Result<&1, &1, Err, Conn>):
2061 (s, r) = m
2062 match r:
2063 case Fail{(+code, why)}:
2064 do IO<Result<&1, &1, Err, Conn>>:
2065 Wire.tls.close(s)
2066 return Fail{err.or_late(code, ErrTls{code, why})}
2067 case Done{u}:
2068 IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{True{}, s}})
2069
2070def conn.h2.sent(client: H2.Client, r: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Result<&1, &1, Err, Conn>):
2071 (s, sent) = r
2072 match sent:
2073 case Fail{(+code, why)}:
2074 do IO<Result<&1, &1, Err, Conn>>:
2075 Wire.tls.close(s)
2076 return Fail{err.or_late(code, ErrWrite{code, why})}
2077 case Done{u}:
2078 IO.pure(Result<&1, &1, Err, Conn>, Done{ConnH2{s, client}})
2079
2080def conn.h2.start(s: Socket, r: H2.Client & HBytes.Bytes) -> IO(Result<&1, &1, Err, Conn>):
2081 (client, HBytes.Bytes{len, buf}) = r
2082 do IO<Result<&1, &1, Err, Conn>>:
2083 sent : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.tls.send.words(s, len, buf)
2084 conn.h2.sent(client, sent)
2085
2086def conn.tls.protocol(proto: String, s: Socket) -> IO(Result<&1, &1, Err, Conn>):
2087 match proto:
2088 case "h2":
2089 conn.h2.start(s, H2.client.start())
2090 case "http/1.1":
2091 IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{True{}, s}})
2092 case "":
2093 IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{True{}, s}})
2094 case other:
2095 do IO<Result<&1, &1, Err, Conn>>:
2096 Wire.tls.close(s)
2097 return Fail{ErrTls{71, "unsupported ALPN: " ++ other}}
2098
2099def conn.tls.alpn(m: Socket & Result<&1, &1, U32 & String, String>) -> IO(Result<&1, &1, Err, Conn>):
2100 (s, r) = m
2101 match r:
2102 case Fail{(+code, why)}:
2103 do IO<Result<&1, &1, Err, Conn>>:
2104 Wire.tls.close(s)
2105 return Fail{err.or_late(code, ErrTls{code, why})}
2106 case Done{proto}:
2107 conn.tls.protocol(proto, s)
2108
2109def conn.secure.no.cert(offer: Bool, s: Socket, host: String, +ms: U32) ->
2110 IO(Result<&1, &1, Err, Conn>):
2111 match offer:
2112 case True{}:
2113 do IO<Result<&1, &1, Err, Conn>>:
2114 hs : Socket & Result<&1, &1, U32 & String, String> <-
2115 Wire.tls.connect.alpn(s, host, ms, "h2,http/1.1")
2116 conn.tls.alpn(hs)
2117 case False{}:
2118 do IO<Result<&1, &1, Err, Conn>>:
2119 hs : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.tls.connect(s, host, ms)
2120 conn.tls(hs)
2121
2122def conn.secure.tls(cert: Maybe<&2, Cert>, s: Socket, host: String, +ms: U32,
2123 offer: Bool) -> IO(Result<&1, &1, Err, Conn>):
2124 match cert:
2125 case None{}:
2126 conn.secure.no.cert(offer, s, host, ms)
2127 case Some{Cert{chain, key}}:
2128 do IO<Result<&1, &1, Err, Conn>>:
2129 hs : Socket & Result<&1, &1, U32 & String, Unit> <-
2130 Wire.tls.connect.cert(s, host, ms, chain, key)
2131 conn.tls(hs)
2132
2133# A failed handshake is an error, never plaintext.
2134def conn.secure(+ms: U32, sni: String, s: Socket, tls: Bool,
2135 cert: Maybe<&2, Cert>, offer: Bool) -> IO(Result<&1, &1, Err, Conn>):
2136 match tls:
2137 case False{}:
2138 IO.pure(Result<&1, &1, Err, Conn>, Done{Conn{False{}, s}})
2139 case True{}:
2140 conn.secure.tls(cert, s, sni, ms, offer)
2141
2142def conn.made(+ms: U32, sni: String, tls: Bool, cert: Maybe<&2, Cert>,
2143 offer: Bool, r: Result<&1, &1, U32 & String, Socket>) ->
2144 IO(Result<&1, &1, Err, Conn>):
2145 match r:
2146 case Fail{(+code, why)}:
2147 IO.pure(Result<&1, &1, Err, Conn>, Fail{err.or_late(code, ErrConnect{code, why})})
2148 case Done{s}:
2149 conn.secure(ms, sni, s, tls, cert, offer)
2150
2151def conn.open(+tls: Bool, +ms: U32, sni: String, ip: String, port: U32) ->
2152 IO(Result<&1, &1, Err, Conn>):
2153 do IO<Result<&1, &1, Err, Conn>>:
2154 c : Result<&1, &1, U32 & String, Socket> <- Wire.connect(ip, port, ms)
2155 conn.made(ms, sni, tls, None{}, False{}, c)
2156
2157# ponytail: addresses are tried in order, not raced; a broken first route can consume the step timeout.
2158type Dial is Type:
2159 Dial{port: U32, ms: U32, deadline: Nat, action: IO(Result<&1, &1, U32 & String, Socket>)}
2160
2161def conn.dial.time(+ip: String, +port: U32, +deadline: Nat, now: Nat, expired: Bool) ->
2162 IO(Result<&1, &1, U32 & String, Socket>):
2163 match expired:
2164 case True{}:
2165 IO.pure(Result<&1, &1, U32 & String, Socket>, Fail{(60, "connect timeout")})
2166 case False{}:
2167 Wire.connect(ip, port, U32.from_nat(Nat.sub(deadline, now)))
2168
2169def conn.dial.with(+ip: String, +port: U32, +ms: U32, +deadline: Nat, +now: Nat, unlimited: Bool) ->
2170 IO(Result<&1, &1, U32 & String, Socket>):
2171 match unlimited:
2172 case True{}:
2173 Wire.connect(ip, port, 0)
2174 case False{}:
2175 conn.dial.time(ip, port, deadline, now, Nat.is_le(deadline, now))
2176
2177def conn.dial.try(+ip: String, +port: U32, +ms: U32, +deadline: Nat) ->
2178 IO(Result<&1, &1, U32 & String, Socket>):
2179 do IO<Result<&1, &1, U32 & String, Socket>>:
2180 now : Nat <- IO.now()
2181 conn.dial.with(ip, port, ms, deadline, now, U32.is_zero(ms))
2182
2183def conn.dial.after(r: Result<&1, &1, U32 & String, Socket>, ip: String, +port: U32, +ms: U32, +deadline: Nat) ->
2184 IO(Result<&1, &1, U32 & String, Socket>):
2185 match r:
2186 case Done{s}:
2187 IO.pure(Result<&1, &1, U32 & String, Socket>, Done{s})
2188 case Fail{e}:
2189 conn.dial.try(ip, port, ms, deadline)
2190
2191def conn.dial.more(prev: IO(Result<&1, &1, U32 & String, Socket>), ip: String, +port: U32, +ms: U32, +deadline: Nat) ->
2192 IO(Result<&1, &1, U32 & String, Socket>):
2193 do IO<Result<&1, &1, U32 & String, Socket>>:
2194 r : Result<&1, &1, U32 & String, Socket> <- prev
2195 conn.dial.after(r, ip, port, ms, deadline)
2196
2197def conn.dial.fold(d: Dial, ip: String) -> Dial:
2198 Dial{+port, +ms, +deadline, action} = d
2199 Dial{port, ms, deadline, conn.dial.more(action, ip, port, ms, deadline)}
2200
2201def conn.dial.run(d: Dial) -> IO(Result<&1, &1, U32 & String, Socket>):
2202 Dial{port, ms, deadline, action} = d
2203 action
2204
2205def conn.dial.all(+port: U32, +ms: U32, +start: Nat, first: String, rest: List<&2, String>) ->
2206 IO(Result<&1, &1, U32 & String, Socket>):
2207 match rest:
2208 case Nil{}:
2209 Wire.connect(first, port, ms)
2210 case Con{ip, tail}:
2211 +deadline = Nat.add(start, U32.to_nat(ms))
2212 conn.dial.run(List.foldl(~&2, ~String, ~Dial, ~conn.dial.fold, Con{ip, tail},
2213 Dial{port, ms, deadline, Wire.connect(first, port, ms)}))
2214
2215def conn.open.all(+tls: Bool, +ms: U32, +host: String, +port: U32,
2216 ips: List<&2, String>, cert: Maybe<&2, Cert>, offer: Bool) ->
2217 IO(Result<&1, &1, Err, Conn>):
2218 match ips:
2219 case Nil{}:
2220 IO.pure(Result<&1, &1, Err, Conn>, Fail{ErrDns{}})
2221 case Con{addr, rest}:
2222 do IO<Result<&1, &1, Err, Conn>>:
2223 start : Nat <- IO.now()
2224 r : Result<&1, &1, U32 & String, Socket> <- conn.dial.all(port, ms, start, addr, rest)
2225 conn.made(ms, host, tls, cert, offer, r)
2226
2227def h2.header.skip(+name: String) -> Bool:
2228 match name:
2229 case SCon{Chr{58}, rest}:
2230 True{}
2231 case other:
2232 Bool.or(req.reserved(name),
2233 Bool.or(String.eq(name, "keep-alive"),
2234 Bool.or(String.eq(name, "proxy-connection"),
2235 Bool.or(String.eq(name, "upgrade"), String.eq(name, "te")))))
2236
2237def h2.header.mode(+name: String) -> U32:
2238 Bool.pick(U32,
2239 Bool.or(String.eq(name, "authorization"),
2240 Bool.or(String.eq(name, "cookie"), String.eq(name, "proxy-authorization"))),
2241 2, 0)
2242
2243def h2.header.values(+name: String, +mode: U32, vs: List<&2, String>) -> List<&2, Hpack.Field>:
2244 match vs:
2245 case Nil{}:
2246 Nil{}
2247 case Con{v, tail}:
2248 Hpack.Field{name, sanitize(v), mode} <> h2.header.values(name, mode, tail)
2249
2250def h2.header.tokens(vs: List<&2, String>) -> List<&2, String>:
2251 match vs:
2252 case Nil{}:
2253 Nil{}
2254 case Con{value, rest}:
2255 List.append(&2, String, String.split(value, ','), h2.header.tokens(rest))
2256
2257def h2.header.nominated.one(enabled: Bool, vs: List<&2, String>,
2258 rest: List<&2, String>) -> List<&2, String>:
2259 match enabled:
2260 case True{}:
2261 List.append(&2, String, h2.header.tokens(vs), rest)
2262 case False{}:
2263 rest
2264
2265def h2.header.nominated(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>) ->
2266 List<&2, String>:
2267 match xs:
2268 case Nil{}:
2269 Nil{}
2270 case (name, values) <> tail:
2271 h2.header.nominated.one(String.eq(String.to_lower(name), "connection"),
2272 values, h2.header.nominated(tail))
2273
2274def h2.header.has(xs: List<&2, String>, +key: String) -> Bool:
2275 match xs:
2276 case Nil{}:
2277 False{}
2278 case Con{value, rest}:
2279 Bool.or(String.eq(String.to_lower(trim(value)), key), h2.header.has(rest, key))
2280
2281def h2.header.item(skip: Bool, +name: String, vs: List<&2, String>,
2282 tail: List<&2, Hpack.Field>) -> List<&2, Hpack.Field>:
2283 match skip:
2284 case True{}:
2285 tail
2286 case False{}:
2287 List.append(&2, Hpack.Field, h2.header.values(name, h2.header.mode(name), vs), tail)
2288
2289def h2.header.items(xs: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>,
2290 +nominated: List<&2, String>) -> List<&2, Hpack.Field>:
2291 match xs:
2292 case Nil{}:
2293 Nil{}
2294 case (name, values) <> tail:
2295 +key = String.to_lower(name)
2296 h2.header.item(Bool.or(h2.header.skip(key), h2.header.has(nominated, key)),
2297 key, values, h2.header.items(tail, nominated))
2298
2299def h2.request.fields(+method: String, target: String, authority: String,
2300 headers: Map<&2, List<&2, String>>) -> List<&2, Hpack.Field>:
2301 +xs = Map.to_list(&2, List<&2, String>, headers)
2302 List.append(&2, Hpack.Field,
2303 [Hpack.Field{":method", method, 0}, Hpack.Field{":scheme", "https", 0},
2304 Hpack.Field{":authority", authority, 0}, Hpack.Field{":path", target, 0}],
2305 h2.header.items(xs, h2.header.nominated(xs)))
2306
2307def h2.response.status.value(+value: String, valid: Bool) -> Maybe<&2, U32>:
2308 match valid:
2309 case False{}:
2310 None{}
2311 case True{}:
2312 parse_u32(value)
2313
2314def h2.response.status(xs: List<&2, Hpack.Field>) -> Maybe<&2, U32>:
2315 match xs:
2316 case Nil{}:
2317 None{}
2318 case Con{Hpack.Field{name, +value, mode}, tail}:
2319 match name:
2320 case ":status":
2321 h2.response.status.value(value, Nat.is_eq(String.length(value), 3n))
2322 case other:
2323 h2.response.status(tail)
2324
2325def h2.response.headers(xs: List<&2, Hpack.Field>, acc: Map<&2, List<&2, String>>) ->
2326 Map<&2, List<&2, String>>:
2327 match xs:
2328 case Nil{}:
2329 acc
2330 case Con{Hpack.Field{name, value, mode}, tail}:
2331 match name:
2332 case SCon{Chr{58}, rest}:
2333 h2.response.headers(tail, acc)
2334 case other:
2335 h2.response.headers(tail, add(acc, String.to_lower(name), value))
2336
2337def h2.response.final(interim: Bool, +status: U32, headers: List<&2, Hpack.Field>,
2338 body: HBytes.Bytes) -> Result<&1, &1, Err, Maybe<&1, Res>>:
2339 match interim:
2340 case True{}:
2341 Done{None{}}
2342 case False{}:
2343 HBytes.Bytes{len, buf} = body
2344 Done{Some{Res{status, h2.response.headers(headers, empty()), Bytes.Bytes{len, buf}}}}
2345
2346def h2.response.valid(valid: Bool, +status: U32, headers: List<&2, Hpack.Field>,
2347 body: HBytes.Bytes) -> Result<&1, &1, Err, Maybe<&1, Res>>:
2348 match valid:
2349 case False{}:
2350 Fail{ErrBad{}}
2351 case True{}:
2352 h2.response.final(U32.is_lt(status, 200), status, headers, body)
2353
2354def h2.response.parsed(m: Maybe<&2, U32>, headers: List<&2, Hpack.Field>,
2355 body: HBytes.Bytes) -> Result<&1, &1, Err, Maybe<&1, Res>>:
2356 match m:
2357 case None{}:
2358 Fail{ErrBad{}}
2359 case Some{+status}:
2360 h2.response.valid(Bool.and(U32.is_ge(status, 100), U32.is_lt(status, 600)),
2361 status, headers, body)
2362
2363def h2.response(+fields: List<&2, Hpack.Field>, body: HBytes.Bytes) ->
2364 Result<&1, &1, Err, Maybe<&1, Res>>:
2365 h2.response.parsed(h2.response.status(fields), fields, body)
2366
2367def h2.event.fold(acc: Result<&1, &1, Err, Maybe<&1, Res>>,
2368 event: H2.ClientEvent) -> Result<&1, &1, Err, Maybe<&1, Res>>:
2369 match acc:
2370 case Fail{e}:
2371 Fail{e}
2372 case Done{Some{res}}:
2373 Done{Some{res}}
2374 case Done{None{}}:
2375 match event:
2376 case H2.Response{id, headers, body}:
2377 h2.response(headers, body)
2378 case H2.Reset{id, code}:
2379 Fail{ErrBad{}}
2380 case H2.Shutdown{last, code}:
2381 Done{None{}}
2382 case H2.Pong{data}:
2383 Done{None{}}
2384
2385def h2.send.report(r: Socket & Result<&1, &1, U32 & String, Unit>) ->
2386 IO(Result<&1, &1, Err, Socket>):
2387 (s, sent) = r
2388 match sent:
2389 case Fail{(+code, why)}:
2390 do IO<Result<&1, &1, Err, Socket>>:
2391 Wire.tls.close(s)
2392 return Fail{err.or_late(code, ErrWrite{code, why})}
2393 case Done{unit}:
2394 IO.pure(Result<&1, &1, Err, Socket>, Done{s})
2395
2396def h2.send.one(prev: Result<&1, &1, Err, Socket>, b: HBytes.Bytes) ->
2397 IO(Result<&1, &1, Err, Socket>):
2398 match prev:
2399 case Fail{e}:
2400 IO.pure(Result<&1, &1, Err, Socket>, Fail{e})
2401 case Done{s}:
2402 HBytes.Bytes{len, buf} = b
2403 do IO<Result<&1, &1, Err, Socket>>:
2404 sent : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.tls.send.words(s, len, buf)
2405 h2.send.report(sent)
2406
2407def h2.send.fold(prev: IO(Result<&1, &1, Err, Socket>), b: HBytes.Bytes) ->
2408 IO(Result<&1, &1, Err, Socket>):
2409 do IO<Result<&1, &1, Err, Socket>>:
2410 r : Result<&1, &1, Err, Socket> <- prev
2411 h2.send.one(r, b)
2412
2413def h2.send(xs: List<&1, HBytes.Bytes>, s: Socket) -> IO(Result<&1, &1, Err, Socket>):
2414 List.foldl(~&1, ~HBytes.Bytes, ~IO(Result<&1, &1, Err, Socket>), ~h2.send.fold,
2415 xs, IO.pure(Result<&1, &1, Err, Socket>, Done{s}))
2416
2417def h2.received.step(over: Bool, s: Socket, client: H2.Client,
2418 +len: U32, buf: Array<U32>) -> H2Step:
2419 match over:
2420 case True{}:
2421 H2Reply{s, H2.Failed{H2.Error{1, True{}, 0}}}
2422 case False{}:
2423 H2Reply{s, H2.client.receive(client, HBytes.Bytes{len, buf})}
2424
2425def h2.fail(s: Socket, e: Err) -> IO(Result<&1, &1, Err, Conn & Res>):
2426 do IO<Result<&1, &1, Err, Conn & Res>>:
2427 Wire.tls.close(s)
2428 return Fail{e}
2429
2430def h2.loop(n: Nat, step: H2Step, +ms: U32, +used: U32) ->
2431 IO(Result<&1, &1, Err, Conn & Res>):
2432 match n:
2433 case 0n:
2434 match step:
2435 case H2Reply{s, reply}:
2436 h2.fail(s, ErrBad{})
2437 case H2Sent{client, events, sent}:
2438 match sent:
2439 case Fail{e}:
2440 IO.pure(Result<&1, &1, Err, Conn & Res>, Fail{e})
2441 case Done{s}:
2442 h2.fail(s, ErrBad{})
2443 case H2Events{s, client, result}:
2444 h2.fail(s, ErrBad{})
2445 case H2Received{client, answer}:
2446 (s, r) = answer
2447 h2.fail(s, ErrBad{})
2448 case 1n+p:
2449 match step:
2450 case H2Reply{s, reply}:
2451 match reply:
2452 case H2.Failed{error}:
2453 h2.fail(s, ErrBad{})
2454 case H2.Ready{client, writes, events}:
2455 do IO<Result<&1, &1, Err, Conn & Res>>:
2456 sent : Result<&1, &1, Err, Socket> <- h2.send(writes, s)
2457 h2.loop(p, H2Sent{client, events, sent}, ms, used)
2458 case H2Sent{client, events, sent}:
2459 match sent:
2460 case Fail{e}:
2461 IO.pure(Result<&1, &1, Err, Conn & Res>, Fail{e})
2462 case Done{s}:
2463 h2.loop(p, H2Events{s, client,
2464 List.foldl(~&1, ~H2.ClientEvent,
2465 ~Result<&1, &1, Err, Maybe<&1, Res>>, ~h2.event.fold,
2466 events, Done{None{}})}, ms, used)
2467 case H2Events{s, client, result}:
2468 match result:
2469 case Fail{e}:
2470 h2.fail(s, e)
2471 case Done{Some{res}}:
2472 IO.pure(Result<&1, &1, Err, Conn & Res>,
2473 Done{(ConnH2{s, client}, res)})
2474 case Done{None{}}:
2475 do IO<Result<&1, &1, Err, Conn & Res>>:
2476 r : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <-
2477 Wire.tls.recv.words(s, 16384, ms)
2478 h2.loop(p, H2Received{client, r}, ms, used)
2479 case H2Received{client, answer}:
2480 match answer:
2481 case (s, Fail{(+code, why)}):
2482 h2.fail(s, err.or_late(code, ErrRead{code, why}))
2483 case (s, Done{(0, buf)}):
2484 h2.fail(s, ErrBad{})
2485 case (s, Done{(+len, buf)}):
2486 +total = (used + len : U32)
2487 h2.loop(p, h2.received.step(fetch.over(total), s, client, len, buf), ms, total)
2488
2489def h2.exchange(s: Socket, client: H2.Client, +ms: U32, request: Send) ->
2490 IO(Result<&1, &1, Err, Conn & Res>):
2491 Send{method, target, authority, headers, Bytes.Bytes{len, buf}} = request
2492 h2.loop(Nat.mul(4n, Nat.add(fetch.max(), 65536n)),
2493 H2Reply{s, H2.client.request(client,
2494 h2.request.fields(method, target, authority, headers), HBytes.Bytes{len, buf})},
2495 ms, 0)
2496
2497def conn.ex.h1(+tls: Bool, s: Socket, +ms: U32, request: Send) -> IO(Out):
2498 Send{+method, target, authority, headers, body} = request
2499 exchange.go(tls, ms, False{}, String.eq(method, "HEAD"), s,
2500 encode_req.on(method, target, authority, headers, body, False{}))
2501
2502# A socket with bytes past the response is out of step with the server, so it is closed.
2503def pool.keep.s(p: Pool, +key: String, +tls: Bool, res: Res, s: Socket, clean: Bool) -> IO(Pool & Result<&1, &1, Err, Res>):
2504 match clean:
2505 case True{}:
2506 do IO<Pool & Result<&1, &1, Err, Res>>:
2507 p2 : Pool <- pool.give(p, key, Conn{tls, s})
2508 return (p2, Done{res})
2509 case False{}:
2510 do IO<Pool & Result<&1, &1, Err, Res>>:
2511 io.close(tls, s)
2512 return (p, Done{res})
2513
2514def pool.keep.m(p: Pool, +key: String, +tls: Bool, res: Res, +clean: Bool, sock: Maybe<&1, Socket>) -> IO(Pool & Result<&1, &1, Err, Res>):
2515 match sock:
2516 case None{}:
2517 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Done{res}))
2518 case Some{s}:
2519 pool.keep.s(p, key, tls, res, s, clean)
2520
2521def pool.keep(p: Pool, +key: String, +tls: Bool, res: Res, sock: Maybe<&1, Socket>, rest: Bytes.Bytes) -> IO(Pool & Result<&1, &1, Err, Res>):
2522 Bytes.Bytes{+len, buf} = rest
2523 pool.keep.m(p, key, tls, res, U32.is_zero(len), sock)
2524
2525def pool.after(p: Pool, +key: String, +tls: Bool, o: Out) -> IO(Pool & Result<&1, &1, Err, Res>):
2526 match o:
2527 case OutFail{e, none}:
2528 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
2529 case OutDone{res, sock, rest}:
2530 pool.keep(p, key, tls, res, sock, rest)
2531
2532def pool.h2.reusable(c: Conn) -> Bool & Conn:
2533 match c:
2534 case Conn{tls, s}:
2535 (True{}, Conn{tls, s})
2536 case ConnH2{s, H2.Client{input, streams, encoder, decoder, +control}}:
2537 H2.Control{next, active, frame_max, initial, max_streams, send_window,
2538 recv_window, first, ack, continuation, +goaway} = control
2539 (Maybe.is_none(&2, U32, goaway),
2540 ConnH2{s, H2.Client{input, streams, encoder, decoder, control}})
2541
2542def pool.h2.keep(p: Pool, +key: String, res: Res, state: Bool & Conn) ->
2543 IO(Pool & Result<&1, &1, Err, Res>):
2544 (reusable, c) = state
2545 match reusable:
2546 case True{}:
2547 do IO<Pool & Result<&1, &1, Err, Res>>:
2548 next : Pool <- pool.give(p, key, c)
2549 return (next, Done{res})
2550 case False{}:
2551 do IO<Pool & Result<&1, &1, Err, Res>>:
2552 conn.close(c)
2553 return (p, Done{res})
2554
2555def pool.h2.result(p: Pool, +key: String, r: Result<&1, &1, Err, Conn & Res>) ->
2556 IO(Pool & Result<&1, &1, Err, Res>):
2557 match r:
2558 case Fail{e}:
2559 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
2560 case Done{(c, res)}:
2561 pool.h2.keep(p, key, res, pool.h2.reusable(c))
2562
2563def pool.h2.ex(p: Pool, +key: String, +ms: U32, request: Send,
2564 s: Socket, client: H2.Client) -> IO(Pool & Result<&1, &1, Err, Res>):
2565 do IO<Pool & Result<&1, &1, Err, Res>>:
2566 r : Result<&1, &1, Err, Conn & Res> <- h2.exchange(s, client, ms, request)
2567 pool.h2.result(p, key, r)
2568
2569def pool.fresh.conn(p: Pool, +key: String, +ms: U32, request: Send,
2570 r: Result<&1, &1, Err, Conn>) -> IO(Pool & Result<&1, &1, Err, Res>):
2571 match r:
2572 case Fail{e}:
2573 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
2574 case Done{c}:
2575 match c:
2576 case Conn{+tls, s}:
2577 do IO<Pool & Result<&1, &1, Err, Res>>:
2578 o : Out <- conn.ex.h1(tls, s, ms, request)
2579 pool.after(p, key, tls, o)
2580 case ConnH2{s, client}:
2581 pool.h2.ex(p, key, ms, request, s, client)
2582
2583def pool.fresh(p: Pool, +key: String, +tls: Bool, +ms: U32, +host: String,
2584 +port: U32, request: Send, cert: Maybe<&2, Cert>) ->
2585 IO(Pool & Result<&1, &1, Err, Res>):
2586 do IO<Pool & Result<&1, &1, Err, Res>>:
2587 ips : List<&2, String> <- Dns.resolve.all(host)
2588 c : Result<&1, &1, Err, Conn> <- conn.open.all(tls, ms, host, port, ips, cert, True{})
2589 pool.fresh.conn(p, key, ms, request, c)
2590
2591# A reused socket the server already closed fails before any response byte.
2592def pool.retry(+none: Bool, +idem: Bool) -> Bool:
2593 Bool.and(none, idem)
2594
2595def pool.stale(p: Pool, +key: String, +tls: Bool, +ms: U32, +host: String,
2596 +port: U32, request: Send, e: Err, again: Bool, cert: Maybe<&2, Cert>) ->
2597 IO(Pool & Result<&1, &1, Err, Res>):
2598 match again:
2599 case True{}:
2600 pool.fresh(p, key, tls, ms, host, port, request, cert)
2601 case False{}:
2602 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{e}))
2603
2604def pool.reused(p: Pool, +key: String, +tls: Bool, +ms: U32, +idem: Bool,
2605 +host: String, +port: U32, spare: Send, o: Out, cert: Maybe<&2, Cert>) ->
2606 IO(Pool & Result<&1, &1, Err, Res>):
2607 match o:
2608 case OutFail{e, +none}:
2609 pool.stale(p, key, tls, ms, host, port, spare, e, pool.retry(none, idem), cert)
2610 case OutDone{res, sock, rest}:
2611 pool.keep(p, key, tls, res, sock, rest)
2612
2613# Copy only the reused HTTP/1.1 request body, for a stale-socket retry.
2614def pool.idle.h1.bodies(p: Pool, +key: String, +tls: Bool, +ms: U32, +idem: Bool,
2615 +host: String, +port: U32, s: Socket, +method: String, +target: String,
2616 +authority: String, +headers: Map<&2, List<&2, String>>,
2617 r: Bytes.Bytes & Bytes.Bytes, cert: Maybe<&2, Cert>) ->
2618 IO(Pool & Result<&1, &1, Err, Res>):
2619 (wire, spare) = r
2620 do IO<Pool & Result<&1, &1, Err, Res>>:
2621 o : Out <- conn.ex.h1(tls, s, ms, Send{method, target, authority, headers, wire})
2622 pool.reused(p, key, tls, ms, idem, host, port,
2623 Send{method, target, authority, headers, spare}, o, cert)
2624
2625def pool.idle.h1(p: Pool, +key: String, +tls: Bool, +ms: U32, +idem: Bool,
2626 +host: String, +port: U32, s: Socket, request: Send, cert: Maybe<&2, Cert>) ->
2627 IO(Pool & Result<&1, &1, Err, Res>):
2628 Send{+method, +target, +authority, +headers, body} = request
2629 pool.idle.h1.bodies(p, key, tls, ms, idem, host, port, s, method, target,
2630 authority, headers, Bytes.slice(body, 0, 4294967295), cert)
2631
2632def pool.idle.reuse(p: Pool, +key: String, +ms: U32, +idem: Bool,
2633 +host: String, +port: U32, c: Conn, request: Send,
2634 cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res>):
2635 match c:
2636 case Conn{tls, s}:
2637 pool.idle.h1(p, key, tls, ms, idem, host, port, s, request, cert)
2638 case ConnH2{s, client}:
2639 pool.h2.ex(p, key, ms, request, s, client)
2640
2641def pool.idle(taken: Pool & Maybe<&1, Conn>, +key: String, +tls: Bool, +ms: U32,
2642 +idem: Bool, +host: String, +port: U32, request: Send, cert: Maybe<&2, Cert>) ->
2643 IO(Pool & Result<&1, &1, Err, Res>):
2644 (p, m) = taken
2645 match m:
2646 case None{}:
2647 pool.fresh(p, key, tls, ms, host, port, request, cert)
2648 case Some{c}:
2649 pool.idle.reuse(p, key, ms, idem, host, port, c, request, cert)
2650
2651def pool.origin(p: Pool, +method: String, +ms: U32,
2652 headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, +hf: String,
2653 a: Url.Abs, known: Bool, +cert: Maybe<&2, Cert>) ->
2654 IO(Pool & Result<&1, &1, Err, Res>):
2655 Url.Abs{+scheme, +host, +port, target} = a
2656 match known:
2657 case False{}:
2658 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{ErrUrl{}}))
2659 case True{}:
2660 +key = pool.key.cert(pool.key(scheme, host, port), cert)
2661 pool.idle(pool.take(p, key), key, String.eq(scheme, "https"), ms,
2662 pool.idempotent(method), host, port, Send{method, target, hf, headers, body}, cert)
2663
2664def pool.scheme.ok(a: Url.Abs) -> Bool:
2665 Url.Abs{+scheme, host, port, target} = a
2666 Bool.or(String.eq(scheme, "http"), String.eq(scheme, "https"))
2667
2668def pool.one.back(h: Hop, pr: Pool & Result<&1, &1, Err, Res>) -> Pool & Result<&1, &1, Err, Res> & Hop:
2669 (p, r) = pr
2670 (p, r, h)
2671
2672def pool.one.of(p: Pool, +method: String, +url: Url.Abs, +headers: Map<&2, List<&2, String>>, +ms: U32, r: Bytes.Bytes & Bytes.Bytes, cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res> & Hop):
2673 (body, wire) = r
2674 do IO<Pool & Result<&1, &1, Err, Res> & Hop>:
2675 pr : Pool & Result<&1, &1, Err, Res> <- pool.origin(p, method, ms, headers, wire, Url.host_field(url), url, pool.scheme.ok(url), cert)
2676 return pool.one.back(Hop{method, url, headers, body}, pr)
2677
2678# One request, on an idle socket to its origin when the pool has one. The hop comes back for the redirect.
2679def pool.one(p: Pool, h: Hop, +ms: U32, cert: Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res> & Hop):
2680 Hop{+method, +url, +headers, body} = h
2681 pool.one.of(p, method, url, headers, ms, Bytes.slice(body, 0, 4294967295), cert)
2682
2683type Next is Type:
2684 NDone{res: Result<&1, &1, Err, Res>}
2685 NStop{}
2686 NGo{left: Nat, hop: Hop}
2687
2688type Mode is Data:
2689 ModeFollow{}
2690 ModeManual{}
2691 ModeError{}
2692
2693# left: redirects still allowed after the request we just finished.
2694def fetch.hop(left: Nat, h: Hop) -> Next:
2695 match left:
2696 case 0n:
2697 NStop{}
2698 case 1n+p:
2699 NGo{p, h}
2700
2701def fetch.decide.r(left: Nat, r: Res, next: Maybe<&1, Hop>) -> Next:
2702 match next:
2703 case None{}:
2704 NDone{Done{r}}
2705 case Some{h}:
2706 fetch.hop(left, h)
2707
2708def fetch.decide.res(left: Nat, h: Hop, r: Res) -> Next:
2709 Res{+status, +headers, body} = r
2710 fetch.decide.r(left, Res{status, headers, body}, redirect(status, headers, h))
2711
2712def fetch.decide(left: Nat, h: Hop, m: Result<&1, &1, Err, Res>) -> Next:
2713 match m:
2714 case Fail{e}:
2715 NDone{Fail{e}}
2716 case Done{r}:
2717 fetch.decide.res(left, h, r)
2718
2719def fetch.error.res(r: Res, bad: Bool) -> Next:
2720 match bad:
2721 case True{}:
2722 NDone{Fail{ErrRedirect{}}}
2723 case False{}:
2724 NDone{Done{r}}
2725
2726def fetch.error(h: Hop, m: Result<&1, &1, Err, Res>) -> Next:
2727 match m:
2728 case Fail{e}:
2729 NDone{Fail{e}}
2730 case Done{r}:
2731 Res{+status, +headers, body} = r
2732 fetch.error.res(Res{status, headers, body}, Bool.and(redirect.code(status), has_header(headers, "location")))
2733
2734def fetch.policy(mode: Mode, left: Nat, h: Hop, m: Result<&1, &1, Err, Res>) -> Next:
2735 match mode:
2736 case ModeFollow{}:
2737 fetch.decide(left, h, m)
2738 case ModeManual{}:
2739 NDone{m}
2740 case ModeError{}:
2741 fetch.error(h, m)
2742
2743# A caller's own Accept-Encoding wins; enc is the codings fetch can undo.
2744def accept.enc(+h: Map<&2, List<&2, String>>, +enc: String) -> Map<&2, List<&2, String>>:
2745 Bool.pick(Map<&2, List<&2, String>>, has_header(h, "accept-encoding"), h, set(h, "accept-encoding", enc))
2746
2747def fetch.start(method: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, u: Maybe<&2, Url.Abs>, +enc: String) -> Next:
2748 match u:
2749 case None{}:
2750 NDone{Fail{ErrUrl{}}}
2751 case Some{a}:
2752 NGo{20n, Hop{method, a, accept.enc(req.put(Map.to_list(&2, List<&2, String>, headers), empty()), enc), body}}
2753
2754def pool.next.move(p: Pool, +old: String, cert: Maybe<&2, Cert>, n: Next) -> Pool & Next & Maybe<&2, Cert>:
2755 match n:
2756 case NGo{left, h}:
2757 Hop{method, +url, headers, body} = h
2758 (p, NGo{left, Hop{method, url, headers, body}},
2759 Bool.pick(Maybe<&2, Cert>, String.eq(old, redirect.origin(url)), cert, None{}))
2760 case NDone{r}:
2761 (p, NDone{r}, None{})
2762 case NStop{}:
2763 (p, NStop{}, None{})
2764
2765def pool.next(+mode: Mode, left: Nat, cert: Maybe<&2, Cert>, x: Pool & Result<&1, &1, Err, Res> & Hop) -> Pool & Next & Maybe<&2, Cert>:
2766 (p, m, h) = x
2767 Hop{method, +url, headers, body} = h
2768 pool.next.move(p, redirect.origin(url), cert, fetch.policy(mode, left, Hop{method, url, headers, body}, m))
2769
2770def pool.hops.one(+mode: Mode, +ms: U32, +cert: Maybe<&2, Cert>, p: Pool, h: Hop, left: Nat) -> IO(Pool & Next & Maybe<&2, Cert>):
2771 do IO<Pool & Next & Maybe<&2, Cert>>:
2772 x : Pool & Result<&1, &1, Err, Res> & Hop <- pool.one(p, h, ms, cert)
2773 return pool.next(mode, left, cert, x)
2774
2775# NGo.left is how many redirects may follow this request. 20 is WHATWG's limit.
2776@unsafe
2777def pool.hops(+mode: Mode, +ms: U32, st: Pool & Next & Maybe<&2, Cert>) -> IO(Pool & Result<&1, &1, Err, Res>):
2778 (p, n, cert) = st
2779 match n:
2780 case NDone{m}:
2781 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, m))
2782 case NStop{}:
2783 IO.pure(Pool & Result<&1, &1, Err, Res>, (p, Fail{ErrRedirect{}}))
2784 case NGo{+left, h}:
2785 do IO<Pool & Result<&1, &1, Err, Res>>:
2786 next : Pool & Next & Maybe<&2, Cert> <- pool.hops.one(mode, ms, cert, p, h, left)
2787 pool.hops(mode, ms, next)
2788
2789# Content-Encoding (RFC 9110 §8.4): each value, trimmed and lowercased, in the order applied.
2790def ce.keep(+w: String, +rest: List<&2, String>) -> List<&2, String>:
2791 Bool.pick(List<&2, String>, String.is_empty(w), rest, Con{w, rest})
2792
2793def ce.norm(xs: List<&2, String>) -> List<&2, String>:
2794 match xs:
2795 case Nil{}:
2796 Nil{}
2797 case Con{v, t}:
2798 ce.keep(String.to_lower(trim(v)), ce.norm(t))
2799
2800def ce.split(xs: List<&2, String>) -> List<&2, String>:
2801 match xs:
2802 case Nil{}:
2803 Nil{}
2804 case Con{v, t}:
2805 List.append(&2, String, ce.norm(String.split(v, ',')), ce.split(t))
2806
2807# Ok: decoded so far. Bad: a coding failed. Skip: a coding we cannot decode, so the body stays as sent.
2808type Dec is Data:
2809 DecOk{b: String}
2810 DecBad{}
2811 DecSkip{}
2812
2813def ce.of(m: Maybe<&2, String>) -> Dec:
2814 match m:
2815 case None{}:
2816 DecBad{}
2817 case Some{b}:
2818 DecOk{b}
2819
2820# Servers send deflate both with and without the zlib wrapper.
2821def ce.deflate(+b: String, m: Maybe<&2, String>) -> Dec:
2822 match m:
2823 case Some{out}:
2824 DecOk{out}
2825 case None{}:
2826 ce.of(Zlib.inflate(b))
2827
2828def ce.apply(+c: String, +b: String) -> Dec:
2829 Bool.pick(Dec, Bool.or(String.eq(c, "gzip"), String.eq(c, "x-gzip")), ce.of(Zlib.gunzip(b)),
2830 Bool.pick(Dec, String.eq(c, "deflate"), ce.deflate(b, Zlib.unzlib(b)),
2831 Bool.pick(Dec, String.eq(c, "identity"), DecOk{b}, DecSkip{})))
2832
2833def ce.go(cs: List<&2, String>, d: Dec) -> Dec:
2834 match cs:
2835 case Nil{}:
2836 d
2837 case Con{+c, t}:
2838 match d:
2839 case DecOk{+b}:
2840 ce.go(t, ce.apply(c, b))
2841 case DecBad{}:
2842 DecBad{}
2843 case DecSkip{}:
2844 DecSkip{}
2845
2846def decoded.pick(d: Dec, +status: U32, headers: Map<&2, List<&2, String>>, body: String) -> Result<&1, &1, Err, Res>:
2847 match d:
2848 case DecOk{b}:
2849 Done{Res{status, headers, Bytes.from_string(b)}}
2850 case DecBad{}:
2851 Fail{ErrBad{}}
2852 case DecSkip{}:
2853 Done{Res{status, headers, Bytes.from_string(body)}}
2854
2855# ponytail: the codings run on a String copy of the body; give zlib a Bytes input if gzip bodies get big.
2856def decoded.cs(+status: U32, +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, cs: List<&2, String>) -> Result<&1, &1, Err, Res>:
2857 match cs:
2858 case Nil{}:
2859 Done{Res{status, headers, body}}
2860 case Con{c, t}:
2861 +s = Bytes.to_string(body)
2862 decoded.pick(ce.go(Con{c, t}, DecOk{s}), status, headers, s)
2863
2864def decoded.go(empty: Bool, +status: U32, +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> Result<&1, &1, Err, Res>:
2865 match empty:
2866 case True{}:
2867 Done{Res{status, headers, body}}
2868 case False{}:
2869 decoded.cs(status, headers, body, List.reverse(&2, String, ce.split(fields(headers, "content-encoding"))))
2870
2871# The body decoded per Content-Encoding; the headers stay as sent. A corrupt body is ErrBad.
2872def decoded(res: Res) -> Result<&1, &1, Err, Res>:
2873 Res{+status, +headers, body} = res
2874 Bytes.Bytes{+len, buf} = body
2875 decoded.go(U32.is_zero(len), status, headers, Bytes.Bytes{len, buf})
2876
2877def decoded.m(r: Result<&1, &1, Err, Res>) -> Maybe<&1, Res>:
2878 match r:
2879 case Done{x}:
2880 Some{x}
2881 case Fail{e}:
2882 None{}
2883
2884def decoded.some(res: Res) -> Maybe<&1, Res>:
2885 decoded.m(decoded(res))
2886
2887def ce.words(r: Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Maybe<&1, Bytes.Bytes>:
2888 match r:
2889 case Fail{e}:
2890 None{}
2891 case Done{(+len, buf)}:
2892 Some{Bytes.Bytes{len, buf}}
2893
2894# A decoded body stops at 16 MiB, like a received one.
2895def ce.eff(~eff: U32 -> U32 -> Array<U32> -> IO(Result<&1, &1, U32 & String, U32 & Array<U32>>), b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
2896 Bytes.Bytes{+len, buf} = b
2897 do IO<Maybe<&1, Bytes.Bytes>>:
2898 r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- eff(16777216, len, buf)
2899 return ce.words(r)
2900
2901def ce.dec(d: Dec) -> Maybe<&1, Bytes.Bytes>:
2902 match d:
2903 case DecOk{b}:
2904 Some{Bytes.from_string(b)}
2905 case DecBad{}:
2906 None{}
2907 case DecSkip{}:
2908 None{}
2909
2910# ponytail: deflate runs on the pure decoder, which also takes raw DEFLATE; servers rarely send it.
2911def ce.io.deflate(on: Bool, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
2912 match on:
2913 case True{}:
2914 +s = Bytes.to_string(b)
2915 IO.pure(Maybe<&1, Bytes.Bytes>, ce.dec(ce.deflate(s, Zlib.unzlib(s))))
2916 case False{}:
2917 IO.pure(Maybe<&1, Bytes.Bytes>, Some{b})
2918
2919def ce.io.zstd(on: Bool, +c: String, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
2920 match on:
2921 case True{}:
2922 ce.eff(~Zlib.zstd.words, b)
2923 case False{}:
2924 ce.io.deflate(String.eq(c, "deflate"), b)
2925
2926def ce.io.br(on: Bool, +c: String, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
2927 match on:
2928 case True{}:
2929 ce.eff(~Zlib.brotli.words, b)
2930 case False{}:
2931 ce.io.zstd(String.eq(c, "zstd"), c, b)
2932
2933# One known coding undone: gzip, x-gzip, br, zstd, deflate, or identity.
2934def ce.io.gz(on: Bool, +c: String, b: Bytes.Bytes) -> IO(Maybe<&1, Bytes.Bytes>):
2935 match on:
2936 case True{}:
2937 ce.eff(~Zlib.inflate.words, b)
2938 case False{}:
2939 ce.io.br(String.eq(c, "br"), c, b)
2940
2941def ce.io.go(cs: List<&2, String>, m: Maybe<&1, Bytes.Bytes>) -> IO(Maybe<&1, Bytes.Bytes>):
2942 match cs:
2943 case Nil{}:
2944 match m:
2945 case None{}:
2946 IO.pure(Maybe<&1, Bytes.Bytes>, None{})
2947 case Some{b}:
2948 IO.pure(Maybe<&1, Bytes.Bytes>, Some{b})
2949 case Con{+c, t}:
2950 match m:
2951 case None{}:
2952 IO.pure(Maybe<&1, Bytes.Bytes>, None{})
2953 case Some{b}:
2954 do IO<Maybe<&1, Bytes.Bytes>>:
2955 n : Maybe<&1, Bytes.Bytes> <- ce.io.gz(Bool.or(String.eq(c, "gzip"), String.eq(c, "x-gzip")), c, b)
2956 ce.io.go(t, n)
2957
2958def ce.has(xs: List<&2, String>, +c: String) -> Bool:
2959 match xs:
2960 case Nil{}:
2961 False{}
2962 case Con{x, t}:
2963 Bool.or(String.eq(c, x), ce.has(t, c))
2964
2965def ce.known(cs: List<&2, String>, +ok: List<&2, String>) -> Bool:
2966 match cs:
2967 case Nil{}:
2968 True{}
2969 case Con{c, t}:
2970 Bool.and(ce.has(ok, c), ce.known(t, ok))
2971
2972def decoded.io.pick(m: Maybe<&1, Bytes.Bytes>, +status: U32, headers: Map<&2, List<&2, String>>) -> Result<&1, &1, Err, Res>:
2973 match m:
2974 case Some{b}:
2975 Done{Res{status, headers, b}}
2976 case None{}:
2977 Fail{ErrBad{}}
2978
2979def 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>):
2980 match known:
2981 case True{}:
2982 do IO<Result<&1, &1, Err, Res>>:
2983 m : Maybe<&1, Bytes.Bytes> <- ce.io.go(cs, Some{body})
2984 return decoded.io.pick(m, status, headers)
2985 case False{}:
2986 IO.pure(Result<&1, &1, Err, Res>, Done{Res{status, headers, body}})
2987
2988def decoded.io.go(empty: Bool, +enc: String, +status: U32, +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Res>):
2989 match empty:
2990 case True{}:
2991 IO.pure(Result<&1, &1, Err, Res>, Done{Res{status, headers, body}})
2992 case False{}:
2993 +cs = List.reverse(&2, String, ce.split(fields(headers, "content-encoding")))
2994 decoded.io.run(ce.known(cs, Con{"identity", Con{"x-gzip", ce.split(Con{enc, Nil{}})}}), status, headers, body, cs)
2995
2996# decoded through the C libraries, for the codings in enc. A body with any other coding stays as sent.
2997def decoded.io(+enc: String, res: Res) -> IO(Result<&1, &1, Err, Res>):
2998 Res{+status, +headers, body} = res
2999 Bytes.Bytes{+len, buf} = body
3000 decoded.io.go(U32.is_zero(len), enc, status, headers, Bytes.Bytes{len, buf})
3001
3002# An effect on empty input fails with ENOENT only when its library does not load.
3003def codings.ok(r: Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Bool:
3004 match r:
3005 case Fail{(+c, why)}:
3006 Bool.not(U32.is_eq(c, 2))
3007 case Done{p}:
3008 True{}
3009
3010def codings.has(~eff: U32 -> U32 -> Array<U32> -> IO(Result<&1, &1, U32 & String, U32 & Array<U32>>), b: Bytes.Bytes) -> IO(Bool):
3011 Bytes.Bytes{+len, buf} = b
3012 do IO<Bool>:
3013 r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- eff(0, len, buf)
3014 return codings.ok(r)
3015
3016def codings.add(has: Bool, +enc: String, +c: String) -> String:
3017 Bool.pick(String, has, enc ++ ", " ++ c, enc)
3018
3019# gzip and deflate, then br and zstd when their C library loads.
3020def codings() -> IO(String):
3021 do IO<String>:
3022 b : Bool <- codings.has(~Zlib.brotli.words, Bytes.new(0))
3023 z : Bool <- codings.has(~Zlib.zstd.words, Bytes.new(0))
3024 return codings.add(z, codings.add(b, "gzip, deflate", "br"), "zstd")
3025
3026# The final response of a fetch, after redirects.
3027def fetch.final(+enc: String, r: Result<&1, &1, Err, Res>) -> IO(Result<&1, &1, Err, Res>):
3028 match r:
3029 case Done{res}:
3030 decoded.io(enc, res)
3031 case Fail{e}:
3032 IO.pure(Result<&1, &1, Err, Res>, Fail{e})
3033
3034def pool.final(+enc: String, pr: Pool & Result<&1, &1, Err, Res>) -> IO(Pool & Result<&1, &1, Err, Res>):
3035 (p, r) = pr
3036 do IO<Pool & Result<&1, &1, Err, Res>>:
3037 d : Result<&1, &1, Err, Res> <- fetch.final(enc, r)
3038 return (p, d)
3039
3040def 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>):
3041 do IO<Pool & Result<&1, &1, Err, Res>>:
3042 pr : Pool & Result<&1, &1, Err, Res> <- pool.hops(mode, ms, (p, fetch.start(method, headers, body, Url.absolute(url), enc), cert))
3043 pool.final(enc, pr)
3044
3045def 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>):
3046 do IO<Pool & Result<&1, &1, Err, Res>>:
3047 enc : String <- codings()
3048 pool.how.enc(enc, p, method, url, headers, body, ms, mode, cert)
3049
3050# pool.how(p, "GET", "https://example.com/x?y=1", headers, body, ms, mode) follows redirects
3051# on p's idle sockets. Fail is a bad URL, a failed lookup, connect, handshake, send, read,
3052# a malformed response, more than 20 redirects, or a step past ms. Bodies are bytes.
3053def 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>):
3054 pool.how.cert(p, method, url, headers, body, ms, mode, None{})
3055
3056def 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>):
3057 pool.how(p, method, url, headers, body, ms, ModeFollow{})
3058
3059def pool.fetch(p: Pool, method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Pool & Result<&1, &1, Err, Res>):
3060 pool.fetch.with(p, method, url, headers, body, 30000)
3061
3062def 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>):
3063 pool.how.cert(p, method, url, headers, body, ms, ModeFollow{}, Some{Cert{chain, key}})
3064
3065def 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>):
3066 pool.fetch.cert.with(p, method, url, headers, body, chain, key, 30000)
3067
3068def fetch.end(pr: Pool & Result<&1, &1, Err, Res>) -> IO(Result<&1, &1, Err, Res>):
3069 (p, r) = pr
3070 do IO<Result<&1, &1, Err, Res>>:
3071 pool.close(p)
3072 return r
3073
3074# fetch is pool.how on a fresh pool that closes afterwards.
3075def 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>):
3076 do IO<Result<&1, &1, Err, Res>>:
3077 pr : Pool & Result<&1, &1, Err, Res> <- pool.how(pool.new(), method, url, headers, body, ms, mode)
3078 fetch.end(pr)
3079
3080def fetch.with(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, ms: U32) -> IO(Result<&1, &1, Err, Res>):
3081 fetch.how(method, url, headers, body, ms, ModeFollow{})
3082
3083def 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>):
3084 do IO<Result<&1, &1, Err, Res>>:
3085 pr : Pool & Result<&1, &1, Err, Res> <- pool.fetch.cert.with(pool.new(), method, url, headers, body, chain, key, ms)
3086 fetch.end(pr)
3087
3088def 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>):
3089 fetch.cert.with(method, url, headers, body, chain, key, 30000)
3090
3091# fetch.with and a 30 s step timeout.
3092def fetch(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Res>):
3093 fetch.with(method, url, headers, body, 30000)
3094
3095def get(url: String) -> IO(Result<&1, &1, Err, Res>):
3096 fetch("GET", url, empty(), Bytes.new(0))
3097
3098# POST v as compact JSON, with content-type: application/json.
3099def post.json(url: String, v: Json.Val) -> IO(Result<&1, &1, Err, Res>):
3100 fetch("POST", url, set(empty(), "content-type", "application/json"), Json.encode.bytes(v))
3101
3102# Base URLs: resolve(base, ref) is ref against the absolute http(s) URL base (RFC 3986 §5.2),
3103# written back as a URL for fetch. None when base is not absolute or ref has another scheme.
3104def resolve.show(a: Url.Abs) -> String:
3105 Url.Abs{+scheme, host, port, +target} = a
3106 scheme ++ "://" ++ Url.host_field(Url.Abs{scheme, host, port, target}) ++ target
3107
3108def resolve.to(m: Maybe<&2, Url.Abs>) -> Maybe<&2, String>:
3109 match m:
3110 case None{}:
3111 None{}
3112 case Some{a}:
3113 Some{resolve.show(a)}
3114
3115def resolve.base(m: Maybe<&2, Url.Abs>, +ref: String) -> Maybe<&2, String>:
3116 match m:
3117 case None{}:
3118 None{}
3119 case Some{b}:
3120 resolve.to(Url.resolve(b, ref))
3121
3122def resolve(base: String, +ref: String) -> Maybe<&2, String>:
3123 resolve.base(Url.absolute(base), ref)
3124
3125# Retry. The wait before retry n (0 first) is 500 ms doubled n times, at most 30 s;
3126# its upper half is jitter r: backoff(n, r) = half + r mod (half + 1).
3127def retry.cap() -> U32:
3128 30000
3129
3130def retry.base(n: Nat) -> U32:
3131 match n:
3132 case 0n:
3133 500
3134 case 1n+p:
3135 U32.min((retry.base(p) * 2 : U32), retry.cap())
3136
3137def retry.backoff.half(+half: U32, +r: U32) -> U32:
3138 (half + (r % (half + 1)) : U32)
3139
3140def retry.backoff(n: Nat, +r: U32) -> U32:
3141 retry.backoff.half((retry.base(n) / 2 : U32), r)
3142
3143# ms clamped to 0 .. retry.cap().
3144def retry.after.ms(+ms: Int.I64) -> U32:
3145 Bool.pick(U32, Int.I64.is_neg(ms), 0,
3146 Bool.pick(U32, Int.I64.is_lt(ms, Int.I64.from_u32(retry.cap())), Int.I64.to_u32(ms), retry.cap()))
3147
3148def retry.after.date(m: Maybe<&2, Time.Instant>, now: Time.Instant) -> Maybe<&2, U32>:
3149 match m:
3150 case None{}:
3151 None{}
3152 case Some{date}:
3153 Some{retry.after.ms(Time.Duration.to_ms(Time.Instant.since(date, now)))}
3154
3155# More than 5 digits is past the cap, and would overflow parse_u32.
3156def retry.after.secs(+v: String, now: Time.Instant, n: Maybe<&2, U32>) -> Maybe<&2, U32>:
3157 match n:
3158 case None{}:
3159 retry.after.date(Time.http_date.parse(v), now)
3160 case Some{s}:
3161 Some{Bool.pick(U32, Nat.is_lt(5n, String.length(v)), retry.cap(), U32.min((s * 1000 : U32), retry.cap()))}
3162
3163# Retry-After (RFC 9110 §10.2.3) as ms from now, at most retry.cap(): delay-seconds, or an
3164# HTTP-date (a past date is 0). None when v is empty or neither form.
3165def retry.after(+v: String, now: Time.Instant) -> Maybe<&2, U32>:
3166 retry.after.secs(v, now, parse_u32(v))
3167
3168def retry.wait(m: Maybe<&2, U32>, n: Nat, +r: U32) -> U32:
3169 match m:
3170 case None{}:
3171 retry.backoff(n, r)
3172 case Some{ms}:
3173 ms
3174
3175# The wait before retry n: Retry-After v when it reads as a delay, else backoff with jitter r.
3176def retry.delay(+v: String, now: Time.Instant, n: Nat, +r: U32) -> U32:
3177 retry.wait(retry.after(v, now), n, r)
3178
3179# Statuses a later try may clear.
3180def retry.status(+s: U32) -> Bool:
3181 Bool.or(Bool.or(U32.is_eq(s, 408), U32.is_eq(s, 429)),
3182 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))))
3183
3184# A refused connect or a timeout may clear; any other error would repeat.
3185def retry.fail(e: Err) -> Result<&1, &1, Err, Res> & Maybe<&2, String>:
3186 match e:
3187 case ErrConnect{code, why}:
3188 (Fail{ErrConnect{code, why}}, Some{""})
3189 case ErrTimeout{}:
3190 (Fail{ErrTimeout{}}, Some{""})
3191 case other:
3192 (Fail{other}, None{})
3193
3194def retry.res(res: Res) -> Result<&1, &1, Err, Res> & Maybe<&2, String>:
3195 Res{+status, +headers, body} = res
3196 (Done{Res{status, headers, body}}, Bool.pick(Maybe<&2, String>, retry.status(status), Some{header(headers, "retry-after")}, None{}))
3197
3198def retry.judge.try(r: Result<&1, &1, Err, Res>) -> Result<&1, &1, Err, Res> & Maybe<&2, String>:
3199 match r:
3200 case Fail{e}:
3201 retry.fail(e)
3202 case Done{res}:
3203 retry.res(res)
3204
3205# One try, judged: the result as it came, and Some{Retry-After value} ("" when absent)
3206# when an idempotent request may try again.
3207def retry.judge(idem: Bool, r: Result<&1, &1, Err, Res>) -> Result<&1, &1, Err, Res> & Maybe<&2, String>:
3208 match idem:
3209 case False{}:
3210 (r, None{})
3211 case True{}:
3212 retry.judge.try(r)
3213
3214# ponytail: a failed random source gives jitter 0, so the wait is the lower half.
3215def retry.jitter(r: Result<&1, &1, U32 & String, U32>) -> U32:
3216 match r:
3217 case Fail{e}:
3218 0
3219 case Done{x}:
3220 x
3221
3222def retry.sleep(+v: String, n: Nat) -> IO(Unit):
3223 do IO<Unit>:
3224 now : Time.Instant <- Time.now()
3225 rnd : Result<&1, &1, U32 & String, U32> <- IO.random_u32()
3226 IO.sleep(retry.delay(v, now, n, retry.jitter(rnd)))
3227
3228def retry.kept(body: Bytes.Bytes, j: Result<&1, &1, Err, Res> & Maybe<&2, String>) -> Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String>:
3229 (r, m) = j
3230 (body, r, m)
3231
3232# One fetch of the copy; the body comes back for the next try.
3233def retry.one(+idem: Bool, +method: String, +url: String, +headers: Map<&2, List<&2, String>>,
3234 r: Bytes.Bytes & Bytes.Bytes) -> IO(Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String>):
3235 (body, spare) = r
3236 do IO<Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String>>:
3237 got : Result<&1, &1, Err, Res> <- fetch(method, url, headers, spare)
3238 return retry.kept(body, retry.judge(idem, got))
3239
3240# left: retries still allowed. n: the retry to wait for next, 0 first.
3241def retry.go(left: Nat, +n: Nat, +idem: Bool, +method: String, +url: String,
3242 +headers: Map<&2, List<&2, String>>,
3243 t: Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String>) -> IO(Result<&1, &1, Err, Res>):
3244 match left:
3245 case 0n:
3246 (body, r, m) = t
3247 IO.pure(Result<&1, &1, Err, Res>, r)
3248 case 1n+p:
3249 (body, r, m) = t
3250 match m:
3251 case None{}:
3252 IO.pure(Result<&1, &1, Err, Res>, r)
3253 case Some{v}:
3254 do IO<Result<&1, &1, Err, Res>>:
3255 retry.sleep(v, n)
3256 tried : Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String> <-
3257 retry.one(idem, method, url, headers, Bytes.slice(body, 0, 4294967295))
3258 retry.go(p, 1n+n, idem, method, url, headers, tried)
3259
3260# fetch.retry(n, method, url, headers, body) is fetch, tried again up to n times while an
3261# idempotent method (GET, HEAD, OPTIONS, TRACE, PUT, DELETE) gets a connect error, a timeout,
3262# or 408, 429, 500, 502, 503, or 504. POST, PATCH and other methods get one try. It waits
3263# Retry-After (seconds or HTTP-date, at most 30 s) when given, else the backoff. When retries
3264# run out, the last response or error comes back as it was.
3265def retry.start(enabled: Bool, n: U32, +method: String, +url: String,
3266 +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) ->
3267 IO(Result<&1, &1, Err, Res>):
3268 match enabled:
3269 case False{}:
3270 fetch(method, url, headers, body)
3271 case True{}:
3272 do IO<Result<&1, &1, Err, Res>>:
3273 first : Bytes.Bytes & Result<&1, &1, Err, Res> & Maybe<&2, String> <-
3274 retry.one(True{}, method, url, headers, Bytes.slice(body, 0, 4294967295))
3275 retry.go(U32.to_nat(n), 0n, True{}, method, url, headers, first)
3276
3277def fetch.retry(+n: U32, +method: String, +url: String,
3278 +headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) ->
3279 IO(Result<&1, &1, Err, Res>):
3280 retry.start(Bool.and(U32.is_ne(n, 0), pool.idempotent(method)),
3281 n, method, url, headers, body)
3282
3283# Streaming (a body read or sent in pieces). A decoded stream owns its decoders.
3284# What the next read returns: read more, a raw piece, a decoded piece, the end, or an error.
3285type Po is Type:
3286 PoNone{}
3287 PoPiece{b: Bytes.Bytes}
3288 PoReady{b: Bytes.Bytes}
3289 PoEnd{}
3290 PoBad{e: Err}
3291
3292type Stream is Type:
3293 Stream{tls: Bool, s: Socket, ms: U32, res: Res, rb: Rb, out: Po, decs: List<&1, Zlib.Decoder>}
3294
3295type Pc is Type:
3296 Pc{rb: Rb, out: Po}
3297
3298# A body piece, or none when empty: more reads the next piece, and not more is the end.
3299def pc.po(more: Bool, empty: Bool, b: Bytes.Bytes) -> Po:
3300 match empty:
3301 case True{}:
3302 Bool.pick(Po, more, PoNone{}, PoEnd{})
3303 case False{}:
3304 PoPiece{b}
3305
3306def pc.piece(more: Bool, +rb: Rb, b: Bytes.Bytes) -> Pc:
3307 Bytes.Bytes{+len, buf} = b
3308 Pc{rb, pc.po(more, U32.is_zero(len), Bytes.Bytes{len, buf})}
3309
3310def pc.fed.of(b: Bytes.Bytes, st: Rb) -> Pc:
3311 match st:
3312 case RbDone{}:
3313 pc.piece(False{}, RbDone{}, b)
3314 case RbBad{}:
3315 Pc{RbDone{}, PoBad{ErrBad{}}}
3316 case RbLen{n}:
3317 pc.piece(True{}, RbLen{n}, b)
3318 case RbChunk{st}:
3319 pc.piece(True{}, RbChunk{st}, b)
3320 case RbClose{}:
3321 pc.piece(True{}, RbClose{}, b)
3322
3323def pc.fed(bf: Bf) -> Pc:
3324 Bf{st, parts, rest} = bf
3325 pc.fed.of(rb.body(parts), st)
3326
3327# The body bytes that just arrived: what they add to the body, and how it ends.
3328def pc.of(rb: Rb, piece: Bytes.Bytes) -> Pc:
3329 pc.fed(rb.feed(rb, Nil{}, piece))
3330
3331# The server closed. Only a close-delimited body may end this way (RFC 9112 §8).
3332def pc.end(ok: Bool) -> Pc:
3333 match ok:
3334 case True{}:
3335 Pc{RbDone{}, PoEnd{}}
3336 case False{}:
3337 Pc{RbDone{}, PoBad{ErrBad{}}}
3338
3339def pc.eof(st: Rb) -> Pc:
3340 pc.end(rb.eof(st))
3341
3342def stream.mk(+tls: Bool, s: Socket, +ms: U32, res: Res, decs: List<&1, Zlib.Decoder>, pc: Pc) -> Stream:
3343 Pc{rb, out} = pc
3344 Stream{tls, s, ms, res, rb, out, decs}
3345
3346def stream.got.piece(+tls: Bool, s: Socket, +ms: U32, res: Res, decs: List<&1, Zlib.Decoder>, +rb: Rb, p: U32 & Array<U32>) -> Stream:
3347 (+len, buf) = p
3348 stream.mk(tls, s, ms, res, decs, Bool.pick(Pc, U32.is_zero(len), pc.eof(rb), pc.of(rb, Bytes.Bytes{len, buf})))
3349
3350def 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:
3351 (s, r) = m
3352 match r:
3353 case Fail{(+code, why)}:
3354 Stream{tls, s, ms, res, RbDone{}, PoBad{err.or_late(code, ErrRead{code, why})}, decs}
3355 case Done{p}:
3356 stream.got.piece(tls, s, ms, res, decs, rb, p)
3357
3358def stream.after(+rb: Rb) -> Po:
3359 match rb:
3360 case RbDone{}:
3361 PoEnd{}
3362 case RbBad{}:
3363 PoEnd{}
3364 case RbLen{n}:
3365 PoNone{}
3366 case RbChunk{st}:
3367 PoNone{}
3368 case RbClose{}:
3369 PoNone{}
3370
3371type Fed is Type:
3372 Fed{decs: List<&1, Zlib.Decoder>, body: Result<&1, &1, Err, Bytes.Bytes>}
3373
3374def stream.feed.received(done: List<&1, Zlib.Decoder>, m: Zlib.Decoder & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Fed:
3375 (d, r) = m
3376 match r:
3377 case Fail{e}:
3378 Fed{d <> done, Fail{ErrBad{}}}
3379 case Done{(+len, buf)}:
3380 Fed{d <> done, Done{Bytes.Bytes{len, buf}}}
3381
3382def stream.feed.step(st: Fed, d: Zlib.Decoder) -> IO(Fed):
3383 Fed{done, body} = st
3384 match body:
3385 case Fail{e}:
3386 IO.pure(Fed, Fed{d <> done, Fail{e}})
3387 case Done{b}:
3388 Bytes.Bytes{+len, buf} = b
3389 do IO<Fed>:
3390 m : Zlib.Decoder & Result<&1, &1, U32 & String, U32 & Array<U32>> <-
3391 Zlib.dec.feed.words(d, 16777216, len, buf)
3392 return stream.feed.received(done, m)
3393
3394def stream.feed.one(prev: IO(Fed), d: Zlib.Decoder) -> IO(Fed):
3395 do IO<Fed>:
3396 st : Fed <- prev
3397 stream.feed.step(st, d)
3398
3399def stream.feed.reverse(st: Fed) -> Fed:
3400 Fed{done, body} = st
3401 Fed{List.reverse(&1, Zlib.Decoder, done), body}
3402
3403def stream.feed.all(decs: List<&1, Zlib.Decoder>, b: Bytes.Bytes) -> IO(Fed):
3404 do IO<Fed>:
3405 st : Fed <- List.foldl(~&1, ~Zlib.Decoder, ~IO(Fed), ~stream.feed.one, decs,
3406 IO.pure(Fed, Fed{Nil{}, Done{b}}))
3407 return stream.feed.reverse(st)
3408
3409def stream.ready(empty: Bool, +rb: Rb, b: Bytes.Bytes) -> Po:
3410 match empty:
3411 case True{}:
3412 stream.after(rb)
3413 case False{}:
3414 PoReady{b}
3415
3416def stream.feed.got(+tls: Bool, s: Socket, +ms: U32, res: Res, +rb: Rb, st: Fed) -> Stream:
3417 Fed{decs, body} = st
3418 match body:
3419 case Fail{e}:
3420 Stream{tls, s, ms, res, rb, PoBad{e}, decs}
3421 case Done{b}:
3422 Bytes.Bytes{+len, buf} = b
3423 Stream{tls, s, ms, res, rb, stream.ready(U32.is_zero(len), rb, Bytes.Bytes{len, buf}), decs}
3424
3425def stream.feed.st(st: Stream, b: Bytes.Bytes) -> IO(Stream):
3426 Stream{+tls, s, +ms, res, +rb, out, decs} = st
3427 match decs:
3428 case Nil{}:
3429 IO.pure(Stream, Stream{tls, s, ms, res, rb, PoReady{b}, Nil{}})
3430 case Con{d, rest}:
3431 do IO<Stream>:
3432 fed : Fed <- stream.feed.all(Con{d, rest}, b)
3433 return stream.feed.got(tls, s, ms, res, rb, fed)
3434
3435def stream.finish.ok(r: Result<&1, &1, U32 & String, Unit>) -> Bool:
3436 match r:
3437 case Fail{e}:
3438 False{}
3439 case Done{u}:
3440 True{}
3441
3442def stream.finish(decs: List<&1, Zlib.Decoder>) -> IO(Bool):
3443 match decs:
3444 case Nil{}:
3445 IO.pure(Bool, True{})
3446 case Con{d, rest}:
3447 do IO<Bool>:
3448 r : Result<&1, &1, U32 & String, Unit> <- Zlib.dec.finish(d)
3449 tail : Bool <- stream.finish(rest)
3450 return Bool.and(stream.finish.ok(r), tail)
3451
3452def stream.ended(good: Bool, +tls: Bool, s: Socket, +ms: U32, res: Res, +rb: Rb) ->
3453 Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>:
3454 match good:
3455 case True{}:
3456 (Stream{tls, s, ms, res, rb, PoEnd{}, Nil{}}, Done{None{}})
3457 case False{}:
3458 (Stream{tls, s, ms, res, rb, PoBad{ErrBad{}}, Nil{}}, Fail{ErrBad{}})
3459
3460# The next piece of the body; None at the end. A piece is never empty.
3461@unsafe
3462def stream.read(st: Stream) -> IO(Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>):
3463 Stream{+tls, s, +ms, res, +rb, out, decs} = st
3464 match out:
3465 case PoPiece{b}:
3466 do IO<Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>>:
3467 next : Stream <- stream.feed.st(Stream{tls, s, ms, res, rb, PoNone{}, decs}, b)
3468 stream.read(next)
3469 case PoReady{b}:
3470 IO.pure(Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>,
3471 (Stream{tls, s, ms, res, rb, stream.after(rb), decs}, Done{Some{b}}))
3472 case PoEnd{}:
3473 do IO<Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>>:
3474 good : Bool <- stream.finish(decs)
3475 return stream.ended(good, tls, s, ms, res, rb)
3476 case PoBad{+e}:
3477 IO.pure(Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>,
3478 (Stream{tls, s, ms, res, rb, PoBad{e}, decs}, Fail{e}))
3479 case PoNone{}:
3480 do IO<Stream & Result<&1, &1, Err, Maybe<&1, Bytes.Bytes>>>:
3481 m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv.words(tls, s, 65536, ms)
3482 stream.read(stream.got(tls, ms, res, decs, rb, m))
3483
3484# Status and headers. Its body is empty: read the body with stream.read.
3485def stream.res(st: Stream) -> Stream & Res:
3486 Stream{tls, s, ms, res, rb, out, decs} = st
3487 Res{+status, +headers, body} = res
3488 (Stream{tls, s, ms, Res{status, headers, body}, rb, out, decs}, Res{status, headers, Bytes.new(0)})
3489
3490def stream.close(st: Stream) -> IO(Unit):
3491 Stream{tls, s, ms, res, rb, out, decs} = st
3492 do IO<Unit>:
3493 good : Bool <- stream.finish(decs)
3494 io.close(tls, s)
3495
3496# Head read state: still scanning, cut short or bad, or the head with the bytes after it.
3497type Sh is Type:
3498 ShMore{buf: Bytes.Bytes, k: U32}
3499 ShBad{err: Maybe<&2, Err>}
3500 ShRes{res: Res, rb: Rb, rest: Bytes.Bytes}
3501
3502def sh.of(hs: Hs) -> Sh:
3503 match hs:
3504 case HsWait{buf, k}:
3505 ShMore{buf, k}
3506 case HsBad{}:
3507 ShBad{None{}}
3508 case HsSeek{buf, from, k}:
3509 ShBad{None{}}
3510 case HsRes{res, rb, rest}:
3511 ShRes{res, rb, rest}
3512
3513def sh.piece(+head: Bool, buf: Bytes.Bytes, +k: U32, p: U32 & Array<U32>) -> Sh:
3514 (+len, b) = p
3515 Bool.pick(Sh, U32.is_zero(len), ShBad{None{}}, sh.of(hs.more(head, k, buf, Bytes.Bytes{len, b})))
3516
3517def sh.next(+head: Bool, buf: Bytes.Bytes, +k: U32, m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Socket & Sh:
3518 (s, r) = m
3519 match r:
3520 case Fail{(+code, why)}:
3521 (s, ShBad{Some{err.or_late(code, ErrRead{code, why})}})
3522 case Done{p}:
3523 (s, sh.piece(head, buf, k, p))
3524
3525def fetch.fail.of(r: Result<&1, &1, Err, Res>) -> Result<&1, &1, Err, Stream>:
3526 match r:
3527 case Fail{e}:
3528 Fail{e}
3529 case Done{res}:
3530 Fail{ErrBad{}}
3531
3532# Reads until the final head is in; the body bytes that came with it are the first piece.
3533@unsafe
3534def stream.head(+tls: Bool, +ms: U32, +head: Bool, st: Socket & Sh) -> IO(Result<&1, &1, Err, Stream>):
3535 (s, sh) = st
3536 match sh:
3537 case ShMore{buf, +k}:
3538 do IO<Result<&1, &1, Err, Stream>>:
3539 m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv.words(tls, s, 65536, ms)
3540 stream.head(tls, ms, head, sh.next(head, buf, k, m))
3541 case ShBad{err}:
3542 do IO<Result<&1, &1, Err, Stream>>:
3543 r : Result<&1, &1, Err, Res> <- fetch.bad(tls, s, err)
3544 return fetch.fail.of(r)
3545 case ShRes{res, rb, rest}:
3546 IO.pure(Result<&1, &1, Err, Stream>, Done{stream.mk(tls, s, ms, res, Nil{}, pc.of(rb, rest))})
3547
3548def stream.sent(+tls: Bool, +ms: U32, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Result<&1, &1, Err, Stream>):
3549 (s, r) = m
3550 match r:
3551 case Fail{(+code, why)}:
3552 do IO<Result<&1, &1, Err, Stream>>:
3553 io.close(tls, s)
3554 return Fail{err.or_late(code, ErrWrite{code, why})}
3555 case Done{u}:
3556 stream.head(tls, ms, head, (s, ShMore{Bytes.new(0), 0}))
3557
3558def stream.conn(r: Result<&1, &1, Err, Conn>, +ms: U32, +head: Bool, wire: Bytes.Bytes) -> IO(Result<&1, &1, Err, Stream>):
3559 match r:
3560 case Fail{e}:
3561 IO.pure(Result<&1, &1, Err, Stream>, Fail{e})
3562 case Done{c}:
3563 match c:
3564 case Conn{+tls, s}:
3565 do IO<Result<&1, &1, Err, Stream>>:
3566 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(tls, s, wire)
3567 stream.sent(tls, ms, head, sent)
3568 case ConnH2{s, client}:
3569 do IO<Result<&1, &1, Err, Stream>>:
3570 Wire.tls.close(s)
3571 return Fail{ErrBad{}}
3572
3573# One connection per stream; the request says close.
3574def stream.origin(+ms: U32, +head: Bool, wire: Bytes.Bytes, a: Url.Abs, known: Bool) -> IO(Result<&1, &1, Err, Stream>):
3575 Url.Abs{+scheme, +host, +port, target} = a
3576 match known:
3577 case False{}:
3578 IO.pure(Result<&1, &1, Err, Stream>, Fail{ErrUrl{}})
3579 case True{}:
3580 do IO<Result<&1, &1, Err, Stream>>:
3581 ips : List<&2, String> <- Dns.resolve.all(host)
3582 c : Result<&1, &1, Err, Conn> <- conn.open.all(String.eq(scheme, "https"), ms, host, port, ips, None{}, False{})
3583 stream.conn(c, ms, head, wire)
3584
3585def 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>):
3586 Url.Abs{scheme, host, port, +target} = url
3587 (body, wire) = r
3588 do IO<Hop & Result<&1, &1, Err, Stream>>:
3589 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))
3590 return (Hop{method, url, headers, body}, got)
3591
3592# One request on its own connection. The hop comes back for the redirect.
3593def stream.one(h: Hop, +ms: U32) -> IO(Hop & Result<&1, &1, Err, Stream>):
3594 Hop{+method, +url, +headers, body} = h
3595 stream.one.of(method, url, headers, ms, Bytes.slice(body, 0, 4294967295))
3596
3597# Go: the next request. Drop: close this stream, then go on. Done: the answer.
3598type Sn is Type:
3599 SnGo{left: Nat, hop: Hop}
3600 SnDrop{st: Stream, next: Next}
3601 SnDone{r: Result<&1, &1, Err, Stream>}
3602
3603def sn.of(n: Next) -> Sn:
3604 match n:
3605 case NGo{l, h}:
3606 SnGo{l, h}
3607 case NStop{}:
3608 SnDone{Fail{ErrRedirect{}}}
3609 case NDone{m}:
3610 match m:
3611 case Fail{e}:
3612 SnDone{Fail{e}}
3613 case Done{r}:
3614 SnDone{Fail{ErrBad{}}}
3615
3616def stream.decide.n(st: Stream, n: Next) -> Sn:
3617 match n:
3618 case NDone{m}:
3619 SnDone{Done{st}}
3620 case NGo{l, h}:
3621 SnDrop{st, NGo{l, h}}
3622 case NStop{}:
3623 SnDrop{st, NStop{}}
3624
3625def stream.decide.of(+left: Nat, hop: Hop, sr: Stream & Res) -> Sn:
3626 (st, res) = sr
3627 stream.decide.n(st, fetch.decide(left, hop, Done{res}))
3628
3629def stream.decide(+left: Nat, x: Hop & Result<&1, &1, Err, Stream>) -> Sn:
3630 (hop, r) = x
3631 match r:
3632 case Fail{e}:
3633 SnDone{Fail{e}}
3634 case Done{st}:
3635 stream.decide.of(left, hop, stream.res(st))
3636
3637@unsafe
3638def stream.hops(+ms: U32, sn: Sn) -> IO(Result<&1, &1, Err, Stream>):
3639 match sn:
3640 case SnDone{r}:
3641 IO.pure(Result<&1, &1, Err, Stream>, r)
3642 case SnGo{+left, hop}:
3643 do IO<Result<&1, &1, Err, Stream>>:
3644 x : Hop & Result<&1, &1, Err, Stream> <- stream.one(hop, ms)
3645 stream.hops(ms, stream.decide(left, x))
3646 case SnDrop{st, next}:
3647 do IO<Result<&1, &1, Err, Stream>>:
3648 stream.close(st)
3649 stream.hops(ms, sn.of(next))
3650
3651type Opened is Type:
3652 Opened{decs: List<&1, Zlib.Decoder>, bad: Bool}
3653
3654def stream.open.got(st: Opened, r: Result<&1, &1, U32 & String, Zlib.Decoder>) -> Opened:
3655 Opened{decs, bad} = st
3656 match r:
3657 case Fail{e}:
3658 Opened{decs, True{}}
3659 case Done{d}:
3660 Opened{d <> decs, bad}
3661
3662def stream.open.add(st: Opened, m: IO(Result<&1, &1, U32 & String, Zlib.Decoder>)) -> IO(Opened):
3663 do IO<Opened>:
3664 r : Result<&1, &1, U32 & String, Zlib.Decoder> <- m
3665 return stream.open.got(st, r)
3666
3667def stream.open.zstd(zstd: Bool, st: Opened) -> IO(Opened):
3668 match zstd:
3669 case True{}:
3670 stream.open.add(st, Zlib.zstd.new())
3671 case False{}:
3672 IO.pure(Opened, st)
3673
3674def stream.open.br(br: Bool, +c: String, st: Opened) -> IO(Opened):
3675 match br:
3676 case True{}:
3677 stream.open.add(st, Zlib.brotli.new())
3678 case False{}:
3679 stream.open.zstd(String.eq(c, "zstd"), st)
3680
3681def stream.open.gz(gz: Bool, +c: String, st: Opened) -> IO(Opened):
3682 match gz:
3683 case True{}:
3684 stream.open.add(st, Zlib.inflate.new())
3685 case False{}:
3686 stream.open.br(String.eq(c, "br"), c, st)
3687
3688def stream.open.step(+c: String, st: Opened) -> IO(Opened):
3689 Opened{decs, bad} = st
3690 match bad:
3691 case True{}:
3692 IO.pure(Opened, Opened{decs, True{}})
3693 case False{}:
3694 stream.open.gz(Bool.or(String.eq(c, "gzip"), Bool.or(String.eq(c, "x-gzip"), String.eq(c, "deflate"))),
3695 c, Opened{decs, False{}})
3696
3697def stream.open.one(prev: IO(Opened), c: String) -> IO(Opened):
3698 do IO<Opened>:
3699 st : Opened <- prev
3700 stream.open.step(c, st)
3701
3702def stream.open.all(cs: List<&2, String>) -> IO(Opened):
3703 List.foldl(~&2, ~String, ~IO(Opened), ~stream.open.one, cs, IO.pure(Opened, Opened{Nil{}, False{}}))
3704
3705def stream.put.decs(st: Stream, decs: List<&1, Zlib.Decoder>) -> Stream:
3706 Stream{tls, s, ms, res, rb, out, old} = st
3707 Stream{tls, s, ms, res, rb, out, decs}
3708
3709def stream.init.opened(st: Stream, opened: Opened) -> IO(Result<&1, &1, Err, Stream>):
3710 Opened{decs, bad} = opened
3711 match bad:
3712 case True{}:
3713 do IO<Result<&1, &1, Err, Stream>>:
3714 stream.close(stream.put.decs(st, decs))
3715 return Fail{ErrBad{}}
3716 case False{}:
3717 IO.pure(Result<&1, &1, Err, Stream>, Done{stream.put.decs(st, List.reverse(&1, Zlib.Decoder, decs))})
3718
3719def stream.init.known(known: Bool, st: Stream, cs: List<&2, String>) -> IO(Result<&1, &1, Err, Stream>):
3720 match known:
3721 case False{}:
3722 IO.pure(Result<&1, &1, Err, Stream>, Done{st})
3723 case True{}:
3724 do IO<Result<&1, &1, Err, Stream>>:
3725 opened : Opened <- stream.open.all(cs)
3726 stream.init.opened(st, opened)
3727
3728def stream.init.st(+enc: String, st: Stream) -> IO(Result<&1, &1, Err, Stream>):
3729 Stream{tls, s, ms, res, rb, out, decs} = st
3730 Res{+status, +headers, body} = res
3731 +cs = List.reverse(&2, String, ce.split(fields(headers, "content-encoding")))
3732 stream.init.known(ce.known(cs, Con{"identity", Con{"x-gzip", ce.split(Con{enc, Nil{}})}}),
3733 Stream{tls, s, ms, Res{status, headers, body}, rb, out, decs}, cs)
3734
3735def stream.init(+enc: String, r: Result<&1, &1, Err, Stream>) -> IO(Result<&1, &1, Err, Stream>):
3736 match r:
3737 case Fail{e}:
3738 IO.pure(Result<&1, &1, Err, Stream>, Fail{e})
3739 case Done{st}:
3740 stream.init.st(enc, st)
3741
3742def stream.start(method: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, u: Maybe<&2, Url.Abs>) -> Sn:
3743 match u:
3744 case None{}:
3745 SnDone{Fail{ErrUrl{}}}
3746 case Some{a}:
3747 SnGo{20n, Hop{method, a, req.put(Map.to_list(&2, List<&2, String>, headers), empty()), body}}
3748
3749# Open a raw stream. Its body bytes and headers remain as sent.
3750def open.raw.with(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, +ms: U32) -> IO(Result<&1, &1, Err, Stream>):
3751 stream.hops(ms, stream.start(method, headers, body, Url.absolute(url)))
3752
3753def open.raw(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Stream>):
3754 open.raw.with(method, url, headers, body, 30000)
3755
3756def 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>):
3757 do IO<Result<&1, &1, Err, Stream>>:
3758 r : Result<&1, &1, Err, Stream> <-
3759 stream.hops(ms, stream.start(method, accept.enc(headers, enc), body, Url.absolute(url)))
3760 stream.init(enc, r)
3761
3762# Follow redirects, then decode each body piece by Content-Encoding. Unknown codings stay raw.
3763def open.with(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes, +ms: U32) -> IO(Result<&1, &1, Err, Stream>):
3764 do IO<Result<&1, &1, Err, Stream>>:
3765 enc : String <- codings()
3766 open.with.enc(enc, method, url, headers, body, ms)
3767
3768def open(method: String, url: String, headers: Map<&2, List<&2, String>>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, Stream>):
3769 open.with(method, url, headers, body, 30000)
3770
3771# Upload: the request body sent in chunks (RFC 9112 §7.1). err: the first failed write.
3772type Up is Type:
3773 Up{tls: Bool, s: Socket, ms: U32, head: Bool, err: Maybe<&2, Err>}
3774
3775def hex.digit(+n: U32) -> Char:
3776 Chr{Bool.pick(U32, U32.is_lt(n, 10), (48 + n : U32), (87 + n : U32))}
3777
3778def hex.go(k: Nat, +n: U32, acc: String) -> String:
3779 match k:
3780 case 0n:
3781 acc
3782 case 1n+p:
3783 hex.go(p, U32.shrn(n, 4n), SCon{hex.digit(U32.and(n, 15)), acc})
3784
3785def hex.trim(+s: String) -> String:
3786 match s:
3787 case SNil{}:
3788 SNil{}
3789 case SCon{Chr{+c}, +t}:
3790 Bool.pick(String, Bool.and(U32.is_eq(c, 48), Bool.not(String.is_empty(t))), hex.trim(t), SCon{Chr{c}, t})
3791
3792def hex(+n: U32) -> String:
3793 hex.trim(hex.go(8n, n, ""))
3794
3795def up.sent(+tls: Bool, +ms: U32, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> Up:
3796 (s, r) = m
3797 match r:
3798 case Fail{(+code, why)}:
3799 Up{tls, s, ms, head, Some{err.or_late(code, ErrWrite{code, why})}}
3800 case Done{u}:
3801 Up{tls, s, ms, head, None{}}
3802
3803def up.conn(r: Result<&1, &1, Err, Conn>, +ms: U32, +head: Bool, wire: String) -> IO(Result<&1, &1, Err, Up>):
3804 match r:
3805 case Fail{e}:
3806 IO.pure(Result<&1, &1, Err, Up>, Fail{e})
3807 case Done{c}:
3808 match c:
3809 case Conn{+tls, s}:
3810 do IO<Result<&1, &1, Err, Up>>:
3811 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send(tls, s, wire)
3812 return Done{up.sent(tls, ms, head, sent)}
3813 case ConnH2{s, client}:
3814 do IO<Result<&1, &1, Err, Up>>:
3815 Wire.tls.close(s)
3816 return Fail{ErrBad{}}
3817
3818def up.head(+method: String, +target: String, +hf: String, +headers: Map<&2, List<&2, String>>) -> String:
3819 request(method, target, set(set(set(req.put(Map.to_list(&2, List<&2, String>, headers), empty()), "host", hf), "connection", "close"), "transfer-encoding", "chunked"), "")
3820
3821def up.origin(+method: String, +ms: U32, headers: Map<&2, List<&2, String>>, a: Url.Abs, known: Bool) -> IO(Result<&1, &1, Err, Up>):
3822 Url.Abs{+scheme, +host, +port, +target} = a
3823 match known:
3824 case False{}:
3825 IO.pure(Result<&1, &1, Err, Up>, Fail{ErrUrl{}})
3826 case True{}:
3827 do IO<Result<&1, &1, Err, Up>>:
3828 ips : List<&2, String> <- Dns.resolve.all(host)
3829 c : Result<&1, &1, Err, Conn> <- conn.open.all(String.eq(scheme, "https"), ms, host, port, ips, None{}, False{})
3830 up.conn(c, ms, String.eq(method, "HEAD"), up.head(method, target, Url.host_field(a), headers))
3831
3832def up.url(+method: String, +ms: U32, headers: Map<&2, List<&2, String>>, u: Maybe<&2, Url.Abs>) -> IO(Result<&1, &1, Err, Up>):
3833 match u:
3834 case None{}:
3835 IO.pure(Result<&1, &1, Err, Up>, Fail{ErrUrl{}})
3836 case Some{+a}:
3837 up.origin(method, ms, headers, a, pool.scheme.ok(a))
3838
3839# Http.upload(method, url, headers) sends the head. A streamed body cannot be replayed, so redirects are not followed.
3840def upload.with(+method: String, url: String, headers: Map<&2, List<&2, String>>, +ms: U32) -> IO(Result<&1, &1, Err, Up>):
3841 up.url(method, ms, headers, Url.absolute(url))
3842
3843def upload(+method: String, url: String, headers: Map<&2, List<&2, String>>) -> IO(Result<&1, &1, Err, Up>):
3844 upload.with(method, url, headers, 30000)
3845
3846def up.wrote(+tls: Bool, +ms: U32, +head: Bool, m: Socket & Result<&1, &1, U32 & String, Unit>) -> Up & Result<&2, &2, Err, Unit>:
3847 (s, r) = m
3848 match r:
3849 case Fail{(+code, why)}:
3850 +e = err.or_late(code, ErrWrite{code, why})
3851 (Up{tls, s, ms, head, Some{e}}, Fail{e})
3852 case Done{u}:
3853 (Up{tls, s, ms, head, None{}}, Done{Unit{}})
3854
3855# One write per chunk, so the size line and the data do not wait on each other (Nagle).
3856def up.put(+tls: Bool, s: Socket, +ms: U32, +head: Bool, +len: U32, piece: Bytes.Bytes, skip: Bool) -> IO(Up & Result<&2, &2, Err, Unit>):
3857 match skip:
3858 case True{}:
3859 IO.pure(Up & Result<&2, &2, Err, Unit>, (Up{tls, s, ms, head, None{}}, Done{Unit{}}))
3860 case False{}:
3861 do IO<Up & Result<&2, &2, Err, Unit>>:
3862 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{}}}}))
3863 return up.wrote(tls, ms, head, sent)
3864
3865def up.chunk(+tls: Bool, s: Socket, +ms: U32, +head: Bool, piece: Bytes.Bytes) -> IO(Up & Result<&2, &2, Err, Unit>):
3866 Bytes.Bytes{+len, buf} = piece
3867 up.put(tls, s, ms, head, len, Bytes.Bytes{len, buf}, U32.is_zero(len))
3868
3869# One chunk. An empty piece sends nothing, since an empty chunk would end the body.
3870def upload.write(up: Up, piece: Bytes.Bytes) -> IO(Up & Result<&2, &2, Err, Unit>):
3871 Up{+tls, s, +ms, +head, err} = up
3872 match err:
3873 case Some{+e}:
3874 IO.pure(Up & Result<&2, &2, Err, Unit>, (Up{tls, s, ms, head, Some{e}}, Fail{e}))
3875 case None{}:
3876 up.chunk(tls, s, ms, head, piece)
3877
3878# Ends the body and returns the response as a stream.
3879def upload.finish(up: Up) -> IO(Result<&1, &1, Err, Stream>):
3880 Up{+tls, s, +ms, +head, err} = up
3881 match err:
3882 case Some{e}:
3883 do IO<Result<&1, &1, Err, Stream>>:
3884 io.close(tls, s)
3885 return Fail{e}
3886 case None{}:
3887 do IO<Result<&1, &1, Err, Stream>>:
3888 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send(tls, s, "0\r\n\r\n")
3889 stream.sent(tls, ms, head, sent)
3890
3891def reply.bytes(res: Res, head: Bool, close: Bool) -> Bytes.Bytes:
3892 Res{+status, +headers, body} = res
3893 encode.on(Res{status, Bool.pick(Map<&2, List<&2, String>>, close, set(headers, "connection", "close"), headers), body}, head)
3894
3895def reply.fail.bytes(+status: U32) -> Res:
3896 Res{status, empty(), Bytes.from_string(reason(status))}
3897
3898def reply.sent.close(m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Unit):
3899 (s, r) = m
3900 Socket.close(s)
3901
3902def reply_fail(s: Socket, +status: U32) -> IO(Unit):
3903 do IO<Unit>:
3904 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(False{}, s, encode(reply.fail.bytes(status)))
3905 reply.sent.close(sent)
3906
3907
3908# The head is parsed once, when it is whole. Body pieces are kept as they come and joined once.
3909type Sv is Type:
3910 SvHead{buf: Bytes.Bytes}
3911 SvLen{req: Req, v11: Bool, left: U32, parts: List<&1, Bytes.Bytes>}
3912 SvChunk{req: Req, v11: Bool, n: U32, st: Dc, parts: List<&1, Bytes.Bytes>}
3913
3914# More: read on, first answering 100 Continue when cont is set.
3915type Turn is Type:
3916 TurnClose{}
3917 TurnFail{status: U32}
3918 TurnReq{req: Req, rest: Bytes.Bytes, v11: Bool}
3919 TurnMore{sv: Sv, cont: Bool}
3920
3921def serve.max() -> Nat:
3922 fetch.max()
3923
3924def sv.none() -> Sv:
3925 SvHead{Bytes.new(0)}
3926
3927def sv.body(req: Req, +v11: Bool, parts: List<&1, Bytes.Bytes>, rest: Bytes.Bytes) -> Turn:
3928 Req{method, path, headers, body} = req
3929 TurnReq{Req{method, path, headers, rb.body(parts)}, rest, v11}
3930
3931def sv.len.cut(req: Req, +v11: Bool, parts: List<&1, Bytes.Bytes>, +len: U32, +left: U32, r: Bytes.Bytes & Bytes.Bytes) -> Turn:
3932 (piece, last) = r
3933 sv.body(req, v11, Con{last, parts}, bytes.snd(Bytes.slice(piece, left, (len - left : U32))))
3934
3935def sv.len.have(short: Bool, req: Req, +v11: Bool, +left: U32, parts: List<&1, Bytes.Bytes>, +len: U32, piece: Bytes.Bytes) -> Turn:
3936 match short:
3937 case True{}:
3938 TurnMore{SvLen{req, v11, (left - len : U32), Con{piece, parts}}, False{}}
3939 case False{}:
3940 sv.len.cut(req, v11, parts, len, left, Bytes.slice(piece, 0, left))
3941
3942def sv.len(req: Req, +v11: Bool, +left: U32, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Turn:
3943 Bytes.Bytes{+len, buf} = piece
3944 sv.len.have(U32.is_lt(len, left), req, v11, left, parts, len, Bytes.Bytes{len, buf})
3945
3946def sv.chunk.of(req: Req, +v11: Bool, +n: U32, c: Ck) -> Turn:
3947 Ck{st, parts, rest} = c
3948 match st:
3949 case DcDone{}:
3950 sv.body(req, v11, parts, rest)
3951 case DcBad{}:
3952 TurnFail{400}
3953 case DcSize{a, b}:
3954 TurnMore{SvChunk{req, v11, n, DcSize{a, b}, parts}, False{}}
3955 case DcExt{x}:
3956 TurnMore{SvChunk{req, v11, n, DcExt{x}, parts}, False{}}
3957 case DcSizeLf{x}:
3958 TurnMore{SvChunk{req, v11, n, DcSizeLf{x}, parts}, False{}}
3959 case DcData{k}:
3960 TurnMore{SvChunk{req, v11, n, DcData{k}, parts}, False{}}
3961 case DcDataCr{}:
3962 TurnMore{SvChunk{req, v11, n, DcDataCr{}, parts}, False{}}
3963 case DcDataLf{}:
3964 TurnMore{SvChunk{req, v11, n, DcDataLf{}, parts}, False{}}
3965 case DcTr{j}:
3966 TurnMore{SvChunk{req, v11, n, DcTr{j}, parts}, False{}}
3967
3968def sv.chunk.cap(big: Bool, req: Req, +v11: Bool, +n: U32, st: Dc, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Turn:
3969 match big:
3970 case True{}:
3971 TurnFail{413}
3972 case False{}:
3973 sv.chunk.of(req, v11, n, ck(piece, st, parts))
3974
3975def sv.chunk(+max: Nat, req: Req, +v11: Bool, +n: U32, st: Dc, parts: List<&1, Bytes.Bytes>, piece: Bytes.Bytes) -> Turn:
3976 Bytes.Bytes{+len, buf} = piece
3977 +n2 = (n + len : U32)
3978 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})
3979
3980# RFC 9110 §10.1.1: answer 100 Continue only when the body is still to come.
3981def sv.cont(want: Bool, t: Turn) -> Turn:
3982 match t:
3983 case TurnMore{sv, c}:
3984 TurnMore{sv, want}
3985 case TurnClose{}:
3986 TurnClose{}
3987 case TurnFail{s}:
3988 TurnFail{s}
3989 case TurnReq{req, rest, v11}:
3990 TurnReq{req, rest, v11}
3991
3992def sv.cl.k(big: Bool, req: Req, +v11: Bool, +k: U32, rest: Bytes.Bytes) -> Turn:
3993 match big:
3994 case True{}:
3995 TurnFail{413}
3996 case False{}:
3997 sv.len(req, v11, k, Nil{}, rest)
3998
3999def sv.cl(+max: Nat, req: Req, +v11: Bool, rest: Bytes.Bytes, n: Maybe<&2, U32>) -> Turn:
4000 match n:
4001 case None{}:
4002 TurnFail{400}
4003 case Some{+k}:
4004 sv.cl.k(Nat.is_lt(max, U32.to_nat(k)), req, v11, k, rest)
4005
4006def sv.frame(+max: Nat, req: Req, +v11: Bool, rest: Bytes.Bytes, te: Bool) -> Turn:
4007 Req{method, path, +headers, body} = req
4008 match te:
4009 case True{}:
4010 sv.chunk(max, Req{method, path, headers, body}, v11, 0, dc.start(), Nil{}, rest)
4011 case False{}:
4012 sv.cl(max, Req{method, path, headers, body}, v11, rest, parse_u32(header(headers, "content-length")))
4013
4014def sv.expects(+v11: Bool, +headers: Map<&2, List<&2, String>>) -> Bool:
4015 Bool.and(v11, String.eq(String.to_lower(header(headers, "expect")), "100-continue"))
4016
4017def sv.got.head(+max: Nat, +v11: Bool, rest: Bytes.Bytes, req: Req) -> Turn:
4018 Req{method, path, +headers, body} = req
4019 sv.cont(sv.expects(v11, headers), sv.frame(max, Req{method, path, headers, body}, v11, rest, has_header(headers, "transfer-encoding")))
4020
4021def sv.parsed(+max: Nat, +v11: Bool, rest: Bytes.Bytes, g: Got) -> Turn:
4022 match g:
4023 case GotBad{}:
4024 TurnFail{400}
4025 case GotMore{}:
4026 TurnFail{400}
4027 case GotReq{req}:
4028 TurnReq{req, rest, v11}
4029 case GotHead{req}:
4030 sv.got.head(max, v11, rest, req)
4031
4032def sv.split(+max: Nat, +hlen: U32, +len: U32, r: Bytes.Bytes & Bytes.Bytes) -> Turn:
4033 (buf, hb) = r
4034 +head = Bytes.to_string(hb)
4035 sv.parsed(max, req.v11(head), bytes.snd(Bytes.slice(buf, hlen, (len - hlen : U32))), parse.got(head))
4036
4037def sv.hit.none(big: Bool, buf: Bytes.Bytes) -> Turn:
4038 match big:
4039 case True{}:
4040 TurnFail{431}
4041 case False{}:
4042 TurnMore{SvHead{buf}, False{}}
4043
4044def sv.hit.some(big: Bool, +max: Nat, +hlen: U32, +len: U32, buf: Bytes.Bytes) -> Turn:
4045 match big:
4046 case True{}:
4047 TurnFail{431}
4048 case False{}:
4049 sv.split(max, hlen, len, Bytes.slice(buf, 0, hlen))
4050
4051# RFC 6585 §5: a head over 64 KiB is refused.
4052def sv.hit(+max: Nat, +len: U32, buf: Bytes.Bytes, at: Maybe<&2, U32>) -> Turn:
4053 match at:
4054 case None{}:
4055 sv.hit.none(U32.is_lt(65536, len), buf)
4056 case Some{+i}:
4057 +hlen = (i + 4 : U32)
4058 sv.hit.some(U32.is_lt(65536, hlen), max, hlen, len, buf)
4059
4060def sv.seek.of(+max: Nat, +len: U32, +from: U32, buf: Bytes.Bytes, r: Bytes.Bytes & Maybe<&2, U32>) -> Turn:
4061 (tail, m) = r
4062 sv.hit(max, len, buf, found.at(from, m))
4063
4064def sv.seek(+max: Nat, +len: U32, +from: U32, r: Bytes.Bytes & Bytes.Bytes) -> Turn:
4065 (buf, tail) = r
4066 sv.seek.of(max, len, from, buf, Bytes.find(tail, "\r\n\r\n"))
4067
4068# Only the new bytes, and the 3 before them, can finish the blank line.
4069def sv.head.at(+max: Nat, +from: U32, buf: Bytes.Bytes) -> Turn:
4070 Bytes.Bytes{+len, b} = buf
4071 sv.seek(max, len, from, Bytes.slice(Bytes.Bytes{len, b}, from, (len - from : U32)))
4072
4073def sv.head(+max: Nat, buf: Bytes.Bytes, piece: Bytes.Bytes) -> Turn:
4074 Bytes.Bytes{+ol, ob} = buf
4075 sv.head.at(max, Bool.pick(U32, U32.is_lt(ol, 3), 0, (ol - 3 : U32)), Bytes.append(Bytes.Bytes{ol, ob}, piece))
4076
4077def sv.closed.pick(empty: Bool) -> Turn:
4078 match empty:
4079 case True{}:
4080 TurnClose{}
4081 case False{}:
4082 TurnFail{400}
4083
4084def sv.closed.head(buf: Bytes.Bytes) -> Turn:
4085 Bytes.Bytes{+len, b} = buf
4086 sv.closed.pick(U32.is_eq(len, 0))
4087
4088# A close mid-request is a request cut short (RFC 9112 §8).
4089def sv.step(closed: Bool, +max: Nat, sv: Sv, piece: Bytes.Bytes) -> Turn:
4090 match closed:
4091 case True{}:
4092 match sv:
4093 case SvHead{buf}:
4094 sv.closed.head(buf)
4095 case SvLen{req, v11, left, parts}:
4096 TurnFail{400}
4097 case SvChunk{req, v11, n, st, parts}:
4098 TurnFail{400}
4099 case False{}:
4100 match sv:
4101 case SvHead{buf}:
4102 sv.head(max, buf, piece)
4103 case SvLen{req, +v11, +left, parts}:
4104 sv.len(req, v11, left, parts, piece)
4105 case SvChunk{req, +v11, +n, st, parts}:
4106 sv.chunk(max, req, v11, n, st, parts, piece)
4107
4108def sv.frame.req(t: Turn) -> Maybe<&1, String & String>:
4109 match t:
4110 case TurnReq{req, rest, v11}:
4111 Req{method, path, headers, body} = req
4112 Some{(Bytes.to_string(body), Bytes.to_string(rest))}
4113 case TurnMore{sv, c}:
4114 None{}
4115 case TurnFail{s}:
4116 None{}
4117 case TurnClose{}:
4118 None{}
4119
4120def sv.frame.go(xs: List<&2, String>, t: Turn) -> Maybe<&1, String & String>:
4121 match xs:
4122 case Nil{}:
4123 sv.frame.req(t)
4124 case Con{+x, rest}:
4125 match t:
4126 case TurnMore{sv, c}:
4127 sv.frame.go(rest, sv.step(False{}, serve.max(), sv, Bytes.from_string(x)))
4128 case TurnReq{req, r, v11}:
4129 sv.frame.req(TurnReq{req, r, v11})
4130 case TurnFail{s}:
4131 None{}
4132 case TurnClose{}:
4133 None{}
4134
4135# The body and the bytes after it, once the pieces make a whole request; None otherwise.
4136def serve.frame(xs: List<&2, String>) -> Maybe<&1, String & String>:
4137 sv.frame.go(xs, TurnMore{sv.none(), False{}})
4138
4139def talk.piece(+max: Nat, sv: Sv, p: U32 & Array<U32>) -> Turn:
4140 (+len, buf) = p
4141 sv.step(U32.is_eq(len, 0), max, sv, Bytes.Bytes{len, buf})
4142
4143def talk.next(+max: Nat, sv: Sv, m: Socket & Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Socket & Turn:
4144 (s, r) = m
4145 match r:
4146 case Fail{e}:
4147 (s, TurnClose{})
4148 case Done{p}:
4149 (s, talk.piece(max, sv, p))
4150
4151def talk.after.pick(empty: Bool, +max: Nat, rest: Bytes.Bytes) -> Turn:
4152 match empty:
4153 case True{}:
4154 TurnMore{sv.none(), False{}}
4155 case False{}:
4156 sv.step(False{}, max, sv.none(), rest)
4157
4158def talk.after.rest(+max: Nat, rest: Bytes.Bytes, s: Socket) -> Socket & Turn:
4159 Bytes.Bytes{+len, buf} = rest
4160 (s, talk.after.pick(U32.is_eq(len, 0), max, Bytes.Bytes{len, buf}))
4161
4162def talk.after.keep(keep: Bool, +max: Nat, rest: Bytes.Bytes, s: Socket) -> Socket & Turn:
4163 match keep:
4164 case False{}:
4165 (s, TurnClose{})
4166 case True{}:
4167 talk.after.rest(max, rest, s)
4168
4169def talk.after(+max: Nat, keep: Bool, rest: Bytes.Bytes, m: Socket & Result<&1, &1, U32 & String, Unit>) -> Socket & Turn:
4170 (s, r) = m
4171 match r:
4172 case Fail{e}:
4173 (s, TurnClose{})
4174 case Done{u}:
4175 talk.after.keep(keep, max, rest, s)
4176
4177def talk.send(+max: Nat, s: Socket, rest: Bytes.Bytes, +headers: Map<&2, List<&2, String>>, v11: Bool, +head: Bool, res: Res) -> IO(Socket & Turn):
4178 Res{+status, +rh, body} = res
4179 +keep = serve.keep(headers, v11, status, rh)
4180 do IO<Socket & Turn>:
4181 sent : Socket & Result<&1, &1, U32 & String, Unit> <- io.send.bytes(False{}, s, reply.bytes(Res{status, rh, body}, head, Bool.not(keep)))
4182 return talk.after(max, keep, rest, sent)
4183
4184def talk.cont.sent(m: Socket & Result<&1, &1, U32 & String, Unit>) -> Socket:
4185 (s, r) = m
4186 s
4187
4188def talk.cont(cont: Bool, s: Socket) -> IO(Socket):
4189 match cont:
4190 case False{}:
4191 IO.pure(Socket, s)
4192 case True{}:
4193 do IO<Socket>:
4194 sent : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.send(s, "HTTP/1.1 100 Continue\r\n\r\n")
4195 return talk.cont.sent(sent)
4196
4197@unsafe
4198def talk(~h: Req -> IO(Res), +max: Nat, st: Socket & Turn) -> IO(Unit):
4199 (s, t) = st
4200 match t:
4201 case TurnMore{sv, cont}:
4202 do IO<Unit>:
4203 s2 : Socket <- talk.cont(cont, s)
4204 m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- Wire.recv.words(s2, 65536, 30000)
4205 talk(~h, max, talk.next(max, sv, m))
4206 case TurnReq{req, rest, v11}:
4207 Req{+method, path, +headers, body} = req
4208 do IO<Unit>:
4209 res : Res <- h(Req{method, path, headers, body})
4210 next : Socket & Turn <- talk.send(max, s, rest, headers, v11, String.eq(method, "HEAD"), res)
4211 talk(~h, max, next)
4212 case TurnFail{status}:
4213 reply_fail(s, status)
4214 case TurnClose{}:
4215 Socket.close(s)
4216
4217def conn(~h: Req -> IO(Res), +max: Nat, m: Listener & Result<&1, &1, U32 & String, Socket>) -> IO(Listener):
4218 (l, r) = m
4219 do IO<Listener>:
4220 s : Socket <- IO.pass(Socket, r)
4221 IO.spawn(Unit, talk(~h, max, (s, TurnMore{sv.none(), False{}})))
4222 return l
4223
4224@unsafe
4225def loop(~h: Req -> IO(Res), +max: Nat, l: Listener) -> IO(Unit):
4226 do IO<Unit>:
4227 m : Listener & Result<&1, &1, U32 & String, Socket> <- TCP.accept(l)
4228 l2 : Listener <- conn(~h, max, m)
4229 loop(~h, max, l2)
4230
4231def serve.with(~h: Req -> IO(Res), +port: U32, +max: Nat) -> IO(Unit):
4232 do IO<Unit>:
4233 l : Listener <- IO.try(Listener, TCP.listen(port))
4234 IO.print("http://127.0.0.1:" ++ U32.show(port))
4235 loop(~h, max, l)
4236
4237def serve(~h: Req -> IO(Res), +port: U32) -> IO(Unit):
4238 serve.with(~h, port, serve.max())