50 fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1 }, |
50 fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1 }, |
51 Test_Params { size = size2, iterations = iterations2, default_type = default_type2 }) = |
51 Test_Params { size = size2, iterations = iterations2, default_type = default_type2 }) = |
52 make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)), |
52 make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)), |
53 case default_type1 of NONE => default_type2 | _ => default_type1); |
53 case default_type1 of NONE => default_type2 | _ => default_type1); |
54 |
54 |
55 structure Data = TheoryDataFun( |
55 structure Data = Theory_Data |
|
56 ( |
56 type T = (string * (Proof.context -> term -> int -> term list option)) list |
57 type T = (string * (Proof.context -> term -> int -> term list option)) list |
57 * test_params; |
58 * test_params; |
58 val empty = ([], Test_Params { size = 10, iterations = 100, default_type = NONE }); |
59 val empty = ([], Test_Params { size = 10, iterations = 100, default_type = NONE }); |
59 val copy = I; |
|
60 val extend = I; |
60 val extend = I; |
61 fun merge pp ((generators1, params1), (generators2, params2)) = |
61 fun merge ((generators1, params1), (generators2, params2)) : T = |
62 (AList.merge (op = : string * string -> bool) (K true) (generators1, generators2), |
62 (AList.merge (op =) (K true) (generators1, generators2), |
63 merge_test_params (params1, params2)); |
63 merge_test_params (params1, params2)); |
64 ) |
64 ); |
65 |
65 |
66 val add_generator = Data.map o apfst o AList.update (op =); |
66 val add_generator = Data.map o apfst o AList.update (op =); |
67 |
67 |
68 |
68 |
69 (* generating tests *) |
69 (* generating tests *) |