Export API to run tactics at a given loc

client/src/extension.ts

@@ -9,7 +9,8 @@ import {workspace, window, commands, languages, ExtensionContext, env,
   extensions,
   StatusBarAlignment,
   MarkdownString,
-  WorkspaceEdit
+  WorkspaceEdit,
+  Position
 } from 'vscode';
 
 import {
@@ -27,6 +28,8 @@ import GoalPanel from './panels/GoalPanel';
 import SearchViewProvider from './panels/SearchViewProvider';
 import {
     CoqLogMessage,
+    CoqPilotRequest,
+    CoqPilotResponse,
     DocumentProofsRequest,
     DocumentProofsResponse,
     ErrorAlertNotification,
@@ -69,6 +72,14 @@ export function activate(context: ExtensionContext) {
         return client.sendRequest(req, params);
     };
 
+    const runTacticsAtLocContext = (uri: Uri, position: Position, text: string) => {
+        const textDocument = TextDocumentIdentifier.create(uri.toString());
+        const params: CoqPilotRequest = {textDocument, position, text};
+        const req = new RequestType<CoqPilotRequest, CoqPilotResponse, void>("vscoq/coqPilot");
+        Client.writeToVscoq2Channel("Trying running tactics: (" + text + ") for document: " + uri.toString());
+        return client.sendRequest(req, params);
+    };
+
     // Watch for files being added or removed
     workspace.onDidCreateFiles(checkInCoqProject);
     workspace.onDidDeleteFiles(checkInCoqProject);
@@ -381,7 +392,8 @@ Path: \`${coqTM.getVsCoqTopPath()}\`
     }
 
     const externalApi = {
-        getDocumentProofs
+        getDocumentProofs,
+        runTacticsAtLocContext
     };
 
     return externalApi;

client/src/protocol/types.ts

@@ -168,3 +168,13 @@ type ProofBlock = {
 export interface DocumentProofsResponse {
     proofs: ProofBlock[];
 }
+
+export interface CoqPilotRequest {
+    textDocument: TextDocumentIdentifier;
+    position: Position;
+    text: string;
+}
+
+export interface CoqPilotResponse {
+    errors: string[];
+}

language-server/dm/document.ml

@@ -107,7 +107,7 @@ type parse_state = {
   loc: Loc.t option;
   synterp_state : Vernacstate.Synterp.t;
   stream: (unit, char) Gramlib.Stream.t;
-  raw: RawDocument.t;
+  raw: RawDocument.t option;
   parsed: pre_sentence list;
   errors: parsing_error list;
   parsed_comments: comment list;
@@ -250,6 +250,16 @@ let add_sentence parsed parsing_start start stop (ast: parsed_ast) synterp_state
   } in
   document, scheduler_state_after
 
+let pre_sentence_to_sentence parsing_start start stop (ast: parsed_ast) synterp_state scheduler_state_before schedule =
+  let id = Stateid.fresh () in
+  let ast' = (ast.ast, ast.classification, synterp_state) in
+  let scheduler_state_after, schedule =
+    Scheduler.schedule_sentence (id, ast') scheduler_state_before schedule
+  in
+  (* FIXME may invalidate scheduler_state_XXX for following sentences -> propagate? *)
+  let sentence = { parsing_start; start; stop; ast; id; synterp_state; scheduler_state_before; scheduler_state_after } in
+  sentence, schedule, scheduler_state_after
+
 let remove_sentence parsed id =
   match SM.find_opt id parsed.sentences_by_id with
   | None -> parsed
@@ -512,15 +522,15 @@ let handle_parse_error start msg qf ({stream; errors;} as parse_state) =
   let errors = parsing_error :: errors in
   let parse_state = {parse_state with errors} in
   (* TODO: we could count the \n between start and stop and increase Loc.line_nb *)
-  create_parsing_event (ParseEvent parse_state)
+  ParseEvent parse_state
 
 let handle_parse_more ({loc; synterp_state; stream; raw; parsed; parsed_comments} as parse_state) =
   let start = Stream.count stream in
   log @@ "Start of parse is: " ^ (string_of_int start);
   begin
     (* FIXME should we save lexer state? *)
     match parse_one_sentence ?loc stream ~st:synterp_state with
-    | None, _ (* EOI *) -> create_parsing_event (Invalidate parse_state)
+    | None, _ (* EOI *) -> Invalidate parse_state
     | Some ast, comments ->
       let stop = Stream.count stream in
       log @@ "Parsed: " ^ (Pp.string_of_ppcmds @@ Ppvernac.pr_vernac ast);
@@ -529,10 +539,14 @@ let handle_parse_more ({loc; synterp_state; stream; raw; parsed; parsed_comments
               | Some lc -> lc.line_nb, lc.bp, lc.ep
               | None -> assert false
       in
-      let str = String.sub (RawDocument.text raw) begin_char (end_char - begin_char) in
-      let sstr = Stream.of_string str in
-      let lex = CLexer.Lexer.tok_func sstr in
-      let tokens = stream_tok 0 [] lex begin_line begin_char in
+        let tokens = match raw with
+        | None -> []
+        | Some raw ->
+          let str = String.sub (RawDocument.text raw) begin_char (end_char - begin_char) in
+          let sstr = Stream.of_string str in
+          let lex = CLexer.Lexer.tok_func sstr in
+          stream_tok 0 [] lex begin_line begin_char
+        in
       begin
         try
           let entry = get_entry ast in
@@ -544,7 +558,7 @@ let handle_parse_more ({loc; synterp_state; stream; raw; parsed; parsed_comments
           let parsed_comments = List.append comments parsed_comments in
           let loc = ast.loc in
           let parse_state = {parse_state with parsed_comments; parsed; loc; synterp_state} in
-          create_parsing_event (ParseEvent parse_state)
+          ParseEvent parse_state
         with exn ->
           let e, info = Exninfo.capture exn in
           let loc = get_loc_from_info_or_exn e info in
@@ -626,7 +640,7 @@ let validate_document ({ parsed_loc; raw_doc; cancel_handle } as document) =
   while Stream.count stream < stop do Stream.junk () stream done;
   log @@ Format.sprintf "Parsing more from pos %i" stop;
   let started = Unix.gettimeofday () in
-  let parsed_state = {stop; top_id;synterp_state; stream; raw=raw_doc; parsed=[]; errors=[]; parsed_comments=[]; loc=None; started; previous_document=document} in
+  let parsed_state = {stop; top_id;synterp_state; stream; raw=(Some raw_doc); parsed=[]; errors=[]; parsed_comments=[]; loc=None; started; previous_document=document} in
   let priority = Some PriorityManager.parsing in
   let event = Sel.now ?priority (ParseEvent parsed_state) in
   let cancel_handle = Some (Sel.Event.get_cancellation_handle event) in
@@ -659,10 +673,31 @@ let handle_invalidate {parsed; errors; parsed_comments; stop; top_id; started; p
 let handle_event document = function
 | ParseEvent state -> 
   let event = handle_parse_more state in
+  let event = create_parsing_event event in
   let cancel_handle = Some (Sel.Event.get_cancellation_handle event) in
   {document with cancel_handle}, [event], None
 | Invalidate state -> {document with cancel_handle=None}, [], handle_invalidate state document
 
+let rec parse_full = function
+| ParseEvent state ->
+  let event = handle_parse_more state in
+  parse_full event
+| Invalidate state ->
+  state
+
+let parse_text_at_loc loc text document =
+  let top_id = Option.map (fun sentence -> sentence.id) (find_sentence_strictly_before document loc) in
+  let (stop, synterp_state, scheduler_state) = state_strictly_before document loc in
+  let stream = Stream.of_string text in
+  let parsed_state = {synterp_state; started = Unix.gettimeofday (); top_id; stream; raw=None; loc=None; errors=[]; parsed=[]; parsed_comments=[]; previous_document=document; stop} in
+  let {parsed} = parse_full (ParseEvent parsed_state) in
+  let add_sentence (sentences, schedule, scheduler_state) ({ parsing_start; start; stop; ast; synterp_state } : pre_sentence) =
+    let added_sentence, schedule, schedule_state = pre_sentence_to_sentence parsing_start start stop ast synterp_state scheduler_state schedule in
+    sentences @ [added_sentence], schedule, schedule_state
+  in
+  let sentences, schedule, _ = List.fold_left add_sentence ([],document.schedule, scheduler_state) parsed in
+  sentences, schedule
+
 let create_document init_synterp_state text =
   let raw_doc = RawDocument.create text in
     { 

language-server/dm/document.mli

@@ -161,6 +161,8 @@ val range_of_id : document -> Stateid.t -> Range.t
 val range_of_id_with_blank_space : document -> Stateid.t -> Range.t
 (** [range_of_id_with_blank_space doc id] returns a Range object coressponding to the sentence id given in argument but with the white spaces before (until the previous sentence) *)
 
+val parse_text_at_loc : int -> string -> document -> sentence list * Scheduler.schedule
+
 module Internal : sig
 
   val string_of_sentence : sentence -> string

language-server/dm/documentManager.ml

@@ -318,6 +318,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 coq_pilot_observe st position text =
+  let loc = RawDocument.loc_of_position (Document.raw_document st.document) position in
+  match Document.find_sentence_before st.document loc with
+  | None -> log @@ "COQ PILOT ON NON VALID POSITION"; [] (* HANDLE ERROR *)
+  | Some {id} ->
+    let sentences, sch = Document.parse_text_at_loc loc text st.document in
+    let vst_for_next_todo, execution_state, task, _ = ExecutionManager.build_tasks_for st.document (Document.schedule st.document) st.execution_state id false in
+    let execution_state = ExecutionManager.build_tasks_for_sentences execution_state sch sentences in
+    let rec execute_task execution_state vst_for_next_todo task =
+      match task with
+      | None -> execution_state, vst_for_next_todo
+      | Some task ->
+        let (next, execution_state,vst_for_next_todo,_events,_interrupted) =
+        ExecutionManager.execute execution_state st.document (vst_for_next_todo, [], false) task false in
+        execute_task execution_state vst_for_next_todo next
+    in
+    let execution_state, _ = execute_task execution_state vst_for_next_todo task in
+    let all_errors = ExecutionManager.all_errors execution_state in  (* TODO: RETURN ONLY THE NEW ERRORS *)
+    let get_pp_error (_, (_, pp, _)) = pp in
+    List.map (fun e -> Pp.string_of_ppcmds @@  get_pp_error e) all_errors
 
 let get_document_proofs st =
   let outline = Document.outline st.document in

language-server/dm/documentManager.mli

@@ -142,6 +142,7 @@ val locate : state -> Position.t -> pattern:string -> (pp, error) Result.t
 
 val print : state -> Position.t -> pattern:string -> (pp, error) Result.t
 
+val coq_pilot_observe : state -> Position.t -> string -> string list
 
 module Internal : sig
 

language-server/dm/executionManager.ml

@@ -710,6 +710,11 @@ let build_tasks_for document sch st id block =
   | Some id, true ->
     vs, {st with todo=[]}, None, Some id
 
+let build_tasks_for_sentences st sch sentences =
+  let tasks = List.map (fun ({id}: Document.sentence) -> snd @@ task_for_sentence sch id) sentences in
+  let todo = List.concat_map prepare_task tasks in
+  {st with todo}
+
 let all_errors st =
   List.fold_left (fun acc (id, (p,_)) ->
     match p with

language-server/dm/executionManager.mli

@@ -74,7 +74,8 @@ val handle_event : event -> state -> (sentence_id option * state option * events
 (** Execution happens in two steps. In particular the event one takes only
     one task at a time to ease checking for interruption *)
 type prepared_task
-val build_tasks_for : Document.document -> Scheduler.schedule -> state -> sentence_id -> bool -> Vernacstate.t * state * prepared_task option * errored_sentence
+val build_tasks_for : Document.document -> Scheduler.schedule -> state -> sentence_id -> bool -> Vernacstate.t * state * prepared_task option * sentence_id option
+val build_tasks_for_sentences : state -> Scheduler.schedule -> Document.sentence list -> state
 val execute : state -> Document.document -> Vernacstate.t * events * bool -> prepared_task -> bool -> (prepared_task option * state * Vernacstate.t * events * errored_sentence)
 
 (* val update_overview : prepared_task -> prepared_task list -> state -> Document.document -> state

language-server/protocol/extProtocol.ml

@@ -253,13 +253,29 @@ module Request = struct
     type t = {
       textDocument: TextDocumentIdentifier.t
     } [@@deriving yojson]
+
+  end
+  module CoqPilotParams = struct
+
+    type t = {
+      textDocument : TextDocumentIdentifier.t;
+      position: Position.t;
+      text: string;
+    } [@@deriving yojson]
 
   end
 
   module DocumentProofsResult = struct
 
     type t = {
       proofs: ProofState.proof_block list;
+    } [@@ deriving yojson]
+
+  end
+  module CoqPilotResult = struct
+
+    type t = {
+      errors: string list;
     } [@@deriving yojson]
 
   end
@@ -274,6 +290,7 @@ module Request = struct
   | Search : SearchParams.t -> unit t
   | DocumentState : DocumentStateParams.t -> DocumentStateResult.t t
   | DocumentProofs : DocumentProofsParams.t -> DocumentProofsResult.t t
+  | CoqPilot : CoqPilotParams.t -> CoqPilotResult.t t
 
   type packed = Pack : 'a t -> packed
 
@@ -304,6 +321,9 @@ module Request = struct
     | "vscoq/documentProofs" ->
       let+ params = Lsp.Import.Json.message_params params DocumentProofsParams.t_of_yojson in
       Pack (DocumentProofs params)
+    | "vscoq/coqPilot" ->
+      let+ params = Lsp.Import.Json.message_params params CoqPilotParams.t_of_yojson in
+      Pack (CoqPilot params)
     | _ ->
       let+ E req = Lsp.Client_request.of_jsonrpc req in
       Pack (Std req)
@@ -319,6 +339,7 @@ module Request = struct
       | Search _ -> yojson_of_unit resp
       | DocumentState _ -> DocumentStateResult.(yojson_of_t resp)
       | DocumentProofs _ -> DocumentProofsResult.(yojson_of_t resp)
+      | CoqPilot _ -> CoqPilotResult.(yojson_of_t resp)
       | Std req -> Lsp.Client_request.yojson_of_result req resp
 
   end

language-server/vscoqtop/lspManager.ml

@@ -558,6 +558,17 @@ let sendDocumentProofs id params =
       let proofs = Dm.DocumentManager.get_document_proofs st in
       Ok Request.Client.DocumentProofsResult.{ proofs }, []
 
+let sendCoqPilotResult id params =
+  let Request.Client.CoqPilotParams.{ textDocument; position; text} = params in
+  let uri = textDocument.uri in
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ "[coqPilotResult] ignoring event on non existant document"; Error({message="Document does not exist"; code=None}), []
+  | Some { st } -> 
+    let errors = Dm.DocumentManager.coq_pilot_observe st position text in
+    log "Sending errors for coqpilot request:";
+    List.iter (fun e -> log e) errors;
+    Ok Request.Client.CoqPilotResult.{ errors }, []
+
 let workspaceDidChangeConfiguration params = 
   let Lsp.Types.DidChangeConfigurationParams.{ settings } = params in
   let settings = Settings.t_of_yojson settings in
@@ -595,6 +606,7 @@ let dispatch_request : type a. Jsonrpc.Id.t -> a Request.Client.t -> (a,error) r
   | Search params -> coqtopSearch id params
   | DocumentState params -> sendDocumentState id params
   | DocumentProofs params -> sendDocumentProofs id params
+  | CoqPilot params -> log "Recieved request: vscoq/coqPilot"; sendCoqPilotResult id params
 
 let dispatch_std_notification = 
   let open Lsp.Client_notification in function