src/wirespec.bend
emerging-ezhttp@0.13.0.0 · 269 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.13.0.0/src/http.bend as Http
14import emerging-ezhttp@0.13.0.0/src/url.bend as Url
15
16# the word the effect reads for a scheme that wants TLS
17def wire.scheme(secure: Bool) -> String:
18 match secure:
19 case True{}:
20 "tls"
21 case False{}:
22 "tcp"
23
24# the spec the effect reads
25def wire.spec(secure: Bool, host: String, port: U32, req: String) -> String:
26 wire.scheme(secure) ++ "\n" ++ host ++ "\n" ++ U32.show(port) ++ "\n" ++ req
27
28# --- the timeout ---
29
30# the timeout a spec with none carries: 60 s, in milliseconds
31def wire.ms.dflt() -> U32:
32 60000
33
34# one bit as a binary digit
35def wire.bit(b: Bool) -> Char:
36 match b:
37 case True{}:
38 '1'
39 case False{}:
40 '0'
41
42# a word as binary digits, least significant first
43def wire.bits(n: Nat, w: Word(n)) -> String:
44 match n:
45 case 0n:
46 SNil{}
47 case 1n+p:
48 match w:
49 case WCon{b, t}:
50 SCon{wire.bit(b), wire.bits(p, t)}
51
52# binary digits, least significant first, as a word; a missing digit is 0
53def wire.bits.read(n: Nat, s: String) -> Word(n):
54 match n:
55 case 0n:
56 WNil{}
57 case 1n+p:
58 match s:
59 case SNil{}:
60 WCon{False{}, wire.bits.read(p, SNil{})}
61 case SCon{c, t}:
62 WCon{Char.is_eq(c, '1'), wire.bits.read(p, t)}
63
64# a timeout as the scheme line carries it
65def wire.ms.text(ms: U32) -> String:
66 match ms:
67 case U32{w}:
68 wire.bits(32n, w)
69
70# the first line of a timed spec: the scheme, a space, the timeout
71def wire.head(secure: Bool, ms: U32) -> String:
72 wire.scheme(secure) ++ " " ++ wire.ms.text(ms)
73
74# the lines after the first: host, port, then the request verbatim
75def wire.rest(host: String, port: U32, req: String) -> String:
76 host ++ "\n" ++ U32.show(port) ++ "\n" ++ req
77
78# the spec the effect reads, with a timeout in milliseconds
79def wire.spec.timed(secure: Bool, ms: U32, host: String, port: U32,
80 req: String) -> String:
81 wire.head(secure, ms) ++ "\n" ++ wire.rest(host, port, req)
82
83# the timeout after the scheme word, or the default when there is none
84def wire.ms.words(ws: List<&2, String>) -> U32:
85 match ws:
86 case []:
87 wire.ms.dflt()
88 case _ <> []:
89 wire.ms.dflt()
90 case _ <> (bits <> _):
91 U32{wire.bits.read(32n, bits)}
92
93# the first line of a spec
94def wire.line(ls: List<&2, String>) -> String:
95 match ls:
96 case []:
97 ""
98 case l <> _:
99 l
100
101# the timeout the effect reads from a spec, in milliseconds
102def wire.ms(spec: String) -> U32:
103 wire.ms.words(String.split(wire.line(String.split(spec, '\n')), ' '))
104
105# --- the answer ---
106
107# the wire status for an exchange that ran out of time (curl's
108# CURLE_OPERATION_TIMEDOUT)
109def wire.late() -> U32:
110 28
111
112# what a failed exchange is reported as: a timeout is marked, any other
113# failure's reason is kept as it is
114def wire.why.of(why: String, late: Bool) -> String:
115 match late:
116 case True{}:
117 "timed out: " ++ why
118 case False{}:
119 why
120
121# a failed exchange's status and reason as the reason the client reports
122def wire.why(code: Maybe<&2, U32>, why: String) -> String:
123 match code:
124 case None{}:
125 why
126 case Some{n}:
127 wire.why.of(why, U32.is_eq(n, wire.late()))
128
129# whether a reported reason is a timeout
130def wire.timed_out(why: String) -> Bool:
131 String.starts_with(why, "timed out: ")
132
133# --- what is sent ---
134
135# what a request to a URL becomes: nothing when the URL did not parse, else
136# the scheme (secure or not), host, port, method and request text the effect
137# is given; the answer is read by that method (wire.read.next)
138type Exchange is Data:
139 NoUrl{why: String}
140 Exchange{secure: Bool, host: String, port: U32, method: String, req: String}
141
142# the exchange once it is known whether the scheme wants TLS
143def wire.exchange.at(+method: String, +secure: Bool, +host: String,
144 +port: U32, path: String, headers: List<&2, Http.Header>, body: String)
145 -> Exchange:
146 Exchange{secure, host, port, method,
147 Http.request.at(method, secure, host, port, path, headers, body)}
148
149# the method an exchange is sent and read by, none when nothing is sent
150def wire.exchange.method(ex: Exchange) -> Maybe<&2, String>:
151 match ex:
152 case NoUrl{why}:
153 None{}
154 case Exchange{secure, host, port, method, req}:
155 Some{method}
156
157# a request with this method, headers and body to a URL that came apart
158def wire.exchange(method: String, l: Url.Loc, headers: List<&2, Http.Header>,
159 body: String) -> Exchange:
160 match l:
161 case Url.Bad{why}:
162 NoUrl{why}
163 case Url.Loc{scheme, host, port, path}:
164 +secure = String.eq(scheme, "https")
165 wire.exchange.at(method, secure, host, port, path, headers, body)
166
167# --- what is heard ---
168
169# an answer's status: the number on its first line, if it is one
170def wire.code.of(c: Http.Cut, raw: String) -> Maybe<&2, U32>:
171 match c:
172 case Http.NoCut{}:
173 U32.read(raw)
174 case Http.Cut{before, after}:
175 U32.read(before)
176
177# an answer's status line as a number
178def wire.code(+raw: String) -> Maybe<&2, U32>:
179 wire.code.of(Http.divide(raw, "\n"), raw)
180
181# the text after an answer's first newline
182def wire.text.of(c: Http.Cut) -> String:
183 match c:
184 case Http.NoCut{}:
185 ""
186 case Http.Cut{before, after}:
187 after
188
189# the text after an answer's first newline
190def wire.text(raw: String) -> String:
191 wire.text.of(Http.divide(raw, "\n"))
192
193# whether a status is success (0)
194def wire.ok.of(m: Maybe<&2, U32>) -> Bool:
195 match m:
196 case None{}:
197 False{}
198 case Some{n}:
199 U32.is_eq(n, 0)
200
201# whether an answer has status 0
202def wire.ok(raw: String) -> Bool:
203 wire.ok.of(wire.code(raw))
204
205# what an open answered: a connection to read from, or the answer itself
206type Opened is Data:
207 Refused{answer: String}
208 Open{conn: U32}
209
210# a connection number that read, or a malformed answer when it did not
211def wire.opened.conn(m: Maybe<&2, U32>) -> Opened:
212 match m:
213 case None{}:
214 Refused{"22\na malformed connection number"}
215 case Some{n}:
216 Open{n}
217
218# an open's answer once it is known whether it succeeded
219def wire.opened.of(+got: String, ok: Bool) -> Opened:
220 match ok:
221 case False{}:
222 Refused{got}
223 case True{}:
224 wire.opened.conn(U32.read(wire.text(got)))
225
226# what an open's answer means
227def wire.opened(+got: String) -> Opened:
228 wire.opened.of(got, wire.ok(got))
229
230# after a read: read again with what has arrived, or answer
231type Read is Data:
232 Again{acc: String}
233 Heard{answer: String}
234
235# everything received, once it is known whether it is a whole response
236def wire.read.whole(all: String, done: Bool) -> Read:
237 match done:
238 case True{}:
239 Heard{"0\n" ++ all}
240 case False{}:
241 Again{all}
242
243# a read that brought text, or found the connection closed
244def wire.read.got(+method: String, acc: String, text: String, closed: Bool)
245 -> Read:
246 match closed:
247 case True{}:
248 Heard{"0\n" ++ acc}
249 case False{}:
250 +all = acc ++ text
251 wire.read.whole(all, Http.whole(method, all))
252
253# a read's answer once it is known whether it succeeded
254def wire.read.of(+method: String, acc: String, +got: String, ok: Bool) -> Read:
255 match ok:
256 case False{}:
257 Heard{got}
258 case True{}:
259 +text = wire.text(got)
260 wire.read.got(method, acc, text, String.is_empty(text))
261
262# what to do after a read answered `got`, with `acc` received before it, for
263# a request with this method (SPEC.md HTTP-CLI-6)
264def wire.read.next(+method: String, acc: String, +got: String) -> Read:
265 wire.read.of(method, acc, got, wire.ok(got))
266
267# the answer when the reads run out before the response ends
268def wire.spent() -> String:
269 "56\nthe answer did not end within 65536 reads"