--- a/src/HOL/Tools/Function/fundef_core.ML Fri Oct 16 00:26:19 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_core.ML Fri Oct 16 10:45:10 2009 +0200
@@ -7,6 +7,8 @@
signature FUNDEF_CORE =
sig
+ val trace: bool Unsynchronized.ref
+
val prepare_fundef : FundefCommon.fundef_config
-> string (* defname *)
-> ((bstring * typ) * mixfix) list (* defined symbol *)
@@ -23,6 +25,9 @@
structure FundefCore : FUNDEF_CORE =
struct
+val trace = Unsynchronized.ref false;
+fun trace_msg msg = if ! trace then tracing (msg ()) else ();
+
val boolT = HOLogic.boolT
val mk_eq = HOLogic.mk_eq
@@ -420,14 +425,14 @@
val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
|> instantiate' [] [NONE, SOME (cterm_of thy h)]
- val _ = Output.debug (K "Proving Replacement lemmas...")
+ val _ = trace_msg (K "Proving Replacement lemmas...")
val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
- val _ = Output.debug (K "Proving cases for unique existence...")
+ val _ = trace_msg (K "Proving cases for unique existence...")
val (ex1s, values) =
split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
- val _ = Output.debug (K "Proving: Graph is a function")
+ val _ = trace_msg (K "Proving: Graph is a function")
val graph_is_function = complete
|> Thm.forall_elim_vars 0
|> fold (curry op COMP) ex1s
--- a/src/HOL/Tools/meson.ML Fri Oct 16 00:26:19 2009 +0200
+++ b/src/HOL/Tools/meson.ML Fri Oct 16 10:45:10 2009 +0200
@@ -7,6 +7,7 @@
signature MESON =
sig
+ val trace: bool Unsynchronized.ref
val term_pair_of: indexname * (typ * 'a) -> term * 'a
val first_order_resolve: thm -> thm -> thm
val flexflex_first_order: thm -> thm
@@ -42,6 +43,9 @@
structure Meson: MESON =
struct
+val trace = Unsynchronized.ref false;
+fun trace_msg msg = if ! trace then tracing (msg ()) else ();
+
val max_clauses_default = 60;
val (max_clauses, setup) = Attrib.config_int "max_clauses" max_clauses_default;
@@ -344,7 +348,7 @@
and cnf_nil th = cnf_aux (th,[])
val cls =
if too_many_clauses (SOME ctxt) (concl_of th)
- then (warning ("cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
+ then (trace_msg (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
else cnf_aux (th,ths)
in (cls, !ctxtr) end;
@@ -547,7 +551,7 @@
| skolemize_nnf_list ctxt (th::ths) =
skolemize ctxt th :: skolemize_nnf_list ctxt ths
handle THM _ => (*RS can fail if Unify.search_bound is too small*)
- (warning ("Failed to Skolemize " ^ Display.string_of_thm ctxt th);
+ (trace_msg (fn () => "Failed to Skolemize " ^ Display.string_of_thm ctxt th);
skolemize_nnf_list ctxt ths);
fun add_clauses (th,cls) =
@@ -636,7 +640,7 @@
| goes =>
let
val horns = make_horns (cls @ ths)
- val _ = Output.debug (fn () =>
+ val _ = trace_msg (fn () =>
cat_lines ("meson method called:" ::
map (Display.string_of_thm ctxt) (cls @ ths) @
["clauses:"] @ map (Display.string_of_thm ctxt) horns))
--- a/src/HOL/Tools/metis_tools.ML Fri Oct 16 00:26:19 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML Fri Oct 16 10:45:10 2009 +0200
@@ -7,6 +7,7 @@
signature METIS_TOOLS =
sig
+ val trace: bool Unsynchronized.ref
val type_lits: bool Config.T
val metis_tac: Proof.context -> thm list -> int -> tactic
val metisF_tac: Proof.context -> thm list -> int -> tactic
@@ -17,6 +18,9 @@
structure MetisTools: METIS_TOOLS =
struct
+ val trace = Unsynchronized.ref false;
+ fun trace_msg msg = if ! trace then tracing (msg ()) else ();
+
structure Recon = ResReconstruct;
val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true;
@@ -221,7 +225,7 @@
(*Maps metis terms to isabelle terms*)
fun fol_term_to_hol_RAW ctxt fol_tm =
let val thy = ProofContext.theory_of ctxt
- val _ = Output.debug (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
+ val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
fun tm_to_tt (Metis.Term.Var v) =
(case Recon.strip_prefix ResClause.tvar_prefix v of
SOME w => Type (Recon.make_tvar w)
@@ -276,7 +280,7 @@
(*Maps fully-typed metis terms to isabelle terms*)
fun fol_term_to_hol_FT ctxt fol_tm =
- let val _ = Output.debug (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
+ let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, ty])) =
(case Recon.strip_prefix ResClause.schematic_var_prefix v of
SOME w => mk_var(w, dummyT)
@@ -303,8 +307,8 @@
| NONE => (*Not a constant. Is it a fixed variable??*)
case Recon.strip_prefix ResClause.fixed_var_prefix x of
SOME v => Free (v, dummyT)
- | NONE => (Output.debug (fn () => "fol_term_to_hol_FT bad const: " ^ x); fol_term_to_hol_RAW ctxt t))
- | cvt t = (Output.debug (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t); fol_term_to_hol_RAW ctxt t)
+ | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x); fol_term_to_hol_RAW ctxt t))
+ | cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t); fol_term_to_hol_RAW ctxt t)
in cvt fol_tm end;
fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt
@@ -313,10 +317,10 @@
fun fol_terms_to_hol ctxt mode fol_tms =
let val ts = map (fol_term_to_hol ctxt mode) fol_tms
- val _ = Output.debug (fn () => " calling type inference:")
- val _ = app (fn t => Output.debug (fn () => Syntax.string_of_term ctxt t)) ts
+ val _ = trace_msg (fn () => " calling type inference:")
+ val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
val ts' = infer_types ctxt ts;
- val _ = app (fn t => Output.debug
+ val _ = app (fn t => trace_msg
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
" of type " ^ Syntax.string_of_typ ctxt (type_of t)))
ts'
@@ -333,9 +337,9 @@
(*for debugging only*)
fun print_thpair (fth,th) =
- (Output.debug (fn () => "=============================================");
- Output.debug (fn () => "Metis: " ^ Metis.Thm.toString fth);
- Output.debug (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
+ (trace_msg (fn () => "=============================================");
+ trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth);
+ trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
fun lookth thpairs (fth : Metis.Thm.thm) =
valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
@@ -374,7 +378,7 @@
val t = fol_term_to_hol ctxt mode y (*we call infer_types below*)
in SOME (cterm_of thy (Var v), t) end
handle Option =>
- (Output.debug (fn() => "List.find failed for the variable " ^ x ^
+ (trace_msg (fn() => "List.find failed for the variable " ^ x ^
" in " ^ Display.string_of_thm ctxt i_th);
NONE)
fun remove_typeinst (a, t) =
@@ -383,13 +387,13 @@
| NONE => case Recon.strip_prefix ResClause.tvar_prefix a of
SOME _ => NONE (*type instantiations are forbidden!*)
| NONE => SOME (a,t) (*internal Metis var?*)
- val _ = Output.debug (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
+ val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
val tms = infer_types ctxt rawtms;
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
val substs' = ListPair.zip (vars, map ctm_of tms)
- val _ = Output.debug (fn () =>
+ val _ = trace_msg (fn () =>
cat_lines ("subst_translations:" ::
(substs' |> map (fn (x, y) =>
Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
@@ -416,23 +420,23 @@
let
val thy = ProofContext.theory_of ctxt
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
- val _ = Output.debug (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
- val _ = Output.debug (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
+ val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
+ val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
in
if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
else if is_TrueI i_th2 then i_th1
else
let
val i_atm = singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm)
- val _ = Output.debug (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
+ val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
val prems_th1 = prems_of i_th1
val prems_th2 = prems_of i_th2
val index_th1 = get_index (mk_not i_atm) prems_th1
handle Empty => error "Failed to find literal in th1"
- val _ = Output.debug (fn () => " index_th1: " ^ Int.toString index_th1)
+ val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1)
val index_th2 = get_index i_atm prems_th2
handle Empty => error "Failed to find literal in th2"
- val _ = Output.debug (fn () => " index_th2: " ^ Int.toString index_th2)
+ val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2)
in resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2) end
end;
@@ -443,7 +447,7 @@
fun refl_inf ctxt mode t =
let val thy = ProofContext.theory_of ctxt
val i_t = singleton (fol_terms_to_hol ctxt mode) t
- val _ = Output.debug (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
+ val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
@@ -456,7 +460,7 @@
let val thy = ProofContext.theory_of ctxt
val m_tm = Metis.Term.Fn atm
val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr]
- val _ = Output.debug (fn () => "sign of the literal: " ^ Bool.toString pos)
+ val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
fun replace_item_list lx 0 (l::ls) = lx::ls
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
fun path_finder_FO tm [] = (tm, Term.Bound 0)
@@ -467,7 +471,7 @@
val tm_p = List.nth(args,p')
handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^
Int.toString adjustment ^ " term " ^ Syntax.string_of_term ctxt tm)
- val _ = Output.debug (fn () => "path_finder: " ^ Int.toString p ^
+ val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
" " ^ Syntax.string_of_term ctxt tm_p)
val (r,t) = path_finder_FO tm_p ps
in
@@ -512,12 +516,12 @@
| path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
val (tm_subst, body) = path_finder_lit i_atm fp
val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
- val _ = Output.debug (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
- val _ = Output.debug (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
- val _ = Output.debug (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
+ val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
+ val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
+ val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*)
val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
- val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
+ val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
val eq_terms = map (pairself (cterm_of thy))
(ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
in cterm_instantiate eq_terms subst' end;
@@ -541,12 +545,12 @@
fun translate mode _ thpairs [] = thpairs
| translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
- let val _ = Output.debug (fn () => "=============================================")
- val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
- val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
+ let val _ = trace_msg (fn () => "=============================================")
+ val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
+ val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf))
- val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
- val _ = Output.debug (fn () => "=============================================")
+ val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
+ val _ = trace_msg (fn () => "=============================================")
val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
in
if nprems_of th = n_metis_lits then ()
@@ -665,52 +669,52 @@
let val thy = ProofContext.theory_of ctxt
val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
val ths = maps #2 th_cls_pairs
- val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
- val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) cls
- val _ = Output.debug (fn () => "THEOREM CLAUSES")
- val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) ths
+ val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
+ val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
+ val _ = trace_msg (fn () => "THEOREM CLAUSES")
+ val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
val _ = if null tfrees then ()
- else (Output.debug (fn () => "TFREE CLAUSES");
- app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)
- val _ = Output.debug (fn () => "CLAUSES GIVEN TO METIS")
+ else (trace_msg (fn () => "TFREE CLAUSES");
+ app (fn tf => trace_msg (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)
+ val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
val thms = map #1 axioms
- val _ = app (fn th => Output.debug (fn () => Metis.Thm.toString th)) thms
- val _ = Output.debug (fn () => "mode = " ^ string_of_mode mode)
- val _ = Output.debug (fn () => "START METIS PROVE PROCESS")
+ val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
+ val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
+ val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
in
case List.filter (is_false o prop_of) cls of
false_th::_ => [false_th RS @{thm FalseE}]
| [] =>
case refute thms of
Metis.Resolution.Contradiction mth =>
- let val _ = Output.debug (fn () => "METIS RECONSTRUCTION START: " ^
+ let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
Metis.Thm.toString mth)
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
(*add constraints arising from converting goal to clause form*)
val proof = Metis.Proof.proof mth
val result = translate mode ctxt' axioms proof
and used = map_filter (used_axioms axioms) proof
- val _ = Output.debug (fn () => "METIS COMPLETED...clauses actually used:")
- val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) used
+ val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
+ val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
in
if null unused then ()
else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
case result of
(_,ith)::_ =>
- (Output.debug (fn () => "success: " ^ Display.string_of_thm ctxt ith);
+ (trace_msg (fn () => "success: " ^ Display.string_of_thm ctxt ith);
[ith])
- | _ => (Output.debug (fn () => "Metis: no result");
+ | _ => (trace_msg (fn () => "Metis: no result");
[])
end
| Metis.Resolution.Satisfiable _ =>
- (Output.debug (fn () => "Metis: No first-order proof with the lemmas supplied");
+ (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
[])
end;
fun metis_general_tac mode ctxt ths i st0 =
- let val _ = Output.debug (fn () =>
+ let val _ = trace_msg (fn () =>
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
if exists_type ResAxioms.type_has_empty_sort (prop_of st0)
--- a/src/HOL/Tools/res_atp.ML Fri Oct 16 00:26:19 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML Fri Oct 16 10:45:10 2009 +0200
@@ -237,10 +237,10 @@
let val cls = sort compare_pairs newpairs
val accepted = List.take (cls, max_new)
in
- Output.debug (fn () => ("Number of candidates, " ^ Int.toString nnew ^
+ ResAxioms.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
", exceeds the limit of " ^ Int.toString (max_new)));
- Output.debug (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
- Output.debug (fn () => "Actually passed: " ^
+ ResAxioms.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
+ ResAxioms.trace_msg (fn () => "Actually passed: " ^
space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
(map #1 accepted, map #1 (List.drop (cls, max_new)))
@@ -255,7 +255,7 @@
val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
val newp = p + (1.0-p) / convergence
in
- Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels)));
+ ResAxioms.trace_msg (fn () => ("relevant this iteration: " ^ Int.toString (length newrels)));
(map #1 newrels) @
(relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
end
@@ -263,12 +263,12 @@
let val weight = clause_weight ctab rel_consts consts_typs
in
if p <= weight orelse (follow_defs andalso defines thy clsthm rel_consts)
- then (Output.debug (fn () => (name ^ " clause " ^ Int.toString n ^
+ then (ResAxioms.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^
" passes: " ^ Real.toString weight));
relevant ((ax,weight)::newrels, rejects) axs)
else relevant (newrels, ax::rejects) axs
end
- in Output.debug (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
+ in ResAxioms.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
relevant ([],[])
end;
@@ -277,12 +277,12 @@
then
let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
val goal_const_tab = get_goal_consts_typs thy goals
- val _ = Output.debug (fn () => ("Initial constants: " ^
+ val _ = ResAxioms.trace_msg (fn () => ("Initial constants: " ^
space_implode ", " (Symtab.keys goal_const_tab)));
val rels = relevant_clauses max_new thy const_tab (pass_mark)
goal_const_tab (map (pair_consts_typs_axiom theory_const thy) axioms)
in
- Output.debug (fn () => ("Total relevant: " ^ Int.toString (length rels)));
+ ResAxioms.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
rels
end
else axioms;
@@ -346,7 +346,7 @@
fun make_unique xs =
let val ht = mk_clause_table 7000
in
- Output.debug (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
+ ResAxioms.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
app (ignore o Polyhash.peekInsert ht) xs;
Polyhash.listItems ht
end;
@@ -409,7 +409,7 @@
fun get_clasimp_atp_lemmas ctxt =
let val included_thms =
if include_all
- then (tap (fn ths => Output.debug
+ then (tap (fn ths => ResAxioms.trace_msg
(fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
(name_thm_pairs ctxt))
else
@@ -545,7 +545,7 @@
val extra_cls = chain_cls @ extra_cls
val isFO = isFO thy goal_cls
val ccls = subtract_cls goal_cls extra_cls
- val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm_global thy th)) ccls
+ val _ = app (fn th => ResAxioms.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
val ccltms = map prop_of ccls
and axtms = map (prop_of o #1) extra_cls
val subs = tfree_classes_of_terms ccltms
--- a/src/HOL/Tools/res_axioms.ML Fri Oct 16 00:26:19 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML Fri Oct 16 10:45:10 2009 +0200
@@ -5,6 +5,8 @@
signature RES_AXIOMS =
sig
+ val trace: bool Unsynchronized.ref
+ val trace_msg: (unit -> string) -> unit
val cnf_axiom: theory -> thm -> thm list
val pairname: thm -> string * thm
val multi_base_blacklist: string list
@@ -24,6 +26,9 @@
structure ResAxioms: RES_AXIOMS =
struct
+val trace = Unsynchronized.ref false;
+fun trace_msg msg = if ! trace then tracing (msg ()) else ();
+
(* FIXME legacy *)
fun freeze_thm th = #1 (Drule.freeze_thaw th);
--- a/src/HOL/Tools/res_hol_clause.ML Fri Oct 16 00:26:19 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Fri Oct 16 10:45:10 2009 +0200
@@ -459,7 +459,7 @@
fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
fun display_arity const_needs_hBOOL (c,n) =
- Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
+ ResAxioms.trace_msg (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
(if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
--- a/src/HOL/Tools/res_reconstruct.ML Fri Oct 16 00:26:19 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Fri Oct 16 10:45:10 2009 +0200
@@ -28,8 +28,9 @@
val trace_path = Path.basic "atp_trace";
-fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
- else ();
+fun trace s =
+ if ! ResAxioms.trace then File.append (File.tmp_path trace_path) s
+ else ();
fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
@@ -446,7 +447,7 @@
val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
val ccls = map forall_intr_vars ccls
val _ =
- if !Output.debugging then app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
+ if ! ResAxioms.trace then app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
else ()
val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
val _ = trace "\ndecode_tstp_file: finishing\n"