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.
4	import 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)
11	type 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
15	def 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	
28	def 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	
35	def 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	
43	def 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	
50	def 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)
55	def 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
62	def 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
68	def 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	
80	def encode.one(+xx: U32, rest: List<&2, U32>) -> List<&2, U32>:
81	  encode.char(width(xx), xx, rest)
82	
83	def 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
91	def 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
103	type 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'
116	def 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
140	def 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)
166	def 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
192	def 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
204	def 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
212	def 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?
220	def 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)
230	def 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
256	def 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	
265	def 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
273	def 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
284	def 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
288	type 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
293	type 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)
298	def 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
306	def 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
313	def 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
328	def 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
337	def 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	
344	def 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
353	def cut(buf: List<&2, U32>) -> Cut:
354	  cut.body(header(buf, [], [D0{}]))