src/http.bend
emerging-ezhttp@0.20.0.0 · 1,667 lines · 0 definitions
1# ezhttp/src/http: HTTP/1.1 message text for client and server — request and
2# response formatting/parsing — with no sockets. Semantics follow RFC 9110;
3# message syntax and framing follow RFC 9112. TLS is outside this module.
4import Base
5import emerging-ezhttp@0.20.0.0/src/body.bend as Body
6
7# a string divided at the first occurrence of a pattern, or not divided at all
8type Cut is Data:
9 NoCut{}
10 Cut{before: String, after: String}
11
12# one header field name and value (RFC 9110 §5 / RFC 9112 §5)
13type Header is Data:
14 H{name: String, value: String}
15
16# what a response turned out to be: status, headers, framed body — or why not
17type Reply is Data:
18 Torn{why: String}
19 Reply{status: U32, headers: List<&2, Header>, body: String}
20
21# the first of a list of pieces, "" when there are none
22def first(ps: List<&2, String>) -> String:
23 match ps:
24 case []:
25 ""
26 case h <> t:
27 h
28
29# the second of a list of pieces, "" when there is no second
30def second(ps: List<&2, String>) -> String:
31 match ps:
32 case []:
33 ""
34 case h <> t:
35 first(t)
36
37# one char of the divide, put back on the front of what the rest found
38def divide.push(h: Char, r: Cut) -> Cut:
39 match r:
40 case NoCut{}:
41 NoCut{}
42 case Cut{before, after}:
43 Cut{SCon{h, before}, after}
44
45# one step of the walk; rest is a thunk so Bool.pick does not force recursion
46def divide.step(here: Bool, h: Char, t: String, n: Nat,
47 rest: Unit -> Cut) -> Cut:
48 match here:
49 case True{}:
50 Cut{"", String.drop(SCon{h, t}, n)}
51 case False{}:
52 divide.push(h, rest(Unit{}))
53
54# the walk: stop at the first hit
55def divide.go(s: String, +pat: String, +n: Nat) -> Cut:
56 match s:
57 case SNil{}:
58 NoCut{}
59 case SCon{+h, +t}:
60 divide.step(String.starts_with(SCon{h, t}, pat), h, t, n,
61 _u => divide.go(t, pat, n))
62
63# a string in two halves around the first occurrence of a pattern
64def divide(s: String, +pat: String) -> Cut:
65 divide.go(s, pat, String.length(pat))
66
67# the value of one hex digit's code point, or 16 when it is not one
68def hex.of(+u: U32) -> U32:
69 Bool.pick(U32, Bool.and(U32.is_ge(u, 48), U32.is_le(u, 57)), U32.sub(u, 48),
70 Bool.pick(U32, Bool.and(U32.is_ge(u, 97), U32.is_le(u, 102)), U32.sub(u, 87),
71 Bool.pick(U32, Bool.and(U32.is_ge(u, 65), U32.is_le(u, 70)), U32.sub(u, 55),
72 16)))
73
74# the value of one hex digit, or 16 when the char is not one
75def hex.val(c: Char) -> U32:
76 hex.of(Char.to_u32(c))
77
78# one step of the hex read
79def hex.step(done: Bool, acc: Nat, rest: Unit -> Nat) -> Nat:
80 match done:
81 case True{}:
82 acc
83 case False{}:
84 rest(Unit{})
85
86# the hex digits at the front of a string, read until one is not a digit
87def hex.go(s: String, +acc: Nat) -> Nat:
88 match s:
89 case SNil{}:
90 acc
91 case SCon{+h, t}:
92 +v = hex.val(h)
93 hex.step(U32.is_ge(v, 16), acc,
94 _u => hex.go(t, Nat.add(Nat.mul(acc, 16n), U32.to_nat(v))))
95
96# chunk-size from a chunk header (RFC 9112 §7.1); extensions after `;` ignored
97def hexlen(s: String) -> Nat:
98 hex.go(String.trim(first(String.split(s, ';'))), 0n)
99
100# whether a character is a hex digit
101def hex.digit(c: Char) -> Bool:
102 U32.is_lt(hex.val(c), 16)
103
104# the rest of a hex token once the first digit is known
105def hex.rest(token: String, good: Bool) -> Bool:
106 match token good:
107 case _ False{}:
108 False{}
109 case SNil{} True{}:
110 True{}
111 case SCon{h, t} True{}:
112 hex.rest(t, hex.digit(h))
113
114# a chunk-size token is one or more hex digits (RFC 9112 §7.1)
115def hex.well(token: String) -> Bool:
116 match token:
117 case SNil{}:
118 False{}
119 case SCon{h, t}:
120 hex.rest(t, hex.digit(h))
121
122# the chunk-size token, extensions after `;` removed
123def chunks.token(before: String) -> String:
124 String.trim(first(String.split(before, ';')))
125
126# octets one code point takes in UTF-8, for a text written onto the wire
127# (RFC 3629 §3). Content-Length counts octets (RFC 9110 §8.6); a Bend String
128# counts code points.
129def utf8.width(+u: U32) -> Nat:
130 Bool.pick(Nat, U32.is_lt(u, 128), 1n,
131 Bool.pick(Nat, U32.is_lt(u, 2048), 2n,
132 Bool.pick(Nat, U32.is_lt(u, 65536), 3n, 4n)))
133
134# how many octets of UTF-8 a text is
135def utf8.len(s: String) -> Nat:
136 match s:
137 case SNil{}:
138 0n
139 case SCon{h, t}:
140 Nat.add(utf8.width(Char.to_u32(h)), utf8.len(t))
141
142# What is received is octets, one character each (SPEC.md HTTP-BODY-1): the
143# octs.* walks below count a character as one octet.
144
145# octets one received character stands for: one
146def octs.width(+_u: U32) -> Nat:
147 1n
148
149# how many octets a received text is
150def octs.len(s: String) -> Nat:
151 match s:
152 case SNil{}:
153 0n
154 case SCon{h, t}:
155 Nat.add(octs.width(Char.to_u32(h)), octs.len(t))
156
157# one step of the take
158def octs.take.step(short: Bool, h: Char, rest: Unit -> String) -> String:
159 match short:
160 case True{}:
161 SNil{}
162 case False{}:
163 SCon{h, rest(Unit{})}
164
165# the front of a string that is this many bytes of UTF-8
166def octs.take(s: String, +n: Nat) -> String:
167 match s:
168 case SNil{}:
169 SNil{}
170 case SCon{+h, t}:
171 +w = octs.width(Char.to_u32(h))
172 octs.take.step(Nat.is_lt(n, w), h, _u => octs.take(t, Nat.sub(n, w)))
173
174# one step of the drop
175def octs.drop.step(short: Bool, h: Char, t: String,
176 rest: Unit -> String) -> String:
177 match short:
178 case True{}:
179 SCon{h, t}
180 case False{}:
181 rest(Unit{})
182
183# the rest of a string after this many bytes of UTF-8
184def octs.drop(s: String, +n: Nat) -> String:
185 match s:
186 case SNil{}:
187 SNil{}
188 case SCon{+h, +t}:
189 +w = octs.width(Char.to_u32(h))
190 octs.drop.step(Nat.is_lt(n, w), h, t, _u => octs.drop(t, Nat.sub(n, w)))
191
192# a decimal digit's value, or 10 when the character is not a digit
193def digits.val.of(+u: U32) -> U32:
194 Bool.pick(U32, Bool.and(U32.is_ge(u, 48), U32.is_le(u, 57)), U32.sub(u, 48), 10)
195
196# a decimal digit's value, or 10 when the character is not a digit
197def digits.val(c: Char) -> U32:
198 digits.val.of(Char.to_u32(c))
199
200# accept one digit and keep reading, or stop when it is not a digit
201def digits.step(ok: Bool, next: Unit -> Maybe<&2, Nat>) -> Maybe<&2, Nat>:
202 match ok:
203 case False{}:
204 None{}
205 case True{}:
206 next(Unit{})
207
208# read a decimal token without building Base's Nat.read ceiling
209def digits.go(s: String, +acc: Nat, left: Nat) -> Maybe<&2, Nat>:
210 match s left:
211 case _ 0n:
212 None{}
213 case SNil{} 1n+k:
214 Some{acc}
215 case SCon{+h, t} 1n+k:
216 +d = digits.val(h)
217 digits.step(U32.is_lt(d, 10),
218 _u => digits.go(t, Nat.add(Nat.mul(acc, 10n), U32.to_nat(d)), k))
219
220# a short decimal (Content-Length, max-age). Empty is none. At most 9 digits.
221def digits.read(s: String) -> Maybe<&2, Nat>:
222 match s:
223 case SNil{}:
224 None{}
225 case SCon{h, t}:
226 digits.go(SCon{h, t}, 0n, 9n)
227
228# one step of the count: a character wider than what is still asked for
229# means the string is longer
230def octs.has.step(short: Bool, rest: Unit -> Bool) -> Bool:
231 match short:
232 case True{}:
233 True{}
234 case False{}:
235 rest(Unit{})
236
237# whether a string is at least this many bytes of UTF-8, walking no further
238# than that many (octs.len walks all of it)
239def octs.has(s: String, +n: Nat) -> Bool:
240 match s:
241 case SNil{}:
242 Bool.not(Nat.is_lt(0n, n))
243 case SCon{+h, t}:
244 +w = octs.width(Char.to_u32(h))
245 octs.has.step(Nat.is_lt(n, w), _u => octs.has(t, Nat.sub(n, w)))
246
247# a non-zero chunk has its data and the following CRLF
248def chunks.ready(+after: String, +n: Nat) -> Bool:
249 Bool.and(octs.has(after, Nat.add(n, 2n)),
250 String.starts_with(octs.drop(after, n), "\r\n"))
251
252# the next scan step, or why this chunk header is not usable
253type Next is Data:
254 Stop{}
255 Go{cut: Cut}
256 Reject{why: String}
257
258# one chunk header: reject non-hex sizes, stop on the 0 chunk, else continue
259def chunks.next.of(zero: Bool, ready: Bool, +after: String, +n: Nat) -> Next:
260 match zero ready:
261 case True{} _:
262 Stop{}
263 case False{} False{}:
264 Reject{"the chunked body stopped short"}
265 case False{} True{}:
266 Go{divide(octs.drop(after, Nat.add(n, 2n)), "\r\n")}
267
268# hex check, then the length
269def chunks.next.hex(+before: String, +after: String, ok: Bool) -> Next:
270 match ok:
271 case False{}:
272 Reject{"chunk size is not hexadecimal"}
273 case True{}:
274 +n = hexlen(before)
275 chunks.next.of(Nat.is_eq(n, 0n), chunks.ready(after, n), after, n)
276
277# classify one chunk header (RFC 9112 §7.1)
278def chunks.next(+before: String, +after: String) -> Next:
279 chunks.next.hex(before, after, hex.well(chunks.token(before)))
280
281# apply one scan step
282def chunks.scan.step(step: Next, rest: Cut -> Maybe<&2, String>)
283 -> Maybe<&2, String>:
284 match step:
285 case Stop{}:
286 None{}
287 case Reject{why}:
288 Some{why}
289 case Go{cut}:
290 rest(cut)
291
292# None when every chunk size is hex and the 0 chunk is reached
293def chunks.scan(fuel: Nat, c: Cut) -> Maybe<&2, String>:
294 match fuel c:
295 case 0n _:
296 Some{"the chunked body is truncated"}
297 case 1n+f NoCut{}:
298 None{}
299 case 1n+f Cut{before, +after}:
300 chunks.scan.step(chunks.next(before, after), cut => chunks.scan(f, cut))
301
302# a zero chunk ends the body; anything after it is a trailer (RFC 9112 §7.1)
303def chunks.more(+n: Nat, +after: String, rest: Unit -> String, zero: Bool)
304 -> String:
305 match zero:
306 case True{}:
307 ""
308 case False{}:
309 octs.take(after, n)
310 ++ rest(Unit{})
311
312# a chunked body put back together (RFC 9112 §7.1)
313def chunks(fuel: Nat, c: Cut) -> String:
314 match fuel c:
315 case 0n _:
316 ""
317 case 1n+f NoCut{}:
318 ""
319 case 1n+f Cut{before, +after}:
320 +n = hexlen(before)
321 chunks.more(n, after,
322 _u => chunks(f, divide(octs.drop(after, Nat.add(n, 2n)), "\r\n")),
323 Nat.is_eq(n, 0n))
324
325# a Transfer-Encoding: chunked body as the octets it stands for
326def dechunk(+s: String) -> String:
327 chunks(String.length(s), divide(s, "\r\n"))
328
329# whether a head line names this header (field names are case-insensitive:
330# RFC 9110 §5.1)
331def head.hit(h: String, +name: String) -> Bool:
332 String.starts_with(String.to_lower(h), name ++ ":")
333
334# this line's value when it is the header asked for
335def head.pick(hit: Bool, h: String, name: String, rest: String) -> String:
336 match hit:
337 case True{}:
338 String.trim(String.drop(h, Nat.add(String.length(name), 1n)))
339 case False{}:
340 rest
341
342# the value a head gave a header, "" when it gave none
343def head.go(ls: List<&2, String>, +name: String) -> String:
344 match ls:
345 case []:
346 ""
347 case +h <> t:
348 head.pick(head.hit(h, name), h, name, head.go(t, name))
349
350# this line's trimmed field value
351def head.value(h: String, name: String) -> String:
352 String.trim(String.drop(h, Nat.add(String.length(name), 1n)))
353
354# cons a value when the line is the header asked for
355def head.values.cons(hit: Bool, value: String, rest: Unit -> List<&2, String>)
356 -> List<&2, String>:
357 match hit:
358 case False{}:
359 rest(Unit{})
360 case True{}:
361 value <> rest(Unit{})
362
363# every value a head gave a header, in order (RFC 9112 §6.3 lists Content-Length)
364def head.values(ls: List<&2, String>, +name: String) -> List<&2, String>:
365 match ls:
366 case []:
367 []
368 case +h <> t:
369 head.values.cons(head.hit(h, name), head.value(h, name),
370 _u => head.values(t, name))
371
372# a field value still holding a line break is obs-fold, which we refuse
373def field.folded(+value: String) -> Bool:
374 Bool.or(String.contains(value, "\n"), String.contains(value, "\r"))
375
376# a trimmed field value, or none when it still contains obs-fold
377def field.keep(name: String, +value: String, folded: Bool) -> Maybe<&2, Header>:
378 match folded:
379 case True{}:
380 None{}
381 case False{}:
382 Some{H{name, value}}
383
384# name and trimmed value from a cut at the first colon
385def head.from_kept(before: String, +after: String) -> Maybe<&2, Header>:
386 +value = String.trim(after)
387 field.keep(before, value, field.folded(value))
388
389# one header line as a Header, or none when it has no colon
390def head.from_cut(c: Cut) -> Maybe<&2, Header>:
391 match c:
392 case NoCut{}:
393 None{}
394 case Cut{before, after}:
395 head.from_kept(before, after)
396
397# one header line as a Header, or none when it has no colon
398def head.line(h: String) -> Maybe<&2, Header>:
399 head.from_cut(divide(h, ":"))
400
401# prepend a parsed header when present
402def head.cons(m: Maybe<&2, Header>, rest: List<&2, Header>) -> List<&2, Header>:
403 match m:
404 case None{}:
405 rest
406 case Some{hdr}:
407 hdr <> rest
408
409# header lines after the status line as a list of fields
410def head.list(ls: List<&2, String>) -> List<&2, Header>:
411 match ls:
412 case []:
413 []
414 case h <> t:
415 head.cons(head.line(h), head.list(t))
416
417# one request header line
418def header.line(h: Header) -> String:
419 match h:
420 case H{name, value}:
421 name ++ ": " ++ value ++ "\r\n"
422
423# the value when this field is the one asked for
424def headers.find.pick(value: String, hit: Bool, rest: Unit -> String) -> String:
425 match hit:
426 case True{}:
427 value
428 case False{}:
429 rest(Unit{})
430
431# case-insensitive field lookup (RFC 9110 §5.1)
432def headers.find.go(hs: List<&2, Header>, +name: String) -> String:
433 match hs:
434 case []:
435 ""
436 case H{n, v} <> t:
437 headers.find.pick(v, String.eq(String.to_lower(n), name),
438 _u => headers.find.go(t, name))
439
440# the value of a field, "" when it is absent
441def headers.find(hs: List<&2, Header>, +name: String) -> String:
442 headers.find.go(hs, String.to_lower(name))
443
444# extra headers rendered in order
445def headers.lines(hs: List<&2, Header>) -> String:
446 match hs:
447 case []:
448 ""
449 case h <> t:
450 header.line(h) ++ headers.lines(t)
451
452# the Content-Length field when the body is not empty (RFC 9110 §8.6)
453def clen.field(+n: Nat, empty: Bool) -> List<&2, Header>:
454 match empty:
455 case True{}:
456 []
457 case False{}:
458 [H{"Content-Length", Nat.show(n)}]
459
460# Content-Length line when the body is not empty (RFC 9110 §8.6)
461def clen.line(+n: Nat, empty: Bool) -> String:
462 headers.lines(clen.field(n, empty))
463
464# the fields a request names: the ones ezhttp writes a default for, the ones
465# it always computes, and every other (SPEC.md HTTP-CLI-8)
466type Field is Data:
467 FHost{}
468 FAgent{}
469 FAccept{}
470 FConn{}
471 FClen{}
472 FOther{}
473
474# a field's place in the order above
475def field.rank(f: Field) -> U32:
476 match f:
477 case FHost{}:
478 0
479 case FAgent{}:
480 1
481 case FAccept{}:
482 2
483 case FConn{}:
484 3
485 case FClen{}:
486 4
487 case FOther{}:
488 5
489
490# whether two fields are the same one
491def field.same(a: Field, b: Field) -> Bool:
492 U32.is_eq(field.rank(a), field.rank(b))
493
494# a lower-case name that is not content-length
495def field.of.clen(hit: Bool) -> Field:
496 match hit:
497 case True{}:
498 FClen{}
499 case False{}:
500 FOther{}
501
502# a lower-case name that is not connection
503def field.of.conn(hit: Bool, +l: String) -> Field:
504 match hit:
505 case True{}:
506 FConn{}
507 case False{}:
508 field.of.clen(String.eq(l, "content-length"))
509
510# a lower-case name that is not accept
511def field.of.accept(hit: Bool, +l: String) -> Field:
512 match hit:
513 case True{}:
514 FAccept{}
515 case False{}:
516 field.of.conn(String.eq(l, "connection"), l)
517
518# a lower-case name that is not user-agent
519def field.of.agent(hit: Bool, +l: String) -> Field:
520 match hit:
521 case True{}:
522 FAgent{}
523 case False{}:
524 field.of.accept(String.eq(l, "accept"), l)
525
526# a lower-case name that is not host
527def field.of.host(hit: Bool, +l: String) -> Field:
528 match hit:
529 case True{}:
530 FHost{}
531 case False{}:
532 field.of.agent(String.eq(l, "user-agent"), l)
533
534# the field a lower-case name names
535def field.of(+l: String) -> Field:
536 field.of.host(String.eq(l, "host"), l)
537
538# the field a name names, compared case-insensitively (RFC 9110 §5.1)
539def field.name(name: String) -> Field:
540 field.of(String.to_lower(name))
541
542# the field a header line names
543def header.field(h: Header) -> Field:
544 match h:
545 case H{name, value}:
546 field.name(name)
547
548# keep a header in front of the rest, or not
549def fields.put(keep: Bool, h: Header, rest: List<&2, Header>)
550 -> List<&2, Header>:
551 match keep:
552 case True{}:
553 h <> rest
554 case False{}:
555 rest
556
557# the headers that name one field, in order
558def fields.of(+f: Field, hs: List<&2, Header>) -> List<&2, Header>:
559 match hs:
560 case []:
561 []
562 case +h <> t:
563 fields.put(field.same(f, header.field(h)), h, fields.of(f, t))
564
565# the caller's fields of a name, or the default when it gave none
566def fields.or(given: List<&2, Header>, dflt: List<&2, Header>)
567 -> List<&2, Header>:
568 match given:
569 case []:
570 dflt
571 case h <> t:
572 h <> t
573
574# a request's header fields for a body of n octets: Host, User-Agent and
575# Accept (the caller's, or the default), Connection: close, the caller's other
576# fields, Content-Length.
577# A caller's Connection or Content-Length is not sent: Connection: close lets
578# the connection end frame the body when no Content-Length / chunked framing
579# applies (RFC 9112 §9.6 / §6.3), and the body's length is computed.
580def request.fields.n(host: String, +hs: List<&2, Header>, +n: Nat)
581 -> List<&2, Header>:
582 List.append(&2, Header, fields.or(fields.of(FHost{}, hs), [H{"Host", host}]),
583 List.append(&2, Header,
584 fields.or(fields.of(FAgent{}, hs), [H{"User-Agent", "ezhttp"}]),
585 List.append(&2, Header,
586 fields.or(fields.of(FAccept{}, hs), [H{"Accept", "*/*"}]),
587 H{"Connection", "close"}
588 <> List.append(&2, Header, fields.of(FOther{}, hs),
589 clen.field(n, Nat.is_eq(n, 0n))))))
590
591# a request's header fields for a text body: the fields for its UTF-8 octets
592def request.fields(host: String, +hs: List<&2, Header>, +body: String)
593 -> List<&2, Header>:
594 request.fields.n(host, hs, utf8.len(body))
595
596# a request-line and headers (RFC 9112 §3, §5). Absolute-path request-target
597# (RFC 9112 §3.2.1); the fields are request.fields'.
598def request(method: String, host: String, path: String,
599 headers: List<&2, Header>, +body: String) -> String:
600 method ++ " " ++ path ++ " HTTP/1.1\r\n"
601 ++ headers.lines(request.fields(host, headers, body))
602 ++ "\r\n"
603 ++ body
604
605# the port a scheme implies: 443 for a secure one, 80 otherwise (RFC 9110
606# §4.2.1, §4.2.2)
607def port.dflt(secure: Bool) -> U32:
608 match secure:
609 case True{}:
610 443
611 case False{}:
612 80
613
614# the Host field value once it is known whether the port is the default
615def authority.of(host: String, +port: U32, dflt: Bool) -> String:
616 match dflt:
617 case True{}:
618 host
619 case False{}:
620 host ++ ":" ++ U32.show(port)
621
622# the Host field value: the host, and the port after a colon unless it is the
623# scheme's default (RFC 9110 §7.2)
624def authority(secure: Bool, host: String, +port: U32) -> String:
625 authority.of(host, port, U32.is_eq(port, port.dflt(secure)))
626
627# the request a client sends to host and port, over TLS when secure
628def request.at(method: String, secure: Bool, host: String, port: U32,
629 path: String, headers: List<&2, Header>, body: String) -> String:
630 request(method, authority(secure, host, port), path, headers, body)
631
632# the request text for a body of n octets that is sent after it as its own
633# octets: the request line, the fields for n octets, and the blank line
634def request.head(method: String, host: String, path: String,
635 headers: List<&2, Header>, +n: Nat) -> String:
636 method ++ " " ++ path ++ " HTTP/1.1\r\n"
637 ++ headers.lines(request.fields.n(host, headers, n))
638 ++ "\r\n"
639
640# the request text a client sends to host and port ahead of n octets
641def request.head.at(method: String, secure: Bool, host: String, port: U32,
642 path: String, headers: List<&2, Header>, n: Nat) -> String:
643 request.head(method, authority(secure, host, port), path, headers, n)
644
645# GET with optional headers
646def get_req(host: String, path: String, headers: List<&2, Header>) -> String:
647 request("GET", host, path, headers, "")
648
649# HEAD with optional headers (RFC 9110 §9.3.2): same as GET, no body
650def head_req(host: String, path: String, headers: List<&2, Header>) -> String:
651 request("HEAD", host, path, headers, "")
652
653# POST with body and optional headers
654def post_req(host: String, path: String, headers: List<&2, Header>,
655 body: String) -> String:
656 request("POST", host, path, headers, body)
657
658# PUT with body and optional headers (RFC 9110 §9.3.4)
659def put_req(host: String, path: String, headers: List<&2, Header>,
660 body: String) -> String:
661 request("PUT", host, path, headers, body)
662
663# DELETE with body and optional headers (RFC 9110 §9.3.5)
664def delete_req(host: String, path: String, headers: List<&2, Header>,
665 body: String) -> String:
666 request("DELETE", host, path, headers, body)
667
668# OPTIONS with optional headers (RFC 9110 §9.3.7). No request body.
669def options_req(host: String, path: String, headers: List<&2, Header>) -> String:
670 request("OPTIONS", host, path, headers, "")
671
672# GET, HEAD, and OPTIONS are safe (RFC 9110 §9.2.1). Tokens are case-sensitive.
673def method.safe(+method: String) -> Bool:
674 Bool.or(String.eq(method, "GET"),
675 Bool.or(String.eq(method, "HEAD"), String.eq(method, "OPTIONS")))
676
677# safe methods, plus PUT and DELETE, are idempotent (RFC 9110 §9.2.2)
678def method.idempotent(+method: String) -> Bool:
679 Bool.or(method.safe(method),
680 Bool.or(String.eq(method, "PUT"), String.eq(method, "DELETE")))
681
682# the rest of a token once this character is known
683def token.ok.step(space: Bool, rest: Unit -> Bool) -> Bool:
684 match space:
685 case True{}:
686 False{}
687 case False{}:
688 rest(Unit{})
689
690# a bearer token has no whitespace (RFC 6750 §2.1)
691def token.ok(s: String) -> Bool:
692 match s:
693 case SNil{}:
694 True{}
695 case SCon{h, t}:
696 token.ok.step(Char.is_space(h), _u => token.ok(t))
697
698# origin-form request-target: absolute-path, optional query (RFC 9112 §3.2.1)
699def target.origin(path: String) -> Bool:
700 String.starts_with(path, "/")
701
702# asterisk-form is only `*` and only for OPTIONS (RFC 9112 §3.2.4)
703def target.asterisk(method: String, star: Bool) -> Bool:
704 match star:
705 case False{}:
706 False{}
707 case True{}:
708 String.eq(method, "OPTIONS")
709
710# origin-form, or OPTIONS asterisk-form
711def target.form(method: String, path: String, absolute: Bool) -> Bool:
712 match absolute:
713 case True{}:
714 True{}
715 case False{}:
716 target.asterisk(method, String.eq(path, "*"))
717
718# a body against the length its head promised
719def parse.short(status: U32, headers: List<&2, Header>, n: Nat, body: String,
720 short: Bool) -> Reply:
721 match short:
722 case True{}:
723 Torn{"the response body stopped before its Content-Length"}
724 case False{}:
725 Reply{status, headers, octs.take(body, n)}
726
727# a body framed by Content-Length (RFC 9110 §8.6 / RFC 9112 §6.3)
728def parse.clen(status: U32, headers: List<&2, Header>, +n: Nat, +body: String)
729 -> Reply:
730 parse.short(status, headers, n, body, Nat.is_lt(octs.len(body), n))
731
732# Content-Length when present; else the rest of the connection is the body
733def parse.len(status: U32, headers: List<&2, Header>, m: Maybe<&2, Nat>,
734 body: String) -> Reply:
735 match m:
736 case None{}:
737 Reply{status, headers, body}
738 case Some{n}:
739 parse.clen(status, headers, n, body)
740
741# every Content-Length text equals the first
742def clen.agree.step(same: Bool, rest: Unit -> Bool) -> Bool:
743 match same:
744 case False{}:
745 False{}
746 case True{}:
747 rest(Unit{})
748
749# the tail of a Content-Length list against the first value
750def clen.agree.go(rest: List<&2, String>, +h: String) -> Bool:
751 match rest:
752 case []:
753 True{}
754 case x <> r:
755 clen.agree.step(String.eq(x, h), _u => clen.agree.go(r, h))
756
757# duplicate Content-Length fields must be the same digits (RFC 9112 §6.3)
758def clen.agree(vs: List<&2, String>) -> Bool:
759 match vs:
760 case []:
761 True{}
762 case h <> t:
763 clen.agree.go(t, h)
764
765# whether any Content-Length field was present
766def clen.any(vs: List<&2, String>) -> Bool:
767 match vs:
768 case []:
769 False{}
770 case h <> t:
771 True{}
772
773# a chunked body, or why the chunk framing was rejected
774def parse.chunked(status: U32, headers: List<&2, Header>, body: String,
775 bad: Maybe<&2, String>) -> Reply:
776 match bad:
777 case None{}:
778 Reply{status, headers, dechunk(body)}
779 case Some{why}:
780 Torn{why}
781
782# scan chunk sizes, then decode when they are hex and closed by 0
783def parse.chunks(status: U32, headers: List<&2, Header>, +body: String) -> Reply:
784 parse.chunked(status, headers, body,
785 chunks.scan(String.length(body), divide(body, "\r\n")))
786
787# Transfer-Encoding together with Content-Length is a bad message
788def parse.te.clash(status: U32, headers: List<&2, Header>, body: String,
789 present: Bool) -> Reply:
790 match present:
791 case True{}:
792 Torn{"Content-Length and Transfer-Encoding conflict"}
793 case False{}:
794 parse.chunks(status, headers, body)
795
796# chunked framing, or Content-Length, or the rest of the connection
797def parse.te(status: U32, headers: List<&2, Header>, +lens: List<&2, String>,
798 +body: String, chunked: Bool) -> Reply:
799 match chunked:
800 case False{}:
801 parse.len(status, headers, digits.read(first(lens)), body)
802 case True{}:
803 parse.te.clash(status, headers, body, clen.any(lens))
804
805# disagreeing Content-Length values are torn before framing
806def parse.agree(status: U32, headers: List<&2, Header>, te: String,
807 +lens: List<&2, String>, body: String, ok: Bool) -> Reply:
808 match ok:
809 case False{}:
810 Torn{"Content-Length values disagree"}
811 case True{}:
812 parse.te(status, headers, lens, body,
813 String.contains(String.to_lower(te), "chunked"))
814
815# the headers that decide the framing (RFC 9112 §6.3)
816def parse.frame(status: U32, headers: List<&2, Header>, te: String,
817 +lens: List<&2, String>, body: String) -> Reply:
818 parse.agree(status, headers, te, lens, body, clen.agree(lens))
819
820# a head whose status line has been read (RFC 9112 §4)
821def parse.status(m: Maybe<&2, U32>, +ls: List<&2, String>, body: String)
822 -> Reply:
823 match m:
824 case None{}:
825 Torn{"the response has no status line"}
826 case Some{n}:
827 +hs = head.list(ls)
828 parse.frame(n, hs, head.go(ls, "transfer-encoding"),
829 head.values(ls, "content-length"), body)
830
831# the status code a head's first line names, if it names one (RFC 9112 §4)
832def status.of(ls: List<&2, String>) -> Maybe<&2, U32>:
833 U32.read(second(String.split(first(ls), ' ')))
834
835# the head's lines, with the status line read off the first
836def parse.head(+ls: List<&2, String>, body: String) -> Reply:
837 parse.status(status.of(ls), ls, body)
838
839# a response divided into its head and everything after the blank line
840# (RFC 9112 §2.1: header section ends at empty line)
841def parse.cut(c: Cut) -> Reply:
842 match c:
843 case NoCut{}:
844 Torn{"the response head has no blank line after it"}
845 case Cut{before, after}:
846 parse.head(String.lines(before), after)
847
848# the status, headers, and body of a raw response
849def parse(raw: String) -> Reply:
850 parse.cut(divide(raw, "\r\n\r\n"))
851
852# a parsed response on one line, for a test to read
853def show(r: Reply) -> String:
854 match r:
855 case Torn{why}:
856 "torn " ++ why
857 case Reply{status, headers, body}:
858 U32.show(status) ++ " " ++ body
859
860# --- inbound request (server) and outbound response (server) ---
861
862# a request that came apart, or the reason it would not (RFC 9112 §3)
863type Request is Data:
864 Bad{why: String}
865 Request{method: String, target: String, headers: List<&2, Header>,
866 body: String}
867
868# a status code and its reason-phrase
869type Phrase is Data:
870 P{code: U32, text: String}
871
872# the reason-phrases RFC 9110 §15 names (RFC 6585 §4 for 429)
873def reasons() -> List<&2, Phrase>:
874 [P{200, "OK"}, P{201, "Created"}, P{202, "Accepted"}, P{204, "No Content"},
875 P{301, "Moved Permanently"}, P{302, "Found"}, P{303, "See Other"},
876 P{304, "Not Modified"}, P{307, "Temporary Redirect"},
877 P{308, "Permanent Redirect"}, P{400, "Bad Request"},
878 P{401, "Unauthorized"}, P{403, "Forbidden"}, P{404, "Not Found"},
879 P{405, "Method Not Allowed"}, P{409, "Conflict"}, P{410, "Gone"},
880 P{413, "Content Too Large"}, P{415, "Unsupported Media Type"},
881 P{422, "Unprocessable Content"}, P{429, "Too Many Requests"},
882 P{500, "Internal Server Error"}, P{501, "Not Implemented"},
883 P{502, "Bad Gateway"}, P{503, "Service Unavailable"},
884 P{504, "Gateway Timeout"}]
885
886# this phrase when its code is the one asked for, else the rest's
887def reason.pick(text: String, hit: Bool, rest: Unit -> String) -> String:
888 match hit:
889 case True{}:
890 text
891 case False{}:
892 rest(Unit{})
893
894# the phrase a list gives a code, "" when it gives none
895def reason.in(ps: List<&2, Phrase>, +code: U32) -> String:
896 match ps:
897 case []:
898 ""
899 case P{c, text} <> t:
900 reason.pick(text, U32.is_eq(code, c), _u => reason.in(t, code))
901
902# the reason-phrase for a status code (RFC 9112 §4); "" for one not listed
903def reason(+code: U32) -> String:
904 reason.in(reasons(), code)
905
906# the head of a reply whose body is n octets, onto what follows it
907# (SPEC.md HTTP-SRV-6)
908def respond.head.onto(+status: U32, headers: List<&2, Header>, +n: Nat,
909 rest: String) -> String:
910 "HTTP/1.1 " ++ U32.show(status) ++ " " ++ reason(status) ++ "\r\n"
911 ++ "Connection: close\r\n"
912 ++ headers.lines(headers)
913 ++ clen.line(n, Nat.is_eq(n, 0n))
914 ++ "\r\n"
915 ++ rest
916
917# the head of a reply whose body is n octets
918def respond.head(+status: U32, headers: List<&2, Header>, +n: Nat) -> String:
919 respond.head.onto(status, headers, n, "")
920
921# status-line + headers + body (RFC 9112 §4, §5). Connection: close ends the
922# exchange after one response.
923def respond(+status: U32, headers: List<&2, Header>, +body: String) -> String:
924 respond.head.onto(status, headers, utf8.len(body), body)
925
926# 204 and 304 are terminated by the header section (RFC 9110 §15.3.5, §15.4.5)
927def status.nocontent(+code: U32) -> Bool:
928 Bool.or(U32.is_eq(code, 204), U32.is_eq(code, 304))
929
930# the Transfer-Encoding line of a streamed reply, when it has a body
931def te.line(te: Bool) -> String:
932 match te:
933 case True{}:
934 "Transfer-Encoding: chunked\r\n"
935 case False{}:
936 ""
937
938# the head of a streamed reply: chunked unless the status has no body
939# (RFC 9112 §6.1, §7.1; SPEC.md HTTP-SRV-7)
940def respond.stream(+status: U32, headers: List<&2, Header>) -> String:
941 "HTTP/1.1 " ++ U32.show(status) ++ " " ++ reason(status) ++ "\r\n"
942 ++ "Connection: close\r\n"
943 ++ headers.lines(headers)
944 ++ te.line(Bool.not(status.nocontent(status)))
945 ++ "\r\n"
946
947# one lowercase hex digit of a value below 16
948def hex.nib(+v: U32) -> Char:
949 Char.from_u32(Bool.pick(U32, U32.is_lt(v, 10), U32.add(v, 48),
950 U32.add(v, 87)))
951
952# the 4 bits of n at this shift as a hex digit
953def hex.at(+n: U32, k: Nat) -> Char:
954 hex.nib(U32.and(U32.shrn(n, k), 15))
955
956# a chunk's size as 8 lowercase hex digits, then CRLF (RFC 9112 §7.1)
957def chunk.line(+n: U32) -> String:
958 SCon{hex.at(n, 28n), SCon{hex.at(n, 24n), SCon{hex.at(n, 20n),
959 SCon{hex.at(n, 16n), SCon{hex.at(n, 12n), SCon{hex.at(n, 8n),
960 SCon{hex.at(n, 4n), SCon{hex.at(n, 0n), "\r\n"}}}}}}}}
961
962# how a chunk of octets is framed: not at all when it is empty, which would
963# end the body, else its size line before it and CRLF after
964type Chunk is Data:
965 NoChunk{}
966 Chunk{line: String}
967
968# the frame of a chunk once it is known whether it is empty
969def chunk.frame.of(+n: U32, empty: Bool) -> Chunk:
970 match empty:
971 case True{}:
972 NoChunk{}
973 case False{}:
974 Chunk{chunk.line(n)}
975
976# the frame of a chunk of n octets (SPEC.md HTTP-SRV-7)
977def chunk.frame(+n: U32) -> Chunk:
978 chunk.frame.of(n, U32.is_eq(n, 0))
979
980# the last chunk and the end of a chunked body
981def chunk.end() -> String:
982 "0\r\n\r\n"
983
984# drop a 204/304 body; any other status keeps it
985def respond.of.body(+status: U32, headers: List<&2, Header>, body: String,
986 drop: Bool) -> String:
987 match drop:
988 case True{}:
989 respond(status, headers, "")
990 case False{}:
991 respond(status, headers, body)
992
993# format a structured Reply as a response message
994def respond.of(r: Reply) -> String:
995 match r:
996 case Torn{why}:
997 respond(500, [], why)
998 case Reply{+status, headers, body}:
999 respond.of.body(status, headers, body, status.nocontent(status))
1000
1001# HEAD carries no message body; any other method keeps the body (RFC 9110 §9.3.2)
1002def reply.for.pick(reply: Reply, head: Bool) -> Reply:
1003 match reply head:
1004 case Torn{why} _:
1005 Torn{why}
1006 case Reply{status, headers, body} False{}:
1007 Reply{status, headers, body}
1008 case Reply{status, headers, body} True{}:
1009 Reply{status, headers, ""}
1010
1011# drop a HEAD response body before it is written
1012def reply.for(method: String, reply: Reply) -> Reply:
1013 reply.for.pick(reply, String.eq(method, "HEAD"))
1014
1015# the method token, or "" when the request did not parse
1016def method.of(req: Request) -> String:
1017 match req:
1018 case Bad{why}:
1019 ""
1020 case Request{method, target, headers, body}:
1021 method
1022
1023# request body against Content-Length
1024def ask.short(method: String, target: String, headers: List<&2, Header>,
1025 n: Nat, body: String, short: Bool) -> Request:
1026 match short:
1027 case True{}:
1028 Bad{"the request body stopped before its Content-Length"}
1029 case False{}:
1030 Request{method, target, headers, octs.take(body, n)}
1031
1032# a request body framed by Content-Length (RFC 9110 §8.6 / RFC 9112 §6.3)
1033def ask.clen(method: String, target: String, headers: List<&2, Header>,
1034 +n: Nat, +body: String) -> Request:
1035 ask.short(method, target, headers, n, body, Nat.is_lt(octs.len(body), n))
1036
1037# Content-Length when present; else the rest of the connection is the body
1038def ask.len(method: String, target: String, headers: List<&2, Header>,
1039 m: Maybe<&2, Nat>, body: String) -> Request:
1040 match m:
1041 case None{}:
1042 Request{method, target, headers, body}
1043 case Some{n}:
1044 ask.clen(method, target, headers, n, body)
1045
1046# a chunked request body, or why the chunk framing was rejected
1047def ask.chunked(method: String, target: String, headers: List<&2, Header>,
1048 body: String, bad: Maybe<&2, String>) -> Request:
1049 match bad:
1050 case None{}:
1051 Request{method, target, headers, dechunk(body)}
1052 case Some{why}:
1053 Bad{why}
1054
1055# scan chunk sizes, then decode when they are hex and closed by 0
1056def ask.chunks(method: String, target: String, headers: List<&2, Header>,
1057 +body: String) -> Request:
1058 ask.chunked(method, target, headers, body,
1059 chunks.scan(String.length(body), divide(body, "\r\n")))
1060
1061# Transfer-Encoding together with Content-Length is a bad request
1062def ask.te.clash(method: String, target: String, headers: List<&2, Header>,
1063 body: String, present: Bool) -> Request:
1064 match present:
1065 case True{}:
1066 Bad{"Content-Length and Transfer-Encoding conflict"}
1067 case False{}:
1068 ask.chunks(method, target, headers, body)
1069
1070# chunked framing, or Content-Length, or the rest of the connection
1071def ask.te(method: String, target: String, headers: List<&2, Header>,
1072 +lens: List<&2, String>, +body: String, chunked: Bool) -> Request:
1073 match chunked:
1074 case False{}:
1075 ask.len(method, target, headers, digits.read(first(lens)), body)
1076 case True{}:
1077 ask.te.clash(method, target, headers, body, clen.any(lens))
1078
1079# disagreeing Content-Length values are bad before framing
1080def ask.agree(method: String, target: String, headers: List<&2, Header>,
1081 te: String, +lens: List<&2, String>, body: String, ok: Bool) -> Request:
1082 match ok:
1083 case False{}:
1084 Bad{"Content-Length values disagree"}
1085 case True{}:
1086 ask.te(method, target, headers, lens, body,
1087 String.contains(String.to_lower(te), "chunked"))
1088
1089# the headers that decide request framing (RFC 9112 §6.3)
1090def ask.frame(method: String, target: String, headers: List<&2, Header>,
1091 te: String, +lens: List<&2, String>, body: String) -> Request:
1092 ask.agree(method, target, headers, te, lens, body, clen.agree(lens))
1093
1094# origin-form, or a bad request when the target is not an absolute-path
1095def ask.origin(method: String, target: String, +ls: List<&2, String>,
1096 body: String, ok: Bool) -> Request:
1097 match ok:
1098 case False{}:
1099 Bad{"the request-target is not in origin-form"}
1100 case True{}:
1101 +hs = head.list(ls)
1102 ask.frame(method, target, hs, head.go(ls, "transfer-encoding"),
1103 head.values(ls, "content-length"), body)
1104
1105# request-line: method SP request-target SP HTTP-version (RFC 9112 §3)
1106def ask.line(+method: String, +target: String, +ls: List<&2, String>,
1107 body: String) -> Request:
1108 ask.origin(method, target, ls, body,
1109 target.form(method, target, target.origin(target)))
1110
1111# three fields of the request-line, or torn
1112def ask.parts(ps: List<&2, String>, +ls: List<&2, String>, body: String)
1113 -> Request:
1114 match ps:
1115 case []:
1116 Bad{"the request has no request line"}
1117 case m <> rest:
1118 match rest:
1119 case []:
1120 Bad{"the request line has no target"}
1121 case t <> _ver:
1122 ask.line(m, t, ls, body)
1123
1124# the head's lines, with the request-line read off the first
1125def ask.head(+ls: List<&2, String>, body: String) -> Request:
1126 match ls:
1127 case []:
1128 Bad{"the request has no request line"}
1129 case _:
1130 ask.parts(String.split(first(ls), ' '), ls, body)
1131
1132# a request divided into its head and everything after the blank line
1133def ask.cut(c: Cut) -> Request:
1134 match c:
1135 case NoCut{}:
1136 Bad{"the request head has no blank line after it"}
1137 case Cut{before, after}:
1138 ask.head(String.lines(before), after)
1139
1140# the method, target, headers, and body of a raw request
1141def ask(raw: String) -> Request:
1142 ask.cut(divide(raw, "\r\n\r\n"))
1143
1144# a parsed request on one line, for a test to read
1145def ask.show(r: Request) -> String:
1146 match r:
1147 case Bad{why}:
1148 "bad " ++ why
1149 case Request{method, target, headers, body}:
1150 method ++ " " ++ target ++ " " ++ body
1151
1152# --- when a response has all arrived (RFC 9112 §6.3) ---
1153
1154# how a response's body is framed
1155type Frame is Data:
1156 Bare{}
1157 Sized{n: Nat}
1158 Chunked{}
1159 Closed{}
1160
1161# 204 and 304 carry no body; a status line that did not parse is framed by
1162# its headers
1163def status.bare(m: Maybe<&2, U32>) -> Bool:
1164 match m:
1165 case None{}:
1166 False{}
1167 case Some{n}:
1168 status.nocontent(n)
1169
1170# a 1xx status is an interim response (RFC 9110 §15.2); a status line that
1171# did not parse is not
1172def status.interim(m: Maybe<&2, U32>) -> Bool:
1173 match m:
1174 case None{}:
1175 False{}
1176 case Some{+n}:
1177 Bool.and(U32.is_le(100, n), U32.is_lt(n, 200))
1178
1179# a Content-Length that reads as a number, or the close when none does
1180def frame.sized(m: Maybe<&2, Nat>) -> Frame:
1181 match m:
1182 case None{}:
1183 Closed{}
1184 case Some{n}:
1185 Sized{n}
1186
1187# Content-Length values that agree frame the body; any others leave the close
1188def frame.agree(+lens: List<&2, String>, ok: Bool) -> Frame:
1189 match ok:
1190 case False{}:
1191 Closed{}
1192 case True{}:
1193 frame.sized(digits.read(first(lens)))
1194
1195# chunked framing wins over Content-Length (RFC 9112 §6.3 item 4)
1196def frame.te(+lens: List<&2, String>, chunked: Bool) -> Frame:
1197 match chunked:
1198 case True{}:
1199 Chunked{}
1200 case False{}:
1201 frame.agree(lens, clen.agree(lens))
1202
1203# the framing of a response: none when bare (a reply to HEAD, a 204 or a 304),
1204# else Transfer-Encoding chunked, else Content-Length, else the close
1205def frame(bare: Bool, te: String, +lens: List<&2, String>) -> Frame:
1206 match bare:
1207 case True{}:
1208 Bare{}
1209 case False{}:
1210 frame.te(lens, String.contains(String.to_lower(te), "chunked"))
1211
1212# a zero chunk's trailer section has ended: at once, or after its fields
1213def chunks.trailer(+after: String) -> Bool:
1214 Bool.or(String.starts_with(after, "\r\n"), String.contains(after, "\r\n\r\n"))
1215
1216# a chunk that has all arrived: on to the next chunk header, else not yet
1217def chunks.ended.data(+after: String, +n: Nat, ready: Bool,
1218 rest: Cut -> Bool) -> Bool:
1219 match ready:
1220 case False{}:
1221 False{}
1222 case True{}:
1223 rest(divide(octs.drop(after, Nat.add(n, 2n)), "\r\n"))
1224
1225# a chunk of size n: the last one when n is 0
1226def chunks.ended.size(+after: String, +n: Nat, zero: Bool,
1227 rest: Cut -> Bool) -> Bool:
1228 match zero:
1229 case True{}:
1230 chunks.trailer(after)
1231 case False{}:
1232 chunks.ended.data(after, n, chunks.ready(after, n), rest)
1233
1234# a chunk header: a size that is not hex ends the read (the parse rejects it)
1235def chunks.ended.hex(+before: String, +after: String, ok: Bool,
1236 rest: Cut -> Bool) -> Bool:
1237 match ok:
1238 case False{}:
1239 True{}
1240 case True{}:
1241 +n = hexlen(before)
1242 chunks.ended.size(after, n, Nat.is_eq(n, 0n), rest)
1243
1244# a chunk header that has arrived, or not yet
1245def chunks.ended.at(c: Cut, rest: Cut -> Bool) -> Bool:
1246 match c:
1247 case NoCut{}:
1248 False{}
1249 case Cut{+before, +after}:
1250 chunks.ended.hex(before, after, hex.well(chunks.token(before)), rest)
1251
1252# whether a chunked body has reached the end of its last chunk
1253def chunks.ended(fuel: Nat, c: Cut) -> Bool:
1254 match fuel:
1255 case 0n:
1256 False{}
1257 case 1n+f:
1258 chunks.ended.at(c, cut => chunks.ended(f, cut))
1259
1260# whether a body has all arrived under its framing
1261def whole.of(f: Frame, +body: String) -> Bool:
1262 match f:
1263 case Bare{}:
1264 True{}
1265 case Sized{n}:
1266 Bool.not(Nat.is_lt(octs.len(body), n))
1267 case Chunked{}:
1268 chunks.ended(String.length(body), divide(body, "\r\n"))
1269 case Closed{}:
1270 False{}
1271
1272# a head that is interim: whole when what follows is; else whole under the
1273# framing it gives
1274def whole.step(asked: Bool, +ls: List<&2, String>, +after: String,
1275 interim: Bool, rest: Cut -> Bool) -> Bool:
1276 match interim:
1277 case True{}:
1278 rest(divide(after, "\r\n\r\n"))
1279 case False{}:
1280 whole.of(frame(Bool.or(asked, status.bare(status.of(ls))),
1281 head.go(ls, "transfer-encoding"), head.values(ls, "content-length")),
1282 after)
1283
1284# a response whose head has ended, or not yet
1285def whole.at(asked: Bool, c: Cut, rest: Cut -> Bool) -> Bool:
1286 match c:
1287 case NoCut{}:
1288 False{}
1289 case Cut{before, after}:
1290 +ls = String.lines(before)
1291 whole.step(asked, ls, after, status.interim(status.of(ls)), rest)
1292
1293# the heads in turn, at most `fuel` of them
1294def whole.go(fuel: Nat, +asked: Bool, c: Cut) -> Bool:
1295 match fuel:
1296 case 0n:
1297 False{}
1298 case 1n+f:
1299 whole.at(asked, c, cut => whole.go(f, asked, cut))
1300
1301# whether the text received so far is a whole response to a request with
1302# this method (RFC 9112 §6.3), interim 1xx heads read past (RFC 9110 §15.2);
1303# a response framed by the close never is
1304def whole(+method: String, +raw: String) -> Bool:
1305 whole.go(String.length(raw), String.eq(method, "HEAD"),
1306 divide(raw, "\r\n\r\n"))
1307
1308# --- a response read by the request's method (RFC 9110 §15.2, §6.4.1) ---
1309
1310# a 1xx, 204 or 304 response has no body (RFC 9110 §6.4.1)
1311def status.empty(+m: Maybe<&2, U32>) -> Bool:
1312 Bool.or(status.interim(m), status.bare(m))
1313
1314# an interim head is skipped when more text follows it
1315def interim.skip(m: Maybe<&2, U32>, after: String) -> Bool:
1316 Bool.and(status.interim(m), Bool.not(String.is_empty(after)))
1317
1318# the final head with no body: its status and fields, an empty body
1319def parse.to.bare(m: Maybe<&2, U32>, ls: List<&2, String>) -> Reply:
1320 match m:
1321 case None{}:
1322 Torn{"the response has no status line"}
1323 case Some{n}:
1324 Reply{n, head.list(ls), ""}
1325
1326# the final head: with no body, or framed as parse frames it
1327def parse.to.final(m: Maybe<&2, U32>, +ls: List<&2, String>, after: String,
1328 bare: Bool) -> Reply:
1329 match bare:
1330 case True{}:
1331 parse.to.bare(m, ls)
1332 case False{}:
1333 parse.status(m, ls, after)
1334
1335# an interim head is skipped, any other is the final one
1336def parse.to.step(head: Bool, +ls: List<&2, String>, +m: Maybe<&2, U32>,
1337 +after: String, skip: Bool, rest: Cut -> Reply) -> Reply:
1338 match skip:
1339 case True{}:
1340 rest(divide(after, "\r\n\r\n"))
1341 case False{}:
1342 parse.to.final(m, ls, after, Bool.or(head, status.empty(m)))
1343
1344# a head that has ended, or the reason it has not
1345def parse.to.at(head: Bool, c: Cut, rest: Cut -> Reply) -> Reply:
1346 match c:
1347 case NoCut{}:
1348 Torn{"the response head has no blank line after it"}
1349 case Cut{before, +after}:
1350 +ls = String.lines(before)
1351 +m = status.of(ls)
1352 parse.to.step(head, ls, m, after, interim.skip(m, after), rest)
1353
1354# the heads in turn, at most `fuel` of them
1355def parse.to.go(fuel: Nat, +head: Bool, c: Cut) -> Reply:
1356 match fuel:
1357 case 0n:
1358 Torn{"the response head has no blank line after it"}
1359 case 1n+f:
1360 parse.to.at(head, c, cut => parse.to.go(f, head, cut))
1361
1362# the response to a request with this method (RFC 9112 §6.3): interim 1xx
1363# heads skipped, and no body for HEAD or a 1xx, 204 or 304 final status
1364def parse.to(+method: String, +raw: String) -> Reply:
1365 parse.to.go(String.length(raw), String.eq(method, "HEAD"),
1366 divide(raw, "\r\n\r\n"))
1367
1368# --- when a response has all arrived, judged read by read (SPEC.md HTTP-CLI-12) ---
1369#
1370# The client judges the text it has received after every read. Judging the
1371# whole text each time (whole) costs the whole text each time; the state
1372# below carries the judgement from one read to the next, so a read costs what
1373# it brought (and the head, while no final head has ended). hear.more(
1374# hear.of(method, a), b) is hear.of(method, a ++ b), and hear.done of it is
1375# whole(method, a ++ b).
1376
1377# bytes of UTF-8 walked off the front of a string: all of it, with this many
1378# still owed, or a stop at the first character that does not fit in what was
1379# left, with what was left and the text from that character on
1380type Skip is Data:
1381 Short{owed: Nat}
1382 Over{left: Nat, rest: String}
1383
1384# one step of the skip: a character wider than what is left stops it
1385def octs.skip.step(short: Bool, +n: Nat, h: Char, t: String,
1386 rest: Unit -> Skip) -> Skip:
1387 match short:
1388 case True{}:
1389 Over{n, SCon{h, t}}
1390 case False{}:
1391 rest(Unit{})
1392
1393# walk n bytes of UTF-8 off a string, as octs.drop does, saying how it ended
1394def octs.skip(s: String, +n: Nat) -> Skip:
1395 match s:
1396 case SNil{}:
1397 Short{n}
1398 case SCon{+h, +t}:
1399 +w = octs.width(Char.to_u32(h))
1400 octs.skip.step(Nat.is_lt(n, w), n, h, t, _u => octs.skip(t, Nat.sub(n, w)))
1401
1402# where a chunked body's walk stands: ended; waiting at a chunk header (or the
1403# last chunk's trailer) that has not all arrived; inside a chunk's data with
1404# octets still owed; or at the end of a chunk's data, at what should be its
1405# CRLF. `fuel` is what chunks.ended would have left there.
1406type Walk is Data:
1407 Ended{}
1408 Hold{fuel: Nat, rest: String}
1409 Owed{fuel: Nat, owed: Nat}
1410 Tail{fuel: Nat, left: Nat, rest: String}
1411
1412# a chunk's data skipped: whether its CRLF has arrived, and on to the next
1413# chunk header when it has
1414def walk.crlf(g: Nat, +left: Nat, +rest: String, ready: Bool,
1415 go: String -> Walk) -> Walk:
1416 match ready:
1417 case True{}:
1418 go(octs.drop(rest, Nat.add(left, 2n)))
1419 case False{}:
1420 Tail{g, left, rest}
1421
1422# a chunk's data: all of what arrived, with octets still owed, or its end
1423def walk.data(+g: Nat, s: Skip, go: String -> Walk) -> Walk:
1424 match s:
1425 case Short{owed}:
1426 Owed{g, owed}
1427 case Over{+left, +rest}:
1428 walk.crlf(g, left, rest, Bool.and(octs.has(rest, Nat.add(left, 2n)),
1429 String.starts_with(rest, "\r\n")), go)
1430
1431# the last chunk: ended once its trailer section has
1432def walk.trail(g: Nat, rest: String, ended: Bool) -> Walk:
1433 match ended:
1434 case True{}:
1435 Ended{}
1436 case False{}:
1437 Hold{1n+g, rest}
1438
1439# a chunk of size n: the last one when n is 0
1440def walk.size(+g: Nat, rest: String, +after: String, +n: Nat, zero: Bool,
1441 go: String -> Walk) -> Walk:
1442 match zero:
1443 case True{}:
1444 walk.trail(g, rest, chunks.trailer(after))
1445 case False{}:
1446 walk.data(g, octs.skip(after, n), go)
1447
1448# a chunk header: a size that is not hex ends the walk (the parse rejects it)
1449def walk.hex(+g: Nat, rest: String, +before: String, +after: String, ok: Bool,
1450 go: String -> Walk) -> Walk:
1451 match ok:
1452 case False{}:
1453 Ended{}
1454 case True{}:
1455 +n = hexlen(before)
1456 walk.size(g, rest, after, n, Nat.is_eq(n, 0n), go)
1457
1458# a chunk header that has arrived, or not yet
1459def walk.at(+g: Nat, rest: String, c: Cut, go: String -> Walk) -> Walk:
1460 match c:
1461 case NoCut{}:
1462 Hold{1n+g, rest}
1463 case Cut{+before, +after}:
1464 walk.hex(g, rest, before, after, hex.well(chunks.token(before)), go)
1465
1466# the walk of chunks.ended from the chunk header at the front of a text
1467def walk(fuel: Nat, +rest: String) -> Walk:
1468 match fuel:
1469 case 0n:
1470 Hold{0n, rest}
1471 case 1n+f:
1472 +g = f
1473 walk.at(g, rest, divide(rest, "\r\n"), s => walk(g, s))
1474
1475# whether the walk has ended
1476def walk.done(w: Walk) -> Bool:
1477 match w:
1478 case Ended{}:
1479 True{}
1480 case Hold{fuel, rest}:
1481 False{}
1482 case Owed{fuel, owed}:
1483 False{}
1484 case Tail{fuel, left, rest}:
1485 False{}
1486
1487# the walk once m more characters, b, have arrived
1488def walk.more(w: Walk, +m: Nat, b: String) -> Walk:
1489 match w:
1490 case Ended{}:
1491 Ended{}
1492 case Hold{fuel, rest}:
1493 walk(Nat.add(fuel, m), rest ++ b)
1494 case Owed{g, owed}:
1495 +f = Nat.add(g, m)
1496 walk.data(f, octs.skip(b, owed), s => walk(f, s))
1497 case Tail{g, left, rest}:
1498 +f = Nat.add(g, m)
1499 walk.data(f, Over{left, rest ++ b}, s => walk(f, s))
1500
1501# where a response stands: no final head yet (with the text from the head
1502# being read on, and the fuel whole.go would have there); no body, so whole;
1503# framed by the close, so never whole; sized, with the octets that have
1504# arrived; or chunked, with its walk
1505type Hear is Data:
1506 Heads{fuel: Nat, asked: Bool, raw: String}
1507 Whole{}
1508 Never{}
1509 Count{n: Nat, have: Nat}
1510 Walking{w: Walk}
1511
1512# a final head's body under its framing
1513def hear.body(f: Frame, +after: String) -> Hear:
1514 match f:
1515 case Bare{}:
1516 Whole{}
1517 case Sized{n}:
1518 Count{n, octs.len(after)}
1519 case Chunked{}:
1520 Walking{walk(String.length(after), after)}
1521 case Closed{}:
1522 Never{}
1523
1524# an interim head: on to the next; a final one: its body
1525def hear.step(asked: Bool, +ls: List<&2, String>, +after: String,
1526 interim: Bool, go: String -> Hear) -> Hear:
1527 match interim:
1528 case True{}:
1529 go(after)
1530 case False{}:
1531 hear.body(frame(Bool.or(asked, status.bare(status.of(ls))),
1532 head.go(ls, "transfer-encoding"), head.values(ls, "content-length")),
1533 after)
1534
1535# a head that has ended, or not yet
1536def hear.at(+g: Nat, +asked: Bool, raw: String, c: Cut, go: String -> Hear)
1537 -> Hear:
1538 match c:
1539 case NoCut{}:
1540 Heads{1n+g, asked, raw}
1541 case Cut{before, after}:
1542 +ls = String.lines(before)
1543 hear.step(asked, ls, after, status.interim(status.of(ls)), go)
1544
1545# the heads in turn, as whole.go reads them
1546def hear.go(fuel: Nat, +asked: Bool, +raw: String) -> Hear:
1547 match fuel:
1548 case 0n:
1549 Heads{0n, asked, raw}
1550 case 1n+f:
1551 +g = f
1552 hear.at(g, asked, raw, divide(raw, "\r\n\r\n"), s => hear.go(g, asked, s))
1553
1554# where a response to a request with this method stands, read from the
1555# whole text received so far
1556def hear.of(+method: String, +raw: String) -> Hear:
1557 hear.go(String.length(raw), String.eq(method, "HEAD"), raw)
1558
1559# whether the response has all arrived
1560def hear.done(h: Hear) -> Bool:
1561 match h:
1562 case Heads{fuel, asked, raw}:
1563 False{}
1564 case Whole{}:
1565 True{}
1566 case Never{}:
1567 False{}
1568 case Count{n, have}:
1569 Bool.not(Nat.is_lt(have, n))
1570 case Walking{w}:
1571 walk.done(w)
1572
1573# where a response stands once more text, b, has arrived
1574def hear.more(h: Hear, +b: String) -> Hear:
1575 match h:
1576 case Heads{fuel, asked, raw}:
1577 hear.go(Nat.add(fuel, String.length(b)), asked, raw ++ b)
1578 case Whole{}:
1579 Whole{}
1580 case Never{}:
1581 Never{}
1582 case Count{n, have}:
1583 Count{n, Nat.add(have, octs.len(b))}
1584 case Walking{w}:
1585 Walking{walk.more(w, String.length(b), b)}
1586
1587# --- a response's reason phrase (RFC 9112 §4) ---
1588
1589# a reason phrase with the CR its line ended with removed; a reason-phrase
1590# itself holds no CR (RFC 9112 §4)
1591def phrase.chop.at(
1592 cr: Bool,
1593 ch: Char,
1594 tl: String,
1595 rest: Unit -> String
1596) -> String:
1597 match cr tl:
1598 case True{} SNil{}:
1599 SNil{}
1600 case True{} SCon{x, xt}:
1601 SCon{ch, rest(Unit{})}
1602 case False{} _:
1603 SCon{ch, rest(Unit{})}
1604
1605# the text of a reason phrase, a final CR removed
1606def phrase.chop(text: String) -> String:
1607 match text:
1608 case SNil{}:
1609 SNil{}
1610 case SCon{+ch, +tl}:
1611 phrase.chop.at(Char.is_eq(ch, '\r'), ch, tl, _u => phrase.chop(tl))
1612
1613# what follows the status code's SP: the reason phrase; none without that SP
1614def phrase.code(cut: Cut) -> String:
1615 match cut:
1616 case NoCut{}:
1617 ""
1618 case Cut{before, after}:
1619 phrase.chop(after)
1620
1621# what follows the version's SP: the status code, an SP and the reason
1622def phrase.after(cut: Cut) -> String:
1623 match cut:
1624 case NoCut{}:
1625 ""
1626 case Cut{before, after}:
1627 phrase.code(divide(after, " "))
1628
1629# a status line's reason phrase (RFC 9112 §4: HTTP-version SP status-code SP
1630# [ reason-phrase ]), empty when the line has fewer than two SPs
1631def phrase.line(line: String) -> String:
1632 phrase.after(divide(line, " "))
1633
1634# an interim head is skipped, any other gives the reason on its first line
1635def phrase.to.step(
1636 +ls: List<&2, String>,
1637 +after: String,
1638 skip: Bool,
1639 rest: Cut -> String
1640) -> String:
1641 match skip:
1642 case True{}:
1643 rest(divide(after, "\r\n\r\n"))
1644 case False{}:
1645 phrase.line(first(ls))
1646
1647# a head that has ended, or none
1648def phrase.to.at(cut: Cut, rest: Cut -> String) -> String:
1649 match cut:
1650 case NoCut{}:
1651 ""
1652 case Cut{before, +after}:
1653 +ls = String.lines(before)
1654 phrase.to.step(ls, after, interim.skip(status.of(ls), after), rest)
1655
1656# the heads in turn, at most `fuel` of them
1657def phrase.to.go(fuel: Nat, cut: Cut) -> String:
1658 match fuel:
1659 case 0n:
1660 ""
1661 case 1n+f:
1662 phrase.to.at(cut, next => phrase.to.go(f, next))
1663
1664# the reason phrase of the head parse.to stops at: interim 1xx heads with
1665# text after them skipped, empty when no head ends
1666def phrase.to(+raw: String) -> String:
1667 phrase.to.go(String.length(raw), divide(raw, "\r\n\r\n"))