src/lsp/proto.bend
bolt@1.17.0.0 · 318 lines · 0 definitions
1# lsp/proto: the messages the server sends, and the little it reads of a URI.
2import Base
3import emerging-ezjson@1.1.0.0/main.bend as Ezjson
4import emerging-ezjson@1.1.0.0/src/value.bend as J
5import bolt@1.17.0.0/src/lsp/frame.bend as Frame
6import bolt@1.17.0.0/src/lsp/report.bend as Rep
7import bolt@1.17.0.0/src/syntax/outline.bend as Outline
8import bolt@1.17.0.0/src/syntax/bind.bend as Bind
9import bolt@1.17.0.0/src/lsp/semantic.bend as Semantic
10import bolt@1.17.0.0/src/finding.bend as Lint
11import bolt@1.17.0.0/src/codes.bend as Codes
12import bolt@1.17.0.0/src/config.bend as Config
13import bolt@1.17.0.0/src/version.bend as Ver
14import bolt@1.17.0.0/src/lsp/enc.bend as Enc
15
16# strings as JSON strings
17def strings(ss: List<&2, String>) -> List<&2, J.Json>:
18 match ss:
19 case Nil{}:
20 Nil{}
21 case Con{h, t}:
22 J.JStr{h} <> strings(t)
23
24# a reply to a request
25def response(id: J.Json, result: J.Json) -> J.Json:
26 Ezjson.obj([("jsonrpc", J.JStr{"2.0"}), ("id", id), ("result", result)])
27
28# a refusal of a request, with LSP's error code and a message
29def failure(id: J.Json, code: String, message: String) -> J.Json:
30 Ezjson.obj([("jsonrpc", J.JStr{"2.0"}), ("id", id),
31 ("error", Ezjson.obj([("code", J.JNum{code}), ("message", J.JStr{message})]))])
32
33# a notification: no id, no reply expected
34def notify(method: String, params: J.Json) -> J.Json:
35 Ezjson.obj([("jsonrpc", J.JStr{"2.0"}), ("method", J.JStr{method}), ("params", params)])
36
37# what the server can do. It takes whole-text edits (change: 1) for hover,
38# definition and symbols; diagnostics still follow open and save, as the
39# checker reads files and their imports from disk
40def capabilities(ee: Enc.Enc) -> J.Json:
41 Ezjson.obj([
42 ("capabilities", Ezjson.obj([
43 ("positionEncoding", J.JStr{Enc.name(ee)}),
44 ("textDocumentSync", Ezjson.obj([("openClose", J.JBool{True{}}), ("change", J.JNum{U32.show(1)}), ("save", J.JBool{True{}})])),
45 ("hoverProvider", J.JBool{True{}}),
46 ("definitionProvider", J.JBool{True{}}),
47 ("documentSymbolProvider", J.JBool{True{}}),
48 ("completionProvider", Ezjson.obj([("triggerCharacters", Ezjson.arr([J.JStr{"."}]))])),
49 ("referencesProvider", J.JBool{True{}}),
50 ("renameProvider", J.JBool{True{}}),
51 ("semanticTokensProvider", Ezjson.obj([
52 ("legend", Ezjson.obj([("tokenTypes", Ezjson.arr(strings(Semantic.legend()))), ("tokenModifiers", Ezjson.arr([]))])),
53 ("full", J.JBool{True{}})]))])),
54 ("serverInfo", Ezjson.obj([("name", J.JStr{"bolt"}), ("version", J.JStr{Ver.text()})]))])
55
56# an LSP position as sent: a line and a character already in the negotiated
57# encoding
58def position.at(line: U32, character: U32) -> J.Json:
59 Ezjson.obj([("line", J.JNum{U32.show(line)}), ("character", J.JNum{U32.show(character)})])
60
61# an LSP position (0-based line and a code-point character), its character
62# sent in the document's negotiated encoding
63def position(cc: Enc.Cols, +line: U32, character: U32) -> J.Json:
64 position.at(line, Enc.out(cc, line, character))
65
66# the checker gives a line and no columns: a diagnostic covers its whole line
67def diagnostic(+cc: Enc.Cols, dd: Rep.Diag) -> J.Json:
68 Rep.Diag{+line, msg} = dd
69 Ezjson.obj([
70 ("range", Ezjson.obj([("start", position(cc, line, 0)), ("end", position(cc, (line + 1 : U32), 0))])),
71 ("severity", J.JNum{U32.show(1)}), ("source", J.JStr{"bend"}), ("message", J.JStr{msg})])
72
73# diagnostics as JSON
74def diagnostics(ds: List<&2, Rep.Diag>, +cc: Enc.Cols) -> List<&2, J.Json>:
75 match ds:
76 case Nil{}:
77 Nil{}
78 case Con{d, t}:
79 diagnostic(cc, d) <> diagnostics(t, cc)
80
81# a finding's range: its name, or from its column to the end of the line
82def finding_range(+cc: Enc.Cols, +line: U32, +col: U32, +len: U32) -> J.Json:
83 Ezjson.obj([("start", position(cc, line, col)),
84 ("end", Bool.pick(J.Json, U32.is_eq(len, 0), position(cc, (line + 1 : U32), 0),
85 position(cc, line, (col + len : U32))))])
86
87# a graded lint finding as a diagnostic: an error or a warning by its level,
88# its stable code, and bolt(group:slug) as the source
89def finding(cc: Enc.Cols, gg: Lint.Graded) -> J.Json:
90 Lint.Graded{level, Lint.Finding{path, line, col, len, +rule, msg}} = gg
91 Ezjson.obj([("range", finding_range(cc, line, col, len)),
92 ("severity", J.JNum{U32.show(Bool.pick(U32, Config.is_error(level), 1, 2))}),
93 ("code", J.JStr{Codes.code(rule)}), ("source", J.JStr{Codes.source(rule)}), ("message", J.JStr{msg})])
94
95# findings as JSON
96def findings(gs: List<&2, Lint.Graded>, +cc: Enc.Cols) -> List<&2, J.Json>:
97 match gs:
98 case Nil{}:
99 Nil{}
100 case Con{g, t}:
101 finding(cc, g) <> findings(t, cc)
102
103# the publishDiagnostics notification for a document: the checker's errors,
104# then the linter's findings
105def publish(+cc: Enc.Cols, uri: String, ds: List<&2, Rep.Diag>, gs: List<&2, Lint.Graded>) -> J.Json:
106 notify("textDocument/publishDiagnostics",
107 Ezjson.obj([("uri", J.JStr{uri}), ("diagnostics", Ezjson.arr(List.append(&2, J.Json, diagnostics(ds, cc), findings(gs, cc))))]))
108
109# a whole line as a range
110def line_range(+cc: Enc.Cols, +line: U32) -> J.Json:
111 Ezjson.obj([("start", position(cc, line, 0)), ("end", position(cc, (line + 1 : U32), 0))])
112
113# an item as hover text: its signature as code, then its doc comment
114def hover.text(sig: String, +doc: String) -> String:
115 "```bend\n" ++ sig ++ "\n```" ++ Bool.pick(String, String.is_empty(doc), "", "\n\n" ++ doc)
116
117# an item as hover: signature, then doc
118def hover(item: Outline.Item) -> J.Json:
119 Outline.Item{k, name, line, sig, doc, path} = item
120 Ezjson.obj([("contents", Ezjson.obj([("kind", J.JStr{"markdown"}), ("value", J.JStr{hover.text(sig, doc)})]))])
121
122# an item's location: its whole line
123def location(cc: Enc.Cols, uri: String, item: Outline.Item) -> J.Json:
124 Outline.Item{k, name, line, sig, doc, path} = item
125 Ezjson.obj([("uri", J.JStr{uri}), ("range", line_range(cc, line))])
126
127# what a binder is, in words
128def kind_name(kk: Bind.BindKind) -> String:
129 match kk:
130 case Bind.KItem{}:
131 "item"
132 case Bind.KCtor{}:
133 "constructor"
134 case Bind.KParam{}:
135 "parameter"
136 case Bind.KTypeParam{}:
137 "type parameter"
138 case Bind.KField{}:
139 "field"
140 case Bind.KLocal{}:
141 "local"
142 case Bind.KPat{}:
143 "local"
144 case Bind.KFor{}:
145 "local"
146 case Bind.KTypeVar{}:
147 "type variable"
148
149# where a local was bound, for hover
150def where_bound(kk: Bind.BindKind, line: U32) -> String:
151 match kk:
152 case Bind.KLocal{}:
153 ", bound on line " ++ U32.show((line + 1 : U32))
154 case Bind.KPat{}:
155 ", bound on line " ++ U32.show((line + 1 : U32))
156 case Bind.KFor{}:
157 ", bound on line " ++ U32.show((line + 1 : U32))
158 case other:
159 ""
160
161# a binder of the document: the text that bound it, and what it is. The
162# server knows binding sites, not types: only a declaration carries one
163def hover.local(bb: Bind.Bind) -> J.Json:
164 Bind.Bind{name, line, col, +kind, note} = bb
165 Ezjson.obj([("contents", Ezjson.obj([("kind", J.JStr{"markdown"}), ("value", J.JStr{"```bend\n" ++ note ++ "\n```\n\n" ++
166 kind_name(kind) ++ where_bound(kind, line)})]))])
167
168# exactly a name's range
169def name_range(+cc: Enc.Cols, +line: U32, +col: U32, name: String) -> J.Json:
170 Ezjson.obj([("start", position(cc, line, col)),
171 ("end", position(cc, line, (col + U32.from_nat(String.length(name)) : U32)))])
172
173# exactly the binder's name
174def location.local(cc: Enc.Cols, uri: String, bb: Bind.Bind) -> J.Json:
175 Bind.Bind{name, line, col, kind, note} = bb
176 Ezjson.obj([("uri", J.JStr{uri}), ("range", name_range(cc, line, col, name))])
177
178# LSP's SymbolKind: module 2, function 12, constant 14, enum member 22, struct 23
179def symbol.kind(kk: Outline.ItemKind) -> U32:
180 match kk:
181 case Outline.IImport{}:
182 2
183 case Outline.IDef{}:
184 12
185 case Outline.ILaw{}:
186 14
187 case Outline.IType{}:
188 23
189 case Outline.ICtor{}:
190 22
191 case Outline.ILocal{}:
192 13
193
194# an item as a DocumentSymbol
195def symbol(+cc: Enc.Cols, item: Outline.Item) -> J.Json:
196 Outline.Item{k, name, +line, sig, doc, path} = item
197 Ezjson.obj([("name", J.JStr{name}), ("kind", J.JNum{U32.show(symbol.kind(k))}),
198 ("range", line_range(cc, line)), ("selectionRange", line_range(cc, line))])
199
200def symbols.go(items: List<&2, Outline.Item>, +cc: Enc.Cols) -> List<&2, J.Json>:
201 match items:
202 case Nil{}:
203 Nil{}
204 case Con{item, t}:
205 symbol(cc, item) <> symbols.go(t, cc)
206
207# the document symbols
208def symbols(cc: Enc.Cols, items: List<&2, Outline.Item>) -> J.Json:
209 Ezjson.arr(symbols.go(items, cc))
210
211# LSP's CompletionItemKind: function 3, module 9, enum member 20, constant 21,
212# struct 22
213def completion.kind(kk: Outline.ItemKind) -> U32:
214 match kk:
215 case Outline.IImport{}:
216 9
217 case Outline.IDef{}:
218 3
219 case Outline.ILaw{}:
220 21
221 case Outline.IType{}:
222 22
223 case Outline.ICtor{}:
224 20
225 case Outline.ILocal{}:
226 6
227
228# a text's first line
229def first_line(s2: String) -> String:
230 Maybe.default(&2, String, List.head(&2, String, String.lines(s2)), "")
231
232# a candidate replaces everything typed of the name, dots included: the
233# editor's own idea of a word stops at a dot
234def completion(+cc: Enc.Cols, item: Outline.Item, +line: U32, start: U32, col: U32) -> J.Json:
235 Outline.Item{k, +name, l, sig, doc, path} = item
236 Ezjson.obj([("label", J.JStr{name}), ("kind", J.JNum{U32.show(completion.kind(k))}), ("detail", J.JStr{first_line(sig)}),
237 ("documentation", Ezjson.obj([("kind", J.JStr{"markdown"}), ("value", J.JStr{doc})])),
238 ("filterText", J.JStr{name}),
239 ("textEdit", Ezjson.obj([("range", Ezjson.obj([("start", position(cc, line, start)), ("end", position(cc, line, col))])),
240 ("newText", J.JStr{name})]))])
241
242def completions.go(
243 items: List<&2, Outline.Item>,
244 +cc: Enc.Cols,
245 +line: U32,
246 +start: U32,
247 +col: U32
248) -> List<&2, J.Json>:
249 match items:
250 case Nil{}:
251 Nil{}
252 case Con{item, t}:
253 completion(cc, item, line, start, col) <> completions.go(t, cc, line, start, col)
254
255# isIncomplete: the server filtered by the prefix, so the editor asks again
256# as the prefix grows
257def completions(cc: Enc.Cols, items: List<&2, Outline.Item>, line: U32, start: U32, col: U32) -> J.Json:
258 Ezjson.obj([("isIncomplete", J.JBool{True{}}), ("items", Ezjson.arr(completions.go(items, cc, line, start, col)))])
259
260# a hex digit's value: 0-9, then a-f and A-F as 10-15
261def hex(ch: Char) -> U32:
262 +x = Char.to_u32(ch)
263 Bool.pick(U32, U32.is_le(x, 57), (x - 48 : U32),
264 Bool.pick(U32, U32.is_ge(x, 97), (x - 87 : U32), (x - 55 : U32)))
265
266# a file URI's path: the scheme dropped, the %XX bytes decoded as UTF-8
267def unpercent(cs: List<&2, Char>) -> List<&2, U32>:
268 match cs:
269 case Nil{}:
270 Nil{}
271 case Con{'%', Con{a, Con{b, t}}}:
272 +hi = hex(a)
273 +lo = hex(b)
274 (hi * 16 + lo : U32) <> unpercent(t)
275 case Con{c, t}:
276 Frame.encode.one(Char.to_u32(c), unpercent(t))
277
278# a file URI's path: the scheme dropped, the %XX bytes decoded as UTF-8
279def path(+uri: String) -> String:
280 Frame.decode(unpercent(String.to_list(
281 Bool.pick(String, String.starts_with(uri, "file://"), String.drop(uri, 7n), uri))))
282
283# references and rename
284# ---------------------
285
286def locations.go(ps: List<&2, Bind.Pos>, +cc: Enc.Cols, +uri: String, +name: String) -> List<&2, J.Json>:
287 match ps:
288 case Nil{}:
289 Nil{}
290 case Con{Bind.Pos{l, c}, rest}:
291 Ezjson.obj([("uri", J.JStr{uri}), ("range", name_range(cc, l, c, name))]) <> locations.go(rest, cc, uri, name)
292
293# the positions a name is at, as Locations
294def locations(cc: Enc.Cols, uri: String, name: String, ps: List<&2, Bind.Pos>) -> J.Json:
295 Ezjson.arr(locations.go(ps, cc, uri, name))
296
297def edits.go(ps: List<&2, Bind.Pos>, +cc: Enc.Cols, +name: String, +new: String) -> List<&2, J.Json>:
298 match ps:
299 case Nil{}:
300 Nil{}
301 case Con{Bind.Pos{l, c}, rest}:
302 Ezjson.obj([("range", name_range(cc, l, c, name)), ("newText", J.JStr{new})]) <> edits.go(rest, cc, name, new)
303
304# a WorkspaceEdit over the one document
305def rename(cc: Enc.Cols, uri: String, name: String, new: String, ps: List<&2, Bind.Pos>) -> J.Json:
306 Ezjson.obj([("changes", Ezjson.obj([(uri, Ezjson.arr(edits.go(ps, cc, name, new)))]))])
307
308# numbers as JSON numbers
309def nums(ns: List<&2, U32>) -> List<&2, J.Json>:
310 match ns:
311 case Nil{}:
312 Nil{}
313 case Con{h, t}:
314 J.JNum{U32.show(h)} <> nums(t)
315
316# the semantic tokens response
317def semantic(data: List<&2, U32>) -> J.Json:
318 Ezjson.obj([("data", Ezjson.arr(nums(data)))])