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