1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML |
|
2 Author: Steffen Juilf Smolka, TU Muenchen |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 |
|
5 Try replacing calls to "metis" with calls to other proof methods to speed up proofs, eliminate |
|
6 dependencies, and repair broken proof steps. |
|
7 *) |
|
8 |
|
9 signature SLEDGEHAMMER_ISAR_TRY0 = |
|
10 sig |
|
11 type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
|
12 type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data |
|
13 |
|
14 val try0_isar_proof : Proof.context -> Time.time -> isar_preplay_data Unsynchronized.ref -> |
|
15 isar_proof -> isar_proof |
|
16 end; |
|
17 |
|
18 structure Sledgehammer_Isar_Try0 : SLEDGEHAMMER_ISAR_TRY0 = |
|
19 struct |
|
20 |
|
21 open Sledgehammer_Util |
|
22 open Sledgehammer_Reconstructor |
|
23 open Sledgehammer_Isar_Proof |
|
24 open Sledgehammer_Isar_Preplay |
|
25 |
|
26 fun step_with_method meth (Prove (qs, xs, l, t, subproofs, (facts, _))) = |
|
27 Prove (qs, xs, l, t, subproofs, (facts, [meth])) |
|
28 |
|
29 val slack = seconds 0.05 |
|
30 |
|
31 fun try0_step _ _ _ (step as Let _) = step |
|
32 | try0_step ctxt preplay_timeout preplay_data |
|
33 (step as Prove (_, _, l, _, _, (_, meths as meth :: _))) = |
|
34 let |
|
35 val timeout = |
|
36 (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of |
|
37 Played time => Time.+ (time, slack) |
|
38 | _ => preplay_timeout) |
|
39 |
|
40 fun try_method meth = |
|
41 (case preplay_isar_step ctxt timeout meth step of |
|
42 outcome as Played _ => SOME (meth, outcome) |
|
43 | _ => NONE) |
|
44 in |
|
45 (* FIXME: create variant after success *) |
|
46 (case Par_List.get_some try_method meths of |
|
47 SOME (meth', outcome) => |
|
48 let val step' = step_with_method meth' step in |
|
49 (set_preplay_outcomes_of_isar_step ctxt timeout preplay_data step' |
|
50 [(meth', Lazy.value outcome)]; |
|
51 step') |
|
52 end |
|
53 | NONE => step) |
|
54 end |
|
55 |
|
56 val try0_isar_proof = map_isar_steps ooo try0_step |
|
57 |
|
58 end; |
|