From fbb502242e7d0cb26439a981a8850180e1aa5998 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 26 Jul 2024 18:07:57 +0200
Subject: [PATCH] more debug

---
 dev/debugger_support.ml |  1 +
 dev/top_printers.ml     | 93 +++++++++++++++++++++++++++++++++--------
 2 files changed, 76 insertions(+), 18 deletions(-)

diff --git a/dev/debugger_support.ml b/dev/debugger_support.ml
index 898417dfd277c..2f9b13acadbfd 100644
--- a/dev/debugger_support.ml
+++ b/dev/debugger_support.ml
@@ -12,6 +12,7 @@ let rawdebug = ref false
 
 let () =
   Flags.in_debugger := true;
+  Goptions.set_bool_option_value ["Printing";"All"] true;
   Goptions.set_bool_option_value ["Printing";"Existential";"Instances"] true;
   Detyping.print_universes := true;
   Goptions.set_bool_option_value ["Printing";"Matching"] false;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 8028761e8af84..11ae4f8e9009e 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -331,38 +331,95 @@ let pr_rec_analysis x =
 
 let pp_rec_analysis x = pp (pr_rec_analysis x)
 
+let map_rtl f c = match kind c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _ | Int _ | Float _ | String _) -> c
+  | Cast (b,k,t) ->
+      let b' = f b in
+      let t' = f t in
+      if b'==b && t' == t then c
+      else mkCast (b', k, t')
+  | Prod (na,t,b) ->
+      let t' = f t in
+      let b' = f b in
+      if b'==b && t' == t then c
+      else mkProd (na, t', b')
+  | Lambda (na,t,b) ->
+      let t' = f t in
+      let b' = f b in
+      if b'==b && t' == t then c
+      else mkLambda (na, t', b')
+  | LetIn (na,b,t,k) ->
+      let b' = f b in
+      let t' = f t in
+      let k' = f k in
+      if b'==b && t' == t && k'==k then c
+      else mkLetIn (na, b', t', k')
+  | App (b,l) ->
+      let b' = f b in
+      let l' = Array.Smart.map f l in
+      if b'==b && l'==l then c
+      else mkApp (b', l')
+  | Proj (p,r,t) ->
+      let t' = f t in
+      if t' == t then c
+      else mkProj (p, r, t')
+  | Evar (e,l) ->
+      let l' = SList.Smart.map f l in
+      if l'==l then c
+      else mkEvar (e, l')
+  | Case (ci,u,pms,p,iv,b,bl) ->
+      let pms' = Array.Smart.map f pms in
+      let p' = map_return_predicate f p in
+      let iv' = map_invert f iv in
+      let b' = f b in
+      let bl' = map_branches f bl in
+      if b'==b && iv'==iv && p'==p && bl'==bl && pms'==pms then c
+      else mkCase (ci, u, pms', p', iv', b', bl')
+  | Fix (ln,(lna,tl,bl)) ->
+      let tl' = Array.Smart.map f tl in
+      let bl' = Array.Smart.map f bl in
+      if tl'==tl && bl'==bl then c
+      else mkFix (ln,(lna,tl',bl'))
+  | CoFix(ln,(lna,tl,bl)) ->
+      let tl' = Array.Smart.map f tl in
+      let bl' = Array.Smart.map f bl in
+      if tl'==tl && bl'==bl then c
+      else mkCoFix (ln,(lna,tl',bl'))
+  | Array(u,t,def,ty) ->
+    let t' = Array.Smart.map f t in
+    let def' = f def in
+    let ty' = f ty in
+    if def'==def && t==t' && ty==ty' then c
+    else mkArray(u,t',def',ty')
+
 let ppdebug d =
   let open Coqrecanalyser.RecAnalyser in
   let info, c = Constr.get_debug d in
   let info = ref info in
   let map = ref Int.Map.empty in
-  let mismatches = ref [] in
+  let annot s c =
+    let s = Id.of_string_soft ("(* "^s^" *)") in
+    mkApp (mkVar s, [|c|])
+  in
   let rec aux c =
     let i', cinf = step !info in
     info := i';
     match cinf with
-    | Fresh idx -> map := Int.Map.add idx c !map; Constr.iter aux c
+    | Fresh idx ->
+      map := Int.Map.add idx c !map;
+      let c = map_rtl aux c in
+      annot ("fresh " ^ string_of_int idx) c
     | Seen idx ->
       match Int.Map.find_opt idx !map with
-      | None -> mismatches := (idx,c,None) :: !mismatches
-      | Some c' -> if c != c' then mismatches := (idx,c,Some c') :: !mismatches
-  in
-  let () = aux c in
-  let data = Int.Map.bindings !map in
-  let pr_one (i,c) = hov 2 (int i ++ str " -> " ++ pr_constr c) in
-  let pr_mismatch (i,c,c') =
-    hov 2 (int i ++ str " ->" ++ spc() ++
-           surround (pr_constr c) ++ spc() ++
-           str "vs" ++ spc() ++
-           match c' with
-           | None -> str "nothing"
-           | Some c' -> surround (pr_constr c'))
+      | None -> annot ("MISSING seen " ^ string_of_int idx) c
+      | Some c' -> if c != c' then annot ("MISMATCH seen " ^ string_of_int idx) c
+        else annot ("seen " ^ string_of_int idx) c
   in
+  let c = aux c in
   let msg =
     str "is_done = " ++ bool (is_done !info) ++ fnl () ++
-    v 0 (prlist_with_sep spc pr_one data) ++
-    if CList.is_empty !mismatches then mt()
-    else (fnl() ++ str "mismatches:" ++ fnl() ++ v 0 (prlist_with_sep spc pr_mismatch !mismatches))
+    pr_constr c
   in
   pp msg