1(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
2    Author:     Steffen Juilf Smolka, TU Muenchen
3    Author:     Jasmin Blanchette, TU Muenchen
4
5Minimize dependencies (used facts) of Isar proof steps.
6*)
7
8signature SLEDGEHAMMER_ISAR_MINIMIZE =
9sig
10  type isar_step = Sledgehammer_Isar_Proof.isar_step
11  type isar_proof = Sledgehammer_Isar_Proof.isar_proof
12  type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
13
14  val keep_fastest_method_of_isar_step : isar_preplay_data -> isar_step -> isar_step
15  val minimized_isar_step : Proof.context -> thm list -> Time.time -> isar_step ->
16    Time.time * isar_step
17  val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref ->
18    isar_step -> isar_step
19  val postprocess_isar_proof_remove_show_stuttering : isar_proof -> isar_proof
20  val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof ->
21    isar_proof
22end;
23
24structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE =
25struct
26
27open Sledgehammer_Util
28open Sledgehammer_Proof_Methods
29open Sledgehammer_Isar_Proof
30open Sledgehammer_Isar_Preplay
31
32fun keep_fastest_method_of_isar_step preplay_data
33      (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) =
34    Prove (qs, xs, l, t, subproofs, facts,
35      meths |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) |> op @,
36      comment)
37  | keep_fastest_method_of_isar_step _ step = step
38
39val slack = seconds 0.025
40
41fun minimized_isar_step ctxt chained time
42    (Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) =
43  let
44    fun mk_step_lfs_gfs lfs gfs =
45      Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), meths, comment)
46
47    fun minimize_half _ min_facts [] time = (min_facts, time)
48      | minimize_half mk_step min_facts (fact :: facts) time =
49        (case preplay_isar_step_for_method ctxt chained (time + slack) meth
50            (mk_step (min_facts @ facts)) of
51          Played time' => minimize_half mk_step min_facts facts time'
52        | _ => minimize_half mk_step (fact :: min_facts) facts time)
53
54    val (min_lfs, time') = minimize_half (fn lfs => mk_step_lfs_gfs lfs gfs0) [] lfs0 time
55    val (min_gfs, time'') = minimize_half (mk_step_lfs_gfs min_lfs) [] gfs0 time'
56  in
57    (time'', mk_step_lfs_gfs min_lfs min_gfs)
58  end
59
60fun minimize_isar_step_dependencies ctxt preplay_data
61      (step as Prove (_, _, l, _, _, _, meth :: meths, _)) =
62    (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
63      Played time =>
64      let
65        fun old_data_for_method meth' =
66          (meth', peek_at_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth'))
67
68        val (time', step') = minimized_isar_step ctxt [] time step
69      in
70        set_preplay_outcomes_of_isar_step ctxt time' preplay_data step'
71          ((meth, Played time') :: (if step' = step then map old_data_for_method meths else []));
72        step'
73      end
74    | _ => step (* don't touch steps that time out or fail *))
75  | minimize_isar_step_dependencies _ _ step = step
76
77fun postprocess_isar_proof_remove_show_stuttering (Proof (fix, assms, steps)) =
78  let
79    fun process_steps [] = []
80      | process_steps (steps as [Prove ([], [], _, t1, subs1, facts1, meths1, comment1),
81          Prove ([Show], [], l2, t2, _, _, _, comment2)]) =
82        if t1 aconv t2 then [Prove ([Show], [], l2, t2, subs1, facts1, meths1, comment1 ^ comment2)]
83        else steps
84      | process_steps (step :: steps) = step :: process_steps steps
85  in
86    Proof (fix, assms, process_steps steps)
87  end
88
89fun postprocess_isar_proof_remove_unreferenced_steps postproc_step =
90  let
91    fun process_proof (Proof (fix, assms, steps)) =
92      process_steps steps ||> (fn steps => Proof (fix, assms, steps))
93    and process_steps [] = ([], [])
94      | process_steps steps =
95        (* the last step is always implicitly referenced *)
96        let val (steps, (used, concl)) = split_last steps ||> process_used_step in
97          fold_rev process_step steps (used, [concl])
98        end
99    and process_step step (used, accu) =
100      (case label_of_isar_step step of
101        NONE => (used, step :: accu)
102      | SOME l =>
103        if Ord_List.member label_ord used l then
104          process_used_step step |>> Ord_List.union label_ord used ||> (fn step => step :: accu)
105        else
106          (used, accu))
107    and process_used_step step = process_used_step_subproofs (postproc_step step)
108    and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) =
109      let
110        val (used, subproofs) =
111          map process_proof subproofs
112          |> split_list
113          |>> Ord_List.unions label_ord
114          |>> fold (Ord_List.insert label_ord) lfs
115      in
116        (used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment))
117      end
118  in
119    snd o process_proof
120  end
121
122end;
123