1	# lsp/proto: the messages the server sends, and the little it reads of a URI.
2	import Base
3	import 0x81c67699424929b5c44cd8577e18117f/main.bend as Ezjson
4	import 0x81c67699424929b5c44cd8577e18117f/src/value.bend as J
5	import ./frame.bend as Frame
6	import ./report.bend as Rep
7	import ../syntax/outline.bend as Outline
8	import ../syntax/bind.bend as Bind
9	import ./semantic.bend as Semantic
10	import ../finding.bend as Lint
11	import ../codes.bend as Codes
12	import ../config.bend as Config
13	import ../version.bend as Ver
14	import ./enc.bend as Enc
15	
16	# strings as JSON strings
17	def 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
25	def 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
29	def 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
34	def 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
40	def 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
58	def 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
63	def 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
67	def 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
74	def 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
82	def 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
89	def 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
96	def 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
105	def 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
110	def 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
114	def 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
118	def 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
123	def 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
128	def 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
150	def 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
163	def 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
169	def 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
174	def 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
179	def 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
195	def 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	
200	def 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
208	def 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
213	def 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
229	def 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
234	def 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	
242	def 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
257	def 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
261	def 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
267	def 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
279	def 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	
286	def 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
294	def 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	
297	def 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
305	def 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
309	def 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
317	def semantic(data: List<&2, U32>) -> J.Json:
318	  Ezjson.obj([("data", Ezjson.arr(nums(data)))])