src/Tools/quickcheck.ML
changeset 35379 d0c779d012dc
parent 35378 95d0e3adf38e
child 35380 6ac5b81a763d
     1.1 --- a/src/Tools/quickcheck.ML	Thu Feb 25 09:28:01 2010 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Thu Feb 25 10:04:50 2010 +0100
     1.3 @@ -63,29 +63,29 @@
     1.4  (* quickcheck configuration -- default parameters, test generators *)
     1.5  
     1.6  datatype test_params = Test_Params of
     1.7 -  { size: int, iterations: int, default_type: typ option, no_assms: bool, report: bool};
     1.8 +  { size: int, iterations: int, default_type: typ option, no_assms: bool, report: bool, quiet : bool};
     1.9  
    1.10 -fun dest_test_params (Test_Params { size, iterations, default_type, no_assms, report }) =
    1.11 -  ((size, iterations), ((default_type, no_assms), report));
    1.12 -fun make_test_params ((size, iterations), ((default_type, no_assms), report)) =
    1.13 +fun dest_test_params (Test_Params { size, iterations, default_type, no_assms, report, quiet }) =
    1.14 +  ((size, iterations), ((default_type, no_assms), (report, quiet)));
    1.15 +fun make_test_params ((size, iterations), ((default_type, no_assms), (report, quiet))) =
    1.16    Test_Params { size = size, iterations = iterations, default_type = default_type,
    1.17 -                no_assms = no_assms, report = report };
    1.18 -fun map_test_params f (Test_Params { size, iterations, default_type, no_assms, report }) =
    1.19 -  make_test_params (f ((size, iterations), ((default_type, no_assms), report)));
    1.20 +                no_assms = no_assms, report = report, quiet = quiet };
    1.21 +fun map_test_params f (Test_Params { size, iterations, default_type, no_assms, report, quiet }) =
    1.22 +  make_test_params (f ((size, iterations), ((default_type, no_assms), (report, quiet))));
    1.23  fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
    1.24 -                                     no_assms = no_assms1, report = report1 },
    1.25 +                                     no_assms = no_assms1, report = report1, quiet = quiet1 },
    1.26    Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
    1.27 -                no_assms = no_assms2, report = report2 }) =
    1.28 +                no_assms = no_assms2, report = report2, quiet = quiet2 }) =
    1.29    make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
    1.30      ((case default_type1 of NONE => default_type2 | _ => default_type1, no_assms1 orelse no_assms2),
    1.31 -    report1 orelse report2));
    1.32 +    (report1 orelse report2, quiet1 orelse quiet2)));
    1.33  
    1.34  structure Data = Theory_Data
    1.35  (
    1.36    type T = (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
    1.37      * test_params;
    1.38    val empty = ([], Test_Params
    1.39 -    { size = 10, iterations = 100, default_type = NONE, no_assms = false, report = false});
    1.40 +    { size = 10, iterations = 100, default_type = NONE, no_assms = false, report = false, quiet = false});
    1.41    val extend = I;
    1.42    fun merge ((generators1, params1), (generators2, params2)) : T =
    1.43      (AList.merge (op =) (K true) (generators1, generators2),
    1.44 @@ -244,7 +244,7 @@
    1.45      let
    1.46        val ctxt = Proof.context_of state;
    1.47        val assms = map term_of (Assumption.all_assms_of ctxt);
    1.48 -      val Test_Params { size, iterations, default_type, no_assms, report } =
    1.49 +      val Test_Params { size, iterations, default_type, no_assms, report, quiet } =
    1.50          (snd o Data.get o Proof.theory_of) state;
    1.51        val res =
    1.52          try (test_goal true false NONE size iterations default_type no_assms [] 1 assms) state;
    1.53 @@ -278,7 +278,9 @@
    1.54    | parse_test_param ctxt ("no_assms", arg) =
    1.55        (apsnd o apfst o apsnd o K) (read_bool arg)
    1.56    | parse_test_param ctxt ("report", arg) =
    1.57 -      (apsnd o apsnd o K) (read_bool arg)
    1.58 +      (apsnd o apsnd o apfst o K) (read_bool arg)
    1.59 +  | parse_test_param ctxt ("quiet", arg) =
    1.60 +      (apsnd o apsnd o apsnd o K) (read_bool arg)
    1.61    | parse_test_param ctxt (name, _) =
    1.62        error ("Unknown test parameter: " ^ name);
    1.63  
    1.64 @@ -306,10 +308,10 @@
    1.65      val assms = map term_of (Assumption.all_assms_of ctxt);
    1.66      val default_params = (dest_test_params o snd o Data.get) thy;
    1.67      val f = fold (parse_test_param_inst ctxt) args;
    1.68 -    val (((size, iterations), ((default_type, no_assms), report)), (generator_name, insts)) =
    1.69 +    val (((size, iterations), ((default_type, no_assms), (report, quiet))), (generator_name, insts)) =
    1.70        f (default_params, (NONE, []));
    1.71    in
    1.72 -    test_goal false report generator_name size iterations default_type no_assms insts i assms state
    1.73 +    test_goal quiet report generator_name size iterations default_type no_assms insts i assms state
    1.74    end;
    1.75  
    1.76  fun quickcheck args i state = fst (gen_quickcheck args i state)