From 493805d7f27488a619c3c112d23d1bf3aec604ce Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 10 Oct 2023 21:02:27 +0200 Subject: [PATCH] [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 --- CHANGES.md | 3 +++ controller/lsp_core.ml | 5 ++++- controller/rq_goals.ml | 45 +++++++++++++++++++++++++++++++++------- controller/rq_goals.mli | 4 +++- editor/code/lib/types.ts | 1 + editor/code/src/goals.ts | 2 ++ etc/doc/PROTOCOL.md | 2 ++ fleche/info.ml | 2 ++ fleche/info.mli | 5 +++-- 9 files changed, 57 insertions(+), 12 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index f5a9a235..dbac0004 100644 --- a/CHANGES.md +++ b/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 ----------------------------- diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index b1848906..3980c0ef 100644 --- a/controller/lsp_core.ml +++ b/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 = diff --git a/controller/rq_goals.ml b/controller/rq_goals.ml index c9d9dc13..35c7027e 100644 --- a/controller/rq_goals.ml +++ b/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 diff --git a/controller/rq_goals.mli b/controller/rq_goals.mli index 4dec5e68..08d9670f 100644 --- a/controller/rq_goals.mli +++ b/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 diff --git a/editor/code/lib/types.ts b/editor/code/lib/types.ts index 11828445..d0cf2166 100644 --- a/editor/code/lib/types.ts +++ b/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 = diff --git a/editor/code/src/goals.ts b/editor/code/src/goals.ts index ff7f67a8..845e74fb 100644 --- a/editor/code/src/goals.ts +++ b/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, diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md index 4c54a85a..8e9d9797 100644 --- a/etc/doc/PROTOCOL.md +++ b/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) diff --git a/fleche/info.ml b/fleche/info.ml index 8a073511..687448d5 100644 --- a/fleche/info.ml +++ b/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 diff --git a/fleche/info.mli b/fleche/info.mli index 6854a4bf..b0b9c781 100644 --- a/fleche/info.mli +++ b/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