src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML
author blanchet
Mon Dec 09 06:33:46 2013 +0100 (2013-12-09 ago)
changeset 54700 64177ce0a7bd
parent 54504 096f7d452164
child 54712 cbebe2cf77f1
permissions -rw-r--r--
adapted code for Z3 proof reconstruction
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
blanchet@54504
    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@52612
    23
fun variants (Let _) = raise Fail "Sledgehammer_Try0: variants"
blanchet@54700
    24
  | variants (Prove (qs, xs, l, t, subproofs, (facts, _))) =
smolkas@52592
    25
      let
smolkas@52629
    26
        val methods = [SimpM, FastforceM, AutoM, ArithM, ForceM, BlastM]
blanchet@54700
    27
        fun step method = Prove (qs, xs, l, t, subproofs, (facts, method))
smolkas@52612
    28
        (*fun step_without_facts method =
blanchet@54700
    29
          Prove (qs, xs, l, t, subproofs, (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@52612
    37
fun try0_step _ _ (step as Let _) = step
smolkas@52626
    38
  | try0_step preplay_timeout ({preplay_quietly, get_preplay_time,
smolkas@52626
    39
    set_preplay_time, ...} : preplay_interface)
smolkas@52592
    40
    (step as Prove (_, _, l, _, _, _)) =
smolkas@52592
    41
      let
smolkas@52592
    42
smolkas@52626
    43
        val timeout =
smolkas@52626
    44
          case get_preplay_time l of
smolkas@52626
    45
            (true, _) => preplay_timeout
smolkas@52626
    46
          | (false, t) => 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@52626
    55
          SOME (step, time) => (set_preplay_time l time; step)
smolkas@52626
    56
        | NONE => step
smolkas@52592
    57
      end
smolkas@52592
    58
smolkas@52626
    59
fun try0 preplay_timeout preplay_interface proof =
smolkas@52626
    60
     map_isar_steps (try0_step preplay_timeout preplay_interface) proof
smolkas@52592
    61
blanchet@54504
    62
end;