Merge pull request #960 from coq/get-proof-blocks-api

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

@@ -27,6 +27,8 @@ import GoalPanel from './panels/GoalPanel';
 import SearchViewProvider from './panels/SearchViewProvider';
 import {
     CoqLogMessage,
+    DocumentProofsRequest,
+    DocumentProofsResponse,
     ErrorAlertNotification,
     MoveCursorNotification, 
     ProofViewNotification, 
@@ -59,6 +61,14 @@ export function activate(context: ExtensionContext) {
         });
     }
 
+    const getDocumentProofs = (uri: Uri) => {
+        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());
+        return client.sendRequest(req, params);
+    };
+
     // Watch for files being added or removed
     workspace.onDidCreateFiles(checkInCoqProject);
     workspace.onDidDeleteFiles(checkInCoqProject);
@@ -368,7 +378,13 @@ Path: \`${coqTM.getVsCoqTopPath()}\`
         });
 
         context.subscriptions.push(client);
-    }	
+    }
+
+    const externalApi = {
+        getDocumentProofs
+    };
+
+    return externalApi;
 
 }
 

client/src/protocol/types.ts

@@ -144,3 +144,27 @@ export interface ResetCoqRequest {
 }
 
 export interface ResetCoqResponse {};
+
+export interface DocumentProofsRequest {
+    textDocument: TextDocumentIdentifier;
+}
+
+type ProofStatement = {
+    range: Range;
+    statement: string;
+}
+
+type ProofStep = {
+    range: Range;
+    tactic: string;
+};
+
+type ProofBlock = {
+    statement: ProofStatement;
+    range: Range;
+    steps: ProofStep[];
+};
+
+export interface DocumentProofsResponse {
+    proofs: ProofBlock[];
+}

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 _ | VtQed _ -> 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,11 +218,15 @@ 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
 
+let compute_outline ({ sentences_by_end } as document) =
+    LM.fold (fun _ {id; ast} -> record_outline document id ast.ast ast.classification) sentences_by_end []
+
+
 let schedule doc = doc.schedule
 
 let raw_document doc = doc.raw_doc
@@ -217,8 +248,7 @@ let add_sentence parsed parsing_start start stop (ast: parsed_ast) synterp_state
     sentences_by_id = SM.add id sentence parsed.sentences_by_id;
     schedule;
   } in
-  let outline = record_outline document id ast.ast ast.classification parsed.outline in
-  {document with outline}, scheduler_state_after
+  document, scheduler_state_after
 
 let remove_sentence parsed id =
   match SM.find_opt id parsed.sentences_by_id with
@@ -622,7 +652,8 @@ let handle_invalidate {parsed; errors; parsed_comments; stop; top_id; started; p
     List.fold_left (fun acc (comment : comment) -> LM.add comment.stop comment acc) comments new_comments
   in
   let parsed_loc = pos_at_end document in
-  let parsed_document = {document with parsed_loc; parsing_errors_by_end; comments_by_end} in
+  let outline = compute_outline document in
+  let parsed_document = {document with parsed_loc; parsing_errors_by_end; comments_by_end; outline} in
   Some {parsed_document; unchanged_id; invalid_ids; previous_document}
 
 let handle_event document = function

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,26 @@ 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 statement = ProofState.mk_proof_statement statement range in
+    let last_step = List.hd proof in
+    let proof = List.rev proof in
+    let fst_step = List.hd proof in
+    let range = Range.create ~start:fst_step.range.start ~end_:last_step.range.end_ in
+    let steps = List.map (fun Document.{tactic; range} -> ProofState.mk_proof_step tactic range) proof 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: TextDocumentIdentifier.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,26 @@
 (**************************************************************************)
 
 open Printing
+open Lsp.Types
 
 open Ppx_yojson_conv_lib.Yojson_conv.Primitives
 
+type proof_statement = {
+  statement: string;
+  range: Range.t;
+} [@@deriving yojson]
+
+type proof_step = {
+  tactic: string;
+  range: Range.t;
+} [@@deriving yojson]
+
+type proof_block = {
+  statement: proof_statement;
+  range: Range.t;
+  steps: proof_step list;
+} [@@deriving yojson]
+
 type goal = {
   id: int;
   hypotheses: pp list;
@@ -118,4 +135,10 @@ let get_proof ~previous diff_mode st =
       shelvedGoals;
       givenUpGoals;
       unfocusedGoals;
-    }
+    }
+
+let mk_proof_statement statement range = {statement; range}
+
+let mk_proof_step tactic range = {tactic; range}
+
+let mk_proof_block statement steps range = {steps; statement; range}

language-server/protocol/proofState.mli

@@ -13,6 +13,16 @@
 (**************************************************************************)
 open Settings
 
+type proof_statement [@@deriving yojson]
+
+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_statement : string -> Lsp.Types.Range.t -> proof_statement
+val mk_proof_step : string -> Lsp.Types.Range.t -> proof_step
+val mk_proof_block : proof_statement -> proof_step list -> Lsp.Types.Range.t -> proof_block