http.bend

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