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