--- 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
--- 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*)
--- 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)
--- 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)