75 val step_vect = steps |> map SOME |> Vector.fromList |
75 val step_vect = steps |> map SOME |> Vector.fromList |
76 val n_metis = add_metis_steps_top_level steps 0 |
76 val n_metis = add_metis_steps_top_level steps 0 |
77 val target_n_metis = Real.fromInt n_metis / isar_compress |> Real.round |
77 val target_n_metis = Real.fromInt n_metis / isar_compress |> Real.round |
78 |
78 |
79 (* table for mapping from (top-level-)label to step_vect position *) |
79 (* table for mapping from (top-level-)label to step_vect position *) |
80 fun update_table (i, Prove (_, _, l, _, _)) = Label_Table.update_new (l, i) |
80 fun update_table (i, Prove (_, _, l, _, _, _)) = |
|
81 Label_Table.update_new (l, i) |
81 | update_table _ = I |
82 | update_table _ = I |
82 val label_index_table = fold_index update_table steps Label_Table.empty |
83 val label_index_table = fold_index update_table steps Label_Table.empty |
83 val lookup_indices = map_filter (Label_Table.lookup label_index_table) |
84 val lookup_indices = map_filter (Label_Table.lookup label_index_table) |
84 |
85 |
85 (* proof step references *) |
86 (* proof step references *) |
86 fun refs step = |
87 fun refs step = |
87 (case byline_of_step step of |
88 fold_isar_step |
88 NONE => [] |
89 (byline_of_step |
89 | SOME (By_Metis (subproofs, (lfs, _))) => |
90 #> (fn SOME (By_Metis (lfs, _)) => append (lookup_indices lfs) |
90 maps (steps_of_proof #> maps refs) subproofs @ lookup_indices lfs) |
91 | _ => I)) |
|
92 step [] |
91 val refed_by_vect = |
93 val refed_by_vect = |
92 Vector.tabulate (Vector.length step_vect, K []) |
94 Vector.tabulate (Vector.length step_vect, K []) |
93 |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) steps |
95 |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) steps |
94 |> Vector.map rev (* after rev, indices are sorted in ascending order *) |
96 |> Vector.map rev (* after rev, indices are sorted in ascending order *) |
95 |
97 |
96 (* candidates for elimination, use table as priority queue (greedy |
98 (* candidates for elimination, use table as priority queue (greedy |
97 algorithm) *) |
99 algorithm) *) |
98 fun add_if_cand step_vect (i, [j]) = |
100 fun add_if_cand step_vect (i, [j]) = |
99 ((case (the (get i step_vect), the (get j step_vect)) of |
101 ((case (the (get i step_vect), the (get j step_vect)) of |
100 (Prove (_, Fix [], _, t, By_Metis _), Prove (_, _, _, _, By_Metis _)) => |
102 (Prove (_, Fix [], _, t, _, By_Metis _), |
101 cons (Term.size_of_term t, i) |
103 Prove (_, _, _, _, _, By_Metis _)) => cons (Term.size_of_term t, i) |
102 | _ => I) |
104 | _ => I) |
103 handle Option.Option => raise Fail "sledgehammer_compress: add_if_cand") |
105 handle Option.Option => raise Fail "sledgehammer_compress: add_if_cand") |
104 | add_if_cand _ _ = I |
106 | add_if_cand _ _ = I |
105 val cand_tab = |
107 val cand_tab = |
106 v_fold_index (add_if_cand step_vect) refed_by_vect [] |
108 v_fold_index (add_if_cand step_vect) refed_by_vect [] |
124 (apfst get_time #> uncurry add_preplay_time) |
126 (apfst get_time #> uncurry add_preplay_time) |
125 zero_preplay_time lazy_time_vector |
127 zero_preplay_time lazy_time_vector |
126 |
128 |
127 (* Merging *) |
129 (* Merging *) |
128 fun merge |
130 fun merge |
129 (Prove (_, Fix [], lbl1, _, By_Metis (subproofs1, (lfs1, gfs1)))) |
131 (Prove (_, Fix [], lbl1, _, subproofs1, By_Metis (lfs1, gfs1))) |
130 (Prove (qs2, fix, lbl2, t, By_Metis (subproofs2, (lfs2, gfs2)))) = |
132 (Prove (qs2, fix, lbl2, t, subproofs2, By_Metis (lfs2, gfs2))) = |
131 let |
133 let |
132 val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1 |
134 val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1 |
133 val gfs = union (op =) gfs1 gfs2 |
135 val gfs = union (op =) gfs1 gfs2 |
134 val subproofs = subproofs1 @ subproofs2 |
136 val subproofs = subproofs1 @ subproofs2 |
135 in Prove (qs2, fix, lbl2, t, By_Metis (subproofs, (lfs, gfs))) end |
137 in Prove (qs2, fix, lbl2, t, subproofs, By_Metis (lfs, gfs)) end |
136 | merge _ _ = raise Fail "sledgehammer_compress: unmergeable Isar steps" |
138 | merge _ _ = raise Fail "sledgehammer_compress: unmergeable Isar steps" |
137 |
139 |
138 fun try_merge metis_time (s1, i) (s2, j) = |
140 fun try_merge metis_time (s1, i) (s2, j) = |
139 if not preplay then (merge s1 s2 |> SOME, metis_time) |
141 if not preplay then (merge s1 s2 |> SOME, metis_time) |
140 else |
142 else |
207 val thy = Proof_Context.theory_of ctxt |
209 val thy = Proof_Context.theory_of ctxt |
208 (* TODO: add Skolem variables to context? *) |
210 (* TODO: add Skolem variables to context? *) |
209 fun enrich_with_fact l t = |
211 fun enrich_with_fact l t = |
210 Proof_Context.put_thms false |
212 Proof_Context.put_thms false |
211 (string_of_label l, SOME [Skip_Proof.make_thm thy t]) |
213 (string_of_label l, SOME [Skip_Proof.make_thm thy t]) |
212 fun enrich_with_step (Prove (_, _, l, t, _)) = enrich_with_fact l t |
214 fun enrich_with_step (Prove (_, _, l, t, _, _)) = enrich_with_fact l t |
213 | enrich_with_step _ = I |
215 | enrich_with_step _ = I |
214 val enrich_with_steps = fold enrich_with_step |
216 val enrich_with_steps = fold enrich_with_step |
215 val enrich_with_assms = fold (uncurry enrich_with_fact) |
217 val enrich_with_assms = fold (uncurry enrich_with_fact) |
216 val rich_ctxt = |
218 val rich_ctxt = |
217 ctxt |> enrich_with_assms assms |> enrich_with_steps steps |
219 ctxt |> enrich_with_assms assms |> enrich_with_steps steps |
232 fun compress_each_and_collect_time compress subproofs = |
234 fun compress_each_and_collect_time compress subproofs = |
233 let fun f_m proof time = compress proof ||> add_preplay_time time |
235 let fun f_m proof time = compress proof ||> add_preplay_time time |
234 in fold_map f_m subproofs zero_preplay_time end |
236 in fold_map f_m subproofs zero_preplay_time end |
235 val compress_subproofs = |
237 val compress_subproofs = |
236 compress_each_and_collect_time (do_proof false ctxt) |
238 compress_each_and_collect_time (do_proof false ctxt) |
237 fun compress (Prove (qs, fix, l, t, By_Metis(subproofs, facts))) = |
239 fun compress (Prove (qs, fix, l, t, subproofs, By_Metis facts)) = |
238 let val (subproofs, time) = compress_subproofs subproofs |
240 let val (subproofs, time) = compress_subproofs subproofs |
239 in (Prove (qs, fix, l, t, By_Metis(subproofs, facts)), time) end |
241 in (Prove (qs, fix, l, t, subproofs, By_Metis facts), time) end |
240 | compress atomic_step = (atomic_step, zero_preplay_time) |
242 | compress atomic_step = (atomic_step, zero_preplay_time) |
241 in |
243 in |
242 compress_each_and_collect_time compress subproofs |
244 compress_each_and_collect_time compress subproofs |
243 end |
245 end |
244 in |
246 in |