src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML
author blanchet
Sun Feb 02 20:53:51 2014 +0100 (2014-02-02)
changeset 55243 66709d41601e
parent 55223 3c593bad6b31
child 55244 12e1a5d8ee48
permissions -rw-r--r--
reset timing information after changes
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML
     2     Author:     Steffen Juilf Smolka, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Try replacing calls to "metis" with calls to other proof methods to speed up proofs, eliminate
     6 dependencies, and repair broken proof steps.
     7 *)
     8 
     9 signature SLEDGEHAMMER_ISAR_TRY0 =
    10 sig
    11   type isar_proof = Sledgehammer_Isar_Proof.isar_proof
    12   type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
    13 
    14   val try0_isar_proof : Time.time -> isar_preplay_data -> isar_proof -> isar_proof
    15 end;
    16 
    17 structure Sledgehammer_Isar_Try0 : SLEDGEHAMMER_ISAR_TRY0 =
    18 struct
    19 
    20 open Sledgehammer_Util
    21 open Sledgehammer_Reconstructor
    22 open Sledgehammer_Isar_Proof
    23 open Sledgehammer_Isar_Preplay
    24 
    25 fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, methss))) =
    26     map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [[meth]]))) (tl (flat methss))
    27   | variants_of_step _ = raise Fail "Sledgehammer_Isar_Try0: variants_of_step"
    28 
    29 val slack = seconds 0.05
    30 
    31 fun try0_step _ _ (step as Let _) = step
    32   | try0_step preplay_timeout
    33       ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
    34       (step as Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
    35     let
    36       val timeout =
    37         (case Lazy.force (preplay_outcome l meth) of
    38           Played time => Time.+ (time, slack)
    39         | _ => preplay_timeout)
    40 
    41       fun try_variant variant =
    42         (case preplay_quietly timeout variant of
    43           result as Played _ => SOME (variant, result)
    44         | _ => NONE)
    45     in
    46       (* FIXME: create variant after success *)
    47       (case Par_List.get_some try_variant (variants_of_step step) of
    48         SOME (step' as Prove (_, _, _, _, _, (_, (meth' :: _) :: _)), result) =>
    49         (set_preplay_outcome l meth' result; step')
    50       | NONE => step)
    51     end
    52 
    53 val try0_isar_proof = map_isar_steps oo try0_step
    54 
    55 end;