author  wenzelm 
Wed, 03 Nov 2010 21:53:56 +0100  
changeset 40335  3e4bb6e7c3ca 
parent 40253  f99ec71de82d 
child 40366  a2866dbfbe6b 
permissions  rwrr 
30824  1 
(* Title: Tools/quickcheck.ML 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

2 
Author: Stefan Berghofer, Florian Haftmann, Lukas Bulwahn, TU Muenchen 
28256  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, 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

19 
expect : expectation, report: bool, quiet : bool, timeout : int}; 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

20 
val test_params_of : Proof.context > test_params 
39253
0c47d615a69b
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn
parents:
39252
diff
changeset

21 
val report : Proof.context > bool 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

22 
val map_test_params : 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

23 
((int * int) * ((typ list * bool) * ((expectation * bool) * (bool * int))) 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

24 
> (int * int) * ((typ list * bool) * ((expectation * bool) * (bool * int)))) 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

25 
> Context.generic > Context.generic 
37910
555287ba8d8d
reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents:
37909
diff
changeset

26 
val add_generator: 
39253
0c47d615a69b
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn
parents:
39252
diff
changeset

27 
string * (Proof.context > term > int > term list option * (bool list * bool)) 
39252
8f176e575a49
changing the container for the quickcheck options to a generic data
bulwahn
parents:
39138
diff
changeset

28 
> Context.generic > Context.generic 
37910
555287ba8d8d
reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents:
37909
diff
changeset

29 
(* testing terms and proof states *) 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

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

31 
(string * term) list option * ((string * int) list * ((int * report list) 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

32 
val quickcheck: (string * string list) list > int > Proof.state > (string * term) list option 
28256  33 
end; 
34 

35 
structure Quickcheck : QUICKCHECK = 

36 
struct 

37 

30980  38 
(* preferences *) 
39 

32740  40 
val auto = Unsynchronized.ref false; 
30980  41 

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

42 
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

43 

30980  44 
val _ = 
45 
ProofGeneralPgip.add_preference Preferences.category_tracing 

39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39329
diff
changeset

46 
(Unsynchronized.setmp auto true (fn () => 
30980  47 
Preferences.bool_pref auto 
48 
"autoquickcheck" 

39329  49 
"Run Quickcheck automatically.") ()); 
30980  50 

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

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

52 

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

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

54 

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

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

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

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

58 

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

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

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

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

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

63 
of MatchExc => 
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 + 1, 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

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

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

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

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

69 
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

70 
(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

71 
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

72 

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

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

74 

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

75 
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

76 

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

77 
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

78 
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

79 

28315  80 
(* quickcheck configuration  default parameters, test generators *) 
81 

28309  82 
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

83 
{ size: int, iterations: int, default_type: typ list, no_assms: bool, 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

84 
expect : expectation, report: bool, quiet : bool, timeout : int}; 
28309  85 

40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

86 
fun dest_test_params 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

87 
(Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) = 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

88 
((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout)))); 
38759
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38390
diff
changeset

89 

40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

90 
fun make_test_params 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

91 
((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout)))) = 
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 = size, iterations = iterations, default_type = default_type, 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

93 
no_assms = no_assms, expect = expect, report = report, quiet = quiet, timeout = timeout }; 
38759
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38390
diff
changeset

94 

40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

95 
fun map_test_params' f 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

96 
(Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) = 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

97 
make_test_params 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

98 
(f ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout))))); 
38759
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38390
diff
changeset

99 

37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38390
diff
changeset

100 
fun merge_test_params 
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38390
diff
changeset

101 
(Test_Params { size = size1, iterations = iterations1, default_type = default_type1, 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

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

103 
Test_Params { size = size2, iterations = iterations2, default_type = default_type2, 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

104 
no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2, timeout = timeout2}) = 
31599  105 
make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)), 
37911  106 
((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2), 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

107 
((merge_expectation (expect1, expect2), report1 orelse report2), 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

108 
(quiet1 orelse quiet2, Int.min (timeout1, timeout2))))); 
28309  109 

39252
8f176e575a49
changing the container for the quickcheck options to a generic data
bulwahn
parents:
39138
diff
changeset

110 
structure Data = Generic_Data 
33522  111 
( 
38759
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38390
diff
changeset

112 
type T = 
39253
0c47d615a69b
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn
parents:
39252
diff
changeset

113 
(string * (Proof.context > term > int > term list option * (bool list * bool))) list 
38759
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38390
diff
changeset

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

115 
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

116 
{ size = 10, iterations = 100, default_type = [], no_assms = false, 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

117 
expect = No_Expectation, report = false, quiet = false, timeout = 30}); 
28256  118 
val extend = I; 
33522  119 
fun merge ((generators1, params1), (generators2, params2)) : T = 
120 
(AList.merge (op =) (K true) (generators1, generators2), 

28309  121 
merge_test_params (params1, params2)); 
33522  122 
); 
28256  123 

39252
8f176e575a49
changing the container for the quickcheck options to a generic data
bulwahn
parents:
39138
diff
changeset

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

125 

40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

126 
val size = fst o fst o dest_test_params o test_params_of 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

127 

c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

128 
val iterations = snd o fst o dest_test_params o test_params_of 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

129 

c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

130 
val default_type = fst o fst o snd o dest_test_params o test_params_of 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

131 

c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

132 
val no_assms = snd o fst o snd o dest_test_params o test_params_of 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

133 

c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

134 
val expect = fst o fst o snd o snd o dest_test_params o test_params_of 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

135 

39253
0c47d615a69b
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn
parents:
39252
diff
changeset

136 
val report = snd o fst o snd o snd o dest_test_params o test_params_of 
0c47d615a69b
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn
parents:
39252
diff
changeset

137 

40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

138 
val quiet = fst o snd o snd o snd o dest_test_params o test_params_of 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

139 

c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

140 
val timeout = snd o snd o snd o snd o dest_test_params o test_params_of 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

141 

c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

142 
fun map_report f 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

143 
(Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) = 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

144 
make_test_params 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

145 
((size, iterations), ((default_type, no_assms), ((expect, f report), (quiet, timeout)))); 
39253
0c47d615a69b
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn
parents:
39252
diff
changeset

146 

40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

147 
fun map_quiet f 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

148 
(Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) = 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

149 
make_test_params 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

150 
((size, iterations), ((default_type, no_assms), ((expect, report), (f quiet, timeout)))); 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

151 

c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

152 
fun set_report report = Data.map (apsnd (map_report (K report))) 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

153 

c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

154 
fun set_quiet quiet = Data.map (apsnd (map_quiet (K quiet))) 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

155 

c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

156 
val map_test_params = Data.map o apsnd o map_test_params' 
39253
0c47d615a69b
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn
parents:
39252
diff
changeset

157 

28309  158 
val add_generator = Data.map o apfst o AList.update (op =); 
159 

28315  160 
(* generating tests *) 
161 

28309  162 
fun mk_tester_select name ctxt = 
39252
8f176e575a49
changing the container for the quickcheck options to a generic data
bulwahn
parents:
39138
diff
changeset

163 
case AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) name 
28309  164 
of NONE => error ("No such quickcheck generator: " ^ name) 
165 
 SOME generator => generator ctxt; 

166 

39253
0c47d615a69b
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn
parents:
39252
diff
changeset

167 
fun mk_testers ctxt t = 
39252
8f176e575a49
changing the container for the quickcheck options to a generic data
bulwahn
parents:
39138
diff
changeset

168 
(map snd o fst o Data.get o Context.Proof) ctxt 
39253
0c47d615a69b
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn
parents:
39252
diff
changeset

169 
> map_filter (fn generator => try (generator ctxt) t); 
28309  170 

39253
0c47d615a69b
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn
parents:
39252
diff
changeset

171 
fun mk_testers_strict ctxt t = 
28309  172 
let 
40235
87998864284e
use Exn.interruptible_capture to keep usercode interruptible (Exn.capture not immediately followed by Exn.release here);
wenzelm
parents:
40225
diff
changeset

173 
val generators = ((map snd o fst o Data.get o Context.Proof) ctxt) 
87998864284e
use Exn.interruptible_capture to keep usercode interruptible (Exn.capture not immediately followed by Exn.release here);
wenzelm
parents:
40225
diff
changeset

174 
val testers = map (fn generator => Exn.interruptible_capture (generator ctxt) t) generators; 
87998864284e
use Exn.interruptible_capture to keep usercode interruptible (Exn.capture not immediately followed by Exn.release here);
wenzelm
parents:
40225
diff
changeset

175 
in 
87998864284e
use Exn.interruptible_capture to keep usercode interruptible (Exn.capture not immediately followed by Exn.release here);
wenzelm
parents:
40225
diff
changeset

176 
if forall (is_none o Exn.get_result) testers 
28309  177 
then [(Exn.release o snd o split_last) testers] 
178 
else map_filter Exn.get_result testers 

179 
end; 

180 

28315  181 

182 
(* testing propositions *) 

183 

28309  184 
fun prep_test_term t = 
185 
let 

29266  186 
val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse 
28309  187 
error "Term to be tested contains type variables"; 
29266  188 
val _ = null (Term.add_vars t []) orelse 
28309  189 
error "Term to be tested contains schematic variables"; 
31138  190 
val frees = Term.add_frees t []; 
28309  191 
in (map fst frees, list_abs_free (frees, t)) end 
28256  192 

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 
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

194 
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

195 
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

196 
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

197 
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

198 
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

199 

40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

200 
fun test_term ctxt generator_name t = 
28309  201 
let 
202 
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

203 
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

204 
(fn () => (case generator_name 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

205 
of NONE => if quiet ctxt then mk_testers ctxt t' else mk_testers_strict ctxt t' 
39253
0c47d615a69b
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn
parents:
39252
diff
changeset

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

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

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

209 
let 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

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

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

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

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

214 
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

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

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

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

218 
fun with_testers k [] = (NONE, []) 
28309  219 
 with_testers k (tester :: testers) = 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

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

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

222 
 (SOME q, report) => (SOME q, [report]); 
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39656
diff
changeset

223 
fun with_size k reports = 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

224 
if k > size ctxt then (NONE, reports) 
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39656
diff
changeset

225 
else 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

226 
(if quiet ctxt then () else Output.urgent_message ("Test data size: " ^ string_of_int k); 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

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

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

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

230 
in case result of NONE => with_size (k + 1) reports  SOME q => (SOME q, reports) end); 
40136  231 
val ((result, reports), exec_time) = 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

232 
TimeLimit.timeLimit (Time.fromSeconds (timeout ctxt)) (fn () => cpu_time "quickcheck execution" 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

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

234 
(fn result => case result of NONE => NONE 
40136  235 
 SOME ts => SOME (names ~~ ts)) (with_size 1 []))) () 
236 
handle TimeLimit.TimeOut => error "Reached timeout during Quickcheck" 

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

237 
in 
39253
0c47d615a69b
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn
parents:
39252
diff
changeset

238 
(result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE)) 
28309  239 
end; 
240 

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

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

242 

28309  243 
fun monomorphic_term thy insts default_T = 
244 
let 

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

246 
let 

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

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

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

250 
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

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

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

254 
Syntax.string_of_sort_global thy S)) 
28309  255 
end 
256 
 subst T = T; 

257 
in (map_types o map_atyps) subst end; 

258 

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

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

260 

40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

261 
fun test_goal generator_name insts i state = 
28309  262 
let 
37974
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

263 
val lthy = Proof.context_of state; 
28309  264 
val thy = Proof.theory_of state; 
265 
fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t 

266 
 strip t = t; 

33291  267 
val {goal = st, ...} = Proof.raw_goal state; 
28309  268 
val (gi, frees) = Logic.goal_params (prop_of st) i; 
38390  269 
val some_locale = case (Option.map #target o Named_Target.peek) lthy 
270 
of NONE => NONE 

271 
 SOME "" => NONE 

272 
 SOME locale => SOME locale; 

40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

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

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

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

276 
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

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

278 
of NONE => [proto_goal] 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

279 
 SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal) 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

280 
(Locale.registrations_of (Context.Theory thy) (*FIXME*) locale); 
37974
d9549f9da779
quickcheck images of goals under registration morphisms
haftmann
parents:
37929
diff
changeset

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

282 
Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal) 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

283 
handle WELLSORTED s => Wellsorted_Error s) (default_type lthy)) check_goals 
37913
e85f5ad02a8f
correcting wellsortedness check and improving error message
bulwahn
parents:
37912
diff
changeset

284 
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

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

286 
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

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

288 
 xs => xs 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

289 
val _ = if quiet lthy then () else warning error_msg 
37912  290 
fun collect_results f reports [] = (NONE, rev reports) 
291 
 collect_results f reports (t :: ts) = 

292 
case f t of 

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

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

40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

295 
in collect_results (test_term lthy generator_name) [] correct_inst_goals end; 
37912  296 

297 
(* pretty printing *) 

28315  298 

40225  299 
fun tool_name auto = (if auto then "Auto " else "") ^ "Quickcheck" 
300 

301 
fun pretty_counterex ctxt auto NONE = Pretty.str (tool_name auto ^ " found no counterexample.") 

302 
 pretty_counterex ctxt auto (SOME cex) = 

303 
Pretty.chunks (Pretty.str (tool_name auto ^ " found a counterexample:\n") :: 

28315  304 
map (fn (s, t) => 
305 
Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex); 

306 

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

307 
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

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

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

310 
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

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

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

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

314 
@ 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

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

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

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

318 

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

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

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

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

322 
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

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

324 

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

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

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

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

328 
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

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

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

331 

40225  332 
fun pretty_counterex_and_reports ctxt auto (cex, timing_and_reports) = 
333 
Pretty.chunks (pretty_counterex ctxt auto cex :: 

334 
map (pretty_reports ctxt) (map snd timing_and_reports)) 

28315  335 

336 
(* automatic testing *) 

28309  337 

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

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

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

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

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

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

343 
val ctxt = Proof.context_of state; 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

344 
val res = 
39253
0c47d615a69b
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn
parents:
39252
diff
changeset

345 
state 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

346 
> Proof.map_context (Context.proof_map (set_report false #> set_quiet true)) 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

347 
> try (test_goal NONE [] 1); 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

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

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

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

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

352 
 SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "", 
40225  353 
Pretty.mark Markup.hilite (pretty_counterex ctxt true cex)])) state) 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33560
diff
changeset

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

355 

39324
05452dd66b2b
finished renaming "Auto_Counterexample" to "Auto_Tools"
blanchet
parents:
39253
diff
changeset

356 
val setup = Auto_Tools.register_tool ("quickcheck", auto_quickcheck) 
28315  357 

358 

30980  359 
(* Isar commands *) 
28315  360 

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

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

364 
 (_, _ :: _) => 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

365 

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

366 
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

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

368 
 read_bool s = error ("Not a Boolean value: " ^ s) 
28315  369 

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

370 
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

371 
 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

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

373 
 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

374 

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

375 
fun parse_test_param ctxt ("size", [arg]) = 
28336  376 
(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

377 
 parse_test_param ctxt ("iterations", [arg]) = 
28336  378 
(apfst o apsnd o K) (read_nat arg) 
379 
 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

380 
(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

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

382 
(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

383 
 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

384 
(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

385 
 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

386 
(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

387 
 parse_test_param ctxt ("quiet", [arg]) = 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

388 
(apsnd o apsnd o apsnd o apfst o K) (read_bool arg) 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

389 
 parse_test_param ctxt ("timeout", [arg]) = 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

390 
(apsnd o apsnd o apsnd o apsnd o K) (read_nat arg) 
28336  391 
 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

392 
error ("Unknown test parameter: " ^ name); 
28315  393 

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

394 
fun parse_test_param_inst ctxt ("generator", [arg]) = 
28336  395 
(apsnd o apfst o K o SOME) arg 
396 
 parse_test_param_inst ctxt (name, arg) = 

397 
case try (ProofContext.read_typ ctxt) name 

398 
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

399 
(v, ProofContext.read_typ ctxt (the_single arg)) 
28336  400 
 _ => (apfst o parse_test_param ctxt) (name, arg); 
28309  401 

28336  402 
fun quickcheck_params_cmd args thy = 
28315  403 
let 
39252
8f176e575a49
changing the container for the quickcheck options to a generic data
bulwahn
parents:
39138
diff
changeset

404 
val ctxt = ProofContext.init_global thy 
28336  405 
val f = fold (parse_test_param ctxt) args; 
28315  406 
in 
407 
thy 

40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

408 
> (Context.theory_map o map_test_params) f 
28315  409 
end; 
410 

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

411 
fun gen_quickcheck args i state = 
28315  412 
let 
32297  413 
val ctxt = Proof.context_of state; 
39252
8f176e575a49
changing the container for the quickcheck options to a generic data
bulwahn
parents:
39138
diff
changeset

414 
val default_params = (dest_test_params o snd o Data.get o Context.Proof) ctxt; 
28336  415 
val f = fold (parse_test_param_inst ctxt) args; 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

416 
val (test_params, (generator_name, insts)) = f (default_params, (NONE, [])); 
32297  417 
in 
39253
0c47d615a69b
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn
parents:
39252
diff
changeset

418 
state 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

419 
> Proof.map_context (Context.proof_map (map_test_params (K test_params))) 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

420 
> (fn state' => test_goal generator_name insts i state' 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

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

422 
error ("quickcheck expected to find no counterexample but found one") else () 
40246
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

423 
 (NONE, _) => if expect (Proof.context_of state') = Counterexample then 
c03fc7d3fa97
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents:
40225
diff
changeset

424 
error ("quickcheck expected to find a counterexample but did not find one") else ())) 
32297  425 
end; 
426 

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

427 
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

428 

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

430 
gen_quickcheck args i (Toplevel.proof_of state) 
40225  431 
> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state) false; 
28309  432 

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

433 
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

434 
((Parse.name >> single)  (Parse.$$$ "["  Parse.list1 Parse.name  Parse.$$$ "]"))) ["true"]); 
28309  435 

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

436 
val parse_args = Parse.$$$ "["  Parse.list1 parse_arg  Parse.$$$ "]" 
28336  437 
 Scan.succeed []; 
438 

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

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

440 
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

441 
(parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args))); 
28309  442 

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

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

444 
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

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

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

28315  448 
end; 
28309  449 

450 

28315  451 
val auto_quickcheck = Quickcheck.auto; 