author  wenzelm 
Thu, 14 Apr 2016 15:56:30 +0200  
changeset 62981  3a01f1f58630 
parent 62979  1e527c40ae40 
child 67149  e61557884799 
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 

42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42391
diff
changeset

41 
val smart_quantifier = Attrib.setup_config_bool @{binding quickcheck_smart_quantifier} (K true) 
48013
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
46565
diff
changeset

42 
val optimise_equality = Attrib.setup_config_bool @{binding quickcheck_optimise_equality} (K true) 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
46565
diff
changeset

43 

42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42391
diff
changeset

44 
val fast = Attrib.setup_config_bool @{binding quickcheck_fast} (K false) 
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42391
diff
changeset

45 
val bounded_forall = Attrib.setup_config_bool @{binding quickcheck_bounded_forall} (K false) 
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42391
diff
changeset

46 
val full_support = Attrib.setup_config_bool @{binding quickcheck_full_support} (K true) 
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42391
diff
changeset

47 
val quickcheck_pretty = Attrib.setup_config_bool @{binding quickcheck_pretty} (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 

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

53 

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

54 
val size = @{term "i :: natural"} 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

55 
val size_pred = @{term "(i :: natural)  1"} 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

56 
val size_ge_zero = @{term "(i :: natural) > 0"} 
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) = 
62979  59 
let val (T as Type (@{type_name option}, _)) = fastype_of x 
62981  60 
in Const (@{const_name orelse}, 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 
64 
in Const (@{const_name If}, @{typ bool} > T > T > T) $ b $ t $ e end 

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 

62979  75 
val resultT = @{typ "(bool * term list) option"} 
45722  76 

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

79 
val bounded_forallN = "bounded_forall" 

42306  80 

62979  81 
fun fast_exhaustiveT T = (T > @{typ unit}) > @{typ natural} > @{typ unit} 
42306  82 

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

83 
fun exhaustiveT T = (T > resultT) > @{typ natural} > resultT 
42304  84 

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

85 
fun bounded_forallT T = (T > @{typ bool}) > @{typ natural} > @{typ bool} 
42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

86 

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

87 
fun full_exhaustiveT T = (termifyT T > resultT) > @{typ natural} > 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) 
62981  122 
val mk_call = gen_mk_call (fn T => Const (@{const_name exhaustive}, 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 = 
62979  126 
mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name None}, resultT)) 
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 
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

131 
fun test_function T = Free ("P", T > @{typ bool}) 
62981  132 
val mk_call = gen_mk_call (fn T => Const (@{const_name bounded_forall}, 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 
62979  135 
fun mk_rhs exprs = mk_if (size_ge_zero, foldr1 HOLogic.mk_conj exprs, @{term True}) 
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 = 
142 
HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> Code_Evaluation.term"}, resultT) 

42304  143 
fun mk_call T = 
144 
let 

62981  145 
val full_exhaustive = Const (@{const_name full_exhaustive}, full_exhaustiveT T) 
62979  146 
in 
147 
(T, 

148 
fn t => 

149 
full_exhaustive $ 

150 
(case_prod_const T $ absdummy T (absdummy @{typ "unit \<Rightarrow> Code_Evaluation.term"} t)) $ 

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 $ 

161 
(case_prod_const T $ absdummy T (absdummy @{typ "unit \<Rightarrow> Code_Evaluation.term"} t)) $ 

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 = 
62979  170 
Const (@{const_name Code_Evaluation.App}, 
171 
HOLogic.termT > HOLogic.termT > HOLogic.termT) 

56257  172 
val Eval_Const = 
62979  173 
Const (@{const_name Code_Evaluation.Const}, 
174 
HOLogic.literalT > @{typ typerep} > HOLogic.termT) 

175 
val term = 

176 
fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"})) 

177 
bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts > simpleT)) 

178 
val start_term = 

179 
test_function simpleT $ 

180 
(HOLogic.pair_const simpleT @{typ "unit \<Rightarrow> Code_Evaluation.term"} $ 

181 
(list_comb (constr, bounds)) $ absdummy @{typ unit} 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 = 
62979  184 
mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name None}, resultT)) 
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 

215 
("bounded universal quantifiers", bounded_forallN, @{sort bounded_forall}, 

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 

220 
("exhaustive generators", exhaustiveN, @{sort exhaustive}, 

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 

225 
("full exhaustive generators", full_exhaustiveN, @{sort full_exhaustive}, 

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)) 
233 
in Const (@{const_name Let}, 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)) 
62979  238 
val if_t = Const (@{const_name If}, @{typ bool} > T2 > T2 > T2) 
48414
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

239 
in 
62979  240 
Const (@{const_name Quickcheck_Random.catch_match}, T2 > T2 > T2) $ 
48414
43875bab3a4c
handling partiality in the case where the equality optimisation is applied
bulwahn
parents:
48273
diff
changeset

241 
(Const (@{const_name Let}, T1 > (T1 > T2) > T2) $ t $ lambda x (e genuine)) $ 
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 
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

321 
val ctxt' = Variable.auto_fixes t ctxt 
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' 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

326 
val depth = Free (depth_name, @{typ natural}) 
62979  327 
fun return _ = 
328 
@{term "throw_Counterexample :: term list \<Rightarrow> unit"} $ 

329 
(HOLogic.mk_list @{typ term} 

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 = 
62981  332 
Const (@{const_name fast_exhaustive}, fast_exhaustiveT T) $ lambda free t $ depth 
42390
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

333 
val none_t = @{term "()"} 
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 

42306  338 
in lambda depth (@{term "catch_Counterexample :: unit => term list option"} $ mk_test_term t) end 
339 

62979  340 
fun mk_unknown_term T = 
62981  341 
HOLogic.reflect_term (Const (@{const_name unknown}, 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 = 
344 
@{term "Quickcheck_Random.catch_match :: term \<Rightarrow> term \<Rightarrow> term"} $ 

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 = 
348 
@{term "Some :: bool \<times> term list \<Rightarrow> (bool \<times> term list) option"} $ 

349 
(HOLogic.pair_const @{typ bool} @{typ "term list"} $ 

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

354 
val ctxt' = Variable.auto_fixes t ctxt 
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' 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

360 
val depth = Free (depth_name, @{typ natural}) 
62979  361 
val genuine_only = Free (genuine_only_name, @{typ bool}) 
362 
val return = 

363 
mk_return (HOLogic.mk_list @{typ term} 

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 = 
62981  366 
Const (@{const_name exhaustive}, exhaustiveT T) $ lambda free t $ depth 
62979  367 
val none_t = Const (@{const_name None}, 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 
42304  377 
val ctxt' = Variable.auto_fixes t ctxt 
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'' 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

383 
val depth = Free (depth_name, @{typ natural}) 
62979  384 
val genuine_only = Free (genuine_only_name, @{typ bool}) 
385 
val term_vars = map (fn n => Free (n, @{typ "unit \<Rightarrow> term"})) 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 

389 
(HOLogic.mk_list @{typ term} 

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

390 
(map (fn v => v $ @{term "()"}) 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 = 
46331
f5598b604a54
generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents:
46306
diff
changeset

392 
if Sign.of_sort thy (T, @{sort check_all}) then 
62981  393 
Const (@{const_name check_all}, check_allT T) $ 
62979  394 
(HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> term"}, resultT) $ 
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 
62981  397 
Const (@{const_name full_exhaustive}, full_exhaustiveT T) $ 
62979  398 
(HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> term"}, resultT) $ 
399 
lambda free (lambda term_var t)) $ depth 

400 
val none_t = Const (@{const_name None}, 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, 
404 
e #> subst_free [(term_var, absdummy @{typ unit} (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, 
62979  412 
absdummy @{typ bool} (absdummy @{typ natural} (Const (@{const_name None}, resultT)))), 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

413 
@{typ bool} > @{typ natural} > 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 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

417 
fun bounded_forallT T = (T > @{typ bool}) > @{typ natural} > @{typ bool} 
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset

418 
val ctxt' = Variable.auto_fixes 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' 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

423 
val depth = Free (depth_name, @{typ natural}) 
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 = 
62981  425 
Const (@{const_name bounded_forall}, 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 = 
48013
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
46565
diff
changeset

429 
mk_test_term lookup mk_bounded_forall mk_safe_if mk_let @{term True} (K @{term False}) 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 = 
436 
@{term "Code_Evaluation.Const (STR ''Pure.dummy_pattern'') (Typerep.Typerep (STR ''dummy'') [])"} 

437 
val return = 

438 
@{term "Some :: term list => term list option"} $ 

439 
(HOLogic.mk_list @{typ term} (replicate (length frees + length eval_terms) dummy_term)) 

44241  440 
val wrap = absdummy @{typ bool} 
62979  441 
(@{term "If :: bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"} $ 
44241  442 
Bound 0 $ @{term "None :: term list option"} $ return) 
42391  443 
in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end 
62979  444 

59154  445 

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

446 
(** generator compiliation **) 
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)) 

507 
(HOLogic.mk_list @{typ "natural => term list option"} 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") 
62979  521 
ctxt (SOME target) (K I) (HOLogic.mk_list @{typ "natural \<Rightarrow> bool"} ts') [] 
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 

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

528 
fun size_matters_for thy Ts = not (forall (fn T => Sign.of_sort thy (T, @{sort check_all})) Ts) 
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 = 
58659
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58354
diff
changeset

538 
Quickcheck_Common.datatype_interpretation @{plugin quickcheck_exhaustive} 
58186  539 
(@{sort exhaustive}, 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 = 
58659
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58354
diff
changeset

542 
BNF_LFP_Compat.interpretation @{plugin quickcheck_bounded_forall} Quickcheck_Common.compat_prefs 
58186  543 
(Quickcheck_Common.ensure_sort 
544 
(((@{sort type}, @{sort type}), @{sort bounded_forall}), 

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 

62979  548 
val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (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 

552 
(Quickcheck_Common.datatype_interpretation @{plugin quickcheck_full_exhaustive} 

553 
(@{sort full_exhaustive}, instantiate_full_exhaustive_datatype) 

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 