src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
author blanchet
Sun Dec 15 18:01:38 2013 +0100 (2013-12-15 ago)
changeset 54754 6b0ca7f79e93
parent 54712 cbebe2cf77f1
child 54813 c8b04da1bd01
permissions -rw-r--r--
robustness in degenerate case + tuning
smolkas@52611
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
blanchet@54712
     2
    Author:     Steffen Juilf Smolka, TU Muenchen
smolkas@52611
     3
    Author:     Jasmin Blanchette, 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
blanchet@54712
    11
  type isar_step = Sledgehammer_Proof.isar_step
smolkas@52611
    12
  type isar_proof = Sledgehammer_Proof.isar_proof
blanchet@54712
    13
blanchet@54712
    14
  val min_deps_of_step : preplay_interface -> isar_step -> isar_step
blanchet@54712
    15
  val postprocess_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
blanchet@54504
    16
end;
smolkas@52611
    17
smolkas@52611
    18
structure Sledgehammer_Minimize_Isar : SLEDGEHAMMER_MINIMIZE_ISAR =
smolkas@52611
    19
struct
smolkas@52611
    20
smolkas@52611
    21
open Sledgehammer_Util
smolkas@52611
    22
open Sledgehammer_Proof
smolkas@52611
    23
open Sledgehammer_Preplay
smolkas@52611
    24
blanchet@54712
    25
val slack = seconds 0.1
smolkas@52611
    26
smolkas@52611
    27
fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
smolkas@52626
    28
  | min_deps_of_step {get_preplay_time, set_preplay_time, preplay_quietly, ...}
blanchet@54712
    29
      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
blanchet@54712
    30
    (case get_preplay_time l of
blanchet@54712
    31
      (* don't touch steps that time out or fail; minimizing won't help (not true -- FIXME) *)
blanchet@54712
    32
      (true, _) => step
blanchet@54712
    33
    | (false, time) =>
blanchet@54712
    34
      let
blanchet@54712
    35
        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
blanchet@54712
    36
        val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
smolkas@52611
    37
blanchet@54712
    38
        fun minimize_facts _ time min_facts [] = (time, min_facts)
blanchet@54712
    39
          | minimize_facts mk_step time min_facts (f :: facts) =
blanchet@54712
    40
            (case preplay_quietly (Time.+ (time, slack)) (mk_step (min_facts @ facts)) of
blanchet@54712
    41
              (true, _) => minimize_facts mk_step time (f :: min_facts) facts
blanchet@54712
    42
            | (false, time) => minimize_facts mk_step time min_facts facts)
smolkas@52611
    43
blanchet@54712
    44
        val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
blanchet@54712
    45
        val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
blanchet@54712
    46
      in
blanchet@54712
    47
        set_preplay_time l (false, time); mk_step_lfs_gfs min_lfs min_gfs
blanchet@54712
    48
      end)
smolkas@52611
    49
blanchet@54712
    50
fun postprocess_remove_unreferenced_steps postproc_step =
smolkas@52611
    51
  let
smolkas@52611
    52
    val add_lfs = fold (Ord_List.insert label_ord)
smolkas@52611
    53
smolkas@52611
    54
    fun do_proof (Proof (fix, assms, steps)) =
blanchet@54712
    55
      let val (refed, steps) = do_steps steps in
smolkas@52611
    56
        (refed, Proof (fix, assms, steps))
smolkas@52611
    57
      end
blanchet@54754
    58
    and do_steps [] = ([], [])
blanchet@54754
    59
      | do_steps steps =
blanchet@54754
    60
        let
blanchet@54754
    61
          (* the last step is always implicitly referenced *)
blanchet@54754
    62
          val (steps, (refed, concl)) =
blanchet@54754
    63
            split_last steps
blanchet@54754
    64
            ||> do_refed_step
blanchet@54754
    65
        in
blanchet@54754
    66
          fold_rev do_step steps (refed, [concl])
blanchet@54754
    67
        end
smolkas@52611
    68
    and do_step step (refed, accu) =
blanchet@54754
    69
      (case label_of_step step of
smolkas@52611
    70
        NONE => (refed, step :: accu)
smolkas@52611
    71
      | SOME l =>
smolkas@52611
    72
          if Ord_List.member label_ord refed l then
smolkas@52611
    73
            do_refed_step step
smolkas@52611
    74
            |>> Ord_List.union label_ord refed
blanchet@54712
    75
            ||> (fn x => x :: accu)
smolkas@52611
    76
          else
blanchet@54754
    77
            (refed, accu))
blanchet@54712
    78
    and do_refed_step step = step |> postproc_step |> do_refed_step'
smolkas@52611
    79
    and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar"
blanchet@54700
    80
      | do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) =
smolkas@52611
    81
        let
smolkas@52611
    82
          val (refed, subproofs) =
smolkas@52611
    83
            map do_proof subproofs
smolkas@52611
    84
            |> split_list
smolkas@52611
    85
            |>> Ord_List.unions label_ord
smolkas@52611
    86
            |>> add_lfs lfs
blanchet@54700
    87
          val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))
smolkas@52611
    88
        in
smolkas@52611
    89
          (refed, step)
smolkas@52611
    90
        end
smolkas@52611
    91
  in
blanchet@54712
    92
    snd o do_proof
smolkas@52611
    93
  end
smolkas@52611
    94
blanchet@54504
    95
end;