author | blanchet |
Sun, 02 Feb 2014 20:53:51 +0100 | |
changeset 55255 | eceebcea3e00 |
parent 55252 | 0dc4993b4f56 |
child 55258 | 8cc42c1f9bb5 |
permissions | -rw-r--r-- |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML |
52592 | 2 |
Author: Steffen Juilf Smolka, TU Muenchen |
54766
6ac273f176cd
store alternative proof methods in Isar data structure
blanchet
parents:
54765
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
52592 | 4 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
5 |
Try replacing calls to "metis" with calls to other proof methods to speed up proofs, eliminate |
54766
6ac273f176cd
store alternative proof methods in Isar data structure
blanchet
parents:
54765
diff
changeset
|
6 |
dependencies, and repair broken proof steps. |
52592 | 7 |
*) |
8 |
||
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
9 |
signature SLEDGEHAMMER_ISAR_TRY0 = |
52592 | 10 |
sig |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
11 |
type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
55213 | 12 |
type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data |
52592 | 13 |
|
55213 | 14 |
val try0_isar_proof : Time.time -> isar_preplay_data -> isar_proof -> isar_proof |
54504 | 15 |
end; |
52592 | 16 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
17 |
structure Sledgehammer_Isar_Try0 : SLEDGEHAMMER_ISAR_TRY0 = |
52592 | 18 |
struct |
19 |
||
54712 | 20 |
open Sledgehammer_Util |
54828 | 21 |
open Sledgehammer_Reconstructor |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
22 |
open Sledgehammer_Isar_Proof |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
23 |
open Sledgehammer_Isar_Preplay |
52592 | 24 |
|
55255 | 25 |
fun step_with_method meth (Prove (qs, xs, l, t, subproofs, (facts, _))) = |
26 |
Prove (qs, xs, l, t, subproofs, (facts, [meth])) |
|
54712 | 27 |
|
28 |
val slack = seconds 0.05 |
|
52592 | 29 |
|
52612 | 30 |
fun try0_step _ _ (step as Let _) = step |
54712 | 31 |
| try0_step preplay_timeout |
55255 | 32 |
({preplay_step, set_preplay_outcomes, preplay_outcome, ...} : isar_preplay_data) |
33 |
(step as Prove (_, _, l, _, _, (_, meths as meth :: _))) = |
|
54712 | 34 |
let |
35 |
val timeout = |
|
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
36 |
(case Lazy.force (preplay_outcome l meth) of |
54828 | 37 |
Played time => Time.+ (time, slack) |
54826 | 38 |
| _ => preplay_timeout) |
52592 | 39 |
|
55255 | 40 |
fun try_method meth = |
41 |
(case preplay_step timeout meth step of |
|
42 |
outcome as Played _ => SOME (meth, outcome) |
|
54827 | 43 |
| _ => NONE) |
54712 | 44 |
in |
55243 | 45 |
(* FIXME: create variant after success *) |
55255 | 46 |
(case Par_List.get_some try_method meths of |
47 |
SOME (meth', outcome) => |
|
48 |
(set_preplay_outcomes l [(meth', Lazy.value outcome)]; step_with_method meth' step) |
|
54712 | 49 |
| NONE => step) |
50 |
end |
|
52592 | 51 |
|
55212 | 52 |
val try0_isar_proof = map_isar_steps oo try0_step |
52592 | 53 |
|
54504 | 54 |
end; |