src/HOL/Tools/res_atp.ML
changeset 22130 0906fd95e0b5
parent 22012 adf68479ae1b
child 22193 62753ae847a2
     1.1 --- a/src/HOL/Tools/res_atp.ML	Sat Jan 20 14:09:12 2007 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Sat Jan 20 14:09:14 2007 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4  structure ResAtp =
     1.5  struct
     1.6  
     1.7 -fun timestamp s = Output.debug ("At " ^ Time.toString (Time.now()) ^ ": " ^ s);
     1.8 +fun timestamp s = Output.debug (fn () => ("At " ^ Time.toString (Time.now()) ^ ": " ^ s));
     1.9  
    1.10  (********************************************************************)
    1.11  (* some settings for both background automatic ATP calling procedure*)
    1.12 @@ -237,7 +237,7 @@
    1.13                              else fn_lg f (FOL,seen)
    1.14        in
    1.15          if is_fol_logic lg' then ()
    1.16 -        else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f);
    1.17 +        else Output.debug (fn () => ("Found a HOL term: " ^ Display.raw_string_of_term f));
    1.18          term_lg (args@tms) (lg',seen')
    1.19        end
    1.20    | term_lg _ (lg,seen) = (lg,seen)
    1.21 @@ -261,7 +261,7 @@
    1.22                              else pred_lg pred (lg,seen)
    1.23        in
    1.24          if is_fol_logic lg' then ()
    1.25 -        else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred);
    1.26 +        else Output.debug (fn () => ("Found a HOL predicate: " ^ Display.raw_string_of_term pred));
    1.27          term_lg args (lg',seen')
    1.28        end;
    1.29  
    1.30 @@ -270,7 +270,7 @@
    1.31        let val (lg,seen') = lit_lg lit (FOL,seen)
    1.32        in
    1.33          if is_fol_logic lg then ()
    1.34 -        else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit);
    1.35 +        else Output.debug (fn () => ("Found a HOL literal: " ^ Display.raw_string_of_term lit));
    1.36          lits_lg lits (lg,seen')
    1.37        end
    1.38    | lits_lg lits (lg,seen) = (lg,seen);
    1.39 @@ -288,7 +288,7 @@
    1.40      let val (lg,seen') = logic_of_clause cls (FOL,seen)
    1.41          val _ =
    1.42            if is_fol_logic lg then ()
    1.43 -          else Output.debug ("Found a HOL clause: " ^ Display.raw_string_of_term cls)
    1.44 +          else Output.debug (fn () => ("Found a HOL clause: " ^ Display.raw_string_of_term cls))
    1.45      in
    1.46          logic_of_clauses clss (lg,seen')
    1.47      end
    1.48 @@ -506,7 +506,7 @@
    1.49  fun make_unique xs =
    1.50    let val ht = mk_clause_table 7000
    1.51    in
    1.52 -      Output.debug("make_unique gets " ^ Int.toString (length xs) ^ " clauses");
    1.53 +      Output.debug (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
    1.54        app (ignore o Polyhash.peekInsert ht) xs;
    1.55        Polyhash.listItems ht
    1.56    end;
    1.57 @@ -529,7 +529,7 @@
    1.58  fun display_thms [] = ()
    1.59    | display_thms ((name,thm)::nthms) =
    1.60        let val nthm = name ^ ": " ^ (string_of_thm thm)
    1.61 -      in Output.debug nthm; display_thms nthms  end;
    1.62 +      in Output.debug (fn () => nthm); display_thms nthms  end;
    1.63  
    1.64  fun all_valid_thms ctxt =
    1.65    PureThy.thms_containing (ProofContext.theory_of ctxt) ([], []) @
    1.66 @@ -571,7 +571,7 @@
    1.67    let val included_thms =
    1.68          if !include_all
    1.69          then (tap (fn ths => Output.debug
    1.70 -                     ("Including all " ^ Int.toString (length ths) ^ " theorems"))
    1.71 +                     (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
    1.72                    (name_thm_pairs ctxt))
    1.73          else
    1.74          let val claset_thms =
    1.75 @@ -583,8 +583,8 @@
    1.76              val atpset_thms =
    1.77                  if !include_atpset then ResAxioms.atpset_rules_of ctxt
    1.78                  else []
    1.79 -            val _ = if !Output.show_debug_msgs
    1.80 -                    then (Output.debug "ATP theorems: "; display_thms atpset_thms)
    1.81 +            val _ = if !Output.debugging
    1.82 +                    then (Output.debug (fn () => "ATP theorems: "); display_thms atpset_thms)
    1.83                      else ()
    1.84          in  claset_thms @ simpset_thms @ atpset_thms  end
    1.85        val user_rules = filter check_named
    1.86 @@ -600,12 +600,11 @@
    1.87        let val banned = make_banned_test (map #1 ths)
    1.88            fun ok (a,_) = not (banned a)
    1.89            val (good,bad) = List.partition ok ths
    1.90 -      in  if !Output.show_debug_msgs then
    1.91 -             (Output.debug("blacklist filter gets " ^ Int.toString (length ths) ^ " theorems");
    1.92 -              Output.debug("filtered: " ^ space_implode ", " (map #1 bad));
    1.93 -              Output.debug("...and returns " ^ Int.toString (length good)))
    1.94 -          else ();
    1.95 -          good 
    1.96 +      in
    1.97 +        Output.debug (fn () => "blacklist filter gets " ^ Int.toString (length ths) ^ " theorems");
    1.98 +        Output.debug (fn () => "filtered: " ^ space_implode ", " (map #1 bad));
    1.99 +        Output.debug (fn () => "...and returns " ^ Int.toString (length good));
   1.100 +        good 
   1.101        end
   1.102    else ths;
   1.103  
   1.104 @@ -751,14 +750,15 @@
   1.105          and user_lemmas_names = map #1 user_rules
   1.106      in
   1.107          writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
   1.108 -        Output.debug ("Writing to " ^ file);
   1.109 +        Output.debug (fn () => "Writing to " ^ file);
   1.110          file
   1.111      end;
   1.112  
   1.113  
   1.114  (**** remove tmp files ****)
   1.115  fun cond_rm_tmp file =
   1.116 -    if !Output.show_debug_msgs orelse !destdir <> "" then Output.debug "ATP input kept..."
   1.117 +    if !Output.debugging orelse !destdir <> ""
   1.118 +    then Output.debug (fn () => "ATP input kept...")
   1.119      else OS.FileSys.remove file;
   1.120  
   1.121  
   1.122 @@ -785,7 +785,7 @@
   1.123              val probfile = prob_pathname n
   1.124              val time = Int.toString (!time_limit)
   1.125            in
   1.126 -            Output.debug ("problem file in watcher_call_provers is " ^ probfile);
   1.127 +            Output.debug (fn () => "problem file in watcher_call_provers is " ^ probfile);
   1.128              (*options are separated by Watcher.setting_sep, currently #"%"*)
   1.129              if !prover = "spass"
   1.130              then
   1.131 @@ -816,7 +816,7 @@
   1.132      val atp_list = make_atp_list sg_terms 1
   1.133    in
   1.134      Watcher.callResProvers(childout,atp_list);
   1.135 -    Output.debug "Sent commands to watcher!"
   1.136 +    Output.debug (fn () => "Sent commands to watcher!")
   1.137    end
   1.138  
   1.139  fun trace_vector fname =
   1.140 @@ -829,7 +829,7 @@
   1.141    subgoals, each involving &&.*)
   1.142  fun write_problem_files probfile (ctxt,th)  =
   1.143    let val goals = Thm.prems_of th
   1.144 -      val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
   1.145 +      val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals))
   1.146        val thy = ProofContext.theory_of ctxt
   1.147        fun get_neg_subgoals [] _ = []
   1.148          | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) :: 
   1.149 @@ -844,11 +844,11 @@
   1.150                                         |> ResAxioms.cnf_rules_pairs |> make_unique
   1.151                                         |> restrict_to_logic logic
   1.152                                         |> remove_unwanted_clauses
   1.153 -      val _ = Output.debug ("included clauses = " ^ Int.toString(length included_cls))
   1.154 +      val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
   1.155        val white_cls = ResAxioms.cnf_rules_pairs white_thms
   1.156        (*clauses relevant to goal gl*)
   1.157        val axcls_list = map (fn ngcls => get_relevant_clauses thy included_cls white_cls (map prop_of ngcls)) goal_cls
   1.158 -      val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls)))
   1.159 +      val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))
   1.160                    axcls_list
   1.161        val writer = if !prover = "spass" then dfg_writer else tptp_writer
   1.162        fun write_all [] [] _ = []
   1.163 @@ -863,12 +863,12 @@
   1.164                  and tycons = type_consts_of_terms thy (ccltms@axtms)
   1.165                  (*TFrees in conjecture clauses; TVars in axiom clauses*)
   1.166                  val classrel_clauses = ResClause.make_classrel_clauses thy subs supers
   1.167 -                val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
   1.168 +                val _ = Output.debug (fn () => "classrel clauses = " ^ Int.toString (length classrel_clauses))
   1.169                  val arity_clauses = ResClause.arity_clause_thy thy tycons supers
   1.170 -                val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
   1.171 +                val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses))
   1.172                  val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
   1.173                  val thm_names = Vector.fromList clnames
   1.174 -                val _ = if !Output.show_debug_msgs
   1.175 +                val _ = if !Output.debugging
   1.176                          then trace_vector (fname ^ "_thm_names") thm_names else ()
   1.177              in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
   1.178        val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
   1.179 @@ -883,10 +883,10 @@
   1.180      (case !last_watcher_pid of
   1.181           NONE => ()
   1.182         | SOME (_, _, pid, files) =>
   1.183 -          (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
   1.184 +          (Output.debug (fn () => "Killing old watcher, pid = " ^ string_of_pid pid);
   1.185             Watcher.killWatcher pid;
   1.186             ignore (map (try cond_rm_tmp) files)))
   1.187 -     handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed";
   1.188 +     handle OS.SysErr _ => Output.debug (fn () => "Attempt to kill watcher failed");
   1.189  
   1.190  (*writes out the current problems and calls ATPs*)
   1.191  fun isar_atp (ctxt, th) =
   1.192 @@ -898,8 +898,8 @@
   1.193        val (childin, childout, pid) = Watcher.createWatcher (ctxt, th, thm_names_list)
   1.194      in
   1.195        last_watcher_pid := SOME (childin, childout, pid, files);
   1.196 -      Output.debug ("problem files: " ^ space_implode ", " files);
   1.197 -      Output.debug ("pid: " ^ string_of_pid pid);
   1.198 +      Output.debug (fn () => "problem files: " ^ space_implode ", " files);
   1.199 +      Output.debug (fn () => "pid: " ^ string_of_pid pid);
   1.200        watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
   1.201      end;
   1.202  
   1.203 @@ -923,12 +923,12 @@
   1.204  fun invoke_atp_ml (ctxt, goal) =
   1.205    let val thy = ProofContext.theory_of ctxt;
   1.206    in
   1.207 -    Output.debug ("subgoals in isar_atp:\n" ^
   1.208 +    Output.debug (fn () => "subgoals in isar_atp:\n" ^
   1.209                    Pretty.string_of (ProofContext.pretty_term ctxt
   1.210                      (Logic.mk_conjunction_list (Thm.prems_of goal))));
   1.211 -    Output.debug ("current theory: " ^ Context.theory_name thy);
   1.212 +    Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
   1.213      inc hook_count;
   1.214 -    Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
   1.215 +    Output.debug (fn () => "in hook for time: " ^ Int.toString (!hook_count));
   1.216      ResClause.init thy;
   1.217      ResHolClause.init thy;
   1.218      if !time_limit > 0 then isar_atp (ctxt, goal)