author | boehmes |
Sat, 05 Sep 2009 11:45:57 +0200 | |
changeset 32521 | f20cc66b2c74 |
parent 32518 | e3c4e337196c |
child 32523 | ba397aa0ff5d |
permissions | -rw-r--r-- |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
1 |
(* Title: mirabelle_sledgehammer.ML |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette and Sascha Boehme |
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" |
9 |
val keepK = "keep" |
|
10 |
val metisK = "metis" |
|
11 |
val full_typesK = "full_types" |
|
12 |
||
13 |
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " |
|
14 |
fun metis_tag id = "#" ^ string_of_int id ^ " metis (sledgehammer): " |
|
15 |
||
16 |
||
17 |
datatype data = Data of { |
|
18 |
sh_calls: int, |
|
19 |
sh_success: int, |
|
20 |
sh_time: int, |
|
21 |
metis_calls: int, |
|
22 |
metis_success: int, |
|
23 |
metis_time: int, |
|
24 |
metis_timeout: int } |
|
25 |
||
26 |
fun make_data (sh_calls, sh_success, sh_time, metis_calls, metis_success, |
|
27 |
metis_time, metis_timeout) = |
|
28 |
Data {sh_calls=sh_calls, sh_success=sh_success, sh_time=sh_time, |
|
29 |
metis_calls=metis_calls, metis_success=metis_success, |
|
30 |
metis_time=metis_time, metis_timeout=metis_timeout} |
|
31 |
||
32 |
fun map_data f (Data {sh_calls, sh_success, sh_time, metis_calls, |
|
33 |
metis_success, metis_time, metis_timeout}) = |
|
34 |
make_data (f (sh_calls, sh_success, sh_time, metis_calls, metis_success, |
|
35 |
metis_time, metis_timeout)) |
|
36 |
||
37 |
val empty_data = make_data (0, 0, 0, 0, 0, 0, 0) |
|
38 |
||
39 |
val inc_sh_calls = map_data (fn (sh_calls, sh_success, sh_time, metis_calls, |
|
40 |
metis_success, metis_time, metis_timeout) => (sh_calls + 1, sh_success, |
|
41 |
sh_time, metis_calls, metis_success, metis_time, metis_timeout)) |
|
42 |
||
43 |
val inc_sh_success = map_data (fn (sh_calls, sh_success, sh_time, metis_calls, |
|
44 |
metis_success, metis_time, metis_timeout) => (sh_calls, sh_success + 1, |
|
45 |
sh_time, metis_calls, metis_success, metis_time, metis_timeout)) |
|
46 |
||
47 |
fun inc_sh_time t = map_data (fn (sh_calls, sh_success, sh_time, metis_calls, |
|
48 |
metis_success, metis_time, metis_timeout) => (sh_calls, sh_success, |
|
49 |
sh_time + t, metis_calls, metis_success, metis_time, metis_timeout)) |
|
50 |
||
51 |
val inc_metis_calls = map_data (fn (sh_calls, sh_success, sh_time, metis_calls, |
|
52 |
metis_success, metis_time, metis_timeout) => (sh_calls, sh_success, |
|
53 |
sh_time, metis_calls + 1, metis_success, metis_time, metis_timeout)) |
|
54 |
||
55 |
val inc_metis_success = map_data (fn (sh_calls, sh_success, sh_time, |
|
56 |
metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls, |
|
57 |
sh_success, sh_time, metis_calls, metis_success + 1, metis_time, |
|
58 |
metis_timeout)) |
|
59 |
||
60 |
fun inc_metis_time t = map_data (fn (sh_calls, sh_success, sh_time, |
|
61 |
metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls, |
|
62 |
sh_success, sh_time, metis_calls, metis_success, metis_time + t, |
|
63 |
metis_timeout)) |
|
64 |
||
65 |
val inc_metis_timeout = map_data (fn (sh_calls, sh_success, sh_time, |
|
66 |
metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls, |
|
67 |
sh_success, sh_time, metis_calls, metis_success, metis_time, |
|
68 |
metis_timeout + 1)) |
|
69 |
||
70 |
||
71 |
local |
|
72 |
||
73 |
val str = string_of_int |
|
74 |
val str3 = Real.fmt (StringCvt.FIX (SOME 3)) |
|
75 |
fun percentage a b = string_of_int (a * 100 div b) |
|
76 |
fun time t = Real.fromInt t / 1000.0 |
|
77 |
fun avg_time t n = |
|
78 |
if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 |
|
79 |
||
80 |
fun log_sh_data log sh_calls sh_success sh_time = |
|
81 |
(log ("Total number of sledgehammer calls: " ^ str sh_calls); |
|
82 |
log ("Number of successful sledgehammer calls: " ^ str sh_success); |
|
83 |
log ("Success rate: " ^ percentage sh_success sh_calls ^ "%"); |
|
84 |
log ("Total time for successful sledgehammer calls: " ^ str3 (time sh_time)); |
|
85 |
log ("Average time for successful sledgehammer calls: " ^ |
|
86 |
str3 (avg_time sh_time sh_success))) |
|
87 |
||
88 |
fun log_metis_data log sh_success metis_calls metis_success metis_time |
|
89 |
metis_timeout = |
|
90 |
(log ("Total number of metis calls: " ^ str metis_calls); |
|
91 |
log ("Number of successful metis calls: " ^ str metis_success); |
|
92 |
log ("Number of metis timeouts: " ^ str metis_timeout); |
|
93 |
log ("Number of metis exceptions: " ^ |
|
94 |
str (sh_success - metis_success - metis_timeout)); |
|
95 |
log ("Success rate: " ^ percentage metis_success metis_calls ^ "%"); |
|
96 |
log ("Total time for successful metis calls: " ^ str3 (time metis_time)); |
|
97 |
log ("Average time for successful metis calls: " ^ |
|
98 |
str3 (avg_time metis_time metis_success))) |
|
99 |
||
100 |
in |
|
101 |
||
102 |
fun log_data id log (Data {sh_calls, sh_success, sh_time, metis_calls, |
|
103 |
metis_success, metis_time, metis_timeout}) = |
|
104 |
if sh_calls > 0 |
|
105 |
then |
|
106 |
(log ("\n\n\nReport #" ^ string_of_int id ^ ":\n"); |
|
107 |
log_sh_data log sh_calls sh_success sh_time; |
|
108 |
log ""; |
|
109 |
if metis_calls > 0 then log_metis_data log sh_success metis_calls |
|
110 |
metis_success metis_time metis_timeout else ()) |
|
111 |
else () |
|
112 |
||
113 |
end |
|
114 |
||
115 |
||
116 |
(* Warning: we implicitly assume single-threaded execution here! *) |
|
117 |
val data = ref ([] : (int * data) list) |
|
118 |
||
119 |
fun init id thy = (change data (cons (id, empty_data)); thy) |
|
120 |
fun done id {log, ...} = |
|
121 |
AList.lookup (op =) (!data) id |
|
122 |
|> Option.map (log_data id log) |
|
123 |
|> K () |
|
124 |
||
125 |
fun change_data id f = (change data (AList.map_entry (op =) id f); ()) |
|
126 |
||
127 |
||
128 |
local |
|
129 |
||
130 |
fun safe init done f x = |
|
131 |
let |
|
132 |
val y = init x |
|
133 |
val z = Exn.capture f y |
|
134 |
val _ = done y |
|
135 |
in Exn.release z end |
|
136 |
||
137 |
fun init_sh NONE = !AtpWrapper.destdir |
|
138 |
| init_sh (SOME path) = |
|
139 |
let |
|
140 |
(* Warning: we implicitly assume single-threaded execution here! *) |
|
141 |
val old = !AtpWrapper.destdir |
|
142 |
val _ = AtpWrapper.destdir := path |
|
143 |
in old end |
|
144 |
||
145 |
fun done_sh path = AtpWrapper.destdir := path |
|
146 |
||
147 |
fun run_sh prover_name timeout st _ = |
|
148 |
let |
|
149 |
val prover = the (AtpManager.get_prover prover_name (Proof.theory_of st)) |
|
150 |
val atp_timeout = AtpManager.get_timeout () |
|
151 |
val atp = prover atp_timeout NONE NONE prover_name 1 |
|
152 |
val ((success, (message, thm_names), time, _, _, _), time') = |
|
153 |
TimeLimit.timeLimit timeout (Mirabelle.cpu_time atp) (Proof.get_goal st) |
|
154 |
in |
|
155 |
if success then (message, SOME (time + time', thm_names)) |
|
156 |
else (message, NONE) |
|
157 |
end |
|
158 |
handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, [])) |
|
159 |
| TimeLimit.TimeOut => ("timeout", NONE) |
|
160 |
| ERROR msg => ("error: " ^ msg, NONE) |
|
161 |
||
162 |
in |
|
163 |
||
164 |
fun run_sledgehammer args thm_names id {pre=st, timeout, log, ...} = |
|
165 |
let |
|
166 |
val _ = change_data id inc_sh_calls |
|
167 |
val prover_name = |
|
168 |
AList.lookup (op =) args proverK |
|
169 |
|> the_default (hd (space_explode " " (AtpManager.get_atps ()))) |
|
170 |
val dir = AList.lookup (op =) args keepK |
|
171 |
val (msg, result) = |
|
172 |
safe init_sh done_sh (run_sh prover_name timeout st) dir |
|
173 |
val _ = |
|
174 |
if is_some result |
|
175 |
then |
|
176 |
let |
|
177 |
val time = fst (the result) |
|
178 |
val _ = change_data id inc_sh_success |
|
179 |
val _ = change_data id (inc_sh_time time) |
|
180 |
in |
|
181 |
log (sh_tag id ^ "succeeded (" ^ string_of_int time ^ ") [" ^ |
|
182 |
prover_name ^ "]:\n" ^ msg) |
|
183 |
end |
|
184 |
else log (sh_tag id ^ "failed: " ^ msg) |
|
185 |
in change thm_names (K (Option.map snd result)) end |
|
186 |
||
187 |
end |
|
188 |
||
189 |
||
190 |
local |
|
191 |
||
32454
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset
|
192 |
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
|
193 |
let |
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset
|
194 |
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
|
195 |
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
|
196 |
in |
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset
|
197 |
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
|
198 |
|> 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
|
199 |
|> 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
|
200 |
|> 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
|
201 |
|> 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
|
202 |
|> 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
|
203 |
end |
32452
d84edd022efe
apply metis with found theorems in case sledgehammer was successful
boehmes
parents:
32434
diff
changeset
|
204 |
|
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
205 |
in |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
206 |
|
32521 | 207 |
fun run_metis args thm_names id {pre=st, timeout, log, ...} = |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
208 |
let |
32521 | 209 |
fun get_thms ctxt = maps (thms_of_name ctxt) |
210 |
||
211 |
fun metis thms ctxt = MetisTools.metis_tac ctxt thms |
|
212 |
fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st |
|
213 |
||
214 |
fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" |
|
215 |
| with_time (true, t) = (change_data id inc_metis_success; |
|
216 |
change_data id (inc_metis_time t); |
|
217 |
"succeeded (" ^ string_of_int t ^ ")") |
|
218 |
fun timed_metis thms = with_time (Mirabelle.cpu_time apply_metis thms) |
|
219 |
handle TimeLimit.TimeOut => (change_data id inc_metis_timeout; "timeout") |
|
220 |
| ERROR msg => "error: " ^ msg |
|
221 |
||
222 |
val _ = log "-----" |
|
223 |
val _ = change_data id inc_metis_calls |
|
224 |
in |
|
225 |
thm_names |
|
226 |
|> get_thms (Proof.context_of st) |
|
227 |
|> timed_metis |
|
228 |
|> log o prefix (metis_tag id) |
|
229 |
end |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
230 |
|
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
231 |
end |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
232 |
|
32452
d84edd022efe
apply metis with found theorems in case sledgehammer was successful
boehmes
parents:
32434
diff
changeset
|
233 |
|
32521 | 234 |
fun sledgehammer_action args id (st as {log, ...}) = |
32515
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32511
diff
changeset
|
235 |
let |
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32511
diff
changeset
|
236 |
val thm_names = ref (NONE : string list option) |
32521 | 237 |
val _ = Mirabelle.catch sh_tag (run_sledgehammer args thm_names) id st |
238 |
in |
|
239 |
if AList.defined (op =) args metisK andalso is_some (!thm_names) |
|
240 |
then Mirabelle.catch metis_tag (run_metis args (these (!thm_names))) id st |
|
241 |
else () |
|
242 |
end |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
243 |
|
32511 | 244 |
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
|
245 |
let |
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32511
diff
changeset
|
246 |
val _ = AtpManager.set_full_types (AList.defined (op =) args full_typesK) |
32521 | 247 |
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
|
248 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
249 |
end |