1	# HTTP/1.1 messages: requests parsed from text, responses serialized to it.
2	# Pure: no IO, no foreign code. A server reads the text from a socket
3	# (gralha-http-server); a header name compares without case.
4	import Base
5	
6	# Utilities
7	# =========
8	
9	# One of two computations, run on c; only the chosen one runs.
10	def when(-A: Type, c: Bool, yes: Unit -> A, no: Unit -> A) -> A:
11	  match c:
12	    case True{}:
13	      yes(Unit{})
14	    case False{}:
15	      no(Unit{})
16	
17	# The text before the first sep and the text after it, or None without sep.
18	def cut.go(s: String, +sep: String, +acc: String) -> Maybe<&1, String & String>:
19	  match s:
20	    case SNil{}:
21	      None{}
22	    case SCon{+h, +t}:
23	      when(Maybe<&1, String & String>, String.starts_with(SCon{h, t}, sep),
24	        _ => Some{(String.reverse(acc), String.drop(SCon{h, t}, String.length(sep)))},
25	        _ => cut.go(t, sep, SCon{h, acc}))
26	
27	def cut(s: String, +sep: String) -> Maybe<&1, String & String>:
28	  cut.go(s, sep, "")
29	
30	def before.cut(c: Maybe<&1, String & String>, whole: String) -> String:
31	  match c:
32	    case None{}:
33	      whole
34	    case Some{(a, b)}:
35	      a
36	
37	# The text before sep, or all of it without sep.
38	def before(+s: String, +sep: String) -> String:
39	  before.cut(cut(s, sep), s)
40	
41	def after.cut(c: Maybe<&1, String & String>) -> String:
42	  match c:
43	    case None{}:
44	      ""
45	    case Some{(a, b)}:
46	      b
47	
48	# The text after sep, or "" without sep.
49	def after(s: String, +sep: String) -> String:
50	  after.cut(cut(s, sep))
51	
52	# UTF-8
53	# =====
54	
55	def utf8.width(+c: U32) -> U32:
56	  when(U32, U32.is_lt(c, 128), _ => 1, _ => when(U32, U32.is_lt(c, 2048), _ => 2,
57	    _ => when(U32, U32.is_lt(c, 65536), _ => 3, _ => 4)))
58	
59	def utf8.count(s: String, acc: U32) -> U32:
60	  match s:
61	    case SNil{}:
62	      acc
63	    case SCon{Chr{c}, t}:
64	      utf8.count(t, (acc + utf8.width(c) : U32))
65	
66	# The bytes a text takes in UTF-8, as Content-Length counts them.
67	def utf8.length(s: String) -> U32:
68	  utf8.count(s, 0)
69	
70	# A character's UTF-8 bytes, prepended to acc in reverse.
71	def utf8.push(+c: U32, +acc: List<&2, U32>) -> List<&2, U32>:
72	  +cont = ((c .&. 63) .|. 128 : U32)
73	  when(List<&2, U32>, U32.is_lt(c, 128), _ => c <> acc,
74	    _ => when(List<&2, U32>, U32.is_lt(c, 2048),
75	      _ => cont <> ((c >> 6n) .|. 192 : U32) <> acc,
76	      _ => when(List<&2, U32>, U32.is_lt(c, 65536),
77	        _ => cont <> (((c >> 6n) .&. 63) .|. 128 : U32) <> ((c >> 12n) .|. 224 : U32) <> acc,
78	        _ => cont <> (((c >> 6n) .&. 63) .|. 128 : U32) <> (((c >> 12n) .&. 63) .|. 128 : U32)
79	          <> ((c >> 18n) .|. 240 : U32) <> acc)))
80	
81	# Decoding reads a byte at a time: need is the continuation bytes still
82	# owed and code the bits so far. A byte out of place is U+FFFD.
83	def utf8.need(+b: U32, +need: U32) -> U32:
84	  when(U32, U32.is_eq(need, 0),
85	    _ => when(U32, U32.is_ge(b, 240), _ => 3, _ => when(U32, U32.is_ge(b, 224), _ => 2,
86	      _ => when(U32, U32.is_ge(b, 192), _ => 1, _ => 0))),
87	    _ => when(U32, U32.is_eq((b .&. 192 : U32), 128), _ => (need - 1 : U32), _ => 0))
88	
89	def utf8.code(+b: U32, +need: U32, +code: U32) -> U32:
90	  when(U32, U32.is_eq(need, 0),
91	    _ => when(U32, U32.is_ge(b, 240), _ => (b .&. 7 : U32), _ => when(U32, U32.is_ge(b, 224),
92	      _ => (b .&. 15 : U32), _ => (b .&. 31 : U32))),
93	    _ => ((code << 6n) .|. (b .&. 63) : U32))
94	
95	def utf8.emit(+b: U32, +need: U32, +code: U32, +acc: String) -> String:
96	  when(String, U32.is_eq(need, 0),
97	    _ => when(String, U32.is_lt(b, 128), _ => SCon{Chr{b}, acc},
98	      _ => when(String, U32.is_ge(b, 192), _ => acc, _ => SCon{Chr{65533}, acc})),
99	    _ => when(String, U32.is_eq((b .&. 192 : U32), 128),
100	      _ => when(String, U32.is_eq(need, 1), _ => SCon{Chr{utf8.code(b, need, code)}, acc}, _ => acc),
101	      _ => SCon{Chr{65533}, acc}))
102	
103	def utf8.decode.go(bytes: List<&2, U32>, +need: U32, +code: U32, acc: String) -> String:
104	  match bytes:
105	    case Nil{}:
106	      String.reverse(acc)
107	    case Con{+b, t}:
108	      utf8.decode.go(t, utf8.need(b, need), utf8.code(b, need, code), utf8.emit(b, need, code, acc))
109	
110	def utf8.decode(bytes: List<&2, U32>) -> String:
111	  utf8.decode.go(bytes, 0, 0, "")
112	
113	# Urls
114	# ====
115	
116	def hex.digit(+c: U32) -> U32:
117	  when(U32, U32.is_le(c, 57), _ => (c - 48 : U32),
118	    _ => when(U32, U32.is_le(c, 70), _ => (c - 55 : U32), _ => (c - 87 : U32)))
119	
120	def hex.is_digit(+c: U32) -> Bool:
121	  (U32.is_ge(c, 48) && U32.is_le(c, 57)) || (U32.is_ge(c, 65) && U32.is_le(c, 70))
122	    || (U32.is_ge(c, 97) && U32.is_le(c, 102))
123	
124	def url.bytes(s: String, +acc: List<&2, U32>) -> List<&2, U32>:
125	  match s:
126	    case SNil{}:
127	      List.reverse(&2, U32, acc)
128	    case SCon{Chr{+c}, SCon{Chr{+x}, SCon{Chr{+y}, +t}}}:
129	      when(List<&2, U32>, U32.is_eq(c, 37) && hex.is_digit(x) && hex.is_digit(y),
130	        _ => url.bytes(t, (hex.digit(x) * 16 + hex.digit(y) : U32) <> acc),
131	        _ => url.bytes(SCon{Chr{x}, SCon{Chr{y}, t}},
132	          utf8.push(when(U32, U32.is_eq(c, 43), _ => 32, _ => c), acc)))
133	    case SCon{Chr{+c}, t}:
134	      url.bytes(t, utf8.push(when(U32, U32.is_eq(c, 43), _ => 32, _ => c), acc))
135	
136	# A url component with %XX escapes and + (a space, as forms send it)
137	# decoded; the bytes read as UTF-8.
138	def url.decode(s: String) -> String:
139	  utf8.decode(url.bytes(s, Nil{}))
140	
141	# A target's path: the part before ?.
142	def target.path(+target: String) -> String:
143	  before(target, "?")
144	
145	# A target's query: the part after ?, or "".
146	def target.query(target: String) -> String:
147	  after(target, "?")
148	
149	def query.find(pairs: List<&2, String>, +name: String) -> Maybe<&2, String>:
150	  match pairs:
151	    case Nil{}:
152	      None{}
153	    case Con{+p, t}:
154	      when(Maybe<&2, String>, String.eq(url.decode(before(p, "=")), name),
155	        _ => Some{url.decode(after(p, "="))}, _ => query.find(t, name))
156	
157	# The first value of a query parameter, decoded, e.g. query.get("a=1&b=x%20y", "b").
158	def query.get(query: String, +name: String) -> Maybe<&2, String>:
159	  query.find(String.split(query, '&'), name)
160	
161	# Headers
162	# =======
163	
164	type Header is Data:
165	  Header{name: String, value: String}
166	
167	# The value of the first header named name, any case.
168	def header.find(headers: List<&2, Header>, +name: String) -> Maybe<&2, String>:
169	  match headers:
170	    case Nil{}:
171	      None{}
172	    case Con{Header{n, v}, t}:
173	      when(Maybe<&2, String>, String.eq(String.to_lower(n), name),
174	        _ => Some{v}, _ => header.find(t, name))
175	
176	def header.get(headers: List<&2, Header>, name: String) -> Maybe<&2, String>:
177	  header.find(headers, String.to_lower(name))
178	
179	def header.has(headers: List<&2, Header>, name: String) -> Bool:
180	  Maybe.is_some(&2, String, header.get(headers, name))
181	
182	def header.line(c: Maybe<&1, String & String>, rest: List<&2, Header>) -> List<&2, Header>:
183	  match c:
184	    case None{}:
185	      rest
186	    case Some{(n, v)}:
187	      Header{String.trim(n), String.trim(v)} <> rest
188	
189	# Header lines, "Name: value" each; a line with no colon is skipped.
190	def header.parse(lines: List<&2, String>) -> List<&2, Header>:
191	  match lines:
192	    case Nil{}:
193	      Nil{}
194	    case Con{l, t}:
195	      header.line(cut(l, ":"), header.parse(t))
196	
197	def header.text(headers: List<&2, Header>) -> String:
198	  match headers:
199	    case Nil{}:
200	      ""
201	    case Con{Header{n, v}, t}:
202	      n ++ ": " ++ v ++ "\r\n" ++ header.text(t)
203	
204	def digits(s: String) -> Bool:
205	  match s:
206	    case SNil{}:
207	      True{}
208	    case SCon{Chr{+c}, t}:
209	      U32.is_ge(c, 48) && U32.is_le(c, 57) && digits(t)
210	
211	# A decimal number made of digits only, as Content-Length is.
212	def number(+s: String) -> Maybe<&2, U32>:
213	  when(Maybe<&2, U32>, digits(s), _ => U32.read(s), _ => None{})
214	
215	def number.or_zero(m: Maybe<&2, String>) -> U32:
216	  match m:
217	    case None{}:
218	      0
219	    case Some{s}:
220	      Maybe.default(&2, U32, number(s), 0)
221	
222	# The Content-Length a header list declares, or 0.
223	def content.length(headers: List<&2, Header>) -> U32:
224	  number.or_zero(header.get(headers, "content-length"))
225	
226	# Requests
227	# ========
228	
229	type Request is Data:
230	  Request{method: String, target: String, version: String, headers: List<&2, Header>, body: String}
231	
232	def request.line(parts: List<&2, String>, headers: List<&2, Header>, body: String) -> Maybe<&2, Request>:
233	  match parts:
234	    case Con{m, Con{t, Con{v, Nil{}}}}:
235	      Some{Request{m, t, v, headers, body}}
236	    case _:
237	      None{}
238	
239	def request.head(lines: List<&2, String>, body: String) -> Maybe<&2, Request>:
240	  match lines:
241	    case Nil{}:
242	      None{}
243	    case Con{first, rest}:
244	      request.line(String.split(String.trim(first), ' '), header.parse(rest), body)
245	
246	def request.cut(c: Maybe<&1, String & String>) -> Maybe<&2, Request>:
247	  match c:
248	    case None{}:
249	      None{}
250	    case Some{(head, body)}:
251	      request.head(String.split(head, '\n'), body)
252	
253	# A request: "METHOD target HTTP/x.y", header lines, a blank line, the body
254	# (all that follows it). None when the head is unfinished or malformed.
255	def request.parse(text: String) -> Maybe<&2, Request>:
256	  request.cut(cut(text, "\r\n\r\n"))
257	
258	def request.complete.cut(c: Maybe<&1, String & String>) -> Bool:
259	  match c:
260	    case None{}:
261	      False{}
262	    case Some{(head, body)}:
263	      U32.is_ge(utf8.length(body), content.length(header.parse(String.split(head, '\n'))))
264	
265	# Whether text holds a whole request: its head ended, and as many body bytes
266	# as its Content-Length (none without one).
267	def request.complete(text: String) -> Bool:
268	  request.complete.cut(cut(text, "\r\n\r\n"))
269	
270	def request.method(r: Request) -> String:
271	  match r:
272	    case Request{m, t, v, h, b}:
273	      m
274	
275	def request.target(r: Request) -> String:
276	  match r:
277	    case Request{m, t, v, h, b}:
278	      t
279	
280	def request.path(r: Request) -> String:
281	  match r:
282	    case Request{m, t, v, h, b}:
283	      target.path(t)
284	
285	def request.body(r: Request) -> String:
286	  match r:
287	    case Request{m, t, v, h, b}:
288	      b
289	
290	# A header of the request, any case.
291	def request.header(r: Request, name: String) -> Maybe<&2, String>:
292	  match r:
293	    case Request{m, t, v, h, b}:
294	      header.get(h, name)
295	
296	# A query parameter of the request's target, decoded.
297	def request.query(r: Request, +name: String) -> Maybe<&2, String>:
298	  match r:
299	    case Request{m, t, v, h, b}:
300	      query.get(target.query(t), name)
301	
302	# Whether the request is method on path, e.g. request.is(r, "GET", "/").
303	def request.is(+r: Request, method: String, path: String) -> Bool:
304	  String.eq(request.method(r), method) && String.eq(request.path(r), path)
305	
306	# Responses
307	# =========
308	
309	type Response is Data:
310	  Response{status: U32, headers: List<&2, Header>, body: String}
311	
312	# The reason phrase of a status code, or "" for one not listed.
313	def reason(+code: U32) -> String:
314	  match code:
315	    case 200: "OK"
316	    case 201: "Created"
317	    case 202: "Accepted"
318	    case 204: "No Content"
319	    case 206: "Partial Content"
320	    case 100: "Continue"
321	    case 101: "Switching Protocols"
322	    case 301: "Moved Permanently"
323	    case 302: "Found"
324	    case 303: "See Other"
325	    case 304: "Not Modified"
326	    case 307: "Temporary Redirect"
327	    case 308: "Permanent Redirect"
328	    case 400: "Bad Request"
329	    case 401: "Unauthorized"
330	    case 403: "Forbidden"
331	    case 404: "Not Found"
332	    case 405: "Method Not Allowed"
333	    case 406: "Not Acceptable"
334	    case 408: "Request Timeout"
335	    case 409: "Conflict"
336	    case 410: "Gone"
337	    case 411: "Length Required"
338	    case 413: "Content Too Large"
339	    case 414: "URI Too Long"
340	    case 415: "Unsupported Media Type"
341	    case 416: "Range Not Satisfiable"
342	    case 422: "Unprocessable Content"
343	    case 429: "Too Many Requests"
344	    case 500: "Internal Server Error"
345	    case 501: "Not Implemented"
346	    case 502: "Bad Gateway"
347	    case 503: "Service Unavailable"
348	    case 504: "Gateway Timeout"
349	    case _: ""
350	
351	# A response with a status, a Content-Type and a body.
352	def response(+status: U32, content_type: String, body: String) -> Response:
353	  Response{status, [Header{"Content-Type", content_type}], body}
354	
355	# A 200 response with a Content-Type and a body.
356	def ok(content_type: String, body: String) -> Response:
357	  response(200, content_type, body)
358	
359	# A plain-text response with the status's reason phrase as its body.
360	def status(+code: U32) -> Response:
361	  response(code, "text/plain; charset=utf-8", reason(code))
362	
363	# The response with one more header, after the ones it has.
364	def response.with(r: Response, name: String, value: String) -> Response:
365	  match r:
366	    case Response{s, h, b}:
367	      Response{s, List.append(&2, Header, h, [Header{name, value}]), b}
368	
369	def response.status(r: Response) -> U32:
370	  match r:
371	    case Response{s, h, b}:
372	      s
373	
374	# The status line and the header lines, up to the blank line: what a server
375	# sends before a body it writes itself.
376	def head(+status: U32, headers: List<&2, Header>) -> String:
377	  "HTTP/1.1 " ++ U32.show(status) ++ " " ++ reason(status) ++ "\r\n" ++ header.text(headers) ++ "\r\n"
378	
379	def length.with(+headers: List<&2, Header>, +body: String) -> List<&2, Header>:
380	  when(List<&2, Header>, header.has(headers, "content-length"), _ => headers,
381	    _ => List.append(&2, Header, headers, [Header{"Content-Length", U32.show(utf8.length(body))}]))
382	
383	# The response as sent: its head, with a Content-Length counted in UTF-8
384	# bytes after its own headers (unless it has one), then its body.
385	def response.text(r: Response) -> String:
386	  match r:
387	    case Response{+s, h, +b}:
388	      head(s, length.with(h, b)) ++ b
389	
390	# Laws
391	# ====
392	
393	law ok_is_200:
394	  for t: String
395	  for b: String
396	  {response.status(ok(t, b)) == 200 : U32}
397	
398	def ok_is_200(t, b):
399	  {==}
400	
401	law with_keeps_status:
402	  for r: Response
403	  for n: String
404	  for v: String
405	  {response.status(response.with(r, n, v)) == response.status(r) : U32}
406	
407	def with_keeps_status(r, n, v):
408	  match r:
409	    case Response{s, h, b}:
410	      {==}