http.bend

gralha-http-core@0.1.0.0 · 410 lines · 61 definitions

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.
4import Base
5
6# Utilities
7# =========
8
9# One of two computations, run on c; only the chosen one runs.
10def 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.
18def 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
27def cut(s: String, +sep: String) -> Maybe<&1, String & String>:
28  cut.go(s, sep, "")
29
30def 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.
38def before(+s: String, +sep: String) -> String:
39  before.cut(cut(s, sep), s)
40
41def 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.
49def after(s: String, +sep: String) -> String:
50  after.cut(cut(s, sep))
51
52# UTF-8
53# =====
54
55def 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
59def 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.
67def utf8.length(s: String) -> U32:
68  utf8.count(s, 0)
69
70# A character's UTF-8 bytes, prepended to acc in reverse.
71def 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.
83def 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
89def 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
95def 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
103def 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
110def utf8.decode(bytes: List<&2, U32>) -> String:
111  utf8.decode.go(bytes, 0, 0, "")
112
113# Urls
114# ====
115
116def 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
120def 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
124def 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.
138def url.decode(s: String) -> String:
139  utf8.decode(url.bytes(s, Nil{}))
140
141# A target's path: the part before ?.
142def target.path(+target: String) -> String:
143  before(target, "?")
144
145# A target's query: the part after ?, or "".
146def target.query(target: String) -> String:
147  after(target, "?")
148
149def 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").
158def query.get(query: String, +name: String) -> Maybe<&2, String>:
159  query.find(String.split(query, '&'), name)
160
161# Headers
162# =======
163
164type Header is Data:
165  Header{name: String, value: String}
166
167# The value of the first header named name, any case.
168def 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
176def header.get(headers: List<&2, Header>, name: String) -> Maybe<&2, String>:
177  header.find(headers, String.to_lower(name))
178
179def header.has(headers: List<&2, Header>, name: String) -> Bool:
180  Maybe.is_some(&2, String, header.get(headers, name))
181
182def 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.
190def 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
197def 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
204def 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.
212def number(+s: String) -> Maybe<&2, U32>:
213  when(Maybe<&2, U32>, digits(s), _ => U32.read(s), _ => None{})
214
215def 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.
223def content.length(headers: List<&2, Header>) -> U32:
224  number.or_zero(header.get(headers, "content-length"))
225
226# Requests
227# ========
228
229type Request is Data:
230  Request{method: String, target: String, version: String, headers: List<&2, Header>, body: String}
231
232def 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
239def 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
246def 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.
255def request.parse(text: String) -> Maybe<&2, Request>:
256  request.cut(cut(text, "\r\n\r\n"))
257
258def 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).
267def request.complete(text: String) -> Bool:
268  request.complete.cut(cut(text, "\r\n\r\n"))
269
270def request.method(r: Request) -> String:
271  match r:
272    case Request{m, t, v, h, b}:
273      m
274
275def request.target(r: Request) -> String:
276  match r:
277    case Request{m, t, v, h, b}:
278      t
279
280def request.path(r: Request) -> String:
281  match r:
282    case Request{m, t, v, h, b}:
283      target.path(t)
284
285def 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.
291def 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.
297def 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", "/").
303def 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
309type 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.
313def 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.
352def 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.
356def 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.
360def 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.
364def 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
369def 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.
376def 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
379def 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.
385def 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
393law ok_is_200:
394  for t: String
395  for b: String
396  {response.status(ok(t, b)) == 200 : U32}
397
398def ok_is_200(t, b):
399  {==}
400
401law 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
407def with_keeps_status(r, n, v):
408  match r:
409    case Response{s, h, b}:
410      {==}