author  paulson 
Wed, 28 Nov 2007 16:26:03 +0100  
changeset 25492  4cc7976948ac 
parent 25243  78f8aaa27493 
child 25761  466e714de2fc 
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 

25047  28 
val max_sledgehammers : int ref 
24287  29 
val follow_defs : bool ref 
19894  30 
val add_all : unit > unit 
19227
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

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

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

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

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

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

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

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

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

42 
val type_consts_of_terms : theory > term list > string list 

15347  43 
end; 
44 

22865  45 
structure ResAtp: RES_ATP = 
15347  46 
struct 
47 

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

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

49 

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

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

54 
(* and also explicit ATP invocation methods *) 

55 
(********************************************************************) 

56 

57 
(*** background linkup ***) 

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

60 
val prover = ref Recon.E; 
25047  61 
val max_sledgehammers = ref 1; 
62 

21224  63 

24287  64 
(*** relevance filter parameters ***) 
65 
val run_relevance_filter = ref true; 

66 
val theory_const = ref true; 

67 
val pass_mark = ref 0.5; 

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

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

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

71 

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

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

77 
prover := Recon.E) 
21588  78 
 "spass" => 
24287  79 
(max_new := 40; 
80 
theory_const := true; 

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

81 
prover := Recon.SPASS) 
21588  82 
 "vampire" => 
24287  83 
(max_new := 60; 
84 
theory_const := false; 

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

85 
prover := Recon.Vampire) 
21224  86 
 _ => error ("No such prover: " ^ atp); 
87 

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

89 

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

90 
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

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

92 

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

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

21588  98 
 home => 
17819  99 
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

100 
in if File.exists (File.explode_platform_path path) then path 
21588  101 
else error ("Could not find the file " ^ path) 
102 
end; 

17819  103 

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

105 
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

106 
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

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

108 
else error ("No such directory: " ^ !destdir); 
15644  109 

17717  110 
fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n; 
111 

19194  112 
fun atp_input_file () = 
21588  113 
let val file = !problem_name 
19194  114 
in 
21588  115 
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

116 
else if File.exists (File.explode_platform_path (!destdir)) 
21588  117 
then !destdir ^ "/" ^ file 
118 
else error ("No such directory: " ^ !destdir) 

19194  119 
end; 
120 

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

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

125 

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

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

128 
fun rm_all() = include_all:=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_simpset() = include_simpset:=true; 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

131 
fun rm_simpset() = include_simpset:=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_claset() = include_claset:=true; 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

134 
fun rm_claset() = 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_clasimp() = (include_simpset:=true;include_claset:=true); 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

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

138 

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

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

140 
fun rm_atpset() = include_atpset:=false; 
19194  141 

24958  142 
fun strip_Trueprop (Const("Trueprop",_) $ t) = t 
143 
 strip_Trueprop t = t; 

19194  144 

21311  145 

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

146 
(***************************************************************) 
24287  147 
(* Relevance Filtering *) 
148 
(***************************************************************) 

149 

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

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

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

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

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

155 

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

157 

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

159 
the constant frequencies.*) 

160 
val weight_fn = ref log_weight2; 

161 

162 

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

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

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

166 
must be within comprehensions.*) 

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

168 

169 

170 
(*** constants with types ***) 

171 

172 
(*An abstraction of Isabelle types*) 

173 
datatype const_typ = CTVar  CType of string * const_typ list 

174 

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

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

177 
con1=con2 andalso match_types args1 args2 

178 
 match_type CTVar _ = true 

179 
 match_type _ CTVar = false 

180 
and match_types [] [] = true 

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

182 

183 
(*Is there a unifiable constant?*) 

184 
fun uni_mem gctab (c,c_typ) = 

185 
case Symtab.lookup gctab c of 

186 
NONE => false 

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

188 

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

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

191 
 const_typ_of (TFree _) = CTVar 

192 
 const_typ_of (TVar _) = CTVar 

193 

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

195 
fun const_with_typ thy (c,typ) = 

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

197 
in (c, map const_typ_of tvars) end 

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

199 

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

201 
which we ignore.*) 

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

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

204 
tab; 

205 

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

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

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

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

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

211 
 add_term_consts_typs_rm thy (t $ u, tab) = 

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

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

214 
 add_term_consts_typs_rm thy (_, tab) = tab; 

215 

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

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

218 

219 
val null_const_tab : const_typ list list Symtab.table = 

220 
foldl add_standard_const Symtab.empty standard_consts; 

221 

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

223 

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

225 
takes the given theory into account.*) 

226 
fun const_prop_of th = 

227 
if !theory_const then 

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

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

230 
in t $ prop_of th end 

231 
else prop_of th; 

232 

233 
(**** Constant / Type Frequencies ****) 

234 

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

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

237 
a linear ordering on type const_typ list.*) 

238 

239 
local 

240 

241 
fun cons_nr CTVar = 0 

242 
 cons_nr (CType _) = 1; 

243 

244 
in 

245 

246 
fun const_typ_ord TU = 

247 
case TU of 

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

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

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

251 

252 
end; 

253 

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

255 

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

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

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

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

260 
Symtab.map_default (c, CTtab.empty) 

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

262 
end 

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

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

265 
 count_term_consts (t $ u, tab) = 

266 
count_term_consts (t, count_term_consts (u, tab)) 

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

268 
 count_term_consts (_, tab) = tab 

269 
in count_term_consts (const_prop_of thm, tab) end; 

270 

271 

272 
(**** Actual Filtering Code ****) 

273 

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

275 
fun const_frequency ctab (c, cts) = 

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

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

278 
in List.foldl add 0 pairs end; 

279 

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

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

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

283 

284 
(*Relevant constants are weighted according to frequency, 

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

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

287 
fun clause_weight ctab gctyps consts_typs = 

288 
let val rel = filter (uni_mem gctyps) consts_typs 

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

290 
in 

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

292 
end; 

293 

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

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

296 

297 
fun consts_typs_of_term thy t = 

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

299 
in Symtab.fold add_expand_pairs tab [] end; 

300 

301 
fun pair_consts_typs_axiom thy (thm,name) = 

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

303 

304 
exception ConstFree; 

305 
fun dest_ConstFree (Const aT) = aT 

306 
 dest_ConstFree (Free aT) = aT 

307 
 dest_ConstFree _ = raise ConstFree; 

308 

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

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

311 
let val tm = prop_of thm 

312 
fun defs lhs rhs = 

313 
let val (rator,args) = strip_comb lhs 

314 
val ct = const_with_typ thy (dest_ConstFree rator) 

315 
in forall is_Var args andalso uni_mem gctypes ct andalso 

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

317 
end 

318 
handle ConstFree => false 

319 
in 

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

321 
defs lhs rhs andalso 

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

323 
 _ => false 

324 
end; 

325 

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

327 

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

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

330 

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

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

333 
let val nnew = length newpairs 

334 
in 

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

336 
else 

337 
let val cls = sort compare_pairs newpairs 

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

339 
in 

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

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

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

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

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

345 

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

347 
end 

348 
end; 

349 

350 
fun relevant_clauses thy ctab p rel_consts = 

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

352 
 relevant (newpairs,rejects) [] = 

353 
let val (newrels,more_rejects) = take_best newpairs 

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

355 
val rel_consts' = foldl add_const_typ_table rel_consts new_consts 

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

357 
in 

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

359 
(map #1 newrels) @ 

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

361 
end 

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

363 
let val weight = clause_weight ctab rel_consts consts_typs 

364 
in 

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

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

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

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

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

370 
end 

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

372 
relevant ([],[]) 

373 
end; 

374 

375 
fun relevance_filter thy axioms goals = 

376 
if !run_relevance_filter andalso !pass_mark >= 0.1 

377 
then 

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

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

380 
val goal_const_tab = get_goal_consts_typs thy goals 

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

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

383 
val rels = relevant_clauses thy const_tab (!pass_mark) 

384 
goal_const_tab (map (pair_consts_typs_axiom thy) axioms) 

385 
in 

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

387 
rels 

388 
end 

389 
else axioms; 

390 

391 
(***************************************************************) 

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

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

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

394 

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

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

396 

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

399 
val whitelist = [subsetI]; 

21588  400 

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

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

402 

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

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

404 

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

405 
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

406 

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

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

408 
"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

409 
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

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

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

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

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

414 
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

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

416 

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

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

418 
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

419 

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

420 
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

421 
 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

422 
 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

423 
 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

424 
 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

425 
 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

426 

21070  427 
fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0)) 
428 
 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

429 

24958  430 
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

431 

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

432 
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

433 

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

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

435 

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

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

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

438 
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

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

440 

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

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

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

444 
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

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

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

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

450 

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

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

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

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

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

456 
in 
21588  457 
app (ignore o Polyhash.peekInsert ht) ax_clauses; 
458 
filter (not o known) c_clauses 

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

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

460 

21224  461 
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

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

463 
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

464 

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

465 
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

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

467 
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

468 
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

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

470 
if blacklisted name then I 
25243  471 
else if is_valid (xname, ths) then cons (xname, filter_out ResAxioms.bad_for_atp ths) 
472 
else if is_valid (name, ths) then cons (name, filter_out ResAxioms.bad_for_atp ths) 

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

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

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

475 
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

476 
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

477 

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

478 
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

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

480 
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

481 
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

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

483 
end; 
21224  484 

21588  485 
fun multi_name a (th, (n,pairs)) = 
21224  486 
(n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs) 
487 

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

488 
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

489 
 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

490 
 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

491 

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

492 
(*Ignore blacklisted basenames*) 
21588  493 
fun add_multi_names ((a, ths), pairs) = 
24854  494 
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

495 
else add_single_names ((a, ths), pairs); 
21224  496 

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

497 
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

498 

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

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

501 
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

502 
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

503 
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

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

505 
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

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

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

508 
end; 
21224  509 

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

511 
 check_named (_,th) = true; 

19894  512 

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

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

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

22130  520 
(fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems"))) 
21588  521 
(name_thm_pairs ctxt)) 
522 
else 

523 
let val claset_thms = 

524 
if !include_claset then ResAxioms.claset_rules_of ctxt 

525 
else [] 

526 
val simpset_thms = 

527 
if !include_simpset then ResAxioms.simpset_rules_of ctxt 

528 
else [] 

529 
val atpset_thms = 

530 
if !include_atpset then ResAxioms.atpset_rules_of ctxt 

531 
else [] 

22193  532 
val _ = (Output.debug (fn () => "ATP theorems: "); app display_thm atpset_thms) 
21588  533 
in claset_thms @ simpset_thms @ atpset_thms end 
534 
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

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

540 

21290
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 
(* Type Classes Present in the Axiom or Conjecture Clauses *) 
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 

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

545 
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

546 

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

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

548 
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

549 

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

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

551 
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

552 
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

553 

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

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

555 
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

556 
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

557 

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

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

559 
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

560 
 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

561 

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

562 
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

563 

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

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

565 
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

566 
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

567 
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

568 
 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

569 
 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

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

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

572 

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

573 
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

574 
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

575 

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

576 

19194  577 
(***************************************************************) 
578 
(* ATP invocation methods setup *) 

579 
(***************************************************************) 

580 

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

582 
let val ths = Assumption.prems_of ctxt 
25006  583 
in fold (fold (insert Thm.eq_thm) o ResAxioms.cnf_axiom) ths [] end; 
19194  584 

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

585 
(*Translation mode can be autodetected, or forced to be firstorder or higherorder*) 
19194  586 
datatype mode = Auto  Fol  Hol; 
587 

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

588 
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

589 

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

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

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

593 

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

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

595 

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

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

597 
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

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

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

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

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

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

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

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

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

606 

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

607 
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

608 

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

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

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

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

613 
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

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

615 

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

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

617 
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

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

619 

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

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

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

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

623 

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

624 
(*True if the term contains a variable whose (atomic) type is in the given list.*) 
21588  625 
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

626 
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

627 
 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

628 
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

629 

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

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

631 
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

632 
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

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

635 

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

636 
fun unwanted t = 
24958  637 
is_taut t orelse has_typed_var unwanted_types t orelse 
638 
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

639 

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

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

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

642 
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

643 

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

650 
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

651 
val thy = ProofContext.theory_of ctxt 
24958  652 
val isFO = case mode of 
653 
Auto => forall (Meson.is_fol_term thy) goal_tms 

654 
 Fol => true 

655 
 Hol => false 

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

660 
> remove_unwanted_clauses 
21588  661 
val user_cls = ResAxioms.cnf_rules_pairs user_rules 
24287  662 
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

663 
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

664 
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

665 
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

666 
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

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

24958  670 
val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file 
21588  671 
and file = atp_input_file() 
672 
and user_lemmas_names = map #1 user_rules 

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

679 

680 
(**** remove tmp files ****) 

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

20870  684 
else OS.FileSys.remove file; 
19194  685 

686 

687 
(***************************************************************) 

688 
(* automatic ATP invocation *) 

689 
(***************************************************************) 

690 

17306  691 
(* call prover with settings and problem file for the current subgoal *) 
25085
aa9db4e3cd5e
Ensured that the right number of ATP calls is generated
paulson
parents:
25047
diff
changeset

692 
fun watcher_call_provers files (childin, childout, pid) = 
aa9db4e3cd5e
Ensured that the right number of ATP calls is generated
paulson
parents:
25047
diff
changeset

693 
let val time = Int.toString (!time_limit) 
aa9db4e3cd5e
Ensured that the right number of ATP calls is generated
paulson
parents:
25047
diff
changeset

694 
fun make_atp_list [] = [] 
aa9db4e3cd5e
Ensured that the right number of ATP calls is generated
paulson
parents:
25047
diff
changeset

695 
 make_atp_list (file::files) = 
aa9db4e3cd5e
Ensured that the right number of ATP calls is generated
paulson
parents:
25047
diff
changeset

696 
(Output.debug (fn () => "problem file in watcher_call_provers is " ^ file); 
aa9db4e3cd5e
Ensured that the right number of ATP calls is generated
paulson
parents:
25047
diff
changeset

697 
(*options are separated by Watcher.setting_sep, currently #"%"*) 
aa9db4e3cd5e
Ensured that the right number of ATP calls is generated
paulson
parents:
25047
diff
changeset

698 
case !prover of 
aa9db4e3cd5e
Ensured that the right number of ATP calls is generated
paulson
parents:
25047
diff
changeset

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

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

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

702 
"Auto%SOS=1%PGiven=0%PProblem=0%Splits=0%FullRed=0%DocProof%TimeLimit=" ^ time 
25085
aa9db4e3cd5e
Ensured that the right number of ATP calls is generated
paulson
parents:
25047
diff
changeset

703 
in ("spass", spass, sopts, file) :: make_atp_list files end 
aa9db4e3cd5e
Ensured that the right number of ATP calls is generated
paulson
parents:
25047
diff
changeset

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

705 
let val vampire = helper_path "VAMPIRE_HOME" "vampire" 
24546  706 
val vopts = "output_syntax tptp%mode casc%t " ^ time 
25085
aa9db4e3cd5e
Ensured that the right number of ATP calls is generated
paulson
parents:
25047
diff
changeset

707 
in ("vampire", vampire, vopts, file) :: make_atp_list files end 
aa9db4e3cd5e
Ensured that the right number of ATP calls is generated
paulson
parents:
25047
diff
changeset

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

709 
let val eproof = helper_path "E_HOME" "eproof" 
25085
aa9db4e3cd5e
Ensured that the right number of ATP calls is generated
paulson
parents:
25047
diff
changeset

710 
val eopts = "tstpin%tstpout%l5%xAutoDev%tAutoDev%silent%cpulimit=" ^ time 
aa9db4e3cd5e
Ensured that the right number of ATP calls is generated
paulson
parents:
25047
diff
changeset

711 
in ("E", eproof, eopts, file) :: make_atp_list files end) 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

712 
in 
25085
aa9db4e3cd5e
Ensured that the right number of ATP calls is generated
paulson
parents:
25047
diff
changeset

713 
Watcher.callResProvers(childout, make_atp_list files); 
22130  714 
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

715 
end 
21588  716 

22193  717 
(*For debugging the generated set of theorem names*) 
21888  718 
fun trace_vector fname = 
22193  719 
let val path = File.explode_platform_path (fname ^ "_thm_names") 
21888  720 
in Vector.app (File.append path o (fn s => s ^ "\n")) end; 
16357  721 

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

725 
subgoals, each involving &&.*) 

24546  726 
fun write_problem_files probfile (ctxt, chain_ths, th) = 
25047  727 
let val goals = Library.take (!max_sledgehammers, Thm.prems_of th) (*raises no exception*) 
22130  728 
val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals)) 
17717  729 
val thy = ProofContext.theory_of ctxt 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

730 
fun get_neg_subgoals [] _ = [] 
22865  731 
 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

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

733 
val goal_cls = get_neg_subgoals goals 1 
25243  734 
handle THM ("assume: variables", _, _) => 
735 
error "Sledgehammer: Goal contains type variables (TVars)" 

24958  736 
val isFO = case !linkup_logic_mode of 
737 
Auto => forall (Meson.is_fol_term thy) (map prop_of (List.concat goal_cls)) 

738 
 Fol => true 

739 
 Hol => false 

24546  740 
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

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

743 
> remove_unwanted_clauses 
22130  744 
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

745 
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

746 
(*clauses relevant to goal gl*) 
24287  747 
val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls 
22130  748 
val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls))) 
21070  749 
axcls_list 
24958  750 
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

751 
fun write_all [] [] _ = [] 
21588  752 
 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

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

754 
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

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

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

757 
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

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

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

760 
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

761 
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

762 
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

763 
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

764 
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

765 
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

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

769 
val classrel_clauses = ResClause.make_classrel_clauses thy subs supers' 

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

19194  776 
in 
20870  777 
(filenames, thm_names_list) 
19194  778 
end; 
15644  779 

21588  780 
val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
17775  781 
Posix.Process.pid * string list) option); 
782 

783 
fun kill_last_watcher () = 

21588  784 
(case !last_watcher_pid of 
17775  785 
NONE => () 
21588  786 
 SOME (_, _, pid, files) => 
22130  787 
(Output.debug (fn () => "Killing old watcher, pid = " ^ string_of_pid pid); 
21588  788 
Watcher.killWatcher pid; 
789 
ignore (map (try cond_rm_tmp) files))) 

22130  790 
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

791 

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

792 
(*writes out the current problems and calls ATPs*) 
24546  793 
fun isar_atp (ctxt, chain_ths, th) = 
25047  794 
if Thm.no_prems th then warning "Nothing to prove" 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

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

796 
let 
17775  797 
val _ = kill_last_watcher() 
24546  798 
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

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

801 
last_watcher_pid := SOME (childin, childout, pid, files); 
22130  802 
Output.debug (fn () => "problem files: " ^ space_implode ", " files); 
803 
Output.debug (fn () => "pid: " ^ string_of_pid pid); 

25085
aa9db4e3cd5e
Ensured that the right number of ATP calls is generated
paulson
parents:
25047
diff
changeset

804 
watcher_call_provers files (childin, childout, pid) 
20954  805 
end; 
806 

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

21588  808 
fun callatp () = 
20954  809 
let val th = topthm() 
810 
val ctxt = ProofContext.init (theory_of_thm th) 

24546  811 
in isar_atp (ctxt, [], th) end; 
15608  812 

24634  813 
val isar_atp_writeonly = PrintMode.setmp [] 
24546  814 
(fn (ctxt, chain_ths, th) => 
25047  815 
if Thm.no_prems th then warning "Nothing to prove" 
21588  816 
else 
817 
let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 

818 
else prob_pathname 

24546  819 
in ignore (write_problem_files probfile (ctxt, chain_ths, th)) end); 
15452  820 

16357  821 

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

823 

22865  824 
fun sledgehammer state = 
825 
let 

25492
4cc7976948ac
Chained theorems are no longer mentioned in metis calls and (if used) they prevent the
paulson
parents:
25243
diff
changeset

826 
val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state) 
4cc7976948ac
Chained theorems are no longer mentioned in metis calls and (if used) they prevent the
paulson
parents:
25243
diff
changeset

827 
val chain_ths = map (PureThy.put_name_hint Recon.chained_hint) chain_ths 
4cc7976948ac
Chained theorems are no longer mentioned in metis calls and (if used) they prevent the
paulson
parents:
25243
diff
changeset

828 
(*Mark the chained theorems to keep them out of metis calls; 
4cc7976948ac
Chained theorems are no longer mentioned in metis calls and (if used) they prevent the
paulson
parents:
25243
diff
changeset

829 
their original "name hints" may be bad anyway.*) 
4cc7976948ac
Chained theorems are no longer mentioned in metis calls and (if used) they prevent the
paulson
parents:
25243
diff
changeset

830 
val thy = ProofContext.theory_of ctxt 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

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

22865  837 
else (warning ("Writing problem file only: " ^ !problem_name); 
24546  838 
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

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

840 

24867  841 
val _ = 
842 
OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag 

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

17091  844 

15347  845 
end; 