lsp gains hover, definition and completion from a text-level symbol scan

4 files changed, 364 insertions, 28 deletions

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
                 [
diff --git a/docs/tooling.org b/docs/tooling.org
index 7fb0e8c..e09917e 100644
--- a/docs/tooling.org
+++ b/docs/tooling.org
@@ -9,15 +9,31 @@ the checker the runtime runs.
 
 * The language server
 
-=sol lsp= speaks the Language Server Protocol over stdio. It has one
-capability, the load bearing one: diagnostics. On every open and
-every change the document goes through the same parse and the same
-admission the loader performs, so a recursive rule without a
-decrease witness, a fact violating its schema, an unknown relation
-or a failed membership criterion appears in the editor at typing
-time, with the same message the runtime would give. Parse errors
-carry line and column; admission errors anchor at the top of the
-file until the loader learns source locations.
+=sol lsp= speaks the Language Server Protocol over stdio. Four
+capabilities:
+
+- diagnostics :: on every open and change the document goes through
+  the same parse and the same admission the loader performs, so a
+  recursive rule without a decrease witness, a fact violating its
+  schema, an unknown relation or a failed membership criterion
+  appears in the editor at typing time, with the runtime's own
+  message. Parse errors carry line and column; admission errors
+  anchor at the top of the file until the loader learns source
+  locations.
+- hover :: a builtin shows its signature and operational meaning
+  (what solves backward, what residuates, what generates); a
+  declared relation shows its defining source lines, verbatim,
+  which is the honest notion of type in a language where types are
+  relations.
+- definition :: jumping from a use site to the Relation directive
+  or the rule heads that define the name.
+- completion :: declared relations, builtins and quantifier forms,
+  every label spelled in the document, directives, and the
+  combinators, triggered on =[=, =#= and =:=.
+
+Hover, definition and completion work from a per-line symbol scan of
+the stored text, deliberately not from the parsed program, so they
+keep working while the buffer is broken mid edit.
 
 The server is hand rolled JSON-RPC on yojson, in =bin/lsp.ml=. It
 answers =initialize=, tracks documents through full-content sync,
diff --git a/examples/#family.sol# b/examples/#family.sol#
new file mode 100644
index 0000000..200b0af
--- /dev/null
+++ b/examples/#family.sol#
@@ -0,0 +1,29 @@
+% Relations, facts, rules, joins and negation.
+
+Relation named: Person schema: #(
+  [name domain: String]
+  [age domain: Integer]
+)
+
+[Person name: "Marcos" age: 30]
+[Person name: "Ana" age: 12]
+[Person name: "Rui" age: 70]
+
+Rule name: "an adult is a person of age at least 18"
+     head: [Adult name: N]
+     body: [Person name: N age: A] :and
+           [GreaterEqual left: A right: 18]
+
+% Everyone stored.
+Query expression: [Person name: N age: A]
+
+% The rule, joined through the shared variable N.
+Query expression: [Adult name: N]
+
+% Decidable denial: people who are not adults.
+Query expression: ([Person name: N age: A]) :not [Adult name: N]
+
+% The specification's negation form, scoped by the universe.
+Query expression: [World] :not [Adult name: "Ana"]
+
+World
\ No newline at end of file
diff --git a/lib/builtin.mli b/lib/builtin.mli
index d7017e3..18d5f82 100644
--- a/lib/builtin.mli
+++ b/lib/builtin.mli
@@ -23,6 +23,9 @@ val is_builtin : string -> bool
 (** Whether a name is a builtin. The loader uses it for reference
     checking, so user relations cannot shadow builtins. *)
 
+val names : string list
+(** Every builtin relation name, for tooling (completion). *)
+
 val run : Pattern.Subst.t -> string -> Pattern.t Label.Map.t -> outcome option
 (** Executes one builtin goal under the substitution. [None] when
     the name is not a builtin, so the VM falls through to the