local channels for tracing/debugging;
authorwenzelm
Fri Oct 16 10:45:10 2009 +0200 (2009-10-16)
changeset 329554a78daeb012b
parent 32954 c054b03c7881
child 32956 c39860141415
local channels for tracing/debugging;
src/HOL/Tools/Function/fundef_core.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_hol_clause.ML
src/HOL/Tools/res_reconstruct.ML
     1.1 --- a/src/HOL/Tools/Function/fundef_core.ML	Fri Oct 16 00:26:19 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/fundef_core.ML	Fri Oct 16 10:45:10 2009 +0200
     1.3 @@ -7,6 +7,8 @@
     1.4  
     1.5  signature FUNDEF_CORE =
     1.6  sig
     1.7 +    val trace: bool Unsynchronized.ref
     1.8 +
     1.9      val prepare_fundef : FundefCommon.fundef_config
    1.10                           -> string (* defname *)
    1.11                           -> ((bstring * typ) * mixfix) list (* defined symbol *)
    1.12 @@ -23,6 +25,9 @@
    1.13  structure FundefCore : FUNDEF_CORE =
    1.14  struct
    1.15  
    1.16 +val trace = Unsynchronized.ref false;
    1.17 +fun trace_msg msg = if ! trace then tracing (msg ()) else ();
    1.18 +
    1.19  val boolT = HOLogic.boolT
    1.20  val mk_eq = HOLogic.mk_eq
    1.21  
    1.22 @@ -420,14 +425,14 @@
    1.23          val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
    1.24                          |> instantiate' [] [NONE, SOME (cterm_of thy h)]
    1.25  
    1.26 -        val _ = Output.debug (K "Proving Replacement lemmas...")
    1.27 +        val _ = trace_msg (K "Proving Replacement lemmas...")
    1.28          val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
    1.29  
    1.30 -        val _ = Output.debug (K "Proving cases for unique existence...")
    1.31 +        val _ = trace_msg (K "Proving cases for unique existence...")
    1.32          val (ex1s, values) =
    1.33              split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
    1.34  
    1.35 -        val _ = Output.debug (K "Proving: Graph is a function")
    1.36 +        val _ = trace_msg (K "Proving: Graph is a function")
    1.37          val graph_is_function = complete
    1.38                                    |> Thm.forall_elim_vars 0
    1.39                                    |> fold (curry op COMP) ex1s
     2.1 --- a/src/HOL/Tools/meson.ML	Fri Oct 16 00:26:19 2009 +0200
     2.2 +++ b/src/HOL/Tools/meson.ML	Fri Oct 16 10:45:10 2009 +0200
     2.3 @@ -7,6 +7,7 @@
     2.4  
     2.5  signature MESON =
     2.6  sig
     2.7 +  val trace: bool Unsynchronized.ref
     2.8    val term_pair_of: indexname * (typ * 'a) -> term * 'a
     2.9    val first_order_resolve: thm -> thm -> thm
    2.10    val flexflex_first_order: thm -> thm
    2.11 @@ -42,6 +43,9 @@
    2.12  structure Meson: MESON =
    2.13  struct
    2.14  
    2.15 +val trace = Unsynchronized.ref false;
    2.16 +fun trace_msg msg = if ! trace then tracing (msg ()) else ();
    2.17 +
    2.18  val max_clauses_default = 60;
    2.19  val (max_clauses, setup) = Attrib.config_int "max_clauses" max_clauses_default;
    2.20  
    2.21 @@ -344,7 +348,7 @@
    2.22        and cnf_nil th = cnf_aux (th,[])
    2.23        val cls = 
    2.24  	    if too_many_clauses (SOME ctxt) (concl_of th)
    2.25 -	    then (warning ("cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
    2.26 +	    then (trace_msg (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
    2.27  	    else cnf_aux (th,ths)
    2.28    in  (cls, !ctxtr)  end;
    2.29  
    2.30 @@ -547,7 +551,7 @@
    2.31    | skolemize_nnf_list ctxt (th::ths) =
    2.32        skolemize ctxt th :: skolemize_nnf_list ctxt ths
    2.33        handle THM _ => (*RS can fail if Unify.search_bound is too small*)
    2.34 -       (warning ("Failed to Skolemize " ^ Display.string_of_thm ctxt th);
    2.35 +       (trace_msg (fn () => "Failed to Skolemize " ^ Display.string_of_thm ctxt th);
    2.36          skolemize_nnf_list ctxt ths);
    2.37  
    2.38  fun add_clauses (th,cls) =
    2.39 @@ -636,7 +640,7 @@
    2.40      | goes =>
    2.41          let
    2.42            val horns = make_horns (cls @ ths)
    2.43 -          val _ = Output.debug (fn () =>
    2.44 +          val _ = trace_msg (fn () =>
    2.45              cat_lines ("meson method called:" ::
    2.46                map (Display.string_of_thm ctxt) (cls @ ths) @
    2.47                ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
     3.1 --- a/src/HOL/Tools/metis_tools.ML	Fri Oct 16 00:26:19 2009 +0200
     3.2 +++ b/src/HOL/Tools/metis_tools.ML	Fri Oct 16 10:45:10 2009 +0200
     3.3 @@ -7,6 +7,7 @@
     3.4  
     3.5  signature METIS_TOOLS =
     3.6  sig
     3.7 +  val trace: bool Unsynchronized.ref
     3.8    val type_lits: bool Config.T
     3.9    val metis_tac: Proof.context -> thm list -> int -> tactic
    3.10    val metisF_tac: Proof.context -> thm list -> int -> tactic
    3.11 @@ -17,6 +18,9 @@
    3.12  structure MetisTools: METIS_TOOLS =
    3.13  struct
    3.14  
    3.15 +  val trace = Unsynchronized.ref false;
    3.16 +  fun trace_msg msg = if ! trace then tracing (msg ()) else ();
    3.17 +
    3.18    structure Recon = ResReconstruct;
    3.19  
    3.20    val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true;
    3.21 @@ -221,7 +225,7 @@
    3.22    (*Maps metis terms to isabelle terms*)
    3.23    fun fol_term_to_hol_RAW ctxt fol_tm =
    3.24      let val thy = ProofContext.theory_of ctxt
    3.25 -        val _ = Output.debug (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
    3.26 +        val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
    3.27          fun tm_to_tt (Metis.Term.Var v) =
    3.28                 (case Recon.strip_prefix ResClause.tvar_prefix v of
    3.29                      SOME w => Type (Recon.make_tvar w)
    3.30 @@ -276,7 +280,7 @@
    3.31  
    3.32    (*Maps fully-typed metis terms to isabelle terms*)
    3.33    fun fol_term_to_hol_FT ctxt fol_tm =
    3.34 -    let val _ = Output.debug (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
    3.35 +    let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
    3.36          fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, ty])) =
    3.37                 (case Recon.strip_prefix ResClause.schematic_var_prefix v of
    3.38                      SOME w =>  mk_var(w, dummyT)
    3.39 @@ -303,8 +307,8 @@
    3.40                  | NONE => (*Not a constant. Is it a fixed variable??*)
    3.41                case Recon.strip_prefix ResClause.fixed_var_prefix x of
    3.42                    SOME v => Free (v, dummyT)
    3.43 -                | NONE =>  (Output.debug (fn () => "fol_term_to_hol_FT bad const: " ^ x); fol_term_to_hol_RAW ctxt t))
    3.44 -          | cvt t = (Output.debug (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t); fol_term_to_hol_RAW ctxt t)
    3.45 +                | NONE =>  (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x); fol_term_to_hol_RAW ctxt t))
    3.46 +          | cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t); fol_term_to_hol_RAW ctxt t)
    3.47      in  cvt fol_tm   end;
    3.48  
    3.49    fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt
    3.50 @@ -313,10 +317,10 @@
    3.51  
    3.52    fun fol_terms_to_hol ctxt mode fol_tms =
    3.53      let val ts = map (fol_term_to_hol ctxt mode) fol_tms
    3.54 -        val _ = Output.debug (fn () => "  calling type inference:")
    3.55 -        val _ = app (fn t => Output.debug (fn () => Syntax.string_of_term ctxt t)) ts
    3.56 +        val _ = trace_msg (fn () => "  calling type inference:")
    3.57 +        val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
    3.58          val ts' = infer_types ctxt ts;
    3.59 -        val _ = app (fn t => Output.debug
    3.60 +        val _ = app (fn t => trace_msg
    3.61                        (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
    3.62                                  "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
    3.63                      ts'
    3.64 @@ -333,9 +337,9 @@
    3.65  
    3.66    (*for debugging only*)
    3.67    fun print_thpair (fth,th) =
    3.68 -    (Output.debug (fn () => "=============================================");
    3.69 -     Output.debug (fn () => "Metis: " ^ Metis.Thm.toString fth);
    3.70 -     Output.debug (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
    3.71 +    (trace_msg (fn () => "=============================================");
    3.72 +     trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth);
    3.73 +     trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
    3.74  
    3.75    fun lookth thpairs (fth : Metis.Thm.thm) =
    3.76      valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
    3.77 @@ -374,7 +378,7 @@
    3.78                    val t = fol_term_to_hol ctxt mode y (*we call infer_types below*)
    3.79                in  SOME (cterm_of thy (Var v), t)  end
    3.80                handle Option =>
    3.81 -                  (Output.debug (fn() => "List.find failed for the variable " ^ x ^
    3.82 +                  (trace_msg (fn() => "List.find failed for the variable " ^ x ^
    3.83                                           " in " ^ Display.string_of_thm ctxt i_th);
    3.84                     NONE)
    3.85          fun remove_typeinst (a, t) =
    3.86 @@ -383,13 +387,13 @@
    3.87                  | NONE   => case Recon.strip_prefix ResClause.tvar_prefix a of
    3.88                    SOME _ => NONE          (*type instantiations are forbidden!*)
    3.89                  | NONE   => SOME (a,t)    (*internal Metis var?*)
    3.90 -        val _ = Output.debug (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
    3.91 +        val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
    3.92          val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
    3.93          val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
    3.94          val tms = infer_types ctxt rawtms;
    3.95          val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
    3.96          val substs' = ListPair.zip (vars, map ctm_of tms)
    3.97 -        val _ = Output.debug (fn () =>
    3.98 +        val _ = trace_msg (fn () =>
    3.99            cat_lines ("subst_translations:" ::
   3.100              (substs' |> map (fn (x, y) =>
   3.101                Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
   3.102 @@ -416,23 +420,23 @@
   3.103      let
   3.104        val thy = ProofContext.theory_of ctxt
   3.105        val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   3.106 -      val _ = Output.debug (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   3.107 -      val _ = Output.debug (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   3.108 +      val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   3.109 +      val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   3.110      in
   3.111        if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
   3.112        else if is_TrueI i_th2 then i_th1
   3.113        else
   3.114          let
   3.115            val i_atm = singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm)
   3.116 -          val _ = Output.debug (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   3.117 +          val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   3.118            val prems_th1 = prems_of i_th1
   3.119            val prems_th2 = prems_of i_th2
   3.120            val index_th1 = get_index (mk_not i_atm) prems_th1
   3.121                  handle Empty => error "Failed to find literal in th1"
   3.122 -          val _ = Output.debug (fn () => "  index_th1: " ^ Int.toString index_th1)
   3.123 +          val _ = trace_msg (fn () => "  index_th1: " ^ Int.toString index_th1)
   3.124            val index_th2 = get_index i_atm prems_th2
   3.125                  handle Empty => error "Failed to find literal in th2"
   3.126 -          val _ = Output.debug (fn () => "  index_th2: " ^ Int.toString index_th2)
   3.127 +          val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
   3.128        in  resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2)  end
   3.129      end;
   3.130  
   3.131 @@ -443,7 +447,7 @@
   3.132    fun refl_inf ctxt mode t =
   3.133      let val thy = ProofContext.theory_of ctxt
   3.134          val i_t = singleton (fol_terms_to_hol ctxt mode) t
   3.135 -        val _ = Output.debug (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   3.136 +        val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   3.137          val c_t = cterm_incr_types thy refl_idx i_t
   3.138      in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
   3.139  
   3.140 @@ -456,7 +460,7 @@
   3.141      let val thy = ProofContext.theory_of ctxt
   3.142          val m_tm = Metis.Term.Fn atm
   3.143          val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr]
   3.144 -        val _ = Output.debug (fn () => "sign of the literal: " ^ Bool.toString pos)
   3.145 +        val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
   3.146          fun replace_item_list lx 0 (l::ls) = lx::ls
   3.147            | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   3.148          fun path_finder_FO tm [] = (tm, Term.Bound 0)
   3.149 @@ -467,7 +471,7 @@
   3.150                    val tm_p = List.nth(args,p')
   3.151                      handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^
   3.152                        Int.toString adjustment  ^ " term " ^  Syntax.string_of_term ctxt tm)
   3.153 -                  val _ = Output.debug (fn () => "path_finder: " ^ Int.toString p ^
   3.154 +                  val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
   3.155                                          "  " ^ Syntax.string_of_term ctxt tm_p)
   3.156  		  val (r,t) = path_finder_FO tm_p ps
   3.157                in
   3.158 @@ -512,12 +516,12 @@
   3.159            | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
   3.160          val (tm_subst, body) = path_finder_lit i_atm fp
   3.161          val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
   3.162 -        val _ = Output.debug (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   3.163 -        val _ = Output.debug (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   3.164 -        val _ = Output.debug (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   3.165 +        val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   3.166 +        val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   3.167 +        val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   3.168          val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
   3.169          val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   3.170 -        val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   3.171 +        val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   3.172          val eq_terms = map (pairself (cterm_of thy))
   3.173                             (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   3.174      in  cterm_instantiate eq_terms subst'  end;
   3.175 @@ -541,12 +545,12 @@
   3.176  
   3.177    fun translate mode _    thpairs [] = thpairs
   3.178      | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
   3.179 -        let val _ = Output.debug (fn () => "=============================================")
   3.180 -            val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
   3.181 -            val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
   3.182 +        let val _ = trace_msg (fn () => "=============================================")
   3.183 +            val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
   3.184 +            val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
   3.185              val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf))
   3.186 -            val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   3.187 -            val _ = Output.debug (fn () => "=============================================")
   3.188 +            val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   3.189 +            val _ = trace_msg (fn () => "=============================================")
   3.190              val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
   3.191          in
   3.192              if nprems_of th = n_metis_lits then ()
   3.193 @@ -665,52 +669,52 @@
   3.194      let val thy = ProofContext.theory_of ctxt
   3.195          val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
   3.196          val ths = maps #2 th_cls_pairs
   3.197 -        val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   3.198 -        val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) cls
   3.199 -        val _ = Output.debug (fn () => "THEOREM CLAUSES")
   3.200 -        val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) ths
   3.201 +        val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   3.202 +        val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
   3.203 +        val _ = trace_msg (fn () => "THEOREM CLAUSES")
   3.204 +        val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
   3.205          val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
   3.206          val _ = if null tfrees then ()
   3.207 -                else (Output.debug (fn () => "TFREE CLAUSES");
   3.208 -                      app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)
   3.209 -        val _ = Output.debug (fn () => "CLAUSES GIVEN TO METIS")
   3.210 +                else (trace_msg (fn () => "TFREE CLAUSES");
   3.211 +                      app (fn tf => trace_msg (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)
   3.212 +        val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
   3.213          val thms = map #1 axioms
   3.214 -        val _ = app (fn th => Output.debug (fn () => Metis.Thm.toString th)) thms
   3.215 -        val _ = Output.debug (fn () => "mode = " ^ string_of_mode mode)
   3.216 -        val _ = Output.debug (fn () => "START METIS PROVE PROCESS")
   3.217 +        val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
   3.218 +        val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
   3.219 +        val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
   3.220      in
   3.221          case List.filter (is_false o prop_of) cls of
   3.222              false_th::_ => [false_th RS @{thm FalseE}]
   3.223            | [] =>
   3.224          case refute thms of
   3.225              Metis.Resolution.Contradiction mth =>
   3.226 -              let val _ = Output.debug (fn () => "METIS RECONSTRUCTION START: " ^
   3.227 +              let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
   3.228                              Metis.Thm.toString mth)
   3.229                    val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
   3.230                                 (*add constraints arising from converting goal to clause form*)
   3.231                    val proof = Metis.Proof.proof mth
   3.232                    val result = translate mode ctxt' axioms proof
   3.233                    and used = map_filter (used_axioms axioms) proof
   3.234 -                  val _ = Output.debug (fn () => "METIS COMPLETED...clauses actually used:")
   3.235 -	          val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) used
   3.236 +                  val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
   3.237 +	          val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
   3.238  	          val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
   3.239                in
   3.240                    if null unused then ()
   3.241                    else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
   3.242                    case result of
   3.243                        (_,ith)::_ => 
   3.244 -                          (Output.debug (fn () => "success: " ^ Display.string_of_thm ctxt ith); 
   3.245 +                          (trace_msg (fn () => "success: " ^ Display.string_of_thm ctxt ith); 
   3.246                             [ith])
   3.247 -                    | _ => (Output.debug (fn () => "Metis: no result"); 
   3.248 +                    | _ => (trace_msg (fn () => "Metis: no result"); 
   3.249                              [])
   3.250                end
   3.251            | Metis.Resolution.Satisfiable _ => 
   3.252 -	      (Output.debug (fn () => "Metis: No first-order proof with the lemmas supplied"); 
   3.253 +	      (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied"); 
   3.254  	       [])
   3.255      end;
   3.256  
   3.257    fun metis_general_tac mode ctxt ths i st0 =
   3.258 -    let val _ = Output.debug (fn () =>
   3.259 +    let val _ = trace_msg (fn () =>
   3.260            "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   3.261      in
   3.262         if exists_type ResAxioms.type_has_empty_sort (prop_of st0)  
     4.1 --- a/src/HOL/Tools/res_atp.ML	Fri Oct 16 00:26:19 2009 +0200
     4.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Oct 16 10:45:10 2009 +0200
     4.3 @@ -237,10 +237,10 @@
     4.4        let val cls = sort compare_pairs newpairs
     4.5            val accepted = List.take (cls, max_new)
     4.6        in
     4.7 -        Output.debug (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
     4.8 +        ResAxioms.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
     4.9  		       ", exceeds the limit of " ^ Int.toString (max_new)));
    4.10 -        Output.debug (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
    4.11 -        Output.debug (fn () => "Actually passed: " ^
    4.12 +        ResAxioms.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
    4.13 +        ResAxioms.trace_msg (fn () => "Actually passed: " ^
    4.14            space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
    4.15  
    4.16  	(map #1 accepted, map #1 (List.drop (cls, max_new)))
    4.17 @@ -255,7 +255,7 @@
    4.18  		val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
    4.19  		val newp = p + (1.0-p) / convergence
    4.20  	    in
    4.21 -              Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels)));
    4.22 +              ResAxioms.trace_msg (fn () => ("relevant this iteration: " ^ Int.toString (length newrels)));
    4.23  	       (map #1 newrels) @ 
    4.24  	       (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
    4.25  	    end
    4.26 @@ -263,12 +263,12 @@
    4.27  	    let val weight = clause_weight ctab rel_consts consts_typs
    4.28  	    in
    4.29  	      if p <= weight orelse (follow_defs andalso defines thy clsthm rel_consts)
    4.30 -	      then (Output.debug (fn () => (name ^ " clause " ^ Int.toString n ^ 
    4.31 +	      then (ResAxioms.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ 
    4.32  	                                    " passes: " ^ Real.toString weight));
    4.33  	            relevant ((ax,weight)::newrels, rejects) axs)
    4.34  	      else relevant (newrels, ax::rejects) axs
    4.35  	    end
    4.36 -    in  Output.debug (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
    4.37 +    in  ResAxioms.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
    4.38          relevant ([],[]) 
    4.39      end;
    4.40  	
    4.41 @@ -277,12 +277,12 @@
    4.42   then
    4.43    let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
    4.44        val goal_const_tab = get_goal_consts_typs thy goals
    4.45 -      val _ = Output.debug (fn () => ("Initial constants: " ^
    4.46 +      val _ = ResAxioms.trace_msg (fn () => ("Initial constants: " ^
    4.47                                   space_implode ", " (Symtab.keys goal_const_tab)));
    4.48        val rels = relevant_clauses max_new thy const_tab (pass_mark) 
    4.49                     goal_const_tab  (map (pair_consts_typs_axiom theory_const thy) axioms)
    4.50    in
    4.51 -      Output.debug (fn () => ("Total relevant: " ^ Int.toString (length rels)));
    4.52 +      ResAxioms.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
    4.53        rels
    4.54    end
    4.55   else axioms;
    4.56 @@ -346,7 +346,7 @@
    4.57  fun make_unique xs =
    4.58    let val ht = mk_clause_table 7000
    4.59    in
    4.60 -      Output.debug (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
    4.61 +      ResAxioms.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
    4.62        app (ignore o Polyhash.peekInsert ht) xs;
    4.63        Polyhash.listItems ht
    4.64    end;
    4.65 @@ -409,7 +409,7 @@
    4.66  fun get_clasimp_atp_lemmas ctxt =
    4.67    let val included_thms =
    4.68      if include_all
    4.69 -    then (tap (fn ths => Output.debug
    4.70 +    then (tap (fn ths => ResAxioms.trace_msg
    4.71                   (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
    4.72                (name_thm_pairs ctxt))
    4.73      else
    4.74 @@ -545,7 +545,7 @@
    4.75      val extra_cls = chain_cls @ extra_cls
    4.76      val isFO = isFO thy goal_cls
    4.77      val ccls = subtract_cls goal_cls extra_cls
    4.78 -    val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm_global thy th)) ccls
    4.79 +    val _ = app (fn th => ResAxioms.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
    4.80      val ccltms = map prop_of ccls
    4.81      and axtms = map (prop_of o #1) extra_cls
    4.82      val subs = tfree_classes_of_terms ccltms
     5.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Oct 16 00:26:19 2009 +0200
     5.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Oct 16 10:45:10 2009 +0200
     5.3 @@ -5,6 +5,8 @@
     5.4  
     5.5  signature RES_AXIOMS =
     5.6  sig
     5.7 +  val trace: bool Unsynchronized.ref
     5.8 +  val trace_msg: (unit -> string) -> unit
     5.9    val cnf_axiom: theory -> thm -> thm list
    5.10    val pairname: thm -> string * thm
    5.11    val multi_base_blacklist: string list
    5.12 @@ -24,6 +26,9 @@
    5.13  structure ResAxioms: RES_AXIOMS =
    5.14  struct
    5.15  
    5.16 +val trace = Unsynchronized.ref false;
    5.17 +fun trace_msg msg = if ! trace then tracing (msg ()) else ();
    5.18 +
    5.19  (* FIXME legacy *)
    5.20  fun freeze_thm th = #1 (Drule.freeze_thaw th);
    5.21  
     6.1 --- a/src/HOL/Tools/res_hol_clause.ML	Fri Oct 16 00:26:19 2009 +0200
     6.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Fri Oct 16 10:45:10 2009 +0200
     6.3 @@ -459,7 +459,7 @@
     6.4    fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
     6.5  
     6.6  fun display_arity const_needs_hBOOL (c,n) =
     6.7 -  Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
     6.8 +  ResAxioms.trace_msg (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
     6.9                  (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
    6.10  
    6.11  fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
     7.1 --- a/src/HOL/Tools/res_reconstruct.ML	Fri Oct 16 00:26:19 2009 +0200
     7.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Fri Oct 16 10:45:10 2009 +0200
     7.3 @@ -28,8 +28,9 @@
     7.4  
     7.5  val trace_path = Path.basic "atp_trace";
     7.6  
     7.7 -fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
     7.8 -              else ();
     7.9 +fun trace s =
    7.10 +  if ! ResAxioms.trace then File.append (File.tmp_path trace_path) s
    7.11 +  else ();
    7.12  
    7.13  fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
    7.14  
    7.15 @@ -446,7 +447,7 @@
    7.16        val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
    7.17        val ccls = map forall_intr_vars ccls
    7.18        val _ =
    7.19 -        if !Output.debugging then app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
    7.20 +        if ! ResAxioms.trace then app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
    7.21          else ()
    7.22        val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
    7.23        val _ = trace "\ndecode_tstp_file: finishing\n"