src/wirespec.bend
emerging-ezhttp@0.11.0.0 · 127 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.
4#
5# Spec: scheme, host, port each on their own line; everything after the third
6# newline is the request verbatim. The scheme line may carry a timeout after a
7# space: 32 binary digits, least significant first, in milliseconds. A scheme
8# line with no timeout means 60000 ms. SPEC.md HTTP-CLI lists what is
9# guaranteed.
10import Base
11
12# the word the effect reads for a scheme that wants TLS
13def wire.scheme(secure: Bool) -> String:
14 match secure:
15 case True{}:
16 "tls"
17 case False{}:
18 "tcp"
19
20# the spec the effect reads
21def wire.spec(secure: Bool, host: String, port: U32, req: String) -> String:
22 wire.scheme(secure) ++ "\n" ++ host ++ "\n" ++ U32.show(port) ++ "\n" ++ req
23
24# --- the timeout ---
25
26# the timeout a spec with none carries: 60 s, in milliseconds
27def wire.ms.dflt() -> U32:
28 60000
29
30# one bit as a binary digit
31def wire.bit(b: Bool) -> Char:
32 match b:
33 case True{}:
34 '1'
35 case False{}:
36 '0'
37
38# a word as binary digits, least significant first
39def wire.bits(n: Nat, w: Word(n)) -> String:
40 match n:
41 case 0n:
42 SNil{}
43 case 1n+p:
44 match w:
45 case WCon{b, t}:
46 SCon{wire.bit(b), wire.bits(p, t)}
47
48# binary digits, least significant first, as a word; a missing digit is 0
49def wire.bits.read(n: Nat, s: String) -> Word(n):
50 match n:
51 case 0n:
52 WNil{}
53 case 1n+p:
54 match s:
55 case SNil{}:
56 WCon{False{}, wire.bits.read(p, SNil{})}
57 case SCon{c, t}:
58 WCon{Char.is_eq(c, '1'), wire.bits.read(p, t)}
59
60# a timeout as the scheme line carries it
61def wire.ms.text(ms: U32) -> String:
62 match ms:
63 case U32{w}:
64 wire.bits(32n, w)
65
66# the first line of a timed spec: the scheme, a space, the timeout
67def wire.head(secure: Bool, ms: U32) -> String:
68 wire.scheme(secure) ++ " " ++ wire.ms.text(ms)
69
70# the lines after the first: host, port, then the request verbatim
71def wire.rest(host: String, port: U32, req: String) -> String:
72 host ++ "\n" ++ U32.show(port) ++ "\n" ++ req
73
74# the spec the effect reads, with a timeout in milliseconds
75def wire.spec.timed(secure: Bool, ms: U32, host: String, port: U32,
76 req: String) -> String:
77 wire.head(secure, ms) ++ "\n" ++ wire.rest(host, port, req)
78
79# the timeout after the scheme word, or the default when there is none
80def wire.ms.words(ws: List<&2, String>) -> U32:
81 match ws:
82 case []:
83 wire.ms.dflt()
84 case _ <> []:
85 wire.ms.dflt()
86 case _ <> (bits <> _):
87 U32{wire.bits.read(32n, bits)}
88
89# the first line of a spec
90def wire.line(ls: List<&2, String>) -> String:
91 match ls:
92 case []:
93 ""
94 case l <> _:
95 l
96
97# the timeout the effect reads from a spec, in milliseconds
98def wire.ms(spec: String) -> U32:
99 wire.ms.words(String.split(wire.line(String.split(spec, '\n')), ' '))
100
101# --- the answer ---
102
103# the wire status for an exchange that ran out of time (curl's
104# CURLE_OPERATION_TIMEDOUT)
105def wire.late() -> U32:
106 28
107
108# what a failed exchange is reported as: a timeout is marked, any other
109# failure's reason is kept as it is
110def wire.why.of(why: String, late: Bool) -> String:
111 match late:
112 case True{}:
113 "timed out: " ++ why
114 case False{}:
115 why
116
117# a failed exchange's status and reason as the reason the client reports
118def wire.why(code: Maybe<&2, U32>, why: String) -> String:
119 match code:
120 case None{}:
121 why
122 case Some{n}:
123 wire.why.of(why, U32.is_eq(n, wire.late()))
124
125# whether a reported reason is a timeout
126def wire.timed_out(why: String) -> Bool:
127 String.starts_with(why, "timed out: ")