author  quigley 
Mon, 20 Jun 2005 18:39:24 +0200  
changeset 16478  d0a1f6231e2f 
parent 16475  8f3ba52a7937 
child 16515  7896ea4f3a87 
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 

15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

11 

15347  12 
signature RES_ATP = 
16478  13 
sig 
15608  14 
val trace_res : bool ref 
15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

15 
val subgoals: Thm.thm list 
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

16 
val traceflag : bool ref 
15608  17 
val axiom_file : Path.T 
18 
val hyps_file : Path.T 

19 
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

20 
val prob_file : Path.T; 
15644  21 
(*val atp_ax_tac : Thm.thm list > int > Tactical.tactic*) 
22 
(*val atp_tac : int > Tactical.tactic*) 

15608  23 
val debug: bool ref 
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16089
diff
changeset

24 
val full_spass: bool ref 
16478  25 
(*val spass: bool ref*) 
26 
val vampire: bool ref 

15347  27 
end; 
28 

29 
structure ResAtp : RES_ATP = 

15608  30 

15347  31 
struct 
32 

15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

33 
val subgoals = []; 
15644  34 

15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

35 
val traceflag = ref true; 
16357  36 
(* used for debug *) 
37 
val debug = ref false; 

16172
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

38 

15608  39 
fun debug_tac tac = (warning "testing";tac); 
16357  40 
(* default value is false *) 
16478  41 

16357  42 
val full_spass = ref false; 
16478  43 

44 
(* use spass as default prover *) 

45 
(*val spass = ref true;*) 

46 

47 
val vampire = ref false; 

48 

15608  49 
val trace_res = ref false; 
15347  50 

15608  51 
val skolem_tac = skolemize_tac; 
52 

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

55 

15347  56 

15608  57 
val atomize_tac = 
58 
SUBGOAL 

59 
(fn (prop,_) => 

60 
let val ts = Logic.strip_assums_hyp prop 

61 
in EVERY1 

62 
[METAHYPS 

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

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

65 
end); 

15347  66 

15608  67 
(* temporarily use these files, which will be loaded by Vampire *) 
15644  68 
val file_id_num =ref 0; 
15608  69 

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

15347  72 

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

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

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

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

78 

79 

15347  80 
(**** for Isabelle/ML interface ****) 
81 

16357  82 
fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ") 
15608  83 

16357  84 
fun proofstring x = let val exp = explode x 
85 
in 

86 
List.filter (is_proof_char ) exp 

87 
end 

88 

15608  89 

15452  90 

15644  91 
(* 
92 
fun call_atp_tac thms n = (tptp_inputs thms ; dummy_tac); 

15347  93 

15644  94 
*) 
15347  95 

96 
(**** For running in Isar ****) 

97 

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

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

101 
in 

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

103 
end; 

104 

105 
(* a special version of repeat_RS *) 

106 
fun repeat_someI_ex thm = repeat_RS thm someI_ex; 

107 

15644  108 
(*********************************************************************) 
15608  109 
(* convert clauses from "assume" to conjecture. write to file "hyps" *) 
15644  110 
(* hypotheses of the goal currently being proved *) 
111 
(*********************************************************************) 

112 

15608  113 
fun isar_atp_h thms = 
15644  114 

15608  115 
let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms 
15644  116 
val prems' = map repeat_someI_ex prems 
117 
val prems'' = make_clauses prems' 

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

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

15774  120 
val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
15608  121 
val tfree_lits = ResLib.flat_noDup tfree_litss 
122 
val tfree_clss = map ResClause.tfree_clause tfree_lits 

16259  123 
val hypsfile = File.platform_path hyps_file 
15608  124 
val out = TextIO.openOut(hypsfile) 
125 
in 

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

127 
end; 

15347  128 

15644  129 

130 
(*********************************************************************) 

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

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

133 
(*********************************************************************) 

134 

15608  135 
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

136 
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

137 
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

138 
val _ = (warning ("in tptp_inputs_tfrees 1")) 
15774  139 
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

140 
val _ = (warning ("in tptp_inputs_tfrees 2")) 
15608  141 
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

142 
val _ = (warning ("in tptp_inputs_tfrees 3")) 
16259  143 
val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) 
15608  144 
val out = TextIO.openOut(probfile) 
145 
in 

16357  146 
(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ())) 
15608  147 
end; 
15452  148 

15608  149 

16357  150 

15644  151 
(*********************************************************************) 
152 
(* call SPASS with settings and problem file for the current subgoal *) 

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

154 
(*********************************************************************) 

16357  155 
(* now passing in list of skolemized thms and list of sgterms to go with them *) 
156 
fun call_resolve_tac (thms: Thm.thm list list) sign (sg_terms: Term.term list) (childin, childout,pid) n = let 

157 
val axfile = (File.platform_path axiom_file) 

16475  158 
val hypsfile = (File.platform_path hyps_file) 
159 
val clasimpfile = (File.platform_path clasimp_file) 

160 
val spass_home = getenv "SPASS_HOME" 

161 
val spass = spass_home ^ "/SPASS" 

162 
val _ = if File.exists (File.unpack_platform_path spass) then () 

163 
else error ("Could not find the file " ^ spass) 

16357  164 

16475  165 
fun make_atp_list [] sign n = [] 
166 
 make_atp_list ((sko_thm, sg_term)::xs) sign n = 

167 
let 

16357  168 
val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm) 
169 
val thmproofstr = proofstring ( skothmstr) 

170 
val no_returns =List.filter not_newline ( thmproofstr) 

171 
val thmstr = implode no_returns 

172 
val _ = warning ("thmstring in make_atp_lists is: "^thmstr) 

15608  173 

16357  174 
val sgstr = Sign.string_of_term sign sg_term 
175 
val goalproofstring = proofstring sgstr 

16089
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

176 
val no_returns =List.filter not_newline ( goalproofstring) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

177 
val goalstring = implode no_returns 
16357  178 
val _ = warning ("goalstring in make_atp_lists is: "^goalstring) 
179 

16259  180 
val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) 
16357  181 
val _ = (warning ("prob file in cal_res_tac is: "^probfile)) 
182 
in 

16478  183 
if !SpassComm.spass 
184 
then if !full_spass 

185 
then 

16357  186 
([("spass", thmstr, goalstring (*,spass_home*), 
187 
getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*), 

188 
"DocProof%TimeLimit=60", 

189 
clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) 

16478  190 
else 
16357  191 
([("spass", thmstr, goalstring (*,spass_home*), 
192 
getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*), 

16478  193 
"Auto=0%IORe%IOFc%RTaut%RFSub%RBSub%DocProof%TimeLimit=60", 
194 
clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) 

195 
else 

196 
([("vampire", thmstr, goalstring (*,spass_home*), 

197 
"/homes/jm318/Vampire8/vkernel"(*( getenv "SPASS_HOME")^"/SPASS"*), 

198 
"t 300%m 100000", 

16357  199 
clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) 
200 
end 

15452  201 

16357  202 
val thms_goals = ListPair.zip( thms, sg_terms) 
203 
val atp_list = make_atp_list thms_goals sign 1 

204 
in 

205 
Watcher.callResProvers(childout,atp_list); 

206 
warning("Sent commands to watcher!"); 

207 
dummy_tac 

208 
end 

209 
(* 

210 
val axfile = (File.platform_path axiom_file) 

211 
val hypsfile = (File.platform_path hyps_file) 

212 
val clasimpfile = (File.platform_path clasimp_file) 

213 
val spass_home = getenv "SPASS_HOME" 

214 
val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int 1) 

215 

216 
val (clause_arr, num_of_clauses) = ResClasimp.write_out_clasimp_small (File.platform_path clasimp_file) ; 

217 
val (childin,childout,pid) = Watcher.createWatcher(mp, clause_arr, num_of_clauses); 

218 
Watcher.callResProvers(childout, [("spass", "thmstring", "goalstr", spass_home, "DocProof", clasimpfile, axfile, hypsfile,probfile)]); 

219 

220 
Watcher.callResProvers(childout, [("spass", "thmstring", "goalstr", "/homes/clq20/spassshell", "", clasimpfile, axfile, hypsfile,probfile)]); 

221 

222 

223 
*) 

15644  224 
(**********************************************************) 
225 
(* write out the current subgoal as a tptp file, probN, *) 

226 
(* then call dummy_tac  should be call_res_tac *) 

227 
(**********************************************************) 

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

228 

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

229 

16357  230 
fun get_sko_thms tfrees sign sg_terms (childin, childout,pid) thm n sko_thms = 
231 
if (equal n 0) then 

232 
(call_resolve_tac (rev sko_thms) sign sg_terms (childin, childout, pid) (List.length sg_terms);dummy_tac thm) 

233 
else 

234 

235 
( SELECT_GOAL 

236 
(EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 

237 
METAHYPS(fn negs => (tptp_inputs_tfrees (make_clauses negs) n tfrees; 

238 
get_sko_thms tfrees sign sg_terms (childin, childout, pid) thm (n 1) (negs::sko_thms);dummy_tac))]) n thm ) 

15644  239 

240 

241 

242 
(**********************************************) 

243 
(* recursively call atp_tac_g on all subgoals *) 

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

245 
(* in proof reconstruction *) 

246 
(**********************************************) 

247 

16357  248 
fun isar_atp_goal' thm n tfree_lits (childin, childout, pid) = 
249 

250 
(let val prems = prems_of thm 

251 
(*val sg_term = get_nth k prems*) 

252 
val sign = sign_of_thm thm 

253 
val thmstring = string_of_thm thm 

254 
in 

255 

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

257 
(warning("thmstring in isar_atp_goal': "^thmstring)); 

258 
(* go and call callResProvers with this subgoal *) 

259 
(* isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm; *) 

260 
(* recursive call to pick up the remaining subgoals *) 

261 
(* isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid) *) 

262 
get_sko_thms tfree_lits sign prems (childin, childout, pid) thm n [] 

263 
end); 

15644  264 

16357  265 
(*fun isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid) = 
15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

266 
(if (!debug) then warning (string_of_thm thm) 
16357  267 
else (isar_atp_goal' thm n_subgoals tfree_lits (childin, childout, pid) ));*) 
15644  268 

269 
(**************************************************) 

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

271 
(* 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

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

273 
(* statements; *) 
15644  274 
(* write to file "hyps" *) 
275 
(**************************************************) 

276 

277 

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

15608  279 
let val tfree_lits = isar_atp_h thms 
16357  280 
in 
281 
(warning("in isar_atp_aux")); 

282 
isar_atp_goal' thm n_subgoals tfree_lits (childin, childout, pid) 

15608  283 
end; 
15644  284 

285 
(******************************************************************) 

286 
(* called in Isar automatically *) 

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

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

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

290 
(******************************************************************) 

15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

291 
(*FIX changed to clasimp_file *) 
16357  292 
fun isar_atp' (ctxt,thms, thm) = 
293 
let 

294 
val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) 

15644  295 
val _= (warning ("in isar_atp'")) 
15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

296 
val prems = prems_of thm 
15697  297 
val sign = sign_of_thm thm 
15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

298 
val thms_string = Meson.concat_with_and (map string_of_thm thms) 
15644  299 
val thmstring = string_of_thm thm 
15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

300 
val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

301 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

302 
(* set up variables for writing out the clasimps to a tptp file *) 
16172
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

303 
val (clause_arr, num_of_clauses) = 
16357  304 
ResClasimp.write_out_clasimp(*_small*) (File.platform_path clasimp_file) 
16172
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

305 
(ProofContext.theory_of ctxt) 
16357  306 
val _ = (warning ("clasimp_file is this: "^(File.platform_path clasimp_file)) ) 
15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

307 

15644  308 
(* cq: add write out clasimps to file *) 
15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

309 
(* cq:create watcher and pass to isar_atp_aux *) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

310 
(* tracing *) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

311 
(*val tenth_ax = fst( Array.sub(clause_arr, 1)) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

312 
val tenth_ax_thms = Recon_Transfer.memo_find_clause (tenth_ax, clause_tab) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

313 
val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

314 
val _ = (warning ("tenth axiom in array is: "^tenth_ax)) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

315 
val _ = (warning ("tenth axiom in table is: "^clause_str)) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

316 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

317 
val _ = (warning ("num_of_clauses is: "^(string_of_int (num_of_clauses))) ) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

318 
*) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

319 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

320 
val (childin,childout,pid) = Watcher.createWatcher(thm,clause_arr, num_of_clauses) 
15644  321 
val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid ))) 
15608  322 
in 
15644  323 
case prems of [] => () 
324 
 _ => ((warning ("initial thms: "^thms_string)); 

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

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

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

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

16357  329 
(warning("turning xsymbol back on!")); 
15644  330 
print_mode := (["xsymbols", "symbols"] @ ! print_mode) 
15608  331 
end; 
332 

15452  333 

15608  334 

335 

336 
local 

337 

338 
fun get_thms_cs claset = 

339 
let val clsset = rep_cs claset 

340 
val safeEs = #safeEs clsset 

341 
val safeIs = #safeIs clsset 

342 
val hazEs = #hazEs clsset 

343 
val hazIs = #hazIs clsset 

344 
in 

345 
safeEs @ safeIs @ hazEs @ hazIs 

346 
end; 

347 

16357  348 

349 

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

352 

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

354 
let val thms' = append_name name thms 0 

355 
in 

356 
thms'::(append_names names thmss) 

357 
end; 

358 

16357  359 

15608  360 
fun get_thms_ss [] = [] 
361 
 get_thms_ss thms = 

362 
let val names = map Thm.name_of_thm thms 

363 
val thms' = map (mksimps mksimps_pairs) thms 

364 
val thms'' = append_names names thms' 

365 
in 

366 
ResLib.flat_noDup thms'' 

367 
end; 

368 

16357  369 

370 

371 

15608  372 
in 
373 

15452  374 

15608  375 
(* convert locally declared rules to axiom clauses *) 
376 
(* write axiom clauses to ax_file *) 

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

379 
(*claset file and prob file*) 

16357  380 
(* FIX*) 
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

381 
(*fun isar_local_thms (delta_cs, delta_ss_thms) = 
15608  382 
let val thms_cs = get_thms_cs delta_cs 
383 
val thms_ss = get_thms_ss delta_ss_thms 

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

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

16259  386 
val ax_file = File.platform_path axiom_file 
15608  387 
val out = TextIO.openOut ax_file 
388 
in 

15644  389 
(ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out) 
15608  390 
end; 
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

391 
*) 
15608  392 

393 

16357  394 

395 

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

397 

15608  398 
fun isar_atp (ctxt,thm) = 
399 
let val prems = ProofContext.prems_of ctxt 

15644  400 
val d_cs = Classical.get_delta_claset ctxt 
401 
val d_ss_thms = Simplifier.get_delta_simpset ctxt 

402 
val thmstring = string_of_thm thm 

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

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

405 
val prem_no = length sg_prems 
15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

406 
val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems) 
15608  407 
in 
15644  408 
(warning ("initial thm in isar_atp: "^thmstring)); 
409 
(warning ("subgoals in isar_atp: "^prems_string)); 

15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

410 
(warning ("number of subgoals in isar_atp: "^(string_of_int prem_no))); 
16357  411 
(*isar_local_thms (d_cs,d_ss_thms);*) 
412 
isar_atp' (ctxt,prems, thm) 

15608  413 
end; 
15347  414 

15608  415 
end 
416 

417 

16357  418 

419 

15347  420 
end; 
421 

422 
Proof.atp_hook := ResAtp.isar_atp; 