(* The Sol language server: JSON-RPC over stdio, hand rolled on
yojson.
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 = Yojson.Safe.to_string json in
Printf.printf "Content-Length: %d\r\n\r\n%s" (String.length body) body;
flush stdout
let read_message () =
let rec headers length =
match In_channel.input_line stdin with
| None -> None
| Some line -> (
let line = String.trim line in
if line = "" then length
else
match String.index_opt line ':' with
| Some i
when String.lowercase_ascii (String.sub line 0 i) = "content-length"
->
headers
(int_of_string_opt
(String.trim
(String.sub line (i + 1) (String.length line - i - 1))))
| _ -> headers length)
in
match headers None with
| None -> None
| Some length -> (
match really_input_string stdin length with
| body -> ( try Some (Yojson.Safe.from_string body) with _ -> None)
| exception End_of_file -> None)
let member name json =
match json with
| `Assoc fields -> Option.value ~default:`Null (List.assoc_opt name fields)
| _ -> `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. *)
(* ------------------------------------------------------------------ *)
let diagnostics text =
match Sol.Front.parse text with
| Error { Sol.Front.line; column; message } ->
[ (max 0 (line - 1), max 0 column, message) ]
| Ok statements -> (
match Sol.Program.load statements with
| Error error -> [ (0, 0, Format.asprintf "%a" Sol.Program.pp_error error) ]
| Ok _ -> [])
let publish uri text =
let items =
List.map
(fun (line, column, message) ->
`Assoc
[
( "range",
`Assoc
[
( "start",
`Assoc [ ("line", `Int line); ("character", `Int column) ]
);
( "end",
`Assoc
[ ("line", `Int line); ("character", `Int (column + 1)) ]
);
] );
("severity", `Int 1);
("source", `String "sol");
("message", `String message);
])
(diagnostics text)
in
send
(`Assoc
[
("jsonrpc", `String "2.0");
("method", `String "textDocument/publishDiagnostics");
("params", `Assoc [ ("uri", `String uri); ("diagnostics", `List items) ]);
])
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 text =
match to_string_opt (member "text" (member "textDocument" params)) with
| Some text -> Some text
| None -> (
match member "contentChanges" params with
| `List changes -> (
match List.rev changes with
| last :: _ -> to_string_opt (member "text" last)
| [] -> None)
| _ -> None)
in
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;
set_binary_mode_out stdout true;
let running = ref true in
while !running do
match read_message () with
| None -> running := false
| 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);
("hoverProvider", `Bool true);
("definitionProvider", `Bool true);
( "completionProvider",
`Assoc
[
( "triggerCharacters",
`List [ `String "["; `String "#"; `String ":" ]
);
] );
] );
( "serverInfo",
`Assoc
[
("name", `String "sol-lsp"); ("version", `String "0.2.0");
] );
])
| Some "shutdown" -> respond id `Null
| Some "exit" -> running := false
| Some ("textDocument/didOpen" | "textDocument/didChange") ->
check_notification params
| Some "textDocument/didClose" -> (
match uri with
| Some uri ->
Hashtbl.remove documents uri;
send
(`Assoc
[
("jsonrpc", `String "2.0");
("method", `String "textDocument/publishDiagnostics");
( "params",
`Assoc
[ ("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 ->
send
(`Assoc
[
("jsonrpc", `String "2.0");
("id", id);
( "error",
`Assoc
[
("code", `Int (-32601));
("message", `String "method not found");
] );
])
| _ -> ())
done
