aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/ccalgo.ml36
-rw-r--r--plugins/cc/ccalgo.mli2
-rw-r--r--plugins/cc/ccproof.ml12
-rw-r--r--plugins/cc/cctac.ml8
-rw-r--r--plugins/micromega/zify.ml30
-rw-r--r--plugins/nsatz/utile.ml6
-rw-r--r--plugins/ssr/ssrcommon.ml4
-rw-r--r--plugins/ssr/ssrelim.ml28
-rw-r--r--plugins/ssr/ssrequality.ml22
-rw-r--r--plugins/ssr/ssrfwd.ml14
-rw-r--r--plugins/ssr/ssripats.ml16
-rw-r--r--plugins/ssr/ssrprinters.ml14
-rw-r--r--plugins/ssr/ssrprinters.mli3
-rw-r--r--plugins/ssr/ssrview.ml24
14 files changed, 96 insertions, 123 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
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index d1403558ad..61966b60c0 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -14,7 +14,7 @@ open Pp
open Lazy
module NamedDecl = Context.Named.Declaration
-let debug = false
+let debug_zify = CDebug.create ~name:"zify" ()
(* The following [constr] are necessary for constructing the proof terms *)
@@ -805,12 +805,11 @@ let pp_prf prf =
let interp_prf evd inj source prf =
let t, prf' = interp_prf evd inj source prf in
- if debug then
- Feedback.msg_debug
+ debug_zify (fun () ->
Pp.(
str "interp_prf " ++ gl_pr_constr inj.EInjT.inj ++ str " "
++ gl_pr_constr source ++ str " = " ++ gl_pr_constr t ++ str " by "
- ++ gl_pr_constr prf' ++ str " from " ++ pp_prf prf ++ fnl ());
+ ++ gl_pr_constr prf' ++ str " from " ++ pp_prf prf ++ fnl ()));
(t, prf')
let mkvar evd inj e =
@@ -888,13 +887,12 @@ let app_unop evd src unop arg prf =
let app_unop evd src unop arg prf =
let res = app_unop evd src unop arg prf in
- if debug then
- Feedback.msg_debug
+ debug_zify (fun () ->
Pp.(
str "\napp_unop "
++ pp_prf evd unop.EUnOpT.inj1_t arg prf
++ str " => "
- ++ pp_prf evd unop.EUnOpT.inj2_t src res);
+ ++ pp_prf evd unop.EUnOpT.inj2_t src res));
res
let app_binop evd src binop arg1 prf1 arg2 prf2 =
@@ -1066,8 +1064,7 @@ let match_operator env evd hd args (t, d) =
let pp_trans_expr env evd e res =
let {deriv = inj} = get_injection env evd e.typ in
- if debug then
- Feedback.msg_debug Pp.(str "\ntrans_expr " ++ pp_prf evd inj e.constr res);
+ debug_zify (fun () -> Pp.(str "\ntrans_expr " ++ pp_prf evd inj e.constr res));
res
let declared_term env evd hd args =
@@ -1187,7 +1184,7 @@ let trans_binrel evd src rop a1 prf1 a2 prf2 =
let trans_binrel evd src rop a1 prf1 a2 prf2 =
let res = trans_binrel evd src rop a1 prf1 a2 prf2 in
- if debug then Feedback.msg_debug Pp.(str "\ntrans_binrel " ++ pp_prfp res);
+ debug_zify (fun () -> Pp.(str "\ntrans_binrel " ++ pp_prfp res));
res
let mkprf t p =
@@ -1199,11 +1196,10 @@ let mkprf t p =
let mkprf t p =
let t', p = mkprf t p in
- if debug then
- Feedback.msg_debug
+ debug_zify (fun () ->
Pp.(
str "mkprf " ++ gl_pr_constr t ++ str " <-> " ++ gl_pr_constr t'
- ++ str " by " ++ gl_pr_constr p);
+ ++ str " by " ++ gl_pr_constr p));
(t', p)
let trans_bin_prop op_constr op_iff t1 p1 t2 p2 =
@@ -1221,7 +1217,7 @@ let trans_bin_prop op_constr op_iff t1 p1 t2 p2 =
let trans_bin_prop op_constr op_iff t1 p1 t2 p2 =
let prf = trans_bin_prop op_constr op_iff t1 p1 t2 p2 in
- if debug then Feedback.msg_debug (pp_prfp prf);
+ debug_zify (fun () -> pp_prfp prf);
prf
let trans_un_prop op_constr op_iff p1 prf1 =
@@ -1285,8 +1281,7 @@ let trans_hyps env evd l =
[] l
let trans_hyp h t0 prfp =
- if debug then
- Feedback.msg_debug Pp.(str "trans_hyp: " ++ pp_prfp prfp ++ fnl ());
+ debug_zify (fun () -> Pp.(str "trans_hyp: " ++ pp_prfp prfp ++ fnl ()));
match prfp with
| IProof -> Tacticals.New.tclIDTAC (* Should detect before *)
| CProof t' ->
@@ -1313,8 +1308,7 @@ let trans_hyp h t0 prfp =
(tclTHEN (Tactics.clear [h]) (Tactics.rename_hyp [(h', h)])))))
let trans_concl prfp =
- if debug then
- Feedback.msg_debug Pp.(str "trans_concl: " ++ pp_prfp prfp ++ fnl ());
+ debug_zify (fun () -> Pp.(str "trans_concl: " ++ pp_prfp prfp ++ fnl ()));
match prfp with
| IProof -> Tacticals.New.tclIDTAC
| CProof t ->
diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml
index 1caa042db6..19bdcbac58 100644
--- a/plugins/nsatz/utile.ml
+++ b/plugins/nsatz/utile.ml
@@ -1,9 +1,9 @@
(* Printing *)
let pr x =
- if !Flags.debug then (Format.printf "@[%s@]" x; flush(stdout);)else ()
+ if CDebug.(get_flag misc) then (Format.printf "@[%s@]" x; flush(stdout);)else ()
let prt0 s = () (* print_string s;flush(stdout)*)
-let sinfo s = if !Flags.debug then Feedback.msg_debug (Pp.str s)
-let info s = if !Flags.debug then Feedback.msg_debug (Pp.str (s ()))
+let sinfo s = if CDebug.(get_flag misc) then Feedback.msg_debug (Pp.str s)
+let info s = if CDebug.(get_flag misc) then Feedback.msg_debug (Pp.str (s ()))
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 4d57abb465..41fd96ccb5 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -252,7 +252,7 @@ let interp_refine ist gl rc =
in
let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in
(* ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *)
- ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr_env (pf_env gl) sigma c));
+ debug_ssr (fun () -> str"c@interp_refine=" ++ Printer.pr_econstr_env (pf_env gl) sigma c);
(sigma, (sigma, c))
@@ -1207,7 +1207,7 @@ let gentac gen =
Proofview.V82.tactic begin fun gl ->
(* ppdebug(lazy(str"sigma@gentac=" ++ pr_evar_map None (project gl))); *)
let conv, _, cl, c, clr, ucst,gl = pf_interp_gen_aux gl false gen in
- ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c));
+ debug_ssr (fun () -> str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c);
let gl = pf_merge_uc ucst gl in
if conv
then tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl)) (old_cleartac clr) gl
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 582c45cde1..78a59abda9 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -126,17 +126,17 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
fun (oc, orig_clr, occ, c_gen) -> pfLIFT begin fun gl ->
let orig_gl, concl, env = gl, pf_concl gl, pf_env gl in
- ppdebug(lazy(Pp.str(if is_case then "==CASE==" else "==ELIM==")));
+ debug_ssr (fun () -> (Pp.str(if is_case then "==CASE==" else "==ELIM==")));
let fire_subst gl t = Reductionops.nf_evar (project gl) t in
let is_undef_pat = function
| sigma, T t -> EConstr.isEvar sigma (EConstr.of_constr t)
| _ -> false in
let match_pat env p occ h cl =
let sigma0 = project orig_gl in
- ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern env p));
+ debug_ssr (fun () -> Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern env p));
let (c,ucst), cl =
fill_occ_pattern ~raise_NoMatch:true env sigma0 (EConstr.Unsafe.to_constr cl) p occ h in
- ppdebug(lazy Pp.(str" got: " ++ pr_constr_env env sigma0 c));
+ debug_ssr (fun () -> Pp.(str" got: " ++ pr_constr_env env sigma0 c));
c, EConstr.of_constr cl, ucst in
let mkTpat gl t = (* takes a term, refreshes it and makes a T pattern *)
let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in
@@ -212,10 +212,10 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
let renamed_tys =
Array.mapi (fun j (ctx, cty) ->
let t = Term.it_mkProd_or_LetIn cty ctx in
- ppdebug(lazy Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t));
+ debug_ssr (fun () -> Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t));
let t = Arguments_renaming.rename_type t
(GlobRef.ConstructRef((kn,i),j+1)) in
- ppdebug(lazy Pp.(str"Done Search " ++ Printer.pr_constr_env env (project gl) t));
+ debug_ssr (fun () -> Pp.(str"Done Search " ++ Printer.pr_constr_env env (project gl) t));
t)
tys
in
@@ -241,8 +241,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
in
let () =
let sigma = project gl in
- ppdebug(lazy Pp.(str"elim= "++ pr_econstr_pat env sigma elim));
- ppdebug(lazy Pp.(str"elimty= "++ pr_econstr_pat env sigma elimty)) in
+ debug_ssr (fun () -> Pp.(str"elim= "++ pr_econstr_pat env sigma elim));
+ debug_ssr (fun () -> Pp.(str"elimty= "++ pr_econstr_pat env sigma elimty)) in
let open EConstr in
let inf_deps_r = match kind_of_type (project gl) elimty with
| AtomicType (_, args) -> List.rev (Array.to_list args)
@@ -301,7 +301,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
| Some (c, _, _,gl) -> Some(true, gl)
| None -> None in
first [try_c_last_arg;try_c_last_pattern] in
- ppdebug(lazy Pp.(str"c_is_head_p= " ++ bool c_is_head_p));
+ debug_ssr (fun () -> Pp.(str"c_is_head_p= " ++ bool c_is_head_p));
let gl, predty = pfe_type_of gl pred in
(* Patterns for the inductive types indexes to be bound in pred are computed
* looking at the ones provided by the user and the inferred ones looking at
@@ -321,7 +321,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
loop (patterns @ [i, p, inf_t, occ])
(clr_t @ clr) (i+1) (deps, inf_deps)
| [], c :: inf_deps ->
- ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_econstr_pat env (project gl) c));
+ debug_ssr (fun () -> Pp.(str"adding inf pattern " ++ pr_econstr_pat env (project gl) c));
loop (patterns @ [i, mkTpat gl c, c, allocc])
clr (i+1) ([], inf_deps)
| _::_, [] -> errorstrm Pp.(str "Too many dependent abstractions") in
@@ -337,8 +337,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
loop [] orig_clr (List.length head_p+1) (List.rev deps, inf_deps_r) in
head_p @ patterns, Util.List.uniquize clr, gl
in
- ppdebug(lazy Pp.(pp_concat (str"patterns=") (List.map pp_pat patterns)));
- ppdebug(lazy Pp.(pp_concat (str"inf. patterns=") (List.map (pp_inf_pat gl) patterns)));
+ debug_ssr (fun () -> Pp.(pp_concat (str"patterns=") (List.map pp_pat patterns)));
+ debug_ssr (fun () -> Pp.(pp_concat (str"inf. patterns=") (List.map (pp_inf_pat gl) patterns)));
(* Predicate generation, and (if necessary) tactic to generalize the
* equation asked by the user *)
let elim_pred, gen_eq_tac, clr, gl =
@@ -348,7 +348,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
let match_or_postpone (cl, gl, post) (h, p, inf_t, occ) =
let p = unif_redex gl p inf_t in
if is_undef_pat p then
- let () = ppdebug(lazy Pp.(str"postponing " ++ pp_pattern env p)) in
+ let () = debug_ssr (fun () -> Pp.(str"postponing " ++ pp_pattern env p)) in
cl, gl, post @ [h, p, inf_t, occ]
else try
let c, cl, ucst = match_pat env p occ h cl in
@@ -420,8 +420,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
else gl, concl in
concl, gen_eq_tac, clr, gl in
let gl, pty = pf_e_type_of gl elim_pred in
- ppdebug(lazy Pp.(str"elim_pred=" ++ pp_term gl elim_pred));
- ppdebug(lazy Pp.(str"elim_pred_ty=" ++ pp_term gl pty));
+ debug_ssr (fun () -> Pp.(str"elim_pred=" ++ pp_term gl elim_pred));
+ debug_ssr (fun () -> Pp.(str"elim_pred_ty=" ++ pp_term gl pty));
let gl = pf_unify_HO gl pred elim_pred in
let elim = fire_subst gl elim in
let gl = pf_resolve_typeclasses ~where:elim ~fail:false gl in
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 0008d31ffd..92a481dd18 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -76,7 +76,7 @@ let simpltac s = Proofview.Goal.enter (fun _ -> simpltac s)
(** The "congr" tactic *)
let interp_congrarg_at ist gl n rf ty m =
- ppdebug(lazy Pp.(str"===interp_congrarg_at==="));
+ debug_ssr (fun () -> Pp.(str"===interp_congrarg_at==="));
let congrn, _ = mkSsrRRef "nary_congruence" in
let args1 = mkRnat n :: mkRHoles n @ [ty] in
let args2 = mkRHoles (3 * n) in
@@ -84,7 +84,7 @@ let interp_congrarg_at ist gl n rf ty m =
if i + n > m then None else
try
let rt = mkRApp congrn (args1 @ mkRApp rf (mkRHoles i) :: args2) in
- ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) (project gl) rt));
+ debug_ssr (fun () -> Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) (project gl) rt));
Some (interp_refine ist gl rt)
with _ -> loop (i + 1) in
loop 0
@@ -92,8 +92,8 @@ let interp_congrarg_at ist gl n rf ty m =
let pattern_id = mk_internal_id "pattern value"
let congrtac ((n, t), ty) ist gl =
- ppdebug(lazy (Pp.str"===congr==="));
- ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl)));
+ debug_ssr (fun () -> (Pp.str"===congr==="));
+ debug_ssr (fun () -> Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl)));
let sigma, _ as it = interp_term (pf_env gl) (project gl) ist t in
let gl = pf_merge_uc_of sigma gl in
let _, f, _, _ucst = pf_abs_evars gl it in
@@ -124,8 +124,8 @@ let newssrcongrtac arg ist =
Proofview.Goal.enter_one ~__LOC__ begin fun _g ->
(Ssrcommon.tacMK_SSR_CONST "ssr_congr_arrow") end >>= fun arr ->
Proofview.V82.tactic begin fun gl ->
- ppdebug(lazy Pp.(str"===newcongr==="));
- ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl)));
+ debug_ssr (fun () -> Pp.(str"===newcongr==="));
+ debug_ssr (fun () -> Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl)));
(* utils *)
let fs gl t = Reductionops.nf_evar (project gl) t in
let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl =
@@ -385,8 +385,8 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
| Pretype_errors.PretypeError (env, sigma, te) -> raise (PRtype_error (Some (env, sigma, te)))
| e when CErrors.noncritical e -> raise (PRtype_error None)
in
- ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof));
- ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty));
+ debug_ssr (fun () -> Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof));
+ debug_ssr (fun () -> Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty));
try Proofview.V82.of_tactic (refine_with
~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof)) gl
with e when CErrors.noncritical e ->
@@ -435,12 +435,12 @@ let rwcltac ?under ?map_redex cl rdx dir sr =
let sigma0 = Evd.set_universe_context sigma0 ucst in
let rdxt = Retyping.get_type_of env (fst sr) rdx in
(* ppdebug(lazy(str"sigma@rwcltac=" ++ pr_evar_map None (fst sr))); *)
- ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env env sigma0 (snd sr)));
+ debug_ssr (fun () -> Pp.(str"r@rwcltac=" ++ pr_econstr_env env sigma0 (snd sr)));
let cvtac, rwtac, sigma0 =
if EConstr.Vars.closed0 sigma0 r' then
let sigma, c, c_eq = fst sr, snd sr, Coqlib.(lib_ref "core.eq.type") in
let sigma, c_ty = Typing.type_of env sigma c in
- ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty));
+ debug_ssr (fun () -> Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty));
let open EConstr in
match kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
| AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq ->
@@ -521,7 +521,7 @@ let rwprocess_rule env dir rule =
let t =
if red = 1 then Tacred.hnf_constr env sigma t0
else Reductionops.whd_betaiotazeta env sigma t0 in
- ppdebug(lazy Pp.(str"rewrule="++pr_econstr_pat env sigma t));
+ debug_ssr (fun () -> Pp.(str"rewrule="++pr_econstr_pat env sigma t));
match EConstr.kind sigma t with
| Prod (_, xt, at) ->
let sigma = Evd.create_evar_defs sigma in
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index f2c7f495b3..bc46c23761 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -296,8 +296,8 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave =
| Some id ->
if pats = [] then Tacticals.New.tclIDTAC else
let args = Array.of_list args in
- ppdebug(lazy(str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args))));
- ppdebug(lazy(str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct));
+ debug_ssr (fun () -> str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args)));
+ debug_ssr (fun () -> str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct);
Tacticals.New.tclTHENS (basecuttac "ssr_have" ct)
[Tactics.apply EConstr.(mkApp (mkVar id,args)); Tacticals.New.tclIDTAC] in
"ssr_have",
@@ -395,7 +395,7 @@ let intro_lock ipats =
Array.length args = 3 && is_app_evar sigma args.(2) ->
protect_subgoal env sigma hd args
| _ ->
- ppdebug(lazy Pp.(str"under: stop:" ++ pr_econstr_env env sigma t));
+ debug_ssr (fun () -> Pp.(str"under: stop:" ++ pr_econstr_env env sigma t));
Proofview.tclUNIT ()
end)
@@ -468,13 +468,13 @@ let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint =
| Some l -> [IPatCase(Regular [l;[]])] in
let map_redex env evar_map ~before:_ ~after:t =
- ppdebug(lazy Pp.(str"under vars: " ++ prlist Names.Name.print varnames));
+ debug_ssr (fun () -> Pp.(str"under vars: " ++ prlist Names.Name.print varnames));
let evar_map, ty = Typing.type_of env evar_map t in
let new_t = (* pretty-rename the bound variables *)
try begin match EConstr.destApp evar_map t with (f, ar) ->
let lam = Array.last ar in
- ppdebug(lazy Pp.(str"under: mapping:" ++
+ debug_ssr(fun () -> Pp.(str"under: mapping:" ++
pr_econstr_env env evar_map lam));
let new_lam = pretty_rename evar_map lam varnames in
let new_ar, len1 = Array.copy ar, pred (Array.length ar) in
@@ -482,10 +482,10 @@ let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint =
EConstr.mkApp (f, new_ar)
end with
| DestKO ->
- ppdebug(lazy Pp.(str"under: cannot pretty-rename bound variables with destApp"));
+ debug_ssr (fun () -> Pp.(str"under: cannot pretty-rename bound variables with destApp"));
t
in
- ppdebug(lazy Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t));
+ debug_ssr (fun () -> Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t));
evar_map, new_t
in
let undertacs =
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 1e940b5ad3..f8abed5482 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -324,7 +324,7 @@ end
`tac`, where k is the size of `seeds` *)
let tclSEED_SUBGOALS seeds tac =
tclTHENin tac (fun i n ->
- Ssrprinters.ppdebug (lazy Pp.(str"seeding"));
+ Ssrprinters.debug_ssr (fun () -> Pp.(str"seeding"));
(* eg [case: (H _ : nat)] generates 3 goals:
- 1 for _
- 2 for the nat constructors *)
@@ -416,11 +416,11 @@ let tclMK_ABSTRACT_VARS ids =
(* Debugging *)
let tclLOG p t =
tclUNIT () >>= begin fun () ->
- Ssrprinters.ppdebug (lazy Pp.(str "exec: " ++ pr_ipatop p));
+ Ssrprinters.debug_ssr (fun () -> Pp.(str "exec: " ++ pr_ipatop p));
tclUNIT ()
end <*>
Goal.enter begin fun g ->
- Ssrprinters.ppdebug (lazy Pp.(str" on state:" ++ spc () ++
+ Ssrprinters.debug_ssr (fun () -> Pp.(str" on state:" ++ spc () ++
isPRINT g ++
str" goal:" ++ spc () ++ Printer.pr_goal (Goal.print g)));
tclUNIT ()
@@ -429,7 +429,7 @@ let tclLOG p t =
t p
>>= fun ret ->
Goal.enter begin fun g ->
- Ssrprinters.ppdebug (lazy Pp.(str "done: " ++ isPRINT g));
+ Ssrprinters.debug_ssr (fun () -> Pp.(str "done: " ++ isPRINT g));
tclUNIT ()
end
>>= fun () -> tclUNIT ret
@@ -579,10 +579,10 @@ let tclCompileIPats l =
elab l
;;
let tclCompileIPats l =
- Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats input: " ++
+ Ssrprinters.debug_ssr (fun () -> Pp.(str "tclCompileIPats input: " ++
prlist_with_sep spc Ssrprinters.pr_ipat l));
let ops = tclCompileIPats l in
- Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats output: " ++
+ Ssrprinters.debug_ssr (fun () -> Pp.(str "tclCompileIPats output: " ++
prlist_with_sep spc pr_ipatop ops));
ops
@@ -597,11 +597,11 @@ let main ?eqtac ~first_case_is_dispatch iops =
end (* }}} *)
let tclIPAT_EQ eqtac ip =
- Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip));
+ Ssrprinters.debug_ssr (fun () -> Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip));
IpatMachine.(main ~eqtac ~first_case_is_dispatch:true (tclCompileIPats ip))
let tclIPATssr ip =
- Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip));
+ Ssrprinters.debug_ssr (fun () -> Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip));
IpatMachine.(main ~first_case_is_dispatch:true (tclCompileIPats ip))
let tclCompileIPats = IpatMachine.tclCompileIPats
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 6ed68094dc..434568b554 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -15,7 +15,6 @@ open Names
open Printer
open Tacmach
-open Ssrmatching_plugin
open Ssrast
let pr_spc () = str " "
@@ -121,15 +120,4 @@ and pr_block = function (Prefix id) -> str"^" ++ Id.print id
| (SuffixId id) -> str"^~" ++ Id.print id
| (SuffixNum n) -> str"^~" ++ int n
-(* 0 cost pp function. Active only if Debug Ssreflect is Set *)
-let ppdebug_ref = ref (fun _ -> ())
-let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s)
-let () =
- Goptions.(declare_bool_option
- { optkey = ["Debug";"Ssreflect"];
- optdepr = false;
- optread = (fun _ -> !ppdebug_ref == ssr_pp);
- optwrite = (fun b ->
- Ssrmatching.debug b;
- if b then ppdebug_ref := ssr_pp else ppdebug_ref := fun _ -> ()) })
-let ppdebug s = !ppdebug_ref s
+let debug_ssr = CDebug.create ~name:"ssreflect" ()
diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli
index 21fb28038a..994577a0c9 100644
--- a/plugins/ssr/ssrprinters.mli
+++ b/plugins/ssr/ssrprinters.mli
@@ -51,5 +51,4 @@ val pr_guarded :
val pr_occ : ssrocc -> Pp.t
-val ppdebug : Pp.t Lazy.t -> unit
-
+val debug_ssr : CDebug.t
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 97926753f5..b3a9e71a3f 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -194,17 +194,17 @@ let mkGApp f args =
let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
let env = Goal.env goal in
let sigma = Goal.sigma goal in
- Ssrprinters.ppdebug (lazy
+ Ssrprinters.debug_ssr (fun () ->
Pp.(str"interp-in: " ++ Printer.pr_glob_constr_env env sigma glob));
try
let sigma,term = Tacinterp.interp_open_constr ist env sigma (glob,None) in
- Ssrprinters.ppdebug (lazy
+ Ssrprinters.debug_ssr (fun () ->
Pp.(str"interp-out: " ++ Printer.pr_econstr_env env sigma term));
tclUNIT (env,sigma,term)
with e ->
(* XXX this is another catch all! *)
let e, info = Exninfo.capture e in
- Ssrprinters.ppdebug (lazy
+ Ssrprinters.debug_ssr (fun () ->
Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env sigma glob));
tclZERO ~info e
end
@@ -217,7 +217,7 @@ end
let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t
let tclADD_CLEAR_IF_ID (env, ist, t) x =
- Ssrprinters.ppdebug (lazy
+ Ssrprinters.debug_ssr (fun () ->
Pp.(str"tclADD_CLEAR_IF_ID: " ++ Printer.pr_econstr_env env ist t));
let hd, args = EConstr.decompose_app ist t in
match EConstr.kind ist hd with
@@ -269,11 +269,11 @@ let interp_view ~clear_if_id ist v p =
let p_id = DAst.make p_id in
match DAst.get v with
| Glob_term.GApp (hd, rargs) when is_specialize hd ->
- Ssrprinters.ppdebug (lazy Pp.(str "specialize"));
+ Ssrprinters.debug_ssr (fun () -> Pp.(str "specialize"));
interp_glob ist (mkGApp p_id rargs)
>>= tclKeepOpenConstr >>= tclPAIR []
| _ ->
- Ssrprinters.ppdebug (lazy Pp.(str "view"));
+ Ssrprinters.debug_ssr (fun () -> Pp.(str "view"));
(* We find out how to build (v p) eventually using an adaptor *)
let adaptors = AdaptorDb.(get Forward) in
Proofview.tclORELSE
@@ -324,7 +324,7 @@ Goal.enter_one ~__LOC__ begin fun g ->
let rigid = rigid_of und0 in
let n, p, to_prune, _ucst = pf_abs_evars2 s0 rigid (sigma, p) in
let p = if simple_types then pf_abs_cterm s0 n p else p in
- Ssrprinters.ppdebug (lazy Pp.(str"view@finalized: " ++
+ Ssrprinters.debug_ssr (fun () -> Pp.(str"view@finalized: " ++
Printer.pr_econstr_env env sigma p));
let sigma = List.fold_left Evd.remove sigma to_prune in
Unsafe.tclEVARS sigma <*>
@@ -349,26 +349,26 @@ let rec apply_all_views_aux ~clear_if_id vs finalization conclusion s0 =
pose_proof name p <*> conclusion ~to_clear:name) <*>
tclUNIT false)
| v :: vs ->
- Ssrprinters.ppdebug (lazy Pp.(str"piling..."));
+ Ssrprinters.debug_ssr (fun () -> Pp.(str"piling..."));
is_tac_in_term ~extra_scope:"ssripat" v >>= function
| `Term v ->
- Ssrprinters.ppdebug (lazy Pp.(str"..a term"));
+ Ssrprinters.debug_ssr (fun () -> Pp.(str"..a term"));
pile_up_view ~clear_if_id v <*>
apply_all_views_aux ~clear_if_id vs finalization conclusion s0
| `Tac tac ->
- Ssrprinters.ppdebug (lazy Pp.(str"..a tactic"));
+ Ssrprinters.debug_ssr (fun () -> Pp.(str"..a tactic"));
finalization s0 (fun name p ->
(match p with
| None -> tclUNIT ()
| Some p -> pose_proof name p) <*>
Tacinterp.eval_tactic tac <*>
if vs = [] then begin
- Ssrprinters.ppdebug (lazy Pp.(str"..was the last view"));
+ Ssrprinters.debug_ssr (fun () -> Pp.(str"..was the last view"));
conclusion ~to_clear:name <*> tclUNIT true
end else
Tactics.clear name <*>
tclINDEPENDENTL begin
- Ssrprinters.ppdebug (lazy Pp.(str"..was NOT the last view"));
+ Ssrprinters.debug_ssr (fun () -> Pp.(str"..was NOT the last view"));
Ssrcommon.tacSIGMA >>=
apply_all_views_aux ~clear_if_id vs finalization conclusion
end >>= reduce_or)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:12:43 +0000