http.bend

bend-kit-http@0.15.0.3 · 3,023 lines · 0 definitions

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