[protocol] New request coq/getDocument to get serialized document.

cc: rocq-archive/coq-serapi#318

CHANGES.md

@@ -8,6 +8,9 @@
    fixes #321)
  - Trigger completion on quote char "'" (@ejgallego, #350)
  - Fix typo on keybinding config for show goals (@tomtomjhj, #357)
+ - New request `coq/getDocument` to get serialized full document
+   contents. Thanks to Clément Pit-Claudel for feedback and ideas.
+   (@ejgallego, #350)
 
 # coq-lsp 0.1.5: Form
 ---------------------

controller/lsp_core.ml

@@ -253,6 +253,7 @@ let do_document_request ~params ~handler =
     Postpone (PendingRequest.DocRequest { uri; handler })
 
 let do_symbols = do_document_request ~handler:Rq_symbols.symbols
+let do_document = do_document_request ~handler:Rq_document.request
 
 let do_trace params =
   let trace = string_field "value" params in
@@ -336,6 +337,8 @@ let dispatch_request ~method_ ~params : RAction.t =
   | "textDocument/hover" -> do_hover ~params
   (* Proof-specific stuff *)
   | "proof/goals" -> do_goals ~params
+  (* Coq specific stuff *)
+  | "coq/getDocument" -> do_document ~params
   (* Generic handler *)
   | msg ->
     LIO.trace "no_handler" msg;

controller/rq_document.ml

@@ -0,0 +1,22 @@
+(************************************************************************)
+(* Coq Language Server Protocol -- Document                             *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2019-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+let to_span { Fleche.Doc.Node.range; ast; _ } =
+  let span = Option.map (fun { Fleche.Doc.Node.Ast.v; _ } -> v) ast in
+  Lsp.JFleche.RangedSpan.{ range; span }
+
+let to_completed = function
+  | Fleche.Doc.Completion.Yes range ->
+    { Lsp.JFleche.CompletionStatus.status = `Yes; range }
+  | Stopped range -> { status = `Stopped; range }
+  | Failed range | FailedPermanent range -> { status = `Failed; range }
+
+let request ~doc =
+  let { Fleche.Doc.nodes; completed; _ } = doc in
+  let spans = List.map to_span nodes in
+  let completed = to_completed completed in
+  Lsp.JFleche.FlecheDocument.({ spans; completed } |> to_yojson)

controller/rq_document.mli

@@ -0,0 +1,8 @@
+(************************************************************************)
+(* Coq Language Server Protocol -- Document                             *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2019-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+val request : Requests.document_request

editor/code/lib/types.ts

@@ -53,3 +53,26 @@ export type Pp =
   | ["Pp_comment", string[]];
 
 export type PpString = Pp | string;
+
+export interface FlecheDocumentParams {
+  textDocument: VersionedTextDocumentIdentifier;
+}
+
+// Status of the document, Yes if fully checked, range contains the last seen lexical token
+interface CompletionStatus {
+  status: ["Yes" | "Stopped" | "Failed"];
+  range: Range;
+}
+
+// Implementation-specific span information, for now the serialized Ast if present.
+type SpanInfo = any;
+
+interface RangedSpan {
+  range: Range;
+  span?: SpanInfo;
+}
+
+export interface FlecheDocument {
+  spans: RangedSpan[];
+  completed: CompletionStatus;
+}

editor/code/package.json

@@ -88,6 +88,10 @@
       {
         "command": "coq-lsp.goals",
         "title": "Coq LSP: Show Goals at Point"
+      },
+      {
+        "command": "coq-lsp.document",
+        "title": "Coq LSP: Get document in serialized format, print in console"
       }
     ],
     "keybindings": [

editor/code/src/client.ts

@@ -14,7 +14,11 @@ import {
   LanguageClientOptions,
   RevealOutputChannelOn,
 } from "vscode-languageclient/node";
-
+import {
+  RequestType,
+  VersionedTextDocumentIdentifier,
+} from "vscode-languageclient";
+import { FlecheDocumentParams, FlecheDocument } from "../lib/types";
 import { CoqLspClientConfig, CoqLspServerConfig } from "./config";
 import { InfoPanel } from "./goals";
 import { FileProgressManager } from "./progress";
@@ -138,8 +142,23 @@ export function activate(context: ExtensionContext): void {
 
   context.subscriptions.push(goalsHook);
 
+  const docReq = new RequestType<FlecheDocumentParams, FlecheDocument, void>(
+    "coq/getDocument"
+  );
+
+  let getDocument = (editor: TextEditor) => {
+    let uri = editor.document.uri;
+    let version = editor.document.version;
+    let textDocument = VersionedTextDocumentIdentifier.create(
+      uri.toString(),
+      version
+    );
+    let params: FlecheDocumentParams = { textDocument };
+    client.sendRequest(docReq, params).then((fd) => console.log(fd));
+  };
   coqCommand("restart", restart);
   coqEditorCommand("goals", goals);
+  coqEditorCommand("document", getDocument);
 
   restart();
 }

etc/doc/PROTOCOL.md

@@ -201,3 +201,45 @@ interface CoqFileProgressParams {
 #### Changelog
 
 - v0.1.1: exact copy from Lean protocol (spec under Apache License)
+
+### Document Ast Request
+
+The `coq/getDocument` request returns a serialized version of Fleche's
+document. It is modelled after LSP's standard
+`textDocument/documentSymbol`, but returns instead the full document
+contents as understood by Flèche.
+
+Caveats: Flèche notion of document is evolving, in particular you
+should not assume that the document will remain a list, but it will
+become a tree at some point.
+
+```typescript
+interface FlecheDocumentParams {
+    textDocument: VersionedTextDocumentIdentifier;
+}
+```
+
+```typescript
+// Status of the document, Yes if fully checked, range contains the last seen lexical token
+interface CompletionStatus {
+    status : ['Yes' | 'Stopped' | 'Failed']
+    range : Range
+};
+
+// Implementation-specific span information, for now the serialized Ast if present.
+type SpanInfo = any;
+
+interface RangedSpan {
+    range : Range;
+    span?: SpanInfo
+};
+
+interface FlecheDocument {
+    spans: RangedSpan[];
+    completed : CompletionStatus
+};
+```
+
+#### Changelog
+
+- v0.1.6: initial version

lsp/jCoq.ml

@@ -56,3 +56,10 @@ module Goals = struct
 
   type 'pp reified_pp = ('pp reified_goal, 'pp) goals [@@deriving to_yojson]
 end
+
+module Ast = struct
+  type t = Coq.Ast.t
+
+  let to_yojson x =
+    Serlib.Ser_vernacexpr.vernac_control_to_yojson (Coq.Ast.to_coq x)
+end

lsp/jFleche.ml

@@ -16,6 +16,7 @@
 (************************************************************************)
 
 module Pp = JCoq.Pp
+module Ast = JCoq.Ast
 module Lang = JLang
 
 module Config = struct
@@ -172,3 +173,27 @@ module CompletionData = struct
     }
   [@@deriving yojson]
 end
+
+module CompletionStatus = struct
+  type t =
+    { status : [ `Yes | `Stopped | `Failed ]
+    ; range : Lang.Range.t
+    }
+  [@@deriving yojson]
+end
+
+module RangedSpan = struct
+  type t =
+    { range : Lang.Range.t
+    ; span : Ast.t option [@default None]
+    }
+  [@@deriving to_yojson]
+end
+
+module FlecheDocument = struct
+  type t =
+    { spans : RangedSpan.t list
+    ; completed : CompletionStatus.t
+    }
+  [@@deriving to_yojson]
+end

lsp/jFleche.mli

@@ -132,3 +132,28 @@ module CompletionData : sig
     }
   [@@deriving yojson]
 end
+
+(** Coq-lsp-specific *)
+module CompletionStatus : sig
+  type t =
+    { status : [ `Yes | `Stopped | `Failed ]
+    ; range : Lang.Range.t
+    }
+  [@@deriving yojson]
+end
+
+module RangedSpan : sig
+  type t =
+    { range : Lang.Range.t
+    ; span : Coq.Ast.t option [@default None]
+    }
+  [@@deriving to_yojson]
+end
+
+module FlecheDocument : sig
+  type t =
+    { spans : RangedSpan.t list
+    ; completed : CompletionStatus.t
+    }
+  [@@deriving to_yojson]
+end