aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cbv.ml11
-rw-r--r--pretyping/evarconv.ml105
-rw-r--r--pretyping/nativenorm.ml6
-rw-r--r--pretyping/reductionops.ml16
-rw-r--r--pretyping/reductionops.mli2
-rw-r--r--pretyping/unification.ml15
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 =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:02:06 +0000