src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
author blanchet
Mon Feb 03 10:14:18 2014 +0100 (2014-02-03 ago)
changeset 55264 43473497fb65
parent 55263 4d63fffcde8d
child 55265 bd9f033b9896
permissions -rw-r--r--
centralize preplaying
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@55260
    14
  val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref ->
blanchet@55260
    15
    isar_step -> isar_step
blanchet@55213
    16
  val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof ->
blanchet@55213
    17
    isar_proof
blanchet@54504
    18
end;
smolkas@52611
    19
blanchet@55202
    20
structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE =
smolkas@52611
    21
struct
smolkas@52611
    22
blanchet@54828
    23
open Sledgehammer_Reconstructor
blanchet@55202
    24
open Sledgehammer_Isar_Proof
blanchet@55202
    25
open Sledgehammer_Isar_Preplay
smolkas@52611
    26
blanchet@54712
    27
val slack = seconds 0.1
smolkas@52611
    28
blanchet@55260
    29
fun minimize_isar_step_dependencies _ _ (step as Let _) = step
blanchet@55260
    30
  | minimize_isar_step_dependencies ctxt preplay_data
blanchet@55244
    31
      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) =
blanchet@55260
    32
    (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of
blanchet@54828
    33
      Played time =>
blanchet@54712
    34
      let
blanchet@55244
    35
        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))
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@55263
    44
        val (time, min_lfs) = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs) time [] lfs
blanchet@54712
    45
        val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
blanchet@55264
    46
blanchet@55264
    47
        val step' = mk_step_lfs_gfs min_lfs min_gfs
blanchet@54712
    48
      in
blanchet@55264
    49
        set_preplay_outcomes_of_isar_step ctxt time preplay_data step'
blanchet@55264
    50
          [(meth, Lazy.value (Played time))];
blanchet@55264
    51
        step'
blanchet@54826
    52
      end
blanchet@54826
    53
    | _ => step (* don't touch steps that time out or fail *))
smolkas@52611
    54
blanchet@55213
    55
fun postprocess_isar_proof_remove_unreferenced_steps postproc_step =
smolkas@52611
    56
  let
blanchet@55259
    57
    fun process_proof (Proof (fix, assms, steps)) =
blanchet@55259
    58
      let val (refed, steps) = process_steps steps in
smolkas@52611
    59
        (refed, Proof (fix, assms, steps))
smolkas@52611
    60
      end
blanchet@55259
    61
    and process_steps [] = ([], [])
blanchet@55259
    62
      | process_steps steps =
blanchet@55212
    63
        (* the last step is always implicitly referenced *)
blanchet@55259
    64
        let val (steps, (refed, concl)) = split_last steps ||> process_referenced_step in
blanchet@55259
    65
          fold_rev process_step steps (refed, [concl])
blanchet@54754
    66
        end
blanchet@55259
    67
    and process_step step (refed, accu) =
blanchet@55223
    68
      (case label_of_isar_step step of
smolkas@52611
    69
        NONE => (refed, step :: accu)
smolkas@52611
    70
      | SOME l =>
blanchet@54813
    71
        if Ord_List.member label_ord refed l then
blanchet@55259
    72
          process_referenced_step step
blanchet@54813
    73
          |>> Ord_List.union label_ord refed
blanchet@54813
    74
          ||> (fn x => x :: accu)
blanchet@54813
    75
        else
blanchet@54813
    76
          (refed, accu))
blanchet@55259
    77
    and process_referenced_step step = step |> postproc_step |> process_referenced_step_subproofs
blanchet@55259
    78
    and process_referenced_step_subproofs (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) =
blanchet@55259
    79
      let
blanchet@55259
    80
        val (refed, subproofs) =
blanchet@55259
    81
          map process_proof subproofs
blanchet@55259
    82
          |> split_list
blanchet@55259
    83
          |>> Ord_List.unions label_ord
blanchet@55259
    84
          |>> fold (Ord_List.insert label_ord) lfs
blanchet@55259
    85
        val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))
blanchet@55259
    86
      in
blanchet@55259
    87
        (refed, step)
blanchet@55259
    88
      end
smolkas@52611
    89
  in
blanchet@55259
    90
    snd o process_proof
smolkas@52611
    91
  end
smolkas@52611
    92
blanchet@54504
    93
end;