http.bend

bend-kit-http@0.15.0.4 · 3,084 lines · 0 definitions

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