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