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