src/HOL/Tools/res_atp.ML
author mengj
Tue Mar 07 03:51:40 2006 +0100 (2006-03-07 ago)
changeset 19194 7681c04d8bff
parent 18986 5060ca625e02
child 19205 4ec788c69f82
permissions -rw-r--r--
Merged res_atp_setup.ML into res_atp.ML.
HOL translation is integrated with background Isabelle-ATP linkup.
Both ATP methods and background linkup retrieve lemmas stored in claset, simpset and atpset.
     1 (*  Author: Jia Meng, Cambridge University Computer Laboratory, NICTA
     2     ID: $Id$
     3     Copyright 2004 University of Cambridge
     4 
     5 ATPs with TPTP format input.
     6 *)
     7 
     8 signature RES_ATP =
     9 sig
    10   val prover: string ref
    11   val custom_spass: string list ref
    12   val destdir: string ref
    13   val helper_path: string -> string -> string
    14   val problem_name: string ref
    15   val time_limit: int ref
    16    
    17   datatype mode = Auto | Fol | Hol
    18   val write_subgoal_file: mode -> Proof.context -> Thm.thm list -> Thm.thm list -> int -> string
    19   val vampire_time: int ref
    20   val eprover_time: int ref
    21   val run_vampire: int -> unit
    22   val run_eprover: int -> unit
    23   val vampireLimit: unit -> int
    24   val eproverLimit: unit -> int
    25   val atp_method: (ProofContext.context -> Thm.thm list -> int -> Tactical.tactic) ->
    26 		  Method.src -> ProofContext.context -> Method.method
    27   val cond_rm_tmp: string -> unit
    28   val keep_atp_input: bool ref
    29   val fol_keep_types: bool ref
    30   val hol_full_types: unit -> unit
    31   val hol_partial_types: unit -> unit
    32   val hol_const_types_only: unit -> unit
    33   val hol_no_types: unit -> unit
    34   val hol_typ_level: unit -> ResHolClause.type_level
    35   val run_relevance_filter: bool ref
    36 
    37 end;
    38 
    39 structure ResAtp: RES_ATP =
    40 struct
    41 
    42 (********************************************************************)
    43 (* some settings for both background automatic ATP calling procedure*)
    44 (* and also explicit ATP invocation methods                         *)
    45 (********************************************************************)
    46 
    47 (*** background linkup ***)
    48 val call_atp = ref false; 
    49 val hook_count = ref 0;
    50 val time_limit = ref 30;
    51 val prover = ref "E";   (* use E as the default prover *)
    52 val custom_spass =   (*specialized options for SPASS*)
    53       ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"];
    54 val destdir = ref "";   (*Empty means write files to /tmp*)
    55 val problem_name = ref "prob";
    56 
    57 (*Return the path to a "helper" like SPASS or tptp2X, first checking that
    58   it exists.  FIXME: modify to use Path primitives and move to some central place.*)  
    59 fun helper_path evar base =
    60   case getenv evar of
    61       "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
    62     | home => 
    63         let val path = home ^ "/" ^ base
    64         in  if File.exists (File.unpack_platform_path path) then path 
    65 	    else error ("Could not find the file " ^ path)
    66 	end;  
    67 
    68 fun probfile_nosuffix _ = 
    69   if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
    70   else if File.exists (File.unpack_platform_path (!destdir))
    71   then !destdir ^ "/" ^ !problem_name
    72   else error ("No such directory: " ^ !destdir);
    73 
    74 fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
    75 
    76 
    77 (*** ATP methods ***)
    78 val vampire_time = ref 60;
    79 val eprover_time = ref 60;
    80 fun run_vampire time =  
    81     if (time >0) then vampire_time:= time
    82     else vampire_time:=60;
    83 
    84 fun run_eprover time = 
    85     if (time > 0) then eprover_time:= time
    86     else eprover_time:=60;
    87 
    88 fun vampireLimit () = !vampire_time;
    89 fun eproverLimit () = !eprover_time;
    90 
    91 val keep_atp_input = ref false;
    92 val fol_keep_types = ResClause.keep_types;
    93 val hol_full_types = ResHolClause.full_types;
    94 val hol_partial_types = ResHolClause.partial_types;
    95 val hol_const_types_only = ResHolClause.const_types_only;
    96 val hol_no_types = ResHolClause.no_types;
    97 fun hol_typ_level () = ResHolClause.find_typ_level ();
    98 fun is_typed_hol () = 
    99     let val tp_level = hol_typ_level()
   100     in
   101 	not (tp_level = ResHolClause.T_NONE)
   102     end;
   103 val include_combS = ResHolClause.include_combS;
   104 val include_min_comb = ResHolClause.include_min_comb;
   105 
   106 fun atp_input_file () =
   107     let val file = !problem_name 
   108     in
   109 	if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
   110 	else if File.exists (File.unpack_platform_path (!destdir))
   111 	then !destdir ^ "/" ^ file
   112 	else error ("No such directory: " ^ !destdir)
   113     end;
   114 
   115 val include_simpset = ref false;
   116 val include_claset = ref false; 
   117 val include_atpset = ref true;
   118 val add_simpset = (fn () => include_simpset:=true);
   119 val add_claset = (fn () => include_claset:=true);
   120 val add_clasimp = (fn () => include_simpset:=true;include_claset:=true);
   121 val add_atpset = (fn () => include_atpset:=true);
   122 val rm_simpset = (fn () => include_simpset:=false);
   123 val rm_claset = (fn () => include_claset:=false);
   124 val rm_clasimp = (fn () => include_simpset:=false;include_claset:=false);
   125 val rm_atpset = (fn () => include_atpset:=false);
   126 
   127 (*** paths for HOL helper files ***)
   128 fun full_typed_comb_inclS () =
   129     helper_path "E_HOME" "additionals/full_comb_inclS"
   130     handle _ => helper_path "VAMPIRE_HOME" "additionals/full_comb_inclS";
   131 
   132 fun full_typed_comb_noS () =
   133     helper_path "E_HOME" "additionals/full_comb_noS"
   134     handle _ => helper_path "VAMPIRE_HOME" "additionals/full_comb_noS";
   135 									      
   136 fun partial_typed_comb_inclS () =
   137     helper_path "E_HOME" "additionals/par_comb_inclS"
   138     handle _ => helper_path "VAMPIRE_HOME" "additionals/par_comb_inclS";
   139 
   140 fun partial_typed_comb_noS () =
   141     helper_path "E_HOME" "additionals/par_comb_noS"
   142     handle _ => helper_path "VAMPIRE_HOME" "additionals/par_comb_noS";
   143 
   144 fun const_typed_comb_inclS () =
   145     helper_path "E_HOME" "additionals/const_comb_inclS"
   146     handle _ => helper_path "VAMPIRE_HOME" "additionals/const_comb_inclS";
   147 
   148 fun const_typed_comb_noS () =
   149     helper_path "E_HOME" "additionals/const_comb_noS"
   150     handle _ => helper_path "VAMPIRE_HOME" "additionals/const_comb_noS";
   151 
   152 fun untyped_comb_inclS () =
   153     helper_path "E_HOME" "additionals/u_comb_inclS"
   154     handle _ => helper_path "VAMPIRE_HOME" "additionals/u_comb_inclS";
   155 
   156 fun untyped_comb_noS () =
   157     helper_path "E_HOME" "additionals/u_comb_noS"
   158     handle _ => helper_path "VAMPIRE_HOME" "additionals/u_comb_noS";
   159 
   160 fun full_typed_HOL_helper1 () =
   161     helper_path "E_HOME" "additionals/full_helper1"
   162     handle _ => helper_path "VAMPIRE_HOME" "additionals/full_helper1";
   163 
   164 fun partial_typed_HOL_helper1 () = 
   165     helper_path "E_HOME" "additionals/par_helper1"
   166     handle _ => helper_path "VAMPIRE_HOME" "additionals/par_helper1";
   167 
   168 fun const_typed_HOL_helper1 () = 
   169     helper_path "E_HOME" "additionals/const_helper1"
   170     handle _ => helper_path "VAMPIRE_HOME" "additionals/const_helper1";
   171 
   172 fun untyped_HOL_helper1 () = 
   173     helper_path "E_HOME" "additionals/u_helper1"
   174     handle _ => helper_path "VAMPIRE_HOME" "additionals/u_helper1";
   175 
   176 fun get_full_typed_helpers () =
   177     (full_typed_HOL_helper1 (), full_typed_comb_noS (), full_typed_comb_inclS ());
   178 
   179 fun get_partial_typed_helpers () =
   180     (partial_typed_HOL_helper1 (), partial_typed_comb_noS (), partial_typed_comb_inclS ());
   181 
   182 fun get_const_typed_helpers () =
   183     (const_typed_HOL_helper1 (), const_typed_comb_noS (), const_typed_comb_inclS ());
   184 
   185 fun get_untyped_helpers () =
   186     (untyped_HOL_helper1 (), untyped_comb_noS (), untyped_comb_inclS ());
   187 
   188 fun get_all_helpers () =
   189     (get_full_typed_helpers (), get_partial_typed_helpers (), get_const_typed_helpers (), get_untyped_helpers ());
   190 
   191 
   192 (**** relevance filter ****)
   193 val run_relevance_filter = ref true;
   194 
   195 (******************************************************************)
   196 (* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
   197 (******************************************************************)
   198 
   199 datatype logic = FOL | HOL | HOLC | HOLCS;
   200 
   201 fun string_of_logic FOL = "FOL"
   202   | string_of_logic HOL = "HOL"
   203   | string_of_logic HOLC = "HOLC"
   204   | string_of_logic HOLCS = "HOLCS";
   205 
   206 
   207 fun is_fol_logic FOL = true
   208   | is_fol_logic  _ = false
   209 
   210 
   211 (*HOLCS will not occur here*)
   212 fun upgrade_lg HOLC _ = HOLC
   213   | upgrade_lg HOL HOLC = HOLC
   214   | upgrade_lg HOL _ = HOL
   215   | upgrade_lg FOL lg = lg; 
   216 
   217 (* check types *)
   218 fun has_bool (Type("bool",_)) = true
   219   | has_bool (Type(_, Ts)) = exists has_bool Ts
   220   | has_bool _ = false;
   221 
   222 fun has_bool_arg tp = 
   223     let val (targs,tr) = strip_type tp
   224     in
   225 	exists has_bool targs
   226     end;
   227 
   228 fun is_fn_tp (Type("fun",_)) = true
   229   | is_fn_tp _ = false;
   230 
   231 
   232 exception FN_LG of term;
   233 
   234 fun fn_lg (t as Const(f,tp)) (lg,seen) = 
   235     if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
   236   | fn_lg (t as Free(f,tp)) (lg,seen) = 
   237     if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
   238   | fn_lg (t as Var(f,tp)) (lg,seen) =
   239     if is_fn_tp tp orelse has_bool tp then (upgrade_lg HOL lg,t ins seen)
   240     else (lg,t ins seen)
   241   | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen)
   242   | fn_lg f _ = raise FN_LG(f); 
   243 
   244 
   245 fun term_lg [] (lg,seen) = (lg,seen)
   246   | term_lg (tm::tms) (FOL,seen) =
   247     let val (f,args) = strip_comb tm
   248 	val (lg',seen') = if f mem seen then (FOL,seen) 
   249 			  else fn_lg f (FOL,seen)
   250 
   251 	 in
   252 	     term_lg (args@tms) (lg',seen')
   253     end
   254   | term_lg _ (lg,seen) = (lg,seen)
   255 
   256 exception PRED_LG of term;
   257 
   258 fun pred_lg (t as Const(P,tp)) (lg,seen)= 
   259     if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
   260   | pred_lg (t as Free(P,tp)) (lg,seen) =
   261     if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
   262   | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen)
   263   | pred_lg P _ = raise PRED_LG(P);
   264 
   265 
   266 fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
   267   | lit_lg P (lg,seen) =
   268     let val (pred,args) = strip_comb P
   269 	val (lg',seen') = if pred mem seen then (lg,seen) 
   270 			  else pred_lg pred (lg,seen)
   271     in
   272 	term_lg args (lg',seen')
   273     end;
   274 
   275 fun lits_lg [] (lg,seen) = (lg,seen)
   276   | lits_lg (lit::lits) (FOL,seen) =
   277     lits_lg lits (lit_lg lit (FOL,seen))
   278   | lits_lg lits (lg,seen) = (lg,seen);
   279 
   280 
   281 fun logic_of_clause tm (lg,seen) =
   282     let val tm' = HOLogic.dest_Trueprop tm
   283 	val disjs = HOLogic.dest_disj tm'
   284     in
   285 	lits_lg disjs (lg,seen)
   286     end;
   287 
   288 fun lits_lg [] (lg,seen) = (lg,seen)
   289   | lits_lg (lit::lits) (FOL,seen) =
   290     lits_lg lits (lit_lg lit (FOL,seen))
   291   | lits_lg lits (lg,seen) = (lg,seen);
   292 
   293 
   294 fun logic_of_clause tm (lg,seen) =
   295     let val tm' = HOLogic.dest_Trueprop tm
   296 	val disjs = HOLogic.dest_disj tm'
   297     in
   298 	lits_lg disjs (lg,seen)
   299     end;
   300 
   301 fun logic_of_clauses [] (lg,seen) = (lg,seen)
   302   | logic_of_clauses (cls::clss) (FOL,seen) =
   303     logic_of_clauses clss (logic_of_clause cls (FOL,seen))
   304   | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
   305 
   306 fun logic_of_nclauses [] (lg,seen) = (lg,seen)
   307   | logic_of_nclauses (cls::clss) (FOL,seen) =
   308     logic_of_nclauses clss (logic_of_clauses (snd cls) (FOL,seen))
   309   | logic_of_nclauses clss (lg,seen) = (lg,seen);
   310 
   311 fun problem_logic (goal_cls,rules_cls) =
   312     let val (lg1,seen1) = logic_of_clauses goal_cls (FOL,[])
   313 	val (lg2,seen2) = logic_of_nclauses rules_cls (lg1,seen1)
   314     in
   315 	lg2
   316     end;
   317 
   318 fun problem_logic_goals_aux [] (lg,seen) = lg
   319   | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = 
   320     problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
   321     
   322 fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]);
   323 
   324 
   325 (***************************************************************)
   326 (* ATP invocation methods setup                                *)
   327 (***************************************************************)
   328 
   329 
   330 (**** prover-specific format: TPTP ****)
   331 
   332 
   333 fun cnf_hyps_thms ctxt = 
   334     let val ths = ProofContext.prems_of ctxt
   335     in
   336 	ResClause.union_all (map ResAxioms.skolem_thm ths)
   337     end;
   338 
   339 
   340 (**** write to files ****)
   341 
   342 datatype mode = Auto | Fol | Hol;
   343 
   344 fun tptp_writer logic goals filename (axioms,classrels,arities) =
   345     if is_fol_logic logic then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
   346     else
   347 	ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) (get_all_helpers());
   348 
   349 
   350 fun write_subgoal_file mode ctxt conjectures user_thms n =
   351     let val conj_cls = map prop_of (make_clauses conjectures) 
   352 	val hyp_cls = map prop_of (cnf_hyps_thms ctxt)
   353 	val goal_cls = conj_cls@hyp_cls
   354 	val user_rules = map ResAxioms.pairname user_thms
   355 	val (names_arr,axclauses_as_tms) = ResClasimp.get_clasimp_atp_lemmas ctxt (goal_cls) user_rules (!include_claset,!include_simpset,!include_atpset) (!run_relevance_filter)  
   356 	val thy = ProofContext.theory_of ctxt
   357 	val prob_logic = case mode of Auto => problem_logic_goals [goal_cls]
   358 				    | Fol => FOL
   359 				    | Hol => HOL
   360 	val keep_types = if is_fol_logic prob_logic then !fol_keep_types else is_typed_hol ()
   361 	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
   362 	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
   363 	val writer = tptp_writer
   364 	val file = atp_input_file()
   365     in
   366 	(writer prob_logic goal_cls file (axclauses_as_tms,classrel_clauses,arity_clauses);
   367 	 warning ("Writing to " ^ file);
   368 	 file)
   369     end;
   370 
   371 
   372 (**** remove tmp files ****)
   373 fun cond_rm_tmp file = 
   374     if !keep_atp_input then warning "ATP input kept..." 
   375     else if !destdir <> "" then warning ("ATP input kept in directory " ^ (!destdir))
   376     else (warning "deleting ATP inputs..."; OS.FileSys.remove file);
   377 
   378 
   379 (****** setup ATPs as Isabelle methods ******)
   380 fun atp_meth' tac ths ctxt = 
   381     Method.SIMPLE_METHOD' HEADGOAL
   382     (tac ctxt ths);
   383 
   384 fun atp_meth tac ths ctxt = 
   385     let val thy = ProofContext.theory_of ctxt
   386 	val _ = ResClause.init thy
   387 	val _ = ResHolClause.init thy
   388     in
   389 	atp_meth' tac ths ctxt
   390     end;
   391 
   392 fun atp_method tac = Method.thms_ctxt_args (atp_meth tac);
   393 
   394 (***************************************************************)
   395 (* automatic ATP invocation                                    *)
   396 (***************************************************************)
   397 
   398 (* call prover with settings and problem file for the current subgoal *)
   399 fun watcher_call_provers sign sg_terms (childin, childout, pid) =
   400   let
   401     fun make_atp_list [] n = []
   402       | make_atp_list (sg_term::xs) n =
   403           let
   404             val probfile = prob_pathname n
   405             val time = Int.toString (!time_limit)
   406           in
   407             Output.debug ("problem file in watcher_call_provers is " ^ probfile);
   408             (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
   409               versions of Unix.execute treat them differently!*)
   410             (*options are separated by Watcher.setting_sep, currently #"%"*)
   411             if !prover = "spass"
   412             then
   413               let val baseopts = "%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
   414               val infopts = 
   415 		      if !AtpCommunication.reconstruct 
   416 		          (*Proof reconstruction needs a limited set of inf rules*)
   417                       then space_implode "%" (!custom_spass)                           
   418                       else "-Auto%-SOS=1"
   419                   val spass = helper_path "SPASS_HOME" "SPASS"
   420             in 
   421                 ([("spass", spass, infopts ^ baseopts, probfile)] @ 
   422                   make_atp_list xs (n+1))
   423               end
   424             else if !prover = "vampire"
   425 	    then 
   426               let val vampire = helper_path "VAMPIRE_HOME" "vampire"
   427               in
   428                 ([("vampire", vampire, "-m 100000%-t " ^ time, probfile)] @
   429                  make_atp_list xs (n+1))       (*BEWARE! spaces in options!*)
   430               end
   431       	     else if !prover = "E"
   432       	     then
   433 	       let val Eprover = helper_path "E_HOME" "eproof"
   434 	       in
   435 		  ([("E", Eprover, 
   436 		     "--tptp-in%-l5%-xAuto%-tAuto%--cpu-limit=" ^ time,
   437 		     probfile)] @
   438 		   make_atp_list xs (n+1))
   439 	       end
   440 	     else error ("Invalid prover name: " ^ !prover)
   441           end
   442 
   443     val atp_list = make_atp_list sg_terms 1
   444   in
   445     Watcher.callResProvers(childout,atp_list);
   446     Output.debug "Sent commands to watcher!"
   447   end
   448 
   449 (*We write out problem files for each subgoal. Argument pf generates filenames,
   450   and allows the suppression of the suffix "_1" in problem-generation mode.
   451   FIXME: does not cope with &&, and it isn't easy because one could have multiple
   452   subgoals, each involving &&.*)
   453 fun write_problem_files pf (ctxt,th)  =
   454   let val goals = Thm.prems_of th
   455       val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
   456       val (names_arr, axclauses_as_terms) = ResClasimp.get_clasimp_atp_lemmas ctxt goals [] (true,true,true) (!run_relevance_filter) (* no user supplied rules here, because no user invocation *)
   457       val _ = Output.debug ("claset, simprules and atprules total clauses = " ^ 
   458                      Int.toString (Array.length names_arr))
   459       val thy = ProofContext.theory_of ctxt
   460       fun get_neg_subgoals n =
   461 	  if n=0 then []
   462 	  else
   463 	      let val st = Seq.hd (EVERY'
   464 				       [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac] n th)
   465 		  val negs = Option.valOf (metahyps_thms n st)
   466 		  val negs_clauses = map prop_of (make_clauses negs)
   467 	      in
   468 		  negs_clauses::(get_neg_subgoals (n - 1))
   469 	      end
   470       val neg_subgoals = get_neg_subgoals (length goals) 
   471       val goals_logic = problem_logic_goals neg_subgoals
   472       val keep_types = if is_fol_logic goals_logic then !ResClause.keep_types else is_typed_hol ()
   473       val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
   474       val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
   475       val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
   476       val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
   477       val writer = (*if !prover ~= "spass" then *)tptp_writer 
   478       fun write_all [] _ = []
   479 	| write_all (subgoal::subgoals) k =
   480 	  (writer goals_logic subgoal (pf k) (axclauses_as_terms,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1))
   481   in
   482       (write_all neg_subgoals (length goals), names_arr)
   483   end;
   484 
   485 val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
   486                                     Posix.Process.pid * string list) option);
   487 
   488 fun kill_last_watcher () =
   489     (case !last_watcher_pid of 
   490          NONE => ()
   491        | SOME (_, childout, pid, files) => 
   492 	  (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
   493 	   Watcher.killWatcher pid;  
   494 	   ignore (map (try OS.FileSys.remove) files)))
   495      handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed";
   496 
   497 (*writes out the current clasimpset to a tptp file;
   498   turns off xsymbol at start of function, restoring it at end    *)
   499 val isar_atp = setmp print_mode [] 
   500  (fn (ctxt, th) =>
   501   if Thm.no_prems th then ()
   502   else
   503     let
   504       val _ = kill_last_watcher()
   505       val (files,names_arr) = write_problem_files prob_pathname (ctxt,th)
   506       val (childin, childout, pid) = Watcher.createWatcher (th, names_arr)
   507     in
   508       last_watcher_pid := SOME (childin, childout, pid, files);
   509       Output.debug ("problem files: " ^ space_implode ", " files); 
   510       Output.debug ("pid: " ^ string_of_pid pid);
   511       watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
   512     end);
   513 
   514 val isar_atp_writeonly = setmp print_mode [] 
   515       (fn (ctxt,th) =>
   516        if Thm.no_prems th then ()
   517        else 
   518          let val pf = if Thm.nprems_of th = 1 then probfile_nosuffix 
   519          	      else prob_pathname
   520          in ignore (write_problem_files pf (ctxt,th)) end);
   521 
   522 
   523 (** the Isar toplevel hook **)
   524 
   525 val invoke_atp = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   526   let
   527     val proof = Toplevel.proof_of state
   528     val (ctxt, (_, goal)) = Proof.get_goal proof;
   529     val thy = ProofContext.theory_of ctxt;
   530   in
   531     Output.debug ("subgoals in isar_atp:\n" ^ 
   532            Pretty.string_of (ProofContext.pretty_term ctxt
   533              (Logic.mk_conjunction_list (Thm.prems_of goal))));
   534     Output.debug ("current theory: " ^ Context.theory_name thy);
   535     hook_count := !hook_count +1;
   536     Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
   537     ResClause.init thy;
   538     ResHolClause.init thy;
   539     if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal)
   540     else isar_atp_writeonly (ctxt, goal)
   541   end);
   542 
   543 val call_atpP =
   544   OuterSyntax.command 
   545     "ProofGeneral.call_atp" 
   546     "call automatic theorem provers" 
   547     OuterKeyword.diag
   548     (Scan.succeed (Toplevel.no_timing o invoke_atp));
   549 
   550 val _ = OuterSyntax.add_parsers [call_atpP];
   551 
   552 end;