author | blanchet |
Sun, 02 Feb 2014 20:53:51 +0100 | |
changeset 55244 | 12e1a5d8ee48 |
parent 55243 | 66709d41601e |
child 55252 | 0dc4993b4f56 |
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 |
|
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55243
diff
changeset
|
25 |
fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, meths))) = |
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55243
diff
changeset
|
26 |
map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [meth]))) (tl meths) |
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) |
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55243
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 |
55243 | 46 |
(* FIXME: create variant after success *) |
54712 | 47 |
(case Par_List.get_some try_variant (variants_of_step step) of |
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55243
diff
changeset
|
48 |
SOME (step' as Prove (_, _, _, _, _, (_, meth' :: _)), result) => |
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
49 |
(set_preplay_outcome l meth' result; step') |
54712 | 50 |
| NONE => step) |
51 |
end |
|
52592 | 52 |
|
55212 | 53 |
val try0_isar_proof = map_isar_steps oo try0_step |
52592 | 54 |
|
54504 | 55 |
end; |