Merge PR #13202: Infrastructure for fine-grained debug flags

Reviewed-by: gares
Ack-by: herbelin
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer
Ack-by: ejgallego

4 files changed, 25 insertions, 33 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 129b220680..6617f4726e 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -19,20 +19,12 @@ open Sorts
 open Constr
 open Context
 open Vars
-open Goptions
 open Tacmach
 open Util
 
 let init_size=5
 
-let cc_verbose=
-  declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Congruence";"Verbose"]
-    ~value:false
-
-let debug x =
-  if cc_verbose () then Feedback.msg_debug (x ())
+let debug_congruence = CDebug.create ~name:"congruence" ()
 
 (* Signature table *)
 
@@ -576,7 +568,7 @@ let add_inst state (inst,int_subst) =
   Control.check_for_interrupt ();
   if state.rew_depth > 0 then
   if is_redundant state inst.qe_hyp_id int_subst then
-    debug (fun () -> str "discarding redundant (dis)equality")
+    debug_congruence (fun () -> str "discarding redundant (dis)equality")
   else
     begin
       Identhash.add state.q_history inst.qe_hyp_id int_subst;
@@ -591,7 +583,7 @@ let add_inst state (inst,int_subst) =
             state.rew_depth<-pred state.rew_depth;
             if inst.qe_pol then
               begin
-                debug (fun () ->
+                debug_congruence (fun () ->
                    (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
                   (str "  [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++
                            pr_term state.env state.sigma s ++ str " == " ++ pr_term state.env state.sigma t ++ str "]"));
@@ -599,7 +591,7 @@ let add_inst state (inst,int_subst) =
               end
             else
               begin
-                debug (fun () ->
+                debug_congruence (fun () ->
                    (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
                   (str "  [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++
                            pr_term state.env state.sigma s ++ str " <> " ++ pr_term state.env state.sigma t ++ str "]"));
@@ -630,7 +622,7 @@ let join_path uf i j=
   min_path (down_path uf i [],down_path uf j [])
 
 let union state i1 i2 eq=
-  debug (fun () -> str "Linking " ++ pr_idx_term state.env state.sigma state.uf i1 ++
+  debug_congruence (fun () -> str "Linking " ++ pr_idx_term state.env state.sigma state.uf i1 ++
                  str " and " ++ pr_idx_term state.env state.sigma state.uf i2 ++ str ".");
   let r1= get_representative state.uf i1
   and r2= get_representative state.uf i2 in
@@ -670,7 +662,7 @@ let union state i1 i2 eq=
         | _,_ -> ()
 
 let merge eq state = (* merge and no-merge *)
-  debug
+  debug_congruence
     (fun () -> str "Merging " ++ pr_idx_term state.env state.sigma state.uf eq.lhs ++
        str " and " ++ pr_idx_term state.env state.sigma state.uf eq.rhs ++ str ".");
   let uf=state.uf in
@@ -683,7 +675,7 @@ let merge eq state = (* merge and no-merge *)
         union state j i (swap eq)
 
 let update t state = (* update 1 and 2 *)
-  debug
+  debug_congruence
     (fun () -> str "Updating term " ++ pr_idx_term state.env state.sigma state.uf t ++ str ".");
   let (i,j) as sign = signature state.uf t in
   let (u,v) = subterms state.uf t in
@@ -745,7 +737,7 @@ let process_constructor_mark t i rep pac state =
             end
 
 let process_mark t m state =
-  debug
+  debug_congruence
     (fun () -> str "Processing mark for term " ++ pr_idx_term state.env state.sigma state.uf t ++ str ".");
   let i=find state.uf t in
   let rep=get_representative state.uf i in
@@ -766,7 +758,7 @@ let check_disequalities state =
           if Int.equal (find uf dis.lhs) (find uf dis.rhs) then (str "Yes", Some dis)
           else (str "No", check_aux q)
         in
-        let _ = debug
+        let _ = debug_congruence
         (fun () -> str "Checking if " ++ pr_idx_term state.env state.sigma state.uf dis.lhs ++ str " = " ++
          pr_idx_term state.env state.sigma state.uf dis.rhs ++ str " ... " ++ info) in
         ans
@@ -953,7 +945,7 @@ let find_instances state =
   let pb_stack= init_pb_stack state in
   let res =ref [] in
   let _ =
-    debug (fun () -> str "Running E-matching algorithm ... ");
+    debug_congruence (fun () -> str "Running E-matching algorithm ... ");
     try
       while true do
         Control.check_for_interrupt ();
@@ -964,7 +956,7 @@ let find_instances state =
     !res
 
 let rec execute first_run state =
-  debug (fun () -> str "Executing ... ");
+  debug_congruence (fun () -> str "Executing ... ");
   try
     while
       Control.check_for_interrupt ();
@@ -974,7 +966,7 @@ let rec execute first_run state =
         None ->
           if not(Int.Set.is_empty state.pa_classes) then
             begin
-              debug (fun () -> str "First run was incomplete, completing ... ");
+              debug_congruence (fun () -> str "First run was incomplete, completing ... ");
               complete state;
               execute false state
             end
@@ -989,12 +981,12 @@ let rec execute first_run state =
                   end
                 else
               begin
-                debug (fun () -> str "Out of instances ... ");
+                debug_congruence (fun () -> str "Out of instances ... ");
                 None
               end
             else
               begin
-                debug (fun () -> str "Out of depth ... ");
+                debug_congruence (fun () -> str "Out of depth ... ");
                 None
               end
       | Some dis -> Some
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 3270f74479..047756deef 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -121,7 +121,7 @@ val term_equal : term -> term -> bool
 
 val constr_of_term : term -> constr
 
-val debug : (unit -> Pp.t) -> unit
+val debug_congruence : CDebug.t
 
 val forest : state -> forest
 
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 53d8c5bdd9..e7e0822916 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -95,13 +95,13 @@ let pinject p c n a =
    p_rule=Inject(p,c,n,a)}
 
 let rec equal_proof env sigma uf i j=
-  debug (fun () -> str "equal_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
+  debug_congruence (fun () -> str "equal_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   if i=j then prefl (term uf i) else
     let (li,lj)=join_path uf i j in
     ptrans (path_proof env sigma uf i li) (psym (path_proof env sigma uf j lj))
 
 and edge_proof env sigma uf ((i,j),eq)=
-  debug (fun () -> str "edge_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
+  debug_congruence (fun () -> str "edge_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   let pi=equal_proof env sigma uf i eq.lhs in
   let pj=psym (equal_proof env sigma uf j eq.rhs) in
   let pij=
@@ -117,7 +117,7 @@ and edge_proof env sigma uf ((i,j),eq)=
   ptrans (ptrans pi pij) pj
 
 and constr_proof env sigma uf i ipac=
-  debug (fun () -> str "constr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20));
+  debug_congruence (fun () -> str "constr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20));
   let t=find_oldest_pac uf i ipac in
   let eq_it=equal_proof env sigma uf i t in
   if ipac.args=[] then
@@ -130,20 +130,20 @@ and constr_proof env sigma uf i ipac=
     ptrans eq_it (pcongr p (prefl targ))
 
 and path_proof env sigma uf i l=
-  debug (fun () -> str "path_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ str "{" ++
+  debug_congruence (fun () -> str "path_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ str "{" ++
            (prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}");
   match l with
   | [] -> prefl (term uf i)
   | x::q->ptrans (path_proof env sigma uf (snd (fst x)) q) (edge_proof env sigma uf x)
 
 and congr_proof env sigma uf i j=
-  debug (fun () -> str "congr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
+  debug_congruence (fun () -> str "congr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   let (i1,i2) = subterms uf i
   and (j1,j2) = subterms uf j in
   pcongr (equal_proof env sigma uf i1 j1) (equal_proof env sigma uf i2 j2)
 
 and ind_proof env sigma uf i ipac j jpac=
-   debug (fun () -> str "ind_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
+   debug_congruence (fun () -> str "ind_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   let p=equal_proof env sigma uf i j
   and p1=constr_proof env sigma uf i ipac
   and p2=constr_proof env sigma uf j jpac in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 72f77508d8..341fde7b77 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -420,16 +420,16 @@ let cc_tactic depth additionnal_terms =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     Coqlib.(check_required_library logic_module_name);
-    let _ = debug (fun () -> Pp.str "Reading goal ...") in
+    let _ = debug_congruence (fun () -> Pp.str "Reading goal ...") in
     let state = make_prb gl depth additionnal_terms in
-    let _ = debug (fun () -> Pp.str "Problem built, solving ...") in
+    let _ = debug_congruence (fun () -> Pp.str "Problem built, solving ...") in
     let sol = execute true state in
-    let _ = debug (fun () -> Pp.str "Computation completed.") in
+    let _ = debug_congruence (fun () -> Pp.str "Computation completed.") in
     let uf=forest state in
     match sol with
       None -> Tacticals.New.tclFAIL 0 (str "congruence failed")
     | Some reason ->
-      debug (fun () -> Pp.str "Goal solved, generating proof ...");
+      debug_congruence (fun () -> Pp.str "Goal solved, generating proof ...");
       match reason with
         Discrimination (i,ipac,j,jpac) ->
         let p=build_proof (Tacmach.New.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in