src/HOL/Tools/res_atp.ML
changeset 17775 2679ba74411f
parent 17773 a7258e1020b7
child 17819 1241e5d31d5b
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Oct 07 15:08:28 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Oct 07 17:57:21 2005 +0200
     1.3 @@ -55,18 +55,18 @@
     1.4  
     1.5  (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
     1.6  fun tptp_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) =
     1.7 -    let
     1.8 -      val clss = map (ResClause.make_conjecture_clause_thm) thms
     1.9 -      val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
    1.10 -      val tfree_clss = map ResClause.tfree_clause (ResLib.flat_noDup tfree_litss)
    1.11 -      val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
    1.12 -      val arity_cls = map ResClause.tptp_arity_clause arity_clauses
    1.13 -      val out = TextIO.openOut(pf n)
    1.14 -    in
    1.15 -      writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
    1.16 -      writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls);
    1.17 -      TextIO.closeOut out
    1.18 -    end;
    1.19 +  let
    1.20 +    val clss = map (ResClause.make_conjecture_clause_thm) thms
    1.21 +    val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
    1.22 +    val tfree_clss = map ResClause.tfree_clause (foldl (op union_string) [] tfree_litss)
    1.23 +    val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
    1.24 +    val arity_cls = map ResClause.tptp_arity_clause arity_clauses
    1.25 +    val out = TextIO.openOut(pf n)
    1.26 +  in
    1.27 +    writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
    1.28 +    writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls);
    1.29 +    TextIO.closeOut out
    1.30 +  end;
    1.31  
    1.32  (* write out a subgoal in DFG format to the file "xxxx_N"*)
    1.33  fun dfg_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) = 
    1.34 @@ -165,9 +165,17 @@
    1.35  	    pf n :: writenext (n-1))
    1.36        in (writenext (length prems), clause_arr) end;
    1.37  
    1.38 -val last_watcher_pid =
    1.39 -  ref (NONE : (TextIO.instream * TextIO.outstream * 
    1.40 -               Posix.Process.pid * string list) option);
    1.41 +val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
    1.42 +                                    Posix.Process.pid * string list) option);
    1.43 +
    1.44 +fun kill_last_watcher () =
    1.45 +    (case !last_watcher_pid of 
    1.46 +         NONE => ()
    1.47 +       | SOME (_, childout, pid, files) => 
    1.48 +	  (debug ("Killing old watcher, pid = " ^ Int.toString (ResLib.intOfPid pid));
    1.49 +	   Watcher.killWatcher pid;  
    1.50 +	   ignore (map (try OS.FileSys.remove) files)))
    1.51 +     handle OS.SysErr _ => debug "Attempt to kill watcher failed";
    1.52  
    1.53  (*writes out the current clasimpset to a tptp file;
    1.54    turns off xsymbol at start of function, restoring it at end    *)
    1.55 @@ -176,13 +184,7 @@
    1.56    if Thm.no_prems th then ()
    1.57    else
    1.58      let
    1.59 -      val _ = (case !last_watcher_pid of NONE => ()
    1.60 -               | SOME (_, childout, pid, files) => 
    1.61 -                  (debug ("Killing old watcher, pid = " ^ 
    1.62 -                          Int.toString (ResLib.intOfPid pid));
    1.63 -                   Watcher.killWatcher pid;  
    1.64 -                   ignore (map (try OS.FileSys.remove) files)))
    1.65 -              handle OS.SysErr _ => debug "Attempt to kill watcher failed";
    1.66 +      val _ = kill_last_watcher()
    1.67        val (files,clause_arr) = write_problem_files prob_pathname (ctxt,th)
    1.68        val (childin, childout, pid) = Watcher.createWatcher (th, clause_arr)
    1.69      in