author  wenzelm 
Thu, 14 Apr 2016 15:33:51 +0200  
changeset 62979  1e527c40ae40 
parent 61424  c3658c18b7bc 
child 62981  3a01f1f58630 
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 
60 
in Const (@{const_name Quickcheck_Exhaustive.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) 
42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

122 
val mk_call = gen_mk_call (fn T => 
62979  123 
Const (@{const_name Quickcheck_Exhaustive.exhaustive_class.exhaustive}, exhaustiveT T)) 
42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

124 
val mk_aux_call = gen_mk_aux_call functerms 
46306  125 
val mk_consexpr = gen_mk_consexpr test_function 
42304  126 
fun mk_rhs exprs = 
62979  127 
mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name None}, resultT)) 
128 
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

129 

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

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

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

132 
fun test_function T = Free ("P", T > @{typ bool}) 
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

133 
val mk_call = gen_mk_call (fn T => 
62979  134 
Const (@{const_name Quickcheck_Exhaustive.bounded_forall_class.bounded_forall}, 
42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

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

136 
val mk_aux_call = gen_mk_aux_call functerms 
46306  137 
val mk_consexpr = gen_mk_consexpr test_function 
62979  138 
fun mk_rhs exprs = mk_if (size_ge_zero, foldr1 HOLogic.mk_conj exprs, @{term True}) 
139 
in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end 

140 

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

141 
fun mk_full_equations functerms = 
42304  142 
let 
45722  143 
fun test_function T = Free ("f", termifyT T > resultT) 
62979  144 
fun case_prod_const T = 
145 
HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> Code_Evaluation.term"}, resultT) 

42304  146 
fun mk_call T = 
147 
let 

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

148 
val full_exhaustive = 
62979  149 
Const (@{const_name Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive}, 
42308
e2abd1ca8d01
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents:
42307
diff
changeset

150 
full_exhaustiveT T) 
62979  151 
in 
152 
(T, 

153 
fn t => 

154 
full_exhaustive $ 

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

156 
size_pred) 

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

157 
end 
41918  158 
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

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

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

161 
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

162 
in 
62979  163 
(T, 
164 
fn t => 

165 
nth functerms k $ 

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

167 
size_pred) 

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

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

169 
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

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

171 
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

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

173 
val bounds = map (fn x => Bound (2 * x + 1)) (((length xs)  1) downto 0) 
56257  174 
val Eval_App = 
62979  175 
Const (@{const_name Code_Evaluation.App}, 
176 
HOLogic.termT > HOLogic.termT > HOLogic.termT) 

56257  177 
val Eval_Const = 
62979  178 
Const (@{const_name Code_Evaluation.Const}, 
179 
HOLogic.literalT > @{typ typerep} > HOLogic.termT) 

180 
val term = 

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

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

183 
val start_term = 

184 
test_function simpleT $ 

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

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

187 
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

188 
fun mk_rhs exprs = 
62979  189 
mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name None}, resultT)) 
190 
in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end 

191 

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

192 

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

193 
(** instantiating generator classes **) 
62979  194 

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

196 
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

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

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

199 
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

200 
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

201 
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

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

203 
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

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

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

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

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

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

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

210 
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

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

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

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

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

215 
("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

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

217 

62979  218 
val instantiate_bounded_forall_datatype = 
219 
instantiate_datatype 

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

221 
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

222 

62979  223 
val instantiate_exhaustive_datatype = 
224 
instantiate_datatype 

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

226 
mk_equations, exhaustiveT, ["f", "i"]) 

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

227 

62979  228 
val instantiate_full_exhaustive_datatype = 
229 
instantiate_datatype 

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

231 
mk_full_equations, full_exhaustiveT, ["f", "i"]) 

232 

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

233 

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

234 
(* 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

235 

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

236 
fun mk_let_expr (x, t, e) genuine = 
62979  237 
let val (T1, T2) = (fastype_of x, fastype_of (e genuine)) 
238 
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

239 

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

240 
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

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

242 
val (T1, T2) = (fastype_of x, fastype_of (e genuine)) 
62979  243 
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

244 
in 
62979  245 
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

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

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

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

249 

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

250 
fun mk_test_term lookup mk_closure mk_if mk_let none_t return ctxt = 
42306  251 
let 
62979  252 
val cnstrs = 
253 
flat (maps 

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

255 
(Symtab.dest 

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

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

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

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

260 
 _ => false) 

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

261 
 is_constrt _ = false 
42306  262 
fun mk_naive_test_term t = 
62979  263 
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

264 
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

265 
fun mk_smart_test_term' concl bound_vars assms genuine = 
42306  266 
let 
267 
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

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

271 
else 

272 
let 

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

274 
fun safe genuine = 

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

276 
in 

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

278 
mk_let safe f (try lookup x) lhs 

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

280 

281 
end 

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

282 
 mk_equality_term (lhs, t) c (assm, assms) = 
62979  283 
if is_constrt (strip_comb t) then 
284 
let 

285 
val (constr, args) = strip_comb t 

286 
val T = fastype_of t 

287 
val vars = 

288 
map Free 

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

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

291 
val varnames = map (fst o dest_Free) vars 

292 
val dummy_var = 

293 
Free (singleton 

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

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

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

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

298 
in 

299 
mk_test (vars_of lhs, 

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

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

302 
end 

303 
else c (assm, assms) 

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

304 
fun default (assm, assms) = 
62979  305 
mk_test 
306 
(vars_of assm, 

307 
mk_if (HOLogic.mk_not assm, none_t, 

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

42306  309 
in 
62979  310 
(case assms of 
311 
[] => mk_test (vars_of concl, mk_if (concl, none_t, return) genuine) 

312 
 assm :: assms => 

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

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

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

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

316 
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

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

320 
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

321 
Quickcheck_Common.strip_imp #> (fn (assms, concl) => mk_smart_test_term' concl [] assms true) 
62979  322 
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

323 

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

324 
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

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

326 
val ctxt' = Variable.auto_fixes t ctxt 
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

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

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

329 
fun lookup v = the (AList.lookup (op =) (names ~~ frees) v) 
46306  330 
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

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

334 
(HOLogic.mk_list @{typ term} 

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

336 
fun mk_exhaustive_closure (free as Free (_, T)) t = 
62979  337 
Const (@{const_name Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive}, 
338 
fast_exhaustiveT T) $ lambda free t $ depth 

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

339 
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

340 
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

341 
fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e) 
62979  342 
val mk_test_term = 
343 
mk_test_term lookup mk_exhaustive_closure mk_safe_if mk_let none_t return ctxt 

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

62979  346 
fun mk_unknown_term T = 
347 
HOLogic.reflect_term (Const (@{const_name Quickcheck_Exhaustive.unknown}, T)) 

45688
d4ac5e090cd9
also potential counterexamples in the simple exhaustive testing in quickcheck
bulwahn
parents:
45684
diff
changeset

348 

62979  349 
fun mk_safe_term t = 
350 
@{term "Quickcheck_Random.catch_match :: term \<Rightarrow> term \<Rightarrow> term"} $ 

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

352 

62979  353 
fun mk_return t genuine = 
354 
@{term "Some :: bool \<times> term list \<Rightarrow> (bool \<times> term list) option"} $ 

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

356 
Quickcheck_Common.reflect_bool genuine $ t) 

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

357 

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

358 
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

359 
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

360 
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

361 
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

362 
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

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

365 
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

366 
val depth = Free (depth_name, @{typ natural}) 
62979  367 
val genuine_only = Free (genuine_only_name, @{typ bool}) 
368 
val return = 

369 
mk_return (HOLogic.mk_list @{typ term} 

45688
d4ac5e090cd9
also potential counterexamples in the simple exhaustive testing in quickcheck
bulwahn
parents:
45684
diff
changeset

370 
(map (fn t => HOLogic.mk_term_of (fastype_of t) t) frees @ map mk_safe_term eval_terms)) 
42304  371 
fun mk_exhaustive_closure (free as Free (_, T)) t = 
62979  372 
Const (@{const_name Quickcheck_Exhaustive.exhaustive_class.exhaustive}, exhaustiveT T) $ 
373 
lambda free t $ depth 

374 
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

375 
val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t 
62979  376 
fun mk_let safe def v_opt t e = 
377 
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

378 
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

379 
in lambda genuine_only (lambda depth (mk_test_term t)) end 
42304  380 

381 
fun mk_full_generator_expr ctxt (t, eval_terms) = 

382 
let 

42361  383 
val thy = Proof_Context.theory_of ctxt 
42304  384 
val ctxt' = Variable.auto_fixes t ctxt 
385 
val names = Term.add_free_names t [] 

386 
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

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

388 
Variable.variant_fixes ["depth", "genuine_only"] ctxt' 
46306  389 
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

390 
val depth = Free (depth_name, @{typ natural}) 
62979  391 
val genuine_only = Free (genuine_only_name, @{typ bool}) 
392 
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

393 
fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v) 
62979  394 
val return = 
395 
mk_return 

396 
(HOLogic.mk_list @{typ term} 

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

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

398 
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

399 
if Sign.of_sort thy (T, @{sort check_all}) then 
62979  400 
Const (@{const_name Quickcheck_Exhaustive.check_all_class.check_all}, check_allT T) $ 
401 
(HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> term"}, resultT) $ 

402 
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

403 
else 
62979  404 
Const (@{const_name Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive}, 
405 
full_exhaustiveT T) $ 

406 
(HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> term"}, resultT) $ 

407 
lambda free (lambda term_var t)) $ depth 

408 
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

409 
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

410 
fun mk_let safe _ (SOME (v, term_var)) t e = 
62979  411 
mk_safe_let_expr genuine_only none_t safe (v, t, 
412 
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

413 
 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

414 
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

415 
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

416 

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

419 
((mk_generator_expr, 
62979  420 
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

421 
@{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

422 

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

423 
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

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

425 
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

426 
val ctxt' = Variable.auto_fixes t ctxt 
42390
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

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

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

429 
fun lookup v = the (AList.lookup (op =) (names ~~ frees) v) 
46306  430 
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

431 
val depth = Free (depth_name, @{typ natural}) 
42390
be7af468f7b3
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents:
42361
diff
changeset

432 
fun mk_bounded_forall (Free (s, T)) t = 
62979  433 
Const (@{const_name Quickcheck_Exhaustive.bounded_forall_class.bounded_forall}, 
434 
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

435 
fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine) 
50046  436 
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

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

438 
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

439 
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

440 

62979  441 
fun mk_bounded_forall_generator_expr ctxt (t, eval_terms) = 
42391  442 
let 
443 
val frees = Term.add_free_names t [] 

62979  444 
val dummy_term = 
445 
@{term "Code_Evaluation.Const (STR ''Pure.dummy_pattern'') (Typerep.Typerep (STR ''dummy'') [])"} 

446 
val return = 

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

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

44241  449 
val wrap = absdummy @{typ bool} 
62979  450 
(@{term "If :: bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"} $ 
44241  451 
Bound 0 $ @{term "None :: term list option"} $ return) 
42391  452 
in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end 
62979  453 

59154  454 

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

455 
(** 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

456 

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

458 
( 
59154  459 
type T = 
62979  460 
(unit > Code_Numeral.natural > bool > Code_Numeral.natural > (bool * term list) option) * 
59154  461 
(unit > (Code_Numeral.natural > term list option) list) * 
62979  462 
(unit > (Code_Numeral.natural > bool) list) 
59154  463 
val empty: T = 
464 
(fn () => raise Fail "counterexample", 

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

62979  466 
fn () => raise Fail "validator_batch") 
467 
fun init _ = empty 

468 
) 

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

469 

62979  470 
val get_counterexample = #1 o Data.get 
471 
val get_counterexample_batch = #2 o Data.get 

472 
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

473 

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

476 
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

477 

62979  478 
val target = "Quickcheck" 
42391  479 

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

480 
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

481 
let 
62979  482 
val mk_generator_expr = 
42306  483 
if Config.get ctxt fast then mk_fast_generator_expr 
42391  484 
else if Config.get ctxt bounded_forall then mk_bounded_forall_generator_expr 
42306  485 
else if Config.get ctxt full_support then mk_full_generator_expr else mk_generator_expr 
62979  486 
val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts 
487 
val compile = 

488 
Code_Runtime.dynamic_value_strict 

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

490 
ctxt (SOME target) 

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

492 
g card genuine_only size 

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

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

494 
in 
62979  495 
fn genuine_only => fn [card, size] => 
496 
rpair NONE (compile card genuine_only size 

497 
> (if Config.get ctxt quickcheck_pretty then 

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

499 
end 

42391  500 

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

501 
fun compile_generator_expr ctxt ts = 
62979  502 
let val compiled = compile_generator_expr_raw ctxt ts in 
503 
fn genuine_only => fn [card, size] => 

504 
compiled genuine_only 

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

506 
end 

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

507 

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

508 
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

509 
let 
62979  510 
val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts 
511 
val compiles = 

512 
Code_Runtime.dynamic_value_strict 

513 
(get_counterexample_batch, put_counterexample_batch, 

514 
"Exhaustive_Generators.put_counterexample_batch") 

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

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

517 
in 
62979  518 
map (fn compile => fn size => 
519 
compile size > (Option.map o map) Quickcheck_Common.post_process_term) compiles 

520 
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

521 

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

522 
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

523 
compile_generator_exprs_raw ctxt ts 
62979  524 
> 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

525 

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

526 
fun compile_validator_exprs_raw ctxt ts = 
62979  527 
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

528 
Code_Runtime.dynamic_value_strict 
59154  529 
(get_validator_batch, put_validator_batch, "Exhaustive_Generators.put_validator_batch") 
62979  530 
ctxt (SOME target) (K I) (HOLogic.mk_list @{typ "natural \<Rightarrow> bool"} ts') [] 
531 
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

532 

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

533 
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

534 
compile_validator_exprs_raw ctxt ts 
62979  535 
> 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

536 

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

537 
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

538 

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

539 
val test_goals = 
62979  540 
Quickcheck_Common.generator_test_goal_terms 
541 
("exhaustive", (size_matters_for, compile_generator_expr)) 

542 

543 

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

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

545 

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

546 
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

547 
Quickcheck_Common.datatype_interpretation @{plugin quickcheck_exhaustive} 
58186  548 
(@{sort exhaustive}, instantiate_exhaustive_datatype) 
45484
23871e17dddb
setting up exhaustive generators which are used for the smart generators
bulwahn
parents:
45420
diff
changeset

549 

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

550 
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

551 
BNF_LFP_Compat.interpretation @{plugin quickcheck_bounded_forall} Quickcheck_Common.compat_prefs 
58186  552 
(Quickcheck_Common.ensure_sort 
553 
(((@{sort type}, @{sort type}), @{sort bounded_forall}), 

58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58225
diff
changeset

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

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

556 

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

558 

58826  559 
val _ = 
560 
Theory.setup 

561 
(Quickcheck_Common.datatype_interpretation @{plugin quickcheck_full_exhaustive} 

562 
(@{sort full_exhaustive}, instantiate_full_exhaustive_datatype) 

563 
#> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals))) 

564 
#> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs)) 

62979  565 
#> 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

566 

62979  567 
end 