1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
|
Set Warnings "-notation-overridden,-parsing".
From mathcomp Require Import ssreflect ssrfun ssrbool.
From Coq Require Import Relations ZArith Strings.Ascii Strings.String.
From QuickChick Require Import LazyList QuickChick.
From doc Require Import QuickChickInterface.
(* This module is just to keep the BasicInterface up-to-date with the implementation. *)
Module ConsistencyCheck : QuickChickSig.
Definition RandomSeed := RandomSeed.
Definition G := @G.
Definition semGen := @semProd G ProducerGen.
Definition semGenSize := @semGenSize.
Definition Functor_G := @Functor_Monad _ (@super _ ProducerGen).
Definition Applicative_G :=
@Applicative_Monad _ (@super _ ProducerGen).
Definition Monad_G := @super _ ProducerGen.
Definition bindGen' := @bindPf G ProducerGen.
Definition bindGenOpt := @bindOpt G ProducerGen.
Definition run := @Generators.run.
Definition listOf := @listOf G ProducerGen.
Definition vectorOf := @vectorOf G ProducerGen.
Definition elems_ := @elems_ G ProducerGen.
Definition oneOf_ := @oneOf_ G ProducerGen.
Definition freq_ := @freq_.
Definition backtrack := @backtrack.
Definition resize := @resize G ProducerGen.
Definition sized := @sized G ProducerGen.
Definition suchThatMaybe := @suchThatMaybe.
Definition suchThatMaybeOpt := @suchThatMaybeOpt.
Class ChoosableFromInterval (A : Type) (le : relation A) : Type :=
{
randomR : A * A -> RandomSeed -> A * RandomSeed;
randomRCorrect :
forall (a a1 a2 : A), le a1 a2 ->
(le a1 a /\ le a a2 <->
exists seed, fst (randomR (a1, a2) seed) = a);
enumR : A * A -> LazyList A;
enumRCorrect :
forall (a a1 a2 : A), le a1 a2 ->
(le a1 a /\ le a a2 <->
In_ll a (enumR (a1,a2)))
}.
#[global] Existing Instance super.
Definition ChooseN := ChooseN.
Definition ChooseNat := ChooseNat.
Definition ChooseZ := ChooseZ.
Definition choose := @choose G ProducerGen.
Module QcDefaultNotation.
(*
(** 'elems' as a shorthand for elements without a default argument *)
Notation " 'elems' [ x ] " :=
(elements x (cons x nil)) : qc_scope.
Notation " 'elems' [ x ; y ] " :=
(elements x (cons x (cons y nil))) : qc_scope.
Notation " 'elems' [ x ; y ; .. ; z ] " :=
(elements x (cons x (cons y .. (cons z nil) ..))) : qc_scope.
Notation " 'elems' ( x ;; l ) " :=
(elements x (cons x l)) (at level 1, no associativity) : qc_scope.
(** 'oneOf' as a shorthand for oneof without a default argument *)
Notation " 'oneOf' [ x ] " :=
(oneof x (cons x nil)) : qc_scope.
Notation " 'oneOf' [ x ; y ] " :=
(oneof x (cons x (cons y nil))) : qc_scope.
Notation " 'oneOf' [ x ; y ; .. ; z ] " :=
(oneof x (cons x (cons y .. (cons z nil) ..))) : qc_scope.
Notation " 'oneOf' ( x ;; l ) " :=
(oneof x (cons x l)) (at level 1, no associativity) : qc_scope.
(** 'freq' as a shorthund for frequency without a default argument *)
Notation " 'freq' [ x ] " :=
(frequency x (cons x nil)) : qc_scope.
Notation " 'freq' [ ( n , x ) ; y ] " :=
(frequency x (cons (n, x) (cons y nil))) : qc_scope.
Notation " 'freq' [ ( n , x ) ; y ; .. ; z ] " :=
(frequency x (cons (n, x) (cons y .. (cons z nil) ..))) : qc_scope.
Notation " 'freq' ( ( n , x ) ;; l ) " :=
(frequency x (cons (n, x) l)) (at level 1, no associativity) : qc_scope.
*)
End QcDefaultNotation.
(* Note: These will soon be replaced by an ExtLib dependency. *)
Module QcDoNotation.
Notation "'do!' X <- A ; B" :=
(bindGen A (fun X => B))
(at level 200, X name, A at level 100, B at level 200).
Notation "'do\'' X <- A ; B" :=
(bindGen' A (fun X H => B))
(at level 200, X name, A at level 100, B at level 200).
Notation "'doM!' X <- A ; B" :=
(bindGenOpt A (fun X => B))
(at level 200, X name, A at level 100, B at level 200).
End QcDoNotation.
Definition showNat := showNat .
Definition showBool := showBool .
Definition showZ := showZ .
Definition showString := showString .
Definition showList := @showList .
Definition showPair := @showPair .
Definition showOpt := @showOpt .
Definition showEx := @showEx .
Definition nl := nl.
Definition GenOfGenSized := @GenOfGenSized.
Definition genBoolSized := @genBoolSized .
Definition genNatSized := @genNatSized .
Definition genZSized := @genZSized .
Definition genListSized := @genListSized .
Definition genList := @genList .
Definition genOption := @genOption .
Definition genPairSized := @genPairSized .
Definition genPair := @Instances.genPair .
(* TODO: Strings? *)
Definition shrinkBool := shrinkBool.
Definition shrinkNat := shrinkNat .
Definition shrinkZ := shrinkZ .
Definition shrinkList := @shrinkList .
Definition shrinkPair := @shrinkPair .
Definition shrinkOption := @shrinkOption .
Definition ArbitraryOfGenShrink := @ArbitraryOfGenShrink.
Definition Checker := @Checker.
Definition testBool := testBool .
Definition testUnit := testUnit .
Definition forAll := @forAll.
Definition forAllProof := @forAllProof.
Definition forAllShrink := @forAllShrink.
Definition testFun := @testFun .
Definition testProd := @testProd.
Definition testPolyFun := @testPolyFun.
Definition whenFail := @whenFail.
Definition expectFailure := @expectFailure.
Definition collect := @collect.
Definition tag := @tag.
Definition conjoin := @conjoin.
Definition disjoin := @disjoin.
Definition implication := @implication.
Module QcNotation.
Export QcDefaultNotation.
Notation "x ==> y" :=
(implication x y) (at level 55, right associativity)
: Checker_scope.
End QcNotation.
Definition testDec := @testDec .
Definition Dec_neg := @Dec_neg .
Definition Dec_conj := @Dec_conj .
Definition Dec_disj := @Dec_disj .
(* Convenient notation. *)
Notation "P '?'" := (match (@dec P _) with
| left _ => true
| right _ => false
end) (at level 100).
Definition dec_if_dec_eq := @dec_if_dec_eq.
Definition Dec_Eq_implies_DecEq := @Dec_Eq_implies_DecEq.
Definition Dec_eq_unit := @Dec_eq_unit.
Definition Dec_eq_bool := @Dec_eq_bool.
Definition Dec_eq_nat := @Dec_eq_nat.
Definition Dec_eq_Z := @Dec_eq_Z.
Definition Dec_eq_N := @Dec_eq_N.
Definition Dec_eq_opt := @Dec_eq_opt.
Definition Dec_eq_prod := @Dec_eq_prod.
Definition Dec_eq_sum := @Dec_eq_sum.
Definition Dec_eq_list := @Dec_eq_list.
Definition Dec_eq_ascii := @Dec_eq_ascii.
Definition Dec_eq_string := @Dec_eq_string.
(** =================================================================== *)
(** QuickChick toplevel commands and arguments. *)
(** =================================================================== *)
(* Samples a generator. 'g' is of type 'G A' for showable 'A'. *)
(**
Sample g.
*)
(* Runs a test. 'prop' must be 'Checkable'. *)
(**
QuickChick prop.
*)
(* Arguments to customize execution. *)
Record Args :=
MkArgs
{
(* Re-execute a test. *)
(* Default: None *)
replay : option (RandomSeed * nat);
(* Maximum number of successful tests to run. *)
(* Default: 10000 *)
maxSuccess : nat;
(* Maximum number of discards to accept. *)
(* Default: 20000 *)
maxDiscard : nat;
(* Maximum number of shrinks to perform before terminating. *)
(* Default : 1000 *)
maxShrinks : nat;
(* Maximum size of terms to generate (depth). *)
(* Default : 7 *)
maxSize : nat;
(* Verbosity. Note: Doesn't do much... *)
(* Default true. *)
chatty : bool
}.
End ConsistencyCheck.
|
