--- a/src/Tools/quickcheck.ML Sun Jan 25 13:04:36 2015 +0100
+++ b/src/Tools/quickcheck.ML Sun Jan 25 13:14:50 2015 +0100
@@ -208,38 +208,33 @@
structure Data = Generic_Data
(
type T =
- ((string * (bool Config.T * tester)) list *
- ((string * (Proof.context -> term list -> (int -> term list option) list)) list *
- ((string * (Proof.context -> term list -> (int -> bool) list)) list))) *
- test_params;
- val empty = (([], ([], [])), Test_Params {default_type = [], expect = No_Expectation});
+ (string * (bool Config.T * tester)) list *
+ (string * (Proof.context -> term list -> (int -> term list option) list)) list *
+ (string * (Proof.context -> term list -> (int -> bool) list)) list *
+ test_params;
+ val empty = ([], [], [], Test_Params {default_type = [], expect = No_Expectation});
val extend = I;
fun merge
- (((testers1, (batch_generators1, batch_validators1)), params1),
- ((testers2, (batch_generators2, batch_validators2)), params2)) : T =
- ((AList.merge (op =) (K true) (testers1, testers2),
- (AList.merge (op =) (K true) (batch_generators1, batch_generators2),
- AList.merge (op =) (K true) (batch_validators1, batch_validators2))),
- merge_test_params (params1, params2));
+ ((testers1, batch_generators1, batch_validators1, params1),
+ (testers2, batch_generators2, batch_validators2, params2)) : T =
+ (AList.merge (op =) (K true) (testers1, testers2),
+ AList.merge (op =) (K true) (batch_generators1, batch_generators2),
+ AList.merge (op =) (K true) (batch_validators1, batch_validators2),
+ merge_test_params (params1, params2));
);
-val test_params_of = snd o Data.get o Context.Proof;
-
+val test_params_of = #4 o Data.get o Context.Proof;
val default_type = fst o dest_test_params o test_params_of;
-
val expect = snd o dest_test_params o test_params_of;
+val map_test_params = Data.map o @{apply 4(4)} o map_test_params';
-val map_test_params = Data.map o apsnd o map_test_params';
-
-val add_tester = Data.map o apfst o apfst o AList.update (op =);
-
-val add_batch_generator = Data.map o apfst o apsnd o apfst o AList.update (op =);
-
-val add_batch_validator = Data.map o apfst o apsnd o apsnd o AList.update (op =);
+val add_tester = Data.map o @{apply 4(1)} o AList.update (op =);
+val add_batch_generator = Data.map o @{apply 4(2)} o AList.update (op =);
+val add_batch_validator = Data.map o @{apply 4(3)} o AList.update (op =);
fun active_testers ctxt =
let
- val testers = map snd (fst (fst (Data.get (Context.Proof ctxt))));
+ val testers = map snd (#1 (Data.get (Context.Proof ctxt)));
in
map snd (filter (fn (active, _) => Config.get ctxt active) testers)
end;
@@ -247,7 +242,7 @@
fun set_active_testers [] context = context
| set_active_testers testers context =
let
- val registered_testers = fst (fst (Data.get context));
+ val registered_testers = #1 (Data.get context);
in
fold (fn (name, (config, _)) => Config.put_generic config (member (op =) testers name))
registered_testers context
@@ -276,10 +271,8 @@
end
end;
-val mk_batch_tester =
- gen_mk_tester (AList.lookup (op =) o fst o snd o fst o Data.get o Context.Proof);
-val mk_batch_validator =
- gen_mk_tester (AList.lookup (op =) o snd o snd o fst o Data.get o Context.Proof);
+val mk_batch_tester = gen_mk_tester (AList.lookup (op =) o #2 o Data.get o Context.Proof);
+val mk_batch_validator = gen_mk_tester (AList.lookup (op =) o #3 o Data.get o Context.Proof);
(* testing propositions *)
@@ -433,7 +426,7 @@
| read_expectation s = error ("Not an expectation value: " ^ s);
fun valid_tester_name genctxt name =
- AList.defined (op =) (fst (fst (Data.get genctxt))) name;
+ AList.defined (op =) (#1 (Data.get genctxt)) name;
fun parse_tester name (testers, genctxt) =
if valid_tester_name genctxt name then