src/Tools/quickcheck.ML
changeset 32740 9dd0a2f83429
parent 32297 3a4081abb3f7
child 32859 204f749f35a9
equal deleted inserted replaced
32739:31e75ad9ae17 32740:9dd0a2f83429
     4 Generic counterexample search engine.
     4 Generic counterexample search engine.
     5 *)
     5 *)
     6 
     6 
     7 signature QUICKCHECK =
     7 signature QUICKCHECK =
     8 sig
     8 sig
     9   val auto: bool ref
     9   val auto: bool Unsynchronized.ref
    10   val auto_time_limit: int ref
    10   val auto_time_limit: int Unsynchronized.ref
    11   val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
    11   val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
    12     (string * term) list option
    12     (string * term) list option
    13   val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
    13   val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
    14   val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option
    14   val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option
    15 end;
    15 end;
    17 structure Quickcheck : QUICKCHECK =
    17 structure Quickcheck : QUICKCHECK =
    18 struct
    18 struct
    19 
    19 
    20 (* preferences *)
    20 (* preferences *)
    21 
    21 
    22 val auto = ref false;
    22 val auto = Unsynchronized.ref false;
    23 val auto_time_limit = ref 2500;
    23 val auto_time_limit = Unsynchronized.ref 2500;
    24 
    24 
    25 val _ =
    25 val _ =
    26   ProofGeneralPgip.add_preference Preferences.category_tracing
    26   ProofGeneralPgip.add_preference Preferences.category_tracing
    27   (setmp auto true (fn () =>
    27   (setmp auto true (fn () =>
    28     Preferences.bool_pref auto
    28     Preferences.bool_pref auto