[hover] Display debug statistic for universes

CHANGES.md

@@ -4,7 +4,7 @@
  - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI
    dependency, and will greatly easy the development of tools that
    require AST manipulation (@ejgallego, #698)
- - [fleche] Remove 8.16 compatibility layer (@ejgallgo, #747)
+ - [fleche] Remove 8.16 compatibility layer (@ejgallego, #747)
  - [fleche] Preserve view hint across document changes. With this
    change, we get local continuous checking mode when the view-port
    heuristic is enabled (@ejgallego, #748)
@@ -47,6 +47,8 @@
  - [diagnostics] Ensure extra diagnostics info is present in all
    errors, not only on those sentences that did parse successfully
    (@ejgallego, Diego Rivera, #772)
+ - [hover] New option `show_universes_on_hover` that will display
+   universe data on hover (@ejgallego, @SkySkimmer, #666)
 
 # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
 ----------------------------------------------------

controller/rq_hover.ml

@@ -263,6 +263,33 @@ module InputHelp : HoverProvider = struct
   let h = Handler.MaybeNode input_help
 end
 
+module UniDiff = struct
+  let show_unidiff ~token ?diff ~st () =
+    let nuniv_prev, nconst_prev =
+      match diff with
+      | Some st -> (
+        match Coq.State.info_universes ~token ~st with
+        | Coq.Protect.{ E.r = R.Completed (Ok (nuniv, nconst)); feedback = _ }
+          -> (nuniv, nconst)
+        | _ -> (0, 0))
+      | None -> (0, 0)
+    in
+    match Coq.State.info_universes ~token ~st with
+    | Coq.Protect.{ E.r = R.Completed (Ok (nuniv, nconst)); feedback = _ } ->
+      Some
+        (Format.asprintf "@[univ data (%4d,%4d) {+%d, +%d}@\n@]" nuniv nconst
+           (nuniv - nuniv_prev) (nconst - nconst_prev))
+    | _ -> None
+
+  let h ~token ~contents:_ ~point:_ ~(node : Fleche.Doc.Node.t) =
+    if !Fleche.Config.v.show_universes_on_hover then
+      let diff = Option.map Fleche.Doc.Node.state node.prev in
+      show_unidiff ~token ?diff ~st:node.state ()
+    else None
+
+  let h = Handler.WithNode h
+end
+
 module Register = struct
   let handlers : Handler.t list ref = ref []
   let add fn = handlers := fn :: !handlers
@@ -282,7 +309,7 @@ end
 (* Register in-file hover plugins *)
 let () =
   List.iter Register.add
-    [ Loc_info.h; Stats.h; Type.h; Notation.h; InputHelp.h ]
+    [ Loc_info.h; Stats.h; Type.h; Notation.h; InputHelp.h; UniDiff.h ]
 
 let hover ~token ~(doc : Fleche.Doc.t) ~point =
   let node = Info.LC.node ~doc ~point Exact in

controller/rq_hover.mli

@@ -41,3 +41,8 @@ end
 module Register : sig
   val add : Handler.t -> unit
 end
+
+(** Auxiliary functions *)
+module UniDiff : sig
+  (** [info_universes ~node] returns [nunivs, nconstraints] *)
+end

coq/state.ml

@@ -135,3 +135,23 @@ let admit_goal ~st () =
     { st with interp = { st.interp with lemmas } }
 
 let admit_goal ~token ~st = Protect.eval ~token ~f:(admit_goal ~st) ()
+
+let count_edges univ =
+  let univ = UGraph.repr univ in
+  Univ.Level.Map.fold
+    (fun _ node acc ->
+      acc
+      +
+      match node with
+      | UGraph.Alias _ -> 1
+      | Node m -> Univ.Level.Map.cardinal m)
+    univ
+    (Univ.Level.Map.cardinal univ)
+
+let info_universes ~token ~st =
+  let open Protect.E.O in
+  let+ univ = in_state ~token ~st ~f:Global.universes () in
+  let univs = UGraph.domain univ in
+  let nuniv = Univ.Level.Set.cardinal univs in
+  let nconst = count_edges univ in
+  (nuniv, nconst)

coq/state.mli

@@ -38,6 +38,10 @@ val admit : token:Limits.Token.t -> st:t -> (t, Loc.t) Protect.E.t
 (** Admit the current sub-goal *)
 val admit_goal : token:Limits.Token.t -> st:t -> (t, Loc.t) Protect.E.t
 
+(** Info about universes *)
+val info_universes :
+  token:Limits.Token.t -> st:t -> (int * int, Loc.t) Protect.E.t
+
 (** Extra / interanl *)
 val marshal_in : in_channel -> t
 

editor/code/package.json

@@ -217,6 +217,11 @@
             "type": "boolean",
             "default": false,
             "description": "Show parsing information for a sentence on hover."
+          },
+          "coq-lsp.show_universes_on_hover": {
+            "type": "boolean",
+            "default": false,
+            "description": "Show universe information and diff for a sentence on hover."
           }
         }
       },

editor/code/src/config.ts

@@ -13,6 +13,7 @@ export interface CoqLspServerConfig {
   pp_type: 0 | 1 | 2;
   show_stats_on_hover: boolean;
   show_loc_info_on_hover: boolean;
+  show_universes_on_hover: boolean;
   check_only_on_request: boolean;
   send_perf_data: boolean;
 }
@@ -35,6 +36,7 @@ export namespace CoqLspServerConfig {
       pp_type: wsConfig.pp_type,
       show_stats_on_hover: wsConfig.show_stats_on_hover,
       show_loc_info_on_hover: wsConfig.show_loc_info_on_hover,
+      show_universes_on_hover: wsConfig.show_universes_on_hover,
       check_only_on_request: wsConfig.check_only_on_request,
       send_perf_data: wsConfig.send_perf_data,
     };

fleche/config.ml

@@ -39,6 +39,8 @@ type t =
   ; show_stats_on_hover : bool [@default false]  (** Show stats on hover *)
   ; show_loc_info_on_hover : bool [@default false]
         (** Show loc info on hover *)
+  ; show_universes_on_hover : bool [@default false]
+        (** Show universe data on hover *)
   ; pp_json : bool [@default false]
         (** Whether to pretty print the protocol JSON on the wire *)
   ; send_perf_data : bool [@default true]
@@ -71,6 +73,7 @@ let default =
   ; pp_type = 0
   ; show_stats_on_hover = false
   ; show_loc_info_on_hover = false
+  ; show_universes_on_hover = false
   ; verbosity = 2
   ; pp_json = false
   ; send_perf_data = true