author  paulson 
Thu, 11 Oct 2007 15:59:31 +0200  
changeset 24958  ff15f76741bd 
parent 24920  2a45e400fdad 
child 25006  fcf5a999d1c3 
permissions  rwrr 
19194  1 
(* Author: Jia Meng, Cambridge University Computer Laboratory, NICTA 
15608  2 
ID: $Id$ 
3 
Copyright 2004 University of Cambridge 

15347  4 

5 
ATPs with TPTP format input. 

6 
*) 

15452  7 

16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

8 
signature RES_ATP = 
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

9 
sig 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

10 
val prover: ResReconstruct.atp ref 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

11 
val destdir: string ref 
17849  12 
val helper_path: string > string > string 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

13 
val problem_name: string ref 
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17525
diff
changeset

14 
val time_limit: int ref 
21224  15 
val set_prover: string > unit 
21588  16 

19194  17 
datatype mode = Auto  Fol  Hol 
19450
651d949776f8
exported linkup_logic_mode and changed the default setting
paulson
parents:
19445
diff
changeset

18 
val linkup_logic_mode : mode ref 
19722  19 
val write_subgoal_file: bool > mode > Proof.context > thm list > thm list > int > string 
19194  20 
val cond_rm_tmp: string > unit 
20246
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

21 
val include_all: bool ref 
19194  22 
val run_relevance_filter: bool ref 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

23 
val run_blacklist_filter: bool ref 
24287  24 
val theory_const : bool ref 
25 
val pass_mark : real ref 

26 
val convergence : real ref 

27 
val max_new : int ref 

28 
val follow_defs : bool ref 

19894  29 
val add_all : unit > unit 
19227
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

30 
val add_claset : unit > unit 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

31 
val add_simpset : unit > unit 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

32 
val add_clasimp : unit > unit 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

33 
val add_atpset : unit > unit 
19894  34 
val rm_all : unit > unit 
19227
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

35 
val rm_claset : unit > unit 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

36 
val rm_simpset : unit > unit 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

37 
val rm_atpset : unit > unit 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

38 
val rm_clasimp : unit > unit 
22989  39 
val tvar_classes_of_terms : term list > string list 
40 
val tfree_classes_of_terms : term list > string list 

41 
val type_consts_of_terms : theory > term list > string list 

15347  42 
end; 
43 

22865  44 
structure ResAtp: RES_ATP = 
15347  45 
struct 
46 

24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

47 
structure Recon = ResReconstruct; 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

48 

22130  49 
fun timestamp s = Output.debug (fn () => ("At " ^ Time.toString (Time.now()) ^ ": " ^ s)); 
21070  50 

19194  51 
(********************************************************************) 
52 
(* some settings for both background automatic ATP calling procedure*) 

53 
(* and also explicit ATP invocation methods *) 

54 
(********************************************************************) 

55 

56 
(*** background linkup ***) 

24287  57 
val run_blacklist_filter = ref true; 
21224  58 
val time_limit = ref 60; 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

59 
val prover = ref Recon.E; 
21224  60 

24287  61 
(*** relevance filter parameters ***) 
62 
val run_relevance_filter = ref true; 

63 
val theory_const = ref true; 

64 
val pass_mark = ref 0.5; 

65 
val convergence = ref 3.2; (*Higher numbers allow longer inference chains*) 

66 
val max_new = ref 60; (*Limits how many clauses can be picked up per stage*) 

67 
val follow_defs = ref false; (*Follow definitions. Makes problems bigger.*) 

68 

21588  69 
fun set_prover atp = 
21224  70 
case String.map Char.toLower atp of 
21588  71 
"e" => 
24287  72 
(max_new := 100; 
73 
theory_const := false; 

24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

74 
prover := Recon.E) 
21588  75 
 "spass" => 
24287  76 
(max_new := 40; 
77 
theory_const := true; 

24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

78 
prover := Recon.SPASS) 
21588  79 
 "vampire" => 
24287  80 
(max_new := 60; 
81 
theory_const := false; 

24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

82 
prover := Recon.Vampire) 
21224  83 
 _ => error ("No such prover: " ^ atp); 
84 

85 
val _ = set_prover "E"; (* use E as the default prover *) 

86 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

87 
val destdir = ref ""; (*Empty means write files to /tmp*) 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

88 
val problem_name = ref "prob"; 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

89 

17819  90 
(*Return the path to a "helper" like SPASS or tptp2X, first checking that 
21588  91 
it exists. FIXME: modify to use Path primitives and move to some central place.*) 
17819  92 
fun helper_path evar base = 
93 
case getenv evar of 

94 
"" => error ("Isabelle environment variable " ^ evar ^ " not defined") 

21588  95 
 home => 
17819  96 
let val path = home ^ "/" ^ base 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21790
diff
changeset

97 
in if File.exists (File.explode_platform_path path) then path 
21588  98 
else error ("Could not find the file " ^ path) 
99 
end; 

17819  100 

21588  101 
fun probfile_nosuffix _ = 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

102 
if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name))) 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21790
diff
changeset

103 
else if File.exists (File.explode_platform_path (!destdir)) 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

104 
then !destdir ^ "/" ^ !problem_name 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

105 
else error ("No such directory: " ^ !destdir); 
15644  106 

17717  107 
fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n; 
108 

19194  109 
fun atp_input_file () = 
21588  110 
let val file = !problem_name 
19194  111 
in 
21588  112 
if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file)) 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21790
diff
changeset

113 
else if File.exists (File.explode_platform_path (!destdir)) 
21588  114 
then !destdir ^ "/" ^ file 
115 
else error ("No such directory: " ^ !destdir) 

19194  116 
end; 
117 

20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

118 
val include_all = ref true; 
19194  119 
val include_simpset = ref false; 
21588  120 
val include_claset = ref false; 
19194  121 
val include_atpset = ref true; 
20246
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

122 

fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

123 
(*Tests show that follow_defs gives VERY poor results with "include_all"*) 
24287  124 
fun add_all() = (include_all:=true; follow_defs := false); 
20246
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

125 
fun rm_all() = include_all:=false; 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

126 

fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

127 
fun add_simpset() = include_simpset:=true; 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

128 
fun rm_simpset() = include_simpset:=false; 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

129 

fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

130 
fun add_claset() = include_claset:=true; 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

131 
fun rm_claset() = include_claset:=false; 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

132 

fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

133 
fun add_clasimp() = (include_simpset:=true;include_claset:=true); 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

134 
fun rm_clasimp() = (include_simpset:=false;include_claset:=false); 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

135 

fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

136 
fun add_atpset() = include_atpset:=true; 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

137 
fun rm_atpset() = include_atpset:=false; 
19194  138 

24958  139 
fun strip_Trueprop (Const("Trueprop",_) $ t) = t 
140 
 strip_Trueprop t = t; 

19194  141 

21311  142 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

143 
(***************************************************************) 
24287  144 
(* Relevance Filtering *) 
145 
(***************************************************************) 

146 

147 
(*A surprising number of theorems contain only a few significant constants. 

148 
These include all induction rules, and other general theorems. Filtering 

149 
theorems in clause form reveals these complexities in the form of Skolem 

150 
functions. If we were instead to filter theorems in their natural form, 

151 
some other method of measuring theorem complexity would become necessary.*) 

152 

153 
fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0); 

154 

155 
(*The default seems best in practice. A constant function of one ignores 

156 
the constant frequencies.*) 

157 
val weight_fn = ref log_weight2; 

158 

159 

160 
(*Including equality in this list might be expected to stop rules like subset_antisym from 

161 
being chosen, but for some reason filtering works better with them listed. The 

162 
logical signs All, Ex, &, and > are omitted because any remaining occurrrences 

163 
must be within comprehensions.*) 

164 
val standard_consts = ["Trueprop","==>","all","==","op ","Not","op ="]; 

165 

166 

167 
(*** constants with types ***) 

168 

169 
(*An abstraction of Isabelle types*) 

170 
datatype const_typ = CTVar  CType of string * const_typ list 

171 

172 
(*Is the second type an instance of the first one?*) 

173 
fun match_type (CType(con1,args1)) (CType(con2,args2)) = 

174 
con1=con2 andalso match_types args1 args2 

175 
 match_type CTVar _ = true 

176 
 match_type _ CTVar = false 

177 
and match_types [] [] = true 

178 
 match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2; 

179 

180 
(*Is there a unifiable constant?*) 

181 
fun uni_mem gctab (c,c_typ) = 

182 
case Symtab.lookup gctab c of 

183 
NONE => false 

184 
 SOME ctyps_list => exists (match_types c_typ) ctyps_list; 

185 

186 
(*Maps a "real" type to a const_typ*) 

187 
fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 

188 
 const_typ_of (TFree _) = CTVar 

189 
 const_typ_of (TVar _) = CTVar 

190 

191 
(*Pairs a constant with the list of its type instantiations (using const_typ)*) 

192 
fun const_with_typ thy (c,typ) = 

193 
let val tvars = Sign.const_typargs thy (c,typ) 

194 
in (c, map const_typ_of tvars) end 

195 
handle TYPE _ => (c,[]); (*Variable (locale constant): monomorphic*) 

196 

197 
(*Add a const/type pair to the table, but a [] entry means a standard connective, 

198 
which we ignore.*) 

199 
fun add_const_typ_table ((c,ctyps), tab) = 

200 
Symtab.map_default (c, [ctyps]) (fn [] => []  ctyps_list => insert (op =) ctyps ctyps_list) 

201 
tab; 

202 

203 
(*Free variables are included, as well as constants, to handle locales*) 

204 
fun add_term_consts_typs_rm thy (Const(c, typ), tab) = 

205 
add_const_typ_table (const_with_typ thy (c,typ), tab) 

206 
 add_term_consts_typs_rm thy (Free(c, typ), tab) = 

207 
add_const_typ_table (const_with_typ thy (c,typ), tab) 

208 
 add_term_consts_typs_rm thy (t $ u, tab) = 

209 
add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab)) 

210 
 add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab) 

211 
 add_term_consts_typs_rm thy (_, tab) = tab; 

212 

213 
(*The empty list here indicates that the constant is being ignored*) 

214 
fun add_standard_const (s,tab) = Symtab.update (s,[]) tab; 

215 

216 
val null_const_tab : const_typ list list Symtab.table = 

217 
foldl add_standard_const Symtab.empty standard_consts; 

218 

219 
fun get_goal_consts_typs thy = foldl (add_term_consts_typs_rm thy) null_const_tab; 

220 

221 
(*Inserts a dummy "constant" referring to the theory name, so that relevance 

222 
takes the given theory into account.*) 

223 
fun const_prop_of th = 

224 
if !theory_const then 

225 
let val name = Context.theory_name (theory_of_thm th) 

226 
val t = Const (name ^ ". 1", HOLogic.boolT) 

227 
in t $ prop_of th end 

228 
else prop_of th; 

229 

230 
(**** Constant / Type Frequencies ****) 

231 

232 
(*A twodimensional symbol table counts frequencies of constants. It's keyed first by 

233 
constant name and second by its list of type instantiations. For the latter, we need 

234 
a linear ordering on type const_typ list.*) 

235 

236 
local 

237 

238 
fun cons_nr CTVar = 0 

239 
 cons_nr (CType _) = 1; 

240 

241 
in 

242 

243 
fun const_typ_ord TU = 

244 
case TU of 

245 
(CType (a, Ts), CType (b, Us)) => 

246 
(case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us)  ord => ord) 

247 
 (T, U) => int_ord (cons_nr T, cons_nr U); 

248 

249 
end; 

250 

251 
structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord); 

252 

253 
fun count_axiom_consts thy ((thm,_), tab) = 

254 
let fun count_const (a, T, tab) = 

255 
let val (c, cts) = const_with_typ thy (a,T) 

256 
in (*Twodimensional table update. Constant maps to types maps to count.*) 

257 
Symtab.map_default (c, CTtab.empty) 

258 
(CTtab.map_default (cts,0) (fn n => n+1)) tab 

259 
end 

260 
fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab) 

261 
 count_term_consts (Free(a,T), tab) = count_const(a,T,tab) 

262 
 count_term_consts (t $ u, tab) = 

263 
count_term_consts (t, count_term_consts (u, tab)) 

264 
 count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab) 

265 
 count_term_consts (_, tab) = tab 

266 
in count_term_consts (const_prop_of thm, tab) end; 

267 

268 

269 
(**** Actual Filtering Code ****) 

270 

271 
(*The frequency of a constant is the sum of those of all instances of its type.*) 

272 
fun const_frequency ctab (c, cts) = 

273 
let val pairs = CTtab.dest (the (Symtab.lookup ctab c)) 

274 
fun add ((cts',m), n) = if match_types cts cts' then m+n else n 

275 
in List.foldl add 0 pairs end; 

276 

277 
(*Add in a constant's weight, as determined by its frequency.*) 

278 
fun add_ct_weight ctab ((c,T), w) = 

279 
w + !weight_fn (real (const_frequency ctab (c,T))); 

280 

281 
(*Relevant constants are weighted according to frequency, 

282 
but irrelevant constants are simply counted. Otherwise, Skolem functions, 

283 
which are rare, would harm a clause's chances of being picked.*) 

284 
fun clause_weight ctab gctyps consts_typs = 

285 
let val rel = filter (uni_mem gctyps) consts_typs 

286 
val rel_weight = List.foldl (add_ct_weight ctab) 0.0 rel 

287 
in 

288 
rel_weight / (rel_weight + real (length consts_typs  length rel)) 

289 
end; 

290 

291 
(*Multiplies out to a list of pairs: 'a * 'b list > ('a * 'b) list > ('a * 'b) list*) 

292 
fun add_expand_pairs (x,ys) xys = foldl (fn (y,acc) => (x,y)::acc) xys ys; 

293 

294 
fun consts_typs_of_term thy t = 

295 
let val tab = add_term_consts_typs_rm thy (t, null_const_tab) 

296 
in Symtab.fold add_expand_pairs tab [] end; 

297 

298 
fun pair_consts_typs_axiom thy (thm,name) = 

299 
((thm,name), (consts_typs_of_term thy (const_prop_of thm))); 

300 

301 
exception ConstFree; 

302 
fun dest_ConstFree (Const aT) = aT 

303 
 dest_ConstFree (Free aT) = aT 

304 
 dest_ConstFree _ = raise ConstFree; 

305 

306 
(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*) 

307 
fun defines thy (thm,(name,n)) gctypes = 

308 
let val tm = prop_of thm 

309 
fun defs lhs rhs = 

310 
let val (rator,args) = strip_comb lhs 

311 
val ct = const_with_typ thy (dest_ConstFree rator) 

312 
in forall is_Var args andalso uni_mem gctypes ct andalso 

313 
Term.add_vars rhs [] subset Term.add_vars lhs [] 

314 
end 

315 
handle ConstFree => false 

316 
in 

317 
case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 

318 
defs lhs rhs andalso 

319 
(Output.debug (fn () => "Definition found: " ^ name ^ "_" ^ Int.toString n); true) 

320 
 _ => false 

321 
end; 

322 

323 
type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list); 

324 

325 
(*For a reverse sort, putting the largest values first.*) 

326 
fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1); 

327 

328 
(*Limit the number of new clauses, to prevent runaway acceptance.*) 

329 
fun take_best (newpairs : (annotd_cls*real) list) = 

330 
let val nnew = length newpairs 

331 
in 

332 
if nnew <= !max_new then (map #1 newpairs, []) 

333 
else 

334 
let val cls = sort compare_pairs newpairs 

335 
val accepted = List.take (cls, !max_new) 

336 
in 

337 
Output.debug (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 

338 
", exceeds the limit of " ^ Int.toString (!max_new))); 

339 
Output.debug (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted)))); 

340 
Output.debug (fn () => "Actually passed: " ^ 

341 
space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted)); 

342 

343 
(map #1 accepted, map #1 (List.drop (cls, !max_new))) 

344 
end 

345 
end; 

346 

347 
fun relevant_clauses thy ctab p rel_consts = 

348 
let fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*) 

349 
 relevant (newpairs,rejects) [] = 

350 
let val (newrels,more_rejects) = take_best newpairs 

351 
val new_consts = List.concat (map #2 newrels) 

352 
val rel_consts' = foldl add_const_typ_table rel_consts new_consts 

353 
val newp = p + (1.0p) / !convergence 

354 
in 

355 
Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels))); 

356 
(map #1 newrels) @ 

357 
(relevant_clauses thy ctab newp rel_consts' (more_rejects@rejects)) 

358 
end 

359 
 relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) = 

360 
let val weight = clause_weight ctab rel_consts consts_typs 

361 
in 

362 
if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts) 

363 
then (Output.debug (fn () => (name ^ " clause " ^ Int.toString n ^ 

364 
" passes: " ^ Real.toString weight)); 

365 
relevant ((ax,weight)::newrels, rejects) axs) 

366 
else relevant (newrels, ax::rejects) axs 

367 
end 

368 
in Output.debug (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p)); 

369 
relevant ([],[]) 

370 
end; 

371 

372 
fun relevance_filter thy axioms goals = 

373 
if !run_relevance_filter andalso !pass_mark >= 0.1 

374 
then 

375 
let val _ = Output.debug (fn () => "Start of relevance filtering"); 

376 
val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms 

377 
val goal_const_tab = get_goal_consts_typs thy goals 

378 
val _ = Output.debug (fn () => ("Initial constants: " ^ 

379 
space_implode ", " (Symtab.keys goal_const_tab))); 

380 
val rels = relevant_clauses thy const_tab (!pass_mark) 

381 
goal_const_tab (map (pair_consts_typs_axiom thy) axioms) 

382 
in 

383 
Output.debug (fn () => ("Total relevant: " ^ Int.toString (length rels))); 

384 
rels 

385 
end 

386 
else axioms; 

387 

388 
(***************************************************************) 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

389 
(* Retrieving and filtering lemmas *) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

390 
(***************************************************************) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

391 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

392 
(*** white list and black list of lemmas ***) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

393 

24215  394 
(*The rule subsetI is frequently omitted by the relevance filter. This could be theory data 
395 
or identified with ATPset (which however is too big currently)*) 

396 
val whitelist = [subsetI]; 

21588  397 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

398 
(*** retrieve lemmas from clasimpset and atpset, may filter them ***) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

399 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

400 
(*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

401 

22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

402 
fun setinsert (x,s) = Symtab.update (x,()) s; 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

403 

20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

404 
(*Reject theorems with names like "List.filter.filter_list_def" or 
21690
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

405 
"Accessible_Part.acc.defs", as these are definitions arising from packages.*) 
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

406 
fun is_package_def a = 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21790
diff
changeset

407 
let val names = NameSpace.explode a 
21690
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

408 
in 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

409 
length names > 2 andalso 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

410 
not (hd names = "local") andalso 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

411 
String.isSuffix "_def" a orelse String.isSuffix "_defs" a 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

412 
end; 
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

413 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

414 
(** a hash function from Term.term to int, and also a hash table **) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

415 
val xor_words = List.foldl Word.xorb 0w0; 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

416 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

417 
fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w) 
20661
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

418 
 hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

419 
 hashw_term ((Var(_,_)), w) = w 
20661
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

420 
 hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

421 
 hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

422 
 hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w))); 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

423 

21070  424 
fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0)) 
425 
 hash_literal P = hashw_term(P,0w0); 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

426 

24958  427 
fun hash_term t = Word.toIntX (xor_words (map hash_literal (HOLogic.disjuncts (strip_Trueprop t)))); 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

428 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

429 
fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2); 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

430 

22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

431 
exception HASH_CLAUSE; 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

432 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

433 
(*Create a hash table for clauses, of the given size*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

434 
fun mk_clause_table n = 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

435 
Polyhash.mkTable (hash_term o prop_of, equal_thm) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

436 
(n, HASH_CLAUSE); 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

437 

20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

438 
(*Use a hash table to eliminate duplicates from xs. Argument is a list of 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

439 
(thm * (string * int)) tuples. The theorems are hashed into the table. *) 
21588  440 
fun make_unique xs = 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

441 
let val ht = mk_clause_table 7000 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

442 
in 
22130  443 
Output.debug (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses")); 
21588  444 
app (ignore o Polyhash.peekInsert ht) xs; 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

445 
Polyhash.listItems ht 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

446 
end; 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

447 

20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

448 
(*Remove existing axiom clauses from the conjecture clauses, as this can dramatically 
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

449 
boost an ATP's performance (for some reason)*) 
21588  450 
fun subtract_cls c_clauses ax_clauses = 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

451 
let val ht = mk_clause_table 2200 
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

452 
fun known x = isSome (Polyhash.peek ht x) 
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

453 
in 
21588  454 
app (ignore o Polyhash.peekInsert ht) ax_clauses; 
455 
filter (not o known) c_clauses 

20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

456 
end; 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

457 

21224  458 
fun all_valid_thms ctxt = 
22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

459 
let 
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

460 
fun blacklisted s = !run_blacklist_filter andalso is_package_def s 
22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

461 

dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

462 
fun extern_valid space (name, ths) = 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

463 
let 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

464 
val is_valid = ProofContext.valid_thms ctxt; 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

465 
val xname = NameSpace.extern space name; 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

466 
in 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

467 
if blacklisted name then I 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

468 
else if is_valid (xname, ths) then cons (xname, ths) 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

469 
else if is_valid (name, ths) then cons (name, ths) 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

470 
else I 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

471 
end; 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

472 
val thy = ProofContext.theory_of ctxt; 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

473 
val all_thys = thy :: Theory.ancestors_of thy; 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

474 

dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

475 
fun dest_valid (space, tab) = Symtab.fold (extern_valid space) tab []; 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

476 
in 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

477 
maps (dest_valid o PureThy.theorems_of) all_thys @ 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

478 
fold (extern_valid (#1 (ProofContext.theorems_of ctxt))) 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

479 
(FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])) [] 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

480 
end; 
21224  481 

21588  482 
fun multi_name a (th, (n,pairs)) = 
21224  483 
(n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs) 
484 

22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

485 
fun add_single_names ((a, []), pairs) = pairs 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

486 
 add_single_names ((a, [th]), pairs) = (a,th)::pairs 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

487 
 add_single_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths); 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

488 

22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

489 
(*Ignore blacklisted basenames*) 
21588  490 
fun add_multi_names ((a, ths), pairs) = 
24854  491 
if (Sign.base_name a) mem_string ResAxioms.multi_base_blacklist then pairs 
22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

492 
else add_single_names ((a, ths), pairs); 
21224  493 

21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

494 
fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

495 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

496 
(*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*) 
21588  497 
fun name_thm_pairs ctxt = 
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

498 
let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt) 
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

499 
val ht = mk_clause_table 900 (*ht for blacklisted theorems*) 
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

500 
fun blacklisted x = !run_blacklist_filter andalso isSome (Polyhash.peek ht x) 
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

501 
in 
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

502 
app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt); 
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

503 
filter (not o blacklisted o #2) 
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

504 
(foldl add_single_names (foldl add_multi_names [] mults) singles) 
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

505 
end; 
21224  506 

507 
fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false) 

508 
 check_named (_,th) = true; 

19894  509 

22193  510 
fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ string_of_thm th); 
511 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

512 
(* get lemmas from claset, simpset, atpset and extra supplied rules *) 
21588  513 
fun get_clasimp_atp_lemmas ctxt user_thms = 
19894  514 
let val included_thms = 
21588  515 
if !include_all 
516 
then (tap (fn ths => Output.debug 

22130  517 
(fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems"))) 
21588  518 
(name_thm_pairs ctxt)) 
519 
else 

520 
let val claset_thms = 

521 
if !include_claset then ResAxioms.claset_rules_of ctxt 

522 
else [] 

523 
val simpset_thms = 

524 
if !include_simpset then ResAxioms.simpset_rules_of ctxt 

525 
else [] 

526 
val atpset_thms = 

527 
if !include_atpset then ResAxioms.atpset_rules_of ctxt 

528 
else [] 

22193  529 
val _ = (Output.debug (fn () => "ATP theorems: "); app display_thm atpset_thms) 
21588  530 
in claset_thms @ simpset_thms @ atpset_thms end 
531 
val user_rules = filter check_named 

22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

532 
(map ResAxioms.pairname 
24215  533 
(if null user_thms then whitelist else user_thms)) 
19894  534 
in 
21224  535 
(filter check_named included_thms, user_rules) 
19894  536 
end; 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

537 

21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

538 
(***************************************************************) 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

539 
(* Type Classes Present in the Axiom or Conjecture Clauses *) 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

540 
(***************************************************************) 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

541 

33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

542 
fun add_classes (sorts, cset) = foldl setinsert cset (List.concat sorts); 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

543 

33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

544 
(*Remove this trivial type class*) 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

545 
fun delete_type cset = Symtab.delete_safe "HOL.type" cset; 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

546 

33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

547 
fun tvar_classes_of_terms ts = 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

548 
let val sorts_list = map (map #2 o term_tvars) ts 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

549 
in Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list)) end; 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

550 

33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

551 
fun tfree_classes_of_terms ts = 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

552 
let val sorts_list = map (map #2 o term_tfrees) ts 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

553 
in Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list)) end; 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

554 

21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

555 
(*fold type constructors*) 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

556 
fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

557 
 fold_type_consts f T x = x; 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

558 

18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

559 
val add_type_consts_in_type = fold_type_consts setinsert; 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

560 

21397
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

561 
(*Type constructors used to instantiate overloaded constants are the only ones needed.*) 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

562 
fun add_type_consts_in_term thy = 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

563 
let val const_typargs = Sign.const_typargs thy 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

564 
fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

565 
 add_tcs (Abs (_, T, u)) x = add_tcs u x 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

566 
 add_tcs (t $ u) x = add_tcs t (add_tcs u x) 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

567 
 add_tcs _ x = x 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

568 
in add_tcs end 
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

569 

21397
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

570 
fun type_consts_of_terms thy ts = 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

571 
Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty); 
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

572 

18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

573 

19194  574 
(***************************************************************) 
575 
(* ATP invocation methods setup *) 

576 
(***************************************************************) 

577 

21588  578 
fun cnf_hyps_thms ctxt = 
20224
9c40a144ee0e
moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents:
20131
diff
changeset

579 
let val ths = Assumption.prems_of ctxt 
19617  580 
in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end; 
19194  581 

20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

582 
(*Translation mode can be autodetected, or forced to be firstorder or higherorder*) 
19194  583 
datatype mode = Auto  Fol  Hol; 
584 

19450
651d949776f8
exported linkup_logic_mode and changed the default setting
paulson
parents:
19445
diff
changeset

585 
val linkup_logic_mode = ref Auto; 
19205
4ec788c69f82
Tidying. New invoke_atp_ml for toplevel debugging. Flag to force FOL mode.
paulson
parents:
19194
diff
changeset

586 

20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

587 
(*Ensures that no higherorder theorems "leak out"*) 
24958  588 
fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls 
589 
 restrict_to_logic thy false cls = cls; 

20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

590 

21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

591 
(**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****) 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

592 

7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

593 
(** Too general means, positive equality literal with a variable X as one operand, 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

594 
when X does not occur properly in the other operand. This rules out clearly 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

595 
inconsistent clauses such as V=aV=b, though it by no means guarantees soundness. **) 
21588  596 

21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

597 
fun occurs ix = 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

598 
let fun occ(Var (jx,_)) = (ix=jx) 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

599 
 occ(t1$t2) = occ t1 orelse occ t2 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

600 
 occ(Abs(_,_,t)) = occ t 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

601 
 occ _ = false 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

602 
in occ end; 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

603 

7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

604 
fun is_recordtype T = not (null (RecordPackage.dest_recTs T)); 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

605 

7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

606 
(*Unwanted equalities include 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

607 
(1) those between a variable that does not properly occur in the second operand, 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

608 
(2) those between a variable and a record, since these seem to be prolific "cases" thms 
21588  609 
*) 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

610 
fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

611 
 too_general_eqterms _ = false; 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

612 

7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

613 
fun too_general_equality (Const ("op =", _) $ x $ y) = 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

614 
too_general_eqterms (x,y) orelse too_general_eqterms(y,x) 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

615 
 too_general_equality _ = false; 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

616 

7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

617 
(* tautologous? *) 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

618 
fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

619 
 is_taut _ = false; 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

620 

21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

621 
(*True if the term contains a variable whose (atomic) type is in the given list.*) 
21588  622 
fun has_typed_var tycons = 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

623 
let fun var_tycon (Var (_, Type(a,_))) = a mem_string tycons 
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

624 
 var_tycon _ = false 
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

625 
in exists var_tycon o term_vars end; 
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

626 

22217
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

627 
(*Clauses are forbidden to contain variables of these types. The typical reason is that 
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

628 
they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=(). 
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

629 
The resulting clause will have no type constraint, yielding false proofs. Even "bool" 
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

630 
leads to many unsound proofs, though (obviously) only for higherorder problems.*) 
24215  631 
val unwanted_types = ["Product_Type.unit","bool"]; 
22217
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

632 

21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

633 
fun unwanted t = 
24958  634 
is_taut t orelse has_typed_var unwanted_types t orelse 
635 
forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)); 

21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

636 

21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

637 
(*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and 
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

638 
likely to lead to unsound proofs.*) 
22217
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

639 
fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls; 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

640 

20022  641 
(*Called by the oraclebased methods declared in res_atp_methods.ML*) 
19722  642 
fun write_subgoal_file dfg mode ctxt conjectures user_thms n = 
24300  643 
let val conj_cls = Meson.make_clauses conjectures 
24827  644 
> map ResAxioms.combinators > Meson.finish_cnf 
21588  645 
val hyp_cls = cnf_hyps_thms ctxt 
646 
val goal_cls = conj_cls@hyp_cls 

647 
val goal_tms = map prop_of goal_cls 

22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

648 
val thy = ProofContext.theory_of ctxt 
24958  649 
val isFO = case mode of 
650 
Auto => forall (Meson.is_fol_term thy) goal_tms 

651 
 Fol => true 

652 
 Hol => false 

21588  653 
val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms 
22865  654 
val cla_simp_atp_clauses = included_thms 
21588  655 
> ResAxioms.cnf_rules_pairs > make_unique 
24958  656 
> restrict_to_logic thy isFO 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

657 
> remove_unwanted_clauses 
21588  658 
val user_cls = ResAxioms.cnf_rules_pairs user_rules 
24287  659 
val axclauses = make_unique (user_cls @ relevance_filter thy cla_simp_atp_clauses goal_tms) 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

660 
val subs = tfree_classes_of_terms goal_tms 
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

661 
and axtms = map (prop_of o #1) axclauses 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

662 
val supers = tvar_classes_of_terms axtms 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

663 
and tycons = type_consts_of_terms thy (goal_tms@axtms) 
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

664 
(*TFrees in conjecture clauses; TVars in axiom clauses*) 
22645  665 
val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers 
666 
val classrel_clauses = ResClause.make_classrel_clauses thy subs supers' 

24958  667 
val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file 
21588  668 
and file = atp_input_file() 
669 
and user_lemmas_names = map #1 user_rules 

19194  670 
in 
24958  671 
writer thy isFO goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names; 
22130  672 
Output.debug (fn () => "Writing to " ^ file); 
21588  673 
file 
19194  674 
end; 
675 

676 

677 
(**** remove tmp files ****) 

21588  678 
fun cond_rm_tmp file = 
22130  679 
if !Output.debugging orelse !destdir <> "" 
680 
then Output.debug (fn () => "ATP input kept...") 

20870  681 
else OS.FileSys.remove file; 
19194  682 

683 

684 
(***************************************************************) 

685 
(* automatic ATP invocation *) 

686 
(***************************************************************) 

687 

17306  688 
(* call prover with settings and problem file for the current subgoal *) 
17764  689 
fun watcher_call_provers sign sg_terms (childin, childout, pid) = 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

690 
let 
17422  691 
fun make_atp_list [] n = [] 
17717  692 
 make_atp_list (sg_term::xs) n = 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

693 
let 
17717  694 
val probfile = prob_pathname n 
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17525
diff
changeset

695 
val time = Int.toString (!time_limit) 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

696 
in 
22130  697 
Output.debug (fn () => "problem file in watcher_call_provers is " ^ probfile); 
17764  698 
(*options are separated by Watcher.setting_sep, currently #"%"*) 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

699 
case !prover of 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

700 
Recon.SPASS => 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

701 
let val spass = helper_path "SPASS_HOME" "SPASS" 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

702 
val sopts = 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

703 
"Auto%SOS=1%PGiven=0%PProblem=0%Splits=0%FullRed=0%DocProof%TimeLimit=" ^ time 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

704 
in 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

705 
("spass", spass, sopts, probfile) :: make_atp_list xs (n+1) 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

706 
end 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

707 
 Recon.Vampire => 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

708 
let val vampire = helper_path "VAMPIRE_HOME" "vampire" 
24546  709 
val vopts = "output_syntax tptp%mode casc%t " ^ time 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

710 
in 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

711 
("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1) 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

712 
end 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

713 
 Recon.E => 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

714 
let val eproof = helper_path "E_HOME" "eproof" 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

715 
val eopts = "tstpin%tstpout%l5%xAutoDev%tAutoDev%silent%cpulimit=" ^ time 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

716 
in 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

717 
("E", eproof, eopts, probfile) :: make_atp_list xs (n+1) 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

718 
end 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

719 
end 
15452  720 

17422  721 
val atp_list = make_atp_list sg_terms 1 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

722 
in 
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

723 
Watcher.callResProvers(childout,atp_list); 
22130  724 
Output.debug (fn () => "Sent commands to watcher!") 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

725 
end 
21588  726 

22193  727 
(*For debugging the generated set of theorem names*) 
21888  728 
fun trace_vector fname = 
22193  729 
let val path = File.explode_platform_path (fname ^ "_thm_names") 
21888  730 
in Vector.app (File.append path o (fn s => s ^ "\n")) end; 
16357  731 

20022  732 
(*We write out problem files for each subgoal. Argument probfile generates filenames, 
18986  733 
and allows the suppression of the suffix "_1" in problemgeneration mode. 
734 
FIXME: does not cope with &&, and it isn't easy because one could have multiple 

735 
subgoals, each involving &&.*) 

24546  736 
fun write_problem_files probfile (ctxt, chain_ths, th) = 
18753
aa82bd41555d
ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
paulson
parents:
18700
diff
changeset

737 
let val goals = Thm.prems_of th 
22130  738 
val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals)) 
17717  739 
val thy = ProofContext.theory_of ctxt 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

740 
fun get_neg_subgoals [] _ = [] 
22865  741 
 get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) :: 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21980
diff
changeset

742 
get_neg_subgoals gls (n+1) 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

743 
val goal_cls = get_neg_subgoals goals 1 
24958  744 
val isFO = case !linkup_logic_mode of 
745 
Auto => forall (Meson.is_fol_term thy) (map prop_of (List.concat goal_cls)) 

746 
 Fol => true 

747 
 Hol => false 

24546  748 
val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths 
22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

749 
val included_cls = included_thms > ResAxioms.cnf_rules_pairs > make_unique 
24958  750 
> restrict_to_logic thy isFO 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

751 
> remove_unwanted_clauses 
22130  752 
val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls)) 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

753 
val white_cls = ResAxioms.cnf_rules_pairs white_thms 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

754 
(*clauses relevant to goal gl*) 
24287  755 
val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls 
22130  756 
val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls))) 
21070  757 
axcls_list 
24958  758 
val writer = if !prover = Recon.SPASS then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

759 
fun write_all [] [] _ = [] 
21588  760 
 write_all (ccls::ccls_list) (axcls::axcls_list) k = 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

761 
let val fname = probfile k 
22217
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

762 
val _ = Output.debug (fn () => "About to write file " ^ fname) 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

763 
val axcls = make_unique axcls 
22217
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

764 
val _ = Output.debug (fn () => "Conjecture Clauses (before duplicate removal)") 
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

765 
val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

766 
val ccls = subtract_cls ccls axcls 
22217
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

767 
val _ = Output.debug (fn () => "Conjecture Clauses (AFTER duplicate removal)") 
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

768 
val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

769 
val ccltms = map prop_of ccls 
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

770 
and axtms = map (prop_of o #1) axcls 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

771 
val subs = tfree_classes_of_terms ccltms 
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

772 
and supers = tvar_classes_of_terms axtms 
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

773 
and tycons = type_consts_of_terms thy (ccltms@axtms) 
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

774 
(*TFrees in conjecture clauses; TVars in axiom clauses*) 
22645  775 
val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers 
776 
val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses)) 

777 
val classrel_clauses = ResClause.make_classrel_clauses thy subs supers' 

22130  778 
val _ = Output.debug (fn () => "classrel clauses = " ^ Int.toString (length classrel_clauses)) 
24958  779 
val clnames = writer thy isFO ccls fname (axcls,classrel_clauses,arity_clauses) [] 
21888  780 
val thm_names = Vector.fromList clnames 
22193  781 
val _ = if !Output.debugging then trace_vector fname thm_names else () 
20870  782 
in (thm_names,fname) :: write_all ccls_list axcls_list (k+1) end 
783 
val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1) 

19194  784 
in 
20870  785 
(filenames, thm_names_list) 
19194  786 
end; 
15644  787 

21588  788 
val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
17775  789 
Posix.Process.pid * string list) option); 
790 

791 
fun kill_last_watcher () = 

21588  792 
(case !last_watcher_pid of 
17775  793 
NONE => () 
21588  794 
 SOME (_, _, pid, files) => 
22130  795 
(Output.debug (fn () => "Killing old watcher, pid = " ^ string_of_pid pid); 
21588  796 
Watcher.killWatcher pid; 
797 
ignore (map (try cond_rm_tmp) files))) 

22130  798 
handle OS.SysErr _ => Output.debug (fn () => "Attempt to kill watcher failed"); 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17502
diff
changeset

799 

21980
d22f7e3c5ad9
xsymbol is no longer switched off in the ATP linkup
paulson
parents:
21900
diff
changeset

800 
(*writes out the current problems and calls ATPs*) 
24546  801 
fun isar_atp (ctxt, chain_ths, th) = 
17717  802 
if Thm.no_prems th then () 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

803 
else 
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

804 
let 
17775  805 
val _ = kill_last_watcher() 
24546  806 
val (files,thm_names_list) = write_problem_files prob_pathname (ctxt, chain_ths, th) 
22012
adf68479ae1b
Proof.context now sent to watcher and used in type inference step of proof reconstruction
paulson
parents:
21999
diff
changeset

807 
val (childin, childout, pid) = Watcher.createWatcher (ctxt, th, thm_names_list) 
15608  808 
in 
17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17764
diff
changeset

809 
last_watcher_pid := SOME (childin, childout, pid, files); 
22130  810 
Output.debug (fn () => "problem files: " ^ space_implode ", " files); 
811 
Output.debug (fn () => "pid: " ^ string_of_pid pid); 

22578  812 
watcher_call_provers (Thm.theory_of_thm th) (Thm.prems_of th) (childin, childout, pid) 
20954  813 
end; 
814 

815 
(*For ML scripts, and primarily, for debugging*) 

21588  816 
fun callatp () = 
20954  817 
let val th = topthm() 
818 
val ctxt = ProofContext.init (theory_of_thm th) 

24546  819 
in isar_atp (ctxt, [], th) end; 
15608  820 

24634  821 
val isar_atp_writeonly = PrintMode.setmp [] 
24546  822 
(fn (ctxt, chain_ths, th) => 
17717  823 
if Thm.no_prems th then () 
21588  824 
else 
825 
let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 

826 
else prob_pathname 

24546  827 
in ignore (write_problem_files probfile (ctxt, chain_ths, th)) end); 
15452  828 

16357  829 

22865  830 
(** the Isar toplevel command **) 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

831 

22865  832 
fun sledgehammer state = 
833 
let 

24546  834 
val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state); 
22865  835 
val thy = ProofContext.theory_of ctxt; 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

836 
in 
22130  837 
Output.debug (fn () => "subgoals in isar_atp:\n" ^ 
24920  838 
Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal))); 
22130  839 
Output.debug (fn () => "current theory: " ^ Context.theory_name thy); 
24546  840 
app (fn th => Output.debug (fn _ => "chained: " ^ string_of_thm th)) chain_ths; 
841 
if !time_limit > 0 then isar_atp (ctxt, chain_ths, goal) 

22865  842 
else (warning ("Writing problem file only: " ^ !problem_name); 
24546  843 
isar_atp_writeonly (ctxt, chain_ths, goal)) 
19205
4ec788c69f82
Tidying. New invoke_atp_ml for toplevel debugging. Flag to force FOL mode.
paulson
parents:
19194
diff
changeset

844 
end; 
4ec788c69f82
Tidying. New invoke_atp_ml for toplevel debugging. Flag to force FOL mode.
paulson
parents:
19194
diff
changeset

845 

24867  846 
val _ = 
847 
OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag 

848 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer)); 

17091  849 

15347  850 
end; 