From 19ba625e0345a88da6c29ab91a3ba2d7a8462065 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sun, 12 Jul 2026 18:43:23 -0300 Subject: lsp gains hover, definition and completion from a text-level symbol scan --- bin/lsp.ml | 326 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 307 insertions(+), 19 deletions(-) (limited to 'bin/lsp.ml') diff --git a/bin/lsp.ml b/bin/lsp.ml index bfe2573..f7529f2 100644 --- a/bin/lsp.ml +++ b/bin/lsp.ml @@ -1,15 +1,16 @@ (* The Sol language server: JSON-RPC over stdio, hand rolled on - yojson. One capability, the load-bearing one: diagnostics. Every - edit runs the same admission the runtime runs, so a rule with no - decrease witness or a fact violating its schema is an error in - the editor, at typing time, with the same message the loader - gives. Parse errors carry positions; admission errors anchor at - the top of the file until the loader learns locations. *) + yojson. -let log_json json = Yojson.Safe.to_string json + Diagnostics run the same admission the runtime runs, so a rule + with no decrease witness or a fact violating its schema is an + error in the editor with the runtime's own message. Completion, + hover, and definition work from a parse-level symbol scan of the + document text, so they keep working while the buffer is broken + mid-edit. Parse errors carry positions; admission errors anchor + at the top of the file until the loader learns locations. *) let send json = - let body = log_json json in + let body = Yojson.Safe.to_string json in Printf.printf "Content-Length: %d\r\n\r\n%s" (String.length body) body; flush stdout @@ -44,9 +45,167 @@ let member name json = | _ -> `Null let to_string_opt = function `String s -> Some s | _ -> None +let to_int_opt = function `Int i -> Some i | _ -> None + +(* ------------------------------------------------------------------ *) +(* Document store and symbol scan. *) +(* ------------------------------------------------------------------ *) + +type doc = { lines : string array } + +let documents : (string, doc) Hashtbl.t = Hashtbl.create 8 + +let store uri text = + Hashtbl.replace documents uri + { lines = Array.of_list (String.split_on_char '\n' text) } + +let is_ident_char c = + (c >= 'a' && c <= 'z') + || (c >= 'A' && c <= 'Z') + || (c >= '0' && c <= '9') + || c = '_' + +(* The identifier under the cursor; a leading # is part of it and + stripped, so hovering a reference reaches its relation. *) +let token_at doc ~line ~character = + if line < 0 || line >= Array.length doc.lines then None + else + let text = doc.lines.(line) in + let n = String.length text in + let i = min character (max 0 (n - 1)) in + if n = 0 then None + else + let i = if i < n && is_ident_char text.[i] then i else i - 1 in + if i < 0 || not (is_ident_char text.[i]) then None + else + let start = ref i and stop = ref i in + while !start > 0 && is_ident_char text.[!start - 1] do decr start done; + while !stop < n - 1 && is_ident_char text.[!stop + 1] do incr stop done; + Some (String.sub text !start (!stop - !start + 1)) + +(* Definition sites, scanned per line so they survive parse errors: + a relation is defined by its Relation directive or by the rules + whose head applies it. *) +let find_after text needle = + let tl = String.length text and nl = String.length needle in + let rec go i = + if i + nl > tl then None + else if String.sub text i nl = needle then Some (i + nl) + else go (i + 1) + in + go 0 + +let ident_at text i = + let n = String.length text in + let rec skip i = if i < n && text.[i] = ' ' then skip (i + 1) else i in + let start = skip i in + let stop = ref start in + while !stop < n && is_ident_char text.[!stop] do incr stop done; + if !stop > start then Some (String.sub text start (!stop - start), start) + else None + +let definitions doc name = + let hits = ref [] in + Array.iteri + (fun lineno text -> + let head_of needle = + match find_after text needle with + | Some i -> ident_at text i + | None -> None + in + let relation = head_of "Relation named:" in + let rule_head = + match find_after text "head:" with + | Some i -> ( + match find_after (String.sub text i (String.length text - i)) "[" with + | Some j -> ( + match ident_at text (i + j) with + | Some (n, col) -> Some (n, col) + | None -> None) + | None -> None) + | None -> None + in + List.iter + (function + | Some (n, col) when String.equal n name -> + hits := (lineno, col) :: !hits + | _ -> ()) + [ relation; rule_head ]) + doc.lines; + List.rev !hits + +(* Names available for completion: declared relations and rule + heads, every label spelled in the document, builtins, directives + and combinators. Harvested from text, so a broken buffer still + completes. *) +let harvest doc = + let relations = ref [] and labels = ref [] in + Array.iter + (fun text -> + let n = String.length text in + let i = ref 0 in + while !i < n do + if is_ident_char text.[!i] then begin + let start = !i in + while !i < n && is_ident_char text.[!i] do incr i done; + let word = String.sub text start (!i - start) in + if !i < n && text.[!i] = ':' then begin + if word.[0] >= 'a' && word.[0] <= 'z' then + labels := word :: !labels + end + else if + (word.[0] >= 'A' && word.[0] <= 'Z') + && start > 0 + && (text.[start - 1] = '[' || text.[start - 1] = '#') + then relations := word :: !relations + end + else if text.[!i] = '%' then i := n + else incr i + done) + doc.lines; + ( List.sort_uniq String.compare !relations + |> List.filter (fun name -> not (Sol.Builtin.is_builtin name)), + List.sort_uniq String.compare !labels ) + +(* ------------------------------------------------------------------ *) +(* What hover says. *) +(* ------------------------------------------------------------------ *) + +let builtin_hover = function + | "Integer" -> Some "[Integer value: T]\nmembership in the integers; checks once ground, residuates open" + | "Natural" -> Some "[Natural value: T]\nmembership in the naturals (an Integer at least 0)" + | "Rational" -> Some "[Rational value: T]\nmembership in the rationals; every Integer is one, literally" + | "String" -> Some "[String value: T]\nmembership in the strings" + | "Equal" -> Some "[Equal left: T right: T]\nunification" + | "Plus" -> Some "[Plus left: T right: T result: T]\naddition over the rationals; any two ground arguments determine the third" + | "Times" -> Some "[Times left: T right: T result: T]\nmultiplication over the rationals; solves backward except through zero" + | "LessThan" -> Some "[LessThan left: T right: T]\ndecides once both sides are ground; contributes interval bounds while open" + | "LessThanEqual" -> Some "[LessThanEqual left: T right: T]\ndecides once both sides are ground; contributes interval bounds while open" + | "GreaterThan" -> Some "[GreaterThan left: T right: T]\ndecides once both sides are ground; contributes interval bounds while open" + | "GreaterEqual" -> Some "[GreaterEqual left: T right: T]\ndecides once both sides are ground; contributes interval bounds while open" + | "Between" -> Some "[Between value: T lower: T upper: T]\nbounded generation: enumerates the finite integer range" + | "True" -> Some "[True]\nthe proposition that holds" + | "World" -> Some "[World]\nthe universe; true of every tuple, scopes denial: [World] :not [...]" + | "ForAll" -> Some "[ForAll variable: V quantifier: [...] body: [...]]\nuniversal: every quantifier solution satisfies the body; infinite domains discharge symbolically or reject" + | "Exists" -> Some "[Exists variable: V quantifier: [...] body: [...]]\nexistential: lowers to a conjunction with V renamed apart" + | "Insert" -> Some "[Insert relation: #R tuple: {...} before: S after: S']\ntransition relation between states (stateful worlds only)" + | _ -> None + +(* For a declared relation: its defining lines, verbatim. The + honest hover is the source of the definition. *) +let declared_hover doc name = + match definitions doc name with + | [] -> None + | sites -> + let lines = + List.map (fun (lineno, _) -> String.trim doc.lines.(lineno)) sites + in + Some (String.concat "\n" (List.sort_uniq String.compare lines)) + +(* ------------------------------------------------------------------ *) +(* Diagnostics. *) +(* ------------------------------------------------------------------ *) -(* Everything the checker can say about a document, as LSP - diagnostics: (line, column, message), zero-based lines. *) let diagnostics text = match Sol.Front.parse text with | Error { Sol.Front.line; column; message } -> @@ -91,14 +250,11 @@ let respond id result = send (`Assoc [ ("jsonrpc", `String "2.0"); ("id", id); ("result", result) ]) let check_notification params = - let uri = - to_string_opt (member "uri" (member "textDocument" params)) - in + let uri = to_string_opt (member "uri" (member "textDocument" params)) in let text = match to_string_opt (member "text" (member "textDocument" params)) with | Some text -> Some text | None -> ( - (* didChange, full sync: the last full content change. *) match member "contentChanges" params with | `List changes -> ( match List.rev changes with @@ -106,7 +262,121 @@ let check_notification params = | [] -> None) | _ -> None) in - match (uri, text) with Some uri, Some text -> publish uri text | _ -> () + match (uri, text) with + | Some uri, Some text -> + store uri text; + publish uri text + | _ -> () + +(* ------------------------------------------------------------------ *) +(* Requests. *) +(* ------------------------------------------------------------------ *) + +let position params = + let uri = to_string_opt (member "uri" (member "textDocument" params)) + and line = to_int_opt (member "line" (member "position" params)) + and character = to_int_opt (member "character" (member "position" params)) in + match (uri, line, character) with + | Some uri, Some line, Some character -> ( + match Hashtbl.find_opt documents uri with + | Some doc -> Some (uri, doc, line, character) + | None -> None) + | _ -> None + +let handle_hover params = + match position params with + | None -> `Null + | Some (_, doc, line, character) -> ( + match token_at doc ~line ~character with + | None -> `Null + | Some token -> ( + let text = + match builtin_hover token with + | Some text -> Some text + | None -> declared_hover doc token + in + match text with + | None -> `Null + | Some value -> + `Assoc + [ + ( "contents", + `Assoc + [ ("kind", `String "plaintext"); ("value", `String value) ] + ); + ])) + +let handle_definition uri params = + match position params with + | None -> `Null + | Some (_, doc, line, character) -> ( + match token_at doc ~line ~character with + | None -> `Null + | Some token -> + let locations = + List.map + (fun (lineno, col) -> + `Assoc + [ + ("uri", `String uri); + ( "range", + `Assoc + [ + ( "start", + `Assoc + [ ("line", `Int lineno); ("character", `Int col) ] + ); + ( "end", + `Assoc + [ + ("line", `Int lineno); + ( "character", + `Int (col + String.length token) ); + ] ); + ] ); + ]) + (definitions doc token) + in + `List locations) + +let directive_items = [ "Relation"; "Rule"; "Query" ] +let combinator_items = [ ":and"; ":or"; ":not" ] +let form_items = [ "ForAll"; "Exists" ] + +let handle_completion params = + match position params with + | None -> `Null + | Some (_, doc, _, _) -> + let relations, labels = harvest doc in + let item ?detail kind label = + `Assoc + (List.concat + [ + [ ("label", `String label); ("kind", `Int kind) ]; + (match detail with + | Some d -> [ ("detail", `String d) ] + | None -> []); + ]) + in + (* LSP completion kinds: 7 class, 5 field, 14 keyword, 3 + function. The client filters by prefix. *) + let items = + List.concat + [ + List.map (item 7 ~detail:"relation") relations; + List.map + (fun name -> item 3 ~detail:"builtin" name) + (Sol.Builtin.names @ form_items); + List.map (fun l -> item 5 ~detail:"label" (l ^ ":")) labels; + List.map (item 14 ~detail:"directive") directive_items; + List.map (item 14 ~detail:"combinator") combinator_items; + ] + in + `Assoc [ ("isIncomplete", `Bool false); ("items", `List items) ] + +(* ------------------------------------------------------------------ *) +(* The loop. *) +(* ------------------------------------------------------------------ *) let run () = set_binary_mode_in stdin true; @@ -118,17 +388,30 @@ let run () = | Some message -> ( let id = member "id" message in let params = member "params" message in + let uri = to_string_opt (member "uri" (member "textDocument" params)) in match to_string_opt (member "method" message) with | Some "initialize" -> respond id (`Assoc [ ( "capabilities", - `Assoc [ ("textDocumentSync", `Int 1) ] ); + `Assoc + [ + ("textDocumentSync", `Int 1); + ("hoverProvider", `Bool true); + ("definitionProvider", `Bool true); + ( "completionProvider", + `Assoc + [ + ( "triggerCharacters", + `List [ `String "["; `String "#"; `String ":" ] + ); + ] ); + ] ); ( "serverInfo", `Assoc [ - ("name", `String "sol-lsp"); ("version", `String "0.1.0"); + ("name", `String "sol-lsp"); ("version", `String "0.2.0"); ] ); ]) | Some "shutdown" -> respond id `Null @@ -136,8 +419,9 @@ let run () = | Some ("textDocument/didOpen" | "textDocument/didChange") -> check_notification params | Some "textDocument/didClose" -> ( - match to_string_opt (member "uri" (member "textDocument" params)) with + match uri with | Some uri -> + Hashtbl.remove documents uri; send (`Assoc [ @@ -148,8 +432,12 @@ let run () = [ ("uri", `String uri); ("diagnostics", `List []) ] ); ]) | None -> ()) + | Some "textDocument/hover" -> respond id (handle_hover params) + | Some "textDocument/definition" -> + respond id + (handle_definition (Option.value ~default:"" uri) params) + | Some "textDocument/completion" -> respond id (handle_completion params) | Some _ when id <> `Null -> - (* An unsupported request deserves an answer, not silence. *) send (`Assoc [ -- cgit v1.2.3