author  wenzelm 
Tue, 15 Apr 2008 22:09:23 +0200  
changeset 26675  fba93ce71435 
parent 26662  39483503705f 
child 26691  520c99e0b9a0 
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 
26501
494f418cc51c
discontinued File.explode_platform_path  use plain Path.explode;
wenzelm
parents:
26278
diff
changeset

100 
in if File.exists (Path.explode 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))) 
26501
494f418cc51c
discontinued File.explode_platform_path  use plain Path.explode;
wenzelm
parents:
26278
diff
changeset

106 
else if File.exists (Path.explode (!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)) 
26501
494f418cc51c
discontinued File.explode_platform_path  use plain Path.explode;
wenzelm
parents:
26278
diff
changeset

116 
else if File.exists (Path.explode (!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 

26675  461 
fun valid_facts facts = 
462 
Facts.dest_table facts 

463 
> filter_out (fn (name, _) => !run_blacklist_filter andalso is_package_def name) 

464 
> map (apfst (Facts.extern facts)) 

465 
> filter_out (NameSpace.is_hidden o #1) 

466 
> map (apsnd (filter_out ResAxioms.bad_for_atp)); 

467 

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

469 
let 
26675  470 
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt); 
26278  471 
val local_facts = ProofContext.facts_of ctxt; 
26675  472 
in valid_facts global_facts @ valid_facts local_facts end; 
21224  473 

21588  474 
fun multi_name a (th, (n,pairs)) = 
21224  475 
(n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs) 
476 

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

477 
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

478 
 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

479 
 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

480 

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

481 
(*Ignore blacklisted basenames*) 
21588  482 
fun add_multi_names ((a, ths), pairs) = 
24854  483 
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

484 
else add_single_names ((a, ths), pairs); 
21224  485 

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

486 
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

487 

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

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

490 
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

491 
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

492 
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

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

494 
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

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

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

497 
end; 
21224  498 

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

500 
 check_named (_,th) = true; 

19894  501 

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

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

504 
(* get lemmas from claset, simpset, atpset and extra supplied rules *) 
21588  505 
fun get_clasimp_atp_lemmas ctxt user_thms = 
19894  506 
let val included_thms = 
21588  507 
if !include_all 
508 
then (tap (fn ths => Output.debug 

22130  509 
(fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems"))) 
21588  510 
(name_thm_pairs ctxt)) 
511 
else 

512 
let val claset_thms = 

513 
if !include_claset then ResAxioms.claset_rules_of ctxt 

514 
else [] 

515 
val simpset_thms = 

516 
if !include_simpset then ResAxioms.simpset_rules_of ctxt 

517 
else [] 

518 
val atpset_thms = 

519 
if !include_atpset then ResAxioms.atpset_rules_of ctxt 

520 
else [] 

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

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

529 

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

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

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

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

533 

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

534 
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

535 

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

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

537 
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

538 

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

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

540 
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

541 
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

542 

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

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

544 
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

545 
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

546 

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

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

548 
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

549 
 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

550 

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

551 
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

552 

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

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

554 
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

555 
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

556 
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

557 
 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

558 
 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

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

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

561 

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

562 
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

563 
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

564 

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

565 

19194  566 
(***************************************************************) 
567 
(* ATP invocation methods setup *) 

568 
(***************************************************************) 

569 

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

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

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

574 
(*Translation mode can be autodetected, or forced to be firstorder or higherorder*) 
19194  575 
datatype mode = Auto  Fol  Hol; 
576 

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

577 
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

578 

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

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

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

582 

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

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

584 

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

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

586 
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

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

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

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

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

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

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

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

594 
in occ end; 
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 
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

597 

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

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

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

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

602 
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

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

604 

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

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

606 
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

607 
 too_general_equality _ = false; 
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 
(* tautologous? *) 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

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

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

612 

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

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

615 
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

616 
 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

617 
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

618 

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

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

620 
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

621 
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

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

624 

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

625 
fun unwanted t = 
24958  626 
is_taut t orelse has_typed_var unwanted_types t orelse 
627 
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

628 

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

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

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

631 
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

632 

20022  633 
(*Called by the oraclebased methods declared in res_atp_methods.ML*) 
19722  634 
fun write_subgoal_file dfg mode ctxt conjectures user_thms n = 
24300  635 
let val conj_cls = Meson.make_clauses conjectures 
24827  636 
> map ResAxioms.combinators > Meson.finish_cnf 
21588  637 
val hyp_cls = cnf_hyps_thms ctxt 
638 
val goal_cls = conj_cls@hyp_cls 

639 
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

640 
val thy = ProofContext.theory_of ctxt 
24958  641 
val isFO = case mode of 
642 
Auto => forall (Meson.is_fol_term thy) goal_tms 

643 
 Fol => true 

644 
 Hol => false 

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

649 
> remove_unwanted_clauses 
21588  650 
val user_cls = ResAxioms.cnf_rules_pairs user_rules 
24287  651 
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

652 
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

653 
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

654 
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

655 
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

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

24958  659 
val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file 
21588  660 
and file = atp_input_file() 
661 
and user_lemmas_names = map #1 user_rules 

19194  662 
in 
24958  663 
writer thy isFO goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names; 
22130  664 
Output.debug (fn () => "Writing to " ^ file); 
21588  665 
file 
19194  666 
end; 
667 

668 

669 
(**** remove tmp files ****) 

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

20870  673 
else OS.FileSys.remove file; 
19194  674 

675 

676 
(***************************************************************) 

677 
(* automatic ATP invocation *) 

678 
(***************************************************************) 

679 

17306  680 
(* 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

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

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

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

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

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

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

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

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

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

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

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

692 
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

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

694 
let val vampire = helper_path "VAMPIRE_HOME" "vampire" 
24546  695 
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

696 
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

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

698 
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

699 
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

700 
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

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

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

704 
end 
21588  705 

22193  706 
(*For debugging the generated set of theorem names*) 
21888  707 
fun trace_vector fname = 
26501
494f418cc51c
discontinued File.explode_platform_path  use plain Path.explode;
wenzelm
parents:
26278
diff
changeset

708 
let val path = Path.explode (fname ^ "_thm_names") 
21888  709 
in Vector.app (File.append path o (fn s => s ^ "\n")) end; 
16357  710 

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

714 
subgoals, each involving &&.*) 

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

719 
fun get_neg_subgoals [] _ = [] 
22865  720 
 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

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

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

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

727 
 Fol => true 

728 
 Hol => false 

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

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

732 
> remove_unwanted_clauses 
22130  733 
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

734 
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

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

740 
fun write_all [] [] _ = [] 
21588  741 
 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

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

743 
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

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

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

746 
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

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

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

749 
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

750 
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

751 
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

752 
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

753 
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

754 
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

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

758 
val classrel_clauses = ResClause.make_classrel_clauses thy subs supers' 

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

19194  765 
in 
20870  766 
(filenames, thm_names_list) 
19194  767 
end; 
15644  768 

21588  769 
val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
17775  770 
Posix.Process.pid * string list) option); 
771 

772 
fun kill_last_watcher () = 

21588  773 
(case !last_watcher_pid of 
17775  774 
NONE => () 
21588  775 
 SOME (_, _, pid, files) => 
22130  776 
(Output.debug (fn () => "Killing old watcher, pid = " ^ string_of_pid pid); 
21588  777 
Watcher.killWatcher pid; 
778 
ignore (map (try cond_rm_tmp) files))) 

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

780 

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

781 
(*writes out the current problems and calls ATPs*) 
24546  782 
fun isar_atp (ctxt, chain_ths, th) = 
25047  783 
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

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

785 
let 
17775  786 
val _ = kill_last_watcher() 
24546  787 
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

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

790 
last_watcher_pid := SOME (childin, childout, pid, files); 
22130  791 
Output.debug (fn () => "problem files: " ^ space_implode ", " files); 
792 
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

793 
watcher_call_provers files (childin, childout, pid) 
20954  794 
end; 
795 

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

21588  797 
fun callatp () = 
20954  798 
let val th = topthm() 
799 
val ctxt = ProofContext.init (theory_of_thm th) 

24546  800 
in isar_atp (ctxt, [], th) end; 
15608  801 

24634  802 
val isar_atp_writeonly = PrintMode.setmp [] 
24546  803 
(fn (ctxt, chain_ths, th) => 
25047  804 
if Thm.no_prems th then warning "Nothing to prove" 
21588  805 
else 
806 
let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 

807 
else prob_pathname 

24546  808 
in ignore (write_problem_files probfile (ctxt, chain_ths, th)) end); 
15452  809 

16357  810 

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

812 

22865  813 
fun sledgehammer state = 
814 
let 

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

815 
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

816 
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

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

818 
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

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

820 
in 
25761  821 
if exists_type ResAxioms.type_has_empty_sort (prop_of goal) 
822 
then error "Proof state contains the empty sort" else (); 

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

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

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

831 

24867  832 
val _ = 
833 
OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag 

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

17091  835 

15347  836 
end; 