Get proof blocks api

client/src/client.ts

@@ -4,7 +4,6 @@ import {
   LanguageClient,
   LanguageClientOptions,
   ServerOptions,
-  integer
 } from 'vscode-languageclient/node';
 
 import {decorationsManual, decorationsContinuous, decorationsErrorAnimation} from './Decorations';

client/src/extension.ts

@@ -17,6 +17,7 @@
   RequestType,
   ServerOptions,
   TextDocumentIdentifier,
+  VersionedTextDocumentIdentifier,
 } from 'vscode-languageclient/node';
 
 import Client from './client';
@@ -27,6 +28,8 @@
 import SearchViewProvider from './panels/SearchViewProvider';
 import {
     CoqLogMessage,
+    DocumentProofsRequest,
+    DocumentProofsResponse,
     ErrorAlertNotification,
     MoveCursorNotification, 
     ProofViewNotification, 
@@ -41,8 +44,8 @@
     sendStepBackward
 } from './manualChecking';
 import { 
     makeVersionedDocumentId,
     isMouseOrKeyboardEvent
 } from './utilities/utils';
 import { DocumentStateViewProvider } from './panels/DocumentStateViewProvider';
 import VsCoqToolchainManager, {ToolchainError, ToolChainErrorCode} from './utilities/toolchain';
@@ -59,6 +62,21 @@
         });
     }
 
+    const getDocumentProofs = (uri: VersionedTextDocumentIdentifier) => {
+        const textDocument = TextDocumentIdentifier.create(uri.toString());
+        const params: DocumentProofsRequest = {textDocument};
+        const req = new RequestType<DocumentProofsRequest, DocumentProofsResponse, void>("vscoq/documentProofs");
+        Client.writeToVscoq2Channel("Getting proofs for: " + uri.toString());
+        client.sendRequest(req, params).then(
+            (res) => {
+                return res;
+            }, 
+            (err) => {
+                window.showErrorMessage(err);
+            }
+        );
+    };
+
     // Watch for files being added or removed
     workspace.onDidCreateFiles(checkInCoqProject);
     workspace.onDidDeleteFiles(checkInCoqProject);
@@ -193,7 +211,7 @@
             const req = new RequestType<ResetCoqRequest, ResetCoqResponse, void>("vscoq/resetCoq");
             Client.writeToVscoq2Channel(uri.toString());
             client.sendRequest(req, params).then(
                 (res) => {
                     GoalPanel.resetGoalPanel();
                 }, 
                 (err) => {
@@ -351,7 +369,7 @@
                 }
             }));
 
             let goalsHook = window.onDidChangeTextEditorSelection(
                 (evt: TextEditorSelectionChangeEvent) => {                    
                     if (evt.textEditor.document.languageId === "coq"
                         && workspace.getConfiguration('vscoq.proof').mode === 1)
@@ -361,14 +379,20 @@
                 }
             );
 
             window.onDidChangeActiveTextEditor(editor => {
                 client.updateHightlights();
             });
 
         });
 
         context.subscriptions.push(client);
-    }	
+    }
+
+    const externalApi = {
+        getDocumentProofs
+    };
+
+    return externalApi;
 
 }
 

client/src/protocol/types.ts

@@ -144,3 +144,22 @@ export interface ResetCoqRequest {
 }
 
 export interface ResetCoqResponse {};
+
+export interface DocumentProofsRequest {
+    textDocument: TextDocumentIdentifier;
+}
+
+type proof_step = {
+    range: Range;
+    tactic: string;
+};
+
+type proof_block = {
+    statement: string;
+    range: Range;
+    proofs: proof_step[];
+};
+
+export interface DocumentProofsResponse {
+    proofs: proof_block[];
+}

language-server/dm/document.ml

@@ -27,11 +27,18 @@ type proof_block_type =
   | DefinitionType of Decls.definition_object_kind
   | Other
 
+type proof_step = {
+  id: sentence_id;
+  tactic: string;
+  range: Range.t;
+}
+
 type outline_element = {
   id: sentence_id;
   name: string;
   type_: proof_block_type;
   statement: string;
+  proof: proof_step list;
   range: Range.t
 }
 
@@ -132,11 +139,20 @@ let range_of_sentence raw (sentence : sentence) =
   let end_ = RawDocument.position_of_loc raw sentence.stop in
   Range.{ start; end_ }
 
+let string_of_sentence raw (sentence: sentence) =
+    let string = RawDocument.string_in_range raw sentence.start sentence.stop in
+    string
+
 let range_of_sentence_with_blank_space raw (sentence : sentence) =
   let start = RawDocument.position_of_loc raw sentence.parsing_start in
   let end_ = RawDocument.position_of_loc raw sentence.stop in
   Range.{ start; end_ }
 
+let string_of_id document id =
+  match SM.find_opt id document.sentences_by_id with
+  | None -> CErrors.anomaly Pp.(str"Trying to get range of non-existing sentence " ++ Stateid.print id)
+  | Some sentence -> string_of_sentence document.raw_doc sentence
+
 let range_of_id document id =
   match SM.find_opt id document.sentences_by_id with
   | None -> CErrors.anomaly Pp.(str"Trying to get range of non-existing sentence " ++ Stateid.print id)
@@ -147,19 +163,29 @@ let range_of_id_with_blank_space document id =
   | None -> CErrors.anomaly Pp.(str"Trying to get range of non-existing sentence " ++ Stateid.print id)
   | Some sentence -> range_of_sentence_with_blank_space document.raw_doc sentence
 
+let push_proof_step_in_outline document id (outline : outline) =
+  let range = range_of_id document id in
+  let tactic = string_of_id document id in
+  let proof_step = {id; tactic; range} in
+  match outline with
+  | [] -> outline
+  | e :: l -> 
+    let proof = proof_step :: e.proof in
+    {e with proof} :: l
 
 let record_outline document id (ast : Synterp.vernac_control_entry) classif (outline : outline) =
   let open Vernacextend in
   match classif with
+  | VtProofStep _ -> push_proof_step_in_outline document id outline
   | VtStartProof (_, names) ->
     let vernac_gen_expr = ast.v.expr in
-    let type_, statement = match vernac_gen_expr with
-      | VernacSynterp _ -> None, ""
+    let type_ = match vernac_gen_expr with
+      | VernacSynterp _ -> None
       | VernacSynPure pure -> 
         match pure with
-        | Vernacexpr.VernacStartTheoremProof (kind, _) -> Some (TheoremKind kind), "theorem"
-        | Vernacexpr.VernacDefinition ((_, def), _, _) -> Some (DefinitionType def), "definition"
-        | _ -> None, ""
+        | Vernacexpr.VernacStartTheoremProof (kind, _) -> Some (TheoremKind kind)
+        | Vernacexpr.VernacDefinition ((_, def), _, _) -> Some (DefinitionType def)
+        | _ -> None
     in
     let name = match names with
     |[] -> "default"
@@ -169,7 +195,8 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out
     | None -> outline
     | Some type_ ->
       let range = range_of_id document id in
-      let element = {id; type_; name; statement; range} in
+      let statement = string_of_id document id in
+      let element = {id; type_; name; statement; range; proof=[]} in
       element :: outline
     end
   | VtSideff (names, _) ->
@@ -179,8 +206,8 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out
       | VernacSynterp _ -> None, ""
       | VernacSynPure pure -> 
         match pure with
-        | Vernacexpr.VernacStartTheoremProof (kind, _) -> Some (TheoremKind kind), "theroem"
-        | Vernacexpr.VernacDefinition ((_, def), _, _) -> Some (DefinitionType def), "definition"
+        | Vernacexpr.VernacStartTheoremProof (kind, _) -> Some (TheoremKind kind), string_of_id document id
+        | Vernacexpr.VernacDefinition ((_, def), _, _) -> Some (DefinitionType def), string_of_id document id
         | _ -> None, ""
     in
     let name = match names with
@@ -191,7 +218,7 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out
     | None -> outline
     | Some type_ ->
       let range = range_of_id document id in
-      let element = {id; type_; name; statement; range} in
+      let element = {id; type_; name; statement; range; proof=[]} in
       element :: outline
     end
   | _ -> outline

language-server/dm/document.mli

@@ -27,12 +27,19 @@ type proof_block_type =
   | DefinitionType of Decls.definition_object_kind
   | Other
 
+type proof_step = {
+  id: sentence_id;
+  tactic: string;
+  range: Range.t;
+}
+
 type outline_element = {
     id: sentence_id;
     name: string;
     type_: proof_block_type;
     statement: string;
-    range: Range.t
+    proof: proof_step list;
+    range: Range.t;
   }
 
 type outline = outline_element list

language-server/dm/documentManager.ml

@@ -319,6 +319,24 @@ let observe ~background state id ~should_block_on_error : (state * event Sel.Eve
 
 let reset_to_top st = { st with observe_id = Top }
 
+
+let get_document_proofs st =
+  let outline = Document.outline st.document in
+  let is_theorem Document.{ type_ } =
+    match type_ with
+    | TheoremKind _ -> true
+    | _ -> false
+    in
+  let mk_proof_block Document.{statement; proof; range } =
+    let steps = List.map (fun Document.{tactic; range} -> ProofState.mk_proof_step tactic range) proof in
+    let step_ranges = List.map (fun (x: Document.proof_step) -> x.range) proof in
+    let range = List.fold_right RangeList.insert_or_merge_range step_ranges [range] in
+    let range = List.hd range in
+    ProofState.mk_proof_block statement steps range
+  in
+  let proofs, _  = List.partition is_theorem outline in
+  List.map mk_proof_block proofs
+
 let get_document_symbols st =
   let outline = Document.outline st.document in
   let to_document_symbol elem =

language-server/dm/documentManager.mli

@@ -110,6 +110,8 @@ val get_info_messages : state -> Position.t option -> (DiagnosticSeverity.t * pp
 
 val get_document_symbols : state -> DocumentSymbol.t list
 
+val get_document_proofs : state -> ProofState.proof_block list
+
 val all_diagnostics : state -> Diagnostic.t list
 (** all_diagnostics [doc] returns the diagnostics corresponding to the sentences
     that have been executed in [doc]. *)

language-server/dm/rawDocument.ml

@@ -102,6 +102,12 @@ let word_at_position raw pos : string option =
   with _ ->
     None
 
+let string_in_range raw start end_ =
+  try
+    String.sub raw.text start (end_ - start)
+  with _ -> (* TODO: ERROR *)
+    ""
+
 let apply_text_edit raw (Range.{start; end_}, editText) =
   let start = loc_of_position raw start in
   let stop = loc_of_position raw end_ in

language-server/dm/rawDocument.mli

@@ -26,6 +26,7 @@ val end_loc : t -> int
 
 val range_of_loc : t -> Loc.t -> Range.t
 val word_at_position: t -> Position.t -> string option
+val string_in_range: t -> int -> int -> string
 
 (** Applies a text edit, and returns start location *)
 val apply_text_edit : t -> text_edit -> t * int

language-server/protocol/extProtocol.ml

@@ -248,6 +248,22 @@ module Request = struct
 
   end
 
+  module DocumentProofsParams = struct
+
+    type t = {
+      textDocument: VersionedTextDocumentIdentifier.t
+    } [@@deriving yojson]
+
+  end
+
+  module DocumentProofsResult = struct
+
+    type t = {
+      proofs: ProofState.proof_block list;
+    } [@@deriving yojson]
+
+  end
+
   type 'a t =
   | Std : 'a Lsp.Client_request.t -> 'a t
   | Reset : ResetParams.t -> unit t
@@ -257,6 +273,7 @@ module Request = struct
   | Print : PrintParams.t -> pp t
   | Search : SearchParams.t -> unit t
   | DocumentState : DocumentStateParams.t -> DocumentStateResult.t t
+  | DocumentProofs : DocumentProofsParams.t -> DocumentProofsResult.t t
 
   type packed = Pack : 'a t -> packed
 
@@ -284,6 +301,9 @@ module Request = struct
     | "vscoq/documentState" ->
       let+ params = Lsp.Import.Json.message_params params DocumentStateParams.t_of_yojson in
       Pack (DocumentState params)
+    | "vscoq/documentProofs" ->
+      let+ params = Lsp.Import.Json.message_params params DocumentProofsParams.t_of_yojson in
+      Pack (DocumentProofs params)
     | _ ->
       let+ E req = Lsp.Client_request.of_jsonrpc req in
       Pack (Std req)
@@ -298,6 +318,7 @@ module Request = struct
       | Print _ -> yojson_of_pp resp
       | Search _ -> yojson_of_unit resp
       | DocumentState _ -> DocumentStateResult.(yojson_of_t resp)
+      | DocumentProofs _ -> DocumentProofsResult.(yojson_of_t resp)
       | Std req -> Lsp.Client_request.yojson_of_result req resp
 
   end

language-server/protocol/proofState.ml

@@ -13,9 +13,21 @@
 (**************************************************************************)
 
 open Printing
+open Lsp.Types
 
 open Ppx_yojson_conv_lib.Yojson_conv.Primitives
 
+type proof_step = {
+  tactic: string;
+  range: Range.t;
+} [@@deriving yojson]
+
+type proof_block = {
+  statement: string;
+  range: Range.t;
+  steps: proof_step list;
+} [@@deriving yojson]
+
 type goal = {
   id: int;
   hypotheses: pp list;
@@ -118,4 +130,8 @@ let get_proof ~previous diff_mode st =
       shelvedGoals;
       givenUpGoals;
       unfocusedGoals;
-    }
+    }
+
+let mk_proof_step tactic range = {tactic; range}
+
+let mk_proof_block statement steps range = {statement; steps; range}

language-server/protocol/proofState.mli

@@ -13,6 +13,13 @@
 (**************************************************************************)
 open Settings
 
+type proof_step [@@deriving yojson]
+
+type proof_block [@@deriving yojson]
+
 type t [@@deriving yojson]
 
-val get_proof : previous:Vernacstate.t option -> Goals.Diff.Mode.t -> Vernacstate.t -> t option
+val get_proof : previous:Vernacstate.t option -> Goals.Diff.Mode.t -> Vernacstate.t -> t option
+
+val mk_proof_step : string -> Lsp.Types.Range.t -> proof_step
+val mk_proof_block : string -> proof_step list -> Lsp.Types.Range.t -> proof_block

language-server/vscoqtop/lspManager.ml

@@ -546,6 +546,14 @@ let sendDocumentState id params =
   | Some { st } -> let document = Dm.DocumentManager.Internal.string_of_state st in
     Ok Request.Client.DocumentStateResult.{ document }, []
 
+let sendDocumentProofs id params = 
+  let Request.Client.DocumentProofsParams.{ textDocument } = params in
+  let uri = textDocument.uri in
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ "[documentProofs] ignoring event on non existent document"; Error({message="Document does not exist"; code=None}), []
+  | Some { st } -> let proofs = Dm.DocumentManager.get_document_proofs st in
+    Ok Request.Client.DocumentProofsResult.{ proofs }, []
+
 let workspaceDidChangeConfiguration params = 
   let Lsp.Types.DidChangeConfigurationParams.{ settings } = params in
   let settings = Settings.t_of_yojson settings in
@@ -582,6 +590,7 @@ let dispatch_request : type a. Jsonrpc.Id.t -> a Request.Client.t -> (a,error) r
   | Print params -> coqtopPrint id params
   | Search params -> coqtopSearch id params
   | DocumentState params -> sendDocumentState id params
+  | DocumentProofs params -> sendDocumentProofs id params
 
 let dispatch_std_notification = 
   let open Lsp.Client_notification in function