src/HOL/Tools/Sledgehammer/sledgehammer_try0.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_try0.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Author:     Steffen Juilf Smolka, TU Muenchen
     4 
     5 Try replacing calls to metis with calls to other proof methods in order to
     6 speed up proofs, eliminate dependencies, and repair broken proof steps.
     7 *)
     8 
     9 signature SLEDGEHAMMER_TRY0 =
    10 sig
    11   type isar_proof = Sledgehammer_Proof.isar_proof
    12   type preplay_interface = Sledgehammer_Preplay.preplay_interface
    13 
    14   val try0 : Time.time -> preplay_interface -> isar_proof -> isar_proof
    15 end;
    16 
    17 structure Sledgehammer_Try0 : SLEDGEHAMMER_TRY0 =
    18 struct
    19 
    20 open Sledgehammer_Proof
    21 open Sledgehammer_Preplay
    22 
    23 fun variants (Let _) = raise Fail "Sledgehammer_Try0: variants"
    24   | variants (Prove (qs, xs, l, t, subproofs, By (facts, _))) =
    25       let
    26         val methods = [SimpM, FastforceM, AutoM, ArithM, ForceM, BlastM]
    27         fun step method = Prove (qs, xs, l, t, subproofs, By (facts, method))
    28         (*fun step_without_facts method =
    29           Prove (qs, xs, l, t, subproofs, By (no_facts, method))*)
    30       in
    31         (* FIXME *)
    32         (* There seems to be a bias for methods earlier in the list, so we put
    33            the variants using no facts first. *)
    34         (*map step_without_facts methods @*) map step methods
    35       end
    36 
    37 fun try0_step _ _ (step as Let _) = step
    38   | try0_step preplay_timeout ({preplay_quietly, get_preplay_time,
    39     set_preplay_time, ...} : preplay_interface)
    40     (step as Prove (_, _, l, _, _, _)) =
    41       let
    42 
    43         val timeout =
    44           case get_preplay_time l of
    45             (true, _) => preplay_timeout
    46           | (false, t) => t
    47 
    48         fun try_variant variant =
    49            case preplay_quietly timeout variant of
    50              (true, _) => NONE
    51            | time as (false, _) => SOME (variant, time)
    52 
    53       in
    54         case Par_List.get_some try_variant (variants step) of
    55           SOME (step, time) => (set_preplay_time l time; step)
    56         | NONE => step
    57       end
    58 
    59 fun try0 preplay_timeout preplay_interface proof =
    60      map_isar_steps (try0_step preplay_timeout preplay_interface) proof
    61 
    62 end;