author | blanchet |
Mon, 03 Feb 2014 10:14:18 +0100 | |
changeset 55264 | 43473497fb65 |
parent 55263 | 4d63fffcde8d |
child 55265 | bd9f033b9896 |
permissions | -rw-r--r-- |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML |
54712 | 2 |
Author: Steffen Juilf Smolka, TU Muenchen |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
4 |
|
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
5 |
Minimize dependencies (used facts) of Isar proof steps. |
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
6 |
*) |
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
7 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
8 |
signature SLEDGEHAMMER_ISAR_MINIMIZE = |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
9 |
sig |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
10 |
type isar_step = Sledgehammer_Isar_Proof.isar_step |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
11 |
type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
55213 | 12 |
type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data |
54712 | 13 |
|
55260 | 14 |
val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref -> |
15 |
isar_step -> isar_step |
|
55213 | 16 |
val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> |
17 |
isar_proof |
|
54504 | 18 |
end; |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
19 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
20 |
structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE = |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
21 |
struct |
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
22 |
|
54828 | 23 |
open Sledgehammer_Reconstructor |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
24 |
open Sledgehammer_Isar_Proof |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset
|
25 |
open Sledgehammer_Isar_Preplay |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
26 |
|
54712 | 27 |
val slack = seconds 0.1 |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
28 |
|
55260 | 29 |
fun minimize_isar_step_dependencies _ _ (step as Let _) = step |
30 |
| minimize_isar_step_dependencies ctxt preplay_data |
|
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55243
diff
changeset
|
31 |
(step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) = |
55260 | 32 |
(case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of |
54828 | 33 |
Played time => |
54712 | 34 |
let |
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55243
diff
changeset
|
35 |
fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths)) |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
36 |
|
54712 | 37 |
fun minimize_facts _ time min_facts [] = (time, min_facts) |
38 |
| minimize_facts mk_step time min_facts (f :: facts) = |
|
55258 | 39 |
(case preplay_isar_step ctxt (Time.+ (time, slack)) meth |
40 |
(mk_step (min_facts @ facts)) of |
|
54828 | 41 |
Played time => minimize_facts mk_step time min_facts facts |
54827 | 42 |
| _ => minimize_facts mk_step time (f :: min_facts) facts) |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
43 |
|
55263 | 44 |
val (time, min_lfs) = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs) time [] lfs |
54712 | 45 |
val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs |
55264 | 46 |
|
47 |
val step' = mk_step_lfs_gfs min_lfs min_gfs |
|
54712 | 48 |
in |
55264 | 49 |
set_preplay_outcomes_of_isar_step ctxt time preplay_data step' |
50 |
[(meth, Lazy.value (Played time))]; |
|
51 |
step' |
|
54826 | 52 |
end |
53 |
| _ => step (* don't touch steps that time out or fail *)) |
|
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
54 |
|
55213 | 55 |
fun postprocess_isar_proof_remove_unreferenced_steps postproc_step = |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
56 |
let |
55259 | 57 |
fun process_proof (Proof (fix, assms, steps)) = |
58 |
let val (refed, steps) = process_steps steps in |
|
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
59 |
(refed, Proof (fix, assms, steps)) |
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
60 |
end |
55259 | 61 |
and process_steps [] = ([], []) |
62 |
| process_steps steps = |
|
55212 | 63 |
(* the last step is always implicitly referenced *) |
55259 | 64 |
let val (steps, (refed, concl)) = split_last steps ||> process_referenced_step in |
65 |
fold_rev process_step steps (refed, [concl]) |
|
54754 | 66 |
end |
55259 | 67 |
and process_step step (refed, accu) = |
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset
|
68 |
(case label_of_isar_step step of |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
69 |
NONE => (refed, step :: accu) |
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
70 |
| SOME l => |
54813 | 71 |
if Ord_List.member label_ord refed l then |
55259 | 72 |
process_referenced_step step |
54813 | 73 |
|>> Ord_List.union label_ord refed |
74 |
||> (fn x => x :: accu) |
|
75 |
else |
|
76 |
(refed, accu)) |
|
55259 | 77 |
and process_referenced_step step = step |> postproc_step |> process_referenced_step_subproofs |
78 |
and process_referenced_step_subproofs (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) = |
|
79 |
let |
|
80 |
val (refed, subproofs) = |
|
81 |
map process_proof subproofs |
|
82 |
|> split_list |
|
83 |
|>> Ord_List.unions label_ord |
|
84 |
|>> fold (Ord_List.insert label_ord) lfs |
|
85 |
val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m)) |
|
86 |
in |
|
87 |
(refed, step) |
|
88 |
end |
|
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
89 |
in |
55259 | 90 |
snd o process_proof |
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
91 |
end |
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset
|
92 |
|
54504 | 93 |
end; |