src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
author blanchet
Sun Feb 02 20:53:51 2014 +0100 (2014-02-02 ago)
changeset 55258 8cc42c1f9bb5
parent 55255 eceebcea3e00
child 55259 7f2930d9bb2c
permissions -rw-r--r--
more data structure rationalization
blanchet@55202
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.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
blanchet@55202
     8
signature SLEDGEHAMMER_ISAR_MINIMIZE =
smolkas@52611
     9
sig
blanchet@55202
    10
  type isar_step = Sledgehammer_Isar_Proof.isar_step
blanchet@55202
    11
  type isar_proof = Sledgehammer_Isar_Proof.isar_proof
blanchet@55213
    12
  type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
blanchet@54712
    13
blanchet@55258
    14
  val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data -> isar_step -> isar_step
blanchet@55213
    15
  val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof ->
blanchet@55213
    16
    isar_proof
blanchet@54504
    17
end;
smolkas@52611
    18
blanchet@55202
    19
structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE =
smolkas@52611
    20
struct
smolkas@52611
    21
blanchet@54828
    22
open Sledgehammer_Reconstructor
blanchet@55202
    23
open Sledgehammer_Isar_Proof
blanchet@55202
    24
open Sledgehammer_Isar_Preplay
smolkas@52611
    25
blanchet@54712
    26
val slack = seconds 0.1
smolkas@52611
    27
blanchet@55258
    28
fun minimize_isar_step_dependencies _ (_ : isar_preplay_data) (step as Let _) = step
blanchet@55258
    29
  | minimize_isar_step_dependencies ctxt {set_preplay_outcomes, preplay_outcome, ...}
blanchet@55244
    30
      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) =
blanchet@55223
    31
    (case Lazy.force (preplay_outcome l meth) of
blanchet@54828
    32
      Played time =>
blanchet@54712
    33
      let
blanchet@55244
    34
        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))
blanchet@54712
    35
        val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
smolkas@52611
    36
blanchet@54712
    37
        fun minimize_facts _ time min_facts [] = (time, min_facts)
blanchet@54712
    38
          | minimize_facts mk_step time min_facts (f :: facts) =
blanchet@55258
    39
            (case preplay_isar_step ctxt (Time.+ (time, slack)) meth
blanchet@55258
    40
                (mk_step (min_facts @ facts)) of
blanchet@54828
    41
              Played time => minimize_facts mk_step time min_facts facts
blanchet@54827
    42
            | _ => minimize_facts mk_step time (f :: 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@55252
    47
        set_preplay_outcomes l [(meth, Lazy.value (Played time))];
blanchet@55252
    48
        mk_step_lfs_gfs min_lfs min_gfs
blanchet@54826
    49
      end
blanchet@54826
    50
    | _ => step (* don't touch steps that time out or fail *))
smolkas@52611
    51
blanchet@55213
    52
fun postprocess_isar_proof_remove_unreferenced_steps postproc_step =
smolkas@52611
    53
  let
smolkas@52611
    54
    val add_lfs = fold (Ord_List.insert label_ord)
smolkas@52611
    55
smolkas@52611
    56
    fun do_proof (Proof (fix, assms, steps)) =
blanchet@54712
    57
      let val (refed, steps) = do_steps steps in
smolkas@52611
    58
        (refed, Proof (fix, assms, steps))
smolkas@52611
    59
      end
blanchet@54754
    60
    and do_steps [] = ([], [])
blanchet@54754
    61
      | do_steps steps =
blanchet@55212
    62
        (* the last step is always implicitly referenced *)
blanchet@55212
    63
        let val (steps, (refed, concl)) = split_last steps ||> do_refed_step in
blanchet@54754
    64
          fold_rev do_step steps (refed, [concl])
blanchet@54754
    65
        end
smolkas@52611
    66
    and do_step step (refed, accu) =
blanchet@55223
    67
      (case label_of_isar_step step of
smolkas@52611
    68
        NONE => (refed, step :: accu)
smolkas@52611
    69
      | SOME l =>
blanchet@54813
    70
        if Ord_List.member label_ord refed l then
blanchet@54813
    71
          do_refed_step step
blanchet@54813
    72
          |>> Ord_List.union label_ord refed
blanchet@54813
    73
          ||> (fn x => x :: accu)
blanchet@54813
    74
        else
blanchet@54813
    75
          (refed, accu))
blanchet@54712
    76
    and do_refed_step step = step |> postproc_step |> do_refed_step'
blanchet@55202
    77
    and do_refed_step' (Let _) = raise Fail "Sledgehammer_Isar_Minimize"
blanchet@54700
    78
      | do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) =
smolkas@52611
    79
        let
smolkas@52611
    80
          val (refed, subproofs) =
smolkas@52611
    81
            map do_proof subproofs
smolkas@52611
    82
            |> split_list
smolkas@52611
    83
            |>> Ord_List.unions label_ord
smolkas@52611
    84
            |>> add_lfs lfs
blanchet@54700
    85
          val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))
smolkas@52611
    86
        in
smolkas@52611
    87
          (refed, step)
smolkas@52611
    88
        end
smolkas@52611
    89
  in
blanchet@54712
    90
    snd o do_proof
smolkas@52611
    91
  end
smolkas@52611
    92
blanchet@54504
    93
end;