# HG changeset patch # User wenzelm # Date 1137255253 -3600 # Node ID 677e2bdd75f00323d132fcc9b4909564d5c62cac # Parent cf9f1584431aae922133a749933d03977af943e1 Output.debug; diff -r cf9f1584431a -r 677e2bdd75f0 src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Sat Jan 14 17:14:11 2006 +0100 +++ b/src/HOL/Tools/ATP/watcher.ML Sat Jan 14 17:14:13 2006 +0100 @@ -190,7 +190,7 @@ fun number_from_filename s = case String.tokens (not o Char.isDigit) s of [] => (trace ("\nWatcher could not read subgoal nunber! " ^ s); - raise ERROR) + error "") | numbers => valOf (Int.fromString (List.last numbers)); (* call ATP. Settings should be a list of strings ["-t300", "-m100000"]*) @@ -350,16 +350,16 @@ (goals_being_watched := !goals_being_watched - 1; if !goals_being_watched = 0 then - (debug ("\nReaping a watcher, childpid = " ^ string_of_pid childpid); + (Output.debug ("\nReaping a watcher, childpid = " ^ string_of_pid childpid); killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) ) else ()) - val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of th); + val _ = Output.debug ("subgoals forked to createWatcher: "^ prems_string_of th); fun proofHandler n = let val outcome = TextIO.inputLine childin val probfile = TextIO.inputLine childin val sgno = number_from_filename probfile val text = string_of_subgoal th sgno - val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ + val _ = Output.debug ("In signal handler. outcome = \"" ^ outcome ^ "\"\nprobfile = " ^ probfile ^ "\nGoals being watched: "^ Int.toString (!goals_being_watched)) in diff -r cf9f1584431a -r 677e2bdd75f0 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Sat Jan 14 17:14:11 2006 +0100 +++ b/src/HOL/Tools/meson.ML Sat Jan 14 17:14:13 2006 +0100 @@ -142,7 +142,7 @@ fun refl_clause_aux 0 th = th | refl_clause_aux n th = -(debug ("refl_clause_aux " ^ Int.toString n ^ " " ^ string_of_thm th); +(Output.debug ("refl_clause_aux " ^ Int.toString n ^ " " ^ string_of_thm th); case HOLogic.dest_Trueprop (concl_of th) of (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) => refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*) diff -r cf9f1584431a -r 677e2bdd75f0 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Sat Jan 14 17:14:11 2006 +0100 +++ b/src/HOL/Tools/res_atp.ML Sat Jan 14 17:14:13 2006 +0100 @@ -91,7 +91,7 @@ val probfile = prob_pathname n val time = Int.toString (!time_limit) in - debug ("problem file in watcher_call_provers is " ^ probfile); + Output.debug ("problem file in watcher_call_provers is " ^ probfile); (*Avoid command arguments containing spaces: Poly/ML and SML/NJ versions of Unix.execute treat them differently!*) (*options are separated by Watcher.setting_sep, currently #"%"*) @@ -104,7 +104,7 @@ then space_implode "%" (!custom_spass) ^ "%-DocProof%-TimeLimit=" ^ time else "-DocProof%-SOS%-FullRed=0%-TimeLimit=" ^ time (*Auto mode*) - val _ = debug ("SPASS option string is " ^ optionline) + val _ = Output.debug ("SPASS option string is " ^ optionline) val _ = helper_path "SPASS_HOME" "SPASS" (*We've checked that SPASS is there for ATP/spassshell to run.*) in @@ -135,7 +135,7 @@ val atp_list = make_atp_list sg_terms 1 in Watcher.callResProvers(childout,atp_list); - debug "Sent commands to watcher!" + Output.debug "Sent commands to watcher!" end (*We write out problem files for each subgoal. Argument pf generates filenames, @@ -144,13 +144,13 @@ let val prems = Thm.prems_of th val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) (*FIXME: hack!! need to consider relevance for all prems*) - val _ = debug ("claset and simprules total clauses = " ^ + val _ = Output.debug ("claset and simprules total clauses = " ^ Int.toString (Array.length clause_arr)) val thy = ProofContext.theory_of ctxt val classrel_clauses = if !ResClause.keep_types then ResClause.classrel_clauses_thy thy else [] - val _ = debug ("classrel clauses = " ^ Int.toString (length classrel_clauses)) + val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses)) val arity_clauses = if !ResClause.keep_types then ResClause.arity_clause_thy thy else [] - val _ = debug ("arity clauses = " ^ Int.toString (length arity_clauses)) + val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses)) val write = if !prover = "spass" then dfg_inputs_tfrees else tptp_inputs_tfrees fun writenext n = if n=0 then [] @@ -171,10 +171,10 @@ (case !last_watcher_pid of NONE => () | SOME (_, childout, pid, files) => - (debug ("Killing old watcher, pid = " ^ string_of_pid pid); + (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid); Watcher.killWatcher pid; ignore (map (try OS.FileSys.remove) files))) - handle OS.SysErr _ => debug "Attempt to kill watcher failed"; + handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed"; (*writes out the current clasimpset to a tptp file; turns off xsymbol at start of function, restoring it at end *) @@ -188,8 +188,8 @@ val (childin, childout, pid) = Watcher.createWatcher (th, clause_arr) in last_watcher_pid := SOME (childin, childout, pid, files); - debug ("problem files: " ^ space_implode ", " files); - debug ("pid: " ^ string_of_pid pid); + Output.debug ("problem files: " ^ space_implode ", " files); + Output.debug ("pid: " ^ string_of_pid pid); watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid) end); @@ -207,17 +207,16 @@ val invoke_atp = Toplevel.unknown_proof o Toplevel.keep (fn state => let val proof = Toplevel.proof_of state - val (ctxt, (_, goal)) = Proof.get_goal proof - handle Proof.STATE _ => error "No goal present"; + val (ctxt, (_, goal)) = Proof.get_goal proof; val thy = ProofContext.theory_of ctxt; in - debug ("subgoals in isar_atp:\n" ^ + Output.debug ("subgoals in isar_atp:\n" ^ Pretty.string_of (ProofContext.pretty_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)))); - debug ("number of subgoals in isar_atp: " ^ Int.toString (Thm.nprems_of goal)); - debug ("current theory: " ^ Context.theory_name thy); + Output.debug ("number of subgoals in isar_atp: " ^ Int.toString (Thm.nprems_of goal)); + Output.debug ("current theory: " ^ Context.theory_name thy); hook_count := !hook_count +1; - debug ("in hook for time: " ^ Int.toString (!hook_count)); + Output.debug ("in hook for time: " ^ Int.toString (!hook_count)); ResClause.init thy; if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal) else isar_atp_writeonly (ctxt, goal) diff -r cf9f1584431a -r 677e2bdd75f0 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Sat Jan 14 17:14:11 2006 +0100 +++ b/src/HOL/Tools/res_axioms.ML Sat Jan 14 17:14:13 2006 +0100 @@ -349,7 +349,7 @@ val intros = safeIs @ hazIs val elims = map Classical.classical_rule (safeEs @ hazEs) in - debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^ + Output.debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^ " elims: " ^ Int.toString(length elims)); if tagging_enabled then map pairname (map tag_intro intros @ map tag_elim elims) @@ -360,7 +360,7 @@ let val ({rules,...}, _) = rep_ss ss val simps = Net.entries rules in - debug ("rules_of_simpset: " ^ Int.toString(length simps)); + Output.debug ("rules_of_simpset: " ^ Int.toString(length simps)); map (fn r => (#name r, #thm r)) simps end; @@ -421,10 +421,10 @@ | clausify_rules_pairs_aux result ((name,th)::ths) = clausify_rules_pairs_aux (clausify_axiom_pairs (name,th) :: result) ths handle THM (msg,_,_) => - (debug ("Cannot clausify " ^ name ^ ": " ^ msg); + (Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg); clausify_rules_pairs_aux result ths) | ResClause.CLAUSE (msg,t) => - (debug ("Cannot clausify " ^ name ^ ": " ^ msg ^ + (Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg ^ ": " ^ TermLib.string_of_term t); clausify_rules_pairs_aux result ths) @@ -433,10 +433,10 @@ | clausify_rules_pairs_auxH result ((name,th)::ths) = clausify_rules_pairs_auxH (clausify_axiom_pairsH (name,th) :: result) ths handle THM (msg,_,_) => - (debug ("Cannot clausify " ^ name ^ ": " ^ msg); + (Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg); clausify_rules_pairs_auxH result ths) | ResHolClause.LAM2COMB (t) => - (debug ("Cannot clausify " ^ TermLib.string_of_term t); + (Output.debug ("Cannot clausify " ^ TermLib.string_of_term t); clausify_rules_pairs_auxH result ths)