File ‹Tools/Sledgehammer/sledgehammer_isar_compress.ML›
signature SLEDGEHAMMER_ISAR_COMPRESS =
sig
type isar_proof = Sledgehammer_Isar_Proof.isar_proof
type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
val compress_isar_proof : Proof.context -> real -> Time.time ->
isar_preplay_data Unsynchronized.ref -> isar_proof -> isar_proof
end;
structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS =
struct
open Sledgehammer_Util
open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Proof
open Sledgehammer_Isar_Preplay
fun collect_successors steps lbls =
let
fun collect_steps _ (accum as ([], _)) = accum
| collect_steps [] accum = accum
| collect_steps (step :: steps) accum = collect_steps steps (collect_step step accum)
and collect_step (step as Prove {label, subproofs, ...}) x =
(case collect_subproofs subproofs x of
accum as ([], _) => accum
| accum as (l' :: lbls', accu) => if label = l' then (lbls', step :: accu) else accum)
| collect_step _ accum = accum
and collect_subproofs [] accum = accum
| collect_subproofs (proof :: subproofs) accum =
(case collect_steps (steps_of_isar_proof proof) accum of
accum as ([], _) => accum
| accum => collect_subproofs subproofs accum)
in
rev (snd (collect_steps steps (lbls, [])))
end
fun update_steps updates steps =
let
fun update_steps [] updates = ([], updates)
| update_steps steps [] = (steps, [])
| update_steps (step :: steps) updates = update_step step (update_steps steps updates)
and update_step step (steps, []) = (step :: steps, [])
| update_step (Prove {qualifiers = qs, obtains = xs, label = l, goal = t, subproofs, facts,
proof_methods = meths, comment}) (steps, updates as Prove {qualifiers = qs',
obtains = xs', label = l', goal = t', subproofs = subproofs', facts = facts',
proof_methods = meths', comment = comment'} :: updates') =
(if l = l' then
update_subproofs subproofs' updates'
|>> (fn subproofs'' => Prove {
qualifiers = qs',
obtains = xs',
label = l',
goal = t',
subproofs = subproofs'',
facts = facts',
proof_methods = meths',
comment = comment'})
else
update_subproofs subproofs updates
|>> (fn subproofs' => Prove {
qualifiers = qs,
obtains = xs,
label = l,
goal = t,
subproofs = subproofs',
facts = facts,
proof_methods = meths,
comment = comment}))
|>> (fn step => step :: steps)
| update_step step (steps, updates) = (step :: steps, updates)
and update_subproofs [] updates = ([], updates)
| update_subproofs steps [] = (steps, [])
| update_subproofs (proof :: subproofs) updates =
update_proof proof (update_subproofs subproofs updates)
and update_proof proof (proofs, []) = (proof :: proofs, [])
| update_proof (proof as Proof {steps, ...}) (proofs, updates) =
let val (steps', updates') = update_steps steps updates in
(isar_proof_with_steps proof steps' :: proofs, updates')
end
in
fst (update_steps steps (rev updates))
end
fun merge_methods preplay_data (l1, meths1) (l2, meths2) =
let
fun is_hopeful l meth =
let val outcome = preplay_outcome_of_isar_step_for_method preplay_data l meth in
not (Lazy.is_finished outcome) orelse
(case Lazy.force outcome of Played _ => true | Play_Timed_Out _ => true | _ => false)
end
val (hopeful, hopeless) =
meths2 @ subtract (op =) meths2 meths1
|> List.partition (is_hopeful l1 andf is_hopeful l2)
in
(hopeful @ hopeless, hopeless)
end
fun merge_steps preplay_data
(Prove (p1 as {qualifiers = [], label = l1, goal = _, facts = (lfs1, gfs1), ...}))
(Prove (p2 as {qualifiers = qs2, label = l2, goal = t, facts = (lfs2, gfs2), ...})) =
let
val (meths, hopeless) =
merge_methods preplay_data (l1, #proof_methods p1) (l2, #proof_methods p2)
val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
val gfs = union (op =) gfs1 gfs2
val prove = Prove {
qualifiers = qs2,
obtains = inter (op =) (Term.add_frees t []) (#obtains p1 @ #obtains p2),
label = l2,
goal = t,
subproofs = #subproofs p1 @ #subproofs p2,
facts = sort_facts (lfs, gfs),
proof_methods = meths,
comment = #comment p1 ^ #comment p2}
in
(prove, hopeless)
end
val merge_slack_time = seconds 0.01
val merge_slack_factor = 1.5
fun adjust_merge_timeout max time =
let val timeout = Time.scale merge_slack_factor (merge_slack_time + time) in
if max < timeout then max else timeout
end
val compress_degree = 2
fun compress_isar_proof ctxt compress preplay_timeout preplay_data proof =
if compress <= 1.0 then
proof
else
let
val (compress_further, decrement_step_count) =
let
val number_of_steps = add_isar_steps (steps_of_isar_proof proof) 0
val target_number_of_steps = Real.ceil (Real.fromInt number_of_steps / compress)
val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps)
in
(fn () => !delta > 0, fn () => delta := !delta - 1)
end
val (get_successors, replace_successor) =
let
fun add_refs (Prove {label, facts = (lfs, _), ...}) =
fold (fn key => Canonical_Label_Tab.cons_list (key, label)) lfs
| add_refs _ = I
val tab =
Canonical_Label_Tab.empty
|> fold_isar_steps add_refs (steps_of_isar_proof proof)
|> Canonical_Label_Tab.map (K rev)
|> Unsynchronized.ref
fun get_successors l = Canonical_Label_Tab.lookup_list (!tab) l
fun set_successors l refs = tab := Canonical_Label_Tab.update (l, refs) (!tab)
fun replace_successor old new dest =
get_successors dest
|> Ord_List.remove canonical_label_ord old
|> Ord_List.union canonical_label_ord new
|> set_successors dest
in
(get_successors, replace_successor)
end
fun reference_time l =
(case forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l of
Played time => time
| _ => preplay_timeout)
fun elim_one_subproof time (step as Prove {qualifiers, obtains, label, goal,
facts = (lfs, gfs), proof_methods, comment, ...}) subs
nontriv_subs =
if null subs orelse not (compress_further ()) then
Prove {
qualifiers = qualifiers,
obtains = obtains,
label = label,
goal = goal,
subproofs = List.revAppend (nontriv_subs, subs),
facts = (lfs, gfs),
proof_methods = proof_methods,
comment = comment}
else
(case subs of
(sub as Proof {assumptions,
steps = [Prove {label = label', subproofs = [], facts = (lfs', gfs'),
proof_methods = proof_methods', ...}], ...}) :: subs =>
let
val subs'' = subs @ nontriv_subs
val lfs'' = union (op =) lfs (subtract (op =) (map fst assumptions) lfs')
val gfs'' = union (op =) gfs' gfs
val (proof_methods'' as _ :: _, hopeless) =
merge_methods (!preplay_data) (label', proof_methods') (label, proof_methods)
val step'' = Prove {
qualifiers = qualifiers,
obtains = obtains,
label = label,
goal = goal,
subproofs = subs'',
facts = (lfs'', gfs''),
proof_methods = proof_methods'',
comment = comment}
val timeout = adjust_merge_timeout preplay_timeout (time + reference_time label')
in
(case preplay_isar_step ctxt [] timeout hopeless step'' of
meths_outcomes as (_, Played time'') :: _ =>
(decrement_step_count ();
set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step'' meths_outcomes;
map (replace_successor label' [label]) lfs';
elim_one_subproof time'' step'' subs nontriv_subs)
| _ => elim_one_subproof time step subs (sub :: nontriv_subs))
end
| sub :: subs => elim_one_subproof time step subs (sub :: nontriv_subs))
fun elim_subproofs (step as Prove {label, subproofs, ...}) =
if exists (null o tl o steps_of_isar_proof) subproofs then
elim_one_subproof (reference_time label) step subproofs []
else
step
| elim_subproofs step = step
fun compress_top_level steps =
let
val cand_key = apfst (length o get_successors)
val cand_ord =
prod_ord int_ord (prod_ord (int_ord o swap) (int_ord o swap)) o apply2 cand_key
fun pop_next_candidate [] = (NONE, [])
| pop_next_candidate (cands as (cand :: cands')) =
fold (fn x => fn y => if is_less (cand_ord (x, y)) then x else y) cands' cand
|> (fn best => (SOME best, remove (op =) best cands))
fun try_eliminate i l labels steps =
let
val (steps_before, (cand as Prove {facts = (lfs, _), ...}) :: steps_after) =
chop i steps
val succs = collect_successors steps_after labels
val (succs', hopelesses) = split_list (map (merge_steps (!preplay_data) cand) succs)
in
(case try (map ((fn Played time => time) o
forced_intermediate_preplay_outcome_of_isar_step (!preplay_data))) labels of
NONE => steps
| SOME times0 =>
let
val n = length labels
val total_time = Library.foldl (op +) (reference_time l, times0)
val timeout = adjust_merge_timeout preplay_timeout
(Time.fromReal (Time.toReal total_time / Real.fromInt n))
val meths_outcomess =
@{map 2} (preplay_isar_step ctxt [] timeout) hopelesses succs'
in
(case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of
NONE => steps
| SOME times =>
(decrement_step_count ();
@{map 3} (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data)
times succs' meths_outcomess;
map (replace_successor l labels) lfs;
steps_before @ update_steps succs' steps_after))
end)
end
fun compression_loop candidates steps =
if not (compress_further ()) then
steps
else
(case pop_next_candidate candidates of
(NONE, _) => steps
| (SOME (l, (num_xs, _)), candidates') =>
(case find_index (curry (op =) (SOME l) o label_of_isar_step) steps of
~1 => steps
| i =>
let
val successors = get_successors l
val num_successors = length successors
in
if num_successors > (if num_xs > 0 then 1 else compress_degree) then
steps
else
steps
|> not (null successors) ? try_eliminate i l successors
|> compression_loop candidates'
end))
fun add_cand (Prove {obtains, label, goal, ...}) =
cons (label, (length obtains, size_of_term goal))
| add_cand _ = I
val candidates = fold add_cand (fst (split_last steps)) []
in
compression_loop candidates steps
end
fun compress_proof (proof as (Proof {steps, ...})) =
if compress_further () then
isar_proof_with_steps proof (compress_steps steps)
else
proof
and compress_steps steps =
steps
|> map (fn step => step |> compress_further () ? compress_sub_levels)
|> compress_further () ? compress_top_level
and compress_sub_levels (Prove {qualifiers, obtains, label, goal, subproofs, facts,
proof_methods, comment}) =
Prove {
qualifiers = qualifiers,
obtains = obtains,
label = label,
goal = goal,
subproofs = map compress_proof subproofs,
facts = facts,
proof_methods = proof_methods,
comment = comment}
|> compress_further () ? elim_subproofs
| compress_sub_levels step = step
in
compress_proof proof
end
end;