equal
deleted
inserted
replaced
3 Copyright 2004 University of Cambridge |
3 Copyright 2004 University of Cambridge |
4 |
4 |
5 ATPs with TPTP format input. |
5 ATPs with TPTP format input. |
6 *) |
6 *) |
7 |
7 |
8 (*FIXME: Do we need this signature?*) |
8 (*Currently unused, during debugging*) |
9 signature RES_ATP = |
9 signature RES_ATP = |
10 sig |
10 sig |
11 val prover: string ref |
11 val prover: string ref |
12 val custom_spass: string list ref |
12 val custom_spass: string list ref |
13 val destdir: string ref |
13 val destdir: string ref |
827 ignore (map (try cond_rm_tmp) files))) |
827 ignore (map (try cond_rm_tmp) files))) |
828 handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed"; |
828 handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed"; |
829 |
829 |
830 (*writes out the current clasimpset to a tptp file; |
830 (*writes out the current clasimpset to a tptp file; |
831 turns off xsymbol at start of function, restoring it at end *) |
831 turns off xsymbol at start of function, restoring it at end *) |
832 val isar_atp = setmp print_mode [] |
832 fun isar_atp_body (ctxt, th) = |
833 (fn (ctxt, th) => |
|
834 if Thm.no_prems th then () |
833 if Thm.no_prems th then () |
835 else |
834 else |
836 let |
835 let |
837 val _ = kill_last_watcher() |
836 val _ = kill_last_watcher() |
838 val (files,thm_names_list) = write_problem_files prob_pathname (ctxt,th) |
837 val (files,thm_names_list) = write_problem_files prob_pathname (ctxt,th) |
840 in |
839 in |
841 last_watcher_pid := SOME (childin, childout, pid, files); |
840 last_watcher_pid := SOME (childin, childout, pid, files); |
842 Output.debug ("problem files: " ^ space_implode ", " files); |
841 Output.debug ("problem files: " ^ space_implode ", " files); |
843 Output.debug ("pid: " ^ string_of_pid pid); |
842 Output.debug ("pid: " ^ string_of_pid pid); |
844 watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid) |
843 watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid) |
845 end); |
844 end; |
|
845 |
|
846 val isar_atp = setmp print_mode [] isar_atp_body; |
|
847 |
|
848 (*For ML scripts, and primarily, for debugging*) |
|
849 fun callatp () = |
|
850 let val th = topthm() |
|
851 val ctxt = ProofContext.init (theory_of_thm th) |
|
852 in isar_atp_body (ctxt, th) end; |
846 |
853 |
847 val isar_atp_writeonly = setmp print_mode [] |
854 val isar_atp_writeonly = setmp print_mode [] |
848 (fn (ctxt,th) => |
855 (fn (ctxt,th) => |
849 if Thm.no_prems th then () |
856 if Thm.no_prems th then () |
850 else |
857 else |