author  quigley 
Thu, 02 Jun 2005 15:54:11 +0200  
changeset 16185  bb71c91e781e 
parent 16172  629ba53a072f 
child 16259  aed1a8ae4b23 
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 = 
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 
15347  25 
end; 
26 

27 
structure ResAtp : RES_ATP = 

15608  28 

15347  29 
struct 
30 

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

31 
val subgoals = []; 
15644  32 

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

33 
val traceflag = ref true; 
16172
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

34 

15608  35 
val debug = ref false; 
36 
fun debug_tac tac = (warning "testing";tac); 

15347  37 

15608  38 
val trace_res = ref false; 
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16089
diff
changeset

39 
val full_spass = ref false; 
15347  40 

15608  41 
val skolem_tac = skolemize_tac; 
42 

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

45 

15347  46 

15608  47 
val atomize_tac = 
48 
SUBGOAL 

49 
(fn (prop,_) => 

50 
let val ts = Logic.strip_assums_hyp prop 

51 
in EVERY1 

52 
[METAHYPS 

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

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

55 
end); 

15347  56 

15608  57 
(* temporarily use these files, which will be loaded by Vampire *) 
15644  58 
val file_id_num =ref 0; 
15608  59 

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

15347  62 

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

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

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

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

68 

69 

15347  70 
(**** for Isabelle/ML interface ****) 
71 

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

72 
fun is_proof_char ch = (ch = " ") orelse 
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

73 
((ord"!" <= ord ch) andalso (ord ch <= ord"~") andalso (ch <> "?")) 
15608  74 

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

75 
fun proofstring x = List.filter (is_proof_char) (explode x); 
15608  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 

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

133 
(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; 
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

134 
if !trace_res then (warning probfile) else ()) 
15608  135 
end; 
15452  136 

15608  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 

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

143 
fun call_resolve_tac sign thms sg_term (childin, childout,pid) n = 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

144 
let val thmstring = Meson.concat_with_and (map string_of_thm thms) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

145 
val thm_no = length thms 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

146 
val _ = warning ("number of thms is : "^(string_of_int thm_no)) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

147 
val _ = warning ("thmstring in call_res is: "^thmstring) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

148 

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

149 
val goalstr = Sign.string_of_term sign sg_term 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

150 
val goalproofstring = proofstring goalstr 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

151 
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

152 
val goalstring = implode no_returns 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

153 
val _ = warning ("goalstring in call_res is: "^goalstring) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

154 

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

155 
(*val prob_file =File.tmp_path (Path.basic newprobfile); *) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

156 
(*val _ =( warning ("calling make_clauses ")) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

157 
val clauses = make_clauses thms 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

158 
val _ =( warning ("called make_clauses "))*) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

159 
(*val _ = tptp_inputs clauses prob_file*) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

160 
val thmstring = Meson.concat_with_and (map string_of_thm thms) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

161 

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

162 
val goalstr = Sign.string_of_term sign sg_term 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

163 
val goalproofstring = proofstring goalstr 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

164 
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

165 
val goalstring = implode no_returns 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

166 

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

167 
val thmproofstring = proofstring ( thmstring) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

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

169 
val thmstr = implode no_returns 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

170 

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

171 
val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

172 
val axfile = (File.sysify_path axiom_file) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

173 
val hypsfile = (File.sysify_path hyps_file) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

174 
val clasimpfile = (File.sysify_path clasimp_file) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

175 
val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "hellofile"))) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

176 
val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring); 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

177 
val _ = TextIO.flushOut outfile; 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

178 
val _ = TextIO.closeOut outfile 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

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

180 
(* without paramodulation *) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

181 
(warning ("goalstring in call_res_tac is: "^goalstring)); 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

182 
(warning ("prob file in cal_res_tac is: "^probfile)); 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

183 
(* Watcher.callResProvers(childout, 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

184 
[("spass",thmstr,goalstring,*spass_home*, 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

185 
"DocProof", 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

186 
clasimpfile, axfile, hypsfile, probfile)]);*) 
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16089
diff
changeset

187 
if !full_spass 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16089
diff
changeset

188 
then 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16089
diff
changeset

189 
(Watcher.callResProvers(childout, 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16089
diff
changeset

190 
[("spass", thmstr, goalstring (*,spass_home*), 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16089
diff
changeset

191 
getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell", 
16185  192 
"DocProof%TimeLimit=60", 
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16089
diff
changeset

193 
clasimpfile, axfile, hypsfile, probfile)])) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16089
diff
changeset

194 
else 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16089
diff
changeset

195 
(Watcher.callResProvers(childout, 
16089
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

196 
[("spass", thmstr, goalstring (*,spass_home*), 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

197 
getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell", 
16185  198 
"Auto=0%ISRe%ISFc%RTaut%RFSub%RBSub%DocProof%TimeLimit=60", 
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16089
diff
changeset

199 
clasimpfile, axfile, hypsfile, probfile)])); 
16089
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

200 

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

201 
(* with paramodulation *) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

202 
(*Watcher.callResProvers(childout, 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

203 
[("spass",thmstr,goalstring,spass_home, 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

204 
"FullRed=0%ISPm=1%Split=0%PObv=0%DocProof", 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

205 
prob_path)]); *) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

206 
(* Watcher.callResProvers(childout, 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

207 
[("spass",thmstr,goalstring,spass_home, 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

208 
"DocProof", prob_path)]);*) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

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

210 
end 
15452  211 

15644  212 
(**********************************************************) 
213 
(* write out the current subgoal as a tptp file, probN, *) 

214 
(* then call dummy_tac  should be call_res_tac *) 

215 
(**********************************************************) 

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

216 

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

217 

15697  218 
fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) = 
16172
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

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

220 
warning("in call_atp_tac_tfrees"); 
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

221 
tptp_inputs_tfrees (make_clauses thms) n tfrees; 
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

222 
call_resolve_tac sign thms sg_term (childin, childout, pid) n; 
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

223 
dummy_tac); 
15644  224 

15697  225 
fun atp_tac_tfrees tfrees sg_term (childin, childout,pid) n st = 
16172
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

226 
let val sign = sign_of_thm st 
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

227 
val _ = warning ("in atp_tac_tfrees ") 
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

228 
val _ = warning ("sg_term :" ^ (Sign.string_of_term sign sg_term)) 
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

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

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

231 
(EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

232 
METAHYPS(fn negs => (call_atp_tac_tfrees sign negs n tfrees sg_term 
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

233 
(childin, childout,pid) ))]) n st 
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

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

235 

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

236 

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

237 
fun isar_atp_g tfrees sg_term (childin, childout, pid) n = 
16172
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

238 
((warning("in isar_atp_g")); 
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

239 
atp_tac_tfrees tfrees sg_term (childin, childout, pid) n); 
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 

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

16061  250 
if (k > n) 
251 
then () 

252 
else 

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

253 
let val prems = prems_of thm 
16061  254 
val sg_term = ReconOrderClauses.get_nth n prems 
255 
val thmstring = string_of_thm thm 

256 
in 

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

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

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

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

261 
end; 

15644  262 

263 

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

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

265 
(if (!debug) then warning (string_of_thm thm) 
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

266 
else (isar_atp_goal' thm 1 n_subgoals tfree_lits (childin, childout, pid) )); 
15644  267 

268 
(**************************************************) 

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

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

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

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

275 

276 

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

15608  278 
let val tfree_lits = isar_atp_h thms 
16172
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

279 
in warning("in isar_atp_aux"); 
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

280 
isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid) 
15608  281 
end; 
15644  282 

283 
(******************************************************************) 

284 
(* called in Isar automatically *) 

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

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

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

288 
(******************************************************************) 

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

289 
(*FIX changed to clasimp_file *) 
16172
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

290 
fun isar_atp' (ctxt, thms, thm) = 
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

291 
let val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) 
15644  292 
val _= (warning ("in isar_atp'")) 
15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

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

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

297 
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

298 

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

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

300 
val (clause_arr, num_of_clauses) = 
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

301 
ResClasimp.write_out_clasimp (File.sysify_path clasimp_file) 
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

302 
(ProofContext.theory_of ctxt) 
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

303 
val _ = warning ("clasimp_file is " ^ File.sysify_path clasimp_file) 
15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

304 

15644  305 
(* cq: add write out clasimps to file *) 
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

306 

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

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

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

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

310 
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

311 
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

312 
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

313 
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

314 

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

315 
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

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

317 

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

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

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

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

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

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

327 

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

15608  329 
end; 
330 

15452  331 

15608  332 

333 

334 
local 

335 

336 
fun get_thms_cs claset = 

337 
let val clsset = rep_cs claset 

338 
val safeEs = #safeEs clsset 

339 
val safeIs = #safeIs clsset 

340 
val hazEs = #hazEs clsset 

341 
val hazIs = #hazIs clsset 

342 
in 

343 
safeEs @ safeIs @ hazEs @ hazIs 

344 
end; 

345 

346 
fun append_name name [] _ = [] 

347 
 append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1)); 

348 

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

350 
let val thms' = append_name name thms 0 

351 
in 

352 
thms'::(append_names names thmss) 

353 
end; 

354 

355 
fun get_thms_ss [] = [] 

356 
 get_thms_ss thms = 

357 
let val names = map Thm.name_of_thm thms 

358 
val thms' = map (mksimps mksimps_pairs) thms 

359 
val thms'' = append_names names thms' 

360 
in 

361 
ResLib.flat_noDup thms'' 

362 
end; 

363 

364 
in 

365 

15452  366 

15608  367 
(* convert locally declared rules to axiom clauses *) 
368 
(* write axiom clauses to ax_file *) 

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

371 
(*claset file and prob file*) 

16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

372 
(* FIX: update to work with clausify_axiom_pairs now in ResAxioms*) 
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

373 
(*fun isar_local_thms (delta_cs, delta_ss_thms) = 
15608  374 
let val thms_cs = get_thms_cs delta_cs 
375 
val thms_ss = get_thms_ss delta_ss_thms 

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

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

378 
val ax_file = File.sysify_path axiom_file 

379 
val out = TextIO.openOut ax_file 

380 
in 

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

383 
*) 
15608  384 

385 

386 
(* called in Isar automatically *) 

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

387 

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

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

392 
val thmstring = string_of_thm thm 

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

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

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

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

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

400 
(warning ("number of subgoals in isar_atp: "^(string_of_int prem_no))); 
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

401 
((*isar_local_thms (d_cs,d_ss_thms); *)(warning("about to call isar_atp'")); 
16172
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

402 
isar_atp' (ctxt, prems, thm)) 
15608  403 
end; 
15347  404 

15608  405 
end 
406 

407 

15347  408 
end; 
409 

410 
Proof.atp_hook := ResAtp.isar_atp; 