author  quigley 
Mon, 11 Jul 2005 16:42:42 +0200  
changeset 16767  2d4433759b8d 
parent 16741  7a6c17b826c0 
child 16802  6eeee59dac4c 
permissions  rwrr 
15608  1 
(* Author: Jia Meng, Cambridge University Computer Laboratory 
16520  2 

15608  3 
ID: $Id$ 
16520  4 

15608  5 
Copyright 2004 University of Cambridge 
15347  6 

7 
ATPs with TPTP format input. 

8 
*) 

15452  9 

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

15644  11 
(*Claire: changed: added actual watcher calls *) 
15452  12 

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

13 

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

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

18 
val traceflag : bool ref 
15608  19 
val axiom_file : Path.T 
20 
val hyps_file : Path.T 

21 
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

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

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

26 
val full_spass: bool ref 
16478  27 
(*val spass: bool ref*) 
28 
val vampire: bool ref 

16520  29 
val custom_spass :string list ref 
15347  30 
end; 
31 

32 
structure ResAtp : RES_ATP = 

15608  33 

15347  34 
struct 
35 

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

36 
val subgoals = []; 
15644  37 

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

38 
val traceflag = ref true; 
16357  39 
(* used for debug *) 
40 
val debug = ref false; 

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

41 

15608  42 
fun debug_tac tac = (warning "testing";tac); 
16357  43 
(* default value is false *) 
16478  44 

16357  45 
val full_spass = ref false; 
16478  46 

47 
(* use spass as default prover *) 

48 
(*val spass = ref true;*) 

49 

16520  50 
val custom_spass = ref ["Auto=0","IORe","IOFc","RTaut","RFSub","RBSub","DocProof","TimeLimit=60"]; 
16478  51 
val vampire = ref false; 
52 

15608  53 
val trace_res = ref false; 
15347  54 

15608  55 
val skolem_tac = skolemize_tac; 
56 

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

59 

15347  60 

15608  61 
val atomize_tac = 
62 
SUBGOAL 

63 
(fn (prop,_) => 

64 
let val ts = Logic.strip_assums_hyp prop 

65 
in EVERY1 

66 
[METAHYPS 

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

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

69 
end); 

15347  70 

15608  71 
(* temporarily use these files, which will be loaded by Vampire *) 
15644  72 
val file_id_num =ref 0; 
15608  73 

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

15347  76 

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

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

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

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

82 

83 

15347  84 
(**** for Isabelle/ML interface ****) 
85 

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

16357  88 
fun proofstring x = let val exp = explode x 
89 
in 

90 
List.filter (is_proof_char ) exp 

91 
end 

92 

15608  93 

15452  94 

15644  95 
(* 
96 
fun call_atp_tac thms n = (tptp_inputs thms ; dummy_tac); 

15347  97 

15644  98 
*) 
15347  99 

100 
(**** For running in Isar ****) 

101 

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

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

105 
in 

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

107 
end; 

108 

109 
(* a special version of repeat_RS *) 

110 
fun repeat_someI_ex thm = repeat_RS thm someI_ex; 

111 

15644  112 
(*********************************************************************) 
15608  113 
(* convert clauses from "assume" to conjecture. write to file "hyps" *) 
15644  114 
(* hypotheses of the goal currently being proved *) 
115 
(*********************************************************************) 

16767  116 
(*perhaps have 2 different versions of this, depending on whether or not SpassComm.spass is set *) 
15608  117 
fun isar_atp_h thms = 
15644  118 

15608  119 
let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms 
15644  120 
val prems' = map repeat_someI_ex prems 
121 
val prems'' = make_clauses prems' 

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

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

15774  124 
val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
15608  125 
val tfree_lits = ResLib.flat_noDup tfree_litss 
16767  126 
(* tfree clause is different in tptp and dfg versions *) 
15608  127 
val tfree_clss = map ResClause.tfree_clause tfree_lits 
16259  128 
val hypsfile = File.platform_path hyps_file 
15608  129 
val out = TextIO.openOut(hypsfile) 
130 
in 

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

132 
end; 

15347  133 

15644  134 

135 
(*********************************************************************) 

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

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

138 
(*********************************************************************) 

139 

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

141 
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

142 
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

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

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

147 
val _ = (warning ("in tptp_inputs_tfrees 3")) 
16259  148 
val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) 
15608  149 
val out = TextIO.openOut(probfile) 
150 
in 

16357  151 
(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ())) 
15608  152 
end; 
15452  153 

15608  154 

16767  155 
(*********************************************************************) 
156 
(* write out a subgoal as DFG clauses to the file "probN" *) 

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

158 
(*********************************************************************) 

159 
(* 

160 
fun dfg_inputs_tfrees thms n tfrees = 

161 
let val _ = (warning ("in dfg_inputs_tfrees 0")) 

162 
val clss = map (ResClause.make_conjecture_clause_thm) thms 

163 
val _ = (warning ("in dfg_inputs_tfrees 1")) 

164 
val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss) 

165 
val _ = (warning ("in dfg_inputs_tfrees 2")) 

166 
val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 

167 
val _ = (warning ("in dfg_inputs_tfrees 3")) 

168 
val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) 

169 
val out = TextIO.openOut(probfile) 

170 
in 

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

172 
end;*) 

16357  173 

15644  174 
(*********************************************************************) 
175 
(* call SPASS with settings and problem file for the current subgoal *) 

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

177 
(*********************************************************************) 

16357  178 
(* now passing in list of skolemized thms and list of sgterms to go with them *) 
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

179 
fun call_resolve_tac (thms: Thm.thm list list) sign (sg_terms: Term.term list) (childin, childout,pid) n = 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

180 
let 
16357  181 
val axfile = (File.platform_path axiom_file) 
16520  182 

183 
val hypsfile = (File.platform_path hyps_file) 

184 
val clasimpfile = (File.platform_path clasimp_file) 

185 
val spass_home = getenv "SPASS_HOME" 

186 

187 

16475  188 
fun make_atp_list [] sign n = [] 
189 
 make_atp_list ((sko_thm, sg_term)::xs) sign n = 

16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

190 
let 
16520  191 

16357  192 
val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm) 
193 
val thmproofstr = proofstring ( skothmstr) 

194 
val no_returns =List.filter not_newline ( thmproofstr) 

195 
val thmstr = implode no_returns 

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

15608  197 

16357  198 
val sgstr = Sign.string_of_term sign sg_term 
199 
val goalproofstring = proofstring sgstr 

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

200 
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

201 
val goalstring = implode no_returns 
16357  202 
val _ = warning ("goalstring in make_atp_lists is: "^goalstring) 
203 

16259  204 
val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) 
16520  205 

16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

206 
val _ = (warning ("prob file in cal_res_tac is: "^probfile)) 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

207 
in 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

208 
if !SpassComm.spass 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

209 
then 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

210 
let val _ = ResLib.helper_path "SPASS_HOME" "SPASS" 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

211 
in (*We've checked that SPASS is there for ATP/spassshell to run.*) 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

212 
if !full_spass 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

213 
then (*Allow SPASS to run in Auto mode, using all its inference rules*) 
16520  214 

16357  215 
([("spass", thmstr, goalstring (*,spass_home*), 
16520  216 

217 
getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*), 

218 
"DocProof%TimeLimit=60%SOS", 

219 

16357  220 
clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) 
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

221 
else (*Restrict SPASS to a small set of rules that we can parse*) 
16357  222 
([("spass", thmstr, goalstring (*,spass_home*), 
223 
getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*), 

16520  224 
("" ^ space_implode "%" (!custom_spass)), 
16478  225 
clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) 
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

226 
end 
16478  227 
else 
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

228 
let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel" 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

229 
in 
16675  230 
([("vampire", thmstr, goalstring, vampire, "t 60%m 100000", 
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

231 
clasimpfile, axfile, hypsfile, probfile)] @ 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

232 
(make_atp_list xs sign (n+1))) 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

233 
end 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

234 
end 
15452  235 

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

238 
in 

239 
Watcher.callResProvers(childout,atp_list); 

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

241 
dummy_tac 

242 
end 

243 

15644  244 
(**********************************************************) 
245 
(* write out the current subgoal as a tptp file, probN, *) 

246 
(* then call dummy_tac  should be call_res_tac *) 

247 
(**********************************************************) 

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

248 

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

249 

16357  250 
fun get_sko_thms tfrees sign sg_terms (childin, childout,pid) thm n sko_thms = 
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

251 
if n=0 then 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

252 
(call_resolve_tac (rev sko_thms) sign sg_terms (childin, childout, pid) (List.length sg_terms);dummy_tac thm) 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

253 
else 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

254 

7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

255 
( SELECT_GOAL 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

256 
(EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

257 
METAHYPS(fn negs => (tptp_inputs_tfrees (make_clauses negs) n tfrees; 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

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

260 

261 

262 
(**********************************************) 

263 
(* recursively call atp_tac_g on all subgoals *) 

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

265 
(* in proof reconstruction *) 

266 
(**********************************************) 

267 

16357  268 
fun isar_atp_goal' thm n tfree_lits (childin, childout, pid) = 
16515
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

269 
let val prems = prems_of thm 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

270 
(*val sg_term = get_nth k prems*) 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

271 
val sign = sign_of_thm thm 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

272 
val thmstring = string_of_thm thm 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

273 
in 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

274 
warning("in isar_atp_goal'"); 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

275 
warning("thmstring in isar_atp_goal': "^thmstring); 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

276 
(* go and call callResProvers with this subgoal *) 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

277 
(* isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm; *) 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

278 
(* recursive call to pick up the remaining subgoals *) 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

279 
(* isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid) *) 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

280 
get_sko_thms tfree_lits sign prems (childin, childout, pid) thm n [] 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
paulson
parents:
16478
diff
changeset

281 
end ; 
15644  282 

16520  283 

15644  284 

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

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

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

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

289 
(* statements; *) 
15644  290 
(* write to file "hyps" *) 
291 
(**************************************************) 

292 

293 

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

15608  295 
let val tfree_lits = isar_atp_h thms 
16357  296 
in 
297 
(warning("in isar_atp_aux")); 

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

15608  299 
end; 
15644  300 

301 
(******************************************************************) 

302 
(* called in Isar automatically *) 

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

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

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

306 
(******************************************************************) 

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

307 
(*FIX changed to clasimp_file *) 
16357  308 
fun isar_atp' (ctxt,thms, thm) = 
16741
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

309 
if null (prems_of thm) then () 
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

310 
else 
16357  311 
let 
16741
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

312 
val _= (print_mode := (Library.gen_rems (op =) 
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

313 
(! print_mode, ["xsymbols", "symbols"]))) 
15644  314 
val _= (warning ("in isar_atp'")) 
16741
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

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

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

319 
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

320 

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

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

322 
val (clause_arr, num_of_clauses) = 
16741
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

323 
ResClasimp.write_out_clasimp (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

324 
(ProofContext.theory_of ctxt) 
16741
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

325 
(hd prems) (*FIXME: hack!! need to do all prems*) 
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

326 
val _ = warning ("clasimp_file is " ^ File.platform_path clasimp_file) 
15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

327 
val (childin,childout,pid) = Watcher.createWatcher(thm,clause_arr, num_of_clauses) 
16741
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

328 
val pidstring = string_of_int(Word.toInt 
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

329 
(Word.fromLargeWord ( Posix.Process.pidToWord pid ))) 
15608  330 
in 
16741
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

331 
warning ("initial thms: "^thms_string); 
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

332 
warning ("initial thm: "^thmstring); 
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

333 
warning ("subgoals: "^prems_string); 
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

334 
warning ("pid: "^ pidstring); 
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

335 
isar_atp_aux thms thm (length prems) (childin, childout, pid); 
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

336 
warning("turning xsymbol back on!"); 
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

337 
print_mode := (["xsymbols", "symbols"] @ ! print_mode) 
15608  338 
end; 
339 

15452  340 

15608  341 

342 

343 
local 

344 

345 
fun get_thms_cs claset = 

346 
let val clsset = rep_cs claset 

347 
val safeEs = #safeEs clsset 

348 
val safeIs = #safeIs clsset 

349 
val hazEs = #hazEs clsset 

350 
val hazIs = #hazIs clsset 

351 
in 

352 
safeEs @ safeIs @ hazEs @ hazIs 

353 
end; 

354 

16357  355 

356 

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

359 

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

361 
let val thms' = append_name name thms 0 

362 
in 

363 
thms'::(append_names names thmss) 

364 
end; 

365 

16357  366 

15608  367 
fun get_thms_ss [] = [] 
368 
 get_thms_ss thms = 

369 
let val names = map Thm.name_of_thm thms 

370 
val thms' = map (mksimps mksimps_pairs) thms 

371 
val thms'' = append_names names thms' 

372 
in 

373 
ResLib.flat_noDup thms'' 

374 
end; 

375 

16357  376 

377 

378 

15608  379 
in 
380 

15452  381 

15608  382 
(* convert locally declared rules to axiom clauses *) 
383 
(* write axiom clauses to ax_file *) 

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

386 
(*claset file and prob file*) 

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

388 
(*fun isar_local_thms (delta_cs, delta_ss_thms) = 
15608  389 
let val thms_cs = get_thms_cs delta_cs 
390 
val thms_ss = get_thms_ss delta_ss_thms 

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

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

16259  393 
val ax_file = File.platform_path axiom_file 
15608  394 
val out = TextIO.openOut ax_file 
395 
in 

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

398 
*) 
15608  399 

400 

16357  401 

402 

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

404 

15608  405 
fun isar_atp (ctxt,thm) = 
406 
let val prems = ProofContext.prems_of ctxt 

15644  407 
val d_cs = Classical.get_delta_claset ctxt 
408 
val d_ss_thms = Simplifier.get_delta_simpset ctxt 

409 
val thmstring = string_of_thm thm 

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

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

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

413 
val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems) 
15608  414 
in 
15644  415 
(warning ("initial thm in isar_atp: "^thmstring)); 
416 
(warning ("subgoals in isar_atp: "^prems_string)); 

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

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

15608  420 
end; 
15347  421 

15608  422 
end 
423 

424 

16357  425 

426 

15347  427 
end; 
428 

429 
Proof.atp_hook := ResAtp.isar_atp; 