author  ballarin 
Sat, 31 Jul 2010 21:14:20 +0200  
changeset 38107  3a46cebd7983 
parent 37974  d9549f9da779 
child 38111  77f56abf158b 
permissions  rwrr 
30824  1 
(* Title: Tools/quickcheck.ML 
28256  2 
Author: Stefan Berghofer, Florian Haftmann, TU Muenchen 
3 

4 
Generic counterexample search engine. 

5 
*) 

6 

7 
signature QUICKCHECK = 

8 
sig 

37910
555287ba8d8d
reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents:
37909
diff
changeset

9 
val setup: theory > theory 
555287ba8d8d
reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents:
37909
diff
changeset

10 
(* configuration *) 
32740  11 
val auto: bool Unsynchronized.ref 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34128
diff
changeset

12 
val timing : bool Unsynchronized.ref 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

13 
datatype report = Report of 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

14 
{ iterations : int, raised_match_errors : int, 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

15 
satisfied_assms : int list, positive_concl_tests : int } 
37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

16 
datatype expectation = No_Expectation  No_Counterexample  Counterexample; 
37910
555287ba8d8d
reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents:
37909
diff
changeset

17 
datatype test_params = Test_Params of 
37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

18 
{ size: int, iterations: int, default_type: typ list, no_assms: bool, 
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

19 
expect : expectation, report: bool, quiet : bool}; 
37910
555287ba8d8d
reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents:
37909
diff
changeset

20 
val test_params_of: theory > test_params 
555287ba8d8d
reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents:
37909
diff
changeset

21 
val add_generator: 
555287ba8d8d
reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents:
37909
diff
changeset

22 
string * (Proof.context > bool > term > int > term list option * (bool list * bool)) 
555287ba8d8d
reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents:
37909
diff
changeset

23 
> theory > theory 
555287ba8d8d
reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents:
37909
diff
changeset

24 
(* testing terms and proof states *) 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

25 
val gen_test_term: Proof.context > bool > bool > string option > int > int > term > 
35380
6ac5b81a763d
adopting Mutabelle to quickcheck reporting; improving quickcheck reporting
bulwahn
parents:
35379
diff
changeset

26 
(string * term) list option * ((string * int) list * ((int * report list) list) option) 
30980  27 
val test_term: Proof.context > bool > string option > int > int > term > 
28 
(string * term) list option 

37909
583543ad6ad1
changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types
bulwahn
parents:
36960
diff
changeset

29 
val quickcheck: (string * string list) list > int > Proof.state > (string * term) list option 
28256  30 
end; 
31 

32 
structure Quickcheck : QUICKCHECK = 

33 
struct 

34 

30980  35 
(* preferences *) 
36 

32740  37 
val auto = Unsynchronized.ref false; 
30980  38 

34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34128
diff
changeset

39 
val timing = Unsynchronized.ref false; 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34128
diff
changeset

40 

30980  41 
val _ = 
42 
ProofGeneralPgip.add_preference Preferences.category_tracing 

32966
5b21661fe618
indicate CRITICAL nature of various setmp combinators;
wenzelm
parents:
32859
diff
changeset

43 
(setmp_CRITICAL auto true (fn () => 
30980  44 
Preferences.bool_pref auto 
45 
"autoquickcheck" 

33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

46 
"Whether to run Quickcheck automatically.") ()); 
30980  47 

35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

48 
(* quickcheck report *) 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

49 

95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

50 
datatype single_report = Run of bool list * bool  MatchExc 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

51 

95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

52 
datatype report = Report of 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

53 
{ iterations : int, raised_match_errors : int, 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

54 
satisfied_assms : int list, positive_concl_tests : int } 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

55 

95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

56 
fun collect_single_report single_report 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

57 
(Report {iterations = iterations, raised_match_errors = raised_match_errors, 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

58 
satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) = 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

59 
case single_report 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

60 
of MatchExc => 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

61 
Report {iterations = iterations + 1, raised_match_errors = raised_match_errors + 1, 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

62 
satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests} 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

63 
 Run (assms, concl) => 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

64 
Report {iterations = iterations + 1, raised_match_errors = raised_match_errors, 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

65 
satisfied_assms = 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

66 
map2 (fn b => fn s => if b then s + 1 else s) assms 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

67 
(if null satisfied_assms then replicate (length assms) 0 else satisfied_assms), 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

68 
positive_concl_tests = if concl then positive_concl_tests + 1 else positive_concl_tests} 
30973
304ab57afa6e
observe distinction between Pure/Tools and Tools more closely
haftmann
parents:
30824
diff
changeset

69 

37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

70 
(* expectation *) 
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

71 

22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

72 
datatype expectation = No_Expectation  No_Counterexample  Counterexample; 
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

73 

22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

74 
fun merge_expectation (expect1, expect2) = 
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

75 
if expect1 = expect2 then expect1 else No_Expectation 
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

76 

28315  77 
(* quickcheck configuration  default parameters, test generators *) 
78 

28309  79 
datatype test_params = Test_Params of 
37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

80 
{ size: int, iterations: int, default_type: typ list, no_assms: bool, 
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

81 
expect : expectation, report: bool, quiet : bool}; 
28309  82 

37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

83 
fun dest_test_params (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) = 
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

84 
((size, iterations), ((default_type, no_assms), ((expect, report), quiet))); 
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

85 
fun make_test_params ((size, iterations), ((default_type, no_assms), ((expect, report), quiet))) = 
34128
8650a073dd9b
made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default;
blanchet
parents:
33583
diff
changeset

86 
Test_Params { size = size, iterations = iterations, default_type = default_type, 
37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

87 
no_assms = no_assms, expect = expect, report = report, quiet = quiet }; 
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

88 
fun map_test_params f (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) = 
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

89 
make_test_params (f ((size, iterations), ((default_type, no_assms), ((expect, report), quiet)))); 
34128
8650a073dd9b
made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default;
blanchet
parents:
33583
diff
changeset

90 
fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1, 
37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

91 
no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1 }, 
34128
8650a073dd9b
made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default;
blanchet
parents:
33583
diff
changeset

92 
Test_Params { size = size2, iterations = iterations2, default_type = default_type2, 
37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

93 
no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2 }) = 
31599  94 
make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)), 
37911  95 
((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2), 
37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

96 
((merge_expectation (expect1, expect2), report1 orelse report2), quiet1 orelse quiet2))); 
28309  97 

33522  98 
structure Data = Theory_Data 
99 
( 

35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

100 
type T = (string * (Proof.context > bool > term > int > term list option * (bool list * bool))) list 
28309  101 
* test_params; 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

102 
val empty = ([], Test_Params 
37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

103 
{ size = 10, iterations = 100, default_type = [], no_assms = false, 
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

104 
expect = No_Expectation, report = false, quiet = false}); 
28256  105 
val extend = I; 
33522  106 
fun merge ((generators1, params1), (generators2, params2)) : T = 
107 
(AList.merge (op =) (K true) (generators1, generators2), 

28309  108 
merge_test_params (params1, params2)); 
33522  109 
); 
28256  110 

37910
555287ba8d8d
reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents:
37909
diff
changeset

111 
val test_params_of = snd o Data.get; 
555287ba8d8d
reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents:
37909
diff
changeset

112 

28309  113 
val add_generator = Data.map o apfst o AList.update (op =); 
114 

28315  115 
(* generating tests *) 
116 

28309  117 
fun mk_tester_select name ctxt = 
118 
case AList.lookup (op =) ((fst o Data.get o ProofContext.theory_of) ctxt) name 

119 
of NONE => error ("No such quickcheck generator: " ^ name) 

120 
 SOME generator => generator ctxt; 

121 

35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

122 
fun mk_testers ctxt report t = 
28309  123 
(map snd o fst o Data.get o ProofContext.theory_of) ctxt 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

124 
> map_filter (fn generator => try (generator ctxt report) t); 
28309  125 

35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

126 
fun mk_testers_strict ctxt report t = 
28309  127 
let 
128 
val generators = ((map snd o fst o Data.get o ProofContext.theory_of) ctxt) 

35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

129 
val testers = map (fn generator => Exn.capture (generator ctxt report) t) generators; 
28309  130 
in if forall (is_none o Exn.get_result) testers 
131 
then [(Exn.release o snd o split_last) testers] 

132 
else map_filter Exn.get_result testers 

133 
end; 

134 

28315  135 

136 
(* testing propositions *) 

137 

28309  138 
fun prep_test_term t = 
139 
let 

29266  140 
val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse 
28309  141 
error "Term to be tested contains type variables"; 
29266  142 
val _ = null (Term.add_vars t []) orelse 
28309  143 
error "Term to be tested contains schematic variables"; 
31138  144 
val frees = Term.add_frees t []; 
28309  145 
in (map fst frees, list_abs_free (frees, t)) end 
28256  146 

35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35077
diff
changeset

147 
fun cpu_time description f = 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35077
diff
changeset

148 
let 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35077
diff
changeset

149 
val start = start_timing () 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35077
diff
changeset

150 
val result = Exn.capture f () 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35077
diff
changeset

151 
val time = Time.toMilliseconds (#cpu (end_timing start)) 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35077
diff
changeset

152 
in (Exn.release result, (description, time)) end 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35077
diff
changeset

153 

35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

154 
fun gen_test_term ctxt quiet report generator_name size i t = 
28309  155 
let 
156 
val (names, t') = prep_test_term t; 

35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35077
diff
changeset

157 
val (testers, comp_time) = cpu_time "quickcheck compilation" 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35077
diff
changeset

158 
(fn () => (case generator_name 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

159 
of NONE => if quiet then mk_testers ctxt report t' else mk_testers_strict ctxt report t' 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

160 
 SOME name => [mk_tester_select name ctxt report t'])); 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

161 
fun iterate f 0 report = (NONE, report) 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

162 
 iterate f j report = 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

163 
let 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

164 
val (test_result, single_report) = apsnd Run (f ()) handle Match => (if quiet then () 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

165 
else warning "Exception Match raised during quickcheck"; (NONE, MatchExc)) 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

166 
val report = collect_single_report single_report report 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

167 
in 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

168 
case test_result of NONE => iterate f (j  1) report  SOME q => (SOME q, report) 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

169 
end 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

170 
val empty_report = Report { iterations = 0, raised_match_errors = 0, 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

171 
satisfied_assms = [], positive_concl_tests = 0 } 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

172 
fun with_testers k [] = (NONE, []) 
28309  173 
 with_testers k (tester :: testers) = 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

174 
case iterate (fn () => tester (k  1)) i empty_report 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

175 
of (NONE, report) => apsnd (cons report) (with_testers k testers) 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

176 
 (SOME q, report) => (SOME q, [report]); 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

177 
fun with_size k reports = if k > size then (NONE, reports) 
28309  178 
else (if quiet then () else priority ("Test data size: " ^ string_of_int k); 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

179 
let 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

180 
val (result, new_report) = with_testers k testers 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

181 
val reports = ((k, new_report) :: reports) 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

182 
in case result of NONE => with_size (k + 1) reports  SOME q => (SOME q, reports) end); 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

183 
val ((result, reports), exec_time) = cpu_time "quickcheck execution" 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

184 
(fn () => apfst 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

185 
(fn result => case result of NONE => NONE 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

186 
 SOME ts => SOME (names ~~ ts)) (with_size 1 [])) 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34128
diff
changeset

187 
in 
35380
6ac5b81a763d
adopting Mutabelle to quickcheck reporting; improving quickcheck reporting
bulwahn
parents:
35379
diff
changeset

188 
(result, ([exec_time, comp_time], if report then SOME reports else NONE)) 
28309  189 
end; 
190 

35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35077
diff
changeset

191 
fun test_term ctxt quiet generator_name size i t = 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

192 
fst (gen_test_term ctxt quiet false generator_name size i t) 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35077
diff
changeset

193 

37913
e85f5ad02a8f
correcting wellsortedness check and improving error message
bulwahn
parents:
37912
diff
changeset

194 
exception WELLSORTED of string 
e85f5ad02a8f
correcting wellsortedness check and improving error message
bulwahn
parents:
37912
diff
changeset

195 

28309  196 
fun monomorphic_term thy insts default_T = 
197 
let 

198 
fun subst (T as TFree (v, S)) = 

199 
let 

200 
val T' = AList.lookup (op =) insts v 

37912  201 
> the_default default_T 
37913
e85f5ad02a8f
correcting wellsortedness check and improving error message
bulwahn
parents:
37912
diff
changeset

202 
in if Sign.of_sort thy (T', S) then T' 
e85f5ad02a8f
correcting wellsortedness check and improving error message
bulwahn
parents:
37912
diff
changeset

203 
else raise (WELLSORTED ("For instantiation with default_type " ^ Syntax.string_of_typ_global thy default_T ^ 
e85f5ad02a8f
correcting wellsortedness check and improving error message
bulwahn
parents:
37912
diff
changeset

204 
":\n" ^ Syntax.string_of_typ_global thy T' ^ 
28309  205 
" to be substituted for variable " ^ 
37913
e85f5ad02a8f
correcting wellsortedness check and improving error message
bulwahn
parents:
37912
diff
changeset

206 
Syntax.string_of_typ_global thy T ^ " does not have sort " ^ 
e85f5ad02a8f
correcting wellsortedness check and improving error message
bulwahn
parents:
37912
diff
changeset

207 
Syntax.string_of_sort_global thy S)) 
28309  208 
end 
209 
 subst T = T; 

210 
in (map_types o map_atyps) subst end; 

211 

37913
e85f5ad02a8f
correcting wellsortedness check and improving error message
bulwahn
parents:
37912
diff
changeset

212 
datatype wellsorted_error = Wellsorted_Error of string  Term of term 
e85f5ad02a8f
correcting wellsortedness check and improving error message
bulwahn
parents:
37912
diff
changeset

213 

37974
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

214 
fun test_goal quiet report generator_name size iterations default_Ts no_assms insts i state = 
28309  215 
let 
37974
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

216 
val lthy = Proof.context_of state; 
28309  217 
val thy = Proof.theory_of state; 
218 
fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t 

219 
 strip t = t; 

33291  220 
val {goal = st, ...} = Proof.raw_goal state; 
28309  221 
val (gi, frees) = Logic.goal_params (prop_of st) i; 
37974
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

222 
val some_locale = case (#target o Theory_Target.peek) lthy 
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

223 
of "" => NONE 
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

224 
 locale => SOME locale; 
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

225 
val assms = if no_assms then [] else case some_locale 
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

226 
of NONE => Assumption.all_assms_of lthy 
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

227 
 SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy); 
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

228 
val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi)); 
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

229 
val check_goals = case some_locale 
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

230 
of NONE => [proto_goal] 
38107  231 
 SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal) (Locale.registrations_of_locale (Context.Theory thy) (*FIXME*) locale); 
37974
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

232 
val inst_goals = maps (fn check_goal => map (fn T => 
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

233 
Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal) 
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

234 
handle WELLSORTED s => Wellsorted_Error s) default_Ts) check_goals 
37913
e85f5ad02a8f
correcting wellsortedness check and improving error message
bulwahn
parents:
37912
diff
changeset

235 
val error_msg = cat_lines (map_filter (fn Term t => NONE  Wellsorted_Error s => SOME s) inst_goals) 
e85f5ad02a8f
correcting wellsortedness check and improving error message
bulwahn
parents:
37912
diff
changeset

236 
val correct_inst_goals = 
e85f5ad02a8f
correcting wellsortedness check and improving error message
bulwahn
parents:
37912
diff
changeset

237 
case map_filter (fn Term t => SOME t  Wellsorted_Error s => NONE) inst_goals of 
e85f5ad02a8f
correcting wellsortedness check and improving error message
bulwahn
parents:
37912
diff
changeset

238 
[] => error error_msg 
e85f5ad02a8f
correcting wellsortedness check and improving error message
bulwahn
parents:
37912
diff
changeset

239 
 xs => xs 
e85f5ad02a8f
correcting wellsortedness check and improving error message
bulwahn
parents:
37912
diff
changeset

240 
val _ = if quiet then () else warning error_msg 
37912  241 
fun collect_results f reports [] = (NONE, rev reports) 
242 
 collect_results f reports (t :: ts) = 

243 
case f t of 

244 
(SOME res, report) => (SOME res, rev (report :: reports)) 

245 
 (NONE, report) => collect_results f (report :: reports) ts 

37974
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

246 
in collect_results (gen_test_term lthy quiet report generator_name size iterations) [] correct_inst_goals end; 
37912  247 

248 
(* pretty printing *) 

28315  249 

35077
c1dac8ace020
make Quickcheck identify itself, so people don't submit bug reports to me thinking that it was Nitpick
blanchet
parents:
34948
diff
changeset

250 
fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample." 
28315  251 
 pretty_counterex ctxt (SOME cex) = 
35077
c1dac8ace020
make Quickcheck identify itself, so people don't submit bug reports to me thinking that it was Nitpick
blanchet
parents:
34948
diff
changeset

252 
Pretty.chunks (Pretty.str "Quickcheck found a counterexample:\n" :: 
28315  253 
map (fn (s, t) => 
254 
Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex); 

255 

35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

256 
fun pretty_report (Report {iterations = iterations, raised_match_errors = raised_match_errors, 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

257 
satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) = 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

258 
let 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

259 
fun pretty_stat s i = Pretty.block ([Pretty.str (s ^ ": " ^ string_of_int i)]) 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

260 
in 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

261 
([pretty_stat "iterations" iterations, 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

262 
pretty_stat "match exceptions" raised_match_errors] 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

263 
@ map_index (fn (i, n) => pretty_stat ("satisfied " ^ string_of_int (i + 1) ^ ". assumption") n) 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

264 
satisfied_assms 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

265 
@ [pretty_stat "positive conclusion tests" positive_concl_tests]) 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

266 
end 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

267 

95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

268 
fun pretty_reports' [report] = [Pretty.chunks (pretty_report report)] 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

269 
 pretty_reports' reports = 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

270 
map_index (fn (i, report) => 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

271 
Pretty.chunks (Pretty.str (string_of_int (i + 1) ^ ". generator:\n") :: pretty_report report)) 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

272 
reports 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

273 

35380
6ac5b81a763d
adopting Mutabelle to quickcheck reporting; improving quickcheck reporting
bulwahn
parents:
35379
diff
changeset

274 
fun pretty_reports ctxt (SOME reports) = 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

275 
Pretty.chunks (Pretty.str "Quickcheck report:" :: 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

276 
maps (fn (size, reports) => 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

277 
Pretty.str ("size " ^ string_of_int size ^ ":") :: pretty_reports' reports @ [Pretty.brk 1]) 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

278 
(rev reports)) 
35380
6ac5b81a763d
adopting Mutabelle to quickcheck reporting; improving quickcheck reporting
bulwahn
parents:
35379
diff
changeset

279 
 pretty_reports ctxt NONE = Pretty.str "" 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

280 

37912  281 
fun pretty_counterex_and_reports ctxt (cex, timing_and_reports) = 
282 
Pretty.chunks (pretty_counterex ctxt cex :: map (pretty_reports ctxt) (map snd timing_and_reports)) 

28315  283 

284 
(* automatic testing *) 

28309  285 

33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

286 
fun auto_quickcheck state = 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

287 
if not (!auto) then 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

288 
(false, state) 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

289 
else 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

290 
let 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

291 
val ctxt = Proof.context_of state; 
37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

292 
val Test_Params {size, iterations, default_type, no_assms, ...} = 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

293 
(snd o Data.get o Proof.theory_of) state; 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

294 
val res = 
37974
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

295 
try (test_goal true false NONE size iterations default_type no_assms [] 1) state; 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

296 
in 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

297 
case res of 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

298 
NONE => (false, state) 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

299 
 SOME (NONE, report) => (false, state) 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

300 
 SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "", 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

301 
Pretty.mark Markup.hilite (pretty_counterex ctxt cex)])) state) 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

302 
end 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

303 

ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

304 
val setup = Auto_Counterexample.register_tool ("quickcheck", auto_quickcheck) 
28315  305 

306 

30980  307 
(* Isar commands *) 
28315  308 

28336  309 
fun read_nat s = case (Library.read_int o Symbol.explode) s 
310 
of (k, []) => if k >= 0 then k 

311 
else error ("Not a natural number: " ^ s) 

312 
 (_, _ :: _) => error ("Not a natural number: " ^ s); 

37909
583543ad6ad1
changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types
bulwahn
parents:
36960
diff
changeset

313 

34128
8650a073dd9b
made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default;
blanchet
parents:
33583
diff
changeset

314 
fun read_bool "false" = false 
8650a073dd9b
made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default;
blanchet
parents:
33583
diff
changeset

315 
 read_bool "true" = true 
8650a073dd9b
made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default;
blanchet
parents:
33583
diff
changeset

316 
 read_bool s = error ("Not a Boolean value: " ^ s) 
28315  317 

37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

318 
fun read_expectation "no_expectation" = No_Expectation 
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

319 
 read_expectation "no_counterexample" = No_Counterexample 
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

320 
 read_expectation "counterexample" = Counterexample 
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

321 
 read_expectation s = error ("Not an expectation value: " ^ s) 
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

322 

37909
583543ad6ad1
changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types
bulwahn
parents:
36960
diff
changeset

323 
fun parse_test_param ctxt ("size", [arg]) = 
28336  324 
(apfst o apfst o K) (read_nat arg) 
37909
583543ad6ad1
changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types
bulwahn
parents:
36960
diff
changeset

325 
 parse_test_param ctxt ("iterations", [arg]) = 
28336  326 
(apfst o apsnd o K) (read_nat arg) 
327 
 parse_test_param ctxt ("default_type", arg) = 

37909
583543ad6ad1
changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types
bulwahn
parents:
36960
diff
changeset

328 
(apsnd o apfst o apfst o K) (map (ProofContext.read_typ ctxt) arg) 
583543ad6ad1
changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types
bulwahn
parents:
36960
diff
changeset

329 
 parse_test_param ctxt ("no_assms", [arg]) = 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

330 
(apsnd o apfst o apsnd o K) (read_bool arg) 
37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

331 
 parse_test_param ctxt ("expect", [arg]) = 
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

332 
(apsnd o apsnd o apfst o apfst o K) (read_expectation arg) 
37909
583543ad6ad1
changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types
bulwahn
parents:
36960
diff
changeset

333 
 parse_test_param ctxt ("report", [arg]) = 
37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

334 
(apsnd o apsnd o apfst o apsnd o K) (read_bool arg) 
37909
583543ad6ad1
changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types
bulwahn
parents:
36960
diff
changeset

335 
 parse_test_param ctxt ("quiet", [arg]) = 
37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

336 
(apsnd o apsnd o apsnd o K) (read_bool arg) 
28336  337 
 parse_test_param ctxt (name, _) = 
34128
8650a073dd9b
made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default;
blanchet
parents:
33583
diff
changeset

338 
error ("Unknown test parameter: " ^ name); 
28315  339 

37909
583543ad6ad1
changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types
bulwahn
parents:
36960
diff
changeset

340 
fun parse_test_param_inst ctxt ("generator", [arg]) = 
28336  341 
(apsnd o apfst o K o SOME) arg 
342 
 parse_test_param_inst ctxt (name, arg) = 

343 
case try (ProofContext.read_typ ctxt) name 

344 
of SOME (TFree (v, _)) => (apsnd o apsnd o AList.update (op =)) 

37909
583543ad6ad1
changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types
bulwahn
parents:
36960
diff
changeset

345 
(v, ProofContext.read_typ ctxt (the_single arg)) 
28336  346 
 _ => (apfst o parse_test_param ctxt) (name, arg); 
28309  347 

28336  348 
fun quickcheck_params_cmd args thy = 
28315  349 
let 
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
35625
diff
changeset

350 
val ctxt = ProofContext.init_global thy; 
28336  351 
val f = fold (parse_test_param ctxt) args; 
28315  352 
in 
353 
thy 

28336  354 
> (Data.map o apsnd o map_test_params) f 
28315  355 
end; 
356 

35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

357 
fun gen_quickcheck args i state = 
28315  358 
let 
32297  359 
val thy = Proof.theory_of state; 
360 
val ctxt = Proof.context_of state; 

28315  361 
val default_params = (dest_test_params o snd o Data.get) thy; 
28336  362 
val f = fold (parse_test_param_inst ctxt) args; 
37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

363 
val (((size, iterations), ((default_type, no_assms), ((expect, report), quiet))), (generator_name, insts)) = 
28336  364 
f (default_params, (NONE, [])); 
32297  365 
in 
37974
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

366 
test_goal quiet report generator_name size iterations default_type no_assms insts i state 
37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

367 
> tap (fn (SOME x, _) => if expect = No_Counterexample then 
37974
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

368 
error ("quickcheck expected to find no counterexample but found one") else () 
37929
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

369 
 (NONE, _) => if expect = Counterexample then 
22e0797857e6
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents:
37913
diff
changeset

370 
error ("quickcheck expected to find a counterexample but did not find one") else ()) 
32297  371 
end; 
372 

36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

373 
fun quickcheck args i state = fst (gen_quickcheck args i state); 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

374 

32297  375 
fun quickcheck_cmd args i state = 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

376 
gen_quickcheck args i (Toplevel.proof_of state) 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

377 
> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state); 
28309  378 

37909
583543ad6ad1
changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types
bulwahn
parents:
36960
diff
changeset

379 
val parse_arg = Parse.name  (Scan.optional (Parse.$$$ "="  
583543ad6ad1
changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types
bulwahn
parents:
36960
diff
changeset

380 
((Parse.name >> single)  (Parse.$$$ "["  Parse.list1 Parse.name  Parse.$$$ "]"))) ["true"]); 
28309  381 

36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

382 
val parse_args = Parse.$$$ "["  Parse.list1 parse_arg  Parse.$$$ "]" 
28336  383 
 Scan.succeed []; 
384 

36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

385 
val _ = 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

386 
Outer_Syntax.command "quickcheck_params" "set parameters for random testing" Keyword.thy_decl 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

387 
(parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args))); 
28309  388 

36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

389 
val _ = 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

390 
Outer_Syntax.improper_command "quickcheck" "try to find counterexample for subgoal" Keyword.diag 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

391 
(parse_args  Scan.optional Parse.nat 1 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

392 
>> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i))); 
28309  393 

28315  394 
end; 
28309  395 

396 

28315  397 
val auto_quickcheck = Quickcheck.auto; 