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