author  wenzelm 
Wed, 12 Jan 2011 14:13:04 +0100  
changeset 41517  7267fb5b724b 
parent 41472  f6ab14e61604 
child 41735  bd7ee90267f2 
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 
41517  13 
val tester : string Config.T 
40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

14 
val size : int Config.T 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

15 
val iterations : int Config.T 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

16 
val no_assms : bool Config.T 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

17 
val report : bool Config.T 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

18 
val quiet : bool Config.T 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

19 
val timeout : real Config.T 
40648
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

20 
val finite_types : bool Config.T 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

21 
val finite_type_size : int Config.T 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

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

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

24 
satisfied_assms : int list, positive_concl_tests : int } 
41517  25 
datatype expectation = No_Expectation  No_Counterexample  Counterexample; 
40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

26 
datatype test_params = Test_Params of {default_type: typ list, expect : expectation}; 
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

27 
val test_params_of : Proof.context > test_params 
40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

28 
val map_test_params : (typ list * expectation > typ list * expectation) 
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

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

30 
val add_generator: 
40911
7febf76e0a69
moving iteration of tests to the testers in quickcheck
bulwahn
parents:
40910
diff
changeset

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

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

33 
(* testing terms and proof states *) 
40909
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

34 
val test_term: Proof.context > bool > term > 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

35 
(string * term) list option * ((string * int) list * ((int * report) list) option) 
40648
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

36 
val test_goal_terms: 
40909
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

37 
Proof.context > bool > (string * typ) list > term list 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

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

39 
val quickcheck: (string * string list) list > int > Proof.state > (string * term) list option 
28256  40 
end; 
41 

42 
structure Quickcheck : QUICKCHECK = 

43 
struct 

44 

30980  45 
(* preferences *) 
46 

32740  47 
val auto = Unsynchronized.ref false; 
30980  48 

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

49 
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

50 

30980  51 
val _ = 
52 
ProofGeneralPgip.add_preference Preferences.category_tracing 

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

53 
(Unsynchronized.setmp auto true (fn () => 
30980  54 
Preferences.bool_pref auto 
55 
"autoquickcheck" 

39329  56 
"Run Quickcheck automatically.") ()); 
30980  57 

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

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

59 

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

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

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

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

63 

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

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

65 

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

67 

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

68 
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

69 
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

70 

28315  71 
(* quickcheck configuration  default parameters, test generators *) 
40908  72 
val (tester, setup_tester) = Attrib.config_string "quickcheck_tester" (K "") 
40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

73 
val (size, setup_size) = Attrib.config_int "quickcheck_size" (K 10) 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

74 
val (iterations, setup_iterations) = Attrib.config_int "quickcheck_iterations" (K 100) 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

75 
val (no_assms, setup_no_assms) = Attrib.config_bool "quickcheck_no_assms" (K false) 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

76 
val (report, setup_report) = Attrib.config_bool "quickcheck_report" (K true) 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

77 
val (quiet, setup_quiet) = Attrib.config_bool "quickcheck_quiet" (K false) 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

78 
val (timeout, setup_timeout) = Attrib.config_real "quickcheck_timeout" (K 30.0) 
40646  79 
val (finite_types, setup_finite_types) = Attrib.config_bool "quickcheck_finite_types" (K true) 
41517  80 
val (finite_type_size, setup_finite_type_size) = 
81 
Attrib.config_int "quickcheck_finite_type_size" (K 3) 

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

82 

40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

83 
val setup_config = 
40908  84 
setup_tester #> setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_quiet 
85 
#> setup_timeout #> setup_finite_types #> setup_finite_type_size 

40646  86 

40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

87 
datatype test_params = Test_Params of 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

88 
{default_type: typ list, expect : expectation}; 
38759
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38390
diff
changeset

89 

40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

90 
fun dest_test_params (Test_Params {default_type, expect}) = (default_type, expect); 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

91 

41517  92 
fun make_test_params (default_type, expect) = 
93 
Test_Params {default_type = default_type, expect = expect}; 

40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

94 

41517  95 
fun map_test_params' f (Test_Params {default_type, expect}) = 
96 
make_test_params (f (default_type, expect)); 

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

97 

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

98 
fun merge_test_params 
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41086
diff
changeset

99 
(Test_Params {default_type = default_type1, expect = expect1}, 
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41086
diff
changeset

100 
Test_Params {default_type = default_type2, expect = expect2}) = 
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41086
diff
changeset

101 
make_test_params 
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41086
diff
changeset

102 
(merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2)); 
28309  103 

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

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

106 
type T = 
40911
7febf76e0a69
moving iteration of tests to the testers in quickcheck
bulwahn
parents:
40910
diff
changeset

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

108 
* test_params; 
40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

109 
val empty = ([], Test_Params {default_type = [], expect = No_Expectation}); 
28256  110 
val extend = I; 
33522  111 
fun merge ((generators1, params1), (generators2, params2)) : T = 
112 
(AList.merge (op =) (K true) (generators1, generators2), 

28309  113 
merge_test_params (params1, params2)); 
33522  114 
); 
28256  115 

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

116 
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

117 

40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

118 
val default_type = fst o dest_test_params o test_params_of 
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

119 

40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

120 
val expect = snd o dest_test_params o test_params_of 
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

121 

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

122 
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

123 

28309  124 
val add_generator = Data.map o apfst o AList.update (op =); 
125 

28315  126 
(* generating tests *) 
127 

40909
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

128 
fun mk_tester ctxt t = 
28309  129 
let 
40909
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

130 
val name = Config.get ctxt tester 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

131 
val tester = case AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) name 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

132 
of NONE => error ("No such quickcheck tester: " ^ name) 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

133 
 SOME tester => tester ctxt; 
40235
87998864284e
use Exn.interruptible_capture to keep usercode interruptible (Exn.capture not immediately followed by Exn.release here);
wenzelm
parents:
40225
diff
changeset

134 
in 
40909
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

135 
if Config.get ctxt quiet then 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

136 
try tester t 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

137 
else 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

138 
let 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

139 
val tester = Exn.interruptible_capture tester t 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

140 
in case Exn.get_result tester of 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

141 
NONE => SOME (Exn.release tester) 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

142 
 SOME tester => SOME tester 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

143 
end 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

144 
end 
28315  145 

146 
(* testing propositions *) 

147 

28309  148 
fun prep_test_term t = 
149 
let 

29266  150 
val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse 
28309  151 
error "Term to be tested contains type variables"; 
29266  152 
val _ = null (Term.add_vars t []) orelse 
28309  153 
error "Term to be tested contains schematic variables"; 
31138  154 
val frees = Term.add_frees t []; 
41086
b4cccce25d9a
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents:
41043
diff
changeset

155 
in (frees, list_abs_free (frees, t)) end 
28256  156 

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

158 
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

159 
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

160 
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

161 
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

162 
in (Exn.release result, (description, time)) end 
41517  163 

40909
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

164 
fun test_term ctxt is_interactive t = 
28309  165 
let 
41086
b4cccce25d9a
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents:
41043
diff
changeset

166 
val (names, t') = apfst (map fst) (prep_test_term t); 
40366
a2866dbfbe6b
changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents:
40253
diff
changeset

167 
val current_size = Unsynchronized.ref 0 
a2866dbfbe6b
changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents:
40253
diff
changeset

168 
fun excipit s = 
a2866dbfbe6b
changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents:
40253
diff
changeset

169 
"Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size) 
40909
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

170 
val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt t'); 
40911
7febf76e0a69
moving iteration of tests to the testers in quickcheck
bulwahn
parents:
40910
diff
changeset

171 
fun with_size test_fun k reports = 
7febf76e0a69
moving iteration of tests to the testers in quickcheck
bulwahn
parents:
40910
diff
changeset

172 
if k > Config.get ctxt size then 
7febf76e0a69
moving iteration of tests to the testers in quickcheck
bulwahn
parents:
40910
diff
changeset

173 
(NONE, reports) 
7febf76e0a69
moving iteration of tests to the testers in quickcheck
bulwahn
parents:
40910
diff
changeset

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

175 
let 
40911
7febf76e0a69
moving iteration of tests to the testers in quickcheck
bulwahn
parents:
40910
diff
changeset

176 
val _ = if Config.get ctxt quiet then () else Output.urgent_message 
7febf76e0a69
moving iteration of tests to the testers in quickcheck
bulwahn
parents:
40910
diff
changeset

177 
("Test data size: " ^ string_of_int k) 
40648
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

178 
val _ = current_size := k 
40911
7febf76e0a69
moving iteration of tests to the testers in quickcheck
bulwahn
parents:
40910
diff
changeset

179 
val ((result, new_report), timing) = 
7febf76e0a69
moving iteration of tests to the testers in quickcheck
bulwahn
parents:
40910
diff
changeset

180 
cpu_time ("size " ^ string_of_int k) (fn () => test_fun (k  1)) 
7febf76e0a69
moving iteration of tests to the testers in quickcheck
bulwahn
parents:
40910
diff
changeset

181 
val reports = case new_report of NONE => reports  SOME rep => (k, rep) :: reports 
41517  182 
in 
183 
case result of NONE => with_size test_fun (k + 1) reports  SOME q => (SOME q, reports) 

184 
end; 

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

185 
in 
41517  186 
case test_fun of NONE => (NONE, ([comp_time], NONE)) 
40909
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

187 
 SOME test_fun => 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

188 
TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () => 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

189 
let 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

190 
val ((result, reports), exec_time) = 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

191 
cpu_time "quickcheck execution" (fn () => with_size test_fun 1 []) 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

192 
in 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

193 
(case result of NONE => NONE  SOME ts => SOME (names ~~ ts), 
40916  194 
([exec_time, comp_time], 
195 
if Config.get ctxt report andalso not (null reports) then SOME reports else NONE)) 

40909
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

196 
end) () 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

197 
handle TimeLimit.TimeOut => 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

198 
if is_interactive then error (excipit "ran out of time") else raise TimeLimit.TimeOut 
28309  199 
end; 
200 

41086
b4cccce25d9a
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents:
41043
diff
changeset

201 
(* FIXME: this function shows that many assumptions are made upon the generation *) 
b4cccce25d9a
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents:
41043
diff
changeset

202 
(* In the end there is probably no generic quickcheck interface left... *) 
b4cccce25d9a
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents:
41043
diff
changeset

203 

41043
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

204 
fun test_term_with_increasing_cardinality ctxt is_interactive ts = 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

205 
let 
41086
b4cccce25d9a
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents:
41043
diff
changeset

206 
val thy = ProofContext.theory_of ctxt 
b4cccce25d9a
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents:
41043
diff
changeset

207 
val (freess, ts') = split_list (map prep_test_term ts) 
b4cccce25d9a
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents:
41043
diff
changeset

208 
val Ts = map snd (hd freess) 
41043
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

209 
val (test_funs, comp_time) = cpu_time "quickcheck compilation" 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

210 
(fn () => map (mk_tester ctxt) ts') 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

211 
fun test_card_size (card, size) = 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

212 
(* FIXME: why decrement size by one? *) 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

213 
case fst (the (nth test_funs (card  1)) (size  1)) of 
41086
b4cccce25d9a
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents:
41043
diff
changeset

214 
SOME ts => SOME (map fst (nth freess (card  1)) ~~ ts) 
41043
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

215 
 NONE => NONE 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

216 
val enumeration_card_size = 
41086
b4cccce25d9a
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents:
41043
diff
changeset

217 
if forall (fn T => Sign.of_sort thy (T, ["Enum.enum"])) Ts then 
b4cccce25d9a
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents:
41043
diff
changeset

218 
(* size does not matter *) 
b4cccce25d9a
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents:
41043
diff
changeset

219 
map (rpair 0) (1 upto (length ts)) 
b4cccce25d9a
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents:
41043
diff
changeset

220 
else 
b4cccce25d9a
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents:
41043
diff
changeset

221 
(* size does matter *) 
b4cccce25d9a
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents:
41043
diff
changeset

222 
map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt size)) 
b4cccce25d9a
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents:
41043
diff
changeset

223 
> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2))) 
41043
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

224 
in 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

225 
if (forall is_none test_funs) then 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

226 
(NONE, ([comp_time], NONE)) 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

227 
else if (forall is_some test_funs) then 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

228 
TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () => 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

229 
(get_first test_card_size enumeration_card_size, ([comp_time], NONE))) () 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

230 
handle TimeLimit.TimeOut => 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

231 
if is_interactive then error ("Quickcheck ran out of time") else raise TimeLimit.TimeOut 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

232 
else 
41517  233 
error "Unexpectedly, testers of some cardinalities are executable but others are not" 
41043
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

234 
end 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

235 

40647  236 
fun get_finite_types ctxt = 
237 
fst (chop (Config.get ctxt finite_type_size) 

238 
(map (Type o rpair []) ["Enum.finite_1", "Enum.finite_2", "Enum.finite_3", 

41517  239 
"Enum.finite_4", "Enum.finite_5"])) 
40647  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 

41517  243 
fun monomorphic_term thy insts default_T = 
28309  244 
let 
245 
fun subst (T as TFree (v, S)) = 

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

248 
> the_default default_T 

249 
in if Sign.of_sort thy (T', S) then T' 

41517  250 
else raise (WELLSORTED ("For instantiation with default_type " ^ 
251 
Syntax.string_of_typ_global thy default_T ^ 

40903  252 
":\n" ^ Syntax.string_of_typ_global thy T' ^ 
253 
" to be substituted for variable " ^ 

254 
Syntax.string_of_typ_global thy T ^ " does not have sort " ^ 

255 
Syntax.string_of_sort_global thy S)) 

256 
end 

28309  257 
 subst T = T; 
258 
in (map_types o map_atyps) subst end; 

259 

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

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

261 

40909
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

262 
fun test_goal_terms lthy is_interactive insts check_goals = 
28309  263 
let 
41517  264 
val thy = ProofContext.theory_of lthy 
40926
c600f6ae4b09
only instantiate type variable if there exists some in quickcheck
bulwahn
parents:
40916
diff
changeset

265 
val default_insts = 
c600f6ae4b09
only instantiate type variable if there exists some in quickcheck
bulwahn
parents:
40916
diff
changeset

266 
if Config.get lthy finite_types then (get_finite_types lthy) else (default_type lthy) 
40647  267 
val inst_goals = 
41043
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

268 
map (fn check_goal => 
40926
c600f6ae4b09
only instantiate type variable if there exists some in quickcheck
bulwahn
parents:
40916
diff
changeset

269 
if not (null (Term.add_tfree_names check_goal [])) then 
c600f6ae4b09
only instantiate type variable if there exists some in quickcheck
bulwahn
parents:
40916
diff
changeset

270 
map (fn T => 
41517  271 
(pair (SOME T) o Term o Object_Logic.atomize_term thy o monomorphic_term thy insts T) 
272 
check_goal 

41043
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

273 
handle WELLSORTED s => (SOME T, Wellsorted_Error s)) default_insts 
40926
c600f6ae4b09
only instantiate type variable if there exists some in quickcheck
bulwahn
parents:
40916
diff
changeset

274 
else 
41043
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

275 
[(NONE, Term (Object_Logic.atomize_term thy check_goal))]) check_goals 
41517  276 
val error_msg = 
277 
cat_lines 

278 
(maps (map_filter (fn (_, Term t) => NONE  (_, Wellsorted_Error s) => SOME s)) inst_goals) 

41043
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

279 
fun is_wellsorted_term (T, Term t) = SOME (T, t) 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

280 
 is_wellsorted_term (_, Wellsorted_Error s) = NONE 
37913
e85f5ad02a8f
correcting wellsortedness check and improving error message
bulwahn
parents:
37912
diff
changeset

281 
val correct_inst_goals = 
41043
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

282 
case map (map_filter is_wellsorted_term) inst_goals of 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

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

284 
 xs => xs 
40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

285 
val _ = if Config.get lthy quiet then () else warning error_msg 
37912  286 
fun collect_results f reports [] = (NONE, rev reports) 
287 
 collect_results f reports (t :: ts) = 

288 
case f t of 

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

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

41043
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

291 
fun test_term' goal = 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

292 
case goal of 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

293 
[(NONE, t)] => test_term lthy is_interactive t 
41517  294 
 ts => test_term_with_increasing_cardinality lthy is_interactive (map snd ts) 
41043
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

295 
in 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

296 
if Config.get lthy finite_types then 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

297 
collect_results test_term' [] correct_inst_goals 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

298 
else 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

299 
collect_results (test_term lthy is_interactive) [] (maps (map snd) correct_inst_goals) 
3750bdac1327
testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents:
40931
diff
changeset

300 
end; 
37912  301 

40909
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

302 
fun test_goal insts i state = 
40648
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

303 
let 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

304 
val lthy = Proof.context_of state; 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

305 
val thy = Proof.theory_of state; 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

306 
fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

307 
 strip t = t; 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

308 
val {goal = st, ...} = Proof.raw_goal state; 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

309 
val (gi, frees) = Logic.goal_params (prop_of st) i; 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

310 
val some_locale = case (Option.map #target o Named_Target.peek) lthy 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

311 
of NONE => NONE 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

312 
 SOME "" => NONE 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

313 
 SOME locale => SOME locale; 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

314 
val assms = if Config.get lthy no_assms then [] else case some_locale 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

315 
of NONE => Assumption.all_assms_of lthy 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

316 
 SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy); 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

317 
val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi)); 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

318 
val check_goals = case some_locale 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

319 
of NONE => [proto_goal] 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

320 
 SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal) 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

321 
(Locale.registrations_of (Context.Theory thy) (*FIXME*) locale); 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

322 
in 
40909
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

323 
test_goal_terms lthy true insts check_goals 
40648
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

324 
end 
1598ec648b0d
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents:
40647
diff
changeset

325 

37912  326 
(* pretty printing *) 
28315  327 

40225  328 
fun tool_name auto = (if auto then "Auto " else "") ^ "Quickcheck" 
329 

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

331 
 pretty_counterex ctxt auto (SOME cex) = 

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

28315  333 
map (fn (s, t) => 
40916  334 
Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex)); 
28315  335 

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

336 
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

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

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

339 
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

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

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

342 
pretty_stat "match exceptions" raised_match_errors] 
41517  343 
@ map_index 
344 
(fn (i, n) => pretty_stat ("satisfied " ^ string_of_int (i + 1) ^ ". assumption") n) 

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

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

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

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

348 

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

349 
fun pretty_reports ctxt (SOME reports) = 
40916  350 
Pretty.chunks (Pretty.fbrk :: Pretty.str "Quickcheck report:" :: 
40909
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

351 
maps (fn (size, report) => 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

352 
Pretty.str ("size " ^ string_of_int size ^ ":") :: pretty_report report @ [Pretty.brk 1]) 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35324
diff
changeset

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

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

355 

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

358 
map (pretty_reports ctxt) (map snd timing_and_reports)) 

28315  359 

360 
(* automatic testing *) 

28309  361 

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

362 
fun auto_quickcheck state = 
40931  363 
let 
364 
val ctxt = Proof.context_of state; 

365 
val res = 

366 
state 

367 
> Proof.map_context (Config.put report false #> Config.put quiet true) 

368 
> try (test_goal [] 1); 

369 
in 

370 
case res of 

371 
NONE => (false, state) 

372 
 SOME (NONE, report) => (false, state) 

373 
 SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "", 

374 
Pretty.mark Markup.hilite (pretty_counterex ctxt true cex)])) state) 

375 
end 

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

376 

40931  377 
val setup = Auto_Tools.register_tool (auto, auto_quickcheck) 
40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

378 
#> setup_config 
28315  379 

30980  380 
(* Isar commands *) 
28315  381 

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

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

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

386 

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

387 
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

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

389 
 read_bool s = error ("Not a Boolean value: " ^ s) 
28315  390 

40366
a2866dbfbe6b
changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents:
40253
diff
changeset

391 
fun read_real s = 
a2866dbfbe6b
changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents:
40253
diff
changeset

392 
case (Real.fromString s) of 
a2866dbfbe6b
changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents:
40253
diff
changeset

393 
SOME s => s 
a2866dbfbe6b
changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents:
40253
diff
changeset

394 
 NONE => error ("Not a real number: " ^ s) 
a2866dbfbe6b
changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents:
40253
diff
changeset

395 

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

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

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

400 

40912
1108529100ce
checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents:
40911
diff
changeset

401 
fun valid_tester_name genctxt = AList.defined (op =) (fst (Data.get genctxt)) 
1108529100ce
checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents:
40911
diff
changeset

402 

1108529100ce
checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents:
40911
diff
changeset

403 
fun parse_tester name genctxt = 
1108529100ce
checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents:
40911
diff
changeset

404 
if valid_tester_name genctxt name then 
1108529100ce
checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents:
40911
diff
changeset

405 
Config.put_generic tester name genctxt 
1108529100ce
checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents:
40911
diff
changeset

406 
else 
1108529100ce
checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents:
40911
diff
changeset

407 
error ("Unknown tester: " ^ name) 
1108529100ce
checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents:
40911
diff
changeset

408 

1108529100ce
checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents:
40911
diff
changeset

409 
fun parse_test_param ("tester", [arg]) = parse_tester arg 
40909
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

410 
 parse_test_param ("size", [arg]) = Config.put_generic size (read_nat arg) 
40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

411 
 parse_test_param ("iterations", [arg]) = Config.put_generic iterations (read_nat arg) 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

412 
 parse_test_param ("default_type", arg) = (fn gen_ctxt => 
41517  413 
map_test_params 
414 
((apfst o K) (map (ProofContext.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt) 

40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

415 
 parse_test_param ("no_assms", [arg]) = Config.put_generic no_assms (read_bool arg) 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

416 
 parse_test_param ("expect", [arg]) = map_test_params ((apsnd o K) (read_expectation arg)) 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

417 
 parse_test_param ("report", [arg]) = Config.put_generic report (read_bool arg) 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

418 
 parse_test_param ("quiet", [arg]) = Config.put_generic quiet (read_bool arg) 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

419 
 parse_test_param ("timeout", [arg]) = Config.put_generic timeout (read_real arg) 
40646  420 
 parse_test_param ("finite_types", [arg]) = Config.put_generic finite_types (read_bool arg) 
41517  421 
 parse_test_param ("finite_type_size", [arg]) = 
422 
Config.put_generic finite_type_size (read_nat arg) 

40912
1108529100ce
checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents:
40911
diff
changeset

423 
 parse_test_param (name, _) = fn genctxt => 
1108529100ce
checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents:
40911
diff
changeset

424 
if valid_tester_name genctxt name then 
1108529100ce
checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents:
40911
diff
changeset

425 
Config.put_generic tester name genctxt 
1108529100ce
checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents:
40911
diff
changeset

426 
else error ("Unknown tester or test parameter: " ^ name); 
28315  427 

40909
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

428 
fun parse_test_param_inst (name, arg) (insts, ctxt) = 
28336  429 
case try (ProofContext.read_typ ctxt) name 
40909
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

430 
of SOME (TFree (v, _)) => (apfst o AList.update (op =)) 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

431 
(v, ProofContext.read_typ ctxt (the_single arg)) (insts, ctxt) 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

432 
 _ => (apsnd o Context.proof_map o parse_test_param) (name, arg) (insts, ctxt); 
28309  433 

40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

434 
fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args); 
41517  435 

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

436 
fun gen_quickcheck args i state = 
40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

437 
state 
40909
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

438 
> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args ([], ctxt)) 
e006d1e06920
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents:
40908
diff
changeset

439 
> (fn (insts, state') => test_goal insts i state' 
40644
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

440 
> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

441 
error ("quickcheck expected to find no counterexample but found one") else () 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

442 
 (NONE, _) => if expect (Proof.context_of state') = Counterexample then 
0850a2a16dce
changed oldstyle quickcheck configurations to new Config.T configurations
bulwahn
parents:
40643
diff
changeset

443 
error ("quickcheck expected to find a counterexample but did not find one") else ())) 
32297  444 

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

445 
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

446 

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

448 
gen_quickcheck args i (Toplevel.proof_of state) 
40225  449 
> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state) false; 
28309  450 

41517  451 
val parse_arg = 
452 
Parse.name  

453 
(Scan.optional (Parse.$$$ "="  

454 
(((Parse.name  Parse.float_number) >> single)  

455 
(Parse.$$$ "["  Parse.list1 Parse.name  Parse.$$$ "]"))) ["true"]); 

28309  456 

41517  457 
val parse_args = 
458 
Parse.$$$ "["  Parse.list1 parse_arg  Parse.$$$ "]"  Scan.succeed []; 

28336  459 

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

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

461 
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

462 
(parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args))); 
28309  463 

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

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

465 
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

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

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

28315  469 
end; 
28309  470 

471 

28315  472 
val auto_quickcheck = Quickcheck.auto; 