author  paulson 
Thu, 07 Jul 2005 18:25:02 +0200  
changeset 16741  7a6c17b826c0 
parent 16675  96bdc59afc05 
child 16767  2d4433759b8d 
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 
(*********************************************************************) 

116 

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 
126 
val tfree_clss = map ResClause.tfree_clause tfree_lits 

16259  127 
val hypsfile = File.platform_path hyps_file 
15608  128 
val out = TextIO.openOut(hypsfile) 
129 
in 

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

131 
end; 

15347  132 

15644  133 

134 
(*********************************************************************) 

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

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

137 
(*********************************************************************) 

138 

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

140 
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

141 
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

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

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

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

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

15608  153 

16357  154 

15644  155 
(*********************************************************************) 
156 
(* call SPASS with settings and problem file for the current subgoal *) 

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

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

16357  159 
(* 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

160 
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

161 
let 
16357  162 
val axfile = (File.platform_path axiom_file) 
16520  163 

164 
val hypsfile = (File.platform_path hyps_file) 

165 
val clasimpfile = (File.platform_path clasimp_file) 

166 
val spass_home = getenv "SPASS_HOME" 

167 

168 

16475  169 
fun make_atp_list [] sign n = [] 
170 
 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

171 
let 
16520  172 

16357  173 
val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm) 
174 
val thmproofstr = proofstring ( skothmstr) 

175 
val no_returns =List.filter not_newline ( thmproofstr) 

176 
val thmstr = implode no_returns 

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

15608  178 

16357  179 
val sgstr = Sign.string_of_term sign sg_term 
180 
val goalproofstring = proofstring sgstr 

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

181 
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

182 
val goalstring = implode no_returns 
16357  183 
val _ = warning ("goalstring in make_atp_lists is: "^goalstring) 
184 

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

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

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

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

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

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

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

192 
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

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

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

16357  196 
([("spass", thmstr, goalstring (*,spass_home*), 
16520  197 

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

199 
"DocProof%TimeLimit=60%SOS", 

200 

16357  201 
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

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

16520  205 
("" ^ space_implode "%" (!custom_spass)), 
16478  206 
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

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

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

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

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

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

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

215 
end 
15452  216 

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

219 
in 

220 
Watcher.callResProvers(childout,atp_list); 

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

222 
dummy_tac 

223 
end 

224 

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

227 
(* then call dummy_tac  should be call_res_tac *) 

228 
(**********************************************************) 

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

229 

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

230 

16357  231 
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

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

233 
(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

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

235 

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

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

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

238 
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

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

241 

242 

243 
(**********************************************) 

244 
(* recursively call atp_tac_g on all subgoals *) 

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

246 
(* in proof reconstruction *) 

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

248 

16357  249 
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

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

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

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

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

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

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

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

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

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

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

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

261 
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

262 
end ; 
15644  263 

16520  264 

15644  265 

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

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

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

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

270 
(* statements; *) 
15644  271 
(* write to file "hyps" *) 
272 
(**************************************************) 

273 

274 

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

15608  276 
let val tfree_lits = isar_atp_h thms 
16357  277 
in 
278 
(warning("in isar_atp_aux")); 

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

15608  280 
end; 
15644  281 

282 
(******************************************************************) 

283 
(* called in Isar automatically *) 

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

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

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

287 
(******************************************************************) 

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

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

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

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

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

294 
(! print_mode, ["xsymbols", "symbols"]))) 
15644  295 
val _= (warning ("in isar_atp'")) 
16741
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
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) = 
16741
7a6c17b826c0
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16675
diff
changeset

304 
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

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

306 
(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

307 
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

308 
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

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

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

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

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

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

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

316 
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

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

318 
print_mode := (["xsymbols", "symbols"] @ ! print_mode) 
15608  319 
end; 
320 

15452  321 

15608  322 

323 

324 
local 

325 

326 
fun get_thms_cs claset = 

327 
let val clsset = rep_cs claset 

328 
val safeEs = #safeEs clsset 

329 
val safeIs = #safeIs clsset 

330 
val hazEs = #hazEs clsset 

331 
val hazIs = #hazIs clsset 

332 
in 

333 
safeEs @ safeIs @ hazEs @ hazIs 

334 
end; 

335 

16357  336 

337 

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

340 

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

342 
let val thms' = append_name name thms 0 

343 
in 

344 
thms'::(append_names names thmss) 

345 
end; 

346 

16357  347 

15608  348 
fun get_thms_ss [] = [] 
349 
 get_thms_ss thms = 

350 
let val names = map Thm.name_of_thm thms 

351 
val thms' = map (mksimps mksimps_pairs) thms 

352 
val thms'' = append_names names thms' 

353 
in 

354 
ResLib.flat_noDup thms'' 

355 
end; 

356 

16357  357 

358 

359 

15608  360 
in 
361 

15452  362 

15608  363 
(* convert locally declared rules to axiom clauses *) 
364 
(* write axiom clauses to ax_file *) 

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

367 
(*claset file and prob file*) 

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

369 
(*fun isar_local_thms (delta_cs, delta_ss_thms) = 
15608  370 
let val thms_cs = get_thms_cs delta_cs 
371 
val thms_ss = get_thms_ss delta_ss_thms 

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

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

16259  374 
val ax_file = File.platform_path axiom_file 
15608  375 
val out = TextIO.openOut ax_file 
376 
in 

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

379 
*) 
15608  380 

381 

16357  382 

383 

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

385 

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

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

390 
val thmstring = string_of_thm thm 

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

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

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

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

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

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

15608  401 
end; 
15347  402 

15608  403 
end 
404 

405 

16357  406 

407 

15347  408 
end; 
409 

410 
Proof.atp_hook := ResAtp.isar_atp; 