Language Server Protocol proposal

dune-project

@@ -81,6 +81,21 @@ implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/de
 which allows clients, such as CoqIDE, to interact with Coq in a
 structured way."))
 
+(package
+ (name coqlsp-server)
+ (depends
+  (coq-core (= :version)))
+ (synopsis "The Coq Proof Assistant, Language Server Protocol server")
+ (description "Coq is a formal proof management system. It provides
+a formal language to write mathematical definitions, executable
+algorithms and theorems together with an environment for
+semi-interactive development of machine-checked proofs.
+
+This package provides the `coqlsptop` language server, an
+implementation of [Language Server Protocol](https://microsoft.github.io/language-server-protocol/)
+which allows clients, such as VSCoq, to interact with Coq in a
+structured way."))
+
 (package
  (name coqide)
  (depends

ide/lsp/dune

@@ -0,0 +1,14 @@
+; LSP Server
+
+(executable
+ (name lsptop)
+ (public_name coqlsptop.opt)
+ (package coqlsp-server)
+ (modes native byte)
+ (libraries coq-core.boot coq-core.lib coq-core.toplevel yojson))
+
+(install
+ (section bin)
+ (package coqlsp-server)
+ (files
+  (lsptop.bc as coqlsptop.byte)))

ide/lsp/json_helper.ml

@@ -0,0 +1,105 @@
+open Yojson.Basic
+open Yojson.Basic.Util
+
+let pmember (k: string) (r: t): t =
+  member "params" r |> member k
+
+let sub_from (str: string) (pos: int) : string =
+  String.sub str pos (String.length str - pos)
+
+(** UNIX paths: "file:///foo/bar" corresponds to /foo/bar
+    Windows paths: "file:///z%3A/foo" corresponds to z:/foo **)
+let uri_to_path u = if String.sub u 9 3 = "%3A" then
+                    Printf.sprintf "%s:%s" (String.sub u 8 1) (sub_from u 12)
+                    else sub_from u 7
+let path_to_uri u = if u.[1] = ':' then
+                      let s = sub_from u 2 in
+                      let rest = String.map (fun character -> if character == '\\' then '/' else character) s in
+                      "file:///" ^ (String.sub u 0 1) ^ "%3A" ^ rest
+                    else
+                      "file://" ^ u
+
+type completion_context = { trigger_kind: int; trigger_char: string option }
+let to_compl_context (j: t) : completion_context =
+  { trigger_kind = member "triggerKind" j |> to_int;
+    trigger_char =
+    match member "triggerChar" j |> to_string with
+    | character -> Some character
+    | exception _ -> None; }
+
+type txdoc_item = { fname: string; langId: string; version: int; text: string }
+let to_txdoc_item (j: t) : txdoc_item =
+  { fname = member "uri" j |> to_string |> uri_to_path;
+    langId = member "languageId" j |> to_string;
+    version = member "version" j |> to_int;
+    text = member "text" j |> to_string }
+
+type txdoc_pos = { path: string; line: int; col: int }
+
+(* Argument is of the form { "textDocument" : {"uri" : ... } } *)
+let to_txdoc_id (r: t) : string =
+  member "textDocument" r |> member "uri" |> to_string |> uri_to_path
+
+(* Argument is of the form { "textDocument" : ...,
+                             "position" : { "line" : ..., "character" : ... } } *)
+let to_txdoc_pos (r: t) : txdoc_pos =
+  let pos = pmember "position" r in
+  { path = to_txdoc_id r;
+    line = pos |> member "line" |> to_int;
+     col = pos |> member "character" |> to_int }
+
+type workspace_folder = { wk_uri: string; wk_name: string }
+type wsch_event = { added: workspace_folder; removed: workspace_folder }
+let to_wsch_event (j: t) : wsch_event =
+  { added = { wk_uri = member "added" j |> member "uri" |> to_string;
+              wk_name = member "added" j |> member "name" |> to_string };
+    removed = { wk_uri = member "removed" j |> member "uri" |> to_string;
+                wk_name = member "removed" j |> member "name" |> to_string } }
+
+let to_contentch (j: t) : string =
+  member "text" j |> to_string
+
+type position = { line: int; character: int }
+type range = { rng_start: position; rng_end: position }
+
+let server_capabilities : t =
+  `Assoc [("capabilities",
+              `Assoc [("textDocumentSync", `Assoc [
+                ("openClose", `Bool true);
+                ("change", `Int 1);
+                ("willSave", `Bool false);
+                ("willSaveWaitUntil", `Bool false);
+                ("save", `Assoc [("includeText", `Bool true)])]);
+              ("hoverProvider", `Bool true);
+              ("completionProvider", `Assoc []);
+              ("signatureHelpProvider", `Assoc []);
+              ("definitionProvider", `Bool true);
+              ("typeDefinitionProvider", `Bool false);
+              ("implementationProvider", `Bool false);
+              ("referencesProvider", `Bool false);
+              ("documentSymbolProvider", `Bool false);
+              ("workspaceSymbolProvider", `Bool false);
+              ("codeActionProvider", `Bool false)])]
+
+let from_position (p: position) : t = `Assoc [("line", `Int p.line);
+                                              ("character", `Int p.character)]
+
+let from_range (r: range) : t =
+  `Assoc [("start", from_position r.rng_start); ("end", from_position r.rng_end)]
+
+let dummyrange : t =
+  from_range { rng_start = { line = 0; character = 0; };
+               rng_end = { line = 0; character = 0; }; }
+
+let diag (fname: string) (msg: string) (r: range option) : t =
+  let r' = match r with
+           | Some r -> from_range r
+           | None -> dummyrange in
+  `Assoc [("method", `String "textDocument/publishDiagnostics");
+          ("params", `Assoc [("uri", `String (path_to_uri fname));
+                             ("diagnostics",
+                              `List [`Assoc [("range", r'); ("message", `String msg)]])])]
+
+let diag_clear (fname: string) : t =
+  `Assoc [("method", `String "textDocument/publishDiagnostics");
+          ("params", `Assoc [("uri", `String (path_to_uri fname)); ("diagnostics", `List [])])]

ide/lsp/json_helper.mli

@@ -0,0 +1,32 @@
+open Yojson.Basic
+
+val sub_from : string -> int -> string
+val pmember : string -> t -> t
+val uri_to_path : string -> string
+
+type completion_context = { trigger_kind: int; trigger_char: string option }
+val to_compl_context : t -> completion_context
+
+type txdoc_item = { fname: string; langId: string; version: int; text: string }
+val to_txdoc_item : t -> txdoc_item
+
+type txdoc_pos = { path: string; line: int; col: int }
+val to_txdoc_id : t -> string
+val to_txdoc_pos : t -> txdoc_pos
+
+type workspace_folder = { wk_uri: string; wk_name: string }
+type wsch_event = { added: workspace_folder; removed: workspace_folder }
+val to_wsch_event : t -> wsch_event
+val to_contentch : t -> string
+
+(* Report on server capabilities *)
+val server_capabilities : t
+
+type position = { line: int; character: int }
+type range = { rng_start: position; rng_end: position }
+
+(* Build a JSON diagnostic *)
+val diag : string -> string -> range option -> t
+
+(* Build an empty JSON diagnostic; used for clearing diagnostic *)
+val diag_clear : string -> t

ide/lsp/lsp.ml

@@ -0,0 +1,210 @@
+open Yojson.Basic
+open Yojson.Basic.Util
+
+open Json_helper
+
+type assoct = (string * t) list
+
+let lsp_of_response (qid: int option) (response: t) : t =
+  match qid with
+  | Some i -> `Assoc ([("jsonrpc", `String "2.0"); ("id", `Int i)] @ (response |> to_assoc))
+  (* In the case of a notification response, there is no query_id associated *)
+  | None -> `Assoc ([("jsonrpc", `String "2.0")] @ (response |> to_assoc))
+
+type lquery =
+| Initialize of int * string
+| Initialized
+| Shutdown
+| Exit
+| Cancel of int
+| FolderChange of wsch_event
+| ChangeConfig
+| ChangeWatch
+| Symbol of string
+| ExecCommand of string
+| DidOpen of txdoc_item
+| DidChange of string * string
+| WillSave of string
+| WillSaveWait of string
+| DidSave of string * string
+| DidClose of string
+| Completion of txdoc_pos * completion_context
+| Resolve
+| Hover of txdoc_pos
+| SignatureHelp of txdoc_pos
+| Declaration of txdoc_pos
+| Definition of txdoc_pos
+| TypeDefinition of txdoc_pos
+| Implementation of txdoc_pos
+| References
+| DocumentHighlight of txdoc_pos
+| DocumentSymbol
+| CodeAction
+| CodeLens
+| CodeLensResolve
+| DocumentLink
+| DocumentLinkResolve
+| DocumentColor
+| ColorPresentation
+| Formatting
+| RangeFormatting
+| TypeFormatting
+| Rename
+| PrepareRename of txdoc_pos
+| FoldingRange
+| BadProtocolMsg of string
+
+type lsp_query = { query_id: int option; q: lquery }
+
+type error_code =
+| MethodNotFound
+| InternalError
+
+let errorcode_to_int : error_code -> int = function
+| MethodNotFound -> -32601
+| InternalError -> -32603
+
+(** For converting back into json **)
+let response_err (err: error_code) (msg: string option) : t =
+  match msg with
+  | Some msg -> `Assoc [("code", `Int (errorcode_to_int err)); ("message", `String msg)]
+  | None -> `Assoc [("code", `Int (errorcode_to_int err))]
+
+let wrap_jsfail (qid: int option) (str: string) (js: t): lsp_query =
+  { query_id = qid; q = BadProtocolMsg (str ^ "\n" ^ (pretty_to_string js)) }
+
+let wrap_parse_err (str: string): lsp_query =
+  { query_id = None; q = BadProtocolMsg str }
+
+let unpack_lsp_query (r : t) : lsp_query =
+  try
+    let qid = member "id" r |> to_int in
+    try
+      { query_id = Some qid;
+        q = match member "method" r |> to_string with
+            | "initialize" -> Initialize (pmember "processId" r |> to_int,
+                                          pmember "rootUri" r |> to_string)
+            | "initialized" -> Initialized
+            | "shutdown" -> Shutdown
+            | "exit" -> Exit
+            | "$/cancelRequest" -> Cancel (pmember "id" r |> to_int)
+            | "workspace/didChangeWorkspaceFolders" -> FolderChange
+                                                      (pmember "event" r |> to_wsch_event)
+            | "workspace/didChangeConfiguration" -> ChangeConfig
+            | "workspace/didChangeWatchedFiles" -> ChangeWatch
+            | "workspace/symbol" -> Symbol (pmember "r" r |> to_string)
+            | "workspace/executeCommand" -> ExecCommand
+                                            (pmember "command" r |> to_string)
+            | "textDocument/didOpen" -> DidOpen (pmember "textDocument" r |> to_txdoc_item)
+            | "textDocument/didChange" -> DidChange (to_txdoc_id r,
+                                                    pmember "contentChanges" r |> to_contentch)
+            | "textDocument/willSave" -> WillSave (to_txdoc_id r)
+            | "textDocument/willSaveWaitUntil" -> WillSaveWait (to_txdoc_id r)
+            | "textDocument/didSave" -> DidSave (to_txdoc_id r, pmember "text" r |> to_string)
+            | "textDocument/didClose" -> DidClose (to_txdoc_id r)
+            | "textDocument/completion" -> Completion (to_txdoc_pos r,
+                                                      pmember "context" r |> to_compl_context)
+            | "completionItem/resolve" -> Resolve
+            | "textDocument/hover" -> Hover (to_txdoc_pos r)
+            | "textDocument/signatureHelp" -> SignatureHelp (to_txdoc_pos r)
+            | "textDocument/declaration" -> Declaration (to_txdoc_pos r)
+            | "textDocument/definition" -> Definition (to_txdoc_pos r)
+            | "textDocument/typeDefinition" -> TypeDefinition (to_txdoc_pos r)
+            | "textDocument/implementation" -> Implementation (to_txdoc_pos r)
+            | "textDocument/references" -> References
+            | "textDocument/documentHighlight" -> DocumentHighlight (to_txdoc_pos r)
+            | "textDocument/documentSymbol" -> DocumentSymbol
+            | "textDocument/codeAction" -> CodeAction
+            | "textDocument/codeLens" -> CodeLens
+            | "codeLens/resolve" -> CodeLensResolve
+            | "textDocument/documentLink" -> DocumentLink
+            | "documentLink/resolve" -> DocumentLinkResolve
+            | "textDocument/documentColor" -> DocumentColor
+            | "textDocument/colorPresentation" -> ColorPresentation
+            | "textDocument/formatting" -> Formatting
+            | "textDocument/rangeFormatting" -> RangeFormatting
+            | "textDocument/onTypeFormatting" -> TypeFormatting
+            | "textDocument/rename" -> Rename
+            | "textDocument/prepareRename" -> PrepareRename (to_txdoc_pos r)
+            | "textDocument/foldingRange" -> FoldingRange
+            | m -> BadProtocolMsg (Printf.sprintf "Unknown method '%s'" m) }
+        with
+        | Type_error (str, js) -> wrap_jsfail (Some qid) str js
+        | Undefined (str, js) -> wrap_jsfail (Some qid) str js
+      with
+      | Type_error (str, js) -> wrap_jsfail None str js
+      | Undefined (str, js) -> wrap_jsfail None str js
+
+(* The three kinds of responses *)
+let resultResponse (r: t) : t option = Some (`Assoc [("result", r)])
+let errorResponse (r: t) : t option = Some (`Assoc [("error", r)])
+let nullResponse : t option = resultResponse `Null
+
+type state_or_exit_t = State of Vernac.State.t | ExitCode of int
+type response_state_t = t option * state_or_exit_t
+
+let run_query (state: Vernac.State.t) (q: lquery) : response_state_t =
+  try
+    match q with
+    | Initialize (_, _) -> resultResponse server_capabilities, State state
+    | Initialized -> None, State state
+    | Shutdown -> nullResponse, State state
+    | Exit -> None, ExitCode 0
+    | Cancel id -> None, State state
+    | FolderChange evt -> nullResponse, State state
+    | ChangeConfig -> nullResponse, State state
+    | ChangeWatch -> None, State state
+    | Symbol sym -> nullResponse, State state
+    | ExecCommand cmd -> nullResponse, State state
+    | DidOpen { fname = f; langId = _; version = _; text = t } -> nullResponse, State state
+    | DidChange (txid, content) -> None, State state
+    | WillSave txid -> None, State state
+    | WillSaveWait txid -> nullResponse, State state
+    | DidSave (f, t) -> nullResponse, State state
+    | DidClose txid -> None, State state
+    | Completion (txpos, ctx) -> nullResponse, State state
+    | Resolve -> nullResponse, State state
+    | Hover txpos -> nullResponse, State state
+    | SignatureHelp txpos -> nullResponse, State state
+    | Declaration txpos -> nullResponse, State state
+    | Definition txpos -> nullResponse, State state
+    | TypeDefinition txpos -> nullResponse, State state
+    | Implementation txpos -> nullResponse, State state
+    | References -> nullResponse, State state
+    | DocumentHighlight txpos -> nullResponse, State state
+    | DocumentSymbol -> nullResponse, State state
+    | CodeAction -> nullResponse, State state
+    | CodeLens -> nullResponse, State state
+    | CodeLensResolve -> nullResponse, State state
+    | DocumentLink -> nullResponse, State state
+    | DocumentLinkResolve -> nullResponse, State state
+    | DocumentColor -> nullResponse, State state
+    | ColorPresentation -> nullResponse, State state
+    | Formatting -> nullResponse, State state
+    | RangeFormatting -> nullResponse, State state
+    | TypeFormatting -> nullResponse, State state
+    | Rename -> nullResponse, State state
+    | PrepareRename txpos -> nullResponse, State state
+    | FoldingRange -> nullResponse, State state
+    | BadProtocolMsg msg -> errorResponse (response_err MethodNotFound (Some msg)), State state
+  with
+  | _ -> errorResponse (response_err InternalError None), State state
+
+let rec parse_header_len (stream: string Stream.t) (len: int): int =
+  let line = Stream.next stream in
+  if String.starts_with ~prefix:"Content-Length: " line then
+    parse_header_len stream (int_of_string (sub_from line 16))
+  else if String.starts_with ~prefix:"Content-Type: " line then
+    parse_header_len stream len
+  else
+    len
+
+let read_lsp_query (stream: string Stream.t): lsp_query =
+  match parse_header_len stream 0 with
+  | n -> let str = Stream.npeek n stream in
+         if List.length str != n then
+           wrap_parse_err (Printf.sprintf "Could not read %d bytes" n)
+         else
+           unpack_lsp_query (from_string (List.fold_right (fun s1 s2 -> s1 ^ s2) str ""))
+  | exception Stream.Failure -> wrap_parse_err "Malformed LSP header"
+