9 sig |
9 sig |
10 type isar_step = Sledgehammer_Isar_Proof.isar_step |
10 type isar_step = Sledgehammer_Isar_Proof.isar_step |
11 type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
11 type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
12 type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data |
12 type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data |
13 |
13 |
|
14 val keep_fastest_method_of_isar_step : isar_preplay_data -> isar_step -> isar_step |
14 val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref -> |
15 val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref -> |
15 isar_step -> isar_step |
16 isar_step -> isar_step |
16 val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> |
17 val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> |
17 isar_proof |
18 isar_proof |
18 end; |
19 end; |
22 |
23 |
23 open Sledgehammer_Reconstructor |
24 open Sledgehammer_Reconstructor |
24 open Sledgehammer_Isar_Proof |
25 open Sledgehammer_Isar_Proof |
25 open Sledgehammer_Isar_Preplay |
26 open Sledgehammer_Isar_Preplay |
26 |
27 |
|
28 fun keep_fastest_method_of_isar_step preplay_data |
|
29 (Prove (qs, xs, l, t, subproofs, (facts, _))) = |
|
30 Prove (qs, xs, l, t, subproofs, (facts, [fastest_method_of_isar_step preplay_data l])) |
|
31 | keep_fastest_method_of_isar_step _ step = step |
|
32 |
27 val slack = seconds 0.1 |
33 val slack = seconds 0.1 |
28 |
34 |
29 fun minimize_isar_step_dependencies _ _ (step as Let _) = step |
35 fun minimize_isar_step_dependencies ctxt preplay_data |
30 | minimize_isar_step_dependencies ctxt preplay_data |
|
31 (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) = |
36 (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) = |
32 (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of |
37 (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of |
33 Played time => |
38 Played time => |
34 let |
39 let |
35 fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths)) |
40 fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths)) |
36 |
41 |
37 fun minimize_facts _ time min_facts [] = (time, min_facts) |
42 fun minimize_facts _ time min_facts [] = (time, min_facts) |
49 set_preplay_outcomes_of_isar_step ctxt time preplay_data step' |
54 set_preplay_outcomes_of_isar_step ctxt time preplay_data step' |
50 [(meth, Lazy.value (Played time))]; |
55 [(meth, Lazy.value (Played time))]; |
51 step' |
56 step' |
52 end |
57 end |
53 | _ => step (* don't touch steps that time out or fail *)) |
58 | _ => step (* don't touch steps that time out or fail *)) |
|
59 | minimize_isar_step_dependencies _ _ step = step |
54 |
60 |
55 fun postprocess_isar_proof_remove_unreferenced_steps postproc_step = |
61 fun postprocess_isar_proof_remove_unreferenced_steps postproc_step = |
56 let |
62 let |
57 fun process_proof (Proof (fix, assms, steps)) = |
63 fun process_proof (Proof (fix, assms, steps)) = |
58 process_steps steps ||> (fn steps => Proof (fix, assms, steps)) |
64 process_steps steps ||> (fn steps => Proof (fix, assms, steps)) |