[hover] Refactor providers into plugins, add basic notation display.

CHANGES.md

@@ -22,6 +22,10 @@
  - 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, #562)
+ - Hover request can now be extended by plugins (@ejgallego, #562)
 
 # coq-lsp 0.1.7: Just-in-time
 -----------------------------

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

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

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

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,41 +118,118 @@ 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 = Option.cata (fun x -> [ x ]) []
-
-let hover ~doc ~node ~point =
-  let open Fleche 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 hovers =
-    if_bool show_loc_info range_string
-    @ if_bool !Config.v.show_stats_on_hover stats_string
-    @ to_list type_string
-  in
+let to_list x = Option.cata (fun x -> [ x ]) [] x
+
+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))
+
+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 ~contents:_ ~point ~node : string option =
+  Option.bind node.Fleche.Doc.Node.ast (info_notation ~point)
+
+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
+
+module Register = struct
+  let handlers : Handler.t list ref = ref []
+  let add fn = handlers := fn :: !handlers
+
+  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 = Register.fire ~contents ~point ~node 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

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