263 |
263 |
264 val dfg_dir = File.tmp_path (Path.basic "dfg"); |
264 val dfg_dir = File.tmp_path (Path.basic "dfg"); |
265 val dfg_path = File.platform_path dfg_dir; |
265 val dfg_path = File.platform_path dfg_dir; |
266 |
266 |
267 val tptp2X = ResLib.helper_path "TPTP2X_HOME" "tptp2X" |
267 val tptp2X = ResLib.helper_path "TPTP2X_HOME" "tptp2X" |
|
268 |
268 |
269 |
269 (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***) |
270 (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***) |
270 val probID = List.last(explode probfile) |
271 val probID = List.last(explode probfile) |
271 val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID)) |
272 val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID)) |
272 |
273 |
812 fun vampire_proofHandler (n) = |
813 fun vampire_proofHandler (n) = |
813 (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
814 (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
814 VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"));() ) |
815 VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"));() ) |
815 |
816 |
816 |
817 |
817 |
|
818 |
|
819 fun spass_proofHandler (n) = ( |
818 fun spass_proofHandler (n) = ( |
820 let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1"))); |
819 let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1"))); |
821 val _ = TextIO.output (outfile, ("In signal handler now\n")) |
820 val _ = TextIO.output (outfile, ("In signal handler now\n")) |
822 val _ = TextIO.closeOut outfile |
821 val _ = TextIO.closeOut outfile |
823 val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin |
822 val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin |
845 killWatcher (childpid); reapWatcher (childpid,childin, childout); () |
844 killWatcher (childpid); reapWatcher (childpid,childin, childout); () |
846 end) |
845 end) |
847 else |
846 else |
848 () |
847 () |
849 ) |
848 ) |
850 (* if there's no proof, but a some sort of message from Spass *) |
849 (* if there's no proof, but a message from Spass *) |
851 else |
850 else if ((substring (reconstr, 0,5))= "SPASS") |
|
851 then |
852 ( |
852 ( |
853 goals_being_watched := (!goals_being_watched) -1; |
853 goals_being_watched := (!goals_being_watched) -1; |
854 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
854 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
855 Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr)); |
855 Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr)); |
856 Pretty.writeln(Pretty.str (oct_char "361")); |
856 Pretty.writeln(Pretty.str (oct_char "361")); |
862 in |
862 in |
863 killWatcher (childpid); reapWatcher (childpid,childin, childout); () |
863 killWatcher (childpid); reapWatcher (childpid,childin, childout); () |
864 end ) |
864 end ) |
865 else |
865 else |
866 () |
866 () |
867 ) |
867 ) |
|
868 (* print out a list of rules used from clasimpset*) |
|
869 else if ((substring (reconstr, 0,5))= "Rules") |
|
870 then |
|
871 ( |
|
872 goals_being_watched := (!goals_being_watched) -1; |
|
873 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
|
874 Pretty.writeln(Pretty.str (goalstring^reconstr)); |
|
875 Pretty.writeln(Pretty.str (oct_char "361")); |
|
876 if (!goals_being_watched = 0) |
|
877 then |
|
878 (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp"))); |
|
879 val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) |
|
880 val _ = TextIO.closeOut outfile |
|
881 in |
|
882 killWatcher (childpid); reapWatcher (childpid,childin, childout);() |
|
883 end ) |
|
884 else |
|
885 () |
|
886 ) |
|
887 |
|
888 (* if proof translation failed *) |
|
889 else if ((substring (reconstr, 0,5)) = "Proof") |
|
890 then |
|
891 ( |
|
892 goals_being_watched := (!goals_being_watched) -1; |
|
893 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
|
894 Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr))); |
|
895 Pretty.writeln(Pretty.str (oct_char "361")); |
|
896 if (!goals_being_watched = 0) |
|
897 then |
|
898 (let val outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp"))); |
|
899 val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) |
|
900 val _ = TextIO.closeOut outfile |
|
901 in |
|
902 killWatcher (childpid); reapWatcher (childpid,childin, childout); () |
|
903 end ) |
|
904 else |
|
905 ( ) |
|
906 ) |
|
907 |
|
908 else if ((substring (reconstr, 0,1)) = "%") |
|
909 then |
|
910 ( |
|
911 goals_being_watched := (!goals_being_watched) -1; |
|
912 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
|
913 Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr))); |
|
914 Pretty.writeln(Pretty.str (oct_char "361")); |
|
915 if (!goals_being_watched = 0) |
|
916 then |
|
917 (let val outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp"))); |
|
918 val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) |
|
919 val _ = TextIO.closeOut outfile |
|
920 in |
|
921 killWatcher (childpid); reapWatcher (childpid,childin, childout); () |
|
922 end ) |
|
923 else |
|
924 ( ) |
|
925 ) |
|
926 |
|
927 |
|
928 else (* add something here ?*) |
|
929 ( |
|
930 goals_being_watched := (!goals_being_watched) -1; |
|
931 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); |
|
932 Pretty.writeln(Pretty.str ("Ran out of options in handler")); |
|
933 Pretty.writeln(Pretty.str (oct_char "361")); |
|
934 if (!goals_being_watched = 0) |
|
935 then |
|
936 (let val outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp"))); |
|
937 val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) |
|
938 val _ = TextIO.closeOut outfile |
|
939 in |
|
940 killWatcher (childpid); reapWatcher (childpid,childin, childout); () |
|
941 end ) |
|
942 else |
|
943 ( ) |
|
944 ) |
|
945 |
|
946 |
868 |
947 |
869 end) |
948 end) |
870 |
949 |
871 |
950 |
872 |
951 |