src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML

+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
+    Author:     Steffen Juilf Smolka, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Compression of Isar proofs by merging steps.
+Only proof steps using the same proof method are merged.
+*)
+
+signature SLEDGEHAMMER_ISAR_COMPRESS =
+sig
+  type isar_proof = Sledgehammer_Isar_Proof.isar_proof
+  type preplay_interface = Sledgehammer_Isar_Preplay.preplay_interface
+
+  val compress_proof : real -> preplay_interface -> isar_proof -> isar_proof
+end;
+
+structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS =
+struct
+
+open Sledgehammer_Util
+open Sledgehammer_Reconstructor
+open Sledgehammer_Isar_Proof
+open Sledgehammer_Isar_Preplay
+
+(* traverses steps in post-order and collects the steps with the given labels *)
+fun collect_successors steps lbls =
+  let
+    fun do_steps _ ([], accu) = ([], accu)
+      | do_steps [] accum = accum
+      | do_steps (step :: steps) accum = do_steps steps (do_step step accum)
+    and do_step (Let _) x = x
+      | do_step (step as Prove (_, _, l, _, subproofs, _)) x =
+        (case do_subproofs subproofs x of
+          ([], accu) => ([], accu)
+        | accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum)
+    and do_subproofs [] x = x
+      | do_subproofs (proof :: subproofs) x =
+        (case do_steps (steps_of_proof proof) x of
+          accum as ([], _) => accum
+        | accum => do_subproofs subproofs accum)
+  in
+    (case do_steps steps (lbls, []) of
+      ([], succs) => rev succs
+    | _ => raise Fail "Sledgehammer_Isar_Compress: collect_successors")
+  end
+
+(* traverses steps in reverse post-order and inserts the given updates *)
+fun update_steps steps updates =
+  let
+    fun do_steps [] updates = ([], updates)
+      | do_steps steps [] = (steps, [])
+      | do_steps (step :: steps) updates = do_step step (do_steps steps updates)
+    and do_step step (steps, []) = (step :: steps, [])
+      | do_step (step as Let _) (steps, updates) = (step :: steps, updates)
+      | do_step (Prove (qs, xs, l, t, subproofs, by))
+          (steps, updates as Prove (qs', xs', l', t', subproofs', by') :: updates') =
+        let
+          val (subproofs, updates) =
+            if l = l' then do_subproofs subproofs' updates' else do_subproofs subproofs updates
+        in
+          if l = l' then (Prove (qs', xs', l', t', subproofs, by') :: steps, updates)
+          else (Prove (qs, xs, l, t, subproofs, by) :: steps, updates)
+        end
+      | do_step _ _ = raise Fail "Sledgehammer_Isar_Compress: update_steps (invalid update)"
+    and do_subproofs [] updates = ([], updates)
+      | do_subproofs steps [] = (steps, [])
+      | do_subproofs (proof :: subproofs) updates =
+        do_proof proof (do_subproofs subproofs updates)
+    and do_proof proof (proofs, []) = (proof :: proofs, [])
+      | do_proof (Proof (fix, assms, steps)) (proofs, updates) =
+        let val (steps, updates) = do_steps steps updates in
+          (Proof (fix, assms, steps) :: proofs, updates)
+        end
+  in
+    (case do_steps steps (rev updates) of
+      (steps, []) => steps
+    | _ => raise Fail "Sledgehammer_Isar_Compress: update_steps")
+  end
+
+(* Tries merging the first step into the second step. Arbitrarily picks the second step's method. *)
+fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), _)))
+      (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meth2))) =
+    let
+      val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
+      val gfs = union (op =) gfs1 gfs2
+    in
+      SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meth2)))
+    end
+  | try_merge _ _ = NONE
+
+val compress_degree = 2
+val merge_timeout_slack = 1.2
+
+(* Precondition: The proof must be labeled canonically
+   (cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
+fun compress_proof compress_isar
+    ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_interface) proof =
+  if compress_isar <= 1.0 then
+    proof
+  else
+    let
+      val (compress_further, decrement_step_count) =
+        let
+          val number_of_steps = add_proof_steps (steps_of_proof proof) 0
+          val target_number_of_steps = Real.round (Real.fromInt number_of_steps / compress_isar)
+          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 (Let _) = I
+            | add_refs (Prove (_, _, v, _, _, ((lfs, _), _))) =
+              fold (fn key => Canonical_Lbl_Tab.cons_list (key, v)) lfs
+
+          val tab =
+            Canonical_Lbl_Tab.empty
+            |> fold_isar_steps add_refs (steps_of_proof proof)
+            (* "rev" should have the same effect as "sort canonical_label_ord" *)
+            |> Canonical_Lbl_Tab.map (K rev)
+            |> Unsynchronized.ref
+
+          fun get_successors l = Canonical_Lbl_Tab.lookup_list (!tab) l
+          fun set_successors l refs = tab := Canonical_Lbl_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
+
+      (** elimination of trivial, one-step subproofs **)
+
+      fun elim_subproofs' time qs fix l t lfs gfs meth subs nontriv_subs =
+        if null subs orelse not (compress_further ()) then
+          (set_preplay_outcome l (Played time);
+           Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meth)))
+        else
+          (case subs of
+            (sub as Proof (_, assms, sub_steps)) :: subs =>
+            (let
+              (* trivial subproofs have exactly one Prove step *)
+              val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
+
+              (* only touch proofs that can be preplayed sucessfully *)
+              val Played time' = get_preplay_outcome l'
+
+              (* merge steps *)
+              val subs'' = subs @ nontriv_subs
+              val lfs'' =
+                subtract (op =) (map fst assms) lfs'
+                |> union (op =) lfs
+              val gfs'' = union (op =) gfs' gfs
+              val by = ((lfs'', gfs''), meth)
+              val step'' = Prove (qs, fix, l, t, subs'', by)
+
+              (* check if the modified step can be preplayed fast enough *)
+              val timeout = time_mult merge_timeout_slack (Time.+(time, time'))
+              val Played time'' = preplay_quietly timeout step''
+
+            in
+              decrement_step_count (); (* l' successfully eliminated! *)
+              map (replace_successor l' [l]) lfs';
+              elim_subproofs' time'' qs fix l t lfs'' gfs'' meth subs nontriv_subs
+            end
+            handle Bind =>
+              elim_subproofs' time qs fix l t lfs gfs meth subs (sub :: nontriv_subs))
+          | _ => raise Fail "Sledgehammer_Isar_Compress: elim_subproofs'")
+
+      fun elim_subproofs (step as Let _) = step
+        | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meth))) =
+          if subproofs = [] then
+            step
+          else
+            (case get_preplay_outcome l of
+              Played time => elim_subproofs' time qs fix l t lfs gfs meth subproofs []
+            | _ => step)
+
+      (** top_level compression: eliminate steps by merging them into their
+          successors **)
+
+      fun compress_top_level steps =
+        let
+          (* (#successors, (size_of_term t, position)) *)
+          fun cand_key (i, l, t_size) = (get_successors l |> length, (t_size, i))
+
+          val compression_ord =
+            prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord)
+            #> rev_order
+
+          val cand_ord = pairself cand_key #> compression_ord
+
+          fun pop_next_cand candidates =
+            (case max_list cand_ord candidates of
+              NONE => (NONE, [])
+            | cand as SOME (i, _, _) => (cand, filter_out (fn (j, _, _) => j = i) candidates))
+
+          val candidates =
+            let
+              fun add_cand (_, Let _) = I
+                | add_cand (i, Prove (_, _, l, t, _, _)) = cons (i, l, size_of_term t)
+            in
+              (steps
+              |> split_last |> fst (* keep last step *)
+              |> fold_index add_cand) []
+            end
+
+          fun try_eliminate (i, l, _) succ_lbls steps =
+            let
+              (* only touch steps that can be preplayed successfully *)
+              val Played time = get_preplay_outcome l
+
+              val succ_times =
+                map (get_preplay_outcome #> (fn Played t => t)) succ_lbls
+              val timeslice = time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
+              val timeouts =
+                map (curry Time.+ timeslice #> time_mult merge_timeout_slack) succ_times
+
+              val ((cand as Prove (_, _, l, _, _, ((lfs, _), _))) :: steps') = drop i steps
+
+              (* FIXME: debugging *)
+              val _ =
+                if the (label_of_step cand) <> l then
+                  raise Fail "Sledgehammer_Isar_Compress: try_eliminate"
+                else
+                  ()
+
+              val succs = collect_successors steps' succ_lbls
+              val succs' = map (try_merge cand #> the) succs
+
+              (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
+              val play_outcomes = map2 preplay_quietly timeouts succs'
+
+              (* ensure none of the modified successors timed out *)
+              val true = List.all (fn Played _ => true) play_outcomes
+
+              val (steps1, _ :: steps2) = chop i steps
+              (* replace successors with their modified versions *)
+              val steps2 = update_steps steps2 succs'
+            in
+              decrement_step_count (); (* candidate successfully eliminated *)
+              map2 set_preplay_outcome succ_lbls play_outcomes;
+              map (replace_successor l succ_lbls) lfs;
+              (* removing the step would mess up the indices -> replace with dummy step instead *)
+              steps1 @ dummy_isar_step :: steps2
+            end
+            handle Bind => steps
+                 | Match => steps
+                 | Option.Option => steps
+
+          fun compression_loop candidates steps =
+            if not (compress_further ()) then
+              steps
+            else
+              (case pop_next_cand candidates of
+                (NONE, _) => steps (* no more candidates for elimination *)
+              | (SOME (cand as (_, l, _)), candidates) =>
+                let val successors = get_successors l in
+                  if length successors > compress_degree then steps
+                  else compression_loop candidates (try_eliminate cand successors steps)
+                end)
+        in
+          compression_loop candidates steps
+          |> remove (op =) dummy_isar_step
+        end
+
+      (** recusion over the proof tree **)
+      (*
+         Proofs are compressed bottom-up, beginning with the innermost
+         subproofs.
+         On the innermost proof level, the proof steps have no subproofs.
+         In the best case, these steps can be merged into just one step,
+         resulting in a trivial subproof. Going one level up, trivial subproofs
+         can be eliminated. In the best case, this once again leads to a proof
+         whose proof steps do not have subproofs. Applying this approach
+         recursively will result in a flat proof in the best cast.
+      *)
+      fun do_proof (proof as (Proof (fix, assms, steps))) =
+        if compress_further () then Proof (fix, assms, do_steps steps) else proof
+      and do_steps steps =
+        (* bottom-up: compress innermost proofs first *)
+        steps |> map (fn step => step |> compress_further () ? do_sub_levels)
+              |> compress_further () ? compress_top_level
+      and do_sub_levels (Let x) = Let x
+        | do_sub_levels (Prove (qs, xs, l, t, subproofs, by)) =
+          (* compress subproofs *)
+          Prove (qs, xs, l, t, map do_proof subproofs, by)
+          (* eliminate trivial subproofs *)
+          |> compress_further () ? elim_subproofs
+    in
+      do_proof proof
+    end
+
+end;