49 end |
49 end |
50 | _ => step (* don't touch steps that time out or fail *)) |
50 | _ => step (* don't touch steps that time out or fail *)) |
51 |
51 |
52 fun postprocess_isar_proof_remove_unreferenced_steps postproc_step = |
52 fun postprocess_isar_proof_remove_unreferenced_steps postproc_step = |
53 let |
53 let |
54 val add_lfs = fold (Ord_List.insert label_ord) |
54 fun process_proof (Proof (fix, assms, steps)) = |
55 |
55 let val (refed, steps) = process_steps steps in |
56 fun do_proof (Proof (fix, assms, steps)) = |
|
57 let val (refed, steps) = do_steps steps in |
|
58 (refed, Proof (fix, assms, steps)) |
56 (refed, Proof (fix, assms, steps)) |
59 end |
57 end |
60 and do_steps [] = ([], []) |
58 and process_steps [] = ([], []) |
61 | do_steps steps = |
59 | process_steps steps = |
62 (* the last step is always implicitly referenced *) |
60 (* the last step is always implicitly referenced *) |
63 let val (steps, (refed, concl)) = split_last steps ||> do_refed_step in |
61 let val (steps, (refed, concl)) = split_last steps ||> process_referenced_step in |
64 fold_rev do_step steps (refed, [concl]) |
62 fold_rev process_step steps (refed, [concl]) |
65 end |
63 end |
66 and do_step step (refed, accu) = |
64 and process_step step (refed, accu) = |
67 (case label_of_isar_step step of |
65 (case label_of_isar_step step of |
68 NONE => (refed, step :: accu) |
66 NONE => (refed, step :: accu) |
69 | SOME l => |
67 | SOME l => |
70 if Ord_List.member label_ord refed l then |
68 if Ord_List.member label_ord refed l then |
71 do_refed_step step |
69 process_referenced_step step |
72 |>> Ord_List.union label_ord refed |
70 |>> Ord_List.union label_ord refed |
73 ||> (fn x => x :: accu) |
71 ||> (fn x => x :: accu) |
74 else |
72 else |
75 (refed, accu)) |
73 (refed, accu)) |
76 and do_refed_step step = step |> postproc_step |> do_refed_step' |
74 and process_referenced_step step = step |> postproc_step |> process_referenced_step_subproofs |
77 and do_refed_step' (Let _) = raise Fail "Sledgehammer_Isar_Minimize" |
75 and process_referenced_step_subproofs (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) = |
78 | do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) = |
76 let |
79 let |
77 val (refed, subproofs) = |
80 val (refed, subproofs) = |
78 map process_proof subproofs |
81 map do_proof subproofs |
79 |> split_list |
82 |> split_list |
80 |>> Ord_List.unions label_ord |
83 |>> Ord_List.unions label_ord |
81 |>> fold (Ord_List.insert label_ord) lfs |
84 |>> add_lfs lfs |
82 val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m)) |
85 val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m)) |
83 in |
86 in |
84 (refed, step) |
87 (refed, step) |
85 end |
88 end |
|
89 in |
86 in |
90 snd o do_proof |
87 snd o process_proof |
91 end |
88 end |
92 |
89 |
93 end; |
90 end; |