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 minimize_isar_step_dependencies : isar_preplay_data -> isar_step -> isar_step |
14 val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data -> isar_step -> isar_step |
15 val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> |
15 val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> |
16 isar_proof |
16 isar_proof |
17 end; |
17 end; |
18 |
18 |
19 structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE = |
19 structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE = |
23 open Sledgehammer_Isar_Proof |
23 open Sledgehammer_Isar_Proof |
24 open Sledgehammer_Isar_Preplay |
24 open Sledgehammer_Isar_Preplay |
25 |
25 |
26 val slack = seconds 0.1 |
26 val slack = seconds 0.1 |
27 |
27 |
28 fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step |
28 fun minimize_isar_step_dependencies _ (_ : isar_preplay_data) (step as Let _) = step |
29 | minimize_isar_step_dependencies {preplay_step, set_preplay_outcomes, preplay_outcome, ...} |
29 | minimize_isar_step_dependencies ctxt {set_preplay_outcomes, preplay_outcome, ...} |
30 (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) = |
30 (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) = |
31 (case Lazy.force (preplay_outcome l meth) of |
31 (case Lazy.force (preplay_outcome l meth) of |
32 Played time => |
32 Played time => |
33 let |
33 let |
34 fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths)) |
34 fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths)) |
35 val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs) |
35 val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs) |
36 |
36 |
37 fun minimize_facts _ time min_facts [] = (time, min_facts) |
37 fun minimize_facts _ time min_facts [] = (time, min_facts) |
38 | minimize_facts mk_step time min_facts (f :: facts) = |
38 | minimize_facts mk_step time min_facts (f :: facts) = |
39 (case preplay_step (Time.+ (time, slack)) meth (mk_step (min_facts @ facts)) of |
39 (case preplay_isar_step ctxt (Time.+ (time, slack)) meth |
|
40 (mk_step (min_facts @ facts)) of |
40 Played time => minimize_facts mk_step time min_facts facts |
41 Played time => minimize_facts mk_step time min_facts facts |
41 | _ => minimize_facts mk_step time (f :: min_facts) facts) |
42 | _ => minimize_facts mk_step time (f :: min_facts) facts) |
42 |
43 |
43 val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs |
44 val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs |
44 val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs |
45 val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs |