src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
author blanchet
Sun Feb 02 20:53:51 2014 +0100 (2014-02-02)
changeset 55243 66709d41601e
parent 55223 3c593bad6b31
child 55244 12e1a5d8ee48
permissions -rw-r--r--
reset timing information after changes
     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 : real -> isar_preplay_data -> isar_proof -> isar_proof
    15 end;
    16 
    17 structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS =
    18 struct
    19 
    20 open Sledgehammer_Util
    21 open Sledgehammer_Reconstructor
    22 open Sledgehammer_Isar_Proof
    23 open Sledgehammer_Isar_Preplay
    24 
    25 val dummy_isar_step = Let (Term.dummy, Term.dummy)
    26 
    27 (* traverses steps in post-order and collects the steps with the given labels *)
    28 fun collect_successors steps lbls =
    29   let
    30     fun do_steps _ ([], accu) = ([], accu)
    31       | do_steps [] accum = accum
    32       | do_steps (step :: steps) accum = do_steps steps (do_step step accum)
    33     and do_step (Let _) x = x
    34       | do_step (step as Prove (_, _, l, _, subproofs, _)) x =
    35         (case do_subproofs subproofs x of
    36           ([], accu) => ([], accu)
    37         | accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum)
    38     and do_subproofs [] x = x
    39       | do_subproofs (proof :: subproofs) x =
    40         (case do_steps (steps_of_proof proof) x of
    41           accum as ([], _) => accum
    42         | accum => do_subproofs subproofs accum)
    43   in
    44     (case do_steps steps (lbls, []) of
    45       ([], succs) => rev succs
    46     | _ => raise Fail "Sledgehammer_Isar_Compress: collect_successors")
    47   end
    48 
    49 (* traverses steps in reverse post-order and inserts the given updates *)
    50 fun update_steps steps updates =
    51   let
    52     fun do_steps [] updates = ([], updates)
    53       | do_steps steps [] = (steps, [])
    54       | do_steps (step :: steps) updates = do_step step (do_steps steps updates)
    55     and do_step step (steps, []) = (step :: steps, [])
    56       | do_step (step as Let _) (steps, updates) = (step :: steps, updates)
    57       | do_step (Prove (qs, xs, l, t, subproofs, by))
    58           (steps, updates as Prove (qs', xs', l', t', subproofs', by') :: updates') =
    59         let
    60           val (subproofs, updates) =
    61             if l = l' then do_subproofs subproofs' updates' else do_subproofs subproofs updates
    62         in
    63           if l = l' then (Prove (qs', xs', l', t', subproofs, by') :: steps, updates)
    64           else (Prove (qs, xs, l, t, subproofs, by) :: steps, updates)
    65         end
    66       | do_step _ _ = raise Fail "Sledgehammer_Isar_Compress: update_steps (invalid update)"
    67     and do_subproofs [] updates = ([], updates)
    68       | do_subproofs steps [] = (steps, [])
    69       | do_subproofs (proof :: subproofs) updates =
    70         do_proof proof (do_subproofs subproofs updates)
    71     and do_proof proof (proofs, []) = (proof :: proofs, [])
    72       | do_proof (Proof (fix, assms, steps)) (proofs, updates) =
    73         let val (steps, updates) = do_steps steps updates in
    74           (Proof (fix, assms, steps) :: proofs, updates)
    75         end
    76   in
    77     (case do_steps steps (rev updates) of
    78       (steps, []) => steps
    79     | _ => raise Fail "Sledgehammer_Isar_Compress: update_steps")
    80   end
    81 
    82 (* Tries merging the first step into the second step.
    83    FIXME: Arbitrarily picks the second step's method. *)
    84 fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), _)))
    85       (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), methss2))) =
    86     let
    87       val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
    88       val gfs = union (op =) gfs1 gfs2
    89     in
    90       SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), methss2)))
    91     end
    92   | try_merge _ _ = NONE
    93 
    94 val compress_degree = 2
    95 val merge_timeout_slack = 1.2
    96 
    97 (* Precondition: The proof must be labeled canonically
    98    (cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
    99 fun compress_isar_proof compress_isar
   100     ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) proof =
   101   if compress_isar <= 1.0 then
   102     proof
   103   else
   104     let
   105       val (compress_further, decrement_step_count) =
   106         let
   107           val number_of_steps = add_isar_steps (steps_of_proof proof) 0
   108           val target_number_of_steps = Real.round (Real.fromInt number_of_steps / compress_isar)
   109           val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps)
   110         in
   111           (fn () => !delta > 0, fn () => delta := !delta - 1)
   112         end
   113 
   114       val (get_successors, replace_successor) =
   115         let
   116           fun add_refs (Let _) = I
   117             | add_refs (Prove (_, _, v, _, _, ((lfs, _), _))) =
   118               fold (fn key => Canonical_Label_Tab.cons_list (key, v)) lfs
   119 
   120           val tab =
   121             Canonical_Label_Tab.empty
   122             |> fold_isar_steps add_refs (steps_of_proof proof)
   123             (* "rev" should have the same effect as "sort canonical_label_ord" *)
   124             |> Canonical_Label_Tab.map (K rev)
   125             |> Unsynchronized.ref
   126 
   127           fun get_successors l = Canonical_Label_Tab.lookup_list (!tab) l
   128           fun set_successors l refs = tab := Canonical_Label_Tab.update (l, refs) (!tab)
   129           fun replace_successor old new dest =
   130             get_successors dest
   131             |> Ord_List.remove canonical_label_ord old
   132             |> Ord_List.union canonical_label_ord new
   133             |> set_successors dest
   134         in
   135           (get_successors, replace_successor)
   136         end
   137 
   138       (* elimination of trivial, one-step subproofs *)
   139       fun elim_subproofs' time qs fix l t lfs gfs (methss as (meth :: _) :: _) subs nontriv_subs =
   140         if null subs orelse not (compress_further ()) then
   141           (set_preplay_outcome l meth (Played time);
   142            Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), methss)))
   143         else
   144           (case subs of
   145             (sub as Proof (_, assms, sub_steps)) :: subs =>
   146             (let
   147               (* trivial subproofs have exactly one "Prove" step *)
   148               val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), (meth' :: _) :: _))) =
   149                 try the_single sub_steps
   150 
   151               (* only touch proofs that can be preplayed sucessfully *)
   152               val Played time' = Lazy.force (preplay_outcome l' meth')
   153 
   154               (* merge steps *)
   155               val subs'' = subs @ nontriv_subs
   156               val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs')
   157               val gfs'' = union (op =) gfs' gfs
   158               val by = ((lfs'', gfs''), methss(*FIXME*))
   159               val step'' = Prove (qs, fix, l, t, subs'', by)
   160 
   161               (* check if the modified step can be preplayed fast enough *)
   162               val timeout = time_mult merge_timeout_slack (Time.+(time, time'))
   163               val Played time'' = preplay_quietly timeout step''
   164             in
   165               decrement_step_count (); (* l' successfully eliminated! *)
   166               map (replace_successor l' [l]) lfs';
   167               elim_subproofs' time'' qs fix l t lfs'' gfs'' methss subs nontriv_subs
   168             end
   169             handle Bind =>
   170             elim_subproofs' time qs fix l t lfs gfs methss subs (sub :: nontriv_subs))
   171           | _ => raise Fail "Sledgehammer_Isar_Compress: elim_subproofs'")
   172 
   173       fun elim_subproofs (step as Let _) = step
   174         | elim_subproofs (step as Prove (qs, fix, l, t, subproofs,
   175             ((lfs, gfs), methss as (meth :: _) :: _))) =
   176           if subproofs = [] then
   177             step
   178           else
   179             (case Lazy.force (preplay_outcome l meth) of
   180               Played time => elim_subproofs' time qs fix l t lfs gfs methss subproofs []
   181             | _ => step)
   182 
   183       (** top_level compression: eliminate steps by merging them into their successors **)
   184       fun compress_top_level steps =
   185         let
   186           (* (#successors, (size_of_term t, position)) *)
   187           fun cand_key (i, l, t_size) = (length (get_successors l), (t_size, i))
   188 
   189           val compression_ord =
   190             prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord)
   191             #> rev_order
   192 
   193           val cand_ord = pairself cand_key #> compression_ord
   194 
   195           fun pop_next_cand [] = (NONE, [])
   196             | pop_next_cand (cands as (cand :: cands')) =
   197               let
   198                 val best as (i, _, _) =
   199                   fold (fn x => fn y => if cand_ord (x, y) = GREATER then x else y) cands' cand
   200               in (SOME best, filter_out (fn (j, _, _) => j = i) cands) end
   201 
   202           val candidates =
   203             let
   204               fun add_cand (_, Let _) = I
   205                 | add_cand (i, Prove (_, _, l, t, _, _)) = cons (i, l, size_of_term t)
   206             in
   207               (steps
   208                |> split_last |> fst (* keep last step *)
   209                |> fold_index add_cand) []
   210             end
   211 
   212           fun try_eliminate (i, l, _) succ_lbls steps =
   213             let
   214               val ((cand as Prove (_, _, l, _, _, ((lfs, _), (meth :: _) :: _))) :: steps') =
   215                 drop i steps
   216 
   217               val succs = collect_successors steps' succ_lbls
   218               val succ_meths = map (hd o hd o snd o the o byline_of_isar_step) succs
   219 
   220               (* only touch steps that can be preplayed successfully *)
   221               val Played time = Lazy.force (preplay_outcome l meth)
   222 
   223               val succs' = map (try_merge cand #> the) succs
   224 
   225               val succ_times =
   226                 map2 ((fn Played t => t) o Lazy.force oo preplay_outcome) succ_lbls succ_meths
   227               val timeslice = time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
   228               val timeouts =
   229                 map (curry Time.+ timeslice #> time_mult merge_timeout_slack) succ_times
   230 
   231               (* FIXME: debugging *)
   232               val _ =
   233                 if the (label_of_isar_step cand) <> l then
   234                   raise Fail "Sledgehammer_Isar_Compress: try_eliminate"
   235                 else
   236                   ()
   237 
   238               (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
   239               val play_outcomes = map2 preplay_quietly timeouts succs'
   240 
   241               (* ensure none of the modified successors timed out *)
   242               val true = List.all (fn Played _ => true) play_outcomes
   243 
   244               val (steps1, _ :: steps2) = chop i steps
   245               (* replace successors with their modified versions *)
   246               val steps2 = update_steps steps2 succs'
   247             in
   248               decrement_step_count (); (* candidate successfully eliminated *)
   249               map3 set_preplay_outcome succ_lbls succ_meths play_outcomes;
   250               map (replace_successor l succ_lbls) lfs;
   251               (* removing the step would mess up the indices; replace with dummy step instead *)
   252               steps1 @ dummy_isar_step :: steps2
   253             end
   254             handle Bind => steps
   255                  | Match => steps
   256                  | Option.Option => steps
   257 
   258           fun compression_loop candidates steps =
   259             if not (compress_further ()) then
   260               steps
   261             else
   262               (case pop_next_cand candidates of
   263                 (NONE, _) => steps (* no more candidates for elimination *)
   264               | (SOME (cand as (_, l, _)), candidates) =>
   265                 let val successors = get_successors l in
   266                   if length successors > compress_degree then steps
   267                   else compression_loop candidates (try_eliminate cand successors steps)
   268                 end)
   269         in
   270           compression_loop candidates steps
   271           |> remove (op =) dummy_isar_step
   272         end
   273 
   274       (** recusion over the proof tree **)
   275       (*
   276          Proofs are compressed bottom-up, beginning with the innermost
   277          subproofs.
   278          On the innermost proof level, the proof steps have no subproofs.
   279          In the best case, these steps can be merged into just one step,
   280          resulting in a trivial subproof. Going one level up, trivial subproofs
   281          can be eliminated. In the best case, this once again leads to a proof
   282          whose proof steps do not have subproofs. Applying this approach
   283          recursively will result in a flat proof in the best cast.
   284       *)
   285       fun do_proof (proof as (Proof (fix, assms, steps))) =
   286         if compress_further () then Proof (fix, assms, do_steps steps) else proof
   287       and do_steps steps =
   288         (* bottom-up: compress innermost proofs first *)
   289         steps |> map (fn step => step |> compress_further () ? do_sub_levels)
   290               |> compress_further () ? compress_top_level
   291       and do_sub_levels (Let x) = Let x
   292         | do_sub_levels (Prove (qs, xs, l, t, subproofs, by)) =
   293           (* compress subproofs *)
   294           Prove (qs, xs, l, t, map do_proof subproofs, by)
   295           (* eliminate trivial subproofs *)
   296           |> compress_further () ? elim_subproofs
   297     in
   298       do_proof proof
   299     end
   300 
   301 end;