author  wenzelm 
Sat, 15 Mar 2008 18:07:59 +0100  
changeset 26278  f0c6839df608 
parent 25761  466e714de2fc 
child 26501  494f418cc51c 
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 

26278  478 
val local_facts = ProofContext.facts_of ctxt; 
479 

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

480 
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

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

482 
maps (dest_valid o PureThy.theorems_of) all_thys @ 
26278  483 
fold (extern_valid (Facts.space_of local_facts)) (Facts.dest local_facts) [] 
22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

484 
end; 
21224  485 

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

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

489 
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

490 
 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

491 
 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

492 

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

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

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

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

498 
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

499 

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

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

502 
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

503 
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

504 
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

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

506 
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

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

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

509 
end; 
21224  510 

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

512 
 check_named (_,th) = true; 

19894  513 

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

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

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

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

524 
let val claset_thms = 

525 
if !include_claset then ResAxioms.claset_rules_of ctxt 

526 
else [] 

527 
val simpset_thms = 

528 
if !include_simpset then ResAxioms.simpset_rules_of ctxt 

529 
else [] 

530 
val atpset_thms = 

531 
if !include_atpset then ResAxioms.atpset_rules_of ctxt 

532 
else [] 

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

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

541 

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

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

546 
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

547 

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

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

549 
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

550 

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

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

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

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

554 

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

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

556 
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

557 
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

558 

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

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

560 
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

561 
 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

562 

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

563 
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

564 

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

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

566 
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

567 
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

568 
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

569 
 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

570 
 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

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

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

573 

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

574 
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

575 
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

576 

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

577 

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

580 
(***************************************************************) 

581 

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

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

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

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

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

589 
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

590 

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

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

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

594 

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

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

596 

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

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

598 
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

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

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

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

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

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

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

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

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

607 

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

608 
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

609 

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

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

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

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

614 
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

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

616 

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

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

618 
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

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

620 

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

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

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

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

624 

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

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

627 
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

628 
 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

629 
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

630 

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

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

632 
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

633 
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

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

636 

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

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

640 

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

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

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

643 
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

644 

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

651 
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

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

655 
 Fol => true 

656 
 Hol => false 

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

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

664 
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

665 
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

666 
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

667 
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

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

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

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

680 

681 
(**** remove tmp files ****) 

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

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

687 

688 
(***************************************************************) 

689 
(* automatic ATP invocation *) 

690 
(***************************************************************) 

691 

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

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

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

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

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

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

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

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

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

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

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

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

704 
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

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

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

708 
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

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

710 
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

711 
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

712 
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

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

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

716 
end 
21588  717 

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

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

726 
subgoals, each involving &&.*) 

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

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

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

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

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

739 
 Fol => true 

740 
 Hol => false 

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

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

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

746 
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

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

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

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

755 
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

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

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

758 
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

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

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

761 
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

762 
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

763 
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

764 
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

765 
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

766 
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

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

770 
val classrel_clauses = ResClause.make_classrel_clauses thy subs supers' 

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

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

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

784 
fun kill_last_watcher () = 

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

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

792 

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

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

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

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

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

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

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

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

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

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

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

819 
else prob_pathname 

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

16357  822 

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

824 

22865  825 
fun sledgehammer state = 
826 
let 

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

827 
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

828 
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

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

830 
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

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

832 
in 
25761  833 
if exists_type ResAxioms.type_has_empty_sort (prop_of goal) 
834 
then error "Proof state contains the empty sort" else (); 

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

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

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

843 

24867  844 
val _ = 
845 
OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag 

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

17091  847 

15347  848 
end; 