src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
author blanchet
Tue Nov 19 18:38:25 2013 +0100 (2013-11-19 ago)
changeset 54504 096f7d452164
parent 53764 eba0d1c069b8
child 54700 64177ce0a7bd
permissions -rw-r--r--
tuning
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@52632
    13
    bool -> preplay_interface -> isar_proof -> isar_proof
blanchet@54504
    14
end;
smolkas@52611
    15
smolkas@52611
    16
structure Sledgehammer_Minimize_Isar : SLEDGEHAMMER_MINIMIZE_ISAR =
smolkas@52611
    17
struct
smolkas@52611
    18
smolkas@52611
    19
open Sledgehammer_Util
smolkas@52611
    20
open Sledgehammer_Proof
smolkas@52611
    21
open Sledgehammer_Preplay
smolkas@52611
    22
smolkas@52611
    23
val slack = 1.3
smolkas@52611
    24
smolkas@52611
    25
fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
smolkas@52626
    26
  | min_deps_of_step {get_preplay_time, set_preplay_time, preplay_quietly, ...}
smolkas@52611
    27
      (step as Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), method))) =
smolkas@52626
    28
  (case get_preplay_time l of
smolkas@52626
    29
    (* don't touch steps that time out or fail; minimizing won't help *)
smolkas@52626
    30
    (true, _) => step
smolkas@52611
    31
  | (false, time) =>
smolkas@52611
    32
    let
smolkas@52611
    33
      fun mk_step_lfs_gfs lfs gfs =
smolkas@52611
    34
        Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), method))
smolkas@52611
    35
      val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
smolkas@52611
    36
smolkas@52611
    37
      fun minimize_facts _ time min_facts [] = (time, min_facts)
smolkas@52611
    38
        | minimize_facts mk_step time min_facts (f :: facts) =
smolkas@52611
    39
          (case preplay_quietly (time_mult slack time)
smolkas@52611
    40
                  (mk_step (min_facts @ facts)) of
smolkas@52611
    41
            (true, _) => minimize_facts mk_step time (f :: min_facts) facts
smolkas@52611
    42
          | (false, time) => minimize_facts mk_step time min_facts facts)
smolkas@52611
    43
smolkas@52611
    44
      val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
smolkas@52611
    45
      val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
smolkas@52611
    46
smolkas@52611
    47
    in
smolkas@52626
    48
      set_preplay_time l (false, time);
smolkas@52611
    49
      mk_step_lfs_gfs min_lfs min_gfs
smolkas@52611
    50
    end)
smolkas@52611
    51
blanchet@53764
    52
fun minimize_dependencies_and_remove_unrefed_steps isar_try0 preplay_interface
blanchet@53764
    53
        proof =
smolkas@52611
    54
  let
smolkas@52611
    55
    fun cons_to xs x = x :: xs
smolkas@52611
    56
smolkas@52611
    57
    val add_lfs = fold (Ord_List.insert label_ord)
smolkas@52611
    58
smolkas@52611
    59
    fun do_proof (Proof (fix, assms, steps)) =
smolkas@52611
    60
      let
smolkas@52611
    61
        val (refed, steps) = do_steps steps
smolkas@52611
    62
      in
smolkas@52611
    63
        (refed, Proof (fix, assms, steps))
smolkas@52611
    64
      end
smolkas@52611
    65
smolkas@52611
    66
    and do_steps steps =
smolkas@52611
    67
      let
smolkas@52611
    68
        (* the last step is always implicitly referenced *)
smolkas@52611
    69
        val (steps, (refed, concl)) =
smolkas@52611
    70
          split_last steps
smolkas@52611
    71
          ||> do_refed_step
smolkas@52611
    72
      in
smolkas@52611
    73
        fold_rev do_step steps (refed, [concl])
smolkas@52611
    74
      end
smolkas@52611
    75
smolkas@52611
    76
    and do_step step (refed, accu) =
smolkas@52611
    77
      case label_of_step step of
smolkas@52611
    78
        NONE => (refed, step :: accu)
smolkas@52611
    79
      | SOME l =>
smolkas@52611
    80
          if Ord_List.member label_ord refed l then
smolkas@52611
    81
            do_refed_step step
smolkas@52611
    82
            |>> Ord_List.union label_ord refed
smolkas@52611
    83
            ||> cons_to accu
smolkas@52611
    84
          else
smolkas@52626
    85
            (refed, accu)
smolkas@52611
    86
smolkas@52611
    87
    and do_refed_step step =
smolkas@52632
    88
      step
blanchet@53764
    89
      |> isar_try0 ? min_deps_of_step preplay_interface
smolkas@52611
    90
      |> do_refed_step'
smolkas@52611
    91
smolkas@52611
    92
    and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar"
smolkas@52611
    93
      | do_refed_step' (Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), m))) =
smolkas@52611
    94
        let
smolkas@52611
    95
          val (refed, subproofs) =
smolkas@52611
    96
            map do_proof subproofs
smolkas@52611
    97
            |> split_list
smolkas@52611
    98
            |>> Ord_List.unions label_ord
smolkas@52611
    99
            |>> add_lfs lfs
smolkas@52611
   100
          val step = Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), m))
smolkas@52611
   101
        in
smolkas@52611
   102
          (refed, step)
smolkas@52611
   103
        end
smolkas@52611
   104
  in
smolkas@52611
   105
    snd (do_proof proof)
smolkas@52611
   106
  end
smolkas@52611
   107
blanchet@54504
   108
end;