Infrastructure for fine-grained debug flags

6 files changed, 66 insertions, 89 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 7930c3d634..02fb347d08 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -201,10 +201,7 @@ let cofixp_reducible flgs _ stk =
   else
     false
 
-let get_debug_cbv = Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~value:false
-    ~key:["Debug";"Cbv"]
+let debug_cbv = CDebug.create ~name:"Cbv" ()
 
 (* Reduction of primitives *)
 
@@ -525,7 +522,7 @@ and norm_head_ref k info env stack normt t =
   if red_set_ref info.reds normt then
     match cbv_value_cache info normt with
       | Declarations.Def body ->
-         if get_debug_cbv () then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt);
+         debug_cbv (fun () -> Pp.(str "Unfolding " ++ debug_pr_key normt));
          strip_appl (shift_value k body) stack
       | Declarations.Primitive op ->
         let c = match normt with
@@ -534,11 +531,11 @@ and norm_head_ref k info env stack normt t =
         in
         (PRIMITIVE(op,c,[||]),stack)
       | Declarations.OpaqueDef _ | Declarations.Undef _ ->
-         if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt);
+         debug_cbv (fun () -> Pp.(str "Not unfolding " ++ debug_pr_key normt));
          (VAL(0,make_constr_ref k normt t),stack)
   else
     begin
-      if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt);
+      debug_cbv (fun () -> Pp.(str "Not unfolding " ++ debug_pr_key normt));
       (VAL(0,make_constr_ref k normt t),stack)
     end
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 990e84e5a7..e1d6fff3e4 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -47,17 +47,9 @@ let default_flags env =
   let ts = default_transparent_state env in
   default_flags_of ts
 
-let debug_unification =
-  Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Debug";"Unification"]
-    ~value:false
-
-let debug_ho_unification =
-  Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Debug";"HO";"Unification"]
-    ~value:false
+let debug_unification = CDebug.create ~name:"unification" ()
+
+let debug_ho_unification = CDebug.create ~name:"ho-unification" ()
 
 (*******************************************)
 (* Functions to deal with impossible cases *)
@@ -808,9 +800,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
   in
   let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in
   (* Evar must be undefined since we have flushed evars *)
-  let () = if debug_unification () then
-             let open Pp in
-             Feedback.msg_debug (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in
+  let () = debug_unification (fun () -> Pp.(v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ()))) in
   match (flex_kind_of_term flags env evd term1 sk1,
          flex_kind_of_term flags env evd term2 sk2) with
     | Flexible (sp1,al1), Flexible (sp2,al2) ->
@@ -1288,17 +1278,17 @@ let apply_on_subterm env evd fixed f test c t =
               (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
               applyrec acc t
     else
-    (if debug_ho_unification () then
-     Feedback.msg_debug Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t);
+    (debug_ho_unification (fun () ->
+     Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t));
      let b, evd =
         try test env !evdref k c t
         with e when CErrors.noncritical e -> assert false in
-     if b then (if debug_ho_unification () then Feedback.msg_debug (Pp.str "succeeded");
+     if b then (debug_ho_unification (fun () -> Pp.str "succeeded");
                 let evd', fixed, t' = f !evdref !fixedref k t in
                 fixedref := fixed;
                 evdref := evd'; t')
      else (
-       if debug_ho_unification () then Feedback.msg_debug (Pp.str "failed");
+       debug_ho_unification (fun () -> Pp.str "failed");
        map_constr_with_binders_left_to_right env !evdref
         (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
         applyrec acc t))
@@ -1404,9 +1394,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
   let env_evar = evar_filtered_env env_rhs evi in
   let sign = named_context_val env_evar in
   let ctxt = evar_filtered_context evi in
-  if debug_ho_unification () then
-    (Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs);
-     Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar));
+  debug_ho_unification (fun () ->
+     Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs ++ fnl () ++
+         str"env evars: " ++ Termops.Internal.print_env env_evar));
   let args = List.map (nf_evar evd) args in
   let argsubst = List.map2 (fun decl c -> (NamedDecl.get_id decl, c)) ctxt args in
   let instance = evar_identity_subst evi in
@@ -1439,17 +1429,17 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
   let rec set_holes env_rhs evd fixed rhs = function
   | (id,idty,c,cty,evsref,filter,occs)::subst ->
      let c = nf_evar evd c in
-     if debug_ho_unification () then
-       Feedback.msg_debug Pp.(str"set holes for: " ++
+     debug_ho_unification (fun () ->
+       Pp.(str"set holes for: " ++
                                 prc env_rhs evd (mkVar id.binder_name) ++ spc () ++
                                 prc env_rhs evd c ++ str" in " ++
-                                prc env_rhs evd rhs);
+                                prc env_rhs evd rhs));
      let occ = ref 1 in
      let set_var evd fixed k inst =
        let oc = !occ in
-       if debug_ho_unification () then
-       (Feedback.msg_debug Pp.(str"Found one occurrence");
-        Feedback.msg_debug Pp.(str"cty: " ++ prc env_rhs evd c));
+       debug_ho_unification (fun () ->
+       Pp.(str"Found one occurrence" ++ fnl () ++
+           str"cty: " ++ prc env_rhs evd c));
        incr occ;
        match occs with
        | AtOccurrences occs ->
@@ -1458,10 +1448,10 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
        | Unspecified prefer_abstraction ->
           let evd, fixed, evty = set_holes env_rhs evd fixed cty subst in
           let evty = nf_evar evd evty in
-          if debug_ho_unification () then
-            Feedback.msg_debug Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++
-                                   str" of type: " ++ prc env_evar evd evty ++
-                                   str " for " ++ prc env_rhs evd c);
+          debug_ho_unification (fun () ->
+            Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++
+                str" of type: " ++ prc env_evar evd evty ++
+                str " for " ++ prc env_rhs evd c));
           let instance = Filter.filter_list filter instance in
           (* Allow any type lower than the variable's type as the
              abstracted subterm might have a smaller type, which could be
@@ -1477,8 +1467,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
           evd, fixed, mkEvar (evk, instance)
      in
      let evd, fixed, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in
-     if debug_ho_unification () then
-       Feedback.msg_debug Pp.(str"abstracted: " ++ prc env_rhs evd rhs');
+     debug_ho_unification (fun () ->
+       Pp.(str"abstracted: " ++ prc env_rhs evd rhs'));
      let () = check_selected_occs env_rhs evd c !occ occs in
      let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in
      set_holes env_rhs' evd fixed rhs' subst
@@ -1491,9 +1481,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
   (* Thin evars making the term typable in env_evar *)
   let evd, rhs' = thin_evars env_evar evd ctxt rhs' in
   (* We instantiate the evars of which the value is forced by typing *)
-  if debug_ho_unification () then
-    (Feedback.msg_debug Pp.(str"solve_evars on: " ++ prc env_evar evd rhs');
-     Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
+  debug_ho_unification (fun () ->
+    Pp.(str"solve_evars on: " ++ prc env_evar evd rhs' ++ fnl () ++
+        str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
   let evd,rhs' =
     try !solve_evars env_evar evd rhs'
     with e when Pretype_errors.precatchable_exception e ->
@@ -1501,18 +1491,18 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
       raise (TypingFailed evd) in
   let rhs' = nf_evar evd rhs' in
   (* We instantiate the evars of which the value is forced by typing *)
-  if debug_ho_unification () then
-    (Feedback.msg_debug Pp.(str"after solve_evars: " ++ prc env_evar evd rhs');
-     Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
+  debug_ho_unification (fun () ->
+    Pp.(str"after solve_evars: " ++ prc env_evar evd rhs' ++ fnl () ++
+    str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
 
   let rec abstract_free_holes evd = function
    | (id,idty,c,cty,evsref,_,_)::l ->
      let id = id.binder_name in
      let c = nf_evar evd c in
-     if debug_ho_unification () then
-       Feedback.msg_debug Pp.(str"abstracting: " ++
-                                prc env_rhs evd (mkVar id) ++ spc () ++
-                                prc env_rhs evd c);
+     debug_ho_unification (fun () ->
+       Pp.(str"abstracting: " ++
+             prc env_rhs evd (mkVar id) ++ spc () ++
+             prc env_rhs evd c));
      let rec force_instantiation evd = function
      | (evk,evty,inst,abstract)::evs ->
        let evk = Option.default evk (Evarutil.advance evd evk) in
@@ -1541,14 +1531,14 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
            with IllTypedInstance _ (* from instantiate_evar *) | TypingFailed _ ->
               user_err (Pp.str "Cannot find an instance.")
          else
-           ((if debug_ho_unification () then
+           ((debug_ho_unification (fun () ->
                let evi = Evd.find evd evk in
                let env = Evd.evar_env env_rhs evi in
-               Feedback.msg_debug Pp.(str"evar is defined: " ++
+               Pp.(str"evar is defined: " ++
                  int (Evar.repr evk) ++ spc () ++
                  prc env evd (match evar_body evi with Evar_defined c -> c
                    | Evar_empty -> assert false)));
-            evd)
+            evd))
        in force_instantiation evd evs
      | [] -> abstract_free_holes evd l
      in force_instantiation evd !evsref
@@ -1556,27 +1546,27 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
      if Evd.is_defined evd evk then
        (* Can happen due to dependencies: instantiating evars in the arguments of evk might
            instantiate evk itself. *)
-       (if debug_ho_unification () then
+       (debug_ho_unification (fun () ->
           begin
             let evi = Evd.find evd evk in
             let evenv = evar_env env_rhs evi in
             let body = match evar_body evi with Evar_empty -> assert false | Evar_defined c -> c in
-            Feedback.msg_debug Pp.(str"evar was defined already as: " ++ prc evenv evd body)
-          end;
+            Pp.(str"evar was defined already as: " ++ prc evenv evd body)
+          end);
         evd)
      else
        try
          let evi = Evd.find_undefined evd evk in
          let evenv = evar_env env_rhs evi in
          let rhs' = nf_evar evd rhs' in
-           if debug_ho_unification () then
-             Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++
-                                      prc evenv evd rhs');
+           debug_ho_unification (fun () ->
+             Pp.(str"abstracted type before second solve_evars: " ++
+                   prc evenv evd rhs'));
          (* solve_evars is not commuting with nf_evar, because restricting
              an evar might provide a more specific type. *)
           let evd, _ = !solve_evars evenv evd rhs' in
-          if debug_ho_unification () then
-            Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs'));
+          debug_ho_unification (fun () ->
+            Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs')));
           let flags = default_flags_of TransparentState.full in
             Evarsolve.instantiate_evar evar_unify flags env_rhs evd evk rhs'
          with IllTypedInstance _ -> raise (TypingFailed evd)
@@ -1629,11 +1619,10 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
   let t2 = apprec_nohdbeta flags env evd (whd_head_evar evd t2) in
   let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in
   let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in
-  let () = if debug_unification () then
-             let open Pp in
-             Feedback.msg_debug (v 0 (str "Heuristic:" ++ spc () ++
+  let () = debug_unification (fun () ->
+             Pp.(v 0 (str "Heuristic:" ++ spc () ++
                                 Termops.Internal.print_constr_env env evd t1 ++ cut () ++
-                                Termops.Internal.print_constr_env env evd t2 ++ cut ())) in
+                                Termops.Internal.print_constr_env env evd t2 ++ cut ()))) in
   let app_empty = Array.is_empty l1 && Array.is_empty l2 in
   match EConstr.kind evd term1, EConstr.kind evd term2 with
   | Evar (evk1,args1), (Rel _|Var _) when app_empty
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 92e412a537..28621aa92e 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -469,15 +469,15 @@ let start_profiler_linux profile_fn =
       Unix.stdin dev_null dev_null
   in
   (* doesn't seem to be a way to test whether process creation succeeded *)
-  if !Flags.debug then
-    Feedback.msg_debug (Pp.str (Format.sprintf "Native compute profiler started, pid = %d, output to: %s" profiler_pid profile_fn));
+  debug_native_compiler (fun () ->
+    Pp.str (Format.sprintf "Native compute profiler started, pid = %d, output to: %s" profiler_pid profile_fn));
   Some profiler_pid
 
 (* kill profiler via SIGINT *)
 let stop_profiler_linux m_pid =
   match m_pid with
   | Some pid -> (
-    let _ = if !Flags.debug then Feedback.msg_debug (Pp.str "Stopping native code profiler") in
+    let _ = debug_native_compiler (fun () -> Pp.str "Stopping native code profiler") in
     try
       Unix.kill pid Sys.sigint;
       let _ = Unix.waitpid [] pid in ()
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 54a47a252d..4083d3bc23 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -686,11 +686,7 @@ module CredNative = RedNative(CNativeEntries)
     contract_* in any case .
 *)
 
-let debug_RAKAM =
-  Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Debug";"RAKAM"]
-    ~value:false
+let debug_RAKAM = CDebug.create ~name:"RAKAM" ()
 
 let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) =
   let args = Stack.tail ci.ci_npar args in
@@ -709,18 +705,18 @@ let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) =
 let rec whd_state_gen flags env sigma =
   let open Context.Named.Declaration in
   let rec whrec (x, stack) : state =
-    let () = if debug_RAKAM () then
+    let () =
         let open Pp in
         let pr c = Termops.Internal.print_constr_env env sigma c in
-        Feedback.msg_debug
+        debug_RAKAM (fun () ->
                (h (str "<<" ++ pr x ++
                    str "|" ++ cut () ++ Stack.pr pr stack ++
-                   str ">>"))
+                   str ">>")))
     in
     let c0 = EConstr.kind sigma x in
     let fold () =
-      let () = if debug_RAKAM () then
-          let open Pp in Feedback.msg_debug (str "<><><><><>") in
+      let () = debug_RAKAM (fun () ->
+          let open Pp in str "<><><><><>") in
       ((EConstr.of_kind c0, stack))
     in
     match c0 with
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 41d16f1c3c..09bcc860d0 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -19,7 +19,7 @@ open Environ
 
 exception Elimconst
 
-val debug_RAKAM : unit -> bool
+val debug_RAKAM : CDebug.t
 
 module CredNative : Primred.RedNative with
   type elem = EConstr.t and type args = EConstr.t array and type evd = Evd.evar_map
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 83e46e3295..df0f49a033 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -49,11 +49,7 @@ let is_keyed_unification =
     ~key:["Keyed";"Unification"]
     ~value:false
 
-let debug_unification =
-  Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Debug";"Tactic";"Unification"]
-    ~value:false
+let debug_tactic_unification = CDebug.create ~name:"tactic-unification" ()
 
 (** Making this unification algorithm correct w.r.t. the evar-map abstraction
     breaks too much stuff. So we redefine incorrect functions here. *)
@@ -713,8 +709,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
     let cM = Evarutil.whd_head_evar sigma curm
     and cN = Evarutil.whd_head_evar sigma curn in
     let () =
-      if debug_unification () then
-        Feedback.msg_debug (
+      debug_tactic_unification (fun () ->
           Termops.Internal.print_constr_env curenv sigma cM ++ str" ~= " ++
           Termops.Internal.print_constr_env curenv sigma cN)
     in
@@ -1138,7 +1133,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
     else error_cannot_unify (fst curenvnb) sigma (cM,cN)
   in
 
-  if debug_unification () then Feedback.msg_debug (str "Starting unification");
+  debug_tactic_unification (fun () -> str "Starting unification");
   let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in
   try
   let res =
@@ -1165,11 +1160,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
     let a = match res with
     | Some sigma -> sigma, ms, es
     | None -> unirec_rec (env,0) cv_pb opt subst (fst m) (fst n) in
-    if debug_unification () then Feedback.msg_debug (str "Leaving unification with success");
+    debug_tactic_unification (fun () -> str "Leaving unification with success");
     a
   with e ->
     let e = Exninfo.capture e in
-    if debug_unification () then Feedback.msg_debug (str "Leaving unification with failure");
+    debug_tactic_unification (fun () -> str "Leaving unification with failure");
     Exninfo.iraise e
 
 let unify_0 env sigma pb flags c1 c2 =