diff options
| author | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-12 18:27:44 -0300 |
|---|---|---|
| committer | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-12 18:27:44 -0300 |
| commit | 27e9ddee53b8fa43725f951434404691d8012190 (patch) | |
| tree | ea78559da973d4628cf135096488d55c7b7cd35e /bin | |
| parent | 257f5288a486740187e44b6ef4cadaad7166930e (diff) | |
| download | SOL-27e9ddee53b8fa43725f951434404691d8012190.tar.gz SOL-27e9ddee53b8fa43725f951434404691d8012190.zip | |
language server over stdio, emacs mode with repl and eglot wiring
Diffstat (limited to 'bin')
| -rw-r--r-- | bin/dune | 3 | ||||
| -rw-r--r-- | bin/lsp.ml | 166 | ||||
| -rw-r--r-- | bin/main.ml | 4 |
3 files changed, 171 insertions, 2 deletions
@@ -1,4 +1,5 @@ (executable (name main) (public_name sol) - (libraries sol)) + (modules main lsp) + (libraries sol yojson)) diff --git a/bin/lsp.ml b/bin/lsp.ml new file mode 100644 index 0000000..bfe2573 --- /dev/null +++ b/bin/lsp.ml @@ -0,0 +1,166 @@ +(* 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. *) + +let log_json json = Yojson.Safe.to_string json + +let send json = + let body = log_json 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 + +(* 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 } -> + [ (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 -> ( + (* didChange, full sync: the last full content change. *) + 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 -> publish uri text | _ -> () + +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 + match to_string_opt (member "method" message) with + | Some "initialize" -> + respond id + (`Assoc + [ + ( "capabilities", + `Assoc [ ("textDocumentSync", `Int 1) ] ); + ( "serverInfo", + `Assoc + [ + ("name", `String "sol-lsp"); ("version", `String "0.1.0"); + ] ); + ]) + | Some "shutdown" -> respond id `Null + | Some "exit" -> running := false + | Some ("textDocument/didOpen" | "textDocument/didChange") -> + check_notification params + | Some "textDocument/didClose" -> ( + match to_string_opt (member "uri" (member "textDocument" params)) with + | Some uri -> + send + (`Assoc + [ + ("jsonrpc", `String "2.0"); + ("method", `String "textDocument/publishDiagnostics"); + ( "params", + `Assoc + [ ("uri", `String uri); ("diagnostics", `List []) ] ); + ]) + | None -> ()) + | Some _ when id <> `Null -> + (* An unsupported request deserves an answer, not silence. *) + send + (`Assoc + [ + ("jsonrpc", `String "2.0"); + ("id", id); + ( "error", + `Assoc + [ + ("code", `Int (-32601)); + ("message", `String "method not found"); + ] ); + ]) + | _ -> ()) + done diff --git a/bin/main.ml b/bin/main.ml index c5c329a..eb212d2 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -48,6 +48,7 @@ let repl () = print_endline "Sol. Statements accumulate; Query expression: ... runs."; let rec loop history = print_string "sol> "; + flush stdout; match In_channel.input_line stdin with | None -> () | Some line when String.trim line = "" -> loop history @@ -73,7 +74,8 @@ let repl () = let () = match Sys.argv with | [| _ |] -> repl () + | [| _; "lsp" |] -> Lsp.run () | [| _; path |] -> run_file path | _ -> - prerr_endline "usage: sol [file.sol]"; + prerr_endline "usage: sol [file.sol | lsp]"; exit 1 |
