# HG changeset patch # User wenzelm # Date 1255682710 -7200 # Node ID 4a78daeb012be31ffb7c1268210df116d9f85f7e # Parent c054b03c7881061d8b211954460a687e51a8abdc local channels for tracing/debugging; diff -r c054b03c7881 -r 4a78daeb012b src/HOL/Tools/Function/fundef_core.ML --- 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 diff -r c054b03c7881 -r 4a78daeb012b src/HOL/Tools/meson.ML --- 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)) diff -r c054b03c7881 -r 4a78daeb012b src/HOL/Tools/metis_tools.ML --- 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) diff -r c054b03c7881 -r 4a78daeb012b src/HOL/Tools/res_atp.ML --- 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 diff -r c054b03c7881 -r 4a78daeb012b src/HOL/Tools/res_axioms.ML --- 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); diff -r c054b03c7881 -r 4a78daeb012b src/HOL/Tools/res_hol_clause.ML --- 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, _, _) = diff -r c054b03c7881 -r 4a78daeb012b src/HOL/Tools/res_reconstruct.ML --- 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"