src/http.bend
emerging-ezhttp@0.14.0.0 · 1,268 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.14.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# bytes one code point takes in UTF-8. Content-Length counts octets
127# (RFC 9110 §8.6); a Bend String counts code points.
128def utf8.width(+u: U32) -> Nat:
129 Bool.pick(Nat, U32.is_lt(u, 128), 1n,
130 Bool.pick(Nat, U32.is_lt(u, 2048), 2n,
131 Bool.pick(Nat, U32.is_lt(u, 65536), 3n, 4n)))
132
133# how many bytes of UTF-8 a string is
134def utf8.len(s: String) -> Nat:
135 match s:
136 case SNil{}:
137 0n
138 case SCon{h, t}:
139 Nat.add(utf8.width(Char.to_u32(h)), utf8.len(t))
140
141# one step of the take
142def utf8.take.step(short: Bool, h: Char, rest: Unit -> String) -> String:
143 match short:
144 case True{}:
145 SNil{}
146 case False{}:
147 SCon{h, rest(Unit{})}
148
149# the front of a string that is this many bytes of UTF-8
150def utf8.take(s: String, +n: Nat) -> String:
151 match s:
152 case SNil{}:
153 SNil{}
154 case SCon{+h, t}:
155 +w = utf8.width(Char.to_u32(h))
156 utf8.take.step(Nat.is_lt(n, w), h, _u => utf8.take(t, Nat.sub(n, w)))
157
158# one step of the drop
159def utf8.drop.step(short: Bool, h: Char, t: String,
160 rest: Unit -> String) -> String:
161 match short:
162 case True{}:
163 SCon{h, t}
164 case False{}:
165 rest(Unit{})
166
167# the rest of a string after this many bytes of UTF-8
168def utf8.drop(s: String, +n: Nat) -> String:
169 match s:
170 case SNil{}:
171 SNil{}
172 case SCon{+h, +t}:
173 +w = utf8.width(Char.to_u32(h))
174 utf8.drop.step(Nat.is_lt(n, w), h, t, _u => utf8.drop(t, Nat.sub(n, w)))
175
176# a decimal digit's value, or 10 when the character is not a digit
177def digits.val.of(+u: U32) -> U32:
178 Bool.pick(U32, Bool.and(U32.is_ge(u, 48), U32.is_le(u, 57)), U32.sub(u, 48), 10)
179
180# a decimal digit's value, or 10 when the character is not a digit
181def digits.val(c: Char) -> U32:
182 digits.val.of(Char.to_u32(c))
183
184# accept one digit and keep reading, or stop when it is not a digit
185def digits.step(ok: Bool, next: Unit -> Maybe<&2, Nat>) -> Maybe<&2, Nat>:
186 match ok:
187 case False{}:
188 None{}
189 case True{}:
190 next(Unit{})
191
192# read a decimal token without building Base's Nat.read ceiling
193def digits.go(s: String, +acc: Nat, left: Nat) -> Maybe<&2, Nat>:
194 match s left:
195 case _ 0n:
196 None{}
197 case SNil{} 1n+k:
198 Some{acc}
199 case SCon{+h, t} 1n+k:
200 +d = digits.val(h)
201 digits.step(U32.is_lt(d, 10),
202 _u => digits.go(t, Nat.add(Nat.mul(acc, 10n), U32.to_nat(d)), k))
203
204# a short decimal (Content-Length, max-age). Empty is none. At most 9 digits.
205def digits.read(s: String) -> Maybe<&2, Nat>:
206 match s:
207 case SNil{}:
208 None{}
209 case SCon{h, t}:
210 digits.go(SCon{h, t}, 0n, 9n)
211
212# a non-zero chunk has its data and the following CRLF
213def chunks.ready(+after: String, +n: Nat) -> Bool:
214 Bool.and(Bool.not(Nat.is_lt(utf8.len(after), Nat.add(n, 2n))),
215 String.starts_with(utf8.drop(after, n), "\r\n"))
216
217# the next scan step, or why this chunk header is not usable
218type Next is Data:
219 Stop{}
220 Go{cut: Cut}
221 Reject{why: String}
222
223# one chunk header: reject non-hex sizes, stop on the 0 chunk, else continue
224def chunks.next.of(zero: Bool, ready: Bool, +after: String, +n: Nat) -> Next:
225 match zero ready:
226 case True{} _:
227 Stop{}
228 case False{} False{}:
229 Reject{"the chunked body stopped short"}
230 case False{} True{}:
231 Go{divide(utf8.drop(after, Nat.add(n, 2n)), "\r\n")}
232
233# hex check, then the length
234def chunks.next.hex(+before: String, +after: String, ok: Bool) -> Next:
235 match ok:
236 case False{}:
237 Reject{"chunk size is not hexadecimal"}
238 case True{}:
239 +n = hexlen(before)
240 chunks.next.of(Nat.is_eq(n, 0n), chunks.ready(after, n), after, n)
241
242# classify one chunk header (RFC 9112 §7.1)
243def chunks.next(+before: String, +after: String) -> Next:
244 chunks.next.hex(before, after, hex.well(chunks.token(before)))
245
246# apply one scan step
247def chunks.scan.step(step: Next, rest: Cut -> Maybe<&2, String>)
248 -> Maybe<&2, String>:
249 match step:
250 case Stop{}:
251 None{}
252 case Reject{why}:
253 Some{why}
254 case Go{cut}:
255 rest(cut)
256
257# None when every chunk size is hex and the 0 chunk is reached
258def chunks.scan(fuel: Nat, c: Cut) -> Maybe<&2, String>:
259 match fuel c:
260 case 0n _:
261 Some{"the chunked body is truncated"}
262 case 1n+f NoCut{}:
263 None{}
264 case 1n+f Cut{before, +after}:
265 chunks.scan.step(chunks.next(before, after), cut => chunks.scan(f, cut))
266
267# a zero chunk ends the body; anything after it is a trailer (RFC 9112 §7.1)
268def chunks.more(+n: Nat, +after: String, rest: Unit -> String, zero: Bool)
269 -> String:
270 match zero:
271 case True{}:
272 ""
273 case False{}:
274 utf8.take(after, n)
275 ++ rest(Unit{})
276
277# a chunked body put back together (RFC 9112 §7.1)
278def chunks(fuel: Nat, c: Cut) -> String:
279 match fuel c:
280 case 0n _:
281 ""
282 case 1n+f NoCut{}:
283 ""
284 case 1n+f Cut{before, +after}:
285 +n = hexlen(before)
286 chunks.more(n, after,
287 _u => chunks(f, divide(utf8.drop(after, Nat.add(n, 2n)), "\r\n")),
288 Nat.is_eq(n, 0n))
289
290# a Transfer-Encoding: chunked body as the octets it stands for
291def dechunk(+s: String) -> String:
292 chunks(String.length(s), divide(s, "\r\n"))
293
294# whether a head line names this header (field names are case-insensitive:
295# RFC 9110 §5.1)
296def head.hit(h: String, +name: String) -> Bool:
297 String.starts_with(String.to_lower(h), name ++ ":")
298
299# this line's value when it is the header asked for
300def head.pick(hit: Bool, h: String, name: String, rest: String) -> String:
301 match hit:
302 case True{}:
303 String.trim(String.drop(h, Nat.add(String.length(name), 1n)))
304 case False{}:
305 rest
306
307# the value a head gave a header, "" when it gave none
308def head.go(ls: List<&2, String>, +name: String) -> String:
309 match ls:
310 case []:
311 ""
312 case +h <> t:
313 head.pick(head.hit(h, name), h, name, head.go(t, name))
314
315# this line's trimmed field value
316def head.value(h: String, name: String) -> String:
317 String.trim(String.drop(h, Nat.add(String.length(name), 1n)))
318
319# cons a value when the line is the header asked for
320def head.values.cons(hit: Bool, value: String, rest: Unit -> List<&2, String>)
321 -> List<&2, String>:
322 match hit:
323 case False{}:
324 rest(Unit{})
325 case True{}:
326 value <> rest(Unit{})
327
328# every value a head gave a header, in order (RFC 9112 §6.3 lists Content-Length)
329def head.values(ls: List<&2, String>, +name: String) -> List<&2, String>:
330 match ls:
331 case []:
332 []
333 case +h <> t:
334 head.values.cons(head.hit(h, name), head.value(h, name),
335 _u => head.values(t, name))
336
337# a field value still holding a line break is obs-fold, which we refuse
338def field.folded(+value: String) -> Bool:
339 Bool.or(String.contains(value, "\n"), String.contains(value, "\r"))
340
341# a trimmed field value, or none when it still contains obs-fold
342def field.keep(name: String, +value: String, folded: Bool) -> Maybe<&2, Header>:
343 match folded:
344 case True{}:
345 None{}
346 case False{}:
347 Some{H{name, value}}
348
349# name and trimmed value from a cut at the first colon
350def head.from_kept(before: String, +after: String) -> Maybe<&2, Header>:
351 +value = String.trim(after)
352 field.keep(before, value, field.folded(value))
353
354# one header line as a Header, or none when it has no colon
355def head.from_cut(c: Cut) -> Maybe<&2, Header>:
356 match c:
357 case NoCut{}:
358 None{}
359 case Cut{before, after}:
360 head.from_kept(before, after)
361
362# one header line as a Header, or none when it has no colon
363def head.line(h: String) -> Maybe<&2, Header>:
364 head.from_cut(divide(h, ":"))
365
366# prepend a parsed header when present
367def head.cons(m: Maybe<&2, Header>, rest: List<&2, Header>) -> List<&2, Header>:
368 match m:
369 case None{}:
370 rest
371 case Some{hdr}:
372 hdr <> rest
373
374# header lines after the status line as a list of fields
375def head.list(ls: List<&2, String>) -> List<&2, Header>:
376 match ls:
377 case []:
378 []
379 case h <> t:
380 head.cons(head.line(h), head.list(t))
381
382# one request header line
383def header.line(h: Header) -> String:
384 match h:
385 case H{name, value}:
386 name ++ ": " ++ value ++ "\r\n"
387
388# the value when this field is the one asked for
389def headers.find.pick(value: String, hit: Bool, rest: Unit -> String) -> String:
390 match hit:
391 case True{}:
392 value
393 case False{}:
394 rest(Unit{})
395
396# case-insensitive field lookup (RFC 9110 §5.1)
397def headers.find.go(hs: List<&2, Header>, +name: String) -> String:
398 match hs:
399 case []:
400 ""
401 case H{n, v} <> t:
402 headers.find.pick(v, String.eq(String.to_lower(n), name),
403 _u => headers.find.go(t, name))
404
405# the value of a field, "" when it is absent
406def headers.find(hs: List<&2, Header>, +name: String) -> String:
407 headers.find.go(hs, String.to_lower(name))
408
409# extra headers rendered in order
410def headers.lines(hs: List<&2, Header>) -> String:
411 match hs:
412 case []:
413 ""
414 case h <> t:
415 header.line(h) ++ headers.lines(t)
416
417# the Content-Length field when the body is not empty (RFC 9110 §8.6)
418def clen.field(+n: Nat, empty: Bool) -> List<&2, Header>:
419 match empty:
420 case True{}:
421 []
422 case False{}:
423 [H{"Content-Length", Nat.show(n)}]
424
425# Content-Length line when the body is not empty (RFC 9110 §8.6)
426def clen.line(+n: Nat, empty: Bool) -> String:
427 headers.lines(clen.field(n, empty))
428
429# the fields a request names: the ones ezhttp writes a default for, the ones
430# it always computes, and every other (SPEC.md HTTP-CLI-8)
431type Field is Data:
432 FHost{}
433 FAgent{}
434 FAccept{}
435 FConn{}
436 FClen{}
437 FOther{}
438
439# a field's place in the order above
440def field.rank(f: Field) -> U32:
441 match f:
442 case FHost{}:
443 0
444 case FAgent{}:
445 1
446 case FAccept{}:
447 2
448 case FConn{}:
449 3
450 case FClen{}:
451 4
452 case FOther{}:
453 5
454
455# whether two fields are the same one
456def field.same(a: Field, b: Field) -> Bool:
457 U32.is_eq(field.rank(a), field.rank(b))
458
459# a lower-case name that is not content-length
460def field.of.clen(hit: Bool) -> Field:
461 match hit:
462 case True{}:
463 FClen{}
464 case False{}:
465 FOther{}
466
467# a lower-case name that is not connection
468def field.of.conn(hit: Bool, +l: String) -> Field:
469 match hit:
470 case True{}:
471 FConn{}
472 case False{}:
473 field.of.clen(String.eq(l, "content-length"))
474
475# a lower-case name that is not accept
476def field.of.accept(hit: Bool, +l: String) -> Field:
477 match hit:
478 case True{}:
479 FAccept{}
480 case False{}:
481 field.of.conn(String.eq(l, "connection"), l)
482
483# a lower-case name that is not user-agent
484def field.of.agent(hit: Bool, +l: String) -> Field:
485 match hit:
486 case True{}:
487 FAgent{}
488 case False{}:
489 field.of.accept(String.eq(l, "accept"), l)
490
491# a lower-case name that is not host
492def field.of.host(hit: Bool, +l: String) -> Field:
493 match hit:
494 case True{}:
495 FHost{}
496 case False{}:
497 field.of.agent(String.eq(l, "user-agent"), l)
498
499# the field a lower-case name names
500def field.of(+l: String) -> Field:
501 field.of.host(String.eq(l, "host"), l)
502
503# the field a name names, compared case-insensitively (RFC 9110 §5.1)
504def field.name(name: String) -> Field:
505 field.of(String.to_lower(name))
506
507# the field a header line names
508def header.field(h: Header) -> Field:
509 match h:
510 case H{name, value}:
511 field.name(name)
512
513# keep a header in front of the rest, or not
514def fields.put(keep: Bool, h: Header, rest: List<&2, Header>)
515 -> List<&2, Header>:
516 match keep:
517 case True{}:
518 h <> rest
519 case False{}:
520 rest
521
522# the headers that name one field, in order
523def fields.of(+f: Field, hs: List<&2, Header>) -> List<&2, Header>:
524 match hs:
525 case []:
526 []
527 case +h <> t:
528 fields.put(field.same(f, header.field(h)), h, fields.of(f, t))
529
530# the caller's fields of a name, or the default when it gave none
531def fields.or(given: List<&2, Header>, dflt: List<&2, Header>)
532 -> List<&2, Header>:
533 match given:
534 case []:
535 dflt
536 case h <> t:
537 h <> t
538
539# a request's header fields for a body of n octets: Host, User-Agent and
540# Accept (the caller's, or the default), Connection: close, the caller's other
541# fields, Content-Length.
542# A caller's Connection or Content-Length is not sent: Connection: close lets
543# the connection end frame the body when no Content-Length / chunked framing
544# applies (RFC 9112 §9.6 / §6.3), and the body's length is computed.
545def request.fields.n(host: String, +hs: List<&2, Header>, +n: Nat)
546 -> List<&2, Header>:
547 List.append(&2, Header, fields.or(fields.of(FHost{}, hs), [H{"Host", host}]),
548 List.append(&2, Header,
549 fields.or(fields.of(FAgent{}, hs), [H{"User-Agent", "ezhttp"}]),
550 List.append(&2, Header,
551 fields.or(fields.of(FAccept{}, hs), [H{"Accept", "*/*"}]),
552 H{"Connection", "close"}
553 <> List.append(&2, Header, fields.of(FOther{}, hs),
554 clen.field(n, Nat.is_eq(n, 0n))))))
555
556# a request's header fields for a text body: the fields for its UTF-8 octets
557def request.fields(host: String, +hs: List<&2, Header>, +body: String)
558 -> List<&2, Header>:
559 request.fields.n(host, hs, utf8.len(body))
560
561# a request-line and headers (RFC 9112 §3, §5). Absolute-path request-target
562# (RFC 9112 §3.2.1); the fields are request.fields'.
563def request(method: String, host: String, path: String,
564 headers: List<&2, Header>, +body: String) -> String:
565 method ++ " " ++ path ++ " HTTP/1.1\r\n"
566 ++ headers.lines(request.fields(host, headers, body))
567 ++ "\r\n"
568 ++ body
569
570# the port a scheme implies: 443 for a secure one, 80 otherwise (RFC 9110
571# §4.2.1, §4.2.2)
572def port.dflt(secure: Bool) -> U32:
573 match secure:
574 case True{}:
575 443
576 case False{}:
577 80
578
579# the Host field value once it is known whether the port is the default
580def authority.of(host: String, +port: U32, dflt: Bool) -> String:
581 match dflt:
582 case True{}:
583 host
584 case False{}:
585 host ++ ":" ++ U32.show(port)
586
587# the Host field value: the host, and the port after a colon unless it is the
588# scheme's default (RFC 9110 §7.2)
589def authority(secure: Bool, host: String, +port: U32) -> String:
590 authority.of(host, port, U32.is_eq(port, port.dflt(secure)))
591
592# the request a client sends to host and port, over TLS when secure
593def request.at(method: String, secure: Bool, host: String, port: U32,
594 path: String, headers: List<&2, Header>, body: String) -> String:
595 request(method, authority(secure, host, port), path, headers, body)
596
597# the request text for a body of n octets that is sent after it as its own
598# octets: the request line, the fields for n octets, and the blank line
599def request.head(method: String, host: String, path: String,
600 headers: List<&2, Header>, +n: Nat) -> String:
601 method ++ " " ++ path ++ " HTTP/1.1\r\n"
602 ++ headers.lines(request.fields.n(host, headers, n))
603 ++ "\r\n"
604
605# the request text a client sends to host and port ahead of n octets
606def request.head.at(method: String, secure: Bool, host: String, port: U32,
607 path: String, headers: List<&2, Header>, n: Nat) -> String:
608 request.head(method, authority(secure, host, port), path, headers, n)
609
610# GET with optional headers
611def get_req(host: String, path: String, headers: List<&2, Header>) -> String:
612 request("GET", host, path, headers, "")
613
614# HEAD with optional headers (RFC 9110 §9.3.2): same as GET, no body
615def head_req(host: String, path: String, headers: List<&2, Header>) -> String:
616 request("HEAD", host, path, headers, "")
617
618# POST with body and optional headers
619def post_req(host: String, path: String, headers: List<&2, Header>,
620 body: Body.Body) -> String:
621 request("POST", host, path, headers, Body.body.payload(body))
622
623# PUT with body and optional headers (RFC 9110 §9.3.4)
624def put_req(host: String, path: String, headers: List<&2, Header>,
625 body: Body.Body) -> String:
626 request("PUT", host, path, headers, Body.body.payload(body))
627
628# DELETE with body and optional headers (RFC 9110 §9.3.5)
629def delete_req(host: String, path: String, headers: List<&2, Header>,
630 body: Body.Body) -> String:
631 request("DELETE", host, path, headers, Body.body.payload(body))
632
633# OPTIONS with optional headers (RFC 9110 §9.3.7). No request body.
634def options_req(host: String, path: String, headers: List<&2, Header>) -> String:
635 request("OPTIONS", host, path, headers, "")
636
637# GET, HEAD, and OPTIONS are safe (RFC 9110 §9.2.1). Tokens are case-sensitive.
638def method.safe(+method: String) -> Bool:
639 Bool.or(String.eq(method, "GET"),
640 Bool.or(String.eq(method, "HEAD"), String.eq(method, "OPTIONS")))
641
642# safe methods, plus PUT and DELETE, are idempotent (RFC 9110 §9.2.2)
643def method.idempotent(+method: String) -> Bool:
644 Bool.or(method.safe(method),
645 Bool.or(String.eq(method, "PUT"), String.eq(method, "DELETE")))
646
647# the rest of a token once this character is known
648def token.ok.step(space: Bool, rest: Unit -> Bool) -> Bool:
649 match space:
650 case True{}:
651 False{}
652 case False{}:
653 rest(Unit{})
654
655# a bearer token has no whitespace (RFC 6750 §2.1)
656def token.ok(s: String) -> Bool:
657 match s:
658 case SNil{}:
659 True{}
660 case SCon{h, t}:
661 token.ok.step(Char.is_space(h), _u => token.ok(t))
662
663# origin-form request-target: absolute-path, optional query (RFC 9112 §3.2.1)
664def target.origin(path: String) -> Bool:
665 String.starts_with(path, "/")
666
667# asterisk-form is only `*` and only for OPTIONS (RFC 9112 §3.2.4)
668def target.asterisk(method: String, star: Bool) -> Bool:
669 match star:
670 case False{}:
671 False{}
672 case True{}:
673 String.eq(method, "OPTIONS")
674
675# origin-form, or OPTIONS asterisk-form
676def target.form(method: String, path: String, absolute: Bool) -> Bool:
677 match absolute:
678 case True{}:
679 True{}
680 case False{}:
681 target.asterisk(method, String.eq(path, "*"))
682
683# a body against the length its head promised
684def parse.short(status: U32, headers: List<&2, Header>, n: Nat, body: String,
685 short: Bool) -> Reply:
686 match short:
687 case True{}:
688 Torn{"the response body stopped before its Content-Length"}
689 case False{}:
690 Reply{status, headers, utf8.take(body, n)}
691
692# a body framed by Content-Length (RFC 9110 §8.6 / RFC 9112 §6.3)
693def parse.clen(status: U32, headers: List<&2, Header>, +n: Nat, +body: String)
694 -> Reply:
695 parse.short(status, headers, n, body, Nat.is_lt(utf8.len(body), n))
696
697# Content-Length when present; else the rest of the connection is the body
698def parse.len(status: U32, headers: List<&2, Header>, m: Maybe<&2, Nat>,
699 body: String) -> Reply:
700 match m:
701 case None{}:
702 Reply{status, headers, body}
703 case Some{n}:
704 parse.clen(status, headers, n, body)
705
706# every Content-Length text equals the first
707def clen.agree.step(same: Bool, rest: Unit -> Bool) -> Bool:
708 match same:
709 case False{}:
710 False{}
711 case True{}:
712 rest(Unit{})
713
714# the tail of a Content-Length list against the first value
715def clen.agree.go(rest: List<&2, String>, +h: String) -> Bool:
716 match rest:
717 case []:
718 True{}
719 case x <> r:
720 clen.agree.step(String.eq(x, h), _u => clen.agree.go(r, h))
721
722# duplicate Content-Length fields must be the same digits (RFC 9112 §6.3)
723def clen.agree(vs: List<&2, String>) -> Bool:
724 match vs:
725 case []:
726 True{}
727 case h <> t:
728 clen.agree.go(t, h)
729
730# whether any Content-Length field was present
731def clen.any(vs: List<&2, String>) -> Bool:
732 match vs:
733 case []:
734 False{}
735 case h <> t:
736 True{}
737
738# a chunked body, or why the chunk framing was rejected
739def parse.chunked(status: U32, headers: List<&2, Header>, body: String,
740 bad: Maybe<&2, String>) -> Reply:
741 match bad:
742 case None{}:
743 Reply{status, headers, dechunk(body)}
744 case Some{why}:
745 Torn{why}
746
747# scan chunk sizes, then decode when they are hex and closed by 0
748def parse.chunks(status: U32, headers: List<&2, Header>, +body: String) -> Reply:
749 parse.chunked(status, headers, body,
750 chunks.scan(String.length(body), divide(body, "\r\n")))
751
752# Transfer-Encoding together with Content-Length is a bad message
753def parse.te.clash(status: U32, headers: List<&2, Header>, body: String,
754 present: Bool) -> Reply:
755 match present:
756 case True{}:
757 Torn{"Content-Length and Transfer-Encoding conflict"}
758 case False{}:
759 parse.chunks(status, headers, body)
760
761# chunked framing, or Content-Length, or the rest of the connection
762def parse.te(status: U32, headers: List<&2, Header>, +lens: List<&2, String>,
763 +body: String, chunked: Bool) -> Reply:
764 match chunked:
765 case False{}:
766 parse.len(status, headers, digits.read(first(lens)), body)
767 case True{}:
768 parse.te.clash(status, headers, body, clen.any(lens))
769
770# disagreeing Content-Length values are torn before framing
771def parse.agree(status: U32, headers: List<&2, Header>, te: String,
772 +lens: List<&2, String>, body: String, ok: Bool) -> Reply:
773 match ok:
774 case False{}:
775 Torn{"Content-Length values disagree"}
776 case True{}:
777 parse.te(status, headers, lens, body,
778 String.contains(String.to_lower(te), "chunked"))
779
780# the headers that decide the framing (RFC 9112 §6.3)
781def parse.frame(status: U32, headers: List<&2, Header>, te: String,
782 +lens: List<&2, String>, body: String) -> Reply:
783 parse.agree(status, headers, te, lens, body, clen.agree(lens))
784
785# a head whose status line has been read (RFC 9112 §4)
786def parse.status(m: Maybe<&2, U32>, +ls: List<&2, String>, body: String)
787 -> Reply:
788 match m:
789 case None{}:
790 Torn{"the response has no status line"}
791 case Some{n}:
792 +hs = head.list(ls)
793 parse.frame(n, hs, head.go(ls, "transfer-encoding"),
794 head.values(ls, "content-length"), body)
795
796# the status code a head's first line names, if it names one (RFC 9112 §4)
797def status.of(ls: List<&2, String>) -> Maybe<&2, U32>:
798 U32.read(second(String.split(first(ls), ' ')))
799
800# the head's lines, with the status line read off the first
801def parse.head(+ls: List<&2, String>, body: String) -> Reply:
802 parse.status(status.of(ls), ls, body)
803
804# a response divided into its head and everything after the blank line
805# (RFC 9112 §2.1: header section ends at empty line)
806def parse.cut(c: Cut) -> Reply:
807 match c:
808 case NoCut{}:
809 Torn{"the response head has no blank line after it"}
810 case Cut{before, after}:
811 parse.head(String.lines(before), after)
812
813# the status, headers, and body of a raw response
814def parse(raw: String) -> Reply:
815 parse.cut(divide(raw, "\r\n\r\n"))
816
817# a parsed response on one line, for a test to read
818def show(r: Reply) -> String:
819 match r:
820 case Torn{why}:
821 "torn " ++ why
822 case Reply{status, headers, body}:
823 U32.show(status) ++ " " ++ body
824
825# --- inbound request (server) and outbound response (server) ---
826
827# a request that came apart, or the reason it would not (RFC 9112 §3)
828type Request is Data:
829 Bad{why: String}
830 Request{method: String, target: String, headers: List<&2, Header>,
831 body: String}
832
833# a status code and its reason-phrase
834type Phrase is Data:
835 P{code: U32, text: String}
836
837# the reason-phrases RFC 9110 §15 names (RFC 6585 §4 for 429)
838def reasons() -> List<&2, Phrase>:
839 [P{200, "OK"}, P{201, "Created"}, P{202, "Accepted"}, P{204, "No Content"},
840 P{301, "Moved Permanently"}, P{302, "Found"}, P{303, "See Other"},
841 P{304, "Not Modified"}, P{307, "Temporary Redirect"},
842 P{308, "Permanent Redirect"}, P{400, "Bad Request"},
843 P{401, "Unauthorized"}, P{403, "Forbidden"}, P{404, "Not Found"},
844 P{405, "Method Not Allowed"}, P{409, "Conflict"}, P{410, "Gone"},
845 P{413, "Content Too Large"}, P{415, "Unsupported Media Type"},
846 P{422, "Unprocessable Content"}, P{429, "Too Many Requests"},
847 P{500, "Internal Server Error"}, P{501, "Not Implemented"},
848 P{502, "Bad Gateway"}, P{503, "Service Unavailable"},
849 P{504, "Gateway Timeout"}]
850
851# this phrase when its code is the one asked for, else the rest's
852def reason.pick(text: String, hit: Bool, rest: Unit -> String) -> String:
853 match hit:
854 case True{}:
855 text
856 case False{}:
857 rest(Unit{})
858
859# the phrase a list gives a code, "" when it gives none
860def reason.in(ps: List<&2, Phrase>, +code: U32) -> String:
861 match ps:
862 case []:
863 ""
864 case P{c, text} <> t:
865 reason.pick(text, U32.is_eq(code, c), _u => reason.in(t, code))
866
867# the reason-phrase for a status code (RFC 9112 §4); "" for one not listed
868def reason(+code: U32) -> String:
869 reason.in(reasons(), code)
870
871# status-line + headers + body (RFC 9112 §4, §5). Connection: close ends the
872# exchange after one response.
873def respond(+status: U32, headers: List<&2, Header>, +body: String) -> String:
874 +n = utf8.len(body)
875 "HTTP/1.1 " ++ U32.show(status) ++ " " ++ reason(status) ++ "\r\n"
876 ++ "Connection: close\r\n"
877 ++ headers.lines(headers)
878 ++ clen.line(n, Nat.is_eq(n, 0n))
879 ++ "\r\n"
880 ++ body
881
882# 204 and 304 are terminated by the header section (RFC 9110 §15.3.5, §15.4.5)
883def status.nocontent(+code: U32) -> Bool:
884 Bool.or(U32.is_eq(code, 204), U32.is_eq(code, 304))
885
886# drop a 204/304 body; any other status keeps it
887def respond.of.body(+status: U32, headers: List<&2, Header>, body: String,
888 drop: Bool) -> String:
889 match drop:
890 case True{}:
891 respond(status, headers, "")
892 case False{}:
893 respond(status, headers, body)
894
895# format a structured Reply as a response message
896def respond.of(r: Reply) -> String:
897 match r:
898 case Torn{why}:
899 respond(500, [], why)
900 case Reply{+status, headers, body}:
901 respond.of.body(status, headers, body, status.nocontent(status))
902
903# HEAD carries no message body; any other method keeps the body (RFC 9110 §9.3.2)
904def reply.for.pick(reply: Reply, head: Bool) -> Reply:
905 match reply head:
906 case Torn{why} _:
907 Torn{why}
908 case Reply{status, headers, body} False{}:
909 Reply{status, headers, body}
910 case Reply{status, headers, body} True{}:
911 Reply{status, headers, ""}
912
913# drop a HEAD response body before it is written
914def reply.for(method: String, reply: Reply) -> Reply:
915 reply.for.pick(reply, String.eq(method, "HEAD"))
916
917# the method token, or "" when the request did not parse
918def method.of(req: Request) -> String:
919 match req:
920 case Bad{why}:
921 ""
922 case Request{method, target, headers, body}:
923 method
924
925# request body against Content-Length
926def ask.short(method: String, target: String, headers: List<&2, Header>,
927 n: Nat, body: String, short: Bool) -> Request:
928 match short:
929 case True{}:
930 Bad{"the request body stopped before its Content-Length"}
931 case False{}:
932 Request{method, target, headers, utf8.take(body, n)}
933
934# a request body framed by Content-Length (RFC 9110 §8.6 / RFC 9112 §6.3)
935def ask.clen(method: String, target: String, headers: List<&2, Header>,
936 +n: Nat, +body: String) -> Request:
937 ask.short(method, target, headers, n, body, Nat.is_lt(utf8.len(body), n))
938
939# Content-Length when present; else the rest of the connection is the body
940def ask.len(method: String, target: String, headers: List<&2, Header>,
941 m: Maybe<&2, Nat>, body: String) -> Request:
942 match m:
943 case None{}:
944 Request{method, target, headers, body}
945 case Some{n}:
946 ask.clen(method, target, headers, n, body)
947
948# a chunked request body, or why the chunk framing was rejected
949def ask.chunked(method: String, target: String, headers: List<&2, Header>,
950 body: String, bad: Maybe<&2, String>) -> Request:
951 match bad:
952 case None{}:
953 Request{method, target, headers, dechunk(body)}
954 case Some{why}:
955 Bad{why}
956
957# scan chunk sizes, then decode when they are hex and closed by 0
958def ask.chunks(method: String, target: String, headers: List<&2, Header>,
959 +body: String) -> Request:
960 ask.chunked(method, target, headers, body,
961 chunks.scan(String.length(body), divide(body, "\r\n")))
962
963# Transfer-Encoding together with Content-Length is a bad request
964def ask.te.clash(method: String, target: String, headers: List<&2, Header>,
965 body: String, present: Bool) -> Request:
966 match present:
967 case True{}:
968 Bad{"Content-Length and Transfer-Encoding conflict"}
969 case False{}:
970 ask.chunks(method, target, headers, body)
971
972# chunked framing, or Content-Length, or the rest of the connection
973def ask.te(method: String, target: String, headers: List<&2, Header>,
974 +lens: List<&2, String>, +body: String, chunked: Bool) -> Request:
975 match chunked:
976 case False{}:
977 ask.len(method, target, headers, digits.read(first(lens)), body)
978 case True{}:
979 ask.te.clash(method, target, headers, body, clen.any(lens))
980
981# disagreeing Content-Length values are bad before framing
982def ask.agree(method: String, target: String, headers: List<&2, Header>,
983 te: String, +lens: List<&2, String>, body: String, ok: Bool) -> Request:
984 match ok:
985 case False{}:
986 Bad{"Content-Length values disagree"}
987 case True{}:
988 ask.te(method, target, headers, lens, body,
989 String.contains(String.to_lower(te), "chunked"))
990
991# the headers that decide request framing (RFC 9112 §6.3)
992def ask.frame(method: String, target: String, headers: List<&2, Header>,
993 te: String, +lens: List<&2, String>, body: String) -> Request:
994 ask.agree(method, target, headers, te, lens, body, clen.agree(lens))
995
996# origin-form, or a bad request when the target is not an absolute-path
997def ask.origin(method: String, target: String, +ls: List<&2, String>,
998 body: String, ok: Bool) -> Request:
999 match ok:
1000 case False{}:
1001 Bad{"the request-target is not in origin-form"}
1002 case True{}:
1003 +hs = head.list(ls)
1004 ask.frame(method, target, hs, head.go(ls, "transfer-encoding"),
1005 head.values(ls, "content-length"), body)
1006
1007# request-line: method SP request-target SP HTTP-version (RFC 9112 §3)
1008def ask.line(+method: String, +target: String, +ls: List<&2, String>,
1009 body: String) -> Request:
1010 ask.origin(method, target, ls, body,
1011 target.form(method, target, target.origin(target)))
1012
1013# three fields of the request-line, or torn
1014def ask.parts(ps: List<&2, String>, +ls: List<&2, String>, body: String)
1015 -> Request:
1016 match ps:
1017 case []:
1018 Bad{"the request has no request line"}
1019 case m <> rest:
1020 match rest:
1021 case []:
1022 Bad{"the request line has no target"}
1023 case t <> _ver:
1024 ask.line(m, t, ls, body)
1025
1026# the head's lines, with the request-line read off the first
1027def ask.head(+ls: List<&2, String>, body: String) -> Request:
1028 match ls:
1029 case []:
1030 Bad{"the request has no request line"}
1031 case _:
1032 ask.parts(String.split(first(ls), ' '), ls, body)
1033
1034# a request divided into its head and everything after the blank line
1035def ask.cut(c: Cut) -> Request:
1036 match c:
1037 case NoCut{}:
1038 Bad{"the request head has no blank line after it"}
1039 case Cut{before, after}:
1040 ask.head(String.lines(before), after)
1041
1042# the method, target, headers, and body of a raw request
1043def ask(raw: String) -> Request:
1044 ask.cut(divide(raw, "\r\n\r\n"))
1045
1046# a parsed request on one line, for a test to read
1047def ask.show(r: Request) -> String:
1048 match r:
1049 case Bad{why}:
1050 "bad " ++ why
1051 case Request{method, target, headers, body}:
1052 method ++ " " ++ target ++ " " ++ body
1053
1054# --- when a response has all arrived (RFC 9112 §6.3) ---
1055
1056# how a response's body is framed
1057type Frame is Data:
1058 Bare{}
1059 Sized{n: Nat}
1060 Chunked{}
1061 Closed{}
1062
1063# 204 and 304 carry no body; a status line that did not parse is framed by
1064# its headers
1065def status.bare(m: Maybe<&2, U32>) -> Bool:
1066 match m:
1067 case None{}:
1068 False{}
1069 case Some{n}:
1070 status.nocontent(n)
1071
1072# a 1xx status is an interim response (RFC 9110 §15.2); a status line that
1073# did not parse is not
1074def status.interim(m: Maybe<&2, U32>) -> Bool:
1075 match m:
1076 case None{}:
1077 False{}
1078 case Some{+n}:
1079 Bool.and(U32.is_le(100, n), U32.is_lt(n, 200))
1080
1081# a Content-Length that reads as a number, or the close when none does
1082def frame.sized(m: Maybe<&2, Nat>) -> Frame:
1083 match m:
1084 case None{}:
1085 Closed{}
1086 case Some{n}:
1087 Sized{n}
1088
1089# Content-Length values that agree frame the body; any others leave the close
1090def frame.agree(+lens: List<&2, String>, ok: Bool) -> Frame:
1091 match ok:
1092 case False{}:
1093 Closed{}
1094 case True{}:
1095 frame.sized(digits.read(first(lens)))
1096
1097# chunked framing wins over Content-Length (RFC 9112 §6.3 item 4)
1098def frame.te(+lens: List<&2, String>, chunked: Bool) -> Frame:
1099 match chunked:
1100 case True{}:
1101 Chunked{}
1102 case False{}:
1103 frame.agree(lens, clen.agree(lens))
1104
1105# the framing of a response: none when bare (a reply to HEAD, a 204 or a 304),
1106# else Transfer-Encoding chunked, else Content-Length, else the close
1107def frame(bare: Bool, te: String, +lens: List<&2, String>) -> Frame:
1108 match bare:
1109 case True{}:
1110 Bare{}
1111 case False{}:
1112 frame.te(lens, String.contains(String.to_lower(te), "chunked"))
1113
1114# a zero chunk's trailer section has ended: at once, or after its fields
1115def chunks.trailer(+after: String) -> Bool:
1116 Bool.or(String.starts_with(after, "\r\n"), String.contains(after, "\r\n\r\n"))
1117
1118# a chunk that has all arrived: on to the next chunk header, else not yet
1119def chunks.ended.data(+after: String, +n: Nat, ready: Bool,
1120 rest: Cut -> Bool) -> Bool:
1121 match ready:
1122 case False{}:
1123 False{}
1124 case True{}:
1125 rest(divide(utf8.drop(after, Nat.add(n, 2n)), "\r\n"))
1126
1127# a chunk of size n: the last one when n is 0
1128def chunks.ended.size(+after: String, +n: Nat, zero: Bool,
1129 rest: Cut -> Bool) -> Bool:
1130 match zero:
1131 case True{}:
1132 chunks.trailer(after)
1133 case False{}:
1134 chunks.ended.data(after, n, chunks.ready(after, n), rest)
1135
1136# a chunk header: a size that is not hex ends the read (the parse rejects it)
1137def chunks.ended.hex(+before: String, +after: String, ok: Bool,
1138 rest: Cut -> Bool) -> Bool:
1139 match ok:
1140 case False{}:
1141 True{}
1142 case True{}:
1143 +n = hexlen(before)
1144 chunks.ended.size(after, n, Nat.is_eq(n, 0n), rest)
1145
1146# a chunk header that has arrived, or not yet
1147def chunks.ended.at(c: Cut, rest: Cut -> Bool) -> Bool:
1148 match c:
1149 case NoCut{}:
1150 False{}
1151 case Cut{+before, +after}:
1152 chunks.ended.hex(before, after, hex.well(chunks.token(before)), rest)
1153
1154# whether a chunked body has reached the end of its last chunk
1155def chunks.ended(fuel: Nat, c: Cut) -> Bool:
1156 match fuel:
1157 case 0n:
1158 False{}
1159 case 1n+f:
1160 chunks.ended.at(c, cut => chunks.ended(f, cut))
1161
1162# whether a body has all arrived under its framing
1163def whole.of(f: Frame, +body: String) -> Bool:
1164 match f:
1165 case Bare{}:
1166 True{}
1167 case Sized{n}:
1168 Bool.not(Nat.is_lt(utf8.len(body), n))
1169 case Chunked{}:
1170 chunks.ended(String.length(body), divide(body, "\r\n"))
1171 case Closed{}:
1172 False{}
1173
1174# a head that is interim: whole when what follows is; else whole under the
1175# framing it gives
1176def whole.step(asked: Bool, +ls: List<&2, String>, +after: String,
1177 interim: Bool, rest: Cut -> Bool) -> Bool:
1178 match interim:
1179 case True{}:
1180 rest(divide(after, "\r\n\r\n"))
1181 case False{}:
1182 whole.of(frame(Bool.or(asked, status.bare(status.of(ls))),
1183 head.go(ls, "transfer-encoding"), head.values(ls, "content-length")),
1184 after)
1185
1186# a response whose head has ended, or not yet
1187def whole.at(asked: Bool, c: Cut, rest: Cut -> Bool) -> Bool:
1188 match c:
1189 case NoCut{}:
1190 False{}
1191 case Cut{before, after}:
1192 +ls = String.lines(before)
1193 whole.step(asked, ls, after, status.interim(status.of(ls)), rest)
1194
1195# the heads in turn, at most `fuel` of them
1196def whole.go(fuel: Nat, +asked: Bool, c: Cut) -> Bool:
1197 match fuel:
1198 case 0n:
1199 False{}
1200 case 1n+f:
1201 whole.at(asked, c, cut => whole.go(f, asked, cut))
1202
1203# whether the text received so far is a whole response to a request with
1204# this method (RFC 9112 §6.3), interim 1xx heads read past (RFC 9110 §15.2);
1205# a response framed by the close never is
1206def whole(+method: String, +raw: String) -> Bool:
1207 whole.go(String.length(raw), String.eq(method, "HEAD"),
1208 divide(raw, "\r\n\r\n"))
1209
1210# --- a response read by the request's method (RFC 9110 §15.2, §6.4.1) ---
1211
1212# a 1xx, 204 or 304 response has no body (RFC 9110 §6.4.1)
1213def status.empty(+m: Maybe<&2, U32>) -> Bool:
1214 Bool.or(status.interim(m), status.bare(m))
1215
1216# an interim head is skipped when more text follows it
1217def interim.skip(m: Maybe<&2, U32>, after: String) -> Bool:
1218 Bool.and(status.interim(m), Bool.not(String.is_empty(after)))
1219
1220# the final head with no body: its status and fields, an empty body
1221def parse.to.bare(m: Maybe<&2, U32>, ls: List<&2, String>) -> Reply:
1222 match m:
1223 case None{}:
1224 Torn{"the response has no status line"}
1225 case Some{n}:
1226 Reply{n, head.list(ls), ""}
1227
1228# the final head: with no body, or framed as parse frames it
1229def parse.to.final(m: Maybe<&2, U32>, +ls: List<&2, String>, after: String,
1230 bare: Bool) -> Reply:
1231 match bare:
1232 case True{}:
1233 parse.to.bare(m, ls)
1234 case False{}:
1235 parse.status(m, ls, after)
1236
1237# an interim head is skipped, any other is the final one
1238def parse.to.step(head: Bool, +ls: List<&2, String>, +m: Maybe<&2, U32>,
1239 +after: String, skip: Bool, rest: Cut -> Reply) -> Reply:
1240 match skip:
1241 case True{}:
1242 rest(divide(after, "\r\n\r\n"))
1243 case False{}:
1244 parse.to.final(m, ls, after, Bool.or(head, status.empty(m)))
1245
1246# a head that has ended, or the reason it has not
1247def parse.to.at(head: Bool, c: Cut, rest: Cut -> Reply) -> Reply:
1248 match c:
1249 case NoCut{}:
1250 Torn{"the response head has no blank line after it"}
1251 case Cut{before, +after}:
1252 +ls = String.lines(before)
1253 +m = status.of(ls)
1254 parse.to.step(head, ls, m, after, interim.skip(m, after), rest)
1255
1256# the heads in turn, at most `fuel` of them
1257def parse.to.go(fuel: Nat, +head: Bool, c: Cut) -> Reply:
1258 match fuel:
1259 case 0n:
1260 Torn{"the response head has no blank line after it"}
1261 case 1n+f:
1262 parse.to.at(head, c, cut => parse.to.go(f, head, cut))
1263
1264# the response to a request with this method (RFC 9112 §6.3): interim 1xx
1265# heads skipped, and no body for HEAD or a 1xx, 204 or 304 final status
1266def parse.to(+method: String, +raw: String) -> Reply:
1267 parse.to.go(String.length(raw), String.eq(method, "HEAD"),
1268 divide(raw, "\r\n\r\n"))