# HG changeset patch # User quigley # Date 1121092962 -7200 # Node ID 2d4433759b8d5d0554648e5ddb74d1badf56cb4b # Parent ea667a5426fe99624cd21afd46057277241f6a6a Fixed some problems with the signal handler. diff -r ea667a5426fe -r 2d4433759b8d src/HOL/Tools/ATP/SpassCommunication.ML --- 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 diff -r ea667a5426fe -r 2d4433759b8d src/HOL/Tools/ATP/watcher.ML --- 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) diff -r ea667a5426fe -r 2d4433759b8d src/HOL/Tools/res_atp.ML --- 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 *) diff -r ea667a5426fe -r 2d4433759b8d src/HOL/Tools/res_clause.ML --- 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