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