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