1(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML 2 Author: Steffen Juilf Smolka, TU Muenchen 3 Author: Jasmin Blanchette, TU Muenchen 4 5Compression of Isar proofs by merging steps. 6Only proof steps using the same proof method are merged. 7*) 8 9signature SLEDGEHAMMER_ISAR_COMPRESS = 10sig 11 type isar_proof = Sledgehammer_Isar_Proof.isar_proof 12 type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data 13 14 val compress_isar_proof : Proof.context -> real -> Time.time -> 15 isar_preplay_data Unsynchronized.ref -> isar_proof -> isar_proof 16end; 17 18structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS = 19struct 20 21open Sledgehammer_Util 22open Sledgehammer_Proof_Methods 23open Sledgehammer_Isar_Proof 24open Sledgehammer_Isar_Preplay 25 26fun collect_successors steps lbls = 27 let 28 fun collect_steps _ (accum as ([], _)) = accum 29 | collect_steps [] accum = accum 30 | collect_steps (step :: steps) accum = collect_steps steps (collect_step step accum) 31 and collect_step (step as Prove (_, _, l, _, subproofs, _, _, _)) x = 32 (case collect_subproofs subproofs x of 33 (accum as ([], _)) => accum 34 | accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum) 35 | collect_step _ accum = accum 36 and collect_subproofs [] accum = accum 37 | collect_subproofs (proof :: subproofs) accum = 38 (case collect_steps (steps_of_isar_proof proof) accum of 39 accum as ([], _) => accum 40 | accum => collect_subproofs subproofs accum) 41 in 42 rev (snd (collect_steps steps (lbls, []))) 43 end 44 45fun update_steps updates steps = 46 let 47 fun update_steps [] updates = ([], updates) 48 | update_steps steps [] = (steps, []) 49 | update_steps (step :: steps) updates = update_step step (update_steps steps updates) 50 and update_step step (steps, []) = (step :: steps, []) 51 | update_step (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) 52 (steps, 53 updates as Prove (qs', xs', l', t', subproofs', facts', meths', comment') :: updates') = 54 (if l = l' then 55 update_subproofs subproofs' updates' 56 |>> (fn subproofs'' => Prove (qs', xs', l', t', subproofs'', facts', meths', comment')) 57 else 58 update_subproofs subproofs updates 59 |>> (fn subproofs' => Prove (qs, xs, l, t, subproofs', facts, meths, comment))) 60 |>> (fn step => step :: steps) 61 | update_step step (steps, updates) = (step :: steps, updates) 62 and update_subproofs [] updates = ([], updates) 63 | update_subproofs steps [] = (steps, []) 64 | update_subproofs (proof :: subproofs) updates = 65 update_proof proof (update_subproofs subproofs updates) 66 and update_proof proof (proofs, []) = (proof :: proofs, []) 67 | update_proof (Proof (xs, assms, steps)) (proofs, updates) = 68 let val (steps', updates') = update_steps steps updates in 69 (Proof (xs, assms, steps') :: proofs, updates') 70 end 71 in 72 fst (update_steps steps (rev updates)) 73 end 74 75fun merge_methods preplay_data (l1, meths1) (l2, meths2) = 76 let 77 fun is_hopeful l meth = 78 let val outcome = preplay_outcome_of_isar_step_for_method preplay_data l meth in 79 not (Lazy.is_finished outcome) orelse 80 (case Lazy.force outcome of Played _ => true | Play_Timed_Out _ => true | _ => false) 81 end 82 83 val (hopeful, hopeless) = 84 meths2 @ subtract (op =) meths2 meths1 85 |> List.partition (is_hopeful l1 andf is_hopeful l2) 86 in 87 (hopeful @ hopeless, hopeless) 88 end 89 90fun merge_steps preplay_data (Prove ([], xs1, l1, _, subproofs1, (lfs1, gfs1), meths1, comment1)) 91 (Prove (qs2, xs2, l2, t, subproofs2, (lfs2, gfs2), meths2, comment2)) = 92 let 93 val (meths, hopeless) = merge_methods preplay_data (l1, meths1) (l2, meths2) 94 val lfs = union (op =) lfs1 (remove (op =) l1 lfs2) 95 val gfs = union (op =) gfs1 gfs2 96 in 97 (Prove (qs2, inter (op =) (Term.add_frees t []) (xs1 @ xs2), l2, t, 98 subproofs1 @ subproofs2, sort_facts (lfs, gfs), meths, comment1 ^ comment2), 99 hopeless) 100 end 101 102val merge_slack_time = seconds 0.01 103val merge_slack_factor = 1.5 104 105fun adjust_merge_timeout max time = 106 let val timeout = time_mult merge_slack_factor (merge_slack_time + time) in 107 if max < timeout then max else timeout 108 end 109 110val compress_degree = 2 111 112(* Precondition: The proof must be labeled canonically. *) 113fun compress_isar_proof ctxt compress preplay_timeout preplay_data proof = 114 if compress <= 1.0 then 115 proof 116 else 117 let 118 val (compress_further, decrement_step_count) = 119 let 120 val number_of_steps = add_isar_steps (steps_of_isar_proof proof) 0 121 val target_number_of_steps = Real.ceil (Real.fromInt number_of_steps / compress) 122 val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps) 123 in 124 (fn () => !delta > 0, fn () => delta := !delta - 1) 125 end 126 127 val (get_successors, replace_successor) = 128 let 129 fun add_refs (Prove (_, _, l, _, _, (lfs, _), _, _)) = 130 fold (fn key => Canonical_Label_Tab.cons_list (key, l)) lfs 131 | add_refs _ = I 132 133 val tab = 134 Canonical_Label_Tab.empty 135 |> fold_isar_steps add_refs (steps_of_isar_proof proof) 136 (* "rev" should have the same effect as "sort canonical_label_ord" *) 137 |> Canonical_Label_Tab.map (K rev) 138 |> Unsynchronized.ref 139 140 fun get_successors l = Canonical_Label_Tab.lookup_list (!tab) l 141 fun set_successors l refs = tab := Canonical_Label_Tab.update (l, refs) (!tab) 142 fun replace_successor old new dest = 143 get_successors dest 144 |> Ord_List.remove canonical_label_ord old 145 |> Ord_List.union canonical_label_ord new 146 |> set_successors dest 147 in 148 (get_successors, replace_successor) 149 end 150 151 fun reference_time l = 152 (case forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l of 153 Played time => time 154 | _ => preplay_timeout) 155 156 (* elimination of trivial, one-step subproofs *) 157 fun elim_one_subproof time (step as Prove (qs, xs, l, t, _, (lfs, gfs), meths, comment)) subs 158 nontriv_subs = 159 if null subs orelse not (compress_further ()) then 160 Prove (qs, xs, l, t, List.revAppend (nontriv_subs, subs), (lfs, gfs), meths, comment) 161 else 162 (case subs of 163 (sub as Proof (_, assms, [Prove (_, _, l', _, [], (lfs', gfs'), meths', _)])) :: subs => 164 let 165 (* merge steps *) 166 val subs'' = subs @ nontriv_subs 167 val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs') 168 val gfs'' = union (op =) gfs' gfs 169 val (meths'' as _ :: _, hopeless) = 170 merge_methods (!preplay_data) (l', meths') (l, meths) 171 val step'' = Prove (qs, xs, l, t, subs'', (lfs'', gfs''), meths'', comment) 172 173 (* check if the modified step can be preplayed fast enough *) 174 val timeout = adjust_merge_timeout preplay_timeout (time + reference_time l') 175 in 176 (case preplay_isar_step ctxt [] timeout hopeless step'' of 177 meths_outcomes as (_, Played time'') :: _ => 178 (* "l'" successfully eliminated *) 179 (decrement_step_count (); 180 set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step'' meths_outcomes; 181 map (replace_successor l' [l]) lfs'; 182 elim_one_subproof time'' step'' subs nontriv_subs) 183 | _ => elim_one_subproof time step subs (sub :: nontriv_subs)) 184 end 185 | sub :: subs => elim_one_subproof time step subs (sub :: nontriv_subs)) 186 187 fun elim_subproofs (step as Prove (_, _, l, _, subproofs, _, _, _)) = 188 if exists (null o tl o steps_of_isar_proof) subproofs then 189 elim_one_subproof (reference_time l) step subproofs [] 190 else 191 step 192 | elim_subproofs step = step 193 194 fun compress_top_level steps = 195 let 196 val cand_key = apfst (length o get_successors) 197 val cand_ord = 198 prod_ord int_ord (prod_ord (int_ord o swap) (int_ord o swap)) o apply2 cand_key 199 200 fun pop_next_candidate [] = (NONE, []) 201 | pop_next_candidate (cands as (cand :: cands')) = 202 fold (fn x => fn y => if is_less (cand_ord (x, y)) then x else y) cands' cand 203 |> (fn best => (SOME best, remove (op =) best cands)) 204 205 fun try_eliminate i l labels steps = 206 let 207 val (steps_before, (cand as Prove (_, _, _, _, _, (lfs, _), _, _)) :: steps_after) = 208 chop i steps 209 val succs = collect_successors steps_after labels 210 val (succs', hopelesses) = split_list (map (merge_steps (!preplay_data) cand) succs) 211 in 212 (case try (map ((fn Played time => time) o 213 forced_intermediate_preplay_outcome_of_isar_step (!preplay_data))) labels of 214 NONE => steps 215 | SOME times0 => 216 let 217 val n = length labels 218 val total_time = Library.foldl (op +) (reference_time l, times0) 219 val timeout = adjust_merge_timeout preplay_timeout 220 (Time.fromReal (Time.toReal total_time / Real.fromInt n)) 221 val meths_outcomess = 222 @{map 2} (preplay_isar_step ctxt [] timeout) hopelesses succs' 223 in 224 (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of 225 NONE => steps 226 | SOME times => 227 (* "l" successfully eliminated *) 228 (decrement_step_count (); 229 @{map 3} (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) 230 times succs' meths_outcomess; 231 map (replace_successor l labels) lfs; 232 steps_before @ update_steps succs' steps_after)) 233 end) 234 end 235 236 fun compression_loop candidates steps = 237 if not (compress_further ()) then 238 steps 239 else 240 (case pop_next_candidate candidates of 241 (NONE, _) => steps (* no more candidates for elimination *) 242 | (SOME (l, (num_xs, _)), candidates') => 243 (case find_index (curry (op =) (SOME l) o label_of_isar_step) steps of 244 ~1 => steps 245 | i => 246 let 247 val successors = get_successors l 248 val num_successors = length successors 249 in 250 (* Careful with "obtain", so we don't "obtain" twice the same variable after a 251 merge. *) 252 if num_successors > (if num_xs > 0 then 1 else compress_degree) then 253 steps 254 else 255 steps 256 |> not (null successors) ? try_eliminate i l successors 257 |> compression_loop candidates' 258 end)) 259 260 fun add_cand (Prove (_, xs, l, t, _, _, _, _)) = cons (l, (length xs, size_of_term t)) 261 | add_cand _ = I 262 263 (* the very last step is not a candidate *) 264 val candidates = fold add_cand (fst (split_last steps)) [] 265 in 266 compression_loop candidates steps 267 end 268 269 (* Proofs are compressed bottom-up, beginning with the innermost subproofs. On the innermost 270 proof level, the proof steps have no subproofs. In the best case, these steps can be merged 271 into just one step, resulting in a trivial subproof. Going one level up, trivial subproofs 272 can be eliminated. In the best case, this once again leads to a proof whose proof steps do 273 not have subproofs. Applying this approach recursively will result in a flat proof in the 274 best cast. *) 275 fun compress_proof (proof as (Proof (xs, assms, steps))) = 276 if compress_further () then Proof (xs, assms, compress_steps steps) else proof 277 and compress_steps steps = 278 (* bottom-up: compress innermost proofs first *) 279 steps 280 |> map (fn step => step |> compress_further () ? compress_sub_levels) 281 |> compress_further () ? compress_top_level 282 and compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) = 283 (* compress subproofs *) 284 Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths, comment) 285 (* eliminate trivial subproofs *) 286 |> compress_further () ? elim_subproofs 287 | compress_sub_levels step = step 288 in 289 compress_proof proof 290 end 291 292end; 293