author  wenzelm 
Fri, 17 Jan 2020 16:59:32 +0100  
changeset 71394  933ad2385480 
parent 70308  7f568724d67e 
permissions  rwrr 
41923
f05fc0711bc7
renaming signatures and structures; correcting header
bulwahn
parents:
41920
diff
changeset

1 
(* Title: HOL/Tools/Quickcheck/exhaustive_generators.ML 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

2 
Author: Lukas Bulwahn, TU Muenchen 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

3 

41918  4 
Exhaustive generators for various types. 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

5 
*) 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

6 

41918  7 
signature EXHAUSTIVE_GENERATORS = 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

8 
sig 
62979  9 
val compile_generator_expr: Proof.context > (term * term list) list > bool > int list > 
10 
(bool * term list) option * Quickcheck.report option 

42159
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset

11 
val compile_generator_exprs: Proof.context > term list > (int > term list option) list 
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset

12 
val compile_validator_exprs: Proof.context > term list > (int > bool) list 
62979  13 
val put_counterexample: 
14 
(unit > Code_Numeral.natural > bool > Code_Numeral.natural > (bool * term list) option) > 

15 
Proof.context > Proof.context 

16 
val put_counterexample_batch: (unit > (Code_Numeral.natural > term list option) list) > 

17 
Proof.context > Proof.context 

18 
val put_validator_batch: (unit > (Code_Numeral.natural > bool) list) > 

19 
Proof.context > Proof.context 

42306  20 
exception Counterexample of term list 
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset

21 
val smart_quantifier : bool Config.T 
48013
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
46565
diff
changeset

22 
val optimise_equality : bool Config.T 
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset

23 
val quickcheck_pretty : bool Config.T 
45484
23871e17dddb
setting up exhaustive generators which are used for the smart generators
bulwahn
parents:
45420
diff
changeset

24 
val setup_exhaustive_datatype_interpretation : theory > theory 
48178
0192811f0a96
exporting important function for the "many conjecture refutation" compilation of quickcheck
bulwahn
parents:
48013
diff
changeset

25 
val setup_bounded_forall_datatype_interpretation : theory > theory 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57996
diff
changeset

26 
val instantiate_full_exhaustive_datatype : Old_Datatype_Aux.config > Old_Datatype_Aux.descr > 
62979  27 
(string * sort) list > string list > string > string list * string list > 
28 
typ list * typ list > theory > theory 

58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57996
diff
changeset

29 
val instantiate_exhaustive_datatype : Old_Datatype_Aux.config > Old_Datatype_Aux.descr > 
62979  30 
(string * sort) list > string list > string > string list * string list > 
31 
typ list * typ list > theory > theory 

32 
end 

40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

33 

41918  34 
structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS = 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

35 
struct 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

36 

42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

37 
(* basics *) 
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

38 

e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

39 
(** dynamic options **) 
40907  40 

67149  41 
val smart_quantifier = Attrib.setup_config_bool \<^binding>\<open>quickcheck_smart_quantifier\<close> (K true) 
42 
val optimise_equality = Attrib.setup_config_bool \<^binding>\<open>quickcheck_optimise_equality\<close> (K true) 

48013
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
46565
diff
changeset

43 

67149  44 
val fast = Attrib.setup_config_bool \<^binding>\<open>quickcheck_fast\<close> (K false) 
45 
val bounded_forall = Attrib.setup_config_bool \<^binding>\<open>quickcheck_bounded_forall\<close> (K false) 

46 
val full_support = Attrib.setup_config_bool \<^binding>\<open>quickcheck_full_support\<close> (K true) 

47 
val quickcheck_pretty = Attrib.setup_config_bool \<^binding>\<open>quickcheck_pretty\<close> (K true) 

62979  48 

40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

49 

552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

50 
(** abstract syntax **) 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

51 

67149  52 
fun termifyT T = HOLogic.mk_prodT (T, \<^typ>\<open>unit \<Rightarrow> Code_Evaluation.term\<close>) 
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset

53 

67149  54 
val size = \<^term>\<open>i :: natural\<close> 
55 
val size_pred = \<^term>\<open>(i :: natural)  1\<close> 

56 
val size_ge_zero = \<^term>\<open>(i :: natural) > 0\<close> 

42304  57 

40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

58 
fun mk_none_continuation (x, y) = 
67149  59 
let val (T as Type (\<^type_name>\<open>option\<close>, _)) = fastype_of x 
60 
in Const (\<^const_name>\<open>orelse\<close>, T > T > T) $ x $ y end 

40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

61 

45721
d1fb55c2ed65
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents:
45718
diff
changeset

62 
fun mk_if (b, t, e) = 
62979  63 
let val T = fastype_of t 
67149  64 
in Const (\<^const_name>\<open>If\<close>, \<^typ>\<open>bool\<close> > T > T > T) $ b $ t $ e end 
62979  65 

45721
d1fb55c2ed65
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents:
45718
diff
changeset

66 

42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

67 
(* handling inductive datatypes *) 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

68 

42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

69 
(** constructing generator instances **) 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

70 

62979  71 
exception FUNCTION_TYPE 
42306  72 

73 
exception Counterexample of term list 

74 

67149  75 
val resultT = \<^typ>\<open>(bool \<times> term list) option\<close> 
45722  76 

62979  77 
val exhaustiveN = "exhaustive" 
78 
val full_exhaustiveN = "full_exhaustive" 

79 
val bounded_forallN = "bounded_forall" 

42306  80 

67149  81 
fun fast_exhaustiveT T = (T > \<^typ>\<open>unit\<close>) > \<^typ>\<open>natural\<close> > \<^typ>\<open>unit\<close> 
42306  82 

67149  83 
fun exhaustiveT T = (T > resultT) > \<^typ>\<open>natural\<close> > resultT 
42304  84 

67149  85 
fun bounded_forallT T = (T > \<^typ>\<open>bool\<close>) > \<^typ>\<open>natural\<close> > \<^typ>\<open>bool\<close> 
42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

86 

67149  87 
fun full_exhaustiveT T = (termifyT T > resultT) > \<^typ>\<open>natural\<close> > resultT 
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40913
diff
changeset

88 

45722  89 
fun check_allT T = (termifyT T > resultT) > resultT 
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40913
diff
changeset

90 

42307
72e2fabb4bc2
creating a general mk_equation_terms for the different compilations
bulwahn
parents:
42306
diff
changeset

91 
fun mk_equation_terms generics (descr, vs, Ts) = 
72e2fabb4bc2
creating a general mk_equation_terms for the different compilations
bulwahn
parents:
42306
diff
changeset

92 
let 
72e2fabb4bc2
creating a general mk_equation_terms for the different compilations
bulwahn
parents:
42306
diff
changeset

93 
val (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, exhaustives) = generics 
72e2fabb4bc2
creating a general mk_equation_terms for the different compilations
bulwahn
parents:
42306
diff
changeset

94 
val rhss = 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57996
diff
changeset

95 
Old_Datatype_Aux.interpret_construction descr vs 
42307
72e2fabb4bc2
creating a general mk_equation_terms for the different compilations
bulwahn
parents:
42306
diff
changeset

96 
{ atyp = mk_call, dtyp = mk_aux_call } 
72e2fabb4bc2
creating a general mk_equation_terms for the different compilations
bulwahn
parents:
42306
diff
changeset

97 
> (map o apfst) Type 
72e2fabb4bc2
creating a general mk_equation_terms for the different compilations
bulwahn
parents:
42306
diff
changeset

98 
> map (fn (T, cs) => map (mk_consexpr T) cs) 
72e2fabb4bc2
creating a general mk_equation_terms for the different compilations
bulwahn
parents:
42306
diff
changeset

99 
> map mk_rhs 
72e2fabb4bc2
creating a general mk_equation_terms for the different compilations
bulwahn
parents:
42306
diff
changeset

100 
val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives Ts 
62979  101 
in map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss) end 
42306  102 

44241  103 
fun gen_mk_call c T = (T, fn t => c T $ absdummy T t $ size_pred) 
42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

104 

e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

105 
fun gen_mk_aux_call functerms fTs (k, _) (tyco, Ts) = 
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

106 
let 
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

107 
val T = Type (tyco, Ts) 
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

108 
val _ = if not (null fTs) then raise FUNCTION_TYPE else () 
62979  109 
in (T, fn t => nth functerms k $ absdummy T t $ size_pred) end 
42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

110 

46306  111 
fun gen_mk_consexpr test_function simpleT (c, xs) = 
42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

112 
let 
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

113 
val (Ts, fns) = split_list xs 
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

114 
val constr = Const (c, Ts > simpleT) 
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

115 
val bounds = map Bound (((length xs)  1) downto 0) 
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

116 
val start_term = test_function simpleT $ list_comb (constr, bounds) 
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

117 
in fold_rev (fn f => fn t => f t) fns start_term end 
42307
72e2fabb4bc2
creating a general mk_equation_terms for the different compilations
bulwahn
parents:
42306
diff
changeset

118 

72e2fabb4bc2
creating a general mk_equation_terms for the different compilations
bulwahn
parents:
42306
diff
changeset

119 
fun mk_equations functerms = 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

120 
let 
45724
1f5fc44254d7
the simple exhaustive compilation also indicates if counterexample is potentially spurious;
bulwahn
parents:
45722
diff
changeset

121 
fun test_function T = Free ("f", T > resultT) 
67149  122 
val mk_call = gen_mk_call (fn T => Const (\<^const_name>\<open>exhaustive\<close>, exhaustiveT T)) 
42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

123 
val mk_aux_call = gen_mk_aux_call functerms 
46306  124 
val mk_consexpr = gen_mk_consexpr test_function 
42304  125 
fun mk_rhs exprs = 
67149  126 
mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (\<^const_name>\<open>None\<close>, resultT)) 
62979  127 
in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end 
42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

128 

e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

129 
fun mk_bounded_forall_equations functerms = 
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

130 
let 
67149  131 
fun test_function T = Free ("P", T > \<^typ>\<open>bool\<close>) 
132 
val mk_call = gen_mk_call (fn T => Const (\<^const_name>\<open>bounded_forall\<close>, bounded_forallT T)) 

42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

133 
val mk_aux_call = gen_mk_aux_call functerms 
46306  134 
val mk_consexpr = gen_mk_consexpr test_function 
67149  135 
fun mk_rhs exprs = mk_if (size_ge_zero, foldr1 HOLogic.mk_conj exprs, \<^term>\<open>True\<close>) 
62979  136 
in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end 
137 

42307
72e2fabb4bc2
creating a general mk_equation_terms for the different compilations
bulwahn
parents:
42306
diff
changeset

138 
fun mk_full_equations functerms = 
42304  139 
let 
45722  140 
fun test_function T = Free ("f", termifyT T > resultT) 
62979  141 
fun case_prod_const T = 
67149  142 
HOLogic.case_prod_const (T, \<^typ>\<open>unit \<Rightarrow> Code_Evaluation.term\<close>, resultT) 
42304  143 
fun mk_call T = 
144 
let 

67149  145 
val full_exhaustive = Const (\<^const_name>\<open>full_exhaustive\<close>, full_exhaustiveT T) 
62979  146 
in 
147 
(T, 

148 
fn t => 

149 
full_exhaustive $ 

67149  150 
(case_prod_const T $ absdummy T (absdummy \<^typ>\<open>unit \<Rightarrow> Code_Evaluation.term\<close> t)) $ 
62979  151 
size_pred) 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

152 
end 
41918  153 
fun mk_aux_call fTs (k, _) (tyco, Ts) = 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

154 
let 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

155 
val T = Type (tyco, Ts) 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

156 
val _ = if not (null fTs) then raise FUNCTION_TYPE else () 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

157 
in 
62979  158 
(T, 
159 
fn t => 

160 
nth functerms k $ 

67149  161 
(case_prod_const T $ absdummy T (absdummy \<^typ>\<open>unit \<Rightarrow> Code_Evaluation.term\<close> t)) $ 
62979  162 
size_pred) 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

163 
end 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

164 
fun mk_consexpr simpleT (c, xs) = 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

165 
let 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

166 
val (Ts, fns) = split_list xs 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

167 
val constr = Const (c, Ts > simpleT) 
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset

168 
val bounds = map (fn x => Bound (2 * x + 1)) (((length xs)  1) downto 0) 
56257  169 
val Eval_App = 
67149  170 
Const (\<^const_name>\<open>Code_Evaluation.App\<close>, 
62979  171 
HOLogic.termT > HOLogic.termT > HOLogic.termT) 
56257  172 
val Eval_Const = 
67149  173 
Const (\<^const_name>\<open>Code_Evaluation.Const\<close>, 
174 
HOLogic.literalT > \<^typ>\<open>typerep\<close> > HOLogic.termT) 

62979  175 
val term = 
67149  176 
fold (fn u => fn t => Eval_App $ t $ (u $ \<^term>\<open>()\<close>)) 
62979  177 
bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts > simpleT)) 
178 
val start_term = 

179 
test_function simpleT $ 

67149  180 
(HOLogic.pair_const simpleT \<^typ>\<open>unit \<Rightarrow> Code_Evaluation.term\<close> $ 
181 
(list_comb (constr, bounds)) $ absdummy \<^typ>\<open>unit\<close> term) 

40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

182 
in fold_rev (fn f => fn t => f t) fns start_term end 
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

183 
fun mk_rhs exprs = 
67149  184 
mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (\<^const_name>\<open>None\<close>, resultT)) 
62979  185 
in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end 
186 

40901
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset

187 

42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

188 
(** instantiating generator classes **) 
62979  189 

42325  190 
fun contains_recursive_type_under_function_types xs = 
42312
5bf3b9612e43
ensuring datatype limitations before the instantiation in quickcheck_exhaustive
bulwahn
parents:
42310
diff
changeset

191 
exists (fn (_, (_, _, cs)) => cs > exists (snd #> exists (fn dT => 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57996
diff
changeset

192 
(case Old_Datatype_Aux.strip_dtyp dT of (_ :: _, Old_Datatype_Aux.DtRec _) => true  _ => false)))) xs 
62979  193 

42315
95dfa082065a
generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents:
42314
diff
changeset

194 
fun instantiate_datatype (name, constprfx, sort, mk_equations, mk_T, argnames) 
95dfa082065a
generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents:
42314
diff
changeset

195 
config descr vs tycos prfx (names, auxnames) (Ts, Us) thy = 
42312
5bf3b9612e43
ensuring datatype limitations before the instantiation in quickcheck_exhaustive
bulwahn
parents:
42310
diff
changeset

196 
if not (contains_recursive_type_under_function_types descr) then 
5bf3b9612e43
ensuring datatype limitations before the instantiation in quickcheck_exhaustive
bulwahn
parents:
42310
diff
changeset

197 
let 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57996
diff
changeset

198 
val _ = Old_Datatype_Aux.message config ("Creating " ^ name ^ "...") 
42315
95dfa082065a
generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents:
42314
diff
changeset

199 
val fullnames = map (prefix (constprfx ^ "_")) (names @ auxnames) 
42312
5bf3b9612e43
ensuring datatype limitations before the instantiation in quickcheck_exhaustive
bulwahn
parents:
42310
diff
changeset

200 
in 
5bf3b9612e43
ensuring datatype limitations before the instantiation in quickcheck_exhaustive
bulwahn
parents:
42310
diff
changeset

201 
thy 
42315
95dfa082065a
generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents:
42314
diff
changeset

202 
> Class.instantiation (tycos, vs, sort) 
42312
5bf3b9612e43
ensuring datatype limitations before the instantiation in quickcheck_exhaustive
bulwahn
parents:
42310
diff
changeset

203 
> Quickcheck_Common.define_functions 
42315
95dfa082065a
generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents:
42314
diff
changeset

204 
(fn functerms => mk_equations functerms (descr, vs, Ts @ Us), NONE) 
95dfa082065a
generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents:
42314
diff
changeset

205 
prfx argnames fullnames (map mk_T (Ts @ Us)) 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59154
diff
changeset

206 
> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) 
42312
5bf3b9612e43
ensuring datatype limitations before the instantiation in quickcheck_exhaustive
bulwahn
parents:
42310
diff
changeset

207 
end 
5bf3b9612e43
ensuring datatype limitations before the instantiation in quickcheck_exhaustive
bulwahn
parents:
42310
diff
changeset

208 
else 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57996
diff
changeset

209 
(Old_Datatype_Aux.message config 
42315
95dfa082065a
generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents:
42314
diff
changeset

210 
("Creation of " ^ name ^ " failed because the datatype is recursive under a function type"); 
42230
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset

211 
thy) 
42315
95dfa082065a
generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents:
42314
diff
changeset

212 

62979  213 
val instantiate_bounded_forall_datatype = 
214 
instantiate_datatype 

67149  215 
("bounded universal quantifiers", bounded_forallN, \<^sort>\<open>bounded_forall\<close>, 
62979  216 
mk_bounded_forall_equations, bounded_forallT, ["P", "i"]) 
42315
95dfa082065a
generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents:
42314
diff
changeset

217 

62979  218 
val instantiate_exhaustive_datatype = 
219 
instantiate_datatype 

67149  220 
("exhaustive generators", exhaustiveN, \<^sort>\<open>exhaustive\<close>, 
62979  221 
mk_equations, exhaustiveT, ["f", "i"]) 
42315
95dfa082065a
generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents:
42314
diff
changeset

222 

62979  223 
val instantiate_full_exhaustive_datatype = 
224 
instantiate_datatype 

67149  225 
("full exhaustive generators", full_exhaustiveN, \<^sort>\<open>full_exhaustive\<close>, 
62979  226 
mk_full_equations, full_exhaustiveT, ["f", "i"]) 
227 

42390
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

228 

42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

229 
(* building and compiling generator expressions *) 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

230 

48013
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
46565
diff
changeset

231 
fun mk_let_expr (x, t, e) genuine = 
62979  232 
let val (T1, T2) = (fastype_of x, fastype_of (e genuine)) 
67149  233 
in Const (\<^const_name>\<open>Let\<close>, T1 > (T1 > T2) > T2) $ t $ lambda x (e genuine) end 
42390
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

234 

48414
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

235 
fun mk_safe_let_expr genuine_only none safe (x, t, e) genuine = 
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

236 
let 
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

237 
val (T1, T2) = (fastype_of x, fastype_of (e genuine)) 
67149  238 
val if_t = Const (\<^const_name>\<open>If\<close>, \<^typ>\<open>bool\<close> > T2 > T2 > T2) 
48414
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

239 
in 
67149  240 
Const (\<^const_name>\<open>Quickcheck_Random.catch_match\<close>, T2 > T2 > T2) $ 
241 
(Const (\<^const_name>\<open>Let\<close>, T1 > (T1 > T2) > T2) $ t $ lambda x (e genuine)) $ 

48414
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

242 
(if_t $ genuine_only $ none $ safe false) 
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

243 
end 
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

244 

48013
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
46565
diff
changeset

245 
fun mk_test_term lookup mk_closure mk_if mk_let none_t return ctxt = 
42306  246 
let 
62979  247 
val cnstrs = 
248 
flat (maps 

249 
(map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd) 

250 
(Symtab.dest 

251 
(BNF_LFP_Compat.get_all (Proof_Context.theory_of ctxt) Quickcheck_Common.compat_prefs))) 

252 
fun is_constrt (Const (s, T), ts) = 

253 
(case (AList.lookup (op =) cnstrs s, body_type T) of 

254 
(SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' 

255 
 _ => false) 

48013
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
46565
diff
changeset

256 
 is_constrt _ = false 
42306  257 
fun mk_naive_test_term t = 
62979  258 
fold_rev mk_closure (map lookup (Term.add_free_names t [])) (mk_if (t, none_t, return) true) 
48414
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

259 
fun mk_test (vars, check) = fold_rev mk_closure (map lookup vars) check 
45721
d1fb55c2ed65
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents:
45718
diff
changeset

260 
fun mk_smart_test_term' concl bound_vars assms genuine = 
42306  261 
let 
262 
fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t []) 

48013
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
46565
diff
changeset

263 
fun mk_equality_term (lhs, f as Free (x, _)) c (assm, assms) = 
62979  264 
if member (op =) (Term.add_free_names lhs bound_vars) x then 
265 
c (assm, assms) 

266 
else 

267 
let 

268 
val rec_call = mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms 

269 
fun safe genuine = 

270 
the_default I (Option.map mk_closure (try lookup x)) (rec_call genuine) 

271 
in 

272 
mk_test (remove (op =) x (vars_of assm), 

273 
mk_let safe f (try lookup x) lhs 

274 
(mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine) 

275 

276 
end 

48013
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
46565
diff
changeset

277 
 mk_equality_term (lhs, t) c (assm, assms) = 
62979  278 
if is_constrt (strip_comb t) then 
279 
let 

280 
val (constr, args) = strip_comb t 

281 
val T = fastype_of t 

282 
val vars = 

283 
map Free 

284 
(Variable.variant_frees ctxt (concl :: assms) 

285 
(map (fn t => ("x", fastype_of t)) args)) 

286 
val varnames = map (fst o dest_Free) vars 

287 
val dummy_var = 

288 
Free (singleton 

289 
(Variable.variant_frees ctxt (concl :: assms @ vars)) ("dummy", T)) 

290 
val new_assms = map HOLogic.mk_eq (vars ~~ args) 

291 
val bound_vars' = union (op =) (vars_of lhs) (union (op =) varnames bound_vars) 

292 
val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine 

293 
in 

294 
mk_test (vars_of lhs, 

295 
Case_Translation.make_case ctxt Case_Translation.Quiet Name.context lhs 

296 
[(list_comb (constr, vars), cont_t), (dummy_var, none_t)]) 

297 
end 

298 
else c (assm, assms) 

48414
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

299 
fun default (assm, assms) = 
62979  300 
mk_test 
301 
(vars_of assm, 

302 
mk_if (HOLogic.mk_not assm, none_t, 

303 
mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine) 

42306  304 
in 
62979  305 
(case assms of 
306 
[] => mk_test (vars_of concl, mk_if (concl, none_t, return) genuine) 

307 
 assm :: assms => 

48414
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

308 
if Config.get ctxt optimise_equality then 
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

309 
(case try HOLogic.dest_eq assm of 
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

310 
SOME (lhs, rhs) => 
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

311 
mk_equality_term (lhs, rhs) (mk_equality_term (rhs, lhs) default) (assm, assms) 
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

312 
 NONE => default (assm, assms)) 
62979  313 
else default (assm, assms)) 
42306  314 
end 
42390
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

315 
val mk_smart_test_term = 
45721
d1fb55c2ed65
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents:
45718
diff
changeset

316 
Quickcheck_Common.strip_imp #> (fn (assms, concl) => mk_smart_test_term' concl [] assms true) 
62979  317 
in if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term end 
42390
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

318 

be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

319 
fun mk_fast_generator_expr ctxt (t, eval_terms) = 
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

320 
let 
70308  321 
val ctxt' = Proof_Context.augment t ctxt 
42390
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

322 
val names = Term.add_free_names t [] 
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

323 
val frees = map Free (Term.add_frees t []) 
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

324 
fun lookup v = the (AList.lookup (op =) (names ~~ frees) v) 
46306  325 
val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt' 
67149  326 
val depth = Free (depth_name, \<^typ>\<open>natural\<close>) 
62979  327 
fun return _ = 
67149  328 
\<^term>\<open>throw_Counterexample :: term list \<Rightarrow> unit\<close> $ 
329 
(HOLogic.mk_list \<^typ>\<open>term\<close> 

62979  330 
(map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms))) 
42390
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

331 
fun mk_exhaustive_closure (free as Free (_, T)) t = 
67149  332 
Const (\<^const_name>\<open>fast_exhaustive\<close>, fast_exhaustiveT T) $ lambda free t $ depth 
333 
val none_t = \<^term>\<open>()\<close> 

45761
90028fd2f1fa
exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly
bulwahn
parents:
45754
diff
changeset

334 
fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine) 
48414
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

335 
fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e) 
62979  336 
val mk_test_term = 
337 
mk_test_term lookup mk_exhaustive_closure mk_safe_if mk_let none_t return ctxt 

67149  338 
in lambda depth (\<^term>\<open>catch_Counterexample :: unit => term list option\<close> $ mk_test_term t) end 
42306  339 

62979  340 
fun mk_unknown_term T = 
67149  341 
HOLogic.reflect_term (Const (\<^const_name>\<open>unknown\<close>, T)) 
45688
d4ac5e090cd9
also potential counterexamples in the simple exhaustive testing in quickcheck
bulwahn
parents:
45684
diff
changeset

342 

62979  343 
fun mk_safe_term t = 
67149  344 
\<^term>\<open>Quickcheck_Random.catch_match :: term \<Rightarrow> term \<Rightarrow> term\<close> $ 
62979  345 
(HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t) 
45688
d4ac5e090cd9
also potential counterexamples in the simple exhaustive testing in quickcheck
bulwahn
parents:
45684
diff
changeset

346 

62979  347 
fun mk_return t genuine = 
67149  348 
\<^term>\<open>Some :: bool \<times> term list \<Rightarrow> (bool \<times> term list) option\<close> $ 
349 
(HOLogic.pair_const \<^typ>\<open>bool\<close> \<^typ>\<open>term list\<close> $ 

62979  350 
Quickcheck_Common.reflect_bool genuine $ t) 
45724
1f5fc44254d7
the simple exhaustive compilation also indicates if counterexample is potentially spurious;
bulwahn
parents:
45722
diff
changeset

351 

42028
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset

352 
fun mk_generator_expr ctxt (t, eval_terms) = 
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset

353 
let 
70308  354 
val ctxt' = Proof_Context.augment t ctxt 
42028
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset

355 
val names = Term.add_free_names t [] 
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset

356 
val frees = map Free (Term.add_frees t []) 
42390
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

357 
fun lookup v = the (AList.lookup (op =) (names ~~ frees) v) 
46306  358 
val ([depth_name, genuine_only_name], _) = 
45754
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

359 
Variable.variant_fixes ["depth", "genuine_only"] ctxt' 
67149  360 
val depth = Free (depth_name, \<^typ>\<open>natural\<close>) 
361 
val genuine_only = Free (genuine_only_name, \<^typ>\<open>bool\<close>) 

62979  362 
val return = 
67149  363 
mk_return (HOLogic.mk_list \<^typ>\<open>term\<close> 
45688
d4ac5e090cd9
also potential counterexamples in the simple exhaustive testing in quickcheck
bulwahn
parents:
45684
diff
changeset

364 
(map (fn t => HOLogic.mk_term_of (fastype_of t) t) frees @ map mk_safe_term eval_terms)) 
42304  365 
fun mk_exhaustive_closure (free as Free (_, T)) t = 
67149  366 
Const (\<^const_name>\<open>exhaustive\<close>, exhaustiveT T) $ lambda free t $ depth 
367 
val none_t = Const (\<^const_name>\<open>None\<close>, resultT) 

45763
3bb2bdf654f7
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn
parents:
45761
diff
changeset

368 
val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t 
62979  369 
fun mk_let safe def v_opt t e = 
370 
mk_safe_let_expr genuine_only none_t safe (the_default def v_opt, t, e) 

48013
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
46565
diff
changeset

371 
val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt 
45754
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

372 
in lambda genuine_only (lambda depth (mk_test_term t)) end 
42304  373 

374 
fun mk_full_generator_expr ctxt (t, eval_terms) = 

375 
let 

42361  376 
val thy = Proof_Context.theory_of ctxt 
70308  377 
val ctxt' = Proof_Context.augment t ctxt 
42304  378 
val names = Term.add_free_names t [] 
379 
val frees = map Free (Term.add_frees t []) 

45753
196697f71488
indicating where the restart should occur; making safe_if dynamic
bulwahn
parents:
45732
diff
changeset

380 
val ([depth_name, genuine_only_name], ctxt'') = 
196697f71488
indicating where the restart should occur; making safe_if dynamic
bulwahn
parents:
45732
diff
changeset

381 
Variable.variant_fixes ["depth", "genuine_only"] ctxt' 
46306  382 
val (term_names, _) = Variable.variant_fixes (map (prefix "t_") names) ctxt'' 
67149  383 
val depth = Free (depth_name, \<^typ>\<open>natural\<close>) 
384 
val genuine_only = Free (genuine_only_name, \<^typ>\<open>bool\<close>) 

385 
val term_vars = map (fn n => Free (n, \<^typ>\<open>unit \<Rightarrow> term\<close>)) term_names 

42390
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

386 
fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v) 
62979  387 
val return = 
388 
mk_return 

67149  389 
(HOLogic.mk_list \<^typ>\<open>term\<close> 
390 
(map (fn v => v $ \<^term>\<open>()\<close>) term_vars @ map mk_safe_term eval_terms)) 

42028
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset

391 
fun mk_exhaustive_closure (free as Free (_, T), term_var) t = 
67149  392 
if Sign.of_sort thy (T, \<^sort>\<open>check_all\<close>) then 
393 
Const (\<^const_name>\<open>check_all\<close>, check_allT T) $ 

394 
(HOLogic.case_prod_const (T, \<^typ>\<open>unit \<Rightarrow> term\<close>, resultT) $ 

62979  395 
lambda free (lambda term_var t)) 
42028
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset

396 
else 
67149  397 
Const (\<^const_name>\<open>full_exhaustive\<close>, full_exhaustiveT T) $ 
398 
(HOLogic.case_prod_const (T, \<^typ>\<open>unit \<Rightarrow> term\<close>, resultT) $ 

62979  399 
lambda free (lambda term_var t)) $ depth 
67149  400 
val none_t = Const (\<^const_name>\<open>None\<close>, resultT) 
45763
3bb2bdf654f7
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn
parents:
45761
diff
changeset

401 
val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t 
48414
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

402 
fun mk_let safe _ (SOME (v, term_var)) t e = 
62979  403 
mk_safe_let_expr genuine_only none_t safe (v, t, 
67149  404 
e #> subst_free [(term_var, absdummy \<^typ>\<open>unit\<close> (mk_safe_term t))]) 
48414
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

405 
 mk_let safe v NONE t e = mk_safe_let_expr genuine_only none_t safe (v, t, e) 
48013
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
46565
diff
changeset

406 
val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt 
45753
196697f71488
indicating where the restart should occur; making safe_if dynamic
bulwahn
parents:
45732
diff
changeset

407 
in lambda genuine_only (lambda depth (mk_test_term t)) end 
42028
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset

408 

42304  409 
fun mk_parametric_generator_expr mk_generator_expr = 
62979  410 
Quickcheck_Common.gen_mk_parametric_generator_expr 
45754
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

411 
((mk_generator_expr, 
67149  412 
absdummy \<^typ>\<open>bool\<close> (absdummy \<^typ>\<open>natural\<close> (Const (\<^const_name>\<open>None\<close>, resultT)))), 
413 
\<^typ>\<open>bool\<close> > \<^typ>\<open>natural\<close> > resultT) 

42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset

414 

1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset

415 
fun mk_validator_expr ctxt t = 
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset

416 
let 
67149  417 
fun bounded_forallT T = (T > \<^typ>\<open>bool\<close>) > \<^typ>\<open>natural\<close> > \<^typ>\<open>bool\<close> 
70308  418 
val ctxt' = Proof_Context.augment t ctxt 
42390
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

419 
val names = Term.add_free_names t [] 
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

420 
val frees = map Free (Term.add_frees t []) 
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

421 
fun lookup v = the (AList.lookup (op =) (names ~~ frees) v) 
46306  422 
val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt' 
67149  423 
val depth = Free (depth_name, \<^typ>\<open>natural\<close>) 
42390
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

424 
fun mk_bounded_forall (Free (s, T)) t = 
67149  425 
Const (\<^const_name>\<open>bounded_forall\<close>, bounded_forallT T) $ lambda (Free (s, T)) t $ depth 
45761
90028fd2f1fa
exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly
bulwahn
parents:
45754
diff
changeset

426 
fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine) 
50046  427 
fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e) 
45721
d1fb55c2ed65
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents:
45718
diff
changeset

428 
val mk_test_term = 
67149  429 
mk_test_term lookup mk_bounded_forall mk_safe_if mk_let \<^term>\<open>True\<close> (K \<^term>\<open>False\<close>) ctxt 
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset

430 
in lambda depth (mk_test_term t) end 
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset

431 

62979  432 
fun mk_bounded_forall_generator_expr ctxt (t, eval_terms) = 
42391  433 
let 
434 
val frees = Term.add_free_names t [] 

62979  435 
val dummy_term = 
67149  436 
\<^term>\<open>Code_Evaluation.Const (STR ''Pure.dummy_pattern'') (Typerep.Typerep (STR ''dummy'') [])\<close> 
62979  437 
val return = 
67149  438 
\<^term>\<open>Some :: term list => term list option\<close> $ 
439 
(HOLogic.mk_list \<^typ>\<open>term\<close> (replicate (length frees + length eval_terms) dummy_term)) 

440 
val wrap = absdummy \<^typ>\<open>bool\<close> 

441 
(\<^term>\<open>If :: bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option\<close> $ 

442 
Bound 0 $ \<^term>\<open>None :: term list option\<close> $ return) 

42391  443 
in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end 
62979  444 

59154  445 

71394  446 
(** generator compilation **) 
42028
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset

447 

59154  448 
structure Data = Proof_Data 
41861
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset

449 
( 
59154  450 
type T = 
62979  451 
(unit > Code_Numeral.natural > bool > Code_Numeral.natural > (bool * term list) option) * 
59154  452 
(unit > (Code_Numeral.natural > term list option) list) * 
62979  453 
(unit > (Code_Numeral.natural > bool) list) 
59154  454 
val empty: T = 
455 
(fn () => raise Fail "counterexample", 

456 
fn () => raise Fail "counterexample_batch", 

62979  457 
fn () => raise Fail "validator_batch") 
458 
fun init _ = empty 

459 
) 

41861
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset

460 

62979  461 
val get_counterexample = #1 o Data.get 
462 
val get_counterexample_batch = #2 o Data.get 

463 
val get_validator_batch = #3 o Data.get 

42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset

464 

62979  465 
val put_counterexample = Data.map o @{apply 3(1)} o K 
466 
val put_counterexample_batch = Data.map o @{apply 3(2)} o K 

467 
val put_validator_batch = Data.map o @{apply 3(3)} o K 

42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset

468 

62979  469 
val target = "Quickcheck" 
42391  470 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

471 
fun compile_generator_expr_raw ctxt ts = 
42159
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset

472 
let 
62979  473 
val mk_generator_expr = 
42306  474 
if Config.get ctxt fast then mk_fast_generator_expr 
42391  475 
else if Config.get ctxt bounded_forall then mk_bounded_forall_generator_expr 
42306  476 
else if Config.get ctxt full_support then mk_full_generator_expr else mk_generator_expr 
62979  477 
val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts 
478 
val compile = 

479 
Code_Runtime.dynamic_value_strict 

480 
(get_counterexample, put_counterexample, "Exhaustive_Generators.put_counterexample") 

481 
ctxt (SOME target) 

482 
(fn proc => fn g => fn card => fn genuine_only => fn size => 

483 
g card genuine_only size 

45754
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

484 
> (Option.map o apsnd o map) proc) t' [] 
42159
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset

485 
in 
62979  486 
fn genuine_only => fn [card, size] => 
487 
rpair NONE (compile card genuine_only size 

488 
> (if Config.get ctxt quickcheck_pretty then 

489 
Option.map (apsnd (map Quickcheck_Common.post_process_term)) else I)) 

490 
end 

42391  491 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

492 
fun compile_generator_expr ctxt ts = 
62979  493 
let val compiled = compile_generator_expr_raw ctxt ts in 
494 
fn genuine_only => fn [card, size] => 

495 
compiled genuine_only 

496 
[Code_Numeral.natural_of_integer card, Code_Numeral.natural_of_integer size] 

497 
end 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

498 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

499 
fun compile_generator_exprs_raw ctxt ts = 
41861
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset

500 
let 
62979  501 
val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts 
502 
val compiles = 

503 
Code_Runtime.dynamic_value_strict 

504 
(get_counterexample_batch, put_counterexample_batch, 

505 
"Exhaustive_Generators.put_counterexample_batch") 

506 
ctxt (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc)) 

67149  507 
(HOLogic.mk_list \<^typ>\<open>natural \<Rightarrow> term list option\<close> ts') [] 
41861
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset

508 
in 
62979  509 
map (fn compile => fn size => 
510 
compile size > (Option.map o map) Quickcheck_Common.post_process_term) compiles 

511 
end 

42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset

512 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

513 
fun compile_generator_exprs ctxt ts = 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

514 
compile_generator_exprs_raw ctxt ts 
62979  515 
> map (fn f => fn size => f (Code_Numeral.natural_of_integer size)) 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

516 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

517 
fun compile_validator_exprs_raw ctxt ts = 
62979  518 
let val ts' = map (mk_validator_expr ctxt) ts in 
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset

519 
Code_Runtime.dynamic_value_strict 
59154  520 
(get_validator_batch, put_validator_batch, "Exhaustive_Generators.put_validator_batch") 
67149  521 
ctxt (SOME target) (K I) (HOLogic.mk_list \<^typ>\<open>natural \<Rightarrow> bool\<close> ts') [] 
62979  522 
end 
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset

523 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

524 
fun compile_validator_exprs ctxt ts = 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

525 
compile_validator_exprs_raw ctxt ts 
62979  526 
> map (fn f => fn size => f (Code_Numeral.natural_of_integer size)) 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

527 

67149  528 
fun size_matters_for thy Ts = not (forall (fn T => Sign.of_sort thy (T, \<^sort>\<open>check_all\<close>)) Ts) 
46331
f5598b604a54
generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents:
46306
diff
changeset

529 

f5598b604a54
generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents:
46306
diff
changeset

530 
val test_goals = 
62979  531 
Quickcheck_Common.generator_test_goal_terms 
532 
("exhaustive", (size_matters_for, compile_generator_expr)) 

533 

534 

42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

535 
(* setup *) 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

536 

45484
23871e17dddb
setting up exhaustive generators which are used for the smart generators
bulwahn
parents:
45420
diff
changeset

537 
val setup_exhaustive_datatype_interpretation = 
67149  538 
Quickcheck_Common.datatype_interpretation \<^plugin>\<open>quickcheck_exhaustive\<close> 
539 
(\<^sort>\<open>exhaustive\<close>, instantiate_exhaustive_datatype) 

45484
23871e17dddb
setting up exhaustive generators which are used for the smart generators
bulwahn
parents:
45420
diff
changeset

540 

48178
0192811f0a96
exporting important function for the "many conjecture refutation" compilation of quickcheck
bulwahn
parents:
48013
diff
changeset

541 
val setup_bounded_forall_datatype_interpretation = 
67149  542 
BNF_LFP_Compat.interpretation \<^plugin>\<open>quickcheck_bounded_forall\<close> Quickcheck_Common.compat_prefs 
58186  543 
(Quickcheck_Common.ensure_sort 
67149  544 
(((\<^sort>\<open>type\<close>, \<^sort>\<open>type\<close>), \<^sort>\<open>bounded_forall\<close>), 
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58225
diff
changeset

545 
(fn thy => BNF_LFP_Compat.the_descr thy Quickcheck_Common.compat_prefs, 
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58225
diff
changeset

546 
instantiate_bounded_forall_datatype))) 
48178
0192811f0a96
exporting important function for the "many conjecture refutation" compilation of quickcheck
bulwahn
parents:
48013
diff
changeset

547 

67149  548 
val active = Attrib.setup_config_bool \<^binding>\<open>quickcheck_exhaustive_active\<close> (K true) 
43878
eeb10fdd9535
changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents:
43877
diff
changeset

549 

58826  550 
val _ = 
551 
Theory.setup 

67149  552 
(Quickcheck_Common.datatype_interpretation \<^plugin>\<open>quickcheck_full_exhaustive\<close> 
553 
(\<^sort>\<open>full_exhaustive\<close>, instantiate_full_exhaustive_datatype) 

58826  554 
#> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals))) 
555 
#> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs)) 

62979  556 
#> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs))) 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset

557 

62979  558 
end 