From c08bfcd8d1ae71180855889da2a4317efb0fa5b8 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Oct 2023 21:19:02 +0200 Subject: [PATCH] [goals] Remove duplicate call to Info.find We were doing two calls to find for each goals request. We now remove unused API as in general the composition of `find` plus a field projection for `Doc.Node.t` was not very useful due to find not being memoized. --- controller/rq_goals.ml | 16 ++++++-- controller/rq_hover.ml | 2 +- fleche/info.ml | 90 ++++++++++++++++-------------------------- fleche/info.mli | 21 ++++++---- 4 files changed, 60 insertions(+), 69 deletions(-) diff --git a/controller/rq_goals.ml b/controller/rq_goals.ml index 109052e5..c9d9dc13 100644 --- a/controller/rq_goals.ml +++ b/controller/rq_goals.ml @@ -35,6 +35,18 @@ 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 = + 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) + let goals ~pp_format ~doc ~point = let open Fleche in let uri, version = (doc.Doc.uri, doc.version) in @@ -42,9 +54,7 @@ let goals ~pp_format ~doc ~point = let position = Lang.Point.{ line = fst point; character = snd point; offset = -1 } in - let goals_mode = get_goals_mode () in - let goals = Info.LC.goals ~doc ~point goals_mode in - let program = Info.LC.program ~doc ~point goals_mode in + let goals, program = get_goals_info ~doc ~point 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_hover.ml b/controller/rq_hover.ml index c59d3715..a441d260 100644 --- a/controller/rq_hover.ml +++ b/controller/rq_hover.ml @@ -108,7 +108,7 @@ let info_of_id ~st id = let info_of_id_at_point ~node id = let st = node.Fleche.Doc.Node.state in - Fleche.Info.LC.in_state ~st ~f:(info_of_id ~st) id + Fleche.Info.in_state ~st ~f:(info_of_id ~st) id let pp_typ id = function | Def typ -> diff --git a/fleche/info.ml b/fleche/info.ml index 7b62aa67..8a073511 100644 --- a/fleche/info.ml +++ b/fleche/info.ml @@ -114,18 +114,9 @@ module type S = sig type ('a, 'r) query = doc:Doc.t -> point:P.t -> 'a -> 'r option val node : (approx, Doc.Node.t) query - val range : (approx, Lang.Range.t) query - val ast : (approx, Doc.Node.Ast.t) query - val goals : (approx, Pp.t Coq.Goals.reified_pp) query - val program : (approx, Declare.OblState.View.t Names.Id.Map.t) query - val messages : (approx, Doc.Node.Message.t list) query - val info : (approx, Doc.Node.Info.t) query - val completion : (string, string list) query - val in_state : st:Coq.State.t -> f:('a -> 'b option) -> 'a -> 'b option end let some x = Some x -let obind x f = Option.bind f x module Make (P : Point) : S with module P := P = struct type ('a, 'r) query = doc:Doc.t -> point:P.t -> 'a -> 'r option @@ -147,7 +138,29 @@ module Make (P : Point) : S with module P := P = struct find None doc.Doc.nodes let node = find +end + +module LC = Make (LineCol) +module O = Make (Offset) +(* XXX: We need to split this module in two: one that handles the extraction of + information from a document, and the other that further processes it, like + for goals, possibly executing Coq code. *) + +(* XXX: This needs fixing by having a better monad *) +let in_state ~st ~f node = + match Coq.State.in_state ~st ~f node with + | { r = Coq.Protect.R.Completed (Result.Ok res); feedback } -> + Io.Log.feedback feedback; + res + | { r = Coq.Protect.R.Completed (Result.Error _) | Coq.Protect.R.Interrupted + ; feedback + } -> + Io.Log.feedback feedback; + None + +(* Related to goal request *) +module Goals = struct let pr_goal st = let ppx env sigma x = let { Coq.Protect.E.r; feedback } = @@ -162,43 +175,11 @@ module Make (P : Point) : S with module P := P = struct let lemmas = Coq.State.lemmas ~st in Option.map (Coq.Goals.reify ~ppx) lemmas - let range ~doc ~point approx = - let node = find ~doc ~point approx in - Option.map Doc.Node.range node - - let ast ~doc ~point approx = - let node = find ~doc ~point approx in - Option.bind node Doc.Node.ast - - let in_state ~st ~f node = - match Coq.State.in_state ~st ~f node with - | { r = Coq.Protect.R.Completed (Result.Ok res); feedback } -> - Io.Log.feedback feedback; - res - | { r = Coq.Protect.R.Completed (Result.Error _) | Coq.Protect.R.Interrupted - ; feedback - } -> - Io.Log.feedback feedback; - None - - let goals ~doc ~point approx = - find ~doc ~point approx - |> obind (fun node -> - let st = node.Doc.Node.state in - in_state ~st ~f:pr_goal st) - - let program ~doc ~point approx = - find ~doc ~point approx - |> Option.map (fun node -> - let st = node.Doc.Node.state in - Coq.State.program ~st) - - let messages ~doc ~point approx = - find ~doc ~point approx |> Option.map Doc.Node.messages - - let info ~doc ~point approx = - find ~doc ~point approx |> Option.map Doc.Node.info + let goals ~st = in_state ~st ~f:pr_goal st + let program ~st = Coq.State.program ~st +end +module Completion = struct (* XXX: This belongs in Coq *) let pr_extref gr = match gr with @@ -209,16 +190,11 @@ module Make (P : Point) : S with module P := P = struct needed *) let to_qualid p = try Some (Libnames.qualid_of_string p) with _ -> None - let completion ~doc ~point prefix = - find ~doc ~point Exact - |> obind (fun node -> - in_state ~st:node.Doc.Node.state prefix ~f:(fun prefix -> - to_qualid prefix - |> obind (fun p -> - Nametab.completion_canditates p - |> List.map (fun x -> Pp.string_of_ppcmds (pr_extref x)) - |> some))) + let candidates ~st prefix = + let ( let* ) = Option.bind in + in_state ~st prefix ~f:(fun prefix -> + let* p = to_qualid prefix in + Nametab.completion_canditates p + |> List.map (fun x -> Pp.string_of_ppcmds (pr_extref x)) + |> some) end - -module LC = Make (LineCol) -module O = Make (Offset) diff --git a/fleche/info.mli b/fleche/info.mli index 57c79743..6854a4bf 100644 --- a/fleche/info.mli +++ b/fleche/info.mli @@ -45,15 +45,20 @@ module type S = sig type ('a, 'r) query = doc:Doc.t -> point:P.t -> 'a -> 'r option val node : (approx, Doc.Node.t) query - val range : (approx, Lang.Range.t) query - val ast : (approx, Doc.Node.Ast.t) query - val goals : (approx, Pp.t Coq.Goals.reified_pp) query - val program : (approx, Declare.OblState.View.t Names.Id.Map.t) query - val messages : (approx, Doc.Node.Message.t list) query - val info : (approx, Doc.Node.Info.t) query - val completion : (string, string list) query - val in_state : st:Coq.State.t -> f:('a -> 'b option) -> 'a -> 'b option 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 *) +val in_state : st:Coq.State.t -> f:('a -> 'b option) -> 'a -> 'b option + +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 +end + +module Completion : sig + val candidates : st:Coq.State.t -> string -> string list option +end