[m-rev.] for review: extras/quickcheck changes
Peter Moulder
pmoulder at csse.monash.edu.au
Fri Mar 15 19:25:39 AEDT 2002
This is a follow-up from the `for review: extras/quickcheck comments'
post made a while back (Feb 22-24).
The below patch acts on the comments made in said post, and probably
some other things. It corrects various issues in the selection of
random values for testing.
I haven't done any testing other than compiling & running the existing
minimal test_qcheck program. My changes should be just in the random
data generation rather than the test predicates, which suggests that any
bugs there are have a relatively low impact on usefulness of the module.
Of course, ideally we should add lots of tests to quickcheck, if only to
get a feel for how good the provided interface is (like writing the
mercury compiler in mercury) and as example code. But that can wait for
another time.
Looking at the patch, the int/vec_digit_nr type duality is perhaps a bit
ugly, but from a runtime perspective the int version is used only by
rnd__init. Anyway, I'm leaving that as is, as it appears that
developers aren't currently looking at the code anyway, so
working-but-verbose code isn't too big an issue. Though I guess I could
probably safely just remove that part from the patch, reverting to the
fully-int code, if the reviewer would prefer. The reason for starting
the vec_digit_nr modification was to remove the redundant runtime checks
of the digit. Possibly could mark as inline: most callers pass a
constant digit number. What do all those bound mode lines do, btw?
pjm.
Estimated hours taken: 15
Various changes to random data generation functions.
extras/quickcheck/qcheck.m:
* Remove now-unused next/4 predicate. (Previously it was being
called for 31 bits of randomness even though it provided no more
than 30 bits.)
* rand_int: Increase the probability of int__min_int and
int__max_int.
* rand_allint: Previously generated a range of less than 2**31,
regardless of int size. Now generates the full 2**32 or 2**64
range of int values.
* rand_char: More efficient by generating the correct range
[char__min_char_value .. char__max_char_value] rather than
looping until char__to_int succeeds.
* rand_float: generate a wider range of floats, almost 64 bits
worth (or however wide the underlying float type is) instead
of 30 bits mantissa + 8 (sic) bits exponent plus 1 sign bit
previously.
extras/quickcheck/rnd.m:
* New pred rnd30/3 providing direct access to a limb of
randomness.
* gaussian: document that the generated floats aren't
independent.
Prevent a runtime error if the initial frange chose 0.0.
* irange: Work even if Max = int__max_int.
* frange: Check `Min < Max' precondition.
* shuffle: Implement using the more efficient & more thorough
random__permutation.
* oneof: Check non-empty-list precondition.
* wghtd_oneof: Check positive-weight-sum and
all-weights-non-negative preconditions.
Fix the selection probabilities. (Previously the first
element was over-represented due to off-by-one error.)
* Get rid of casting wrappers rfloat and misleadingly-named
rint. Callers replaced with float/1 and floor_to_int/1.
extras/quickcheck/tutes/T1.html:
* Code clarifications. Grammar: s/satisfactory/satisfactorily/.
extras/quickcheck/tutes/T5.html:
* Update the descriptions of the probability distributions to
correspond to the qcheck.m changes.
* Remove the code that was copied from qcheck.m: the code
doesn't add much to the descriptions, and it could easily fall
out of date.
Index: qcheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/extras/quickcheck/qcheck.m,v
retrieving revision 1.2
diff -d -u -r1.2 qcheck.m
--- qcheck.m 31 Jul 2001 13:47:32 -0000 1.2
+++ qcheck.m 15 Mar 2002 06:26:22 -0000
@@ -289,7 +289,7 @@
SpecificFrequency, GeneralFrequency, []).
% qcheck/8 first seed the random number on local time, then it
- % generates the reqiured inputs for the invariant function and runs
+ % generates the required inputs for the invariant function and runs
% it. A table of test results are shown at the end.
qcheck(TestFunction, Name, TestCount, SpecificFrequency,
GeneralFrequency, Generators) -->
@@ -803,63 +803,162 @@
gen_arg_list(Types, Fs, GF, UserGenerators, Univs, RS1, RS).
%---------------------------------------------------------------------------%
-
- % generate an int of N Bits
-:- pred next(int, int, rnd, rnd).
-:- mode next(in, out, in, out) is det.
-next(N, Bits, Rnd0, Rnd) :-
- rnd(F, Rnd0, Rnd),
- Range = pow(2.0, N) - 1.0,
- Bits = round_to_int(F * Range).
% generate int
rand_int(BS0, BS) = Int :-
- Temp = rand_allint(BS0, BS1) rem 2,
- (if Temp = 0
+ rnd(Temp, BS0, BS1),
+ % Note: Any modifications to this probability distribution should be
+ % accompanied by corresponding updates to tutes/T5.html.
+ (if Temp < 0.5
then
- irange(-100, 100, Int, BS1, BS)
+ rnd__irange(-100, 100, Int, BS1, BS)
+
+ % We increase the probability of int__max_int and int__min_int,
+ % since these values are very subject to bugs (e.g. due to
+ % assuming that X + 1 > X). (E.g. all implementations of
+ % `between' (it occurs in several places) in the mercury
+ % distribution are buggy for Max == int__max_int.)
+ else if Temp < 0.58
+ then
+ Int = int__max_int,
+ BS = BS1
+ else if Temp < 0.65
+ then
+ Int = int__min_int,
+ BS = BS1
else
Int = rand_allint(BS1, BS)
).
+
% generate int
rand_allint(BS0, BS) = Int :-
- next(1, Sign, BS0, BS1),
- next(31, TempInt, BS1, BS),
- ( Sign > 0 ->
- Int = TempInt
+ rnd30(RndA, BS0, BS1),
+ rnd30(RndB, BS1, BS2),
+
+ % Note that in Mercury, unlike C, the `<<' operator does
+ % the right thing for negative shift amounts.
+
+ A30 = (RndA << (int__bits_per_int - 30 - 1)),
+ B30 = (RndB << (int__bits_per_int - 60 - 1)),
+ ( int__bits_per_int =< 30 ->
+ error("bits_per_int too small")
+ ; int__bits_per_int =< 60 ->
+ BS = BS2,
+ NonSign = A30 \/ B30,
+ SignBit = B30 /\ 1
+ ; int__bits_per_int =< 90 ->
+ rnd30(RndC, BS2, BS),
+ C30 = (RndC << (int__bits_per_int - 90 - 1)),
+ NonSign = A30 \/ B30 \/ C30,
+ SignBit = C30 /\ 1
;
- Int = -TempInt
+ error("bits_per_int too big")
+ ),
+ ( SignBit = 0 ->
+ Int = NonSign
+ ;
+ Int = \ NonSign
).
+
% generate char
rand_char(RS0, RS) = Char :-
- Int = rand_allint(RS0, RS1) rem 1000,
- (if char__to_int(Char0, Int)
- then
- Char = Char0,
- RS = RS1
- else
- Char = rand_char(RS1, RS)
- ).
+ % Note: Any modifications to this probability distribution should be
+ % accompanied by corresponding updates to tutes/T5.html.
+ rnd__irange(char__min_char_value, char__max_char_value, Int, RS0, RS),
+ (char__to_int(Char0, Int) ->
+ Char = Char0
+ ;
+ error("can't happen: bad int to char conversion")
+ ).
- % generate float
+
+ % generate float.
+ %
+ % Never generates infinities, NaN or -0.0: at the time of
+ % writing, Mercury has known bugs handling these values,
+ % so there's little point testing them here.
+ %
+ % However, we do generate subnormalized numbers (including zero).
+ %
+ % XXX: We ought to assign greater probability to:
+ % - zero
+ % - subnormalized numbers generally
+ % - numbers whose significand (the explicit 52-bit part) is 0, 1, or
+ % all-bits-1; and especially the following:
+ % - the highest subnormalized number (and its negative)
+ % - the lowest positive subnormalized number (and its negative)
+ % - the lowest positive normalized number (and its negative)
+ % - Have I missed anything?
+ %
rand_float(BS0, BS) = Flt :-
- next(31, Mant0, BS0, BS1),
- next(1, Sign, BS1, BS2),
- ( Sign > 0 ->
- Mant = Mant0
- ;
- Mant = -Mant0
- ),
- next(7, Exp, BS2, BS3),
- next(1, ExpSign, BS3, BS),
- Flt0 = float(Mant) * pow(2.0, Exp),
- ( ExpSign > 0, Flt0 \= 0.0 ->
- Flt = 1.0/Flt0
- ;
- Flt = Flt0
- ).
+ rnd30(MantHi, BS0, BS1),
+ rnd30(MantLo, BS1, BS2),
+ rnd__irange(float__min_exponent - 1, float__max_exponent, Exp, BS2, BS),
+ Flt = construct_float(MantHi, MantLo, Exp).
+
+:- func construct_float(int, int, int) = float.
+construct_float(MantHi, MantLo, Exp) = Flt :-
+ % +1 or -1.
+ SignScalar = (MantLo /\ 2) - 1,
+ % (We check in the sanity checks below that at least the low two bits
+ % of MantLo will be discarded when assigning to the significand, so
+ % it's fine to use this bit independently.)
+
+ ExpScalar = float__pow(2.0, Exp),
+
+ % Mant0 is in [0.0, 1.0).
+ RShift30 = 1.0 / float(1 << 30),
+ Mant0 = ((float(MantHi)
+ + (float(MantLo)
+ * RShift30))
+ * RShift30),
+ ( Exp < float__min_exponent ->
+ % Mant in [0.0, 1.0).
+ Mant = Mant0
+ ;
+ % Mant in [0.5, 1.0).
+ Mant = (1.0 + Mant0) * 0.5
+ ),
+
+ % A check against java.lang.Double.longBitsToDouble documentation:
+ % Exp in [-1022, 1024]; e in [0, 0x7fe].
+ % s = SignScalar; m = Mant << 53; e = Exp + 1022.
+ % s * m * 2**(e - 1075)
+ % = SignScalar * (Mant << 53) * 2**(Exp + 1022 - 1075)
+ % = SignScalar * (Mant * 2**53) * 2**(Exp - 53)
+ % = SignScalar * Mant * 2**Exp
+ % = SignScalar * Mant * ExpScalar
+
+ Flt0 = float(SignScalar) * Mant * ExpScalar,
+
+ (
+ % Checks on inputs.
+ not (
+ (MantHi /\ \ ((1 << 30) - 1) = 0),
+ (MantLo /\ \ ((1 << 30) - 1) = 0),
+ (float__min_exponent - 1 =< Exp),
+ (Exp =< float__max_exponent)
+ )
+ ->
+ error("inputs out of range")
+ ;
+ % Sanity checks.
+ not (
+ (SignScalar = 1 ; SignScalar = -1),
+ (0.0 =< Mant, Mant < 1.0),
+ (Exp = float__min_exponent - 1 ; 0.5 =< Mant),
+ (ExpScalar \= ExpScalar / 2.0),
+ (Mant = 0.0 ; Flt0 / 2.0 \= Flt0),
+ (float__mantissa_digits =< 2 * 30 - 2)
+ )
+ ->
+ error("bug in float generation")
+ ;
+ Flt = Flt0
+ ).
+
% generate string
rand_string(RS0, RS) = X :-
Index: rnd.m
===================================================================
RCS file: /home/mercury1/repository/mercury/extras/quickcheck/rnd.m,v
retrieving revision 1.1
diff -d -u -r1.1 rnd.m
--- rnd.m 31 May 2001 02:08:45 -0000 1.1
+++ rnd.m 15 Mar 2002 06:26:22 -0000
@@ -11,6 +11,15 @@
%
% The original source is included at the end of the module as a reference.
%
+
+% XXX: N.B. This implementation assumes that overflowing an int will silently
+% give the result that is equal to the real result in modulo pow(2,
+% int__bits_per_int) arithmetic; whereas int.m says that overflowing gives
+% undefined results. It would be nice if int.m (or whatever type) provided
+% some functions corresponding to unsigned arithmetic in C.
+% (C's int type has even fewer behaviour guarantees than Mercury's int type,
+% but its `unsigned' type is guaranteed to operate in modulo 2**n arithmetic.)
+
%---------------------------------------------------------------------------%
:- module rnd.
@@ -25,15 +34,23 @@
:- pred rnd__init(int, rnd).
:- mode rnd__init(in, out) is det.
- % get a random float on the range [0, 1)
+ % Get a random int in the range [0, 1<<30).
+:- pred rnd30(int, rnd, rnd).
+:- mode rnd30(out, in, out) is det.
+
+ % Get a random float in the range [0, 1).
+ % Gives about 30 bits of randomness
+ % (assuming float__mantissa_digits >= 30).
:- pred rnd(float, rnd, rnd).
:- mode rnd(out, in, out) is det.
- % get a random int on the range [Lower, Upper]
+ % Get a random int in the range [Lower, Upper].
+ % Requires Lower =< Upper.
:- pred irange(int, int, int, rnd, rnd).
:- mode irange(in, in, out, in, out) is det.
% get a random float on the range [Lower, Upper)
+ % Requires Lower < Upper.
:- pred frange(float, float, float, rnd, rnd).
:- mode frange(in, in, out, in, out) is det.
@@ -42,15 +59,21 @@
:- mode shuffle(in, out, in, out) is det.
% get a random element of a list.
+ % Requires that the list of options be non-empty.
:- pred oneof(list(T), T, rnd, rnd).
:- mode oneof(in, out, in, out) is det.
% get a random element of a weighted list.
+ % Requires that each weight be non-negative and that the sum of the
+ % weights be strictly positive.
:- pred wghtd_oneof(list(pair(int, T)), T, rnd, rnd).
:- mode wghtd_oneof(in, out, in, out) is det.
% gaussian(X, Y, Rnd0, Rnd)
% generate a pair of gaussian deviates `X' and `Y'.
+ % (Note that X and Y aren't independent in magnitude;
+ % usually their exponents are very close to each other,
+ % even when either X or Y is very far from zero.)
:- pred gaussian(float, float, rnd, rnd).
:- mode gaussian(out, out, in, out) is det.
@@ -59,85 +82,97 @@
:- implementation.
:- import_module math, require.
+:- use_module random. % For random__permutation.
irange(Min, Max, Val, R0, R) :-
- frange(rfloat(Min), rfloat(Max+1), FVal, R0, R),
- Val = rint(FVal).
+ (Min =< Max ->
+ frange(float(Min), float(Max) + 1.0, FVal, R0, R),
+ Val = floor_to_int(FVal)
+ ;
+ error("Min > Max")
+ ).
frange(Min, Max, Val, R0, R) :-
- rnd(J, R0, R),
- Val = J*(Max - Min)+Min.
+ (Min < Max ->
+ rnd(J, R0, R),
+ Val = J*(Max - Min)+Min
+ ;
+ error("Min >= Max")
+ ).
shuffle(Ins, Outs, R0, R) :-
- list__length(Ins, N),
- shuffle2(N, Ins, [], T0, R0, R1),
- shuffle2(N, T0, [], T1, R1, R2),
- shuffle2(N, T1, [], T2, R2, R3),
- shuffle2(N, T2, [], T3, R3, R4),
- shuffle2(N, T3, [], U, R4, R5),
- shuffle2(N, U, [], Outs, R5, R).
+ rnd30(Seed, R0, R),
+ random__init(Seed, Random),
+ random__permutation(Ins, Outs, Random, _Random1).
-:- pred shuffle2(int, list(T), list(T), list(T), rnd, rnd).
-:- mode shuffle2(in, in, in, out, in, out) is det.
-shuffle2(N, Ins, Acc0, Acc, R0, R) :-
- ( N > 0 ->
- irange(0, N-1, J, R0, R1),
- delnth(Ins, J, Rest, T),
- shuffle2(N-1, Rest, [T|Acc0], Acc, R1, R)
+oneof(Things, Thing, R0, R) :-
+ (Things = [] ->
+ error("empty selection list")
;
- Acc = Acc0,
- R = R0
+ list__length(Things, Num),
+ irange(0, Num-1, X, R0, R),
+ list__index0_det(Things, X, Thing)
).
-:- pred delnth(list(T), int, list(T), T).
-:- mode delnth(in, in, out, out) is det.
-
-delnth([], _, _, _) :-
- error("delnth: no enough elems!").
-delnth([X|Xs], N, Zs, Z) :-
- ( N =< 0 ->
- Z = X,
- Zs = Xs
+wghtd_oneof(WghtdThings, Thing, R0, R) :-
+ cumu(WghtdThings, 0, Sum),
+ (Sum =< 0 ->
+ error("must have positive total weight")
;
- Zs = [X|Ys],
- delnth(Xs, N-1, Ys, Z)
+ irange(1, Sum, X, R0, R),
+ pick(WghtdThings, X, Thing)
).
-oneof(Things, Thing, R0, R) :-
- list__length(Things, Num),
- irange(0, Num-1, X, R0, R),
- list__index0_det(Things, X, Thing).
-
-wghtd_oneof(WghtdThings, Thing, R0, R) :-
- cumu(WghtdThings, 0, Sum),
- irange(0, Sum, X, R0, R),
- pick(WghtdThings, X, Thing).
:- pred cumu(list(pair(int, T)), int, int).
:- mode cumu(in, in, out) is det.
cumu([], Sum, Sum).
-cumu([X - _T|Rest0], Sum, Sum1) :-
- cumu(Rest0, X+Sum, Sum1).
+cumu([Weight - _Thing|Rest0], Sum0, Sum) :-
+ Weight >= 0 ->
+ cumu(Rest0, Weight + Sum0, Sum)
+ ;
+ error("negative weight").
+
:- pred pick(list(pair(int, T)), int, T).
:- mode pick(in, in, out) is det.
+% Requires that P >= 1 and
+% some[SumWeight] (cumu(SelectionList, 0, SumWeight), P =< SumWeight).
pick([], _, _) :-
error("pick: no things to pick from!").
-pick([N - T|Rest], P, Thing) :-
- ( N >= P ->
- Thing = T
+pick([Weight0 - Thing0|Rest], P, Thing) :-
+ ( Weight0 >= P ->
+ Thing = Thing0
;
- pick(Rest, P - N, Thing)
+ pick(Rest, P - Weight0, Thing)
).
gaussian(X, Y, Rnd0, Rnd) :-
frange(-1.0, 1.0, V1, Rnd0, Rnd1),
frange(-1.0, 1.0, V2, Rnd1, Rnd2),
R = V1*V1 + V2*V2,
- ( R >= 1.0, R \= 0.0 ->
+ (
+ ( R >= 1.0 ; R = 0.0 )
+
+ % [pjm]: The above used to be `R >= 1.0, R \= 0.0'.
+ % I believe that the current code is the intended test,
+ % with the intention that ln(R) be finite and non-zero.
+
+ % Note that ln(0.0) in Mercury gives a runtime error,
+ % unlike in C (and probably IEEE) where it returns -infinity.
+
+ % I wonder whether we should change the `>=' to `>' though:
+ % R=1.0 gives Fac = -0.0. (Yes, apparently sqrt(-0.0) = -0.0,
+ % both in C and Mercury.) With the existing implementation
+ % (i.e. rejecting 1.0), the only way that X (Y) can be zero is
+ % if V1 (V2) is zero, which is very rare (1 in 2**30) whereas
+ % zero is the most common number in a real gaussian
+ % distribution, and if anything zero ought to be
+ % overrepresented when used by quickcheck.
+ ->
gaussian(X, Y, Rnd2, Rnd)
;
Fac = sqrt(-2.0 * ln(R) / R),
@@ -164,8 +199,8 @@
M1a = vec(0, 0, 0, 0, 0, 0, 0, 0, 0, 0),
M2a = vec(0, 0, 0, 0, 0, 0, 0, 0, 0, 0),
seed1(17, SN, N, M1a, M2a, M1b, M2b),
- set(M1b, 0, (M1b ** 0) /\ ((1 << 15) - 1), M1),
- set(M2b, 0, (M2b ** 0) /\ ((1 << 15) - 1), M2).
+ setd(M1b, d0, (M1b ** d0) /\ ((1 << 15) - 1), M1),
+ setd(M2b, d0, (M2b ** d0) /\ ((1 << 15) - 1), M2).
:- pred seed1(int, int, int, vec, vec, vec, vec).
:- mode seed1(in, in, in, in, in, out, out) is det.
@@ -187,29 +222,45 @@
M2 = M2a
).
-rnd(Res, rnd(M1a, M2a, _Seed0), rnd(M1d, M2d, Seed1)) :-
+
+rnd30(Result, Rnd0, Rnd):-
+ rnd_update(Rnd0, Rnd),
+ Rnd = rnd(_M1, _M2, Seed),
+ ( Seed /\ \((1 << 30) - 1) = 0 ->
+ Result = Seed
+ ;
+ error("bug: rnd30 returning more than 30 bits")
+ ).
+
+
+rnd(Result, Rnd0, Rnd):-
+ rnd_update(Rnd0, Rnd),
+ Rnd = rnd(_M1, _M2, Seed),
+ Result = float(Seed) / float(1 << 30).
+
+:- pred rnd_update(rnd, rnd).
+:- mode rnd_update(in, out) is det.
+rnd_update(rnd(M1a, M2a, _Seed0), rnd(M1d, M2d, Seed1)) :-
shift(M1a, M1b),
shift(M2a, M2b),
- N1a = (M1b ** 0),
- N2a = (M2b ** 0),
-
- N1b = N1a + 1941 * (M1b ** 2) + 1860 * (M1b ** 3) + 1812 * (M1b ** 4)
- + 1776 * (M1b ** 5) + 1492 * (M1b ** 6) + 1215 * (M1b ** 7)
- + 1066 * (M1b ** 8) + 12013 * (M1b ** 9),
+ N1a = (M1b ** d0),
+ N2a = (M2b ** d0),
- N2b = N2a + 1111 * (M2b ** 2) + 2222 * (M2b ** 3) + 3333 * (M2b ** 4)
- + 4444 * (M2b ** 5) + 5555 * (M2b ** 6) + 6666 * (M2b ** 7)
- + 7777 * (M2b ** 8) + 9272 * (M2b ** 9),
+ N1b = N1a + 1941 * (M1b ** d2) + 1860 * (M1b ** d3) + 1812 * (M1b ** d4)
+ + 1776 * (M1b ** d5) + 1492 * (M1b ** d6) + 1215 * (M1b ** d7)
+ + 1066 * (M1b ** d8) + 12013 * (M1b ** d9),
- set(M1b, 0, (N1b >> 15) /\ ((1 << 15) - 1), M1c),
- set(M2b, 0, (N2b >> 15) /\ ((1 << 15) - 1), M2c),
+ N2b = N2a + 1111 * (M2b ** d2) + 2222 * (M2b ** d3) + 3333 * (M2b ** d4)
+ + 4444 * (M2b ** d5) + 5555 * (M2b ** d6) + 6666 * (M2b ** d7)
+ + 7777 * (M2b ** d8) + 9272 * (M2b ** d9),
- set(M1c, 1, N1b /\ ((1 << 15) - 1), M1d),
- set(M2c, 1, N2b /\ ((1 << 15) - 1), M2d),
+ setd(M1b, d0, (N1b >> 15) /\ ((1 << 15) - 1), M1c),
+ setd(M2b, d0, (N2b >> 15) /\ ((1 << 15) - 1), M2c),
- Seed1 = ((M1d ** 1) << 15) + (M2d ** 1),
+ setd(M1c, d1, N1b /\ ((1 << 15) - 1), M1d),
+ setd(M2c, d1, N2b /\ ((1 << 15) - 1), M2d),
- Res = rfloat(Seed1)/rfloat((1 << 30) - 1).
+ Seed1 = ((M1d ** d1) << 15) + (M2d ** d1).
:- pred shift(vec, vec).
:- mode shift(in, out) is det.
@@ -220,39 +271,57 @@
%---------------------------------------------------------------------------%
-:- func (vec ** int) = int.
+% Get the compiler to do the checking for us.
+:- type vec_digit_nr
+ ---> d0 ; d1 ; d2 ; d3 ; d4 ; d5 ; d6 ; d7 ; d8 ; d9.
+
+:- func (vec ** vec_digit_nr) = int.
:- mode ((in ** in) = out) is det.
-:- mode ((in ** in(bound(0))) = out) is det.
-:- mode ((in ** in(bound(1))) = out) is det.
-:- mode ((in ** in(bound(2))) = out) is det.
-:- mode ((in ** in(bound(3))) = out) is det.
-:- mode ((in ** in(bound(4))) = out) is det.
-:- mode ((in ** in(bound(5))) = out) is det.
-:- mode ((in ** in(bound(6))) = out) is det.
-:- mode ((in ** in(bound(7))) = out) is det.
-:- mode ((in ** in(bound(8))) = out) is det.
-:- mode ((in ** in(bound(9))) = out) is det.
+:- mode ((in ** in(bound(d0))) = out) is det.
+:- mode ((in ** in(bound(d1))) = out) is det.
+:- mode ((in ** in(bound(d2))) = out) is det.
+:- mode ((in ** in(bound(d3))) = out) is det.
+:- mode ((in ** in(bound(d4))) = out) is det.
+:- mode ((in ** in(bound(d5))) = out) is det.
+:- mode ((in ** in(bound(d6))) = out) is det.
+:- mode ((in ** in(bound(d7))) = out) is det.
+:- mode ((in ** in(bound(d8))) = out) is det.
+:- mode ((in ** in(bound(d9))) = out) is det.
( Vec ** Ind ) = Res :-
Vec = vec(A, B, C, D, E, F, G, H, I, J),
(
- ( Ind = 0, Res0 = A
- ; Ind = 1, Res0 = B
- ; Ind = 2, Res0 = C
- ; Ind = 3, Res0 = D
- ; Ind = 4, Res0 = E
- ; Ind = 5, Res0 = F
- ; Ind = 6, Res0 = G
- ; Ind = 7, Res0 = H
- ; Ind = 8, Res0 = I
- ; Ind = 9, Res0 = J
- )
- ->
+ ( Ind = d0, Res0 = A
+ ; Ind = d1, Res0 = B
+ ; Ind = d2, Res0 = C
+ ; Ind = d3, Res0 = D
+ ; Ind = d4, Res0 = E
+ ; Ind = d5, Res0 = F
+ ; Ind = d6, Res0 = G
+ ; Ind = d7, Res0 = H
+ ; Ind = d8, Res0 = I
+ ; Ind = d9, Res0 = J
+ ),
Res = Res0
- ;
- error("**: out of range")
).
+:- pred setd(vec, vec_digit_nr, int, vec).
+:- mode setd(in, in, in, out) is det.
+setd(vec(A, B, C, D, E, F, G, H, I, J), Ind, V, Vec) :-
+ (
+ Ind = d0, Vec = vec(V, B, C, D, E, F, G, H, I, J)
+ ; Ind = d1, Vec = vec(A, V, C, D, E, F, G, H, I, J)
+ ; Ind = d2, Vec = vec(A, B, V, D, E, F, G, H, I, J)
+ ; Ind = d3, Vec = vec(A, B, C, V, E, F, G, H, I, J)
+ ; Ind = d4, Vec = vec(A, B, C, D, V, F, G, H, I, J)
+ ; Ind = d5, Vec = vec(A, B, C, D, E, V, G, H, I, J)
+ ; Ind = d6, Vec = vec(A, B, C, D, E, F, V, H, I, J)
+ ; Ind = d7, Vec = vec(A, B, C, D, E, F, G, V, I, J)
+ ; Ind = d8, Vec = vec(A, B, C, D, E, F, G, H, V, J)
+ ; Ind = d9, Vec = vec(A, B, C, D, E, F, G, H, I, V)
+ ).
+
+% Used only by rnd__init (via seed1).
:- pred set(vec, int, int, vec).
:- mode set(in, in, in, out) is det.
:- mode set(in, in(bound(0)), in, out) is det.
@@ -267,32 +336,28 @@
:- mode set(in, in(bound(9)), in, out) is det.
set(Vec0, Ind, V, Vec) :-
- Vec0 = vec(A, B, C, D, E, F, G, H, I, J),
+ setd(Vec0, int2vec_digit_nr(Ind), V, Vec).
+
+:- func int2vec_digit_nr(int) = vec_digit_nr.
+int2vec_digit_nr(Int) = Dig :-
(
- ( Ind = 0, Vec1 = vec(V, B, C, D, E, F, G, H, I, J)
- ; Ind = 1, Vec1 = vec(A, V, C, D, E, F, G, H, I, J)
- ; Ind = 2, Vec1 = vec(A, B, V, D, E, F, G, H, I, J)
- ; Ind = 3, Vec1 = vec(A, B, C, V, E, F, G, H, I, J)
- ; Ind = 4, Vec1 = vec(A, B, C, D, V, F, G, H, I, J)
- ; Ind = 5, Vec1 = vec(A, B, C, D, E, V, G, H, I, J)
- ; Ind = 6, Vec1 = vec(A, B, C, D, E, F, V, H, I, J)
- ; Ind = 7, Vec1 = vec(A, B, C, D, E, F, G, V, I, J)
- ; Ind = 8, Vec1 = vec(A, B, C, D, E, F, G, H, V, J)
- ; Ind = 9, Vec1 = vec(A, B, C, D, E, F, G, H, I, V)
+ ( Int = 0, Dig0 = d0
+ ; Int = 1, Dig0 = d1
+ ; Int = 2, Dig0 = d2
+ ; Int = 3, Dig0 = d3
+ ; Int = 4, Dig0 = d4
+ ; Int = 5, Dig0 = d5
+ ; Int = 6, Dig0 = d6
+ ; Int = 7, Dig0 = d7
+ ; Int = 8, Dig0 = d8
+ ; Int = 9, Dig0 = d9
)
->
- Vec = Vec1
+ Dig = Dig0
;
- error("set: out of range")
+ error("int2vec_degit_nr: out of range")
).
-%---------------------------------------------------------------------------%
-
-:- func rfloat(int) = float.
-:- pragma c_code(rfloat(I::in) = (F::out), "F = I;").
-
-:- func rint(float) = int.
-:- pragma c_code(rint(F::in) = (I::out), "I = F;").
%---------------------------------------------------------------------------%
%
Index: tutes/T1.html
===================================================================
RCS file: /home/mercury1/repository/mercury/extras/quickcheck/tutes/T1.html,v
retrieving revision 1.3
diff -d -u -r1.3 T1.html
--- tutes/T1.html 24 Feb 2002 23:28:49 -0000 1.3
+++ tutes/T1.html 15 Mar 2002 06:26:22 -0000
@@ -153,9 +153,9 @@
<pre>
testing2(Xs, Ys) = (Left `===` Right) :-
nrev2((Xs ++ Ys), Left),
- nrev2(Ys, Part_a),
- nrev2(Ys, Part_b),
- Right = Part_a ++ Part_b.
+ nrev2(Ys, YRev),
+ nrev2(Xs, XRev),
+ Right = YRev ++ XRev.
</pre>
Above code is effectively the same as testing/2, however it requires a few extra
lines to extract the intermediate values, (use1.m):
@@ -189,9 +189,9 @@
:- func testing2(list(int), list(int)) = property.
testing2(Xs, Ys) = (Left `===` Right) :-
nrev2((Xs ++ Ys), Left),
- nrev2(Ys, Part_a),
- nrev2(Xs, Part_b),
- Right = Part_a ++ Part_b.
+ nrev2(Ys, YRev),
+ nrev2(Xs, XRev),
+ Right = YRev ++ XRev.
</pre></tr></table>
An alternative to writing a separate invariant function is to
use Mercury's syntax for higher order terms. When doing this,
@@ -254,7 +254,7 @@
<p>QuickCheck does not care what happens inside Invariant_Function_X. If
the output does not contain 'flag:no', the invariant function is assumed to
-pass the testcase satisfactory.
+pass the testcase satisfactorily.
<p>See <a href="T4.html">part 4 of the tutorial</a> to get the details
on each individual flag.
Index: tutes/T5.html
===================================================================
RCS file: /home/mercury1/repository/mercury/extras/quickcheck/tutes/T5.html,v
retrieving revision 1.3
diff -d -u -r1.3 T5.html
--- tutes/T5.html 24 Feb 2002 23:28:49 -0000 1.3
+++ tutes/T5.html 15 Mar 2002 06:26:22 -0000
@@ -40,87 +40,39 @@
before compiling.
<p>
-The default generator for int is rand_int/2, which has distribution:
+The default generator for int is <code>rand_int</code>/2, which has distribution:
<table>
-<tr>
-<td> 50%
-<td> even distribution in the range [-100, 100]
-<tr>
-<td> 50%
-<td> even distribution in the range (-2^31, 2^31)
- <br>(This will probably change to [int__min_int, int__max_int] in
- a future version.)
+<tr><td> 8% <td><code>int__max_int</code>
+<tr><td> 7% <td><code>int__min_int</code>
+<tr><td> 4% <td>0
+<tr><td>46% <td>uniform distribution in the range [-100, 100]
+<tr><td>35% <td>uniform distribution in the range
+ [<code>int__min_int</code>, <code>int__max_int</code>]
</table>
-<table border=0 width="100%" bgcolor="#eeeee0"><tr><td><pre>
-:- func rand_int(rnd, rnd) = int.
-:- mode rand_int(in, out) = out is det.
-rand_int(BS0, BS) = Int :-
- Temp = rand_allint(BS0, BS1) rem 2,
- (if Temp = 0
- then
- irange(-100, 100, Int, BS1, BS)
- else
- Int = rand_allint(BS1, BS)
- ).
+<p>The default for <code>char</code> is <code>rand_char</code>/2,
+which currently generates characters with a uniform distribution
+over [<code>char__min_char_value</code>, <code>char__max_char_value</code>].
+(Maybe in future a non-uniform distribution will be used, as is done for
+<code>rand_int</code>.)
-:- func rand_allint(rnd, rnd) = int.
-:- mode rand_allint(in, out) = out is det.
-rand_allint(BS0, BS) = Int :-
- next(1, Sign, BS0, BS1),
- next(31, TempInt, BS1, BS),
- ( Sign > 0 ->
- Int = TempInt
- ;
- Int = -TempInt
- ).
-</pre></tr></table>
-Default for char is rand_char/2, with even spread over
-char__to_int(Char, X) where X is (-1000, 1000).
-<!-- Maybe insert `∩ {I : some[C] char__to_int(C, I)}' or English comment. -->
-<table border=0 width="100%" bgcolor="#eeeee0"><tr><td><pre>
-:- func rand_char(rnd, rnd) = char.
-:- mode rand_char(in, out) = out is det.
-rand_char(RS0, RS) = Char :-
- Int = rand_allint(RS0, RS1) rem 1000,
- (if char__to_int(Char0, Int)
- then
- Char = Char0,
- RS = RS1
- else
- Char = rand_char(RS1, RS)
- ).
-</pre></tr></table>
-Default for float is rand_float/2, which has roughly even
-distribution over all discrete values for a 32-bit float.
-If machine is less then 32bits, overfloat occurs. It should still
-cover all possible values, but may alter distribution.
-If machine is more than 32bits, rand_float/2 will miss some values
-but retains even distribution.
+<p>The default for <code>float</code> is <code>rand_float</code>/2,
+which more or less generates a random 64-bit value
+and returns the float with that bit-pattern representation;
+except that currently it never returns certain "strange" values like
+NaN,
++/-infinity,
+or negative zero.
+(This may change once Mercury's float support stabilizes.)
-<table border=0 width="100%" bgcolor="#eeeee0"><tr><td><pre>
-:- func rand_float(rnd, rnd) = float.
-:- mode rand_float(in, out) = out is det.
-rand_float(BS0, BS) = Flt :-
- next(31, Mant0, BS0, BS1),
- next(1, Sign, BS1, BS2),
- ( Sign > 0 ->
- Mant = Mant0
- ;
- Mant = -Mant0
- ),
- next(7, Exp, BS2, BS3),
- next(1, ExpSign, BS3, BS),
- Flt0 = float(Mant) * pow(2.0, Exp),
- ( ExpSign > 0, Flt0 \= 0.0 ->
- Flt = 1.0/Flt0
- ;
- Flt = Flt0
- ).
-</pre></tr></table>
-Default for string is rand_string/2, each element is generated by
-rand_char/2.
+<p>Maybe a future version of <code>rand_float</code>
+will assign greater probability to
+values to values most likely to cause bugs (see comments in the source code).
+
+
+<p>The default for string is <code>rand_string</code>/2,
+each element is generated by <code>rand_char</code>/2.
<table summary="The probability of the string having length i is 0.9^i * 0.1.">
<tr>
<td>0.9^0 * 0.1
@@ -179,6 +131,8 @@
junk(A, B, C, D) =
{A,B,C,D} `>>>` [yes].
</pre></tr></table>
+
+<p>
There are a few thing to note about use51.m :
<pre>
qcheck(qcheck__f(junk), "just to show the inputs", 5, [], []).
--------------------------------------------------------------------------
mercury-reviews mailing list
post: mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------
More information about the reviews
mailing list