1.1 --- a/src/HOL/SMT/Tools/smt_monomorph.ML Thu Oct 15 21:08:03 2009 +0200
1.2 +++ b/src/HOL/SMT/Tools/smt_monomorph.ML Thu Oct 15 21:28:39 2009 +0200
1.3 @@ -112,7 +112,7 @@
1.4 in
1.5 if null is' then ts'
1.6 else if count > monomorph_limit then
1.7 - (Output.warning "monomorphization limit reached"; ts')
1.8 + (warning "monomorphization limit reached"; ts')
1.9 else mono (count + 1) is' ces' cs' ts'
1.10 end
1.11 in mono 0 (consts_of ms) (map (K []) rps) [] ms end
2.1 --- a/src/HOL/SMT/Tools/smt_solver.ML Thu Oct 15 21:08:03 2009 +0200
2.2 +++ b/src/HOL/SMT/Tools/smt_solver.ML Thu Oct 15 21:28:39 2009 +0200
2.3 @@ -84,7 +84,7 @@
2.4 val (trace, setup_trace) = Attrib.config_bool "smt_trace" false
2.5
2.6 fun trace_msg ctxt f x =
2.7 - if Config.get ctxt trace then Output.tracing (f x) else ()
2.8 + if Config.get ctxt trace then tracing (f x) else ()
2.9
2.10
2.11 (* interface to external solvers *)
3.1 --- a/src/HOL/Tools/Function/fundef_datatype.ML Thu Oct 15 21:08:03 2009 +0200
3.2 +++ b/src/HOL/Tools/Function/fundef_datatype.ML Thu Oct 15 21:28:39 2009 +0200
3.3 @@ -247,7 +247,7 @@
3.4 fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t)
3.5
3.6 val (tss', _) = chop (length origs) tss
3.7 - fun check (t, []) = (Output.warning (msg t); [])
3.8 + fun check (t, []) = (warning (msg t); [])
3.9 | check (t, s) = s
3.10 in
3.11 (map check (origs ~~ tss'); tss)
4.1 --- a/src/HOL/Tools/Function/induction_scheme.ML Thu Oct 15 21:08:03 2009 +0200
4.2 +++ b/src/HOL/Tools/Function/induction_scheme.ML Thu Oct 15 21:28:39 2009 +0200
4.3 @@ -355,7 +355,7 @@
4.4 let
4.5 val (ctxt', _, cases, concl) = dest_hhf ctxt t
4.6 val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
4.7 -(* val _ = Output.tracing (makestring scheme)*)
4.8 +(* val _ = tracing (makestring scheme)*)
4.9 val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
4.10 val R = Free (Rn, mk_relT ST)
4.11 val x = Free (xn, ST)
4.12 @@ -378,7 +378,7 @@
4.13 indthm |> Drule.instantiate' [] [SOME inst]
4.14 |> simplify SumTree.sumcase_split_ss
4.15 |> Conv.fconv_rule ind_rulify
4.16 -(* |> (fn thm => (Output.tracing (makestring thm); thm))*)
4.17 +(* |> (fn thm => (tracing (makestring thm); thm))*)
4.18 end
4.19
4.20 val res = Conjunction.intr_balanced (map_index project branches)
5.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Oct 15 21:08:03 2009 +0200
5.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Oct 15 21:28:39 2009 +0200
5.3 @@ -39,7 +39,7 @@
5.4 struct
5.5
5.6 val PROFILE = FundefCommon.PROFILE
5.7 -fun TRACE x = if ! FundefCommon.profile then Output.tracing x else ()
5.8 +fun TRACE x = if ! FundefCommon.profile then tracing x else ()
5.9
5.10 open ScnpSolve
5.11
5.12 @@ -316,17 +316,17 @@
5.13 fun index xs = (1 upto length xs) ~~ xs
5.14 fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
5.15 val ims = index (map index ms)
5.16 - val _ = Output.tracing (concat (outp "fn #" ":\n" (concat o outp "\tmeasure #" ": " (Syntax.string_of_term ctxt)) ims))
5.17 + val _ = tracing (concat (outp "fn #" ":\n" (concat o outp "\tmeasure #" ": " (Syntax.string_of_term ctxt)) ims))
5.18 fun print_call (k, c) =
5.19 let
5.20 val (_, p, _, q, _, _) = dest_call D c
5.21 - val _ = Output.tracing ("call table for call #" ^ Int.toString k ^ ": fn " ^
5.22 + val _ = tracing ("call table for call #" ^ Int.toString k ^ ": fn " ^
5.23 Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1))
5.24 val caller_ms = nth ms p
5.25 val callee_ms = nth ms q
5.26 val entries = map (fn x => map (pair x) (callee_ms)) (caller_ms)
5.27 fun print_ln (i : int, l) = concat (Int.toString i :: " " :: map (enclose " " " " o print_cell o (uncurry (get_descent D c))) l)
5.28 - val _ = Output.tracing (concat (Int.toString (p + 1) ^ "|" ^ Int.toString (q + 1) ^
5.29 + val _ = tracing (concat (Int.toString (p + 1) ^ "|" ^ Int.toString (q + 1) ^
5.30 " " :: map (enclose " " " " o Int.toString) (1 upto length callee_ms)) ^ "\n"
5.31 ^ cat_lines (map print_ln ((1 upto (length entries)) ~~ entries)))
5.32 in
5.33 @@ -335,7 +335,7 @@
5.34 fun list_call (k, c) =
5.35 let
5.36 val (_, p, _, q, _, _) = dest_call D c
5.37 - val _ = Output.tracing ("call #" ^ (Int.toString k) ^ ": fn " ^
5.38 + val _ = tracing ("call #" ^ (Int.toString k) ^ ": fn " ^
5.39 Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1) ^ "\n" ^
5.40 (Syntax.string_of_term ctxt c))
5.41 in true end
6.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Thu Oct 15 21:08:03 2009 +0200
6.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Thu Oct 15 21:28:39 2009 +0200
6.3 @@ -415,7 +415,7 @@
6.4 rewrite concl frees'
6.5 |> map (fn (concl'::conclprems, _) =>
6.6 Logic.list_implies ((flat prems') @ conclprems, concl')))
6.7 - val _ = Output.tracing ("intro_ts': " ^
6.8 + val _ = tracing ("intro_ts': " ^
6.9 commas (map (Syntax.string_of_term_global thy) intro_ts'))
6.10 in
6.11 map (Drule.standard o the_oracle () o cterm_of thy) intro_ts'
7.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Oct 15 21:08:03 2009 +0200
7.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Oct 15 21:28:39 2009 +0200
7.3 @@ -27,7 +27,7 @@
7.4 val (prednames, funnames) = List.partition (is_pred thy) constnames
7.5 (* untangle recursion by defining predicates for all functions *)
7.6 val _ = priority "Compiling functions to predicates..."
7.7 - val _ = Output.tracing ("funnames: " ^ commas funnames)
7.8 + val _ = tracing ("funnames: " ^ commas funnames)
7.9 val thy' =
7.10 thy |> not (null funnames) ? Predicate_Compile_Fun.define_predicates
7.11 (get_specs funnames)
7.12 @@ -54,10 +54,10 @@
7.13
7.14 fun preprocess const thy =
7.15 let
7.16 - val _ = Output.tracing ("Fetching definitions from theory...")
7.17 + val _ = tracing ("Fetching definitions from theory...")
7.18 val table = Pred_Compile_Data.make_const_spec_table thy
7.19 val gr = Pred_Compile_Data.obtain_specification_graph table const
7.20 - val _ = Output.tracing (commas (Graph.all_succs gr [const]))
7.21 + val _ = tracing (commas (Graph.all_succs gr [const]))
7.22 val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr
7.23 in fold_rev (preprocess_strong_conn_constnames gr)
7.24 (Graph.strong_conn gr) thy
8.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Oct 15 21:08:03 2009 +0200
8.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Oct 15 21:28:39 2009 +0200
8.3 @@ -118,10 +118,10 @@
8.4
8.5 (* debug stuff *)
8.6
8.7 -fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
8.8 +fun tracing s = (if ! Toplevel.debug then tracing s else ());
8.9
8.10 fun print_tac s = Seq.single; (*Tactical.print_tac s;*) (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
8.11 -fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
8.12 +fun debug_tac msg = Seq.single; (* (fn st => (tracing msg; Seq.single st)); *)
8.13
8.14 val do_proofs = Unsynchronized.ref true;
8.15
8.16 @@ -407,7 +407,7 @@
8.17
8.18 (* diagnostic display functions *)
8.19
8.20 -fun print_modes modes = Output.tracing ("Inferred modes:\n" ^
8.21 +fun print_modes modes = tracing ("Inferred modes:\n" ^
8.22 cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
8.23 string_of_mode ms)) modes));
8.24
8.25 @@ -417,7 +417,7 @@
8.26 ^ (string_of_entry pred mode entry)
8.27 fun print_pred (pred, modes) =
8.28 "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
8.29 - val _ = Output.tracing (cat_lines (map print_pred pred_mode_table))
8.30 + val _ = tracing (cat_lines (map print_pred pred_mode_table))
8.31 in () end;
8.32
8.33 fun string_of_moded_prem thy (Prem (ts, p), tmode) =
8.34 @@ -498,7 +498,7 @@
8.35
8.36 fun preprocess_elim thy nparams elimrule =
8.37 let
8.38 - val _ = Output.tracing ("Preprocessing elimination rule "
8.39 + val _ = tracing ("Preprocessing elimination rule "
8.40 ^ (Display.string_of_thm_global thy elimrule))
8.41 fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
8.42 HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
8.43 @@ -515,12 +515,12 @@
8.44 end
8.45 val cases' = map preprocess_case (tl prems)
8.46 val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
8.47 - (*val _ = Output.tracing ("elimrule': "^ (Syntax.string_of_term_global thy elimrule'))*)
8.48 + (*val _ = tracing ("elimrule': "^ (Syntax.string_of_term_global thy elimrule'))*)
8.49 val bigeq = (Thm.symmetric (Conv.implies_concl_conv
8.50 (MetaSimplifier.rewrite true [@{thm Predicate.eq_is_eq}])
8.51 (cterm_of thy elimrule')))
8.52 (*
8.53 - val _ = Output.tracing ("bigeq:" ^ (Display.string_of_thm_global thy bigeq))
8.54 + val _ = tracing ("bigeq:" ^ (Display.string_of_thm_global thy bigeq))
8.55 val res =
8.56 Thm.equal_elim bigeq elimrule
8.57 *)
8.58 @@ -528,7 +528,7 @@
8.59 val t = (fn {...} => mycheat_tac thy 1)
8.60 val eq = Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) t
8.61 *)
8.62 - val _ = Output.tracing "Preprocessed elimination rule"
8.63 + val _ = tracing "Preprocessed elimination rule"
8.64 in
8.65 Thm.equal_elim bigeq elimrule
8.66 end;
8.67 @@ -657,8 +657,8 @@
8.68 fun register_intros pre_intros thy =
8.69 let
8.70 val (c, T) = dest_Const (fst (strip_intro_concl 0 (prop_of (hd pre_intros))))
8.71 - val _ = Output.tracing ("Registering introduction rules of " ^ c)
8.72 - val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) pre_intros))
8.73 + val _ = tracing ("Registering introduction rules of " ^ c)
8.74 + val _ = tracing (commas (map (Display.string_of_thm_global thy) pre_intros))
8.75 val nparams = guess_nparams T
8.76 val pre_elim =
8.77 (Drule.standard o (setmp quick_and_dirty true (SkipProof.make_thm thy)))
8.78 @@ -1029,8 +1029,8 @@
8.79 fun check_mode_clause with_generator thy param_vs modes gen_modes (iss, is) (ts, ps) =
8.80 let
8.81 (*
8.82 - val _ = Output.tracing ("param_vs:" ^ commas param_vs)
8.83 - val _ = Output.tracing ("iss:" ^
8.84 + val _ = tracing ("param_vs:" ^ commas param_vs)
8.85 + val _ = tracing ("iss:" ^
8.86 commas (map (fn is => case is of SOME is => string_of_smode is | NONE => "NONE") iss))
8.87 *)
8.88 val modes' = modes @ List.mapPartial
8.89 @@ -1058,7 +1058,7 @@
8.90 SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
8.91 (vs union generator_vs) ps
8.92 | NONE => let
8.93 - val _ = Output.tracing ("ps:" ^ (commas
8.94 + val _ = tracing ("ps:" ^ (commas
8.95 (map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps)))
8.96 in (*error "mode analysis failed"*)NONE end
8.97 end)
8.98 @@ -1088,9 +1088,9 @@
8.99 in (p, List.filter (fn m => case find_index
8.100 (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
8.101 ~1 => true
8.102 - | i => (Output.tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
8.103 + | i => (tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
8.104 p ^ " violates mode " ^ string_of_mode m);
8.105 - Output.tracing (commas (map (Syntax.string_of_term_global thy) (fst (nth rs i)))); false)) ms)
8.106 + tracing (commas (map (Syntax.string_of_term_global thy) (fst (nth rs i)))); false)) ms)
8.107 end;
8.108
8.109 fun get_modes_pred with_generator thy param_vs clauses modes gen_modes (p, ms) =
8.110 @@ -2181,23 +2181,23 @@
8.111
8.112 fun add_equations_of steps prednames thy =
8.113 let
8.114 - val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
8.115 - val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
8.116 + val _ = tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
8.117 + val _ = tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
8.118 val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) =
8.119 prepare_intrs thy prednames
8.120 - val _ = Output.tracing "Infering modes..."
8.121 + val _ = tracing "Infering modes..."
8.122 val moded_clauses = #infer_modes steps thy extra_modes all_modes param_vs clauses
8.123 val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
8.124 val _ = print_modes modes
8.125 val _ = print_moded_clauses thy moded_clauses
8.126 - val _ = Output.tracing "Defining executable functions..."
8.127 + val _ = tracing "Defining executable functions..."
8.128 val thy' = fold (#create_definitions steps preds) modes thy
8.129 |> Theory.checkpoint
8.130 - val _ = Output.tracing "Compiling equations..."
8.131 + val _ = tracing "Compiling equations..."
8.132 val compiled_terms =
8.133 (#compile_preds steps) thy' all_vs param_vs preds moded_clauses
8.134 val _ = print_compiled_terms thy' compiled_terms
8.135 - val _ = Output.tracing "Proving equations..."
8.136 + val _ = tracing "Proving equations..."
8.137 val result_thms = #prove steps thy' clauses preds (extra_modes @ modes)
8.138 moded_clauses compiled_terms
8.139 val qname = #qname steps
9.1 --- a/src/HOL/Tools/refute.ML Thu Oct 15 21:08:03 2009 +0200
9.2 +++ b/src/HOL/Tools/refute.ML Thu Oct 15 21:28:39 2009 +0200
9.3 @@ -725,7 +725,7 @@
9.4 (* check this. However, getting this really right seems *)
9.5 (* difficult because the user may state arbitrary axioms, *)
9.6 (* which could interact with overloading to create loops. *)
9.7 - ((*Output.tracing (" unfolding: " ^ axname);*)
9.8 + ((*tracing (" unfolding: " ^ axname);*)
9.9 unfold_loop rhs)
9.10 | NONE => t)
9.11 | Free _ => t
9.12 @@ -765,20 +765,14 @@
9.13
9.14 fun collect_axioms thy t =
9.15 let
9.16 - val _ = Output.tracing "Adding axioms..."
9.17 - (* (string * Term.term) list *)
9.18 + val _ = tracing "Adding axioms..."
9.19 val axioms = Theory.all_axioms_of thy
9.20 - (* string * Term.term -> Term.term list -> Term.term list *)
9.21 fun collect_this_axiom (axname, ax) axs =
9.22 let
9.23 val ax' = unfold_defs thy ax
9.24 in
9.25 - if member (op aconv) axs ax' then
9.26 - axs
9.27 - else (
9.28 - Output.tracing axname;
9.29 - collect_term_axioms (ax' :: axs, ax')
9.30 - )
9.31 + if member (op aconv) axs ax' then axs
9.32 + else (tracing axname; collect_term_axioms (ax' :: axs, ax'))
9.33 end
9.34 (* Term.term list * Term.typ -> Term.term list *)
9.35 and collect_sort_axioms (axs, T) =
9.36 @@ -939,7 +933,7 @@
9.37 (collect_term_axioms (axs, t1), t2)
9.38 (* Term.term list *)
9.39 val result = map close_form (collect_term_axioms ([], t))
9.40 - val _ = Output.tracing " ...done."
9.41 + val _ = tracing " ...done."
9.42 in
9.43 result
9.44 end;
9.45 @@ -1157,13 +1151,12 @@
9.46 let
9.47 val timer = Timer.startRealTimer ()
9.48 val u = unfold_defs thy t
9.49 - val _ = Output.tracing ("Unfolded term: " ^
9.50 - Syntax.string_of_term_global thy u)
9.51 + val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u)
9.52 val axioms = collect_axioms thy u
9.53 (* Term.typ list *)
9.54 val types = Library.foldl (fn (acc, t') =>
9.55 acc union (ground_types thy t')) ([], u :: axioms)
9.56 - val _ = Output.tracing ("Ground types: "
9.57 + val _ = tracing ("Ground types: "
9.58 ^ (if null types then "none."
9.59 else commas (map (Syntax.string_of_typ_global thy) types)))
9.60 (* we can only consider fragments of recursive IDTs, so we issue a *)
9.61 @@ -1198,7 +1191,7 @@
9.62 val init_model = (universe, [])
9.63 val init_args = {maxvars = maxvars, def_eq = false, next_idx = 1,
9.64 bounds = [], wellformed = True}
9.65 - val _ = Output.tracing ("Translating term (sizes: "
9.66 + val _ = tracing ("Translating term (sizes: "
9.67 ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
9.68 (* translate 'u' and all axioms *)
9.69 val ((model, args), intrs) = Library.foldl_map (fn ((m, a), t') =>
9.70 @@ -1216,31 +1209,31 @@
9.71 val fm_ax = PropLogic.all (map toTrue (tl intrs))
9.72 val fm = PropLogic.all [#wellformed args, fm_ax, fm_u]
9.73 in
9.74 - Output.priority "Invoking SAT solver...";
9.75 + priority "Invoking SAT solver...";
9.76 (case SatSolver.invoke_solver satsolver fm of
9.77 SatSolver.SATISFIABLE assignment =>
9.78 - (Output.priority ("*** Model found: ***\n" ^ print_model thy model
9.79 + (priority ("*** Model found: ***\n" ^ print_model thy model
9.80 (fn i => case assignment i of SOME b => b | NONE => true));
9.81 if maybe_spurious then "potential" else "genuine")
9.82 | SatSolver.UNSATISFIABLE _ =>
9.83 - (Output.priority "No model exists.";
9.84 + (priority "No model exists.";
9.85 case next_universe universe sizes minsize maxsize of
9.86 SOME universe' => find_model_loop universe'
9.87 - | NONE => (Output.priority
9.88 + | NONE => (priority
9.89 "Search terminated, no larger universe within the given limits.";
9.90 "none"))
9.91 | SatSolver.UNKNOWN =>
9.92 - (Output.priority "No model found.";
9.93 + (priority "No model found.";
9.94 case next_universe universe sizes minsize maxsize of
9.95 SOME universe' => find_model_loop universe'
9.96 - | NONE => (Output.priority
9.97 + | NONE => (priority
9.98 "Search terminated, no larger universe within the given limits.";
9.99 "unknown"))
9.100 ) handle SatSolver.NOT_CONFIGURED =>
9.101 (error ("SAT solver " ^ quote satsolver ^ " is not configured.");
9.102 "unknown")
9.103 end handle MAXVARS_EXCEEDED =>
9.104 - (Output.priority ("Search terminated, number of Boolean variables ("
9.105 + (priority ("Search terminated, number of Boolean variables ("
9.106 ^ string_of_int maxvars ^ " allowed) exceeded.");
9.107 "unknown")
9.108 val outcome_code = find_model_loop (first_universe types sizes minsize)
9.109 @@ -1262,14 +1255,14 @@
9.110 maxtime>=0 orelse
9.111 error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0");
9.112 (* enter loop with or without time limit *)
9.113 - Output.priority ("Trying to find a model that "
9.114 + priority ("Trying to find a model that "
9.115 ^ (if negate then "refutes" else "satisfies") ^ ": "
9.116 ^ Syntax.string_of_term_global thy t);
9.117 if maxtime>0 then (
9.118 TimeLimit.timeLimit (Time.fromSeconds maxtime)
9.119 wrapper ()
9.120 handle TimeLimit.TimeOut =>
9.121 - Output.priority ("Search terminated, time limit (" ^
9.122 + priority ("Search terminated, time limit (" ^
9.123 string_of_int maxtime
9.124 ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.")
9.125 ) else
10.1 --- a/src/HOL/ex/predicate_compile.ML Thu Oct 15 21:08:03 2009 +0200
10.2 +++ b/src/HOL/ex/predicate_compile.ML Thu Oct 15 21:28:39 2009 +0200
10.3 @@ -106,10 +106,10 @@
10.4
10.5 (* debug stuff *)
10.6
10.7 -fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
10.8 +fun tracing s = (if ! Toplevel.debug then tracing s else ());
10.9
10.10 fun print_tac s = Seq.single; (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
10.11 -fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
10.12 +fun debug_tac msg = Seq.single; (* (fn st => (tracing msg; Seq.single st)); *)
10.13
10.14 val do_proofs = Unsynchronized.ref true;
10.15
10.16 @@ -344,7 +344,7 @@
10.17
10.18 (* diagnostic display functions *)
10.19
10.20 -fun print_modes modes = Output.tracing ("Inferred modes:\n" ^
10.21 +fun print_modes modes = tracing ("Inferred modes:\n" ^
10.22 cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
10.23 string_of_mode ms)) modes));
10.24
10.25 @@ -354,7 +354,7 @@
10.26 ^ (string_of_entry pred mode entry)
10.27 fun print_pred (pred, modes) =
10.28 "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
10.29 - val _ = Output.tracing (cat_lines (map print_pred pred_mode_table))
10.30 + val _ = tracing (cat_lines (map print_pred pred_mode_table))
10.31 in () end;
10.32
10.33 fun string_of_moded_prem thy (Prem (ts, p), tmode) =
10.34 @@ -1002,7 +1002,7 @@
10.35 in (p, List.filter (fn m => case find_index
10.36 (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
10.37 ~1 => true
10.38 - | i => (Output.tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
10.39 + | i => (tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
10.40 p ^ " violates mode " ^ string_of_mode m); false)) ms)
10.41 end;
10.42
10.43 @@ -1915,22 +1915,22 @@
10.44
10.45 fun add_equations_of steps prednames thy =
10.46 let
10.47 - val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
10.48 + val _ = tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
10.49 val (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) =
10.50 prepare_intrs thy prednames
10.51 - val _ = Output.tracing "Infering modes..."
10.52 + val _ = tracing "Infering modes..."
10.53 val moded_clauses = #infer_modes steps thy extra_modes arities param_vs clauses
10.54 val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
10.55 val _ = print_modes modes
10.56 val _ = print_moded_clauses thy moded_clauses
10.57 - val _ = Output.tracing "Defining executable functions..."
10.58 + val _ = tracing "Defining executable functions..."
10.59 val thy' = fold (#create_definitions steps preds) modes thy
10.60 |> Theory.checkpoint
10.61 - val _ = Output.tracing "Compiling equations..."
10.62 + val _ = tracing "Compiling equations..."
10.63 val compiled_terms =
10.64 (#compile_preds steps) thy' all_vs param_vs preds moded_clauses
10.65 val _ = print_compiled_terms thy' compiled_terms
10.66 - val _ = Output.tracing "Proving equations..."
10.67 + val _ = tracing "Proving equations..."
10.68 val result_thms = #prove steps thy' clauses preds (extra_modes @ modes)
10.69 moded_clauses compiled_terms
10.70 val qname = #qname steps