author | blanchet |
Fri, 31 Jan 2014 10:23:32 +0100 | |
changeset 55202 | 824c48a539c9 |
parent 54828 | src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML@b2271ad695db |
child 55212 | 5832470d956e |
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 |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
12 |
type preplay_interface = Sledgehammer_Isar_Preplay.preplay_interface |
52592 | 13 |
|
14 |
val try0 : Time.time -> preplay_interface -> 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 |
54828 | 33 |
({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_interface) |
54712 | 34 |
(step as Prove (_, _, l, _, _, _)) = |
35 |
let |
|
36 |
val timeout = |
|
54828 | 37 |
(case get_preplay_outcome l of |
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 |
|
54828 | 47 |
SOME (step', result) => (set_preplay_outcome l result; step') |
54712 | 48 |
| NONE => step) |
49 |
end |
|
52592 | 50 |
|
54712 | 51 |
val try0 = map_isar_steps oo try0_step |
52592 | 52 |
|
54504 | 53 |
end; |