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.
4	import Base
5	import ./body.bend as Body
6	
7	# a string divided at the first occurrence of a pattern, or not divided at all
8	type 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)
13	type 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
17	type 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
22	def 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
30	def 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
38	def 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
46	def 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
55	def 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
64	def 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
68	def 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
75	def hex.val(c: Char) -> U32:
76	  hex.of(Char.to_u32(c))
77	
78	# one step of the hex read
79	def 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
87	def 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
97	def hexlen(s: String) -> Nat:
98	  hex.go(String.trim(first(String.split(s, ';'))), 0n)
99	
100	# whether a character is a hex digit
101	def 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
105	def 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)
115	def 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
123	def 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.
128	def 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
134	def 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
142	def 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
150	def 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
159	def 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
168	def 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
177	def 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
181	def 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
185	def 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
193	def 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.
205	def 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
213	def 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
218	type 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
224	def 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
234	def 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)
243	def chunks.next(+before: String, +after: String) -> Next:
244	  chunks.next.hex(before, after, hex.well(chunks.token(before)))
245	
246	# apply one scan step
247	def 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
258	def 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)
268	def 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)
278	def 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
291	def 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)
296	def 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
300	def 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
308	def 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
316	def 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
320	def 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)
329	def 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
338	def 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
342	def 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
350	def 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
355	def 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
363	def head.line(h: String) -> Maybe<&2, Header>:
364	  head.from_cut(divide(h, ":"))
365	
366	# prepend a parsed header when present
367	def 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
375	def 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
383	def 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
389	def 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)
397	def 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
406	def 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
410	def 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)
418	def 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)
426	def 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)
431	type 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
440	def 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
456	def 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
460	def 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
468	def 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
476	def 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
484	def 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
492	def 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
500	def 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)
504	def field.name(name: String) -> Field:
505	  field.of(String.to_lower(name))
506	
507	# the field a header line names
508	def 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
514	def 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
523	def 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
531	def 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.
545	def 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
557	def 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'.
563	def 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)
572	def 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
580	def 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)
589	def 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
593	def 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
599	def 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
606	def 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
611	def 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
615	def 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
619	def 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)
624	def 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)
629	def 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.
634	def 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.
638	def 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)
643	def 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
648	def 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)
656	def 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)
664	def 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)
668	def 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
676	def 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
684	def 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)
693	def 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
698	def 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
707	def 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
715	def 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)
723	def 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
731	def 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
739	def 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
748	def 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
753	def 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
762	def 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
771	def 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)
781	def 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)
786	def 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)
797	def 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
801	def 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)
806	def 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
814	def 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
818	def 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)
828	type 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
834	type Phrase is Data:
835	  P{code: U32, text: String}
836	
837	# the reason-phrases RFC 9110 §15 names (RFC 6585 §4 for 429)
838	def 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
852	def 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
860	def 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
868	def 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.
873	def 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)
883	def 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
887	def 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
896	def 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)
904	def 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
914	def 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
918	def 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
926	def 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)
935	def 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
940	def 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
949	def 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
958	def 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
964	def 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
973	def 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
982	def 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)
992	def 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
997	def 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)
1008	def 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
1014	def 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
1027	def 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
1035	def 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
1043	def 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
1047	def 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
1057	type 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
1065	def 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
1074	def 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
1082	def 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
1090	def 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)
1098	def 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
1107	def 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
1115	def 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
1119	def 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
1128	def 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)
1137	def 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
1147	def 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
1155	def 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
1163	def 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
1176	def 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
1187	def 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
1196	def 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
1206	def 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)
1213	def 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
1217	def 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
1221	def 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
1229	def 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
1238	def 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
1247	def 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
1257	def 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
1266	def 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"))