author  paulson 
Tue, 19 Apr 2005 18:08:44 +0200  
changeset 15774  9df37a0e935d 
parent 15736  1bb0399a9517 
child 15779  aed221aff642 
permissions  rwrr 
15608  1 
(* Author: Jia Meng, Cambridge University Computer Laboratory 
2 
ID: $Id$ 

3 
Copyright 2004 University of Cambridge 

15347  4 

5 
ATPs with TPTP format input. 

6 
*) 

15452  7 

8 
(*Jia: changed: isar_atp now processes entire proof context. fetch thms from delta simpset/claset*) 

15644  9 
(*Claire: changed: added actual watcher calls *) 
15452  10 

15347  11 
signature RES_ATP = 
12 
sig 

15608  13 
val trace_res : bool ref 
14 
val axiom_file : Path.T 

15 
val hyps_file : Path.T 

16 
val isar_atp : ProofContext.context * Thm.thm > unit 

15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

17 
val prob_file : Path.T; 
15644  18 
(*val atp_ax_tac : Thm.thm list > int > Tactical.tactic*) 
19 
(*val atp_tac : int > Tactical.tactic*) 

15608  20 
val debug: bool ref 
15347  21 

22 
end; 

23 

24 
structure ResAtp : RES_ATP = 

15608  25 

15347  26 
struct 
27 

15644  28 

29 

15608  30 
(* used for debug *) 
31 
val debug = ref false; 

15452  32 

15608  33 
fun debug_tac tac = (warning "testing";tac); 
34 
(* default value is false *) 

15347  35 

15608  36 
val trace_res = ref false; 
15347  37 

15608  38 
val skolem_tac = skolemize_tac; 
39 

15644  40 
val num_of_clauses = ref 0; 
41 
val clause_arr = Array.array(3500, ("empty", 0)); 

42 

15347  43 

15608  44 
val atomize_tac = 
45 
SUBGOAL 

46 
(fn (prop,_) => 

47 
let val ts = Logic.strip_assums_hyp prop 

48 
in EVERY1 

49 
[METAHYPS 

50 
(fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)), 

51 
REPEAT_DETERM_N (length ts) o (etac thin_rl)] 

52 
end); 

15347  53 

15608  54 
(* temporarily use these files, which will be loaded by Vampire *) 
15644  55 
val file_id_num =ref 0; 
15608  56 

15644  57 
fun new_prob_file () = (file_id_num := (!file_id_num) + 1;"prob"^(string_of_int (!file_id_num))); 
15608  58 

15347  59 

15644  60 
val axiom_file = File.tmp_path (Path.basic "axioms"); 
61 
val clasimp_file = File.tmp_path (Path.basic "clasimp"); 

62 
val hyps_file = File.tmp_path (Path.basic "hyps"); 

63 
val prob_file = File.tmp_path (Path.basic "prob"); 

64 
val dummy_tac = PRIMITIVE(fn thm => thm ); 

65 

66 

15347  67 
(**** for Isabelle/ML interface ****) 
68 

15644  69 
fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ") 
15608  70 

15644  71 
fun proofstring x = let val exp = explode x 
72 
in 

73 
List.filter (is_proof_char ) exp 

74 
end 

15608  75 

76 

15452  77 

15644  78 
(* 
79 
fun call_atp_tac thms n = (tptp_inputs thms ; dummy_tac); 

15347  80 

15644  81 
*) 
15347  82 

83 
(**** For running in Isar ****) 

84 

15608  85 
(* same function as that in res_axioms.ML *) 
86 
fun repeat_RS thm1 thm2 = 

87 
let val thm1' = thm1 RS thm2 handle THM _ => thm1 

88 
in 

89 
if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2) 

90 
end; 

91 

92 
(* a special version of repeat_RS *) 

93 
fun repeat_someI_ex thm = repeat_RS thm someI_ex; 

94 

15644  95 
(*********************************************************************) 
15608  96 
(* convert clauses from "assume" to conjecture. write to file "hyps" *) 
15644  97 
(* hypotheses of the goal currently being proved *) 
98 
(*********************************************************************) 

99 

15608  100 
fun isar_atp_h thms = 
15644  101 

15608  102 
let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms 
15644  103 
val prems' = map repeat_someI_ex prems 
104 
val prems'' = make_clauses prems' 

105 
val prems''' = ResAxioms.rm_Eps [] prems'' 

106 
val clss = map ResClause.make_conjecture_clause prems''' 

15774  107 
val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
15608  108 
val tfree_lits = ResLib.flat_noDup tfree_litss 
109 
val tfree_clss = map ResClause.tfree_clause tfree_lits 

110 
val hypsfile = File.sysify_path hyps_file 

111 
val out = TextIO.openOut(hypsfile) 

112 
in 

113 
((ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; if !trace_res then (warning hypsfile) else ());tfree_lits) 

114 
end; 

15347  115 

15644  116 

117 
(*********************************************************************) 

118 
(* write out a subgoal as tptp clauses to the file "probN" *) 

119 
(* where N is the number of this subgoal *) 

120 
(*********************************************************************) 

121 

15608  122 
fun tptp_inputs_tfrees thms n tfrees = 
15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

123 
let val _ = (warning ("in tptp_inputs_tfrees 0")) 
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

124 
val clss = map (ResClause.make_conjecture_clause_thm) thms 
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

125 
val _ = (warning ("in tptp_inputs_tfrees 1")) 
15774  126 
val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

127 
val _ = (warning ("in tptp_inputs_tfrees 2")) 
15608  128 
val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 
15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

129 
val _ = (warning ("in tptp_inputs_tfrees 3")) 
15608  130 
val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n) 
131 
val out = TextIO.openOut(probfile) 

132 
in 

133 
(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ())) 

134 
end; 

15452  135 

15608  136 

137 

15644  138 
(*********************************************************************) 
139 
(* call SPASS with settings and problem file for the current subgoal *) 

140 
(* should be modified to allow other provers to be called *) 

141 
(*********************************************************************) 

15608  142 

15697  143 
fun call_resolve_tac sign thms sg_term (childin, childout,pid) n = let 
15736  144 
val thmstring = Meson.concat_with_and (map string_of_thm thms) 
15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

145 
val thm_no = length thms 
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

146 
val _ = warning ("number of thms is : "^(string_of_int thm_no)) 
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

147 
val _ = warning ("thmstring in call_res is: "^thmstring) 
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

148 

15697  149 
val goalstr = Sign.string_of_term sign sg_term 
15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

150 
val goalproofstring = proofstring goalstr 
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

151 
val no_returns =List.filter not_newline ( goalproofstring) 
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

152 
val goalstring = implode no_returns 
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

153 
val _ = warning ("goalstring in call_res is: "^goalstring) 
15644  154 

15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

155 
(*val prob_file =File.tmp_path (Path.basic newprobfile); *) 
15653  156 
(*val _ =( warning ("calling make_clauses ")) 
15644  157 
val clauses = make_clauses thms 
15653  158 
val _ =( warning ("called make_clauses "))*) 
15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

159 
(*val _ = tptp_inputs clauses prob_file*) 
15736  160 
val thmstring = Meson.concat_with_and (map string_of_thm thms) 
15644  161 

15697  162 
val goalstr = Sign.string_of_term sign sg_term 
15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

163 
val goalproofstring = proofstring goalstr 
15644  164 
val no_returns =List.filter not_newline ( goalproofstring) 
15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

165 
val goalstring = implode no_returns 
15608  166 

15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

167 
val thmproofstring = proofstring ( thmstring) 
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

168 
val no_returns =List.filter not_newline ( thmproofstring) 
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

169 
val thmstr = implode no_returns 
15644  170 

15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

171 
val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n) 
15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

172 
val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "hellofile"))) 
15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

173 
val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring); 
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

174 
val _ = TextIO.flushOut outfile; 
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

175 
val _ = TextIO.closeOut outfile 
15644  176 
in 
177 
(* without paramodulation *) 

15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

178 
(warning ("goalstring in call_res_tac is: "^goalstring)); 
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

179 
(warning ("prob file in cal_res_tac is: "^probfile)); 
15644  180 
Watcher.callResProvers(childout, 
181 
[("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS", 

182 
"FullRed=0%Auto=0%ISRe%ISFc%RTaut%RFSub%RBSub%DocProof", 

15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

183 
probfile)]); 
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

184 

15644  185 
(* with paramodulation *) 
186 
(*Watcher.callResProvers(childout, 

187 
[("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS", 

188 
"FullRed=0%ISPm=1%Split=0%PObv=0%DocProof", 

189 
prob_path)]); *) 

15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

190 
(* Watcher.callResProvers(childout, 
15644  191 
[("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS", 
15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

192 
"DocProof", prob_path)]);*) 
15644  193 
dummy_tac 
194 
end 

15452  195 

15644  196 
(************************************************) 
197 
(* pass in subgoal as a term and watcher info *) 

198 
(* process subgoal into skolemized, negated form*) 

199 
(* then call call_resolve_tac to send to ATP *) 

200 
(************************************************) 

15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

201 
(* 
15644  202 
fun resolve_tac sg_term (childin, childout,pid) = 
203 
let val _ = warning ("in resolve_tac ") 

204 
in 

205 
SELECT_GOAL 

15653  206 
(EVERY1 [rtac ccontr,atomize_tac,skolemize_tac, METAHYPS(fn negs => (warning ("calling call_resolve_tac next ");dummy_tac (*call_resolve_tac negs sg_term (childin, childout,pid)*)))]) 
15644  207 
end; 
15452  208 

15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

209 
*) 
15608  210 

15452  211 

15644  212 
(* Need to replace call_atp_tac_tfrees with call res_provers as it's the dummy one *) 
213 

214 
(**********************************************************) 

215 
(* write out the current subgoal as a tptp file, probN, *) 

216 
(* then call dummy_tac  should be call_res_tac *) 

217 
(**********************************************************) 

15653  218 
(* should call call_res_tac here, not resolve_tac *) 
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 *) 

15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

220 

28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

221 
(* dummy tac vs. Doesn't call resolve_tac *) 
15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

222 

15697  223 
fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) = 
15736  224 
( warning("ths for tptp: " ^ 
225 
Meson.concat_with_and (map string_of_thm thms)); 

15697  226 
warning("in call_atp_tac_tfrees"); 
15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

227 

15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

228 
tptp_inputs_tfrees (make_clauses thms) n tfrees; 
15697  229 
call_resolve_tac sign thms sg_term (childin, childout, pid) n; 
15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

230 
dummy_tac); 
15644  231 

15697  232 
fun atp_tac_tfrees tfrees sg_term (childin, childout,pid) n st = 
233 
let val sign = sign_of_thm st 

234 
val _ = warning ("in atp_tac_tfrees ") 

235 
val _ = warning ("sg_term :" ^ (Sign.string_of_term sign sg_term)) 

15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

236 

28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

237 
in 
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

238 
SELECT_GOAL 
15682  239 
(EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
15697  240 
METAHYPS(fn negs => (warning("calling call_atp_tac_tfrees with negs" 
15736  241 
^ Meson.concat_with_and (map string_of_thm negs)); 
15697  242 
call_atp_tac_tfrees sign negs n tfrees sg_term (childin, childout,pid) ))]) n st 
15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

243 
end; 
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

244 

28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

245 

28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

246 
fun isar_atp_g tfrees sg_term (childin, childout, pid) n = 
15644  247 

15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

248 
((warning("in isar_atp_g"));atp_tac_tfrees tfrees sg_term (childin, childout, pid) n); 
15644  249 

250 

251 

252 
(**********************************************) 

253 
(* recursively call atp_tac_g on all subgoals *) 

254 
(* sg_term is the nth subgoal as a term  used*) 

255 
(* in proof reconstruction *) 

256 
(**********************************************) 

257 

258 
fun isar_atp_goal' thm k n tfree_lits (childin, childout, pid) = 

259 
if (k > n) 

260 
then () 

261 
else 

262 
(let val prems = prems_of thm 

263 
val sg_term = get_nth n prems 

15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

264 
val thmstring = string_of_thm thm 
15644  265 
in 
266 

267 
(warning("in isar_atp_goal'")); 

15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

268 
(warning("thmstring in isar_atp_goal: "^thmstring)); 
15644  269 
isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm; 
270 
isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid) 

271 
end); 

272 

273 

274 
fun isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid) = (if (!debug) then warning (string_of_thm thm) else (isar_atp_goal' thm 1 n_subgoals tfree_lits (childin, childout, pid) )); 

275 

276 
(**************************************************) 

277 
(* convert clauses from "assume" to conjecture. *) 

278 
(* i.e. apply make_clauses and then get tptp for *) 

15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

279 
(* any hypotheses in the goal produced by assume *) 
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

280 
(* statements; *) 
15644  281 
(* write to file "hyps" *) 
282 
(**************************************************) 

283 

284 

285 
fun isar_atp_aux thms thm n_subgoals (childin, childout, pid) = 

15608  286 
let val tfree_lits = isar_atp_h thms 
287 
in 

15644  288 
(warning("in isar_atp_aux"));isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid) 
15608  289 
end; 
15644  290 

291 
(******************************************************************) 

292 
(* called in Isar automatically *) 

293 
(* writes out the current clasimpset to a tptp file *) 

294 
(* passes all subgoals on to isar_atp_aux for further processing *) 

295 
(* turns off xsymbol at start of function, restoring it at end *) 

296 
(******************************************************************) 

15452  297 

15608  298 
fun isar_atp' (thms, thm) = 
15644  299 
let val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) 
300 
val _= (warning ("in isar_atp'")) 

301 
val prems = prems_of thm 

15697  302 
val sign = sign_of_thm thm 
15736  303 
val thms_string = Meson.concat_with_and (map string_of_thm thms) 
15644  304 
val thmstring = string_of_thm thm 
15736  305 
val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
15644  306 
(* set up variables for writing out the clasimps to a tptp file *) 
15700  307 
val _ = write_out_clasimp (File.sysify_path axiom_file) 
15644  308 
(* cq: add write out clasimps to file *) 
309 
(* cq:create watcher and pass to isar_atp_aux *) 

15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

310 
val (childin,childout,pid) = Watcher.createWatcher() 
15644  311 
val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid ))) 
15608  312 
in 
15644  313 
case prems of [] => () 
314 
 _ => ((warning ("initial thms: "^thms_string)); 

315 
(warning ("initial thm: "^thmstring)); 

316 
(warning ("subgoals: "^prems_string)); 

317 
(warning ("pid: "^ pidstring))); 

318 
isar_atp_aux thms thm (length prems) (childin, childout, pid) ; 

319 

320 
print_mode := (["xsymbols", "symbols"] @ ! print_mode) 

15608  321 
end; 
322 

15452  323 

15608  324 

325 

326 
local 

327 

328 
fun get_thms_cs claset = 

329 
let val clsset = rep_cs claset 

330 
val safeEs = #safeEs clsset 

331 
val safeIs = #safeIs clsset 

332 
val hazEs = #hazEs clsset 

333 
val hazIs = #hazIs clsset 

334 
in 

335 
safeEs @ safeIs @ hazEs @ hazIs 

336 
end; 

337 

338 

15452  339 

15608  340 
fun append_name name [] _ = [] 
341 
 append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1)); 

342 

343 
fun append_names (name::names) (thms::thmss) = 

344 
let val thms' = append_name name thms 0 

345 
in 

346 
thms'::(append_names names thmss) 

347 
end; 

348 

15452  349 

15608  350 
fun get_thms_ss [] = [] 
351 
 get_thms_ss thms = 

352 
let val names = map Thm.name_of_thm thms 

353 
val thms' = map (mksimps mksimps_pairs) thms 

354 
val thms'' = append_names names thms' 

355 
in 

356 
ResLib.flat_noDup thms'' 

357 
end; 

358 

15452  359 

15608  360 

361 

362 
in 

363 

15452  364 

15608  365 
(* convert locally declared rules to axiom clauses *) 
366 
(* write axiom clauses to ax_file *) 

15644  367 
(* what about clasimpset  it should already be in the ax file  perhaps append to ax file rather than just *) 
368 
(* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *) 

369 
(*claset file and prob file*) 

15608  370 
fun isar_local_thms (delta_cs, delta_ss_thms) = 
371 
let val thms_cs = get_thms_cs delta_cs 

372 
val thms_ss = get_thms_ss delta_ss_thms 

373 
val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss)) 

374 
val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*) 

375 
val ax_file = File.sysify_path axiom_file 

376 
val out = TextIO.openOut ax_file 

377 
in 

15644  378 
(ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out) 
15608  379 
end; 
15347  380 

15608  381 

382 

383 

15347  384 

15608  385 
(* called in Isar automatically *) 
15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

386 

15608  387 
fun isar_atp (ctxt,thm) = 
388 
let val prems = ProofContext.prems_of ctxt 

15644  389 
val d_cs = Classical.get_delta_claset ctxt 
390 
val d_ss_thms = Simplifier.get_delta_simpset ctxt 

391 
val thmstring = string_of_thm thm 

15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

392 
val sg_prems = prems_of thm 
15697  393 
val sign = sign_of_thm thm 
15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

394 
val prem_no = length sg_prems 
15736  395 
val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems) 
15608  396 
in 
15644  397 
(warning ("initial thm in isar_atp: "^thmstring)); 
398 
(warning ("subgoals in isar_atp: "^prems_string)); 

399 
(warning ("number of subgoals in isar_atp: "^(string_of_int prem_no))); 

400 
(isar_local_thms (d_cs,d_ss_thms); (warning("about to call isar_atp'")); 

401 
isar_atp' (prems, thm)) 

15608  402 
end; 
15347  403 

15608  404 
end 
405 

406 

407 

15452  408 

15347  409 
end; 
410 

411 
Proof.atp_hook := ResAtp.isar_atp; 