# HG changeset patch # User wenzelm # Date 1006299411 -3600 # Node ID 11ff5f47df6e34d8bd03f12ce2a589aa8e8f5c4e # Parent ee14db2c571dfc0ca4a56cda438d39278c45a0e4 use tracing function for trace output; diff -r ee14db2c571d -r 11ff5f47df6e src/HOL/Tools/svc_funcs.ML --- 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 diff -r ee14db2c571d -r 11ff5f47df6e src/Provers/Arith/abel_cancel.ML --- 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)) diff -r ee14db2c571d -r 11ff5f47df6e src/Provers/Arith/assoc_fold.ML --- 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, diff -r ee14db2c571d -r 11ff5f47df6e src/Provers/Arith/fast_lin_arith.ML --- 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+... diff -r ee14db2c571d -r 11ff5f47df6e src/Provers/hypsubst.ML --- 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, diff -r ee14db2c571d -r 11ff5f47df6e src/Pure/Isar/method.ML --- 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); diff -r ee14db2c571d -r 11ff5f47df6e src/Pure/Syntax/ast.ML --- 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; diff -r ee14db2c571d -r 11ff5f47df6e src/Pure/meta_simplifier.ML --- 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; diff -r ee14db2c571d -r 11ff5f47df6e src/Pure/search.ML --- 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 (); diff -r ee14db2c571d -r 11ff5f47df6e src/Pure/tactic.ML --- 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 diff -r ee14db2c571d -r 11ff5f47df6e src/Pure/tctical.ML --- 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; diff -r ee14db2c571d -r 11ff5f47df6e src/Pure/unify.ML --- 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;