Fixed some problems with the signal handler.
--- a/src/HOL/Tools/ATP/SpassCommunication.ML Mon Jul 11 14:52:55 2005 +0200
+++ b/src/HOL/Tools/ATP/SpassCommunication.ML Mon Jul 11 16:42:42 2005 +0200
@@ -283,6 +283,19 @@
(reconstr, thmstring, goalstring)
end
)
+ else if ((substring (thisLine, 0,1)) = "%")
+ then
+ (
+ let val reconstr = thisLine
+ val thmstring = TextIO.inputLine instr
+ val goalstring = TextIO.inputLine instr
+ val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_getSpass")));
+ val _ = TextIO.output (outfile, (thisLine))
+ val _ = TextIO.closeOut outfile
+ in
+ (reconstr, thmstring, goalstring)
+ end
+ )
else
getSpassInput instr
--- a/src/HOL/Tools/ATP/watcher.ML Mon Jul 11 14:52:55 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Mon Jul 11 16:42:42 2005 +0200
@@ -266,6 +266,7 @@
val tptp2X = ResLib.helper_path "TPTP2X_HOME" "tptp2X"
+
(*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
val probID = List.last(explode probfile)
val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
@@ -814,8 +815,6 @@
VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"));() )
-
-
fun spass_proofHandler (n) = (
let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
val _ = TextIO.output (outfile, ("In signal handler now\n"))
@@ -847,8 +846,9 @@
else
()
)
- (* if there's no proof, but a some sort of message from Spass *)
- else
+ (* if there's no proof, but a message from Spass *)
+ else if ((substring (reconstr, 0,5))= "SPASS")
+ then
(
goals_being_watched := (!goals_being_watched) -1;
Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
@@ -864,7 +864,86 @@
end )
else
()
- )
+ )
+ (* print out a list of rules used from clasimpset*)
+ else if ((substring (reconstr, 0,5))= "Rules")
+ then
+ (
+ goals_being_watched := (!goals_being_watched) -1;
+ Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ Pretty.writeln(Pretty.str (goalstring^reconstr));
+ Pretty.writeln(Pretty.str (oct_char "361"));
+ if (!goals_being_watched = 0)
+ then
+ (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
+ val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
+ val _ = TextIO.closeOut outfile
+ in
+ killWatcher (childpid); reapWatcher (childpid,childin, childout);()
+ end )
+ else
+ ()
+ )
+
+ (* if proof translation failed *)
+ else if ((substring (reconstr, 0,5)) = "Proof")
+ then
+ (
+ goals_being_watched := (!goals_being_watched) -1;
+ Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
+ Pretty.writeln(Pretty.str (oct_char "361"));
+ if (!goals_being_watched = 0)
+ then
+ (let val outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
+ val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
+ val _ = TextIO.closeOut outfile
+ in
+ killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
+ end )
+ else
+ ( )
+ )
+
+ else if ((substring (reconstr, 0,1)) = "%")
+ then
+ (
+ goals_being_watched := (!goals_being_watched) -1;
+ Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
+ Pretty.writeln(Pretty.str (oct_char "361"));
+ if (!goals_being_watched = 0)
+ then
+ (let val outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
+ val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
+ val _ = TextIO.closeOut outfile
+ in
+ killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
+ end )
+ else
+ ( )
+ )
+
+
+ else (* add something here ?*)
+ (
+ goals_being_watched := (!goals_being_watched) -1;
+ Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ Pretty.writeln(Pretty.str ("Ran out of options in handler"));
+ Pretty.writeln(Pretty.str (oct_char "361"));
+ if (!goals_being_watched = 0)
+ then
+ (let val outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
+ val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
+ val _ = TextIO.closeOut outfile
+ in
+ killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
+ end )
+ else
+ ( )
+ )
+
+
end)
--- a/src/HOL/Tools/res_atp.ML Mon Jul 11 14:52:55 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Mon Jul 11 16:42:42 2005 +0200
@@ -113,7 +113,7 @@
(* convert clauses from "assume" to conjecture. write to file "hyps" *)
(* hypotheses of the goal currently being proved *)
(*********************************************************************)
-
+(*perhaps have 2 different versions of this, depending on whether or not SpassComm.spass is set *)
fun isar_atp_h thms =
let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
@@ -123,6 +123,7 @@
val clss = map ResClause.make_conjecture_clause prems'''
val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
val tfree_lits = ResLib.flat_noDup tfree_litss
+ (* tfree clause is different in tptp and dfg versions *)
val tfree_clss = map ResClause.tfree_clause tfree_lits
val hypsfile = File.platform_path hyps_file
val out = TextIO.openOut(hypsfile)
@@ -151,6 +152,24 @@
end;
+(*********************************************************************)
+(* write out a subgoal as DFG clauses to the file "probN" *)
+(* where N is the number of this subgoal *)
+(*********************************************************************)
+(*
+fun dfg_inputs_tfrees thms n tfrees =
+ let val _ = (warning ("in dfg_inputs_tfrees 0"))
+ val clss = map (ResClause.make_conjecture_clause_thm) thms
+ val _ = (warning ("in dfg_inputs_tfrees 1"))
+ val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
+ val _ = (warning ("in dfg_inputs_tfrees 2"))
+ val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees)
+ val _ = (warning ("in dfg_inputs_tfrees 3"))
+ val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
+ val out = TextIO.openOut(probfile)
+ in
+ (ResLib.writeln_strs out (tfree_clss @ dfg_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
+ end;*)
(*********************************************************************)
(* call SPASS with settings and problem file for the current subgoal *)
--- a/src/HOL/Tools/res_clause.ML Mon Jul 11 14:52:55 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML Mon Jul 11 16:42:42 2005 +0200
@@ -257,6 +257,7 @@
| fun_name_type _ = raise CLAUSE("Function Not First Order");
+(* FIX - add in funcs and stuff to this *)
fun term_of (Var(ind_nm,T)) =
let val (folType,ts) = type_of T