[goals] [fleche] Add tactic-based preprocessing to goals request.

We add a new parameter `pretac` to the `GoalRequest`, that allows to
query for goals but running a set of tactics (or commands) first.

This is an experiment for now; in particular it'd be nice to rework
the API for speculative execution prior merge.

Co-authored-by: Ambroise Lafont <[email protected]>

CHANGES.md

@@ -45,6 +45,9 @@
  - Export Query Goals API in VSCode client; this way other extensions
    can implement their own commands that query Coq goals (@amblafont,
    @ejgallego, #576, closes #558)
+ - New `pretac` field for preprocessing of goals with a tactic using
+   speculative execution, this is experimental for now (@amblafont,
+   @ejgallego, #573, helps with #558)
 
 # coq-lsp 0.1.7: Just-in-time
 -----------------------------

controller/lsp_core.ml

@@ -297,9 +297,12 @@ let get_pp_format params =
     get_pp_format_from_config ()
   | None -> get_pp_format_from_config ()
 
+let get_pretac params = ostring_field "pretac" params
+
 let do_goals ~params =
   let pp_format = get_pp_format params in
-  let handler = Rq_goals.goals ~pp_format in
+  let pretac = get_pretac params in
+  let handler = Rq_goals.goals ~pp_format ?pretac () in
   do_position_request ~postpone:true ~handler ~params
 
 let do_definition =

controller/rq_goals.ml

@@ -35,26 +35,55 @@ let pp ~pp_format pp =
   | Pp -> Lsp.JCoq.Pp.to_yojson pp
   | Str -> `String (Pp.string_of_ppcmds pp)
 
-let get_goals_info ~doc ~point =
+(* XXX: Speculative execution here requires more thought, about errors,
+   location, we need to make the request fail if it is not good, etc... Moreover
+   we should tune whether we cache the results; we try this for now. *)
+let parse_and_execute_in tac st =
+  (* Parse tac, loc==FIXME *)
+  let str = Gramlib.Stream.of_string tac in
+  let str = Coq.Parsing.Parsable.make ?loc:None str in
+  match Coq.Parsing.parse ~st str with
+  | Coq.Protect.E.{ r = Interrupted; feedback = _ }
+  | Coq.Protect.E.{ r = Completed (Error _); feedback = _ }
+  | Coq.Protect.E.{ r = Completed (Ok None); feedback = _ } -> None
+  | Coq.Protect.E.{ r = Completed (Ok (Some ast)); feedback = _ } -> (
+    let open Fleche.Memo in
+    (* XXX use the bind in Coq.Protect.E *)
+    match (Interp.eval (st, ast)).res with
+    | Coq.Protect.E.{ r = Interrupted; feedback = _ }
+    | Coq.Protect.E.{ r = Completed (Error _); feedback = _ } -> None
+    | Coq.Protect.E.{ r = Completed (Ok st); feedback = _ } -> Some st)
+
+let run_pretac ?pretac st =
+  match pretac with
+  | None ->
+    (* Debug option *)
+    (* Lsp.Io.trace "goals" "pretac empty"; *)
+    Some st
+  | Some tac -> Fleche.Info.in_state ~st ~f:(parse_and_execute_in tac) st
+
+let get_goal_info ~doc ~point ?pretac () =
   let open Fleche in
   let goals_mode = get_goals_mode () in
   let node = Info.LC.node ~doc ~point goals_mode in
   match node with
   | None -> (None, None)
-  | Some node ->
-    let st = node.Doc.Node.state in
-    let goals = Info.Goals.goals ~st in
-    let program = Info.Goals.program ~st in
-    (goals, Some program)
+  | Some node -> (
+    match run_pretac ?pretac node.Doc.Node.state with
+    | None -> (None, None)
+    | Some st ->
+      let goals = Info.Goals.goals ~st in
+      let program = Info.Goals.program ~st in
+      (goals, Some program))
 
-let goals ~pp_format ~doc ~point =
+let goals ~pp_format ?pretac () ~doc ~point =
   let open Fleche in
   let uri, version = (doc.Doc.uri, doc.version) in
   let textDocument = Lsp.Doc.VersionedTextDocumentIdentifier.{ uri; version } in
   let position =
     Lang.Point.{ line = fst point; character = snd point; offset = -1 }
   in
-  let goals, program = get_goals_info ~doc ~point in
+  let goals, program = get_goal_info ~doc ~point ?pretac () in
   let node = Info.LC.node ~doc ~point Exact in
   let messages = mk_messages node in
   let error = Option.bind node mk_error in

controller/rq_goals.mli

@@ -9,4 +9,6 @@ type format =
   | Pp
   | Str
 
-val goals : pp_format:format -> Request.position
+(** [goals ~pp_format ?pretac] Serve goals at point; users can request
+    pre-processing and formatting using the provided parameters. *)
+val goals : pp_format:format -> ?pretac:string -> unit -> Request.position

editor/code/lib/types.ts

@@ -69,6 +69,7 @@ export interface GoalRequest {
   textDocument: VersionedTextDocumentIdentifier;
   position: Position;
   pp_format?: "Pp" | "Str";
+  pretac?: string;
 }
 
 export type Pp =

editor/code/src/goals.ts

@@ -126,6 +126,8 @@ export class InfoPanel {
       uri.toString(),
       version
     );
+    // let pretac = "idtac.";
+    // let cursor: GoalRequest = { textDocument, position, pretac };
     let cursor: GoalRequest = { textDocument, position };
     let strCursor: GoalRequest = {
       textDocument,

etc/doc/PROTOCOL.md

@@ -80,6 +80,7 @@ interface GoalRequest {
     textDocument: VersionedTextDocumentIdentifier;
     position: Position;
     pp_format?: 'Pp' | 'Str';
+    pretac?: string;
 }
 ```
 
@@ -162,6 +163,7 @@ was the default.
 
 #### Changelog
 
+- v0.1.8: new optional `pretac` field for post-processing, backwards compatible with 0.1.7
 - v0.1.7: program information added, rest of fields compatible with 0.1.6
 - v0.1.7: pp_format field added to request, backwards compatible
 - v0.1.6: the `Pp` parameter can now be either Coq's `Pp.t` type or `string` (default)

fleche/info.ml

@@ -175,6 +175,8 @@ module Goals = struct
     let lemmas = Coq.State.lemmas ~st in
     Option.map (Coq.Goals.reify ~ppx) lemmas
 
+  (* We need to use [in_state] here due to printing not being pure, but we want
+     a better design here eventually *)
   let goals ~st = in_state ~st ~f:pr_goal st
   let program ~st = Coq.State.program ~st
 end

fleche/info.mli

@@ -50,10 +50,11 @@ end
 module LC : S with module P := LineCol
 module O : S with module P := Offset
 
-(** Helper to absorb errors in state change, needed due to the lack of proper
-    monad in Coq.Protect, to fix soon *)
+(** Helper to absorb errors in state change to [None], needed due to the lack of
+    proper monad in Coq.Protect, to fix soon *)
 val in_state : st:Coq.State.t -> f:('a -> 'b option) -> 'a -> 'b option
 
+(** We move towards a more modular design here, for preprocessing *)
 module Goals : sig
   val goals : st:Coq.State.t -> Pp.t Coq.Goals.reified_pp option
   val program : st:Coq.State.t -> Declare.OblState.View.t Names.Id.Map.t