src/wirespec.bend
emerging-ezhttp@0.17.0.0 · 354 lines · 0 definitions
1# ezhttp/src/wirespec: the text the wire effect reads, and what its answer
2# means, pure. Kept apart from wire.bend (the effect) so the proof gate can
3# import it. What the client sends for a URL (wire.exchange) and when it has
4# heard a whole answer (wire.read.next) are decided here; wire.bend and
5# client.bend act on them.
6#
7# Spec: scheme, host, port each on their own line; everything after the third
8# newline is the request verbatim. The scheme line may carry a timeout after a
9# space: 32 binary digits, least significant first, in milliseconds. A scheme
10# line with no timeout means 60000 ms. SPEC.md HTTP-CLI lists what is
11# guaranteed.
12import Base
13import emerging-ezhttp@0.17.0.0/src/http.bend as Http
14import emerging-ezhttp@0.17.0.0/src/url.bend as Url
15import emerging-ezhttp@0.17.0.0/src/body.bend as Body
16
17# the word the effect reads for a scheme that wants TLS
18def wire.scheme(secure: Bool) -> String:
19 match secure:
20 case True{}:
21 "tls"
22 case False{}:
23 "tcp"
24
25# the spec the effect reads
26def wire.spec(secure: Bool, host: String, port: U32, req: String) -> String:
27 wire.scheme(secure) ++ "\n" ++ host ++ "\n" ++ U32.show(port) ++ "\n" ++ req
28
29# --- the timeout ---
30
31# the timeout a spec with none carries: 60 s, in milliseconds
32def wire.ms.dflt() -> U32:
33 60000
34
35# one bit as a binary digit
36def wire.bit(b: Bool) -> Char:
37 match b:
38 case True{}:
39 '1'
40 case False{}:
41 '0'
42
43# a word as binary digits, least significant first
44def wire.bits(n: Nat, w: Word(n)) -> String:
45 match n:
46 case 0n:
47 SNil{}
48 case 1n+p:
49 match w:
50 case WCon{b, t}:
51 SCon{wire.bit(b), wire.bits(p, t)}
52
53# binary digits, least significant first, as a word; a missing digit is 0
54def wire.bits.read(n: Nat, s: String) -> Word(n):
55 match n:
56 case 0n:
57 WNil{}
58 case 1n+p:
59 match s:
60 case SNil{}:
61 WCon{False{}, wire.bits.read(p, SNil{})}
62 case SCon{c, t}:
63 WCon{Char.is_eq(c, '1'), wire.bits.read(p, t)}
64
65# a timeout as the scheme line carries it
66def wire.ms.text(ms: U32) -> String:
67 match ms:
68 case U32{w}:
69 wire.bits(32n, w)
70
71# the first line of a timed spec: the scheme, a space, the timeout
72def wire.head(secure: Bool, ms: U32) -> String:
73 wire.scheme(secure) ++ " " ++ wire.ms.text(ms)
74
75# the lines after the first: host, port, then the request verbatim
76def wire.rest(host: String, port: U32, req: String) -> String:
77 host ++ "\n" ++ U32.show(port) ++ "\n" ++ req
78
79# the spec the effect reads, with a timeout in milliseconds
80def wire.spec.timed(secure: Bool, ms: U32, host: String, port: U32,
81 req: String) -> String:
82 wire.head(secure, ms) ++ "\n" ++ wire.rest(host, port, req)
83
84# the timeout after the scheme word, or the default when there is none
85def wire.ms.words(ws: List<&2, String>) -> U32:
86 match ws:
87 case []:
88 wire.ms.dflt()
89 case _ <> []:
90 wire.ms.dflt()
91 case _ <> (bits <> _):
92 U32{wire.bits.read(32n, bits)}
93
94# the first line of a spec
95def wire.line(ls: List<&2, String>) -> String:
96 match ls:
97 case []:
98 ""
99 case l <> _:
100 l
101
102# the timeout the effect reads from a spec, in milliseconds
103def wire.ms(spec: String) -> U32:
104 wire.ms.words(String.split(wire.line(String.split(spec, '\n')), ' '))
105
106# --- the answer ---
107
108# the wire status for an exchange that ran out of time (curl's
109# CURLE_OPERATION_TIMEDOUT)
110def wire.late() -> U32:
111 28
112
113# what a failed exchange is reported as: a timeout is marked, any other
114# failure's reason is kept as it is
115def wire.why.of(why: String, late: Bool) -> String:
116 match late:
117 case True{}:
118 "timed out: " ++ why
119 case False{}:
120 why
121
122# a failed exchange's status and reason as the reason the client reports
123def wire.why(code: Maybe<&2, U32>, why: String) -> String:
124 match code:
125 case None{}:
126 why
127 case Some{n}:
128 wire.why.of(why, U32.is_eq(n, wire.late()))
129
130# whether a reported reason is a timeout
131def wire.timed_out(why: String) -> Bool:
132 String.starts_with(why, "timed out: ")
133
134# --- what is sent ---
135
136# what a request to a URL becomes: nothing when the URL did not parse, else
137# the scheme (secure or not), host, port, method and request text the effect
138# is given; the answer is read by that method (wire.read.next)
139type Exchange is Data:
140 NoUrl{why: String}
141 Exchange{secure: Bool, host: String, port: U32, method: String, req: String}
142
143# the exchange once it is known whether the scheme wants TLS
144def wire.exchange.at(+method: String, +secure: Bool, +host: String,
145 +port: U32, path: String, headers: List<&2, Http.Header>, body: String)
146 -> Exchange:
147 Exchange{secure, host, port, method,
148 Http.request.at(method, secure, host, port, path, headers, body)}
149
150# the method an exchange is sent and read by, none when nothing is sent
151def wire.exchange.method(ex: Exchange) -> Maybe<&2, String>:
152 match ex:
153 case NoUrl{why}:
154 None{}
155 case Exchange{secure, host, port, method, req}:
156 Some{method}
157
158# a request with this method, headers and body to a URL that came apart
159def wire.exchange(method: String, l: Url.Loc, headers: List<&2, Http.Header>,
160 body: String) -> Exchange:
161 match l:
162 case Url.Bad{why}:
163 NoUrl{why}
164 case Url.Loc{scheme, host, port, path}:
165 +secure = String.eq(scheme, "https")
166 wire.exchange.at(method, secure, host, port, path, headers, body)
167
168# a request with n octets of body to a URL that came apart: the request text
169# ends at the blank line, and the octets go after it as the tail (wire.tail)
170def wire.exchange.octets(+method: String, l: Url.Loc,
171 headers: List<&2, Http.Header>, n: Nat) -> Exchange:
172 match l:
173 case Url.Bad{why}:
174 NoUrl{why}
175 case Url.Loc{scheme, +host, +port, path}:
176 +secure = String.eq(scheme, "https")
177 Exchange{secure, host, port, method,
178 Http.request.head.at(method, secure, host, port, path, headers, n)}
179
180# a request with this body to a URL that came apart: text inside the request
181# text as UTF-8, octets after it (SPEC.md HTTP-CLI-10)
182def wire.exchange.body(method: String, l: Url.Loc,
183 headers: List<&2, Http.Header>, b: Body.Body) -> Exchange:
184 match b:
185 case Body.Empty{}:
186 wire.exchange(method, l, headers, "")
187 case Body.Plain{text}:
188 wire.exchange(method, l, headers, text)
189 case Body.Octets{bytes}:
190 wire.exchange.octets(method, l, headers, List.length(&2, U32, bytes))
191
192# the octets sent after the request text: an octet body's, else none
193def wire.tail(b: Body.Body) -> List<&2, U32>:
194 match b:
195 case Body.Empty{}:
196 []
197 case Body.Plain{text}:
198 []
199 case Body.Octets{bytes}:
200 bytes
201
202# --- what is heard ---
203
204# an answer's status: the number on its first line, if it is one
205def wire.code.of(c: Http.Cut, raw: String) -> Maybe<&2, U32>:
206 match c:
207 case Http.NoCut{}:
208 U32.read(raw)
209 case Http.Cut{before, after}:
210 U32.read(before)
211
212# an answer's status line as a number
213def wire.code(+raw: String) -> Maybe<&2, U32>:
214 wire.code.of(Http.divide(raw, "\n"), raw)
215
216# the text after an answer's first newline
217def wire.text.of(c: Http.Cut) -> String:
218 match c:
219 case Http.NoCut{}:
220 ""
221 case Http.Cut{before, after}:
222 after
223
224# the text after an answer's first newline
225def wire.text(raw: String) -> String:
226 wire.text.of(Http.divide(raw, "\n"))
227
228# whether a status is success (0)
229def wire.ok.of(m: Maybe<&2, U32>) -> Bool:
230 match m:
231 case None{}:
232 False{}
233 case Some{n}:
234 U32.is_eq(n, 0)
235
236# whether an answer has status 0
237def wire.ok(raw: String) -> Bool:
238 wire.ok.of(wire.code(raw))
239
240# what an open answered: a connection to read from, or the answer itself
241type Opened is Data:
242 Refused{answer: String}
243 Open{conn: U32}
244
245# a connection number that read, or a malformed answer when it did not
246def wire.opened.conn(m: Maybe<&2, U32>) -> Opened:
247 match m:
248 case None{}:
249 Refused{"22\na malformed connection number"}
250 case Some{n}:
251 Open{n}
252
253# an open's answer once it is known whether it succeeded
254def wire.opened.of(+got: String, ok: Bool) -> Opened:
255 match ok:
256 case False{}:
257 Refused{got}
258 case True{}:
259 wire.opened.conn(U32.read(wire.text(got)))
260
261# what an open's answer means
262def wire.opened(+got: String) -> Opened:
263 wire.opened.of(got, wire.ok(got))
264
265# what has been received so far: its pieces, the newest first, and where
266# the response stands (Http.hear)
267type Got is Data:
268 Got{pieces: List<&2, String>, hear: Http.Hear}
269
270# the text a list of pieces, newest first, stands for
271def wire.joined(ps: List<&2, String>) -> String:
272 match ps:
273 case []:
274 ""
275 case p <> rest:
276 wire.joined(rest) ++ p
277
278# the pieces put together onto what follows them, each copied once
279def wire.join.go(ps: List<&2, String>, acc: String) -> String:
280 match ps:
281 case []:
282 acc
283 case p <> rest:
284 wire.join.go(rest, p ++ acc)
285
286# the text a list of pieces, newest first, stands for, built in one pass
287def wire.join(ps: List<&2, String>) -> String:
288 wire.join.go(ps, "")
289
290# what has been received as these pieces, for a request with this method
291def wire.got(+method: String, +ps: List<&2, String>) -> Got:
292 Got{ps, Http.hear.of(method, wire.joined(ps))}
293
294# after a read: read again with what has arrived, or answer
295type Read is Data:
296 Again{acc: Got}
297 Heard{answer: String}
298
299# everything received, once it is known whether it is a whole response
300def wire.read.whole(+ps: List<&2, String>, h: Http.Hear, done: Bool) -> Read:
301 match done:
302 case True{}:
303 Heard{"0\n" ++ wire.join(ps)}
304 case False{}:
305 Again{Got{ps, h}}
306
307# a read that brought text, judged with where the response now stands
308def wire.read.add(text: String, ps: List<&2, String>, +h: Http.Hear) -> Read:
309 wire.read.whole(text <> ps, h, Http.hear.done(h))
310
311# a read that brought text, or found the connection closed
312def wire.read.got(st: Got, +text: String, closed: Bool) -> Read:
313 match st closed:
314 case Got{ps, h} True{}:
315 Heard{"0\n" ++ wire.join(ps)}
316 case Got{ps, h} False{}:
317 wire.read.add(text, ps, Http.hear.more(h, text))
318
319# a read's answer once it is known whether it succeeded
320def wire.read.of(st: Got, +got: String, ok: Bool) -> Read:
321 match ok:
322 case False{}:
323 Heard{got}
324 case True{}:
325 +text = wire.text(got)
326 wire.read.got(st, text, String.is_empty(text))
327
328# what to do after a read answered `got`, with what was received before it
329# (SPEC.md HTTP-CLI-6)
330def wire.read.next(st: Got, +got: String) -> Read:
331 wire.read.of(st, got, wire.ok(got))
332
333# the answer when the reads run out before the response ends
334def wire.spent() -> String:
335 "56\nthe answer did not end within 65536 reads"
336
337# the response an exchange's answer holds, read by the request's method
338# (SPEC.md HTTP-CLI-9); a failed exchange is torn with the reason it is
339# reported with (wire.why)
340def wire.heard.of(+method: String, +raw: String, ok: Bool) -> Http.Reply:
341 match ok:
342 case False{}:
343 Http.Torn{wire.why(wire.code(raw), wire.text(raw))}
344 case True{}:
345 Http.parse.to(method, wire.text(raw))
346
347# the reason phrase of the response an exchange's answer holds (SPEC.md
348# HTTP-CLI-11); a failed exchange's is read from its reason and not used
349def wire.phrase(raw: String) -> String:
350 Http.phrase.to(wire.text(raw))
351
352# the response an exchange's answer holds
353def wire.heard(+method: String, +raw: String) -> Http.Reply:
354 wire.heard.of(method, raw, wire.ok(raw))