src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
author smolkas
Fri Jul 12 14:18:06 2013 +0200 (2013-07-12 ago)
changeset 52611 831f7479c74f
child 52626 79a4e7f8d758
permissions -rw-r--r--
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas@52611
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
smolkas@52611
     2
    Author:     Jasmin Blanchette, TU Muenchen
smolkas@52611
     3
    Author:     Steffen Juilf Smolka, TU Muenchen
smolkas@52611
     4
smolkas@52611
     5
Minimize dependencies (used facts) of Isar proof steps.
smolkas@52611
     6
*)
smolkas@52611
     7
smolkas@52611
     8
signature SLEDGEHAMMER_MINIMIZE_ISAR =
smolkas@52611
     9
sig
smolkas@52611
    10
  type preplay_interface = Sledgehammer_Preplay.preplay_interface
smolkas@52611
    11
  type isar_proof = Sledgehammer_Proof.isar_proof
smolkas@52611
    12
  val minimize_dependencies_and_remove_unrefed_steps :
smolkas@52611
    13
    preplay_interface -> isar_proof -> isar_proof
smolkas@52611
    14
end
smolkas@52611
    15
smolkas@52611
    16
smolkas@52611
    17
structure Sledgehammer_Minimize_Isar : SLEDGEHAMMER_MINIMIZE_ISAR =
smolkas@52611
    18
struct
smolkas@52611
    19
smolkas@52611
    20
open Sledgehammer_Util
smolkas@52611
    21
open Sledgehammer_Proof
smolkas@52611
    22
open Sledgehammer_Preplay
smolkas@52611
    23
smolkas@52611
    24
val slack = 1.3
smolkas@52611
    25
smolkas@52611
    26
fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
smolkas@52611
    27
  | min_deps_of_step {get_time, set_time, preplay_quietly, set_preplay_fail, ...}
smolkas@52611
    28
      (step as Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), method))) =
smolkas@52611
    29
  (case get_time l of
smolkas@52611
    30
    (* don't touch steps that time out *)
smolkas@52611
    31
    (true, _) => (set_preplay_fail true; step)
smolkas@52611
    32
  | (false, time) =>
smolkas@52611
    33
    let
smolkas@52611
    34
      fun mk_step_lfs_gfs lfs gfs =
smolkas@52611
    35
        Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), method))
smolkas@52611
    36
      val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
smolkas@52611
    37
smolkas@52611
    38
      fun minimize_facts _ time min_facts [] = (time, min_facts)
smolkas@52611
    39
        | minimize_facts mk_step time min_facts (f :: facts) =
smolkas@52611
    40
          (case preplay_quietly (time_mult slack time)
smolkas@52611
    41
                  (mk_step (min_facts @ facts)) of
smolkas@52611
    42
            (true, _) => minimize_facts mk_step time (f :: min_facts) facts
smolkas@52611
    43
          | (false, time) => minimize_facts mk_step time min_facts facts)
smolkas@52611
    44
smolkas@52611
    45
      val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
smolkas@52611
    46
      val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
smolkas@52611
    47
smolkas@52611
    48
    in
smolkas@52611
    49
      set_time l (false, time);
smolkas@52611
    50
      mk_step_lfs_gfs min_lfs min_gfs
smolkas@52611
    51
    end)
smolkas@52611
    52
smolkas@52611
    53
fun minimize_dependencies_and_remove_unrefed_steps (preplay_interface as
smolkas@52611
    54
  {set_time, set_preplay_fail, ...} : preplay_interface) proof =
smolkas@52611
    55
  let
smolkas@52611
    56
    fun cons_to xs x = x :: xs
smolkas@52611
    57
smolkas@52611
    58
    val add_lfs = fold (Ord_List.insert label_ord)
smolkas@52611
    59
smolkas@52611
    60
    fun do_proof (Proof (fix, assms, steps)) =
smolkas@52611
    61
      let
smolkas@52611
    62
        val (refed, steps) = do_steps steps
smolkas@52611
    63
      in
smolkas@52611
    64
        (refed, Proof (fix, assms, steps))
smolkas@52611
    65
      end
smolkas@52611
    66
smolkas@52611
    67
    and do_steps steps =
smolkas@52611
    68
      let
smolkas@52611
    69
        (* the last step is always implicitly referenced *)
smolkas@52611
    70
        val (steps, (refed, concl)) =
smolkas@52611
    71
          split_last steps
smolkas@52611
    72
          ||> do_refed_step
smolkas@52611
    73
      in
smolkas@52611
    74
        fold_rev do_step steps (refed, [concl])
smolkas@52611
    75
      end
smolkas@52611
    76
smolkas@52611
    77
    and do_step step (refed, accu) =
smolkas@52611
    78
      case label_of_step step of
smolkas@52611
    79
        NONE => (refed, step :: accu)
smolkas@52611
    80
      | SOME l =>
smolkas@52611
    81
          if Ord_List.member label_ord refed l then
smolkas@52611
    82
            do_refed_step step
smolkas@52611
    83
            |>> Ord_List.union label_ord refed
smolkas@52611
    84
            ||> cons_to accu
smolkas@52611
    85
          else
smolkas@52611
    86
            (set_time l zero_preplay_time; (* remove unrefed step! *)
smolkas@52611
    87
             (refed, accu))
smolkas@52611
    88
smolkas@52611
    89
    and do_refed_step step =
smolkas@52611
    90
      min_deps_of_step preplay_interface step
smolkas@52611
    91
      |> do_refed_step'
smolkas@52611
    92
smolkas@52611
    93
    and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar"
smolkas@52611
    94
      | do_refed_step' (Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), m))) =
smolkas@52611
    95
        let
smolkas@52611
    96
          val (refed, subproofs) =
smolkas@52611
    97
            map do_proof subproofs
smolkas@52611
    98
            |> split_list
smolkas@52611
    99
            |>> Ord_List.unions label_ord
smolkas@52611
   100
            |>> add_lfs lfs
smolkas@52611
   101
          val step = Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), m))
smolkas@52611
   102
        in
smolkas@52611
   103
          (refed, step)
smolkas@52611
   104
        end
smolkas@52611
   105
smolkas@52611
   106
  in
smolkas@52611
   107
    set_preplay_fail false; (* step(s) causing the failure may be removed *)
smolkas@52611
   108
    snd (do_proof proof)
smolkas@52611
   109
  end
smolkas@52611
   110
smolkas@52611
   111
smolkas@52611
   112
end