39 val problem_name = ref "prob"; |
39 val problem_name = ref "prob"; |
40 |
40 |
41 |
41 |
42 (* basic template *) |
42 (* basic template *) |
43 |
43 |
|
44 fun with_path cleanup after f path = |
|
45 Exn.capture f path |
|
46 |> tap (fn _ => cleanup path) |
|
47 |> Exn.release |
|
48 |> tap (after path) |
|
49 |
44 fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer |
50 fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer |
45 timeout axiom_clauses filtered_clauses name subgoalno goal = |
51 timeout axiom_clauses filtered_clauses name subgoalno goal = |
46 let |
52 let |
47 (* path to unique problem file *) |
53 (* path to unique problem file *) |
48 val destdir' = ! destdir |
54 val destdir' = ! destdir |
71 | SOME axcls => axcls |
77 | SOME axcls => axcls |
72 val (thm_names, clauses) = |
78 val (thm_names, clauses) = |
73 preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy |
79 preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy |
74 |
80 |
75 (* write out problem file and call prover *) |
81 (* write out problem file and call prover *) |
76 val probfile = prob_pathname subgoalno |
82 fun cmd_line probfile = space_implode " " ["exec", File.shell_path cmd, |
77 val conj_pos = writer probfile clauses |
83 args, File.platform_path probfile] |
78 val (proof, rc) = system_out ( |
84 fun run_on probfile = |
79 if File.exists cmd then |
85 if File.exists cmd |
80 space_implode " " ["exec", File.shell_path cmd, args, File.platform_path probfile] |
86 then writer probfile clauses |> pair (system_out (cmd_line probfile)) |
81 else error ("Bad executable: " ^ Path.implode cmd)) |
87 else error ("Bad executable: " ^ Path.implode cmd) |
82 |
88 |
83 (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *) |
89 (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *) |
84 val _ = |
90 fun cleanup probfile = if destdir' = "" then File.rm probfile else () |
85 if destdir' = "" then File.rm probfile |
91 fun export probfile ((proof, _), _) = if destdir' = "" then () |
86 else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof |
92 else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof |
|
93 |
|
94 val ((proof, rc), conj_pos) = with_path cleanup export run_on |
|
95 (prob_pathname subgoalno) |
87 |
96 |
88 (* check for success and print out some information on failure *) |
97 (* check for success and print out some information on failure *) |
89 val failure = find_failure proof |
98 val failure = find_failure proof |
90 val success = rc = 0 andalso is_none failure |
99 val success = rc = 0 andalso is_none failure |
91 val message = |
100 val message = |