62 val hyps_file = File.tmp_path (Path.basic "hyps"); |
62 val hyps_file = File.tmp_path (Path.basic "hyps"); |
63 val prob_file = File.tmp_path (Path.basic "prob"); |
63 val prob_file = File.tmp_path (Path.basic "prob"); |
64 val dummy_tac = PRIMITIVE(fn thm => thm ); |
64 val dummy_tac = PRIMITIVE(fn thm => thm ); |
65 |
65 |
66 |
66 |
67 fun concat_with_and [] str = str |
|
68 | concat_with_and (x::[]) str = str^" ("^x^")" |
|
69 | concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & ")) |
|
70 |
|
71 |
|
72 |
|
73 (**** for Isabelle/ML interface ****) |
67 (**** for Isabelle/ML interface ****) |
74 |
68 |
75 fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ") |
69 fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ") |
76 |
70 |
77 fun proofstring x = let val exp = explode x |
71 fun proofstring x = let val exp = explode x |
145 (* call SPASS with settings and problem file for the current subgoal *) |
139 (* call SPASS with settings and problem file for the current subgoal *) |
146 (* should be modified to allow other provers to be called *) |
140 (* should be modified to allow other provers to be called *) |
147 (*********************************************************************) |
141 (*********************************************************************) |
148 |
142 |
149 fun call_resolve_tac sign thms sg_term (childin, childout,pid) n = let |
143 fun call_resolve_tac sign thms sg_term (childin, childout,pid) n = let |
150 val thmstring = concat_with_and (map string_of_thm thms) "" |
144 val thmstring = Meson.concat_with_and (map string_of_thm thms) |
151 val thm_no = length thms |
145 val thm_no = length thms |
152 val _ = warning ("number of thms is : "^(string_of_int thm_no)) |
146 val _ = warning ("number of thms is : "^(string_of_int thm_no)) |
153 val _ = warning ("thmstring in call_res is: "^thmstring) |
147 val _ = warning ("thmstring in call_res is: "^thmstring) |
154 |
148 |
155 val goalstr = Sign.string_of_term sign sg_term |
149 val goalstr = Sign.string_of_term sign sg_term |
161 (*val prob_file =File.tmp_path (Path.basic newprobfile); *) |
155 (*val prob_file =File.tmp_path (Path.basic newprobfile); *) |
162 (*val _ =( warning ("calling make_clauses ")) |
156 (*val _ =( warning ("calling make_clauses ")) |
163 val clauses = make_clauses thms |
157 val clauses = make_clauses thms |
164 val _ =( warning ("called make_clauses "))*) |
158 val _ =( warning ("called make_clauses "))*) |
165 (*val _ = tptp_inputs clauses prob_file*) |
159 (*val _ = tptp_inputs clauses prob_file*) |
166 val thmstring = concat_with_and (map string_of_thm thms) "" |
160 val thmstring = Meson.concat_with_and (map string_of_thm thms) |
167 |
161 |
168 val goalstr = Sign.string_of_term sign sg_term |
162 val goalstr = Sign.string_of_term sign sg_term |
169 val goalproofstring = proofstring goalstr |
163 val goalproofstring = proofstring goalstr |
170 val no_returns =List.filter not_newline ( goalproofstring) |
164 val no_returns =List.filter not_newline ( goalproofstring) |
171 val goalstring = implode no_returns |
165 val goalstring = implode no_returns |
225 (* if we take tptpinputs out it gets into call_res_tac then falls over as usual after printing out goalstring. but if we leave it in it falls over here *) |
219 (* if we take tptpinputs out it gets into call_res_tac then falls over as usual after printing out goalstring. but if we leave it in it falls over here *) |
226 |
220 |
227 (* dummy tac vs. Doesn't call resolve_tac *) |
221 (* dummy tac vs. Doesn't call resolve_tac *) |
228 |
222 |
229 fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) = |
223 fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) = |
230 ( warning("ths for tptp: " ^ (concat_with_and (map string_of_thm thms) "")); |
224 ( warning("ths for tptp: " ^ |
|
225 Meson.concat_with_and (map string_of_thm thms)); |
231 warning("in call_atp_tac_tfrees"); |
226 warning("in call_atp_tac_tfrees"); |
232 |
227 |
233 tptp_inputs_tfrees (make_clauses thms) n tfrees; |
228 tptp_inputs_tfrees (make_clauses thms) n tfrees; |
234 call_resolve_tac sign thms sg_term (childin, childout, pid) n; |
229 call_resolve_tac sign thms sg_term (childin, childout, pid) n; |
235 dummy_tac); |
230 dummy_tac); |
241 |
236 |
242 in |
237 in |
243 SELECT_GOAL |
238 SELECT_GOAL |
244 (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, |
239 (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, |
245 METAHYPS(fn negs => (warning("calling call_atp_tac_tfrees with negs" |
240 METAHYPS(fn negs => (warning("calling call_atp_tac_tfrees with negs" |
246 ^ (concat_with_and (map string_of_thm negs) "")); |
241 ^ Meson.concat_with_and (map string_of_thm negs)); |
247 call_atp_tac_tfrees sign negs n tfrees sg_term (childin, childout,pid) ))]) n st |
242 call_atp_tac_tfrees sign negs n tfrees sg_term (childin, childout,pid) ))]) n st |
248 end; |
243 end; |
249 |
244 |
250 |
245 |
251 fun isar_atp_g tfrees sg_term (childin, childout, pid) n = |
246 fun isar_atp_g tfrees sg_term (childin, childout, pid) n = |
303 fun isar_atp' (thms, thm) = |
298 fun isar_atp' (thms, thm) = |
304 let val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) |
299 let val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) |
305 val _= (warning ("in isar_atp'")) |
300 val _= (warning ("in isar_atp'")) |
306 val prems = prems_of thm |
301 val prems = prems_of thm |
307 val sign = sign_of_thm thm |
302 val sign = sign_of_thm thm |
308 val thms_string =concat_with_and (map string_of_thm thms) "" |
303 val thms_string = Meson.concat_with_and (map string_of_thm thms) |
309 val thmstring = string_of_thm thm |
304 val thmstring = string_of_thm thm |
310 val prems_string = concat_with_and (map (Sign.string_of_term sign) prems) "" |
305 val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) |
311 (* set up variables for writing out the clasimps to a tptp file *) |
306 (* set up variables for writing out the clasimps to a tptp file *) |
312 val _ = write_out_clasimp (File.sysify_path axiom_file) |
307 val _ = write_out_clasimp (File.sysify_path axiom_file) |
313 (* cq: add write out clasimps to file *) |
308 (* cq: add write out clasimps to file *) |
314 (* cq:create watcher and pass to isar_atp_aux *) |
309 (* cq:create watcher and pass to isar_atp_aux *) |
315 val (childin,childout,pid) = Watcher.createWatcher() |
310 val (childin,childout,pid) = Watcher.createWatcher() |
395 val d_ss_thms = Simplifier.get_delta_simpset ctxt |
390 val d_ss_thms = Simplifier.get_delta_simpset ctxt |
396 val thmstring = string_of_thm thm |
391 val thmstring = string_of_thm thm |
397 val sg_prems = prems_of thm |
392 val sg_prems = prems_of thm |
398 val sign = sign_of_thm thm |
393 val sign = sign_of_thm thm |
399 val prem_no = length sg_prems |
394 val prem_no = length sg_prems |
400 val prems_string = concat_with_and (map (Sign.string_of_term sign) sg_prems) "" |
395 val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems) |
401 in |
396 in |
402 |
|
403 (warning ("initial thm in isar_atp: "^thmstring)); |
397 (warning ("initial thm in isar_atp: "^thmstring)); |
404 (warning ("subgoals in isar_atp: "^prems_string)); |
398 (warning ("subgoals in isar_atp: "^prems_string)); |
405 (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no))); |
399 (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no))); |
406 (isar_local_thms (d_cs,d_ss_thms); (warning("about to call isar_atp'")); |
400 (isar_local_thms (d_cs,d_ss_thms); (warning("about to call isar_atp'")); |
407 isar_atp' (prems, thm)) |
401 isar_atp' (prems, thm)) |