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