aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/cc/ccalgo.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-06-01 18:03:06 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-06-01 18:03:06 +0000
commitcf7660a3a8932ee593a376e8ec7ec251896a72e3 (patch)
tree5f3fd167f5dd704bf5482d236624aa8ef8bf6707 /plugins/cc/ccalgo.ml
parent35e4ac349af4fabbc5658b5cba632f98ec04da3f (diff)
Getting rid of Pp.msgnl and Pp.message.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/cc/ccalgo.ml')
-rw-r--r--plugins/cc/ccalgo.ml54
1 files changed, 26 insertions, 28 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 699f1f3df..6fda2284a 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -23,8 +23,8 @@ let init_size=5
let cc_verbose=ref false
-let debug f x =
- if !cc_verbose then f x
+let debug x =
+ if !cc_verbose then msg_debug x
let _=
let gdopt=
@@ -512,7 +512,7 @@ let add_inst state (inst,int_subst) =
check_for_interrupt ();
if state.rew_depth > 0 then
if is_redundant state inst.qe_hyp_id int_subst then
- debug msgnl (str "discarding redundant (dis)equality")
+ debug (str "discarding redundant (dis)equality")
else
begin
Identhash.add state.q_history inst.qe_hyp_id int_subst;
@@ -527,20 +527,18 @@ let add_inst state (inst,int_subst) =
state.rew_depth<-pred state.rew_depth;
if inst.qe_pol then
begin
- debug (fun () ->
- msgnl
- (str "Adding new equality, depth="++ int state.rew_depth);
- msgnl (str " [" ++ Termops.print_constr prf ++ str " : " ++
- pr_term s ++ str " == " ++ pr_term t ++ str "]")) ();
+ debug (
+ (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
+ (str " [" ++ Termops.print_constr prf ++ str " : " ++
+ pr_term s ++ str " == " ++ pr_term t ++ str "]"));
add_equality state prf s t
end
else
begin
- debug (fun () ->
- msgnl
- (str "Adding new disequality, depth="++ int state.rew_depth);
- msgnl (str " [" ++ Termops.print_constr prf ++ str " : " ++
- pr_term s ++ str " <> " ++ pr_term t ++ str "]")) ();
+ debug (
+ (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
+ (str " [" ++ Termops.print_constr prf ++ str " : " ++
+ pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
add_disequality state (Hyp prf) s t
end
end
@@ -566,8 +564,8 @@ let join_path uf i j=
min_path (down_path uf i [],down_path uf j [])
let union state i1 i2 eq=
- debug (fun () -> msgnl (str "Linking " ++ pr_idx_term state i1 ++
- str " and " ++ pr_idx_term state i2 ++ str ".")) ();
+ debug (str "Linking " ++ pr_idx_term state i1 ++
+ str " and " ++ pr_idx_term state i2 ++ str ".");
let r1= get_representative state.uf i1
and r2= get_representative state.uf i2 in
link state.uf i1 i2 eq;
@@ -606,9 +604,9 @@ let union state i1 i2 eq=
| _,_ -> ()
let merge eq state = (* merge and no-merge *)
- debug (fun () -> msgnl
+ debug
(str "Merging " ++ pr_idx_term state eq.lhs ++
- str " and " ++ pr_idx_term state eq.rhs ++ str ".")) ();
+ str " and " ++ pr_idx_term state eq.rhs ++ str ".");
let uf=state.uf in
let i=find uf eq.lhs
and j=find uf eq.rhs in
@@ -619,8 +617,8 @@ let merge eq state = (* merge and no-merge *)
union state j i (swap eq)
let update t state = (* update 1 and 2 *)
- debug (fun () -> msgnl
- (str "Updating term " ++ pr_idx_term state t ++ str ".")) ();
+ debug
+ (str "Updating term " ++ pr_idx_term state 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
@@ -680,8 +678,8 @@ let process_constructor_mark t i rep pac state =
end
let process_mark t m state =
- debug (fun () -> msgnl
- (str "Processing mark for term " ++ pr_idx_term state t ++ str ".")) ();
+ debug
+ (str "Processing mark for term " ++ pr_idx_term state t ++ str ".");
let i=find state.uf t in
let rep=get_representative state.uf i in
match m with
@@ -701,9 +699,9 @@ let check_disequalities state =
if find uf dis.lhs = find uf dis.rhs then (str "Yes", Some dis)
else (str "No", check_aux q)
in
- let _ = debug (fun () -> msg_debug
+ let _ = debug
(str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++
- pr_idx_term state dis.rhs ++ str " ... " ++ info)) () in
+ pr_idx_term state dis.rhs ++ str " ... " ++ info) in
ans
| [] -> None
in
@@ -889,7 +887,7 @@ let find_instances state =
let pb_stack= init_pb_stack state in
let res =ref [] in
let _ =
- debug msgnl (str "Running E-matching algorithm ... ");
+ debug (str "Running E-matching algorithm ... ");
try
while true do
check_for_interrupt ();
@@ -900,7 +898,7 @@ let find_instances state =
!res
let rec execute first_run state =
- debug msgnl (str "Executing ... ");
+ debug (str "Executing ... ");
try
while
check_for_interrupt ();
@@ -910,7 +908,7 @@ let rec execute first_run state =
None ->
if not(Intset.is_empty state.pa_classes) then
begin
- debug msgnl (str "First run was incomplete, completing ... ");
+ debug (str "First run was incomplete, completing ... ");
complete state;
execute false state
end
@@ -925,12 +923,12 @@ let rec execute first_run state =
end
else
begin
- debug msgnl (str "Out of instances ... ");
+ debug (str "Out of instances ... ");
None
end
else
begin
- debug msgnl (str "Out of depth ... ");
+ debug (str "Out of depth ... ");
None
end
| Some dis -> Some