aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr>2016-04-08 14:53:32 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-08 14:58:42 +0200
commit17c9a9775e99d1551bf6d346d731271e3ae34417 (patch)
tree04c63b6dded7381b61a8d915fd486744967efefd
parent9f0a896536e709880de5ba638069dea680803f62 (diff)
Fixing a source of inefficiency and an artificial dependency in the
printer in the congruence tactic. Debugging messages were always built even when not in the verbose mode of congruence.
-rw-r--r--plugins/cc/ccalgo.ml28
-rw-r--r--plugins/cc/ccalgo.mli2
-rw-r--r--plugins/cc/ccproof.ml12
-rw-r--r--plugins/cc/cctac.ml8
4 files changed, 25 insertions, 25 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index bc3d9ed56..5d16edfc6 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -25,7 +25,7 @@ let init_size=5
let cc_verbose=ref false
let debug x =
- if !cc_verbose then msg_debug x
+ if !cc_verbose then msg_debug (x ())
let _=
let gdopt=
@@ -603,7 +603,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 (str "discarding redundant (dis)equality")
+ debug (fun () -> str "discarding redundant (dis)equality")
else
begin
Identhash.add state.q_history inst.qe_hyp_id int_subst;
@@ -618,7 +618,7 @@ let add_inst state (inst,int_subst) =
state.rew_depth<-pred state.rew_depth;
if inst.qe_pol then
begin
- debug (
+ debug (fun () ->
(str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
(str " [" ++ Termops.print_constr prf ++ str " : " ++
pr_term s ++ str " == " ++ pr_term t ++ str "]"));
@@ -626,7 +626,7 @@ let add_inst state (inst,int_subst) =
end
else
begin
- debug (
+ debug (fun () ->
(str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
(str " [" ++ Termops.print_constr prf ++ str " : " ++
pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
@@ -657,7 +657,7 @@ let join_path uf i j=
min_path (down_path uf i [],down_path uf j [])
let union state i1 i2 eq=
- debug (str "Linking " ++ pr_idx_term state.uf i1 ++
+ debug (fun () -> str "Linking " ++ pr_idx_term state.uf i1 ++
str " and " ++ pr_idx_term state.uf i2 ++ str ".");
let r1= get_representative state.uf i1
and r2= get_representative state.uf i2 in
@@ -698,7 +698,7 @@ let union state i1 i2 eq=
let merge eq state = (* merge and no-merge *)
debug
- (str "Merging " ++ pr_idx_term state.uf eq.lhs ++
+ (fun () -> str "Merging " ++ pr_idx_term state.uf eq.lhs ++
str " and " ++ pr_idx_term state.uf eq.rhs ++ str ".");
let uf=state.uf in
let i=find uf eq.lhs
@@ -711,7 +711,7 @@ let merge eq state = (* merge and no-merge *)
let update t state = (* update 1 and 2 *)
debug
- (str "Updating term " ++ pr_idx_term state.uf t ++ str ".");
+ (fun () -> str "Updating term " ++ pr_idx_term state.uf t ++ str ".");
let (i,j) as sign = signature state.uf t in
let (u,v) = subterms state.uf t in
let rep = get_representative state.uf i in
@@ -773,7 +773,7 @@ let process_constructor_mark t i rep pac state =
let process_mark t m state =
debug
- (str "Processing mark for term " ++ pr_idx_term state.uf t ++ str ".");
+ (fun () -> str "Processing mark for term " ++ pr_idx_term state.uf t ++ str ".");
let i=find state.uf t in
let rep=get_representative state.uf i in
match m with
@@ -794,7 +794,7 @@ let check_disequalities state =
else (str "No", check_aux q)
in
let _ = debug
- (str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++
+ (fun () -> str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++
pr_idx_term state.uf dis.rhs ++ str " ... " ++ info) in
ans
| [] -> None
@@ -979,7 +979,7 @@ let find_instances state =
let pb_stack= init_pb_stack state in
let res =ref [] in
let _ =
- debug (str "Running E-matching algorithm ... ");
+ debug (fun () -> str "Running E-matching algorithm ... ");
try
while true do
Control.check_for_interrupt ();
@@ -990,7 +990,7 @@ let find_instances state =
!res
let rec execute first_run state =
- debug (str "Executing ... ");
+ debug (fun () -> str "Executing ... ");
try
while
Control.check_for_interrupt ();
@@ -1000,7 +1000,7 @@ let rec execute first_run state =
None ->
if not(Int.Set.is_empty state.pa_classes) then
begin
- debug (str "First run was incomplete, completing ... ");
+ debug (fun () -> str "First run was incomplete, completing ... ");
complete state;
execute false state
end
@@ -1015,12 +1015,12 @@ let rec execute first_run state =
end
else
begin
- debug (str "Out of instances ... ");
+ debug (fun () -> str "Out of instances ... ");
None
end
else
begin
- debug (str "Out of depth ... ");
+ debug (fun () -> str "Out of depth ... ");
None
end
| Some dis -> Some
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index b73c8eef8..c7fa2f56f 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -120,7 +120,7 @@ val term_equal : term -> term -> bool
val constr_of_term : term -> constr
-val debug : Pp.std_ppcmds -> unit
+val debug : (unit -> Pp.std_ppcmds) -> unit
val forest : state -> forest
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index c188bf3bc..d2bbaf6a7 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -93,13 +93,13 @@ let pinject p c n a =
p_rule=Inject(p,c,n,a)}
let rec equal_proof uf i j=
- debug (str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+ debug (fun () -> str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
if i=j then prefl (term uf i) else
let (li,lj)=join_path uf i j in
ptrans (path_proof uf i li) (psym (path_proof uf j lj))
and edge_proof uf ((i,j),eq)=
- debug (str "edge_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+ debug (fun () -> str "edge_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
let pi=equal_proof uf i eq.lhs in
let pj=psym (equal_proof uf j eq.rhs) in
let pij=
@@ -115,7 +115,7 @@ and edge_proof uf ((i,j),eq)=
ptrans (ptrans pi pij) pj
and constr_proof uf i ipac=
- debug (str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20));
+ debug (fun () -> str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20));
let t=find_oldest_pac uf i ipac in
let eq_it=equal_proof uf i t in
if ipac.args=[] then
@@ -128,20 +128,20 @@ and constr_proof uf i ipac=
ptrans eq_it (pcongr p (prefl targ))
and path_proof uf i l=
- debug (str "path_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ str "{" ++
+ debug (fun () -> str "path_proof " ++ pr_idx_term 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 uf (snd (fst x)) q) (edge_proof uf x)
and congr_proof uf i j=
- debug (str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+ debug (fun () -> str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
let (i1,i2) = subterms uf i
and (j1,j2) = subterms uf j in
pcongr (equal_proof uf i1 j1) (equal_proof uf i2 j2)
and ind_proof uf i ipac j jpac=
- debug (str "ind_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+ debug (fun () -> str "ind_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
let p=equal_proof uf i j
and p1=constr_proof uf i ipac
and p2=constr_proof uf j jpac in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 0baa53370..df4a7319a 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -413,16 +413,16 @@ let build_term_to_complete uf meta pac =
let cc_tactic depth additionnal_terms =
Proofview.Goal.nf_enter begin fun gl ->
Coqlib.check_required_library Coqlib.logic_module_name;
- let _ = debug (Pp.str "Reading subgoal ...") in
+ let _ = debug (fun () -> Pp.str "Reading subgoal ...") in
let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in
- let _ = debug (Pp.str "Problem built, solving ...") in
+ let _ = debug (fun () -> Pp.str "Problem built, solving ...") in
let sol = execute true state in
- let _ = debug (Pp.str "Computation completed.") in
+ let _ = debug (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 (Pp.str "Goal solved, generating proof ...");
+ debug (fun () -> Pp.str "Goal solved, generating proof ...");
match reason with
Discrimination (i,ipac,j,jpac) ->
let p=build_proof uf (`Discr (i,ipac,j,jpac)) in