[m-rev.] for review: extras/quickcheck changes
Peter Moulder
pmoulder at csse.monash.edu.au
Mon Mar 18 11:59:11 AEDT 2002
On Fri, Mar 15, 2002 at 07:25:39PM +1100, Peter Moulder wrote:
> + (char__to_int(Char0, Int) ->
> [...]
> + Weight >= 0 ->
> [and others]
I've fixed up the formatting of if-then-else's in new code, to match
coding_standards.html.
( test_goal ->
blah
;
blahblah
)
(There are a few slightly-wrong if-then-else's in existing code that
I've left as they are, to simplify the patch.)
I've attach the new patch for clarity's sake; though I've already
checked that the only differences between this and the previous patch
are whitespace and in one place adding a pair of parentheses.
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 two floats aren't
independent, usually having nearly the same magnitude.
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.
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 16 Mar 2002 06:17:03 -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,159 @@
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
- then
- irange(-100, 100, Int, BS1, BS)
- else
+ rnd(Temp, BS0, BS1),
+ % Note: Any modifications to this probability distribution should be
+ % accompanied by corresponding updates to tutes/T5.html.
+ ( Temp < 0.5 ->
+ 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.)
+ ; Temp < 0.58 ->
+ Int = int__max_int,
+ BS = BS1
+ ; Temp < 0.65 ->
+ Int = int__min_int,
+ BS = BS1
+ ;
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 16 Mar 2002 06:17:03 -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,98 @@
:- 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,14 +200,14 @@
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.
seed1(N, SNum0, Num0, M1a, M2a, M1, M2) :-
- (N > 0 ->
+ ( N > 0 ->
Num1 = 30903 * SNum0 + (Num0 >> 15),
SNum1 = Num1 /\ ((1 << 15) - 1),
( N >= 9 ->
@@ -187,29 +223,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 +272,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 +337,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 16 Mar 2002 06:17:03 -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 16 Mar 2002 06:17:03 -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