equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 signature QUICKCHECK = |
7 signature QUICKCHECK = |
8 sig |
8 sig |
9 val auto: bool Unsynchronized.ref |
9 val auto: bool Unsynchronized.ref |
|
10 val timing : bool Unsynchronized.ref |
10 val test_term: Proof.context -> bool -> string option -> int -> int -> term -> |
11 val test_term: Proof.context -> bool -> string option -> int -> int -> term -> |
11 (string * term) list option |
12 (string * term) list option |
12 val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory |
13 val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory |
13 val setup: theory -> theory |
14 val setup: theory -> theory |
14 val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option |
15 val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option |
18 struct |
19 struct |
19 |
20 |
20 (* preferences *) |
21 (* preferences *) |
21 |
22 |
22 val auto = Unsynchronized.ref false; |
23 val auto = Unsynchronized.ref false; |
|
24 |
|
25 val timing = Unsynchronized.ref false; |
23 |
26 |
24 val _ = |
27 val _ = |
25 ProofGeneralPgip.add_preference Preferences.category_tracing |
28 ProofGeneralPgip.add_preference Preferences.category_tracing |
26 (setmp_CRITICAL auto true (fn () => |
29 (setmp_CRITICAL auto true (fn () => |
27 Preferences.bool_pref auto |
30 Preferences.bool_pref auto |
95 in (map fst frees, list_abs_free (frees, t)) end |
98 in (map fst frees, list_abs_free (frees, t)) end |
96 |
99 |
97 fun test_term ctxt quiet generator_name size i t = |
100 fun test_term ctxt quiet generator_name size i t = |
98 let |
101 let |
99 val (names, t') = prep_test_term t; |
102 val (names, t') = prep_test_term t; |
100 val testers = case generator_name |
103 val testers = (*cond_timeit (!timing) "quickcheck compilation" |
101 of NONE => if quiet then mk_testers ctxt t' else mk_testers_strict ctxt t' |
104 (fn () => *)(case generator_name |
102 | SOME name => [mk_tester_select name ctxt t']; |
105 of NONE => if quiet then mk_testers ctxt t' else mk_testers_strict ctxt t' |
|
106 | SOME name => [mk_tester_select name ctxt t']); |
103 fun iterate f 0 = NONE |
107 fun iterate f 0 = NONE |
104 | iterate f j = case f () handle Match => (if quiet then () |
108 | iterate f j = case f () handle Match => (if quiet then () |
105 else warning "Exception Match raised during quickcheck"; NONE) |
109 else warning "Exception Match raised during quickcheck"; NONE) |
106 of NONE => iterate f (j - 1) | SOME q => SOME q; |
110 of NONE => iterate f (j - 1) | SOME q => SOME q; |
107 fun with_testers k [] = NONE |
111 fun with_testers k [] = NONE |
111 | SOME q => SOME q; |
115 | SOME q => SOME q; |
112 fun with_size k = if k > size then NONE |
116 fun with_size k = if k > size then NONE |
113 else (if quiet then () else priority ("Test data size: " ^ string_of_int k); |
117 else (if quiet then () else priority ("Test data size: " ^ string_of_int k); |
114 case with_testers k testers |
118 case with_testers k testers |
115 of NONE => with_size (k + 1) | SOME q => SOME q); |
119 of NONE => with_size (k + 1) | SOME q => SOME q); |
116 in case with_size 1 |
120 in |
117 of NONE => NONE |
121 cond_timeit (!timing) "quickcheck execution" |
118 | SOME ts => SOME (names ~~ ts) |
122 (fn () => case with_size 1 |
|
123 of NONE => NONE |
|
124 | SOME ts => SOME (names ~~ ts)) |
119 end; |
125 end; |
120 |
126 |
121 fun monomorphic_term thy insts default_T = |
127 fun monomorphic_term thy insts default_T = |
122 let |
128 let |
123 fun subst (T as TFree (v, S)) = |
129 fun subst (T as TFree (v, S)) = |