src/HOL/Tools/res_atp.ML
changeset 18680 677e2bdd75f0
parent 18675 333a73034023
child 18700 f04a8755d6ca
     1.1 --- a/src/HOL/Tools/res_atp.ML	Sat Jan 14 17:14:11 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Sat Jan 14 17:14:13 2006 +0100
     1.3 @@ -91,7 +91,7 @@
     1.4              val probfile = prob_pathname n
     1.5              val time = Int.toString (!time_limit)
     1.6            in
     1.7 -            debug ("problem file in watcher_call_provers is " ^ probfile);
     1.8 +            Output.debug ("problem file in watcher_call_provers is " ^ probfile);
     1.9              (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
    1.10                versions of Unix.execute treat them differently!*)
    1.11              (*options are separated by Watcher.setting_sep, currently #"%"*)
    1.12 @@ -104,7 +104,7 @@
    1.13                        then space_implode "%" (!custom_spass) ^
    1.14                             "%-DocProof%-TimeLimit=" ^ time
    1.15                        else "-DocProof%-SOS%-FullRed=0%-TimeLimit=" ^ time (*Auto mode*)
    1.16 -                  val _ = debug ("SPASS option string is " ^ optionline)
    1.17 +                  val _ = Output.debug ("SPASS option string is " ^ optionline)
    1.18                    val _ = helper_path "SPASS_HOME" "SPASS"
    1.19                      (*We've checked that SPASS is there for ATP/spassshell to run.*)
    1.20                in 
    1.21 @@ -135,7 +135,7 @@
    1.22      val atp_list = make_atp_list sg_terms 1
    1.23    in
    1.24      Watcher.callResProvers(childout,atp_list);
    1.25 -    debug "Sent commands to watcher!"
    1.26 +    Output.debug "Sent commands to watcher!"
    1.27    end
    1.28  
    1.29  (*We write out problem files for each subgoal. Argument pf generates filenames,
    1.30 @@ -144,13 +144,13 @@
    1.31    let val prems = Thm.prems_of th
    1.32        val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) 
    1.33                (*FIXME: hack!! need to consider relevance for all prems*)
    1.34 -      val _ = debug ("claset and simprules total clauses = " ^ 
    1.35 +      val _ = Output.debug ("claset and simprules total clauses = " ^ 
    1.36                       Int.toString (Array.length clause_arr))
    1.37        val thy = ProofContext.theory_of ctxt
    1.38        val classrel_clauses = if !ResClause.keep_types then ResClause.classrel_clauses_thy thy else []
    1.39 -      val _ = debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
    1.40 +      val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
    1.41        val arity_clauses = if !ResClause.keep_types then ResClause.arity_clause_thy thy else []
    1.42 -      val _ = debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    1.43 +      val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    1.44        val write = if !prover = "spass" then dfg_inputs_tfrees else tptp_inputs_tfrees
    1.45        fun writenext n =
    1.46  	if n=0 then []
    1.47 @@ -171,10 +171,10 @@
    1.48      (case !last_watcher_pid of 
    1.49           NONE => ()
    1.50         | SOME (_, childout, pid, files) => 
    1.51 -	  (debug ("Killing old watcher, pid = " ^ string_of_pid pid);
    1.52 +	  (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
    1.53  	   Watcher.killWatcher pid;  
    1.54  	   ignore (map (try OS.FileSys.remove) files)))
    1.55 -     handle OS.SysErr _ => debug "Attempt to kill watcher failed";
    1.56 +     handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed";
    1.57  
    1.58  (*writes out the current clasimpset to a tptp file;
    1.59    turns off xsymbol at start of function, restoring it at end    *)
    1.60 @@ -188,8 +188,8 @@
    1.61        val (childin, childout, pid) = Watcher.createWatcher (th, clause_arr)
    1.62      in
    1.63        last_watcher_pid := SOME (childin, childout, pid, files);
    1.64 -      debug ("problem files: " ^ space_implode ", " files); 
    1.65 -      debug ("pid: " ^ string_of_pid pid);
    1.66 +      Output.debug ("problem files: " ^ space_implode ", " files); 
    1.67 +      Output.debug ("pid: " ^ string_of_pid pid);
    1.68        watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
    1.69      end);
    1.70  
    1.71 @@ -207,17 +207,16 @@
    1.72  val invoke_atp = Toplevel.unknown_proof o Toplevel.keep (fn state =>
    1.73    let
    1.74      val proof = Toplevel.proof_of state
    1.75 -    val (ctxt, (_, goal)) = Proof.get_goal proof
    1.76 -        handle Proof.STATE _ => error "No goal present";
    1.77 +    val (ctxt, (_, goal)) = Proof.get_goal proof;
    1.78      val thy = ProofContext.theory_of ctxt;
    1.79    in
    1.80 -    debug ("subgoals in isar_atp:\n" ^ 
    1.81 +    Output.debug ("subgoals in isar_atp:\n" ^ 
    1.82             Pretty.string_of (ProofContext.pretty_term ctxt
    1.83               (Logic.mk_conjunction_list (Thm.prems_of goal))));
    1.84 -    debug ("number of subgoals in isar_atp: " ^ Int.toString (Thm.nprems_of goal));
    1.85 -    debug ("current theory: " ^ Context.theory_name thy);
    1.86 +    Output.debug ("number of subgoals in isar_atp: " ^ Int.toString (Thm.nprems_of goal));
    1.87 +    Output.debug ("current theory: " ^ Context.theory_name thy);
    1.88      hook_count := !hook_count +1;
    1.89 -    debug ("in hook for time: " ^ Int.toString (!hook_count));
    1.90 +    Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
    1.91      ResClause.init thy;
    1.92      if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal)
    1.93      else isar_atp_writeonly (ctxt, goal)