src/lsp/frame.bend
bolt@1.12.0.0 · 354 lines · 0 definitions
1# lsp/frame: LSP's base protocol, purely: `Content-Length: N\r\n\r\n` and then
2# N bytes of UTF-8. Framing counts bytes and a read may end inside a char, so
3# the transport reads bytes, cuts on bytes, and only then decodes.
4import Base
5
6# UTF-8, bytes to chars
7# ---------------------
8
9# the decoder's state: continuation bytes still owed, the code point so far,
10# the chars so far (reversed)
11type Dec is Data:
12 Dec{need: Nat, acc: U32, out: List<&2, Char>}
13
14# a lead byte, by its high nibble; a stray continuation byte stands for itself
15def decode.lead(hi: U32, +bb: U32, out: List<&2, Char>) -> Dec:
16 match hi:
17 case 12:
18 Dec{1n, (bb .&. 31 : U32), out}
19 case 13:
20 Dec{1n, (bb .&. 31 : U32), out}
21 case 14:
22 Dec{2n, (bb .&. 15 : U32), out}
23 case 15:
24 Dec{3n, (bb .&. 7 : U32), out}
25 case other:
26 Dec{0n, 0, Char.from_u32(bb) <> out}
27
28def decode.more(left: Nat, +acc: U32, out: List<&2, Char>) -> Dec:
29 match left:
30 case 0n:
31 Dec{0n, 0, Char.from_u32(acc) <> out}
32 case 1n+p:
33 Dec{1n+p, acc, out}
34
35def decode.step(+bb: U32, st: Dec) -> Dec:
36 Dec{need, acc, out} = st
37 match need:
38 case 0n:
39 decode.lead((bb >> 4n : U32), bb, out)
40 case 1n+p:
41 decode.more(p, ((acc << 6n) .|. (bb .&. 63) : U32), out)
42
43def decode.run(bs: List<&2, U32>, st: Dec) -> Dec:
44 match bs:
45 case Nil{}:
46 st
47 case Con{b, t}:
48 decode.run(t, decode.step(b, st))
49
50def decode.end(st: Dec) -> String:
51 Dec{need, acc, out} = st
52 String.from_list(List.reverse(&2, Char, out))
53
54# UTF-8 bytes as a string (a bad byte is skipped)
55def decode(bs: List<&2, U32>) -> String:
56 decode.end(decode.run(bs, Dec{0n, 0, []}))
57
58# UTF-8, chars to bytes
59# ---------------------
60
61# how many bytes a code point takes
62def width(+xx: U32) -> U32:
63 Bool.pick(U32, U32.is_lt(xx, 128), 1,
64 Bool.pick(U32, U32.is_lt(xx, 2048), 2,
65 Bool.pick(U32, U32.is_lt(xx, 65536), 3, 4)))
66
67# a code point's bytes, by its width, in front of the rest
68def encode.char(ww: U32, +xx: U32, rest: List<&2, U32>) -> List<&2, U32>:
69 match ww:
70 case 1:
71 xx <> rest
72 case 2:
73 (192 .|. (xx >> 6n) : U32) <> (128 .|. (xx .&. 63) : U32) <> rest
74 case 3:
75 (224 .|. (xx >> 12n) : U32) <> (128 .|. ((xx >> 6n) .&. 63) : U32) <> (128 .|. (xx .&. 63) : U32) <> rest
76 case other:
77 (240 .|. (xx >> 18n) : U32) <> (128 .|. ((xx >> 12n) .&. 63) : U32) <> (128 .|. ((xx >> 6n) .&. 63) : U32)
78 <> (128 .|. (xx .&. 63) : U32) <> rest
79
80def encode.one(+xx: U32, rest: List<&2, U32>) -> List<&2, U32>:
81 encode.char(width(xx), xx, rest)
82
83def encode.go(cs: List<&2, Char>) -> List<&2, U32>:
84 match cs:
85 case Nil{}:
86 Nil{}
87 case Con{c, t}:
88 encode.one(Char.to_u32(c), encode.go(t))
89
90# a string as UTF-8 bytes
91def encode(ss: String) -> List<&2, U32>:
92 encode.go(String.to_list(ss))
93
94# counts in decimal
95# -----------------
96
97# Content-Length is a count in decimal. It is kept as its digits, least
98# significant first, from writing it to reading it back: neither side goes
99# through a U32, whose text round trip would need laws of division by ten on
100# 32-bit words, and no length wraps at 2^32 or unfolds into a Nat of its size.
101
102# a decimal digit
103type Digit is Data:
104 D0{}
105 D1{}
106 D2{}
107 D3{}
108 D4{}
109 D5{}
110 D6{}
111 D7{}
112 D8{}
113 D9{}
114
115# a digit's char code, '0' to '9'
116def digit.code(dd: Digit) -> U32:
117 match dd:
118 case D0{}:
119 48
120 case D1{}:
121 49
122 case D2{}:
123 50
124 case D3{}:
125 51
126 case D4{}:
127 52
128 case D5{}:
129 53
130 case D6{}:
131 54
132 case D7{}:
133 55
134 case D8{}:
135 56
136 case D9{}:
137 57
138
139# the digit a char code stands for, if it is one
140def digit.read(xx: U32) -> Maybe<&2, Digit>:
141 match xx:
142 case 48:
143 Some{D0{}}
144 case 49:
145 Some{D1{}}
146 case 50:
147 Some{D2{}}
148 case 51:
149 Some{D3{}}
150 case 52:
151 Some{D4{}}
152 case 53:
153 Some{D5{}}
154 case 54:
155 Some{D6{}}
156 case 55:
157 Some{D7{}}
158 case 56:
159 Some{D8{}}
160 case 57:
161 Some{D9{}}
162 case other:
163 None{}
164
165# a count one more (digits least significant first)
166def tick(ds: List<&2, Digit>) -> List<&2, Digit>:
167 match ds:
168 case Nil{}:
169 [D1{}]
170 case Con{D0{}, t}:
171 D1{} <> t
172 case Con{D1{}, t}:
173 D2{} <> t
174 case Con{D2{}, t}:
175 D3{} <> t
176 case Con{D3{}, t}:
177 D4{} <> t
178 case Con{D4{}, t}:
179 D5{} <> t
180 case Con{D5{}, t}:
181 D6{} <> t
182 case Con{D6{}, t}:
183 D7{} <> t
184 case Con{D7{}, t}:
185 D8{} <> t
186 case Con{D8{}, t}:
187 D9{} <> t
188 case Con{D9{}, t}:
189 D0{} <> tick(t)
190
191# a count plus a char's width in bytes
192def tick.by(ww: U32, ds: List<&2, Digit>) -> List<&2, Digit>:
193 match ww:
194 case 1:
195 tick(ds)
196 case 2:
197 tick(tick(ds))
198 case 3:
199 tick(tick(tick(ds)))
200 case other:
201 tick(tick(tick(tick(ds))))
202
203# how many UTF-8 bytes the chars take, counted on from ds
204def byte_count(cs: List<&2, Char>, ds: List<&2, Digit>) -> List<&2, Digit>:
205 match cs:
206 case Nil{}:
207 ds
208 case Con{c, t}:
209 byte_count(t, tick.by(width(Char.to_u32(c)), ds))
210
211# a count's digits, most significant first, in front of acc
212def count.show(ds: List<&2, Digit>, acc: String) -> String:
213 match ds:
214 case Nil{}:
215 acc
216 case Con{d, t}:
217 count.show(t, SCon{Char.from_u32(digit.code(d)), acc})
218
219# is the count zero?
220def count.zero(ds: List<&2, Digit>) -> Bool:
221 match ds:
222 case Nil{}:
223 True{}
224 case Con{D0{}, t}:
225 count.zero(t)
226 case Con{d, t}:
227 False{}
228
229# a count one less (zero stays zero)
230def untick(ds: List<&2, Digit>) -> List<&2, Digit>:
231 match ds:
232 case Nil{}:
233 Nil{}
234 case Con{D0{}, t}:
235 D9{} <> untick(t)
236 case Con{D1{}, t}:
237 D0{} <> t
238 case Con{D2{}, t}:
239 D1{} <> t
240 case Con{D3{}, t}:
241 D2{} <> t
242 case Con{D4{}, t}:
243 D3{} <> t
244 case Con{D5{}, t}:
245 D4{} <> t
246 case Con{D6{}, t}:
247 D5{} <> t
248 case Con{D7{}, t}:
249 D6{} <> t
250 case Con{D8{}, t}:
251 D7{} <> t
252 case Con{D9{}, t}:
253 D8{} <> t
254
255# one more char's digit onto the count read so far; None once one is no digit
256def count.push(md: Maybe<&2, Digit>, acc: Maybe<&2, List<&2, Digit>>) -> Maybe<&2, List<&2, Digit>>:
257 match md acc:
258 case Some{d} Some{ds}:
259 Some{d <> ds}
260 case None{} _:
261 None{}
262 case Some{d} None{}:
263 None{}
264
265def count.read.go(ss: String, acc: Maybe<&2, List<&2, Digit>>) -> Maybe<&2, List<&2, Digit>>:
266 match ss:
267 case SNil{}:
268 acc
269 case SCon{c, t}:
270 count.read.go(t, count.push(digit.read(Char.to_u32(c)), acc))
271
272# a string of digits as a count; None when it is empty or holds anything else
273def count.read(ss: String) -> Maybe<&2, List<&2, Digit>>:
274 match ss:
275 case SNil{}:
276 None{}
277 case SCon{h, t}:
278 count.read.go(SCon{h, t}, Some{[]})
279
280# framing
281# -------
282
283# a message on its way out
284def wrap(+body: String) -> String:
285 "Content-Length: " ++ count.show(byte_count(String.to_list(body), [D0{}]), "") ++ "\r\n\r\n" ++ body
286
287# the header block's Content-Length and the bytes after it, once it is whole
288type Head is Data:
289 NoHead{}
290 Head{len: List<&2, Digit>, rest: List<&2, U32>}
291
292# the front of a buffer: a whole body and the bytes after it, or not yet
293type Cut is Data:
294 More{}
295 Ready{body: List<&2, U32>, rest: List<&2, U32>}
296
297# bytes as chars, one each (for the ASCII header)
298def chars(bs: List<&2, U32>, acc: List<&2, Char>) -> List<&2, Char>:
299 match bs:
300 case Nil{}:
301 acc
302 case Con{b, t}:
303 chars(t, Char.from_u32(b) <> acc)
304
305# a header line (reversed, its \r already dropped) updates the length
306def line_len(line: List<&2, U32>, +len: List<&2, Digit>) -> List<&2, Digit>:
307 +s = String.from_list(chars(line, []))
308 +read = count.read(String.drop(s, 16n))
309 Bool.pick(List<&2, Digit>, String.starts_with(s, "Content-Length: "), Maybe.default(&2, List<&2, Digit>, read, len), len)
310
311# the header block read up to its blank line: Content-Length, and the bytes
312# after; not whole yet when the blank line has not come
313def header(bs: List<&2, U32>, line: List<&2, U32>, len: List<&2, Digit>) -> Head:
314 match bs line:
315 case Nil{} l:
316 NoHead{}
317 case Con{10, t} Nil{}:
318 Head{len, t}
319 case Con{10, t} l:
320 header(t, [], line_len(l, len))
321 case Con{13, t} l:
322 header(t, l, len)
323 case Con{c, t} l:
324 header(t, c <> l, len)
325
326# the bytes taken so far and the rest once the count is down to zero, else
327# what more gives
328def split.on(zz: Bool, xs: List<&2, U32>, acc: List<&2, U32>, more: Unit -> Cut) -> Cut:
329 match zz:
330 case True{}:
331 Ready{List.reverse(&2, U32, acc), xs}
332 case False{}:
333 more(Unit{})
334
335# the first ds bytes (reversed onto acc) and the rest, or not yet when there
336# are fewer. The count goes down a digit at a time: never a Nat of its size
337def split(xs: List<&2, U32>, +ds: List<&2, Digit>, +acc: List<&2, U32>) -> Cut:
338 match xs:
339 case Nil{}:
340 split.on(count.zero(ds), [], acc, _u => More{})
341 case Con{+h, +t}:
342 split.on(count.zero(ds), h <> t, acc, _u => split(t, untick(ds), h <> acc))
343
344def cut.body(hh: Head) -> Cut:
345 match hh:
346 case NoHead{}:
347 More{}
348 case Head{len, rest}:
349 split(rest, len, [])
350
351# the front of a buffer: a whole message body and the bytes after it, or
352# not yet
353def cut(buf: List<&2, U32>) -> Cut:
354 cut.body(header(buf, [], [D0{}]))