src/Tools/quickcheck.ML
changeset 30980 fe0855471964
parent 30973 304ab57afa6e
child 31138 a51ce445d498
     1.1 --- a/src/Tools/quickcheck.ML	Sat Apr 25 20:31:27 2009 +0200
     1.2 +++ b/src/Tools/quickcheck.ML	Sat Apr 25 21:28:04 2009 +0200
     1.3 @@ -6,16 +6,34 @@
     1.4  
     1.5  signature QUICKCHECK =
     1.6  sig
     1.7 -  val test_term: Proof.context -> bool -> string option -> int -> int -> term -> (string * term) list option;
     1.8 -  val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
     1.9    val auto: bool ref
    1.10    val auto_time_limit: int ref
    1.11 +  val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
    1.12 +    (string * term) list option
    1.13 +  val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
    1.14  end;
    1.15  
    1.16  structure Quickcheck : QUICKCHECK =
    1.17  struct
    1.18  
    1.19 -open Quickcheck; (*c.f. Pure/Tools/ROOT.ML*)
    1.20 +(* preferences *)
    1.21 +
    1.22 +val auto = ref false;
    1.23 +val auto_time_limit = ref 2500;
    1.24 +
    1.25 +val _ =
    1.26 +  ProofGeneralPgip.add_preference Preferences.category_tracing
    1.27 +  (setmp auto true (fn () =>
    1.28 +    Preferences.bool_pref auto
    1.29 +      "auto-quickcheck"
    1.30 +      "Whether to enable quickcheck automatically.") ());
    1.31 +
    1.32 +val _ =
    1.33 +  ProofGeneralPgip.add_preference Preferences.category_tracing
    1.34 +    (Preferences.nat_pref auto_time_limit
    1.35 +      "auto-quickcheck-time-limit"
    1.36 +      "Time limit for automatic quickcheck (in milliseconds).");
    1.37 +
    1.38  
    1.39  (* quickcheck configuration -- default parameters, test generators *)
    1.40  
    1.41 @@ -140,7 +158,7 @@
    1.42  
    1.43  (* automatic testing *)
    1.44  
    1.45 -fun test_goal_auto int state =
    1.46 +val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
    1.47    let
    1.48      val ctxt = Proof.context_of state;
    1.49      val assms = map term_of (Assumption.all_assms_of ctxt);
    1.50 @@ -161,12 +179,10 @@
    1.51      if int andalso !auto andalso not (!Toplevel.quiet)
    1.52      then test ()
    1.53      else state
    1.54 -  end;
    1.55 -
    1.56 -val _ = Context.>> (Specification.add_theorem_hook test_goal_auto);
    1.57 +  end));
    1.58  
    1.59  
    1.60 -(* Isar interfaces *)
    1.61 +(* Isar commands *)
    1.62  
    1.63  fun read_nat s = case (Library.read_int o Symbol.explode) s
    1.64   of (k, []) => if k >= 0 then k