author  boehmes 
Tue, 08 Dec 2009 23:05:23 +0100  
changeset 34035  08d34921b7dd 
parent 33316  6a72af4e84b8 
child 34052  b2e6245fb3da 
permissions  rwrr 
32564  1 
(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML 
2 
Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich 

32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

3 
*) 
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

4 

594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

5 
structure Mirabelle_Sledgehammer : MIRABELLE_ACTION = 
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

6 
struct 
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

7 

32521  8 
val proverK = "prover" 
32541  9 
val prover_timeoutK = "prover_timeout" 
32574
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

10 
val prover_hard_timeoutK = "prover_hard_timeout" 
32521  11 
val keepK = "keep" 
12 
val full_typesK = "full_types" 

32525  13 
val minimizeK = "minimize" 
14 
val minimize_timeoutK = "minimize_timeout" 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

15 
val metis_ftK = "metis_ft" 
32521  16 

17 
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " 

32525  18 
fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): " 
32521  19 
fun metis_tag id = "#" ^ string_of_int id ^ " metis (sledgehammer): " 
20 

32525  21 
val separator = "" 
22 

32521  23 

32549  24 
datatype sh_data = ShData of { 
25 
calls: int, 

26 
success: int, 

32585  27 
lemmas: int, 
32818  28 
max_lems: int, 
32549  29 
time_isa: int, 
30 
time_atp: int, 

31 
time_atp_fail: int} 

32 

33 
datatype me_data = MeData of { 

34 
calls: int, 

35 
success: int, 

32676  36 
proofs: int, 
32549  37 
time: int, 
32550  38 
timeout: int, 
32990  39 
lemmas: int * int * int, 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

40 
posns: Position.T list 
32550  41 
} 
32549  42 

32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

43 
datatype min_data = MinData of { 
32609  44 
succs: int, 
45 
ab_ratios: int, 

46 
it_ratios: int 

32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

47 
} 
32521  48 

32818  49 
fun make_sh_data 
50 
(calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail) = 

51 
ShData{calls=calls, success=success, lemmas=lemmas, max_lems=max_lems, 

52 
time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail} 

32521  53 

32609  54 
fun make_min_data (succs, ab_ratios, it_ratios) = 
55 
MinData{succs=succs, ab_ratios=ab_ratios, it_ratios=it_ratios} 

32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

56 

32990  57 
fun make_me_data (calls,success,proofs,time,timeout,lemmas,posns) = 
32818  58 
MeData{calls=calls, success=success, proofs=proofs, time=time, 
32990  59 
timeout=timeout, lemmas=lemmas, posns=posns} 
32549  60 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

61 
val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

62 
val empty_min_data = make_min_data(0, 0, 0) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

63 
val empty_me_data = make_me_data(0, 0, 0, 0, 0, (0,0,0), []) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

64 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

65 
fun tuple_of_sh_data (ShData {calls, success, lemmas, max_lems, time_isa, 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

66 
time_atp, time_atp_fail}) = (calls, success, lemmas, max_lems, time_isa, 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

67 
time_atp, time_atp_fail) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

68 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

69 
fun tuple_of_min_data (MinData {succs, ab_ratios, it_ratios}) = 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

70 
(succs, ab_ratios, it_ratios) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

71 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

72 
fun tuple_of_me_data (MeData {calls, success, proofs, time, timeout, lemmas, 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

73 
posns}) = (calls, success, proofs, time, timeout, lemmas, posns) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

74 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

75 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

76 
datatype metis = Unminimized  Minimized  UnminimizedFT  MinimizedFT 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

77 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

78 
datatype data = Data of { 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

79 
sh: sh_data, 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

80 
min: min_data, 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

81 
me_u: me_data, (* metis with unminimized set of lemmas *) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

82 
me_m: me_data, (* metis with minimized set of lemmas *) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

83 
me_uft: me_data, (* metis with unminimized set of lemmas and fullytyped *) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

84 
me_mft: me_data, (* metis with minimized set of lemmas and fullytyped *) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

85 
mini: bool (* with minimization *) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

86 
} 
32521  87 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

88 
fun make_data (sh, min, me_u, me_m, me_uft, me_mft, mini) = 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

89 
Data {sh=sh, min=min, me_u=me_u, me_m=me_m, me_uft=me_uft, me_mft=me_mft, 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

90 
mini=mini} 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

91 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

92 
val empty_data = make_data (empty_sh_data, empty_min_data, 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

93 
empty_me_data, empty_me_data, empty_me_data, empty_me_data, false) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

94 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

95 
fun map_sh_data f (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) = 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

96 
let val sh' = make_sh_data (f (tuple_of_sh_data sh)) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

97 
in make_data (sh', min, me_u, me_m, me_uft, me_mft, mini) end 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

98 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

99 
fun map_min_data f (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) = 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

100 
let val min' = make_min_data (f (tuple_of_min_data min)) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

101 
in make_data (sh, min', me_u, me_m, me_uft, me_mft, mini) end 
32521  102 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

103 
fun map_me_data f m (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) = 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

104 
let 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

105 
fun map_me g Unminimized (u, m, uft, mft) = (g u, m, uft, mft) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

106 
 map_me g Minimized (u, m, uft, mft) = (u, g m, uft, mft) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

107 
 map_me g UnminimizedFT (u, m, uft, mft) = (u, m, g uft, mft) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

108 
 map_me g MinimizedFT (u, m, uft, mft) = (u, m, uft, g mft) 
32521  109 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

110 
val f' = make_me_data o f o tuple_of_me_data 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

111 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

112 
val (me_u', me_m', me_uft', me_mft') = 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

113 
map_me f' m (me_u, me_m, me_uft, me_mft) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

114 
in make_data (sh, min, me_u', me_m', me_uft', me_mft', mini) end 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

115 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

116 
fun set_mini mini (Data {sh, min, me_u, me_m, me_uft, me_mft, ...}) = 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

117 
make_data (sh, min, me_u, me_m, me_uft, me_mft, mini) 
32990  118 

119 
fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); 

32521  120 

32818  121 
val inc_sh_calls = map_sh_data 
122 
(fn (calls, success, lemmas,max_lems, time_isa, time_atp, time_atp_fail) 

123 
=> (calls + 1, success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)) 

32549  124 

32818  125 
val inc_sh_success = map_sh_data 
126 
(fn (calls, success, lemmas,max_lems, time_isa, time_atp, time_atp_fail) 

127 
=> (calls, success + 1, lemmas,max_lems, time_isa, time_atp, time_atp_fail)) 

32585  128 

32818  129 
fun inc_sh_lemmas n = map_sh_data 
130 
(fn (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail) 

131 
=> (calls,success,lemmas+n,max_lems,time_isa,time_atp,time_atp_fail)) 

32521  132 

32818  133 
fun inc_sh_max_lems n = map_sh_data 
134 
(fn (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail) 

135 
=> (calls,success,lemmas,Int.max(max_lems,n),time_isa,time_atp,time_atp_fail)) 

32549  136 

32818  137 
fun inc_sh_time_isa t = map_sh_data 
138 
(fn (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail) 

139 
=> (calls,success,lemmas,max_lems,time_isa + t,time_atp,time_atp_fail)) 

140 

141 
fun inc_sh_time_atp t = map_sh_data 

142 
(fn (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail) 

143 
=> (calls,success,lemmas,max_lems,time_isa,time_atp + t,time_atp_fail)) 

32521  144 

32818  145 
fun inc_sh_time_atp_fail t = map_sh_data 
146 
(fn (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail) 

147 
=> (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail + t)) 

32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

148 

32818  149 
val inc_min_succs = map_min_data 
150 
(fn (succs,ab_ratios,it_ratios) => (succs+1, ab_ratios, it_ratios)) 

32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

151 

32818  152 
fun inc_min_ab_ratios r = map_min_data 
153 
(fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios+r, it_ratios)) 

32609  154 

32818  155 
fun inc_min_it_ratios r = map_min_data 
156 
(fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r)) 

32549  157 

32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

158 
val inc_metis_calls = map_me_data 
32990  159 
(fn (calls,success,proofs,time,timeout,lemmas,posns) 
160 
=> (calls + 1, success, proofs, time, timeout, lemmas,posns)) 

32533  161 

32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

162 
val inc_metis_success = map_me_data 
32990  163 
(fn (calls,success,proofs,time,timeout,lemmas,posns) 
164 
=> (calls, success + 1, proofs, time, timeout, lemmas,posns)) 

32676  165 

166 
val inc_metis_proofs = map_me_data 

32990  167 
(fn (calls,success,proofs,time,timeout,lemmas,posns) 
168 
=> (calls, success, proofs + 1, time, timeout, lemmas,posns)) 

32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

169 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

170 
fun inc_metis_time m t = map_me_data 
32990  171 
(fn (calls,success,proofs,time,timeout,lemmas,posns) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

172 
=> (calls, success, proofs, time + t, timeout, lemmas,posns)) m 
32536  173 

32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

174 
val inc_metis_timeout = map_me_data 
32990  175 
(fn (calls,success,proofs,time,timeout,lemmas,posns) 
176 
=> (calls, success, proofs, time, timeout + 1, lemmas,posns)) 

32549  177 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

178 
fun inc_metis_lemmas m n = map_me_data 
32990  179 
(fn (calls,success,proofs,time,timeout,lemmas,posns) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

180 
=> (calls, success, proofs, time, timeout, inc_max n lemmas, posns)) m 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

181 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

182 
fun inc_metis_posns m pos = map_me_data 
32990  183 
(fn (calls,success,proofs,time,timeout,lemmas,posns) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

184 
=> (calls, success, proofs, time, timeout, lemmas, pos::posns)) m 
32521  185 

186 
local 

187 

188 
val str = string_of_int 

189 
val str3 = Real.fmt (StringCvt.FIX (SOME 3)) 

190 
fun percentage a b = string_of_int (a * 100 div b) 

191 
fun time t = Real.fromInt t / 1000.0 

192 
fun avg_time t n = 

193 
if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 

194 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

195 
fun log_sh_data log 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

196 
(calls, success, lemmas, max_lems, time_isa, time_atp, time_atp_fail) = 
32818  197 
(log ("Total number of sledgehammer calls: " ^ str calls); 
198 
log ("Number of successful sledgehammer calls: " ^ str success); 

199 
log ("Number of sledgehammer lemmas: " ^ str lemmas); 

200 
log ("Max number of sledgehammer lemmas: " ^ str max_lems); 

201 
log ("Success rate: " ^ percentage success calls ^ "%"); 

202 
log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa)); 

203 
log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_atp)); 

204 
log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_atp_fail)); 

32536  205 
log ("Average time for sledgehammer calls (Isabelle): " ^ 
32818  206 
str3 (avg_time time_isa calls)); 
32533  207 
log ("Average time for successful sledgehammer calls (ATP): " ^ 
32818  208 
str3 (avg_time time_atp success)); 
32536  209 
log ("Average time for failed sledgehammer calls (ATP): " ^ 
32818  210 
str3 (avg_time time_atp_fail (calls  success))) 
32533  211 
) 
32521  212 

32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

213 

421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

214 
fun str_of_pos pos = 
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

215 
let val str0 = string_of_int o the_default 0 
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

216 
in str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) end 
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

217 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

218 
fun log_me_data log tag sh_calls (metis_calls, metis_success, 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

219 
metis_proofs, metis_time, metis_timeout, (lemmas, lems_sos, lems_max), 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

220 
metis_posns) = 
32549  221 
(log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls); 
32740  222 
log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success ^ 
223 
" (proof: " ^ str metis_proofs ^ ")"); 

32549  224 
log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout); 
32533  225 
log ("Success rate: " ^ percentage metis_success sh_calls ^ "%"); 
32990  226 
log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str lemmas); 
227 
log ("SOS of successful " ^ tag ^ "metis lemmas: " ^ str lems_sos); 

228 
log ("Max number of successful " ^ tag ^ "metis lemmas: " ^ str lems_max); 

229 
log ("Total time for successful " ^ tag ^ "metis calls: " ^ str3 (time metis_time)); 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

230 
log ("Average time for successful " ^ tag ^ "metis calls: " ^ 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

231 
str3 (avg_time metis_time metis_success)); 
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

232 
if tag="" 
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

233 
then log ("Proved: " ^ space_implode " " (map str_of_pos metis_posns)) 
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

234 
else () 
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

235 
) 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

236 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

237 
fun log_min_data log (succs, ab_ratios, it_ratios) = 
32609  238 
(log ("Number of successful minimizations: " ^ string_of_int succs); 
239 
log ("After/before ratios: " ^ string_of_int ab_ratios); 

240 
log ("Iterations ratios: " ^ string_of_int it_ratios) 

32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

241 
) 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

242 

32521  243 
in 
244 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

245 
fun log_data id log (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) = 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

246 
let 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

247 
val ShData {calls=sh_calls, ...} = sh 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

248 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

249 
fun app_if (MeData {calls, ...}) f = if calls > 0 then f () else () 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

250 
fun log_me tag m = 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

251 
log_me_data log tag sh_calls (tuple_of_me_data m) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

252 
fun log_metis (tag1, m1) (tag2, m2) = app_if m1 (fn () => 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

253 
(log_me tag1 m1; log ""; app_if m2 (fn () => log_me tag2 m2))) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

254 
in 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

255 
if sh_calls > 0 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

256 
then 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

257 
(log ("\n\n\nReport #" ^ string_of_int id ^ ":\n"); 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

258 
log_sh_data log (tuple_of_sh_data sh); 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

259 
log ""; 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

260 
if not mini 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

261 
then log_metis ("", me_u) ("fullytyped ", me_uft) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

262 
else 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

263 
app_if me_u (fn () => 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

264 
(log_metis ("unminimized ", me_u) ("unminimized fullytyped ", me_uft); 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

265 
log ""; 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

266 
app_if me_m (fn () => 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

267 
(log_min_data log (tuple_of_min_data min); log ""; 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

268 
log_metis ("", me_m) ("fullytyped ", me_mft)))))) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

269 
else () 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

270 
end 
32521  271 

272 
end 

273 

274 

275 
(* Warning: we implicitly assume singlethreaded execution here! *) 

32740  276 
val data = Unsynchronized.ref ([] : (int * data) list) 
32521  277 

32740  278 
fun init id thy = (Unsynchronized.change data (cons (id, empty_data)); thy) 
32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset

279 
fun done id ({log, ...}: Mirabelle.done_args) = 
32521  280 
AList.lookup (op =) (!data) id 
281 
> Option.map (log_data id log) 

282 
> K () 

283 

32740  284 
fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ()) 
32521  285 

286 

32525  287 
fun get_atp thy args = 
33016
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

288 
let 
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

289 
fun default_atp_name () = hd (ATP_Manager.get_atps ()) 
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

290 
handle Empty => error "No ATP available." 
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

291 
fun get_prover name = 
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

292 
(case ATP_Manager.get_prover thy name of 
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

293 
SOME prover => (name, prover) 
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

294 
 NONE => error ("Bad ATP: " ^ quote name)) 
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

295 
in 
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

296 
(case AList.lookup (op =) args proverK of 
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

297 
SOME name => get_prover name 
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

298 
 NONE => get_prover (default_atp_name ())) 
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

299 
end 
32525  300 

32521  301 
local 
302 

32536  303 
datatype sh_result = 
304 
SH_OK of int * int * string list  

305 
SH_FAIL of int * int  

306 
SH_ERROR 

307 

32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32819
diff
changeset

308 
fun run_sh prover hard_timeout timeout dir st = 
32521  309 
let 
33292  310 
val {context = ctxt, facts, goal} = Proof.raw_goal st (* FIXME ?? *) 
33247  311 
val change_dir = (fn SOME d => Config.put ATP_Wrapper.destdir d  _ => I) 
312 
val ctxt' = 

313 
ctxt 

314 
> change_dir dir 

315 
> Config.put ATP_Wrapper.measure_runtime true 

33292  316 
val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal)); 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32819
diff
changeset

317 

32574
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

318 
val time_limit = 
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

319 
(case hard_timeout of 
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

320 
NONE => I 
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

321 
 SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) 
32985  322 
val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Wrapper.prover_result, 
323 
time_isa) = time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout 

32521  324 
in 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32819
diff
changeset

325 
if success then (message, SH_OK (time_isa, time_atp, theorem_names)) 
32536  326 
else (message, SH_FAIL(time_isa, time_atp)) 
32521  327 
end 
33316  328 
handle Res_HOL_Clause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, [])) 
32536  329 
 ERROR msg => ("error: " ^ msg, SH_ERROR) 
32574
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

330 
 TimeLimit.TimeOut => ("timeout", SH_ERROR) 
32521  331 

32454
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

332 
fun thms_of_name ctxt name = 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

333 
let 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

334 
val lex = OuterKeyword.get_lexicons 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

335 
val get = maps (ProofContext.get_fact ctxt o fst) 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

336 
in 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

337 
Source.of_string name 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

338 
> Symbol.source {do_recover=false} 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

339 
> OuterLex.source {do_recover=SOME false} lex Position.start 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

340 
> OuterLex.source_proper 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

341 
> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

342 
> Source.exhaust 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

343 
end 
32452
d84edd022efe
apply metis with found theorems in case sledgehammer was successful
boehmes
parents:
32434
diff
changeset

344 

32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset

345 
in 
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset

346 

32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset

347 
fun run_sledgehammer args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) = 
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

348 
let 
32536  349 
val _ = change_data id inc_sh_calls 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32819
diff
changeset

350 
val (prover_name, prover) = get_atp (Proof.theory_of st) args 
32525  351 
val dir = AList.lookup (op =) args keepK 
32541  352 
val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) 
32574
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

353 
val hard_timeout = AList.lookup (op =) args prover_hard_timeoutK 
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

354 
> Option.map (fst o read_int o explode) 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32819
diff
changeset

355 
val (msg, result) = run_sh prover hard_timeout timeout dir st 
32525  356 
in 
32536  357 
case result of 
358 
SH_OK (time_isa, time_atp, names) => 

32818  359 
let fun get_thms name = (name, thms_of_name (Proof.context_of st) name) 
32525  360 
in 
32818  361 
change_data id inc_sh_success; 
362 
change_data id (inc_sh_lemmas (length names)); 

363 
change_data id (inc_sh_max_lems (length names)); 

364 
change_data id (inc_sh_time_isa time_isa); 

365 
change_data id (inc_sh_time_atp time_atp); 

366 
named_thms := SOME (map get_thms names); 

32536  367 
log (sh_tag id ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ 
368 
string_of_int time_atp ^ ") [" ^ prover_name ^ "]:\n" ^ msg) 

32525  369 
end 
32536  370 
 SH_FAIL (time_isa, time_atp) => 
371 
let 

372 
val _ = change_data id (inc_sh_time_isa time_isa) 

373 
val _ = change_data id (inc_sh_time_atp_fail time_atp) 

374 
in log (sh_tag id ^ "failed: " ^ msg) end 

375 
 SH_ERROR => log (sh_tag id ^ "failed: " ^ msg) 

32525  376 
end 
377 

378 
end 

379 

32521  380 

32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset

381 
fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) = 
32525  382 
let 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

383 
val n0 = length (these (!named_thms)) 
32525  384 
val (prover_name, prover) = get_atp (Proof.theory_of st) args 
32936  385 
val minimize = ATP_Minimal.minimalize prover prover_name 
32525  386 
val timeout = 
387 
AList.lookup (op =) args minimize_timeoutK 

388 
> Option.map (fst o read_int o explode) 

389 
> the_default 5 

390 
val _ = log separator 

391 
in 

32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

392 
case minimize timeout st (these (!named_thms)) of 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

393 
(SOME (named_thms',its), msg) => 
32609  394 
(change_data id inc_min_succs; 
395 
change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0)); 

396 
change_data id (inc_min_it_ratios ((100*its) div n0)); 

32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

397 
if length named_thms' = n0 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

398 
then log (minimize_tag id ^ "already minimal") 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

399 
else (named_thms := SOME named_thms'; 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

400 
log (minimize_tag id ^ "succeeded:\n" ^ msg)) 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

401 
) 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

402 
 (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg) 
32525  403 
end 
404 

405 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

406 
fun run_metis full m name named_thms id 
32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset

407 
({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = 
32525  408 
let 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

409 
fun metis thms ctxt = 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

410 
if full then MetisTools.metisFT_tac ctxt thms 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

411 
else MetisTools.metis_tac ctxt thms 
32521  412 
fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st 
413 

414 
fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

415 
 with_time (true, t) = (change_data id (inc_metis_success m); 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

416 
change_data id (inc_metis_lemmas m (length named_thms)); 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

417 
change_data id (inc_metis_time m t); 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

418 
change_data id (inc_metis_posns m pos); 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

419 
if name = "proof" then change_data id (inc_metis_proofs m) else (); 
32521  420 
"succeeded (" ^ string_of_int t ^ ")") 
421 
fun timed_metis thms = with_time (Mirabelle.cpu_time apply_metis thms) 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

422 
handle TimeLimit.TimeOut => (change_data id (inc_metis_timeout m); "timeout") 
32521  423 
 ERROR msg => "error: " ^ msg 
424 

32525  425 
val _ = log separator 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

426 
val _ = change_data id (inc_metis_calls m) 
32521  427 
in 
32525  428 
maps snd named_thms 
32521  429 
> timed_metis 
430 
> log o prefix (metis_tag id) 

431 
end 

32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

432 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

433 
fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) = 
33292  434 
let val goal = Thm.major_prem_of (#goal (Proof.raw_goal pre)) (* FIXME ?? *) in 
32818  435 
if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal 
32607  436 
then () else 
32515
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32511
diff
changeset

437 
let 
32740  438 
val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option) 
32612  439 
val minimize = AList.defined (op =) args minimizeK 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

440 
val metis_ft = AList.defined (op =) args metis_ftK 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

441 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

442 
fun apply_metis m1 m2 = 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

443 
if metis_ft 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

444 
then 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

445 
Mirabelle.app_timeout metis_tag 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

446 
(run_metis false m1 name (these (!named_thms))) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

447 
(Mirabelle.catch metis_tag 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

448 
(run_metis true m2 name (these (!named_thms)))) id st 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

449 
else 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

450 
Mirabelle.catch metis_tag 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

451 
(run_metis false m1 name (these (!named_thms))) id st 
32612  452 
in 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

453 
change_data id (set_mini minimize); 
32612  454 
Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st; 
455 
if is_some (!named_thms) 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

456 
then 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

457 
(apply_metis Unminimized UnminimizedFT; 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

458 
if minimize andalso not (null (these (!named_thms))) 
32612  459 
then 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

460 
(Mirabelle.catch minimize_tag (run_minimize args named_thms) id st; 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

461 
apply_metis Minimized MinimizedFT) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

462 
else ()) 
32612  463 
else () 
464 
end 

32818  465 
end 
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

466 

32511  467 
fun invoke args = 
32515
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32511
diff
changeset

468 
let 
32937
34f66c9dd8a2
structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32936
diff
changeset

469 
val _ = ATP_Manager.full_types := AList.defined (op =) args full_typesK 
32521  470 
in Mirabelle.register (init, sledgehammer_action args, done) end 
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

471 

594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

472 
end 