[hover] Display debug statistic for universes

New config option `show_universes_on_hover`, that will display
information about the universe graph for developer debug.

Results seem a bit mixed, more research is needed.

controller/rq_hover.ml

@@ -263,6 +263,20 @@ module InputHelp : HoverProvider = struct
   let h = Handler.MaybeNode input_help
 end
 
+module UniDiff = struct
+  let h ~token ~contents:_ ~point:_ ~(node : Fleche.Doc.Node.t) =
+    if !Fleche.Config.v.show_universes_on_hover then
+      match Coq.State.info_universes ~token ~st:node.state with
+      | Coq.Protect.{ E.r = R.Completed (Ok (nuniv, nconst)); feedback = _ } ->
+        Some
+          (Format.asprintf "number of univs: %4d | number of constraints: %5d"
+             nuniv nconst)
+      | _ -> None
+    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 +296,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

plugins/univdiff/dune

@@ -0,0 +1,4 @@
+(library
+ (name Unidiff_plugin)
+ (public_name coq-lsp.plugin.univdiff)
+ (libraries coq-lsp.fleche))

plugins/univdiff/main.ml

@@ -0,0 +1,75 @@
+open Fleche
+
+let extract_raw ~(contents : Contents.t) ~(range : Lang.Range.t) =
+  let start = range.start.offset in
+  let length = range.end_.offset - start in
+  (* We need to be careful here as Doc.t always adds a last empty node on EOF,
+     but somehow the offset of this node seems suspicious, it seems like the Coq
+     parser increases the offset by one, we need to investigate. *)
+  let length =
+    if String.length contents.raw < start + length then
+      String.length contents.raw - start
+    else length
+  in
+  String.sub contents.raw start length
+
+let rec dump_univs ~token ~contents fmt (nuniv_prev, nconst_prev)
+    (qed_total, qed_yes) (nodes : Doc.Node.t list) =
+  match nodes with
+  | [] -> Format.fprintf fmt "qed_total: %d / qed_yes: %d" qed_total qed_yes
+  | next :: nodes -> (
+    let st = next.state in
+    let raw = extract_raw ~contents ~range:next.range in
+    let qed_total = qed_total + if String.equal "Qed." raw then 1 else 0 in
+    match Coq.State.info_universes ~token ~st with
+    | Coq.Protect.{ E.r = R.Completed (Ok (nuniv, nconst)); feedback = _ } ->
+      let qed_yes =
+        qed_yes
+        +
+        if nuniv_prev <> nuniv || nconst_prev <> nconst then (
+          let raw = raw in
+          (* maybe trim above ? *)
+          Format.fprintf fmt "@[univs for \"%s\":@\n (%4d,%4d) {+%d, +%d}@\n@]"
+            raw nuniv nconst (nuniv - nuniv_prev) (nconst - nconst_prev);
+          if String.equal "Qed." raw then 1 else 0)
+        else 0
+      in
+      dump_univs ~token ~contents fmt (nuniv, nconst) (qed_total, qed_yes) nodes
+    | _ ->
+      Format.fprintf fmt "Error!! Terminating!! X_X O_O@\n%!";
+      ())
+
+let dump_univs ~token ~out_file (doc : Doc.t) =
+  let out = Stdlib.open_out out_file in
+  let fmt = Format.formatter_of_out_channel out in
+  (match Coq.State.info_universes ~token ~st:doc.root with
+  | Coq.Protect.{ E.r = R.Completed (Ok root); feedback = _ } ->
+    dump_univs ~token ~contents:doc.contents fmt root (0, 0) doc.nodes
+  | _ -> ());
+  Format.pp_print_flush fmt ();
+  Stdlib.close_out out
+
+let dump_univdiff ~io ~token ~(doc : Doc.t) =
+  let uri = doc.uri in
+  let uri_str = Lang.LUri.File.to_string_uri uri in
+  let out_file = Lang.LUri.File.to_string_file uri ^ ".unidiff" in
+  let lvl = Io.Level.info in
+  let ndiags = Doc.diags doc |> List.length in
+  let message =
+    Format.asprintf "[univdiff plugin] %d diags present for file..." ndiags
+  in
+  Io.Report.message ~io ~lvl ~message;
+  let message =
+    Format.asprintf "[univdiff plugin] dumping universe diff for %s ..." uri_str
+  in
+  Io.Report.message ~io ~lvl ~message;
+  let () = dump_univs ~token ~out_file doc in
+  let message =
+    Format.asprintf
+      "[univdiff plugin] dumping universe diff for %s was completed!" uri_str
+  in
+  Io.Report.message ~io ~lvl ~message;
+  ()
+
+let main () = Theory.Register.Completed.add dump_univdiff
+let () = main ()