Better debug printers for module paths.

Now distinguishes between bound modules (Top#X) and submodules (Top.X).

Could be useful for the regular printer as well (e.g. in error messages), but I
don't know what the compatibility constraints are, so leaving it as it is for
now.

4 files changed, 24 insertions, 7 deletions

diff --git a/dev/db b/dev/db
index f259b50eb..ece22b3f4 100644
--- a/dev/db
+++ b/dev/db
@@ -13,6 +13,7 @@ install_printer Top_printers.ppexistentialset
 install_printer Top_printers.ppintset
 install_printer Top_printers.pplab
 install_printer Top_printers.ppdir
+install_printer Top_printers.ppmbid
 install_printer Top_printers.ppmp
 install_printer Top_printers.ppkn
 install_printer Top_printers.ppcon
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f9f2e1b09..0900bb096 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -40,10 +40,10 @@ let ppid id = pp (pr_id id)
 let pplab l = pp (pr_lab l)
 let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
 let ppdir dir = pp (pr_dirpath dir)
-let ppmp mp = pp(str (string_of_mp mp))
+let ppmp mp = pp(str (ModPath.debug_to_string mp))
 let ppcon con = pp(debug_pr_con con)
 let ppproj con = pp(debug_pr_con (Projection.constant con))
-let ppkn kn = pp(pr_kn kn)
+let ppkn kn = pp(str (KerName.to_string kn))
 let ppmind kn = pp(debug_pr_mind kn)
 let ppind (kn,i) = pp(debug_pr_mind kn ++ str"," ++int i)
 let ppsp sp = pp(pr_path sp)
diff --git a/kernel/names.ml b/kernel/names.ml
index ae2b3b638..9e4e8cd61 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -204,7 +204,7 @@ struct
     DirPath.to_string p ^ "." ^ s
 
   let debug_to_string (i, s, p) =
-    "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">"
+    "<"^DirPath.to_string p ^"#" ^ s ^"#"^ string_of_int i^">"
 
   let compare (x : t) (y : t) =
     if x == y then 0
@@ -282,6 +282,11 @@ module ModPath = struct
     | MPbound uid -> MBId.to_string uid
     | MPdot (mp,l) -> to_string mp ^ "." ^ Label.to_string l
 
+  let rec debug_to_string = function
+    | MPfile sl -> DirPath.to_string sl
+    | MPbound uid -> MBId.debug_to_string uid
+    | MPdot (mp,l) -> debug_to_string mp ^ "." ^ Label.to_string l
+
   (** we compare labels first if both are MPdots *)
   let rec compare mp1 mp2 =
     if mp1 == mp2 then 0
@@ -375,12 +380,16 @@ module KerName = struct
   let modpath kn = kn.modpath
   let label kn = kn.knlabel
 
-  let to_string kn =
+  let to_string_gen mp_to_string kn =
     let dp =
       if DirPath.is_empty kn.dirpath then "."
       else "#" ^ DirPath.to_string kn.dirpath ^ "#"
     in
-    ModPath.to_string kn.modpath ^ dp ^ Label.to_string kn.knlabel
+    mp_to_string kn.modpath ^ dp ^ Label.to_string kn.knlabel
+
+  let to_string kn = to_string_gen ModPath.to_string kn
+
+  let debug_to_string kn = to_string_gen ModPath.debug_to_string kn
 
   let print kn = str (to_string kn)
 
@@ -500,9 +509,9 @@ module KerPair = struct
   let print kp = str (to_string kp)
 
   let debug_to_string = function
-    | Same kn -> "(" ^ KerName.to_string kn ^ ")"
+    | Same kn -> "(" ^ KerName.debug_to_string kn ^ ")"
     | Dual (knu,knc) ->
-      "(" ^ KerName.to_string knu ^ "," ^ KerName.to_string knc ^ ")"
+      "(" ^ KerName.debug_to_string knu ^ "," ^ KerName.debug_to_string knc ^ ")"
 
   let debug_print kp = str (debug_to_string kp)
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 7cc444375..77139f1c3 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -217,6 +217,9 @@ sig
 
   val to_string : t -> string
 
+  val debug_to_string : t -> string
+  (** Same as [to_string], but outputs information related to debug. *)
+
   val initial : t
   (** Name of the toplevel structure ([= MPfile initial_dir]) *)
 
@@ -244,6 +247,10 @@ sig
 
   (** Display *)
   val to_string : t -> string
+
+  val debug_to_string : t -> string
+  (** Same as [to_string], but outputs information related to debug. *)
+
   val print : t -> Pp.std_ppcmds
 
   (** Comparisons *)