From b4d40a0ea9c44128d0bf6d36c516e8bec1d9ada4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 1 Mar 2023 05:00:09 +0100 Subject: [PATCH 1/3] [hover] Provide basic notation information on hover For now we print the key. --- CHANGES.md | 3 +++ controller/rq_common.ml | 3 +-- controller/rq_common.mli | 3 ++- controller/rq_definition.ml | 3 ++- controller/rq_hover.ml | 46 ++++++++++++++++++++++++++++++++----- 5 files changed, 48 insertions(+), 10 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index eab49ae5..12e9817d 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -22,6 +22,9 @@ - Add pointers to Windows installers (@ejgallego, #559) - Recognize `Goal` and `Definition $id : ... .` as proof starters (@ejgallego, #561, reported by @Zimmi48, fixes #548) + - Provide basic notation information on hover. This is intended for + people to build their own more refined notation feedback systems + (@ejgallego, #) # coq-lsp 0.1.7: Just-in-time ----------------------------- diff --git a/controller/rq_common.ml b/controller/rq_common.ml index 5f26749f..048ccbd3 100644 --- a/controller/rq_common.ml +++ b/controller/rq_common.ml @@ -36,11 +36,10 @@ let find_id s c = Lsp.Io.trace "find_id" ("start: " ^ string_of_int start); id_from_start s start -let get_id_at_point ~doc ~point = +let get_id_at_point ~contents ~point = let line, character = point in Lsp.Io.trace "get_id_at_point" ("l: " ^ string_of_int line ^ " c: " ^ string_of_int character); - let { Fleche.Doc.contents; _ } = doc in let { Fleche.Contents.lines; _ } = contents in if line <= Array.length lines then let line = Array.get lines line in diff --git a/controller/rq_common.mli b/controller/rq_common.mli index 90699acf..80ab0dde 100644 --- a/controller/rq_common.mli +++ b/controller/rq_common.mli @@ -5,4 +5,5 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -val get_id_at_point : doc:Fleche.Doc.t -> point:int * int -> string option +val get_id_at_point : + contents:Fleche.Contents.t -> point:int * int -> string option diff --git a/controller/rq_definition.ml b/controller/rq_definition.ml index c5856cbc..44dffcf0 100644 --- a/controller/rq_definition.ml +++ b/controller/rq_definition.ml @@ -6,6 +6,7 @@ (************************************************************************) let request ~(doc : Fleche.Doc.t) ~point = + let { Fleche.Doc.contents; _ } = doc in Option.cata (fun id_at_point -> let { Fleche.Doc.toc; _ } = doc in @@ -15,5 +16,5 @@ let request ~(doc : Fleche.Doc.t) ~point = Lsp.Core.Location.({ uri; range } |> to_yojson) | None -> `Null) `Null - (Rq_common.get_id_at_point ~doc ~point) + (Rq_common.get_id_at_point ~contents ~point) |> Result.ok diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml index 77e60aef..9c514f8f 100644 --- a/controller/rq_hover.ml +++ b/controller/rq_hover.ml @@ -122,22 +122,56 @@ let pp_typ id = function Format.(asprintf "```coq\n%s\n```" nt) let if_bool b l = if b then [ l ] else [] -let to_list = Option.cata (fun x -> [ x ]) [] +let to_list x = Option.cata (fun x -> [ x ]) [] x + +let info_type ~contents ~node ~point : string option = + Option.bind (Rq_common.get_id_at_point ~contents ~point) (fun id -> + Option.map (pp_typ id) (info_of_id_at_point ~node id)) + +let extract_def ~point:_ (def : Vernacexpr.definition_expr) : + Constrexpr.constr_expr list = + match def with + | Vernacexpr.ProveBody (_bl, et) -> [ et ] + | Vernacexpr.DefineBody (_bl, _, et, eb) -> [ et ] @ to_list eb + +let extract_pexpr ~point:_ (pexpr : Vernacexpr.proof_expr) : + Constrexpr.constr_expr list = + let _id, (_bl, et) = pexpr in + [ et ] + +let extract ~point ast = + match (Coq.Ast.to_coq ast).v.expr with + | Vernacexpr.(VernacSynPure (VernacDefinition (_, _, expr))) -> + extract_def ~point expr + | Vernacexpr.(VernacSynPure (VernacStartTheoremProof (_, pexpr))) -> + List.concat_map (extract_pexpr ~point) pexpr + | _ -> [] + +let ntn_key_info (_entry, key) = "notation: " ^ key + +let info_notation ~point (ast : Fleche.Doc.Node.Ast.t) = + (* XXX: Iterate over the results *) + match extract ~point ast.v with + | { CAst.v = Constrexpr.CNotation (_, key, _params); _ } :: _ -> + Some (ntn_key_info key) + | _ -> None + +let info_notation ~node ~point : string option = + Option.bind node.Fleche.Doc.Node.ast (info_notation ~point) let hover ~doc ~node ~point = let open Fleche in + let contents = doc.Fleche.Doc.contents in let range = Doc.Node.range node in let info = Doc.Node.info node in let range_string = Format.asprintf "%a" Lang.Range.pp range in let stats_string = Doc.Node.Info.print info in - let type_string = - Option.bind (Rq_common.get_id_at_point ~doc ~point) (fun id -> - Option.map (pp_typ id) (info_of_id_at_point ~node id)) - in + let type_string = info_type ~contents ~node ~point in + let notation_string = info_notation ~node ~point in let hovers = if_bool show_loc_info range_string @ if_bool !Config.v.show_stats_on_hover stats_string - @ to_list type_string + @ to_list type_string @ to_list notation_string in match hovers with | [] -> `Null From ea182d9ce5a8161f09a2f1bcdfd388c4166384c0 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 2 Oct 2023 03:33:03 +0200 Subject: [PATCH 2/3] [hover] Refactor towards a plugin system. We make the code modular, so it is ready to accommodate generic hover plugins. --- controller/rq_hover.ml | 97 ++++++++++++++++++++++++++++-------------- 1 file changed, 64 insertions(+), 33 deletions(-) diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml index 9c514f8f..86f4414c 100644 --- a/controller/rq_hover.ml +++ b/controller/rq_hover.ml @@ -7,9 +7,6 @@ open Lsp.Core -(* Debug parameters *) -let show_loc_info = false - (* Taken from printmod.ml, funny stuff! *) let build_ind_type mip = Inductive.type_of_inductive mip @@ -121,10 +118,9 @@ let pp_typ id = function let nt = Pp.string_of_ppcmds nt in Format.(asprintf "```coq\n%s\n```" nt) -let if_bool b l = if b then [ l ] else [] let to_list x = Option.cata (fun x -> [ x ]) [] x -let info_type ~contents ~node ~point : string option = +let info_type ~contents ~point ~node : string option = Option.bind (Rq_common.get_id_at_point ~contents ~point) (fun id -> Option.map (pp_typ id) (info_of_id_at_point ~node id)) @@ -156,40 +152,75 @@ let info_notation ~point (ast : Fleche.Doc.Node.Ast.t) = Some (ntn_key_info key) | _ -> None -let info_notation ~node ~point : string option = +let info_notation ~contents:_ ~point ~node : string option = Option.bind node.Fleche.Doc.Node.ast (info_notation ~point) -let hover ~doc ~node ~point = - let open Fleche in - let contents = doc.Fleche.Doc.contents in - let range = Doc.Node.range node in - let info = Doc.Node.info node in - let range_string = Format.asprintf "%a" Lang.Range.pp range in - let stats_string = Doc.Node.Info.print info in - let type_string = info_type ~contents ~node ~point in - let notation_string = info_notation ~node ~point in - let hovers = - if_bool show_loc_info range_string - @ if_bool !Config.v.show_stats_on_hover stats_string - @ to_list type_string @ to_list notation_string - in +open Fleche + +(* Hover handler *) +module Handler = struct + (** Returns [Some markdown] if there is some hover to match *) + type 'node h = + contents:Contents.t -> point:int * int -> node:'node -> string option + + type t = + | MaybeNode : Doc.Node.t option h -> t + | WithNode : Doc.Node.t h -> t +end + +module type HoverProvider = sig + val h : Handler.t +end + +module Loc_info : HoverProvider = struct + let enabled = false + + let h ~contents:_ ~point:_ ~node = + match node with + | None -> "no node here" + | Some node -> + let range = Doc.Node.range node in + Format.asprintf "%a" Lang.Range.pp range + + let h ~contents ~point ~node = + if enabled then Some (h ~contents ~point ~node) else None + + let h = Handler.MaybeNode h +end + +module Stats : HoverProvider = struct + let h ~contents:_ ~point:_ ~node = + if !Config.v.show_stats_on_hover then Some Doc.Node.(Info.print (info node)) + else None + + let h = Handler.WithNode h +end + +module Type : HoverProvider = struct + let h = Handler.WithNode info_type +end + +module Notation : HoverProvider = struct + let h = Handler.WithNode info_notation +end + +let handlers : Handler.t list = [ Loc_info.h; Stats.h; Type.h; Notation.h ] + +let handle_hover ~contents ~point ~node = function + | Handler.MaybeNode h -> h ~contents ~point ~node + | Handler.WithNode h -> + Option.bind node (fun node -> h ~contents ~point ~node) + +let hover ~doc ~point = + let contents = doc.Doc.contents in + let node = Info.LC.node ~doc ~point Exact in + let range = Option.map Doc.Node.range node in + let hovers = List.filter_map (handle_hover ~contents ~point ~node) handlers in match hovers with | [] -> `Null | hovers -> - let range = Some range in let value = String.concat "\n___\n" hovers in let contents = { HoverContents.kind = "markdown"; value } in HoverInfo.(to_yojson { contents; range }) -let hover ~doc ~point = - let node = Fleche.Info.LC.node ~doc ~point Exact in - (match node with - | None -> - if show_loc_info then - let contents = - { HoverContents.kind = "markdown"; value = "no node here" } - in - HoverInfo.(to_yojson { contents; range = None }) - else `Null - | Some node -> hover ~doc ~node ~point) - |> Result.ok +let hover ~doc ~point = hover ~doc ~point |> Result.ok From 1319a8f9e6b199407af01fcf01e6d7cb87f3d31a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 2 Oct 2023 03:43:16 +0200 Subject: [PATCH 3/3] [hover] Add a simple plugin system. This allows users to extend hover in a well-typed way. --- CHANGES.md | 3 ++- controller/rq_hover.ml | 21 +++++++++++++++------ controller/rq_hover.mli | 17 +++++++++++++++++ 3 files changed, 34 insertions(+), 7 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 12e9817d..6d26b336 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -24,7 +24,8 @@ (@ejgallego, #561, reported by @Zimmi48, fixes #548) - Provide basic notation information on hover. This is intended for people to build their own more refined notation feedback systems - (@ejgallego, #) + (@ejgallego, #562) + - Hover request can now be extended by plugins (@ejgallego, #562) # coq-lsp 0.1.7: Just-in-time ----------------------------- diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml index 86f4414c..c59d3715 100644 --- a/controller/rq_hover.ml +++ b/controller/rq_hover.ml @@ -204,18 +204,27 @@ module Notation : HoverProvider = struct let h = Handler.WithNode info_notation end -let handlers : Handler.t list = [ Loc_info.h; Stats.h; Type.h; Notation.h ] +module Register = struct + let handlers : Handler.t list ref = ref [] + let add fn = handlers := fn :: !handlers -let handle_hover ~contents ~point ~node = function - | Handler.MaybeNode h -> h ~contents ~point ~node - | Handler.WithNode h -> - Option.bind node (fun node -> h ~contents ~point ~node) + let handle ~contents ~point ~node = function + | Handler.MaybeNode h -> h ~contents ~point ~node + | Handler.WithNode h -> + Option.bind node (fun node -> h ~contents ~point ~node) + + let fire ~contents ~point ~node = + List.filter_map (handle ~contents ~point ~node) !handlers +end + +(* Register in-file hover plugins *) +let () = List.iter Register.add [ Loc_info.h; Stats.h; Type.h; Notation.h ] let hover ~doc ~point = let contents = doc.Doc.contents in let node = Info.LC.node ~doc ~point Exact in let range = Option.map Doc.Node.range node in - let hovers = List.filter_map (handle_hover ~contents ~point ~node) handlers in + let hovers = Register.fire ~contents ~point ~node in match hovers with | [] -> `Null | hovers -> diff --git a/controller/rq_hover.mli b/controller/rq_hover.mli index 6a2cecb5..7228fac7 100644 --- a/controller/rq_hover.mli +++ b/controller/rq_hover.mli @@ -6,3 +6,20 @@ (************************************************************************) val hover : Request.position + +open Fleche + +module Handler : sig + (** Returns [Some markdown] if there is some hover to match *) + type 'node h = + contents:Contents.t -> point:int * int -> node:'node -> string option + + type t = + | MaybeNode : Doc.Node.t option h -> t + | WithNode : Doc.Node.t h -> t +end + +(** Register a hover plugin *) +module Register : sig + val add : Handler.t -> unit +end