author  blanchet 
Tue, 04 Feb 2014 23:11:18 +0100  
changeset 55324  e04b75bd18e0 
parent 55314  e0233567a8ef 
child 55452  29ec8680e61f 
permissions  rwrr 
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 

55266  14 
val keep_fastest_method_of_isar_step : isar_preplay_data > isar_step > isar_step 
55260  15 
val minimize_isar_step_dependencies : Proof.context > isar_preplay_data Unsynchronized.ref > 
16 
isar_step > isar_step 

55213  17 
val postprocess_isar_proof_remove_unreferenced_steps : (isar_step > isar_step) > isar_proof > 
18 
isar_proof 

54504  19 
end; 
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset

20 

55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset

21 
structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE = 
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset

22 
struct 
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset

23 

55287  24 
open Sledgehammer_Proof_Methods 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset

25 
open Sledgehammer_Isar_Proof 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54828
diff
changeset

26 
open Sledgehammer_Isar_Preplay 
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset

27 

55299  28 
fun keep_fastest_method_of_isar_step preplay_data 
29 
(Prove (qs, xs, l, t, subproofs, facts, meths, comment)) = 

55295
b18f65f77fcd
keep all proof methods in data structure until the end, to enhance debugging output
blanchet
parents:
55287
diff
changeset

30 
Prove (qs, xs, l, t, subproofs, facts, 
55299  31 
meths > List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) > op @, 
32 
comment) 

55266  33 
 keep_fastest_method_of_isar_step _ step = step 
34 

55324  35 
val slack = seconds 0.025 
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset

36 

55266  37 
fun minimize_isar_step_dependencies ctxt preplay_data 
55299  38 
(step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) = 
55266  39 
(case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of 
54828  40 
Played time => 
54712  41 
let 
55299  42 
fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment) 
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset

43 

55314  44 
fun minimize_facts _ min_facts [] time = (min_facts, time) 
45 
 minimize_facts mk_step min_facts (fact :: facts) time = 

55278
73372494fd80
more flexible compression, choosing whichever proof method works
blanchet
parents:
55268
diff
changeset

46 
(case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth 
55258  47 
(mk_step (min_facts @ facts)) of 
55314  48 
Played time' => minimize_facts mk_step min_facts facts time' 
49 
 _ => minimize_facts mk_step (fact :: min_facts) facts time) 

52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset

50 

55314  51 
val (min_lfs, time') = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs0) [] lfs0 time 
52 
val (min_gfs, time'') = minimize_facts (mk_step_lfs_gfs min_lfs) [] gfs0 time' 

55264  53 

54 
val step' = mk_step_lfs_gfs min_lfs min_gfs 

54712  55 
in 
55314  56 
set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step' [(meth, Played time'')]; 
55264  57 
step' 
54826  58 
end 
59 
 _ => step (* don't touch steps that time out or fail *)) 

55266  60 
 minimize_isar_step_dependencies _ _ step = step 
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset

61 

55213  62 
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

63 
let 
55259  64 
fun process_proof (Proof (fix, assms, steps)) = 
55265  65 
process_steps steps > (fn steps => Proof (fix, assms, steps)) 
55259  66 
and process_steps [] = ([], []) 
67 
 process_steps steps = 

55212  68 
(* the last step is always implicitly referenced *) 
55265  69 
let val (steps, (used, concl)) = split_last steps > process_used_step in 
70 
fold_rev process_step steps (used, [concl]) 

54754  71 
end 
55265  72 
and process_step step (used, accu) = 
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55221
diff
changeset

73 
(case label_of_isar_step step of 
55265  74 
NONE => (used, step :: accu) 
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset

75 
 SOME l => 
55265  76 
if Ord_List.member label_ord used l then 
77 
process_used_step step >> Ord_List.union label_ord used > (fn step => step :: accu) 

54813  78 
else 
55265  79 
(used, accu)) 
80 
and process_used_step step = step > postproc_step > process_used_step_subproofs 

55299  81 
and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) = 
55259  82 
let 
55265  83 
val (used, subproofs) = 
55259  84 
map process_proof subproofs 
85 
> split_list 

86 
>> Ord_List.unions label_ord 

87 
>> fold (Ord_List.insert label_ord) lfs 

88 
in 

55299  89 
(used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) 
55259  90 
end 
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset

91 
in 
55259  92 
snd o process_proof 
52611
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset

93 
end 
831f7479c74f
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas
parents:
diff
changeset

94 

54504  95 
end; 