src/Tools/auto_counterexample.ML
author blanchet
Wed, 28 Oct 2009 17:43:43 +0100
changeset 33561 ab01b72715ef
child 33600 16a263d2b1c9
permissions -rw-r--r--
introduced Auto Nitpick in addition to Auto Quickcheck; this required generalizing the theorem hook used by Quickcheck, following a suggestion by Florian
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
     1
(*  Title:      Tools/auto_counterexample.ML
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
     3
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
     4
Counterexample Search Unit (do not abbreviate!).
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
     5
*)
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
     6
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
     7
signature AUTO_COUNTEREXAMPLE =
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
     8
sig
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
     9
  val time_limit: int Unsynchronized.ref
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    10
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    11
  val register_tool :
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    12
    string * (Proof.state -> bool * Proof.state) -> theory -> theory
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    13
end;
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    14
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    15
structure Auto_Counterexample : AUTO_COUNTEREXAMPLE =
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    16
struct
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    17
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    18
(* preferences *)
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    19
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    20
val time_limit = Unsynchronized.ref 2500
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    21
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    22
val _ =
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    23
  ProofGeneralPgip.add_preference Preferences.category_tracing
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    24
    (Preferences.nat_pref time_limit
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    25
      "auto-counterexample-time-limit"
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    26
      "Time limit for automatic counterexample search (in milliseconds).")
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    27
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    28
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    29
(* configuration *)
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    30
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    31
structure Data = TheoryDataFun(
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    32
  type T = (string * (Proof.state -> bool * Proof.state)) list
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    33
  val empty = []
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    34
  val copy = I
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    35
  val extend = I
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    36
  fun merge _ (tools1, tools2) = AList.merge (op =) (K true) (tools1, tools2)
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    37
)
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    38
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    39
val register_tool = Data.map o AList.update (op =)
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    40
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    41
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    42
(* automatic testing *)
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    43
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    44
val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    45
  case !time_limit of
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    46
    0 => state
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    47
  | ms =>
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    48
    TimeLimit.timeLimit (Time.fromMilliseconds ms)
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    49
        (fn () =>
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    50
            if interact andalso not (!Toplevel.quiet) then
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    51
              fold_rev (fn (_, tool) => fn (true, state) => (true, state)
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    52
                                         | (false, state) => tool state)
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    53
                   (Data.get (Proof.theory_of state)) (false, state) |> snd
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    54
            else
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    55
              state) ()
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    56
    handle TimeLimit.TimeOut =>
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    57
           (warning "Automatic counterexample search timed out."; state)))
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    58
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    59
end;