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