52592
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_try0.ML
|
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
|
3 |
Author: Steffen Juilf Smolka, TU Muenchen
|
|
4 |
|
|
5 |
Try replacing calls to metis with calls to other proof methods in order to
|
|
6 |
speed up proofs, eliminate dependencies, and repair broken proof steps.
|
|
7 |
*)
|
|
8 |
|
|
9 |
signature SLEDGEHAMMER_TRY0 =
|
|
10 |
sig
|
|
11 |
type isar_proof = Sledgehammer_Proof.isar_proof
|
|
12 |
type preplay_interface = Sledgehammer_Preplay.preplay_interface
|
|
13 |
|
|
14 |
val try0 : Time.time -> preplay_interface -> isar_proof -> isar_proof
|
54504
|
15 |
end;
|
52592
|
16 |
|
|
17 |
structure Sledgehammer_Try0 : SLEDGEHAMMER_TRY0 =
|
|
18 |
struct
|
|
19 |
|
54712
|
20 |
open Sledgehammer_Util
|
52592
|
21 |
open Sledgehammer_Proof
|
|
22 |
open Sledgehammer_Preplay
|
|
23 |
|
54712
|
24 |
val variant_methods = [SimpM, AutoM, ArithM, FastforceM, BlastM, ForceM, MetisM]
|
|
25 |
|
|
26 |
fun variants_of_step (Let _) = raise Fail "Sledgehammer_Try0: variants_of_step"
|
|
27 |
| variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, meth))) =
|
|
28 |
variant_methods
|
|
29 |
|> remove (op =) meth
|
|
30 |
|> map (fn meth' => Prove (qs, xs, l, t, subproofs, (facts, meth')))
|
|
31 |
|
|
32 |
val slack = seconds 0.05
|
52592
|
33 |
|
52612
|
34 |
fun try0_step _ _ (step as Let _) = step
|
54712
|
35 |
| try0_step preplay_timeout
|
|
36 |
({preplay_quietly, get_preplay_time, set_preplay_time, ...} : preplay_interface)
|
|
37 |
(step as Prove (_, _, l, _, _, _)) =
|
|
38 |
let
|
|
39 |
val timeout =
|
|
40 |
(case get_preplay_time l of
|
|
41 |
(true, _) => preplay_timeout
|
|
42 |
| (false, t) => Time.+ (t, slack))
|
52592
|
43 |
|
54712
|
44 |
fun try_variant variant =
|
|
45 |
(case preplay_quietly timeout variant of
|
|
46 |
(true, _) => NONE
|
|
47 |
| time as (false, _) => SOME (variant, time))
|
|
48 |
in
|
|
49 |
(case Par_List.get_some try_variant (variants_of_step step) of
|
|
50 |
SOME (step, time) => (set_preplay_time l time; step)
|
|
51 |
| NONE => step)
|
|
52 |
end
|
52592
|
53 |
|
54712
|
54 |
val try0 = map_isar_steps oo try0_step
|
52592
|
55 |
|
54504
|
56 |
end;
|