src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
author blanchet
Thu Feb 13 13:16:17 2014 +0100 (2014-02-13 ago)
changeset 55452 29ec8680e61f
parent 55324 e04b75bd18e0
child 57054 fed0329ea8e2
permissions -rw-r--r--
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
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@55266
    14
  val keep_fastest_method_of_isar_step : isar_preplay_data -> isar_step -> isar_step
blanchet@55452
    15
  val minimize_isar_step_dependencies : Proof.context -> bool ->
blanchet@55452
    16
    isar_preplay_data Unsynchronized.ref -> isar_step -> isar_step
blanchet@55213
    17
  val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof ->
blanchet@55213
    18
    isar_proof
blanchet@54504
    19
end;
smolkas@52611
    20
blanchet@55202
    21
structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE =
smolkas@52611
    22
struct
smolkas@52611
    23
blanchet@55287
    24
open Sledgehammer_Proof_Methods
blanchet@55202
    25
open Sledgehammer_Isar_Proof
blanchet@55202
    26
open Sledgehammer_Isar_Preplay
smolkas@52611
    27
blanchet@55299
    28
fun keep_fastest_method_of_isar_step preplay_data
blanchet@55299
    29
      (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) =
blanchet@55295
    30
    Prove (qs, xs, l, t, subproofs, facts,
blanchet@55299
    31
      meths |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) |> op @,
blanchet@55299
    32
      comment)
blanchet@55266
    33
  | keep_fastest_method_of_isar_step _ step = step
blanchet@55266
    34
blanchet@55324
    35
val slack = seconds 0.025
smolkas@52611
    36
blanchet@55452
    37
fun minimize_isar_step_dependencies ctxt debug preplay_data
blanchet@55299
    38
      (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) =
blanchet@55266
    39
    (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
blanchet@54828
    40
      Played time =>
blanchet@54712
    41
      let
blanchet@55299
    42
        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)
smolkas@52611
    43
blanchet@55314
    44
        fun minimize_facts _ min_facts [] time = (min_facts, time)
blanchet@55314
    45
          | minimize_facts mk_step min_facts (fact :: facts) time =
blanchet@55452
    46
            (case preplay_isar_step_for_method ctxt debug (Time.+ (time, slack)) meth
blanchet@55258
    47
                (mk_step (min_facts @ facts)) of
blanchet@55314
    48
              Played time' => minimize_facts mk_step min_facts facts time'
blanchet@55314
    49
            | _ => minimize_facts mk_step (fact :: min_facts) facts time)
smolkas@52611
    50
blanchet@55314
    51
        val (min_lfs, time') = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs0) [] lfs0 time
blanchet@55314
    52
        val (min_gfs, time'') = minimize_facts (mk_step_lfs_gfs min_lfs) [] gfs0 time'
blanchet@55264
    53
blanchet@55264
    54
        val step' = mk_step_lfs_gfs min_lfs min_gfs
blanchet@54712
    55
      in
blanchet@55452
    56
        set_preplay_outcomes_of_isar_step ctxt debug time'' preplay_data step'
blanchet@55452
    57
          [(meth, Played time'')];
blanchet@55264
    58
        step'
blanchet@54826
    59
      end
blanchet@54826
    60
    | _ => step (* don't touch steps that time out or fail *))
blanchet@55452
    61
  | minimize_isar_step_dependencies _ _ _ step = step
smolkas@52611
    62
blanchet@55213
    63
fun postprocess_isar_proof_remove_unreferenced_steps postproc_step =
smolkas@52611
    64
  let
blanchet@55259
    65
    fun process_proof (Proof (fix, assms, steps)) =
blanchet@55265
    66
      process_steps steps ||> (fn steps => Proof (fix, assms, steps))
blanchet@55259
    67
    and process_steps [] = ([], [])
blanchet@55259
    68
      | process_steps steps =
blanchet@55212
    69
        (* the last step is always implicitly referenced *)
blanchet@55265
    70
        let val (steps, (used, concl)) = split_last steps ||> process_used_step in
blanchet@55265
    71
          fold_rev process_step steps (used, [concl])
blanchet@54754
    72
        end
blanchet@55265
    73
    and process_step step (used, accu) =
blanchet@55223
    74
      (case label_of_isar_step step of
blanchet@55265
    75
        NONE => (used, step :: accu)
smolkas@52611
    76
      | SOME l =>
blanchet@55265
    77
        if Ord_List.member label_ord used l then
blanchet@55265
    78
          process_used_step step |>> Ord_List.union label_ord used ||> (fn step => step :: accu)
blanchet@54813
    79
        else
blanchet@55265
    80
          (used, accu))
blanchet@55265
    81
    and process_used_step step = step |> postproc_step |> process_used_step_subproofs
blanchet@55299
    82
    and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) =
blanchet@55259
    83
      let
blanchet@55265
    84
        val (used, subproofs) =
blanchet@55259
    85
          map process_proof subproofs
blanchet@55259
    86
          |> split_list
blanchet@55259
    87
          |>> Ord_List.unions label_ord
blanchet@55259
    88
          |>> fold (Ord_List.insert label_ord) lfs
blanchet@55259
    89
      in
blanchet@55299
    90
        (used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment))
blanchet@55259
    91
      end
smolkas@52611
    92
  in
blanchet@55259
    93
    snd o process_proof
smolkas@52611
    94
  end
smolkas@52611
    95
blanchet@54504
    96
end;