--- a/src/HOL/SMT/Tools/smt_monomorph.ML Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_monomorph.ML Thu Oct 15 21:28:39 2009 +0200
@@ -112,7 +112,7 @@
in
if null is' then ts'
else if count > monomorph_limit then
- (Output.warning "monomorphization limit reached"; ts')
+ (warning "monomorphization limit reached"; ts')
else mono (count + 1) is' ces' cs' ts'
end
in mono 0 (consts_of ms) (map (K []) rps) [] ms end
--- a/src/HOL/SMT/Tools/smt_solver.ML Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML Thu Oct 15 21:28:39 2009 +0200
@@ -84,7 +84,7 @@
val (trace, setup_trace) = Attrib.config_bool "smt_trace" false
fun trace_msg ctxt f x =
- if Config.get ctxt trace then Output.tracing (f x) else ()
+ if Config.get ctxt trace then tracing (f x) else ()
(* interface to external solvers *)
--- a/src/HOL/Tools/Function/fundef_datatype.ML Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_datatype.ML Thu Oct 15 21:28:39 2009 +0200
@@ -247,7 +247,7 @@
fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t)
val (tss', _) = chop (length origs) tss
- fun check (t, []) = (Output.warning (msg t); [])
+ fun check (t, []) = (warning (msg t); [])
| check (t, s) = s
in
(map check (origs ~~ tss'); tss)
--- a/src/HOL/Tools/Function/induction_scheme.ML Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/Tools/Function/induction_scheme.ML Thu Oct 15 21:28:39 2009 +0200
@@ -355,7 +355,7 @@
let
val (ctxt', _, cases, concl) = dest_hhf ctxt t
val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
-(* val _ = Output.tracing (makestring scheme)*)
+(* val _ = tracing (makestring scheme)*)
val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
val R = Free (Rn, mk_relT ST)
val x = Free (xn, ST)
@@ -378,7 +378,7 @@
indthm |> Drule.instantiate' [] [SOME inst]
|> simplify SumTree.sumcase_split_ss
|> Conv.fconv_rule ind_rulify
-(* |> (fn thm => (Output.tracing (makestring thm); thm))*)
+(* |> (fn thm => (tracing (makestring thm); thm))*)
end
val res = Conjunction.intr_balanced (map_index project branches)
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Oct 15 21:28:39 2009 +0200
@@ -39,7 +39,7 @@
struct
val PROFILE = FundefCommon.PROFILE
-fun TRACE x = if ! FundefCommon.profile then Output.tracing x else ()
+fun TRACE x = if ! FundefCommon.profile then tracing x else ()
open ScnpSolve
@@ -316,17 +316,17 @@
fun index xs = (1 upto length xs) ~~ xs
fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
val ims = index (map index ms)
- val _ = Output.tracing (concat (outp "fn #" ":\n" (concat o outp "\tmeasure #" ": " (Syntax.string_of_term ctxt)) ims))
+ val _ = tracing (concat (outp "fn #" ":\n" (concat o outp "\tmeasure #" ": " (Syntax.string_of_term ctxt)) ims))
fun print_call (k, c) =
let
val (_, p, _, q, _, _) = dest_call D c
- val _ = Output.tracing ("call table for call #" ^ Int.toString k ^ ": fn " ^
+ val _ = tracing ("call table for call #" ^ Int.toString k ^ ": fn " ^
Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1))
val caller_ms = nth ms p
val callee_ms = nth ms q
val entries = map (fn x => map (pair x) (callee_ms)) (caller_ms)
fun print_ln (i : int, l) = concat (Int.toString i :: " " :: map (enclose " " " " o print_cell o (uncurry (get_descent D c))) l)
- val _ = Output.tracing (concat (Int.toString (p + 1) ^ "|" ^ Int.toString (q + 1) ^
+ val _ = tracing (concat (Int.toString (p + 1) ^ "|" ^ Int.toString (q + 1) ^
" " :: map (enclose " " " " o Int.toString) (1 upto length callee_ms)) ^ "\n"
^ cat_lines (map print_ln ((1 upto (length entries)) ~~ entries)))
in
@@ -335,7 +335,7 @@
fun list_call (k, c) =
let
val (_, p, _, q, _, _) = dest_call D c
- val _ = Output.tracing ("call #" ^ (Int.toString k) ^ ": fn " ^
+ val _ = tracing ("call #" ^ (Int.toString k) ^ ": fn " ^
Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1) ^ "\n" ^
(Syntax.string_of_term ctxt c))
in true end
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Thu Oct 15 21:28:39 2009 +0200
@@ -415,7 +415,7 @@
rewrite concl frees'
|> map (fn (concl'::conclprems, _) =>
Logic.list_implies ((flat prems') @ conclprems, concl')))
- val _ = Output.tracing ("intro_ts': " ^
+ val _ = tracing ("intro_ts': " ^
commas (map (Syntax.string_of_term_global thy) intro_ts'))
in
map (Drule.standard o the_oracle () o cterm_of thy) intro_ts'
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Oct 15 21:28:39 2009 +0200
@@ -27,7 +27,7 @@
val (prednames, funnames) = List.partition (is_pred thy) constnames
(* untangle recursion by defining predicates for all functions *)
val _ = priority "Compiling functions to predicates..."
- val _ = Output.tracing ("funnames: " ^ commas funnames)
+ val _ = tracing ("funnames: " ^ commas funnames)
val thy' =
thy |> not (null funnames) ? Predicate_Compile_Fun.define_predicates
(get_specs funnames)
@@ -54,10 +54,10 @@
fun preprocess const thy =
let
- val _ = Output.tracing ("Fetching definitions from theory...")
+ val _ = tracing ("Fetching definitions from theory...")
val table = Pred_Compile_Data.make_const_spec_table thy
val gr = Pred_Compile_Data.obtain_specification_graph table const
- val _ = Output.tracing (commas (Graph.all_succs gr [const]))
+ val _ = tracing (commas (Graph.all_succs gr [const]))
val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr
in fold_rev (preprocess_strong_conn_constnames gr)
(Graph.strong_conn gr) thy
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Oct 15 21:28:39 2009 +0200
@@ -118,10 +118,10 @@
(* debug stuff *)
-fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
+fun tracing s = (if ! Toplevel.debug then tracing s else ());
fun print_tac s = Seq.single; (*Tactical.print_tac s;*) (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
-fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
+fun debug_tac msg = Seq.single; (* (fn st => (tracing msg; Seq.single st)); *)
val do_proofs = Unsynchronized.ref true;
@@ -407,7 +407,7 @@
(* diagnostic display functions *)
-fun print_modes modes = Output.tracing ("Inferred modes:\n" ^
+fun print_modes modes = tracing ("Inferred modes:\n" ^
cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
string_of_mode ms)) modes));
@@ -417,7 +417,7 @@
^ (string_of_entry pred mode entry)
fun print_pred (pred, modes) =
"predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
- val _ = Output.tracing (cat_lines (map print_pred pred_mode_table))
+ val _ = tracing (cat_lines (map print_pred pred_mode_table))
in () end;
fun string_of_moded_prem thy (Prem (ts, p), tmode) =
@@ -498,7 +498,7 @@
fun preprocess_elim thy nparams elimrule =
let
- val _ = Output.tracing ("Preprocessing elimination rule "
+ val _ = tracing ("Preprocessing elimination rule "
^ (Display.string_of_thm_global thy elimrule))
fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
@@ -515,12 +515,12 @@
end
val cases' = map preprocess_case (tl prems)
val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
- (*val _ = Output.tracing ("elimrule': "^ (Syntax.string_of_term_global thy elimrule'))*)
+ (*val _ = tracing ("elimrule': "^ (Syntax.string_of_term_global thy elimrule'))*)
val bigeq = (Thm.symmetric (Conv.implies_concl_conv
(MetaSimplifier.rewrite true [@{thm Predicate.eq_is_eq}])
(cterm_of thy elimrule')))
(*
- val _ = Output.tracing ("bigeq:" ^ (Display.string_of_thm_global thy bigeq))
+ val _ = tracing ("bigeq:" ^ (Display.string_of_thm_global thy bigeq))
val res =
Thm.equal_elim bigeq elimrule
*)
@@ -528,7 +528,7 @@
val t = (fn {...} => mycheat_tac thy 1)
val eq = Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) t
*)
- val _ = Output.tracing "Preprocessed elimination rule"
+ val _ = tracing "Preprocessed elimination rule"
in
Thm.equal_elim bigeq elimrule
end;
@@ -657,8 +657,8 @@
fun register_intros pre_intros thy =
let
val (c, T) = dest_Const (fst (strip_intro_concl 0 (prop_of (hd pre_intros))))
- val _ = Output.tracing ("Registering introduction rules of " ^ c)
- val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) pre_intros))
+ val _ = tracing ("Registering introduction rules of " ^ c)
+ val _ = tracing (commas (map (Display.string_of_thm_global thy) pre_intros))
val nparams = guess_nparams T
val pre_elim =
(Drule.standard o (setmp quick_and_dirty true (SkipProof.make_thm thy)))
@@ -1029,8 +1029,8 @@
fun check_mode_clause with_generator thy param_vs modes gen_modes (iss, is) (ts, ps) =
let
(*
- val _ = Output.tracing ("param_vs:" ^ commas param_vs)
- val _ = Output.tracing ("iss:" ^
+ val _ = tracing ("param_vs:" ^ commas param_vs)
+ val _ = tracing ("iss:" ^
commas (map (fn is => case is of SOME is => string_of_smode is | NONE => "NONE") iss))
*)
val modes' = modes @ List.mapPartial
@@ -1058,7 +1058,7 @@
SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
(vs union generator_vs) ps
| NONE => let
- val _ = Output.tracing ("ps:" ^ (commas
+ val _ = tracing ("ps:" ^ (commas
(map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps)))
in (*error "mode analysis failed"*)NONE end
end)
@@ -1088,9 +1088,9 @@
in (p, List.filter (fn m => case find_index
(is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
~1 => true
- | i => (Output.tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
+ | i => (tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
p ^ " violates mode " ^ string_of_mode m);
- Output.tracing (commas (map (Syntax.string_of_term_global thy) (fst (nth rs i)))); false)) ms)
+ tracing (commas (map (Syntax.string_of_term_global thy) (fst (nth rs i)))); false)) ms)
end;
fun get_modes_pred with_generator thy param_vs clauses modes gen_modes (p, ms) =
@@ -2181,23 +2181,23 @@
fun add_equations_of steps prednames thy =
let
- val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
- val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
+ val _ = tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
+ val _ = tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) =
prepare_intrs thy prednames
- val _ = Output.tracing "Infering modes..."
+ val _ = tracing "Infering modes..."
val moded_clauses = #infer_modes steps thy extra_modes all_modes param_vs clauses
val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
val _ = print_modes modes
val _ = print_moded_clauses thy moded_clauses
- val _ = Output.tracing "Defining executable functions..."
+ val _ = tracing "Defining executable functions..."
val thy' = fold (#create_definitions steps preds) modes thy
|> Theory.checkpoint
- val _ = Output.tracing "Compiling equations..."
+ val _ = tracing "Compiling equations..."
val compiled_terms =
(#compile_preds steps) thy' all_vs param_vs preds moded_clauses
val _ = print_compiled_terms thy' compiled_terms
- val _ = Output.tracing "Proving equations..."
+ val _ = tracing "Proving equations..."
val result_thms = #prove steps thy' clauses preds (extra_modes @ modes)
moded_clauses compiled_terms
val qname = #qname steps
--- a/src/HOL/Tools/refute.ML Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/Tools/refute.ML Thu Oct 15 21:28:39 2009 +0200
@@ -725,7 +725,7 @@
(* check this. However, getting this really right seems *)
(* difficult because the user may state arbitrary axioms, *)
(* which could interact with overloading to create loops. *)
- ((*Output.tracing (" unfolding: " ^ axname);*)
+ ((*tracing (" unfolding: " ^ axname);*)
unfold_loop rhs)
| NONE => t)
| Free _ => t
@@ -765,20 +765,14 @@
fun collect_axioms thy t =
let
- val _ = Output.tracing "Adding axioms..."
- (* (string * Term.term) list *)
+ val _ = tracing "Adding axioms..."
val axioms = Theory.all_axioms_of thy
- (* string * Term.term -> Term.term list -> Term.term list *)
fun collect_this_axiom (axname, ax) axs =
let
val ax' = unfold_defs thy ax
in
- if member (op aconv) axs ax' then
- axs
- else (
- Output.tracing axname;
- collect_term_axioms (ax' :: axs, ax')
- )
+ if member (op aconv) axs ax' then axs
+ else (tracing axname; collect_term_axioms (ax' :: axs, ax'))
end
(* Term.term list * Term.typ -> Term.term list *)
and collect_sort_axioms (axs, T) =
@@ -939,7 +933,7 @@
(collect_term_axioms (axs, t1), t2)
(* Term.term list *)
val result = map close_form (collect_term_axioms ([], t))
- val _ = Output.tracing " ...done."
+ val _ = tracing " ...done."
in
result
end;
@@ -1157,13 +1151,12 @@
let
val timer = Timer.startRealTimer ()
val u = unfold_defs thy t
- val _ = Output.tracing ("Unfolded term: " ^
- Syntax.string_of_term_global thy u)
+ val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u)
val axioms = collect_axioms thy u
(* Term.typ list *)
val types = Library.foldl (fn (acc, t') =>
acc union (ground_types thy t')) ([], u :: axioms)
- val _ = Output.tracing ("Ground types: "
+ val _ = tracing ("Ground types: "
^ (if null types then "none."
else commas (map (Syntax.string_of_typ_global thy) types)))
(* we can only consider fragments of recursive IDTs, so we issue a *)
@@ -1198,7 +1191,7 @@
val init_model = (universe, [])
val init_args = {maxvars = maxvars, def_eq = false, next_idx = 1,
bounds = [], wellformed = True}
- val _ = Output.tracing ("Translating term (sizes: "
+ val _ = tracing ("Translating term (sizes: "
^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
(* translate 'u' and all axioms *)
val ((model, args), intrs) = Library.foldl_map (fn ((m, a), t') =>
@@ -1216,31 +1209,31 @@
val fm_ax = PropLogic.all (map toTrue (tl intrs))
val fm = PropLogic.all [#wellformed args, fm_ax, fm_u]
in
- Output.priority "Invoking SAT solver...";
+ priority "Invoking SAT solver...";
(case SatSolver.invoke_solver satsolver fm of
SatSolver.SATISFIABLE assignment =>
- (Output.priority ("*** Model found: ***\n" ^ print_model thy model
+ (priority ("*** Model found: ***\n" ^ print_model thy model
(fn i => case assignment i of SOME b => b | NONE => true));
if maybe_spurious then "potential" else "genuine")
| SatSolver.UNSATISFIABLE _ =>
- (Output.priority "No model exists.";
+ (priority "No model exists.";
case next_universe universe sizes minsize maxsize of
SOME universe' => find_model_loop universe'
- | NONE => (Output.priority
+ | NONE => (priority
"Search terminated, no larger universe within the given limits.";
"none"))
| SatSolver.UNKNOWN =>
- (Output.priority "No model found.";
+ (priority "No model found.";
case next_universe universe sizes minsize maxsize of
SOME universe' => find_model_loop universe'
- | NONE => (Output.priority
+ | NONE => (priority
"Search terminated, no larger universe within the given limits.";
"unknown"))
) handle SatSolver.NOT_CONFIGURED =>
(error ("SAT solver " ^ quote satsolver ^ " is not configured.");
"unknown")
end handle MAXVARS_EXCEEDED =>
- (Output.priority ("Search terminated, number of Boolean variables ("
+ (priority ("Search terminated, number of Boolean variables ("
^ string_of_int maxvars ^ " allowed) exceeded.");
"unknown")
val outcome_code = find_model_loop (first_universe types sizes minsize)
@@ -1262,14 +1255,14 @@
maxtime>=0 orelse
error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0");
(* enter loop with or without time limit *)
- Output.priority ("Trying to find a model that "
+ priority ("Trying to find a model that "
^ (if negate then "refutes" else "satisfies") ^ ": "
^ Syntax.string_of_term_global thy t);
if maxtime>0 then (
TimeLimit.timeLimit (Time.fromSeconds maxtime)
wrapper ()
handle TimeLimit.TimeOut =>
- Output.priority ("Search terminated, time limit (" ^
+ priority ("Search terminated, time limit (" ^
string_of_int maxtime
^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.")
) else
--- a/src/HOL/ex/predicate_compile.ML Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Thu Oct 15 21:28:39 2009 +0200
@@ -106,10 +106,10 @@
(* debug stuff *)
-fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
+fun tracing s = (if ! Toplevel.debug then tracing s else ());
fun print_tac s = Seq.single; (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
-fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
+fun debug_tac msg = Seq.single; (* (fn st => (tracing msg; Seq.single st)); *)
val do_proofs = Unsynchronized.ref true;
@@ -344,7 +344,7 @@
(* diagnostic display functions *)
-fun print_modes modes = Output.tracing ("Inferred modes:\n" ^
+fun print_modes modes = tracing ("Inferred modes:\n" ^
cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
string_of_mode ms)) modes));
@@ -354,7 +354,7 @@
^ (string_of_entry pred mode entry)
fun print_pred (pred, modes) =
"predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
- val _ = Output.tracing (cat_lines (map print_pred pred_mode_table))
+ val _ = tracing (cat_lines (map print_pred pred_mode_table))
in () end;
fun string_of_moded_prem thy (Prem (ts, p), tmode) =
@@ -1002,7 +1002,7 @@
in (p, List.filter (fn m => case find_index
(is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
~1 => true
- | i => (Output.tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
+ | i => (tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
p ^ " violates mode " ^ string_of_mode m); false)) ms)
end;
@@ -1915,22 +1915,22 @@
fun add_equations_of steps prednames thy =
let
- val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
+ val _ = tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
val (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) =
prepare_intrs thy prednames
- val _ = Output.tracing "Infering modes..."
+ val _ = tracing "Infering modes..."
val moded_clauses = #infer_modes steps thy extra_modes arities param_vs clauses
val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
val _ = print_modes modes
val _ = print_moded_clauses thy moded_clauses
- val _ = Output.tracing "Defining executable functions..."
+ val _ = tracing "Defining executable functions..."
val thy' = fold (#create_definitions steps preds) modes thy
|> Theory.checkpoint
- val _ = Output.tracing "Compiling equations..."
+ val _ = tracing "Compiling equations..."
val compiled_terms =
(#compile_preds steps) thy' all_vs param_vs preds moded_clauses
val _ = print_compiled_terms thy' compiled_terms
- val _ = Output.tracing "Proving equations..."
+ val _ = tracing "Proving equations..."
val result_thms = #prove steps thy' clauses preds (extra_modes @ modes)
moded_clauses compiled_terms
val qname = #qname steps