use tracing function for trace output;
authorwenzelm
Wed Nov 21 00:36:51 2001 +0100 (2001-11-21)
changeset 1226211ff5f47df6e
parent 12261 ee14db2c571d
child 12263 6f2acf10e2a2
use tracing function for trace output;
src/HOL/Tools/svc_funcs.ML
src/Provers/Arith/abel_cancel.ML
src/Provers/Arith/assoc_fold.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/hypsubst.ML
src/Pure/Isar/method.ML
src/Pure/Syntax/ast.ML
src/Pure/meta_simplifier.ML
src/Pure/search.ML
src/Pure/tactic.ML
src/Pure/tctical.ML
src/Pure/unify.ML
     1.1 --- a/src/HOL/Tools/svc_funcs.ML	Wed Nov 21 00:35:13 2001 +0100
     1.2 +++ b/src/HOL/Tools/svc_funcs.ML	Wed Nov 21 00:36:51 2001 +0100
     1.3 @@ -66,7 +66,7 @@
     1.4  	                then error "Environment variable SVC_MACHINE not set"
     1.5  			else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid"
     1.6        val svc_input = toString e
     1.7 -      val _ = if !trace then writeln ("Calling SVC:\n" ^ svc_input) else ()
     1.8 +      val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else ()
     1.9        val svc_input_file  = File.tmp_path (Path.basic "SVM_in");
    1.10        val svc_output_file = File.tmp_path (Path.basic "SVM_out");
    1.11        val _ = (File.write svc_input_file svc_input;
    1.12 @@ -79,7 +79,7 @@
    1.13            Some out => out
    1.14          | None => error "SVC returned no output");
    1.15    in
    1.16 -      if ! trace then writeln ("SVC Returns:\n" ^ svc_output)
    1.17 +      if ! trace then tracing ("SVC Returns:\n" ^ svc_output)
    1.18        else (File.rm svc_input_file; File.rm svc_output_file);
    1.19        String.isPrefix "VALID" svc_output
    1.20    end
    1.21 @@ -249,7 +249,7 @@
    1.22  
    1.23   (*The oracle proves the given formula t, if possible*)
    1.24   fun oracle (sign, OracleExn t) = 
    1.25 -   let val dummy = if !trace then writeln ("Subgoal abstracted to\n" ^
    1.26 +   let val dummy = if !trace then tracing ("Subgoal abstracted to\n" ^
    1.27  					   Sign.string_of_term sign t)
    1.28                     else ()
    1.29     in
     2.1 --- a/src/Provers/Arith/abel_cancel.ML	Wed Nov 21 00:35:13 2001 +0100
     2.2 +++ b/src/Provers/Arith/abel_cancel.ML	Wed Nov 21 00:36:51 2001 +0100
     2.3 @@ -104,7 +104,7 @@
     2.4   *)
     2.5  
     2.6   fun sum_proc sg _ lhs =
     2.7 -   let val _ = if !trace then writeln ("cancel_sums: LHS = " ^ 
     2.8 +   let val _ = if !trace then tracing ("cancel_sums: LHS = " ^ 
     2.9  				       string_of_cterm (cterm_of sg lhs))
    2.10  	       else ()
    2.11         val (head::tail) = terms lhs
    2.12 @@ -112,7 +112,7 @@
    2.13         val rhs = mk_sum (cancelled (head',tail))
    2.14         and chead' = Thm.cterm_of sg head'
    2.15         val _ = if !trace then 
    2.16 -		 writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
    2.17 +		 tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
    2.18  	       else ()
    2.19         val ct = Thm.cterm_of sg (Logic.mk_equals (lhs, rhs))
    2.20         val thm = prove ct 
    2.21 @@ -153,7 +153,7 @@
    2.22   val add_ac_ss = Data.ss addsimps [add_assoc,add_commute,add_left_commute];
    2.23  
    2.24   fun rel_proc sg _ (lhs as (rel$lt$rt)) =
    2.25 -   let val _ = if !trace then writeln ("cancel_relations: LHS = " ^ 
    2.26 +   let val _ = if !trace then tracing ("cancel_relations: LHS = " ^ 
    2.27  				       string_of_cterm (cterm_of sg lhs))
    2.28  	       else ()
    2.29         val ltms = terms lt
    2.30 @@ -170,7 +170,7 @@
    2.31  
    2.32         val rhs = rel$lt'$rt'
    2.33         val _ = if !trace then 
    2.34 -		 writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
    2.35 +		 tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
    2.36  	       else ()
    2.37         val ct = Thm.cterm_of sg (Logic.mk_equals (lhs,rhs))
    2.38  
     3.1 --- a/src/Provers/Arith/assoc_fold.ML	Wed Nov 21 00:35:13 2001 +0100
     3.2 +++ b/src/Provers/Arith/assoc_fold.ML	Wed Nov 21 00:36:51 2001 +0100
     3.3 @@ -52,14 +52,14 @@
     3.4   (*Make a simproc to combine all literals in a associative nest*)
     3.5   fun proc sg _ lhs =
     3.6     let fun show t = string_of_cterm (Thm.cterm_of sg t)
     3.7 -       val _ = if !trace then writeln ("assoc_fold simproc: LHS = " ^ show lhs)
     3.8 +       val _ = if !trace then tracing ("assoc_fold simproc: LHS = " ^ show lhs)
     3.9  	       else ()
    3.10         val (lits,others) = sift_terms (lhs, ([],[]))
    3.11         val _ = if length lits < 2
    3.12                 then raise Assoc_fail (*we can't reduce the number of terms*)
    3.13                 else ()  
    3.14         val rhs = Data.plus $ mk_sum lits $ mk_sum others
    3.15 -       val _ = if !trace then writeln ("RHS = " ^ show rhs) else ()
    3.16 +       val _ = if !trace then tracing ("RHS = " ^ show rhs) else ()
    3.17         val th = prove "assoc_fold" 
    3.18  	           (Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)))
    3.19  		   (fn _ => [rtac Data.eq_reflection 1,
     4.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Nov 21 00:35:13 2001 +0100
     4.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Nov 21 00:36:51 2001 +0100
     4.3 @@ -232,7 +232,7 @@
     4.4  
     4.5  fun print_ineqs ineqs =
     4.6    if !trace then
     4.7 -     writeln(cat_lines(""::map (fn Lineq(c,t,l,_) =>
     4.8 +     tracing(cat_lines(""::map (fn Lineq(c,t,l,_) =>
     4.9         string_of_int c ^
    4.10         (case t of Eq => " =  " | Lt=> " <  " | Le => " <= ") ^
    4.11         commas(map string_of_int l)) ineqs))
    4.12 @@ -280,10 +280,10 @@
    4.13  (* ------------------------------------------------------------------------- *)
    4.14  
    4.15  fun trace_thm msg th = 
    4.16 -    if !trace then (writeln msg; prth th) else th;
    4.17 +    if !trace then (tracing msg; tracing (Display.string_of_thm th); th) else th;
    4.18  
    4.19  fun trace_msg msg = 
    4.20 -    if !trace then writeln msg else ();
    4.21 +    if !trace then tracing msg else ();
    4.22  
    4.23  (* FIXME OPTIMIZE!!!!
    4.24     Addition/Multiplication need i*t representation rather than t+t+...
     5.1 --- a/src/Provers/hypsubst.ML	Wed Nov 21 00:35:13 2001 +0100
     5.2 +++ b/src/Provers/hypsubst.ML	Wed Nov 21 00:36:51 2001 +0100
     5.3 @@ -236,7 +236,7 @@
     5.4            val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
     5.5            val n = length hyps
     5.6        in
     5.7 -         if !trace then writeln "Substituting an equality" else ();
     5.8 +         if !trace then tracing "Substituting an equality" else ();
     5.9           DETERM
    5.10             (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
    5.11                     rotate_tac 1 i,
     6.1 --- a/src/Pure/Isar/method.ML	Wed Nov 21 00:35:13 2001 +0100
     6.2 +++ b/src/Pure/Isar/method.ML	Wed Nov 21 00:36:51 2001 +0100
     6.3 @@ -138,8 +138,9 @@
     6.4  val trace_rules = ref false;
     6.5  
     6.6  fun trace ctxt rules =
     6.7 -  if not (! trace_rules) orelse null rules then ()
     6.8 -  else Pretty.writeln (Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules));
     6.9 +  conditional (! trace_rules andalso not (null rules)) (fn () =>
    6.10 +    Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules)
    6.11 +    |> Pretty.string_of |> tracing);
    6.12  
    6.13  
    6.14  
     7.1 --- a/src/Pure/Syntax/ast.ML	Wed Nov 21 00:35:13 2001 +0100
     7.2 +++ b/src/Pure/Syntax/ast.ML	Wed Nov 21 00:36:51 2001 +0100
     7.3 @@ -157,12 +157,6 @@
     7.4  
     7.5  (** normalization of asts **)
     7.6  
     7.7 -(* tracing options *)
     7.8 -
     7.9 -val trace_ast = ref false;
    7.10 -val stat_ast = ref false;
    7.11 -
    7.12 -
    7.13  (* match *)
    7.14  
    7.15  fun match ast pat =
    7.16 @@ -228,9 +222,8 @@
    7.17        | rewrite ast = try_headless_rules ast;
    7.18  
    7.19      fun rewrote old_ast new_ast =
    7.20 -      if trace then
    7.21 -        writeln ("rewrote: " ^ str_of_ast old_ast ^ "  ->  " ^ str_of_ast new_ast)
    7.22 -      else ();
    7.23 +      conditional trace (fn () =>
    7.24 +        tracing ("rewrote: " ^ str_of_ast old_ast ^ "  ->  " ^ str_of_ast new_ast));
    7.25  
    7.26      fun norm_root ast =
    7.27        (case rewrite ast of
    7.28 @@ -258,22 +251,24 @@
    7.29        end;
    7.30  
    7.31  
    7.32 -    val _ = if trace then writeln ("pre: " ^ str_of_ast pre_ast) else ();
    7.33 +    val _ = conditional trace (fn () => tracing ("pre: " ^ str_of_ast pre_ast));
    7.34  
    7.35      val post_ast = normal pre_ast;
    7.36    in
    7.37 -    if trace orelse stat then
    7.38 -      writeln ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
    7.39 +    conditional (trace orelse stat) (fn () =>
    7.40 +      tracing ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
    7.41          string_of_int (! passes) ^ " passes, " ^
    7.42          string_of_int (! changes) ^ " changes, " ^
    7.43 -        string_of_int (! failed_matches) ^ " matches failed")
    7.44 -    else ();
    7.45 +        string_of_int (! failed_matches) ^ " matches failed"));
    7.46      post_ast
    7.47    end;
    7.48  
    7.49  
    7.50  (* normalize_ast *)
    7.51  
    7.52 +val trace_ast = ref false;
    7.53 +val stat_ast = ref false;
    7.54 +
    7.55  fun normalize_ast get_rules ast =
    7.56    normalize (! trace_ast) (! stat_ast) get_rules ast;
    7.57  
     8.1 --- a/src/Pure/meta_simplifier.ML	Wed Nov 21 00:35:13 2001 +0100
     8.2 +++ b/src/Pure/meta_simplifier.ML	Wed Nov 21 00:36:51 2001 +0100
     8.3 @@ -64,7 +64,7 @@
     8.4  
     8.5  val simp_depth = ref 0;
     8.6  
     8.7 -fun println a = writeln(replicate_string (!simp_depth) " " ^ a)
     8.8 +fun println a = tracing (replicate_string (! simp_depth) " " ^ a);
     8.9  
    8.10  fun prnt warn a = if warn then warning a else println a;
    8.11  
     9.1 --- a/src/Pure/search.ML	Wed Nov 21 00:35:13 2001 +0100
     9.2 +++ b/src/Pure/search.ML	Wed Nov 21 00:36:51 2001 +0100
     9.3 @@ -118,7 +118,7 @@
     9.4            | prune_aux (qs, (k,np,rgd,q)::rqs) =
     9.5  	      if np'+1 = np andalso rgd then
     9.6  		  (if !trace_DEPTH_FIRST then
     9.7 -		       writeln ("Pruning " ^ 
     9.8 +		       tracing ("Pruning " ^ 
     9.9  				string_of_int (1+length rqs) ^ " levels")
    9.10  		   else ();
    9.11  		   (*Use OLD k: zero-cost solution; see Stickel, p 365*)
    9.12 @@ -142,7 +142,7 @@
    9.13       and qs0 = tac0 st
    9.14       (*bnd = depth bound; inc = estimate of increment required next*)
    9.15       fun depth (bnd,inc) [] = 
    9.16 -	     (writeln (string_of_int (!countr) ^ 
    9.17 +	     (tracing (string_of_int (!countr) ^ 
    9.18  		       " inferences so far.  Searching to depth " ^ 
    9.19  		       string_of_int bnd);
    9.20  	      (*larger increments make it run slower for the hard problems*)
    9.21 @@ -152,7 +152,7 @@
    9.22            else
    9.23  	  case (countr := !countr+1;
    9.24  		if !trace_DEPTH_FIRST then
    9.25 -		    writeln (string_of_int np ^ 
    9.26 +		    tracing (string_of_int np ^ 
    9.27  			     implode (map (fn _ => "*") qs))
    9.28  		else ();
    9.29  		Seq.pull q) of
    9.30 @@ -185,8 +185,8 @@
    9.31  fun DEEPEN (inc,lim) tacf m i = 
    9.32    let fun dpn m st = st |> (if has_fewer_prems i st then no_tac
    9.33  			    else if m>lim then 
    9.34 -				(writeln "Giving up..."; no_tac)
    9.35 -				 else (writeln ("Depth = " ^ string_of_int m);
    9.36 +				(tracing "Giving up..."; no_tac)
    9.37 +				 else (tracing ("Depth = " ^ string_of_int m);
    9.38  				       tacf m i  ORELSE  dpn (m+inc)))
    9.39    in  dpn m  end;
    9.40  
    9.41 @@ -221,7 +221,7 @@
    9.42  	    else 
    9.43  	    let val (n,prf) = ThmHeap.min nprf_heap
    9.44  	    in if !trace_BEST_FIRST 
    9.45 -	       then writeln("state size = " ^ string_of_int n)  
    9.46 +	       then tracing("state size = " ^ string_of_int n)  
    9.47                 else ();
    9.48  	       bfs (Seq.list_of (tac prf), 
    9.49  		    deleteAllMin prf (ThmHeap.delete_min nprf_heap))
    9.50 @@ -245,7 +245,7 @@
    9.51  	    | (sats,_)  => sats)
    9.52    in (fn st => Seq.of_list (bfs [st])) end;
    9.53  
    9.54 -val BREADTH_FIRST = gen_BREADTH_FIRST writeln;
    9.55 +val BREADTH_FIRST = gen_BREADTH_FIRST tracing;
    9.56  val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ());
    9.57  
    9.58  
    9.59 @@ -281,7 +281,7 @@
    9.60        next []  = None
    9.61          | next ((level,n,prf)::nprfs)  =
    9.62              (if !trace_ASTAR 
    9.63 -               then writeln("level = " ^ string_of_int level ^
    9.64 +               then tracing("level = " ^ string_of_int level ^
    9.65  			 "  cost = " ^ string_of_int n ^ 
    9.66                           "  queue length =" ^ string_of_int (length nprfs))  
    9.67                 else ();
    10.1 --- a/src/Pure/tactic.ML	Wed Nov 21 00:35:13 2001 +0100
    10.2 +++ b/src/Pure/tactic.ML	Wed Nov 21 00:36:51 2001 +0100
    10.3 @@ -124,7 +124,7 @@
    10.4  fun trace_goalno_tac tac i st =
    10.5      case Seq.pull(tac i st) of
    10.6          None    => Seq.empty
    10.7 -      | seqcell => (writeln ("Subgoal " ^ string_of_int i ^ " selected");
    10.8 +      | seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected");
    10.9                           Seq.make(fn()=> seqcell));
   10.10  
   10.11  (*Makes a rule by applying a tactic to an existing rule*)
   10.12 @@ -285,8 +285,8 @@
   10.13    if i > nprems_of st then no_tac st
   10.14    else st |>
   10.15      (compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), nsubgoal) i
   10.16 -     handle TERM (msg,_)   => (writeln msg;  no_tac)
   10.17 -          | THM  (msg,_,_) => (writeln msg;  no_tac));
   10.18 +     handle TERM (msg,_)   => (warning msg;  no_tac)
   10.19 +          | THM  (msg,_,_) => (warning msg;  no_tac));
   10.20  
   10.21  (*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
   10.22    terms that are substituted contain (term or type) unknowns from the
    11.1 --- a/src/Pure/tctical.ML	Wed Nov 21 00:35:13 2001 +0100
    11.2 +++ b/src/Pure/tctical.ML	Wed Nov 21 00:36:51 2001 +0100
    11.3 @@ -198,14 +198,14 @@
    11.4  (*Print the current proof state and pass it on.*)
    11.5  fun print_tac msg = 
    11.6      (fn st => 
    11.7 -     (writeln msg;
    11.8 +     (tracing msg;
    11.9        Display.print_goals (! Display.goals_limit) st; Seq.single st));
   11.10  
   11.11  (*Pause until a line is typed -- if non-empty then fail. *)
   11.12  fun pause_tac st =  
   11.13 -  (writeln "** Press RETURN to continue:";
   11.14 +  (tracing "** Press RETURN to continue:";
   11.15     if TextIO.inputLine TextIO.stdIn = "\n" then Seq.single st
   11.16 -   else (writeln "Goodbye";  Seq.empty));
   11.17 +   else (tracing "Goodbye";  Seq.empty));
   11.18  
   11.19  exception TRACE_EXIT of thm
   11.20  and TRACE_QUIT;
   11.21 @@ -221,9 +221,9 @@
   11.22       | "f\n" => Seq.empty
   11.23       | "o\n" => (flag:=false;  tac st)
   11.24       | "s\n" => (suppress_tracing:=true;  tac st)
   11.25 -     | "x\n" => (writeln "Exiting now";  raise (TRACE_EXIT st))
   11.26 +     | "x\n" => (tracing "Exiting now";  raise (TRACE_EXIT st))
   11.27       | "quit\n" => raise TRACE_QUIT
   11.28 -     | _     => (writeln
   11.29 +     | _     => (tracing
   11.30  "Type RETURN to continue or...\n\
   11.31  \     f    - to fail here\n\
   11.32  \     o    - to switch tracing off\n\
   11.33 @@ -237,7 +237,7 @@
   11.34  fun tracify flag tac st =
   11.35    if !flag andalso not (!suppress_tracing)
   11.36             then (Display.print_goals (! Display.goals_limit) st;
   11.37 -                 writeln "** Press RETURN to continue:";
   11.38 +                 tracing "** Press RETURN to continue:";
   11.39                   exec_trace_command flag (tac,st))
   11.40    else tac st;
   11.41  
    12.1 --- a/src/Pure/unify.ML	Wed Nov 21 00:35:13 2001 +0100
    12.2 +++ b/src/Pure/unify.ML	Wed Nov 21 00:36:51 2001 +0100
    12.3 @@ -186,7 +186,7 @@
    12.4  
    12.5  fun test_unify_types(args as (T,U,_)) =
    12.6  let val sot = Sign.string_of_typ (!sgr);
    12.7 -    fun warn() = writeln("Potential loss of completeness: "^sot U^" = "^sot T);
    12.8 +    fun warn() = tracing ("Potential loss of completeness: "^sot U^" = "^sot T);
    12.9      val env' = unify_types(args)
   12.10  in if is_TVar(T) orelse is_TVar(U) then warn() else ();
   12.11     env'
   12.12 @@ -560,8 +560,8 @@
   12.13                                (Envir.norm_term env (rlist_abs(rbinder,t)))
   12.14              val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
   12.15                            termT t];
   12.16 -        in writeln(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
   12.17 -  in  writeln msg;  seq pdp dpairs  end;
   12.18 +        in tracing(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
   12.19 +  in  tracing msg;  seq pdp dpairs  end;
   12.20  
   12.21  
   12.22  (*Unify the dpairs in the environment.
   12.23 @@ -588,7 +588,7 @@
   12.24  			   (MATCH (env',dp, frigid'@flexflex), reseq)))
   12.25  	  end
   12.26  	  handle CANTUNIFY => 
   12.27 -	    (if tdepth > !trace_bound then writeln"Failure node" else ();
   12.28 +	    (if tdepth > !trace_bound then tracing"Failure node" else ();
   12.29  	     Seq.pull reseq));
   12.30       val dps = map (fn(t,u)=> ([],t,u)) tus
   12.31    in sgr := sg;