author | blanchet |
Fri, 31 Jan 2014 19:16:41 +0100 | |
changeset 55223 | 3c593bad6b31 |
parent 55221 | ee90eebb8b73 |
child 55243 | 66709d41601e |
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 |
|
54767
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
25 |
fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, methss))) = |
81290fe85890
generalize method list further to list of list (clustering preferred methods together)
blanchet
parents:
54766
diff
changeset
|
26 |
map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [[meth]]))) (tl (flat methss)) |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
27 |
| variants_of_step _ = raise Fail "Sledgehammer_Isar_Try0: variants_of_step" |
54712 | 28 |
|
29 |
val slack = seconds 0.05 |
|
52592 | 30 |
|
52612 | 31 |
fun try0_step _ _ (step as Let _) = step |
54712 | 32 |
| try0_step preplay_timeout |
55221 | 33 |
({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) |
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
34 |
(step as Prove (_, _, l, _, _, (_, (meth :: _) :: _))) = |
54712 | 35 |
let |
36 |
val timeout = |
|
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
37 |
(case Lazy.force (preplay_outcome l meth) of |
54828 | 38 |
Played time => Time.+ (time, slack) |
54826 | 39 |
| _ => preplay_timeout) |
52592 | 40 |
|
54712 | 41 |
fun try_variant variant = |
42 |
(case preplay_quietly timeout variant of |
|
54828 | 43 |
result as Played _ => SOME (variant, result) |
54827 | 44 |
| _ => NONE) |
54712 | 45 |
in |
46 |
(case Par_List.get_some try_variant (variants_of_step step) of |
|
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
47 |
SOME (step' as Prove (_, _, _, _, _, (_, (meth' :: _) :: _)), result) => |
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
48 |
(set_preplay_outcome l meth' result; 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; |