src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML
author smolkas
Fri Jul 12 14:18:06 2013 +0200 (2013-07-12 ago)
changeset 52611 831f7479c74f
parent 52592 8a25b17e3d79
child 52612 32e7f3b7c53a
permissions -rw-r--r--
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
smolkas@52592
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_try0.ML
smolkas@52592
     2
    Author:     Jasmin Blanchette, TU Muenchen
smolkas@52592
     3
    Author:     Steffen Juilf Smolka, TU Muenchen
smolkas@52592
     4
smolkas@52592
     5
Try replacing calls to metis with calls to other proof methods in order to
smolkas@52592
     6
speed up proofs, eliminate dependencies, and repair broken proof steps.
smolkas@52592
     7
*)
smolkas@52592
     8
smolkas@52592
     9
signature SLEDGEHAMMER_TRY0 =
smolkas@52592
    10
sig
smolkas@52592
    11
  type isar_proof = Sledgehammer_Proof.isar_proof
smolkas@52592
    12
  type preplay_interface = Sledgehammer_Preplay.preplay_interface
smolkas@52592
    13
smolkas@52592
    14
  val try0 : Time.time -> preplay_interface -> isar_proof -> isar_proof
smolkas@52592
    15
end
smolkas@52592
    16
smolkas@52592
    17
structure Sledgehammer_Try0 : SLEDGEHAMMER_TRY0 =
smolkas@52592
    18
struct
smolkas@52592
    19
smolkas@52592
    20
open Sledgehammer_Proof
smolkas@52592
    21
open Sledgehammer_Preplay
smolkas@52592
    22
smolkas@52592
    23
fun variants (step as Let _) = raise Fail "Sledgehammer_Try0: variants"
smolkas@52592
    24
  | variants (Prove (qs, xs, l, t, subproofs, By (facts, method))) =
smolkas@52592
    25
      let
smolkas@52592
    26
        val methods = [SimpM, AutoM, FastforceM, ArithM]
smolkas@52592
    27
        fun step method = Prove (qs, xs, l, t, subproofs, By (facts, method))
smolkas@52592
    28
        fun step_without_facts method =
smolkas@52592
    29
          Prove (qs, xs, l, t, subproofs, By (no_facts, method))
smolkas@52592
    30
      in
smolkas@52611
    31
        (* FIXME *)
smolkas@52592
    32
        (* There seems to be a bias for methods earlier in the list, so we put
smolkas@52592
    33
           the variants using no facts first. *)
smolkas@52611
    34
        (*map step_without_facts methods @*) map step methods
smolkas@52592
    35
      end
smolkas@52592
    36
smolkas@52592
    37
fun try0_step preplay_timeout preplay_interface (step as Let _) = step
smolkas@52592
    38
  | try0_step preplay_timeout ({preplay_quietly, get_time, set_time,
smolkas@52592
    39
    set_preplay_fail, ...} : preplay_interface)
smolkas@52592
    40
    (step as Prove (_, _, l, _, _, _)) =
smolkas@52592
    41
      let
smolkas@52592
    42
smolkas@52592
    43
        val (preplay_fail, timeout) =
smolkas@52592
    44
          case get_time l of
smolkas@52592
    45
            (true, _) => (true, preplay_timeout)
smolkas@52592
    46
          | (false, t) => (false, t)
smolkas@52592
    47
smolkas@52592
    48
        fun try_variant variant =
smolkas@52592
    49
           case preplay_quietly timeout variant of
smolkas@52592
    50
             (true, _) => NONE
smolkas@52592
    51
           | time as (false, _) => SOME (variant, time)
smolkas@52592
    52
smolkas@52592
    53
      in
smolkas@52592
    54
        case Par_List.get_some try_variant (variants step) of
smolkas@52592
    55
          SOME (step, time) => (set_time l time; step)
smolkas@52592
    56
        | NONE => (if preplay_fail then set_preplay_fail true else (); step)
smolkas@52592
    57
      end
smolkas@52592
    58
smolkas@52592
    59
fun try0 preplay_timeout
smolkas@52592
    60
  (preplay_interface as {set_preplay_fail, ...} : preplay_interface) proof =
smolkas@52611
    61
    (set_preplay_fail false; (* failure might be fixed *)
smolkas@52611
    62
     map_isar_steps (try0_step preplay_timeout preplay_interface) proof)
smolkas@52592
    63
smolkas@52592
    64
end