# HG changeset patch # User wenzelm # Date 1422188090 -3600 # Node ID 570bea2407ea8d5e8f636187a4856bc8aac828b9 # Parent 7789b349f4786b377c1b66d29b84aabd8f482957 prefer plain tuples; diff -r 7789b349f478 -r 570bea2407ea src/Tools/quickcheck.ML --- 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