[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.
ejgallego · Oct 13, 2023 · c08bfcd · c08bfcd
1 parent 34e7e11
commit c08bfcd
Show file tree

Hide file tree

Showing 4 changed files with 60 additions and 69 deletions.
diff --git a/controller/rq_goals.ml b/controller/rq_goals.ml
@@ -35,16 +35,26 @@ 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
   let textDocument = Lsp.Doc.VersionedTextDocumentIdentifier.{ uri; version } in
   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
@@ -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
@@ -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
@@ -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