--- a/src/HOL/Tools/svc_funcs.ML Wed Nov 21 00:35:13 2001 +0100
+++ b/src/HOL/Tools/svc_funcs.ML Wed Nov 21 00:36:51 2001 +0100
@@ -66,7 +66,7 @@
then error "Environment variable SVC_MACHINE not set"
else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid"
val svc_input = toString e
- val _ = if !trace then writeln ("Calling SVC:\n" ^ svc_input) else ()
+ val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else ()
val svc_input_file = File.tmp_path (Path.basic "SVM_in");
val svc_output_file = File.tmp_path (Path.basic "SVM_out");
val _ = (File.write svc_input_file svc_input;
@@ -79,7 +79,7 @@
Some out => out
| None => error "SVC returned no output");
in
- if ! trace then writeln ("SVC Returns:\n" ^ svc_output)
+ if ! trace then tracing ("SVC Returns:\n" ^ svc_output)
else (File.rm svc_input_file; File.rm svc_output_file);
String.isPrefix "VALID" svc_output
end
@@ -249,7 +249,7 @@
(*The oracle proves the given formula t, if possible*)
fun oracle (sign, OracleExn t) =
- let val dummy = if !trace then writeln ("Subgoal abstracted to\n" ^
+ let val dummy = if !trace then tracing ("Subgoal abstracted to\n" ^
Sign.string_of_term sign t)
else ()
in
--- a/src/Provers/Arith/abel_cancel.ML Wed Nov 21 00:35:13 2001 +0100
+++ b/src/Provers/Arith/abel_cancel.ML Wed Nov 21 00:36:51 2001 +0100
@@ -104,7 +104,7 @@
*)
fun sum_proc sg _ lhs =
- let val _ = if !trace then writeln ("cancel_sums: LHS = " ^
+ let val _ = if !trace then tracing ("cancel_sums: LHS = " ^
string_of_cterm (cterm_of sg lhs))
else ()
val (head::tail) = terms lhs
@@ -112,7 +112,7 @@
val rhs = mk_sum (cancelled (head',tail))
and chead' = Thm.cterm_of sg head'
val _ = if !trace then
- writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
+ tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
else ()
val ct = Thm.cterm_of sg (Logic.mk_equals (lhs, rhs))
val thm = prove ct
@@ -153,7 +153,7 @@
val add_ac_ss = Data.ss addsimps [add_assoc,add_commute,add_left_commute];
fun rel_proc sg _ (lhs as (rel$lt$rt)) =
- let val _ = if !trace then writeln ("cancel_relations: LHS = " ^
+ let val _ = if !trace then tracing ("cancel_relations: LHS = " ^
string_of_cterm (cterm_of sg lhs))
else ()
val ltms = terms lt
@@ -170,7 +170,7 @@
val rhs = rel$lt'$rt'
val _ = if !trace then
- writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
+ tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
else ()
val ct = Thm.cterm_of sg (Logic.mk_equals (lhs,rhs))
--- a/src/Provers/Arith/assoc_fold.ML Wed Nov 21 00:35:13 2001 +0100
+++ b/src/Provers/Arith/assoc_fold.ML Wed Nov 21 00:36:51 2001 +0100
@@ -52,14 +52,14 @@
(*Make a simproc to combine all literals in a associative nest*)
fun proc sg _ lhs =
let fun show t = string_of_cterm (Thm.cterm_of sg t)
- val _ = if !trace then writeln ("assoc_fold simproc: LHS = " ^ show lhs)
+ val _ = if !trace then tracing ("assoc_fold simproc: LHS = " ^ show lhs)
else ()
val (lits,others) = sift_terms (lhs, ([],[]))
val _ = if length lits < 2
then raise Assoc_fail (*we can't reduce the number of terms*)
else ()
val rhs = Data.plus $ mk_sum lits $ mk_sum others
- val _ = if !trace then writeln ("RHS = " ^ show rhs) else ()
+ val _ = if !trace then tracing ("RHS = " ^ show rhs) else ()
val th = prove "assoc_fold"
(Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)))
(fn _ => [rtac Data.eq_reflection 1,
--- a/src/Provers/Arith/fast_lin_arith.ML Wed Nov 21 00:35:13 2001 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Wed Nov 21 00:36:51 2001 +0100
@@ -232,7 +232,7 @@
fun print_ineqs ineqs =
if !trace then
- writeln(cat_lines(""::map (fn Lineq(c,t,l,_) =>
+ tracing(cat_lines(""::map (fn Lineq(c,t,l,_) =>
string_of_int c ^
(case t of Eq => " = " | Lt=> " < " | Le => " <= ") ^
commas(map string_of_int l)) ineqs))
@@ -280,10 +280,10 @@
(* ------------------------------------------------------------------------- *)
fun trace_thm msg th =
- if !trace then (writeln msg; prth th) else th;
+ if !trace then (tracing msg; tracing (Display.string_of_thm th); th) else th;
fun trace_msg msg =
- if !trace then writeln msg else ();
+ if !trace then tracing msg else ();
(* FIXME OPTIMIZE!!!!
Addition/Multiplication need i*t representation rather than t+t+...
--- a/src/Provers/hypsubst.ML Wed Nov 21 00:35:13 2001 +0100
+++ b/src/Provers/hypsubst.ML Wed Nov 21 00:36:51 2001 +0100
@@ -236,7 +236,7 @@
val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
val n = length hyps
in
- if !trace then writeln "Substituting an equality" else ();
+ if !trace then tracing "Substituting an equality" else ();
DETERM
(EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
rotate_tac 1 i,
--- a/src/Pure/Isar/method.ML Wed Nov 21 00:35:13 2001 +0100
+++ b/src/Pure/Isar/method.ML Wed Nov 21 00:36:51 2001 +0100
@@ -138,8 +138,9 @@
val trace_rules = ref false;
fun trace ctxt rules =
- if not (! trace_rules) orelse null rules then ()
- else Pretty.writeln (Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules));
+ conditional (! trace_rules andalso not (null rules)) (fn () =>
+ Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules)
+ |> Pretty.string_of |> tracing);
--- a/src/Pure/Syntax/ast.ML Wed Nov 21 00:35:13 2001 +0100
+++ b/src/Pure/Syntax/ast.ML Wed Nov 21 00:36:51 2001 +0100
@@ -157,12 +157,6 @@
(** normalization of asts **)
-(* tracing options *)
-
-val trace_ast = ref false;
-val stat_ast = ref false;
-
-
(* match *)
fun match ast pat =
@@ -228,9 +222,8 @@
| rewrite ast = try_headless_rules ast;
fun rewrote old_ast new_ast =
- if trace then
- writeln ("rewrote: " ^ str_of_ast old_ast ^ " -> " ^ str_of_ast new_ast)
- else ();
+ conditional trace (fn () =>
+ tracing ("rewrote: " ^ str_of_ast old_ast ^ " -> " ^ str_of_ast new_ast));
fun norm_root ast =
(case rewrite ast of
@@ -258,22 +251,24 @@
end;
- val _ = if trace then writeln ("pre: " ^ str_of_ast pre_ast) else ();
+ val _ = conditional trace (fn () => tracing ("pre: " ^ str_of_ast pre_ast));
val post_ast = normal pre_ast;
in
- if trace orelse stat then
- writeln ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
+ conditional (trace orelse stat) (fn () =>
+ tracing ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
string_of_int (! passes) ^ " passes, " ^
string_of_int (! changes) ^ " changes, " ^
- string_of_int (! failed_matches) ^ " matches failed")
- else ();
+ string_of_int (! failed_matches) ^ " matches failed"));
post_ast
end;
(* normalize_ast *)
+val trace_ast = ref false;
+val stat_ast = ref false;
+
fun normalize_ast get_rules ast =
normalize (! trace_ast) (! stat_ast) get_rules ast;
--- a/src/Pure/meta_simplifier.ML Wed Nov 21 00:35:13 2001 +0100
+++ b/src/Pure/meta_simplifier.ML Wed Nov 21 00:36:51 2001 +0100
@@ -64,7 +64,7 @@
val simp_depth = ref 0;
-fun println a = writeln(replicate_string (!simp_depth) " " ^ a)
+fun println a = tracing (replicate_string (! simp_depth) " " ^ a);
fun prnt warn a = if warn then warning a else println a;
--- a/src/Pure/search.ML Wed Nov 21 00:35:13 2001 +0100
+++ b/src/Pure/search.ML Wed Nov 21 00:36:51 2001 +0100
@@ -118,7 +118,7 @@
| prune_aux (qs, (k,np,rgd,q)::rqs) =
if np'+1 = np andalso rgd then
(if !trace_DEPTH_FIRST then
- writeln ("Pruning " ^
+ tracing ("Pruning " ^
string_of_int (1+length rqs) ^ " levels")
else ();
(*Use OLD k: zero-cost solution; see Stickel, p 365*)
@@ -142,7 +142,7 @@
and qs0 = tac0 st
(*bnd = depth bound; inc = estimate of increment required next*)
fun depth (bnd,inc) [] =
- (writeln (string_of_int (!countr) ^
+ (tracing (string_of_int (!countr) ^
" inferences so far. Searching to depth " ^
string_of_int bnd);
(*larger increments make it run slower for the hard problems*)
@@ -152,7 +152,7 @@
else
case (countr := !countr+1;
if !trace_DEPTH_FIRST then
- writeln (string_of_int np ^
+ tracing (string_of_int np ^
implode (map (fn _ => "*") qs))
else ();
Seq.pull q) of
@@ -185,8 +185,8 @@
fun DEEPEN (inc,lim) tacf m i =
let fun dpn m st = st |> (if has_fewer_prems i st then no_tac
else if m>lim then
- (writeln "Giving up..."; no_tac)
- else (writeln ("Depth = " ^ string_of_int m);
+ (tracing "Giving up..."; no_tac)
+ else (tracing ("Depth = " ^ string_of_int m);
tacf m i ORELSE dpn (m+inc)))
in dpn m end;
@@ -221,7 +221,7 @@
else
let val (n,prf) = ThmHeap.min nprf_heap
in if !trace_BEST_FIRST
- then writeln("state size = " ^ string_of_int n)
+ then tracing("state size = " ^ string_of_int n)
else ();
bfs (Seq.list_of (tac prf),
deleteAllMin prf (ThmHeap.delete_min nprf_heap))
@@ -245,7 +245,7 @@
| (sats,_) => sats)
in (fn st => Seq.of_list (bfs [st])) end;
-val BREADTH_FIRST = gen_BREADTH_FIRST writeln;
+val BREADTH_FIRST = gen_BREADTH_FIRST tracing;
val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ());
@@ -281,7 +281,7 @@
next [] = None
| next ((level,n,prf)::nprfs) =
(if !trace_ASTAR
- then writeln("level = " ^ string_of_int level ^
+ then tracing("level = " ^ string_of_int level ^
" cost = " ^ string_of_int n ^
" queue length =" ^ string_of_int (length nprfs))
else ();
--- a/src/Pure/tactic.ML Wed Nov 21 00:35:13 2001 +0100
+++ b/src/Pure/tactic.ML Wed Nov 21 00:36:51 2001 +0100
@@ -124,7 +124,7 @@
fun trace_goalno_tac tac i st =
case Seq.pull(tac i st) of
None => Seq.empty
- | seqcell => (writeln ("Subgoal " ^ string_of_int i ^ " selected");
+ | seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected");
Seq.make(fn()=> seqcell));
(*Makes a rule by applying a tactic to an existing rule*)
@@ -285,8 +285,8 @@
if i > nprems_of st then no_tac st
else st |>
(compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), nsubgoal) i
- handle TERM (msg,_) => (writeln msg; no_tac)
- | THM (msg,_,_) => (writeln msg; no_tac));
+ handle TERM (msg,_) => (warning msg; no_tac)
+ | THM (msg,_,_) => (warning msg; no_tac));
(*"Resolve" version. Note: res_inst_tac cannot behave sensibly if the
terms that are substituted contain (term or type) unknowns from the
--- a/src/Pure/tctical.ML Wed Nov 21 00:35:13 2001 +0100
+++ b/src/Pure/tctical.ML Wed Nov 21 00:36:51 2001 +0100
@@ -198,14 +198,14 @@
(*Print the current proof state and pass it on.*)
fun print_tac msg =
(fn st =>
- (writeln msg;
+ (tracing msg;
Display.print_goals (! Display.goals_limit) st; Seq.single st));
(*Pause until a line is typed -- if non-empty then fail. *)
fun pause_tac st =
- (writeln "** Press RETURN to continue:";
+ (tracing "** Press RETURN to continue:";
if TextIO.inputLine TextIO.stdIn = "\n" then Seq.single st
- else (writeln "Goodbye"; Seq.empty));
+ else (tracing "Goodbye"; Seq.empty));
exception TRACE_EXIT of thm
and TRACE_QUIT;
@@ -221,9 +221,9 @@
| "f\n" => Seq.empty
| "o\n" => (flag:=false; tac st)
| "s\n" => (suppress_tracing:=true; tac st)
- | "x\n" => (writeln "Exiting now"; raise (TRACE_EXIT st))
+ | "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st))
| "quit\n" => raise TRACE_QUIT
- | _ => (writeln
+ | _ => (tracing
"Type RETURN to continue or...\n\
\ f - to fail here\n\
\ o - to switch tracing off\n\
@@ -237,7 +237,7 @@
fun tracify flag tac st =
if !flag andalso not (!suppress_tracing)
then (Display.print_goals (! Display.goals_limit) st;
- writeln "** Press RETURN to continue:";
+ tracing "** Press RETURN to continue:";
exec_trace_command flag (tac,st))
else tac st;
--- a/src/Pure/unify.ML Wed Nov 21 00:35:13 2001 +0100
+++ b/src/Pure/unify.ML Wed Nov 21 00:36:51 2001 +0100
@@ -186,7 +186,7 @@
fun test_unify_types(args as (T,U,_)) =
let val sot = Sign.string_of_typ (!sgr);
- fun warn() = writeln("Potential loss of completeness: "^sot U^" = "^sot T);
+ fun warn() = tracing ("Potential loss of completeness: "^sot U^" = "^sot T);
val env' = unify_types(args)
in if is_TVar(T) orelse is_TVar(U) then warn() else ();
env'
@@ -560,8 +560,8 @@
(Envir.norm_term env (rlist_abs(rbinder,t)))
val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
termT t];
- in writeln(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
- in writeln msg; seq pdp dpairs end;
+ in tracing(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
+ in tracing msg; seq pdp dpairs end;
(*Unify the dpairs in the environment.
@@ -588,7 +588,7 @@
(MATCH (env',dp, frigid'@flexflex), reseq)))
end
handle CANTUNIFY =>
- (if tdepth > !trace_bound then writeln"Failure node" else ();
+ (if tdepth > !trace_bound then tracing"Failure node" else ();
Seq.pull reseq));
val dps = map (fn(t,u)=> ([],t,u)) tus
in sgr := sg;