src/wirespec.bend
emerging-ezhttp@0.12.0.0 · 259 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.12.0.0/src/http.bend as Http
14import emerging-ezhttp@0.12.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 and request text the effect is given
137type Exchange is Data:
138 NoUrl{why: String}
139 Exchange{secure: Bool, host: String, port: U32, req: String}
140
141# the exchange once it is known whether the scheme wants TLS
142def wire.exchange.at(method: String, +secure: Bool, +host: String, +port: U32,
143 path: String, headers: List<&2, Http.Header>, body: String) -> Exchange:
144 Exchange{secure, host, port,
145 Http.request.at(method, secure, host, port, path, headers, body)}
146
147# a request with this method, headers and body to a URL that came apart
148def wire.exchange(method: String, l: Url.Loc, headers: List<&2, Http.Header>,
149 body: String) -> Exchange:
150 match l:
151 case Url.Bad{why}:
152 NoUrl{why}
153 case Url.Loc{scheme, host, port, path}:
154 +secure = String.eq(scheme, "https")
155 wire.exchange.at(method, secure, host, port, path, headers, body)
156
157# --- what is heard ---
158
159# an answer's status: the number on its first line, if it is one
160def wire.code.of(c: Http.Cut, raw: String) -> Maybe<&2, U32>:
161 match c:
162 case Http.NoCut{}:
163 U32.read(raw)
164 case Http.Cut{before, after}:
165 U32.read(before)
166
167# an answer's status line as a number
168def wire.code(+raw: String) -> Maybe<&2, U32>:
169 wire.code.of(Http.divide(raw, "\n"), raw)
170
171# the text after an answer's first newline
172def wire.text.of(c: Http.Cut) -> String:
173 match c:
174 case Http.NoCut{}:
175 ""
176 case Http.Cut{before, after}:
177 after
178
179# the text after an answer's first newline
180def wire.text(raw: String) -> String:
181 wire.text.of(Http.divide(raw, "\n"))
182
183# whether a status is success (0)
184def wire.ok.of(m: Maybe<&2, U32>) -> Bool:
185 match m:
186 case None{}:
187 False{}
188 case Some{n}:
189 U32.is_eq(n, 0)
190
191# whether an answer has status 0
192def wire.ok(raw: String) -> Bool:
193 wire.ok.of(wire.code(raw))
194
195# what an open answered: a connection to read from, or the answer itself
196type Opened is Data:
197 Refused{answer: String}
198 Open{conn: U32}
199
200# a connection number that read, or a malformed answer when it did not
201def wire.opened.conn(m: Maybe<&2, U32>) -> Opened:
202 match m:
203 case None{}:
204 Refused{"22\na malformed connection number"}
205 case Some{n}:
206 Open{n}
207
208# an open's answer once it is known whether it succeeded
209def wire.opened.of(+got: String, ok: Bool) -> Opened:
210 match ok:
211 case False{}:
212 Refused{got}
213 case True{}:
214 wire.opened.conn(U32.read(wire.text(got)))
215
216# what an open's answer means
217def wire.opened(+got: String) -> Opened:
218 wire.opened.of(got, wire.ok(got))
219
220# after a read: read again with what has arrived, or answer
221type Read is Data:
222 Again{acc: String}
223 Heard{answer: String}
224
225# everything received, once it is known whether it is a whole response
226def wire.read.whole(all: String, done: Bool) -> Read:
227 match done:
228 case True{}:
229 Heard{"0\n" ++ all}
230 case False{}:
231 Again{all}
232
233# a read that brought text, or found the connection closed
234def wire.read.got(+method: String, acc: String, text: String, closed: Bool)
235 -> Read:
236 match closed:
237 case True{}:
238 Heard{"0\n" ++ acc}
239 case False{}:
240 +all = acc ++ text
241 wire.read.whole(all, Http.whole(method, all))
242
243# a read's answer once it is known whether it succeeded
244def wire.read.of(+method: String, acc: String, +got: String, ok: Bool) -> Read:
245 match ok:
246 case False{}:
247 Heard{got}
248 case True{}:
249 +text = wire.text(got)
250 wire.read.got(method, acc, text, String.is_empty(text))
251
252# what to do after a read answered `got`, with `acc` received before it, for
253# a request with this method (SPEC.md HTTP-CLI-6)
254def wire.read.next(+method: String, acc: String, +got: String) -> Read:
255 wire.read.of(method, acc, got, wire.ok(got))
256
257# the answer when the reads run out before the response ends
258def wire.spent() -> String:
259 "56\nthe answer did not end within 65536 reads"