src/Tools/auto_counterexample.ML
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 33600 16a263d2b1c9
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
     1 (*  Title:      Tools/auto_counterexample.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3 
     4 Counterexample Search Unit (do not abbreviate!).
     5 *)
     6 
     7 signature AUTO_COUNTEREXAMPLE =
     8 sig
     9   val time_limit: int Unsynchronized.ref
    10 
    11   val register_tool :
    12     string * (Proof.state -> bool * Proof.state) -> theory -> theory
    13 end;
    14 
    15 structure Auto_Counterexample : AUTO_COUNTEREXAMPLE =
    16 struct
    17 
    18 (* preferences *)
    19 
    20 val time_limit = Unsynchronized.ref 2500
    21 
    22 val _ =
    23   ProofGeneralPgip.add_preference Preferences.category_tracing
    24     (Preferences.nat_pref time_limit
    25       "auto-counterexample-time-limit"
    26       "Time limit for automatic counterexample search (in milliseconds).")
    27 
    28 
    29 (* configuration *)
    30 
    31 structure Data = Theory_Data
    32 (
    33   type T = (string * (Proof.state -> bool * Proof.state)) list
    34   val empty = []
    35   val extend = I
    36   fun merge data : T = AList.merge (op =) (K true) data
    37 )
    38 
    39 val register_tool = Data.map o AList.update (op =)
    40 
    41 
    42 (* automatic testing *)
    43 
    44 val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
    45   case !time_limit of
    46     0 => state
    47   | ms =>
    48     TimeLimit.timeLimit (Time.fromMilliseconds ms)
    49         (fn () =>
    50             if interact andalso not (!Toplevel.quiet) then
    51               fold_rev (fn (_, tool) => fn (true, state) => (true, state)
    52                                          | (false, state) => tool state)
    53                    (Data.get (Proof.theory_of state)) (false, state) |> snd
    54             else
    55               state) ()
    56     handle TimeLimit.TimeOut =>
    57            (warning "Automatic counterexample search timed out."; state)))
    58 
    59 end;