From 17c9a9775e99d1551bf6d346d731271e3ae34417 Mon Sep 17 00:00:00 2001 From: Daniel de Rauglaudre Date: Fri, 8 Apr 2016 14:53:32 +0200 Subject: 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. --- plugins/cc/ccproof.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'plugins/cc/ccproof.ml') 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 -- cgit v1.2.3