src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
author blanchet
Thu Nov 21 12:29:29 2013 +0100 (2013-11-21 ago)
changeset 54546 8b403a7a8c44
parent 54504 096f7d452164
child 54700 64177ce0a7bd
permissions -rw-r--r--
fixed spying so that the envirnoment variables are queried at run-time not at build-time
smolkas@51130
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_compress.ML
smolkas@50263
     2
    Author:     Jasmin Blanchette, TU Muenchen
smolkas@50263
     3
    Author:     Steffen Juilf Smolka, TU Muenchen
smolkas@50263
     4
smolkas@52633
     5
Compression of isar proofs by merging steps.
smolkas@52633
     6
Only proof steps using the MetisM proof_method are merged.
smolkas@52556
     7
smolkas@52556
     8
PRE CONDITION: the proof must be labeled canocially, see
smolkas@52556
     9
Slegehammer_Proof.relabel_proof_canonically
smolkas@50263
    10
*)
smolkas@50263
    11
smolkas@51130
    12
signature SLEDGEHAMMER_COMPRESS =
smolkas@50259
    13
sig
smolkas@51179
    14
  type isar_proof = Sledgehammer_Proof.isar_proof
smolkas@52556
    15
  type preplay_interface = Sledgehammer_Preplay.preplay_interface
smolkas@52556
    16
blanchet@53763
    17
  val compress_proof : real -> preplay_interface -> isar_proof -> isar_proof
blanchet@54504
    18
end;
smolkas@52556
    19
smolkas@51130
    20
structure Sledgehammer_Compress : SLEDGEHAMMER_COMPRESS =
smolkas@50259
    21
struct
smolkas@50259
    22
smolkas@50265
    23
open Sledgehammer_Util
smolkas@50264
    24
open Sledgehammer_Proof
smolkas@50923
    25
open Sledgehammer_Preplay
smolkas@50259
    26
smolkas@52556
    27
smolkas@52556
    28
(*** util ***)
smolkas@50259
    29
smolkas@52556
    30
(* traverses steps in post-order and collects the steps with the given labels *)
smolkas@52556
    31
fun collect_successors steps lbls =
smolkas@52556
    32
  let
smolkas@52556
    33
    fun do_steps _ ([], accu) = ([], accu)
smolkas@52556
    34
      | do_steps [] (lbls, accu) = (lbls, accu)
smolkas@52556
    35
      | do_steps (step::steps) (lbls, accu) =
smolkas@52556
    36
          do_steps steps (do_step step (lbls, accu))
smolkas@50259
    37
smolkas@52556
    38
    and do_step (Let _) x = x
smolkas@52556
    39
      | do_step (step as Prove (_, _, l, _, subproofs, _)) x =
smolkas@52556
    40
        (case do_subproofs subproofs x of
smolkas@52556
    41
          ([], accu) => ([], accu)
smolkas@52556
    42
        | (lbls as l'::lbls', accu) =>
smolkas@52556
    43
            if l=l'
smolkas@52556
    44
              then (lbls', step::accu)
smolkas@52556
    45
              else (lbls, accu))
smolkas@50259
    46
smolkas@52556
    47
    and do_subproofs [] x = x
smolkas@52556
    48
      | do_subproofs (proof::subproofs) x =
smolkas@52556
    49
          (case do_steps (steps_of_proof proof) x of
smolkas@52556
    50
            ([], accu) => ([], accu)
smolkas@52556
    51
          | x => do_subproofs subproofs x)
smolkas@52556
    52
  in
smolkas@52556
    53
    case do_steps steps (lbls, []) of
smolkas@52556
    54
      ([], succs) => rev succs
smolkas@52556
    55
    | _ => raise Fail "Sledgehammer_Compress: collect_successors"
smolkas@52556
    56
  end
smolkas@50259
    57
smolkas@52556
    58
(* traverses steps in reverse post-order and inserts the given updates *)
smolkas@52556
    59
fun update_steps steps updates =
smolkas@52556
    60
  let
smolkas@52556
    61
    fun do_steps [] updates = ([], updates)
smolkas@52556
    62
      | do_steps steps [] = (steps, [])
smolkas@52556
    63
      | do_steps (step::steps) updates =
smolkas@52556
    64
          do_step step (do_steps steps updates)
blanchet@50672
    65
smolkas@52556
    66
    and do_step step (steps, []) = (step::steps, [])
smolkas@52556
    67
      | do_step (step as Let _) (steps, updates) = (step::steps, updates)
smolkas@52556
    68
      | do_step (Prove (qs, xs, l, t, subproofs, by))
smolkas@52556
    69
          (steps, updates as
smolkas@52556
    70
           Prove(qs', xs', l', t', subproofs', by') :: updates') =
smolkas@52556
    71
          let
smolkas@52556
    72
            val (subproofs, updates) =
smolkas@52556
    73
              if l=l'
smolkas@52556
    74
                then do_subproofs subproofs' updates'
smolkas@52556
    75
                else do_subproofs subproofs updates
smolkas@52556
    76
          in
smolkas@52556
    77
            if l=l'
smolkas@52556
    78
              then (Prove (qs', xs', l', t', subproofs, by') :: steps,
smolkas@52556
    79
                    updates)
smolkas@52556
    80
              else (Prove (qs, xs, l, t, subproofs, by) :: steps,
smolkas@52556
    81
                    updates)
smolkas@52556
    82
          end
smolkas@52556
    83
      | do_step _ _ =
smolkas@52556
    84
          raise Fail "Sledgehammer_Compress: update_steps (invalid update)"
blanchet@50672
    85
smolkas@52556
    86
    and do_subproofs [] updates = ([], updates)
smolkas@52556
    87
      | do_subproofs steps [] = (steps, [])
smolkas@52556
    88
      | do_subproofs (proof::subproofs) updates =
smolkas@52556
    89
          do_proof proof (do_subproofs subproofs updates)
smolkas@50923
    90
smolkas@52556
    91
    and do_proof proof (proofs, []) = (proof :: proofs, [])
smolkas@52556
    92
      | do_proof (Proof (fix, assms, steps)) (proofs, updates) =
smolkas@52556
    93
          let val (steps, updates) = do_steps steps updates in
smolkas@52556
    94
            (Proof (fix, assms, steps) :: proofs, updates)
smolkas@52556
    95
          end
smolkas@52556
    96
  in
smolkas@52556
    97
    case do_steps steps (rev updates) of
smolkas@52556
    98
      (steps, []) => steps
smolkas@52556
    99
    | _ => raise Fail "Sledgehammer_Compress: update_steps"
smolkas@52556
   100
  end
blanchet@50672
   101
smolkas@52556
   102
(* tries merging the first step into the second step *)
smolkas@52556
   103
fun try_merge
smolkas@52592
   104
  (Prove (_, Fix [], lbl1, _, [], By ((lfs1, gfs1), MetisM)))
smolkas@52592
   105
  (Prove (qs2, fix, lbl2, t, subproofs, By ((lfs2, gfs2), MetisM))) =
smolkas@52556
   106
      let
smolkas@52556
   107
        val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
smolkas@52556
   108
        val gfs = union (op =) gfs1 gfs2
smolkas@52556
   109
      in
smolkas@52592
   110
        SOME (Prove (qs2, fix, lbl2, t, subproofs, By ((lfs, gfs), MetisM)))
smolkas@52556
   111
      end
smolkas@52556
   112
  | try_merge _ _ = NONE
blanchet@50672
   113
smolkas@52556
   114
smolkas@52556
   115
smolkas@52556
   116
(*** main function ***)
smolkas@52556
   117
blanchet@53763
   118
val compress_degree = 2
blanchet@53762
   119
val merge_timeout_slack = 1.2
blanchet@53762
   120
smolkas@52556
   121
(* PRE CONDITION: the proof must be labeled canocially, see
smolkas@52556
   122
   Slegehammer_Proof.relabel_proof_canonically *)
blanchet@53763
   123
fun compress_proof isar_compress
blanchet@53762
   124
        ({get_preplay_time, set_preplay_time, preplay_quietly, ...}
blanchet@53762
   125
         : preplay_interface)
smolkas@52591
   126
  proof =
smolkas@52556
   127
  if isar_compress <= 1.0 then
smolkas@52556
   128
    proof
smolkas@52556
   129
  else
smolkas@52556
   130
  let
smolkas@52556
   131
    val (compress_further : unit -> bool,
smolkas@52556
   132
         decrement_step_count : unit -> unit) =
smolkas@52556
   133
      let
smolkas@52592
   134
        val number_of_steps = add_proof_steps (steps_of_proof proof) 0
smolkas@52556
   135
        val target_number_of_steps =
smolkas@52556
   136
          Real.fromInt number_of_steps / isar_compress
smolkas@52556
   137
          |> Real.round
smolkas@52556
   138
          |> curry Int.max 2 (* don't produce one-step isar proofs *)
smolkas@52556
   139
        val delta =
smolkas@52556
   140
          number_of_steps - target_number_of_steps |> Unsynchronized.ref
smolkas@52556
   141
      in
smolkas@52614
   142
        (fn () => !delta > 0,
smolkas@52556
   143
         fn () => delta := !delta - 1)
smolkas@52556
   144
      end
smolkas@52556
   145
smolkas@52556
   146
smolkas@52556
   147
    val (get_successors : label -> label list,
smolkas@52556
   148
         replace_successor: label -> label list -> label -> unit) =
smolkas@52556
   149
      let
smolkas@52556
   150
        fun add_refs (Let _) tab = tab
blanchet@54503
   151
          | add_refs (Prove (_, _, v, _, _, By ((lfs, _), _))) tab =
blanchet@54503
   152
              fold (fn key => Canonical_Lbl_Tab.cons_list (key, v)) lfs tab
smolkas@52556
   153
smolkas@52556
   154
        val tab =
smolkas@52556
   155
          Canonical_Lbl_Tab.empty
smolkas@52556
   156
          |> fold_isar_steps add_refs (steps_of_proof proof)
smolkas@52556
   157
          (* rev should have the same effect as sort canonical_label_ord *)
smolkas@52556
   158
          |> Canonical_Lbl_Tab.map (K rev)
smolkas@52556
   159
          |> Unsynchronized.ref
blanchet@50672
   160
smolkas@52556
   161
        fun get_successors l = Canonical_Lbl_Tab.lookup_list (!tab) l
smolkas@52556
   162
        fun set_successors l refs =
smolkas@52556
   163
          tab := Canonical_Lbl_Tab.update (l, refs) (!tab)
smolkas@52556
   164
        fun replace_successor old new dest =
smolkas@52556
   165
          set_successors dest
smolkas@52556
   166
            (get_successors dest |> Ord_List.remove canonical_label_ord old
smolkas@52556
   167
                                |> Ord_List.union canonical_label_ord new)
smolkas@51260
   168
blanchet@50672
   169
      in
smolkas@52556
   170
         (get_successors, replace_successor)
blanchet@50672
   171
      end
blanchet@50672
   172
smolkas@52556
   173
smolkas@52592
   174
smolkas@52556
   175
    (** elimination of trivial, one-step subproofs **)
smolkas@52556
   176
smolkas@52556
   177
    fun elim_subproofs' time qs fix l t lfs gfs subs nontriv_subs =
smolkas@52556
   178
      if null subs orelse not (compress_further ()) then
smolkas@52626
   179
        (set_preplay_time l (false, time);
smolkas@52556
   180
         Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs),
blanchet@54503
   181
                By ((lfs, gfs), MetisM)))
smolkas@52556
   182
      else
smolkas@52556
   183
        case subs of
smolkas@52556
   184
          ((sub as Proof(_, Assume assms, sub_steps)) :: subs) =>
smolkas@52556
   185
            (let
smolkas@52556
   186
smolkas@52556
   187
              (* trivial subproofs have exactly one Prove step *)
smolkas@52592
   188
              val SOME (Prove (_, Fix [], l', _, [],
smolkas@52592
   189
                By ((lfs', gfs'), MetisM))) = (try the_single) sub_steps
smolkas@52556
   190
smolkas@52556
   191
              (* only touch proofs that can be preplayed sucessfully *)
smolkas@52626
   192
              val (false, time') = get_preplay_time l'
smolkas@52556
   193
smolkas@52556
   194
              (* merge steps *)
smolkas@52556
   195
              val subs'' = subs @ nontriv_subs
smolkas@52556
   196
              val lfs'' =
smolkas@52556
   197
                subtract (op =) (map fst assms) lfs'
smolkas@52556
   198
                |> union (op =) lfs
smolkas@52556
   199
              val gfs'' = union (op =) gfs' gfs
blanchet@54503
   200
              val by = By ((lfs'', gfs''), MetisM)
smolkas@52556
   201
              val step'' = Prove (qs, fix, l, t, subs'', by)
smolkas@52556
   202
smolkas@52556
   203
              (* check if the modified step can be preplayed fast enough *)
smolkas@52556
   204
              val timeout = time_mult merge_timeout_slack (Time.+(time, time'))
smolkas@52556
   205
              val (false, time'') = preplay_quietly timeout step''
smolkas@52556
   206
smolkas@52556
   207
            in
smolkas@52626
   208
              decrement_step_count (); (* l' successfully eliminated! *)
smolkas@52556
   209
              map (replace_successor l' [l]) lfs';
smolkas@52556
   210
              elim_subproofs' time'' qs fix l t lfs'' gfs'' subs nontriv_subs
smolkas@52556
   211
            end
smolkas@52556
   212
            handle Bind =>
smolkas@52556
   213
              elim_subproofs' time qs fix l t lfs gfs subs (sub::nontriv_subs))
smolkas@52556
   214
        | _ => raise Fail "Sledgehammer_Compress: elim_subproofs'"
smolkas@52556
   215
smolkas@52556
   216
smolkas@52556
   217
    fun elim_subproofs (step as Let _) = step
smolkas@52556
   218
      | elim_subproofs
smolkas@52592
   219
        (step as Prove (qs, fix, l, t, subproofs, By ((lfs, gfs), MetisM))) =
smolkas@52556
   220
          if subproofs = [] then step else
smolkas@52626
   221
            case get_preplay_time l of
smolkas@52626
   222
              (true, _) => step (* timeout or fail *)
smolkas@52556
   223
            | (false, time) =>
smolkas@52556
   224
                elim_subproofs' time qs fix l t lfs gfs subproofs []
smolkas@52556
   225
smolkas@52556
   226
smolkas@52556
   227
smolkas@52556
   228
    (** top_level compression: eliminate steps by merging them into their
smolkas@52556
   229
        successors **)
smolkas@52556
   230
smolkas@52556
   231
    fun compress_top_level steps =
blanchet@50672
   232
      let
smolkas@52556
   233
smolkas@52556
   234
        (* #successors, (size_of_term t, position) *)
smolkas@52556
   235
        fun cand_key (i, l, t_size) =
smolkas@52556
   236
          (get_successors l |> length, (t_size, i))
smolkas@52556
   237
smolkas@52556
   238
        val compression_ord =
smolkas@52556
   239
          prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord)
smolkas@52556
   240
          #> rev_order
smolkas@52556
   241
smolkas@52556
   242
        val cand_ord = pairself cand_key #> compression_ord
smolkas@52556
   243
smolkas@52556
   244
        fun pop_next_cand candidates =
smolkas@52556
   245
          case max_list cand_ord candidates of
smolkas@52556
   246
            NONE => (NONE, [])
smolkas@52556
   247
          | cand as SOME (i, _, _) =>
smolkas@52556
   248
              (cand, filter_out (fn (j, _, _) => j=i) candidates)
smolkas@52556
   249
smolkas@52556
   250
        val candidates =
smolkas@52556
   251
          let
blanchet@54503
   252
            fun add_cand (_, Let _) = I
smolkas@52556
   253
              | add_cand (i, Prove (_, _, l, t, _, _)) =
smolkas@52556
   254
                  cons (i, l, size_of_term t)
smolkas@52556
   255
          in
smolkas@52556
   256
            (steps
smolkas@52556
   257
            |> split_last |> fst (* last step must NOT be eliminated *)
smolkas@52556
   258
            |> fold_index add_cand) []
smolkas@52556
   259
          end
smolkas@52556
   260
blanchet@54503
   261
        fun try_eliminate (i, l, _) succ_lbls steps =
smolkas@52556
   262
          let
smolkas@52556
   263
            (* only touch steps that can be preplayed successfully *)
smolkas@52626
   264
            val (false, time) = get_preplay_time l
smolkas@52556
   265
smolkas@52626
   266
            val succ_times =
smolkas@52626
   267
              map (get_preplay_time #> (fn (false, t) => t)) succ_lbls
smolkas@52556
   268
smolkas@52556
   269
            val timeslice =
smolkas@52556
   270
              time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
smolkas@52556
   271
smolkas@52556
   272
            val timeouts =
smolkas@52556
   273
              map (curry Time.+ timeslice #> time_mult merge_timeout_slack)
smolkas@52556
   274
                succ_times
smolkas@52556
   275
smolkas@52592
   276
            val ((cand as Prove (_, _, l, _, _,
smolkas@52592
   277
              By ((lfs, _), MetisM))) :: steps') = drop i steps
smolkas@52556
   278
smolkas@52556
   279
            (* FIXME: debugging *)
smolkas@52556
   280
            val _ = (if (label_of_step cand |> the) <> l then
smolkas@52556
   281
                      raise Fail "Sledgehammer_Compress: try_eliminate"
smolkas@52556
   282
                    else ())
smolkas@52556
   283
smolkas@52556
   284
            val succs = collect_successors steps' succ_lbls
smolkas@52556
   285
            val succs' = map (try_merge cand #> the) succs
smolkas@52556
   286
smolkas@52692
   287
            (* TODO: should be lazy: stop preplaying as soon as one step
smolkas@52692
   288
               fails/times out *)
smolkas@52556
   289
            val preplay_times =
smolkas@52556
   290
              map (uncurry preplay_quietly) (timeouts ~~ succs')
smolkas@52556
   291
smolkas@52556
   292
            (* ensure none of the modified successors timed out *)
smolkas@52556
   293
            val false = List.exists fst preplay_times
smolkas@52556
   294
smolkas@52556
   295
            val (steps1, _::steps2) = chop i steps
smolkas@52556
   296
smolkas@52556
   297
            (* replace successors with their modified versions *)
smolkas@52556
   298
            val steps2 = update_steps steps2 succs'
smolkas@52556
   299
smolkas@52556
   300
          in
smolkas@52626
   301
            decrement_step_count (); (* candidate successfully eliminated *)
smolkas@52626
   302
            map (uncurry set_preplay_time) (succ_lbls ~~ preplay_times);
smolkas@52556
   303
            map (replace_successor l succ_lbls) lfs;
smolkas@52556
   304
            (* removing the step would mess up the indices
smolkas@52556
   305
               -> replace with dummy step instead *)
smolkas@52556
   306
            steps1 @ dummy_isar_step :: steps2
smolkas@52556
   307
          end
smolkas@52556
   308
          handle Bind => steps
smolkas@52556
   309
               | Match => steps
smolkas@52556
   310
               | Option.Option => steps
smolkas@52556
   311
smolkas@52556
   312
        fun compression_loop candidates steps =
smolkas@52556
   313
          if not (compress_further ()) then
smolkas@52556
   314
            steps
smolkas@52556
   315
          else
smolkas@52556
   316
            case pop_next_cand candidates of
smolkas@52556
   317
              (NONE, _) => steps (* no more candidates for elimination *)
smolkas@52556
   318
            | (SOME (cand as (_, l, _)), candidates) =>
smolkas@52556
   319
              let
smolkas@52556
   320
                val successors = get_successors l
smolkas@52556
   321
              in
blanchet@53763
   322
                if length successors > compress_degree
smolkas@52556
   323
                  then steps
smolkas@52556
   324
                  else compression_loop candidates
smolkas@52556
   325
                         (try_eliminate cand successors steps)
smolkas@52556
   326
              end
smolkas@52556
   327
smolkas@52556
   328
blanchet@50672
   329
      in
smolkas@52556
   330
        compression_loop candidates steps
smolkas@52556
   331
        |> filter_out (fn step => step = dummy_isar_step)
blanchet@50672
   332
      end
smolkas@52556
   333
smolkas@52556
   334
smolkas@52556
   335
smolkas@52556
   336
    (** recusion over the proof tree **)
smolkas@52556
   337
    (*
smolkas@52556
   338
       Proofs are compressed bottom-up, beginning with the innermost
smolkas@52556
   339
       subproofs.
smolkas@52556
   340
       On the innermost proof level, the proof steps have no subproofs.
smolkas@52556
   341
       In the best case, these steps can be merged into just one step,
smolkas@52556
   342
       resulting in a trivial subproof. Going one level up, trivial subproofs
smolkas@52556
   343
       can be eliminated. In the best case, this once again leads to a proof
smolkas@52556
   344
       whose proof steps do not have subproofs. Applying this approach
smolkas@52556
   345
       recursively will result in a flat proof in the best cast.
smolkas@52556
   346
    *)
smolkas@52556
   347
smolkas@52556
   348
    infix 1 ?>
smolkas@52556
   349
    fun x ?> f = if compress_further () then f x else x
smolkas@52556
   350
smolkas@52556
   351
    fun do_proof (proof as (Proof (fix, assms, steps))) =
smolkas@52556
   352
      if compress_further ()
smolkas@52556
   353
        then Proof (fix, assms, do_steps steps)
smolkas@52556
   354
        else proof
smolkas@52556
   355
smolkas@52556
   356
    and do_steps steps =
smolkas@52556
   357
      (* bottom-up: compress innermost proofs first *)
smolkas@52556
   358
      steps |> map (fn step => step ?> do_sub_levels)
smolkas@52556
   359
            ?> compress_top_level
smolkas@52556
   360
smolkas@52556
   361
    and do_sub_levels (Let x) = Let x
smolkas@52556
   362
      | do_sub_levels (Prove (qs, xs, l, t, subproofs, by)) =
smolkas@52556
   363
          (* compress subproofs *)
smolkas@52556
   364
          Prove (qs, xs, l, t, map do_proof subproofs, by)
smolkas@52556
   365
            (* eliminate trivial subproofs *)
smolkas@52556
   366
            ?> elim_subproofs
smolkas@52556
   367
blanchet@50672
   368
  in
smolkas@52556
   369
    do_proof proof
blanchet@50672
   370
  end
smolkas@50259
   371
blanchet@54504
   372
end;