src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
author wenzelm
Sat Apr 02 23:29:05 2016 +0200 (2016-04-02 ago)
changeset 62826 eb94e570c1a4
parent 62219 dbac573b27e7
child 67560 0fa87bd86566
permissions -rw-r--r--
prefer infix operations;
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
     2     Author:     Steffen Juilf Smolka, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Compression of Isar proofs by merging steps.
     6 Only proof steps using the same proof method are merged.
     7 *)
     8 
     9 signature SLEDGEHAMMER_ISAR_COMPRESS =
    10 sig
    11   type isar_proof = Sledgehammer_Isar_Proof.isar_proof
    12   type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
    13 
    14   val compress_isar_proof : Proof.context -> real -> Time.time ->
    15     isar_preplay_data Unsynchronized.ref -> isar_proof -> isar_proof
    16 end;
    17 
    18 structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS =
    19 struct
    20 
    21 open Sledgehammer_Util
    22 open Sledgehammer_Proof_Methods
    23 open Sledgehammer_Isar_Proof
    24 open Sledgehammer_Isar_Preplay
    25 
    26 fun collect_successors steps lbls =
    27   let
    28     fun collect_steps _ (accum as ([], _)) = accum
    29       | collect_steps [] accum = accum
    30       | collect_steps (step :: steps) accum = collect_steps steps (collect_step step accum)
    31     and collect_step (step as Prove (_, _, l, _, subproofs, _, _, _)) x =
    32         (case collect_subproofs subproofs x of
    33           (accum as ([], _)) => accum
    34         | accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum)
    35         | collect_step _ accum = accum
    36     and collect_subproofs [] accum = accum
    37       | collect_subproofs (proof :: subproofs) accum =
    38         (case collect_steps (steps_of_isar_proof proof) accum of
    39           accum as ([], _) => accum
    40         | accum => collect_subproofs subproofs accum)
    41   in
    42     rev (snd (collect_steps steps (lbls, [])))
    43   end
    44 
    45 fun update_steps updates steps =
    46   let
    47     fun update_steps [] updates = ([], updates)
    48       | update_steps steps [] = (steps, [])
    49       | update_steps (step :: steps) updates = update_step step (update_steps steps updates)
    50     and update_step step (steps, []) = (step :: steps, [])
    51       | update_step (Prove (qs, xs, l, t, subproofs, facts, meths, comment))
    52           (steps,
    53            updates as Prove (qs', xs', l', t', subproofs', facts', meths', comment') :: updates') =
    54         (if l = l' then
    55            update_subproofs subproofs' updates'
    56            |>> (fn subproofs'' => Prove (qs', xs', l', t', subproofs'', facts', meths', comment'))
    57          else
    58            update_subproofs subproofs updates
    59            |>> (fn subproofs' => Prove (qs, xs, l, t, subproofs', facts, meths, comment)))
    60         |>> (fn step => step :: steps)
    61       | update_step step (steps, updates) = (step :: steps, updates)
    62     and update_subproofs [] updates = ([], updates)
    63       | update_subproofs steps [] = (steps, [])
    64       | update_subproofs (proof :: subproofs) updates =
    65         update_proof proof (update_subproofs subproofs updates)
    66     and update_proof proof (proofs, []) = (proof :: proofs, [])
    67       | update_proof (Proof (xs, assms, steps)) (proofs, updates) =
    68         let val (steps', updates') = update_steps steps updates in
    69           (Proof (xs, assms, steps') :: proofs, updates')
    70         end
    71   in
    72     fst (update_steps steps (rev updates))
    73   end
    74 
    75 fun merge_methods preplay_data (l1, meths1) (l2, meths2) =
    76   let
    77     fun is_hopeful l meth =
    78       let val outcome = preplay_outcome_of_isar_step_for_method preplay_data l meth in
    79         not (Lazy.is_finished outcome) orelse
    80         (case Lazy.force outcome of Played _ => true | Play_Timed_Out _ => true | _ => false)
    81       end
    82 
    83     val (hopeful, hopeless) =
    84       meths2 @ subtract (op =) meths2 meths1
    85       |> List.partition (is_hopeful l1 andf is_hopeful l2)
    86   in
    87     (hopeful @ hopeless, hopeless)
    88   end
    89 
    90 fun merge_steps preplay_data (Prove ([], xs1, l1, _, subproofs1, (lfs1, gfs1), meths1, comment1))
    91       (Prove (qs2, xs2, l2, t, subproofs2, (lfs2, gfs2), meths2, comment2)) =
    92   let
    93     val (meths, hopeless) = merge_methods preplay_data (l1, meths1) (l2, meths2)
    94     val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
    95     val gfs = union (op =) gfs1 gfs2
    96   in
    97     (Prove (qs2, inter (op =) (Term.add_frees t []) (xs1 @ xs2), l2, t,
    98        subproofs1 @ subproofs2, sort_facts (lfs, gfs), meths, comment1 ^ comment2),
    99      hopeless)
   100   end
   101 
   102 val merge_slack_time = seconds 0.01
   103 val merge_slack_factor = 1.5
   104 
   105 fun adjust_merge_timeout max time =
   106   let val timeout = time_mult merge_slack_factor (merge_slack_time + time) in
   107     if max < timeout then max else timeout
   108   end
   109 
   110 val compress_degree = 2
   111 
   112 (* Precondition: The proof must be labeled canonically. *)
   113 fun compress_isar_proof ctxt compress preplay_timeout preplay_data proof =
   114   if compress <= 1.0 then
   115     proof
   116   else
   117     let
   118       val (compress_further, decrement_step_count) =
   119         let
   120           val number_of_steps = add_isar_steps (steps_of_isar_proof proof) 0
   121           val target_number_of_steps = Real.ceil (Real.fromInt number_of_steps / compress)
   122           val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps)
   123         in
   124           (fn () => !delta > 0, fn () => delta := !delta - 1)
   125         end
   126 
   127       val (get_successors, replace_successor) =
   128         let
   129           fun add_refs (Prove (_, _, l, _, _, (lfs, _), _, _)) =
   130               fold (fn key => Canonical_Label_Tab.cons_list (key, l)) lfs
   131             | add_refs _ = I
   132 
   133           val tab =
   134             Canonical_Label_Tab.empty
   135             |> fold_isar_steps add_refs (steps_of_isar_proof proof)
   136             (* "rev" should have the same effect as "sort canonical_label_ord" *)
   137             |> Canonical_Label_Tab.map (K rev)
   138             |> Unsynchronized.ref
   139 
   140           fun get_successors l = Canonical_Label_Tab.lookup_list (!tab) l
   141           fun set_successors l refs = tab := Canonical_Label_Tab.update (l, refs) (!tab)
   142           fun replace_successor old new dest =
   143             get_successors dest
   144             |> Ord_List.remove canonical_label_ord old
   145             |> Ord_List.union canonical_label_ord new
   146             |> set_successors dest
   147         in
   148           (get_successors, replace_successor)
   149         end
   150 
   151       fun reference_time l =
   152         (case forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l of
   153           Played time => time
   154         | _ => preplay_timeout)
   155 
   156       (* elimination of trivial, one-step subproofs *)
   157       fun elim_one_subproof time (step as Prove (qs, xs, l, t, _, (lfs, gfs), meths, comment)) subs
   158           nontriv_subs =
   159         if null subs orelse not (compress_further ()) then
   160           Prove (qs, xs, l, t, List.revAppend (nontriv_subs, subs), (lfs, gfs), meths, comment)
   161         else
   162           (case subs of
   163             (sub as Proof (_, assms, [Prove (_, _, l', _, [], (lfs', gfs'), meths', _)])) :: subs =>
   164             let
   165               (* merge steps *)
   166               val subs'' = subs @ nontriv_subs
   167               val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs')
   168               val gfs'' = union (op =) gfs' gfs
   169               val (meths'' as _ :: _, hopeless) =
   170                 merge_methods (!preplay_data) (l', meths') (l, meths)
   171               val step'' = Prove (qs, xs, l, t, subs'', (lfs'', gfs''), meths'', comment)
   172 
   173               (* check if the modified step can be preplayed fast enough *)
   174               val timeout = adjust_merge_timeout preplay_timeout (time + reference_time l')
   175             in
   176               (case preplay_isar_step ctxt [] timeout hopeless step'' of
   177                 meths_outcomes as (_, Played time'') :: _ =>
   178                 (* "l'" successfully eliminated *)
   179                 (decrement_step_count ();
   180                  set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step'' meths_outcomes;
   181                  map (replace_successor l' [l]) lfs';
   182                  elim_one_subproof time'' step'' subs nontriv_subs)
   183               | _ => elim_one_subproof time step subs (sub :: nontriv_subs))
   184             end
   185           | sub :: subs => elim_one_subproof time step subs (sub :: nontriv_subs))
   186 
   187       fun elim_subproofs (step as Prove (_, _, l, _, subproofs, _, _, _)) =
   188           if exists (null o tl o steps_of_isar_proof) subproofs then
   189             elim_one_subproof (reference_time l) step subproofs []
   190           else
   191             step
   192         | elim_subproofs step = step
   193 
   194       fun compress_top_level steps =
   195         let
   196           val cand_key = apfst (length o get_successors)
   197           val cand_ord =
   198             prod_ord int_ord (prod_ord (int_ord o swap) (int_ord o swap)) o apply2 cand_key
   199 
   200           fun pop_next_candidate [] = (NONE, [])
   201             | pop_next_candidate (cands as (cand :: cands')) =
   202               fold (fn x => fn y => if cand_ord (x, y) = LESS then x else y) cands' cand
   203               |> (fn best => (SOME best, remove (op =) best cands))
   204 
   205           fun try_eliminate i l labels steps =
   206             let
   207               val (steps_before, (cand as Prove (_, _, _, _, _, (lfs, _), _, _)) :: steps_after) =
   208                 chop i steps
   209               val succs = collect_successors steps_after labels
   210               val (succs', hopelesses) = split_list (map (merge_steps (!preplay_data) cand) succs)
   211             in
   212               (case try (map ((fn Played time => time) o
   213                   forced_intermediate_preplay_outcome_of_isar_step (!preplay_data))) labels of
   214                 NONE => steps
   215               | SOME times0 =>
   216                 let
   217                   val n = length labels
   218                   val total_time = Library.foldl (op +) (reference_time l, times0)
   219                   val timeout = adjust_merge_timeout preplay_timeout
   220                     (Time.fromReal (Time.toReal total_time / Real.fromInt n))
   221                   val meths_outcomess =
   222                     @{map 2} (preplay_isar_step ctxt [] timeout) hopelesses succs'
   223                 in
   224                   (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of
   225                     NONE => steps
   226                   | SOME times =>
   227                     (* "l" successfully eliminated *)
   228                     (decrement_step_count ();
   229                      @{map 3} (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data)
   230                        times succs' meths_outcomess;
   231                      map (replace_successor l labels) lfs;
   232                      steps_before @ update_steps succs' steps_after))
   233                 end)
   234             end
   235 
   236           fun compression_loop candidates steps =
   237             if not (compress_further ()) then
   238               steps
   239             else
   240               (case pop_next_candidate candidates of
   241                 (NONE, _) => steps (* no more candidates for elimination *)
   242               | (SOME (l, (num_xs, _)), candidates') =>
   243                 (case find_index (curry (op =) (SOME l) o label_of_isar_step) steps of
   244                   ~1 => steps
   245                 | i =>
   246                   let
   247                     val successors = get_successors l
   248                     val num_successors = length successors
   249                   in
   250                     (* Careful with "obtain", so we don't "obtain" twice the same variable after a
   251                        merge. *)
   252                     if num_successors > (if num_xs > 0 then 1 else compress_degree) then
   253                       steps
   254                     else
   255                       steps
   256                       |> not (null successors) ? try_eliminate i l successors
   257                       |> compression_loop candidates'
   258                   end))
   259 
   260           fun add_cand (Prove (_, xs, l, t, _, _, _, _)) = cons (l, (length xs, size_of_term t))
   261             | add_cand _ = I
   262 
   263           (* the very last step is not a candidate *)
   264           val candidates = fold add_cand (fst (split_last steps)) []
   265         in
   266           compression_loop candidates steps
   267         end
   268 
   269       (* Proofs are compressed bottom-up, beginning with the innermost subproofs. On the innermost
   270          proof level, the proof steps have no subproofs. In the best case, these steps can be merged
   271          into just one step, resulting in a trivial subproof. Going one level up, trivial subproofs
   272          can be eliminated. In the best case, this once again leads to a proof whose proof steps do
   273          not have subproofs. Applying this approach recursively will result in a flat proof in the
   274          best cast. *)
   275       fun compress_proof (proof as (Proof (xs, assms, steps))) =
   276         if compress_further () then Proof (xs, assms, compress_steps steps) else proof
   277       and compress_steps steps =
   278         (* bottom-up: compress innermost proofs first *)
   279         steps
   280         |> map (fn step => step |> compress_further () ? compress_sub_levels)
   281         |> compress_further () ? compress_top_level
   282       and compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) =
   283           (* compress subproofs *)
   284           Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths, comment)
   285           (* eliminate trivial subproofs *)
   286           |> compress_further () ? elim_subproofs
   287         | compress_sub_levels step = step
   288     in
   289       compress_proof proof
   290     end
   291 
   292 end;