123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778(******************************************************************************)(* *)(* Feat *)(* *)(* François Pottier, Inria Paris *)(* *)(* Copyright Inria. All rights reserved. This file is distributed under the *)(* terms of the MIT license, as described in the file LICENSE. *)(******************************************************************************)(* Uniform random generation of large integers. Copied and adapted from Jane
Street's bignum library. *)(* [random state range] chooses a [depth] and generates random values using
[R.bits state], called [1 lsl depth] times and concatenated. The
preliminary result [n] therefore satisfies [0 <= n < 1 lsl (30 lsl depth)].
In order for the random choice to be uniform between [0] and [range-1],
there must exist [k > 0] such that [n < k * range <= 1 lsl (30 lsl depth)].
If so, [n % range] is returned. Otherwise the random choice process is
repeated from scratch.
The [depth] value is chosen so that repeating is uncommon (1 in 1000 or
less). *)openPrintfmoduleMake(Z:BigIntSig.EXTENDED)(R:RandomSig.S)=structletbits_at_depth(depth:int):int=30lsldepthletrange_at_depth(depth:int):Z.t=Z.(onelsl(bits_at_depthdepth))letrecchoose_bit_depth_for_range_fromrangedepth=ifZ.geq(range_at_depthdepth)rangethendepthelsechoose_bit_depth_for_range_fromrange(depth+1)letchoose_bit_depth_for_range(range:Z.t):int=choose_bit_depth_for_range_fromrange0letrecrandom_bigint_at_depth(state:R.State.t)depth:Z.t=ifdepth=0thenZ.of_int(R.State.bitsstate)elseletdepth=depth-1inletprefix=random_bigint_at_depthstatedepthinletsuffix=random_bigint_at_depthstatedepthinZ.(prefixlsl(bits_at_depthdepth)lorsuffix)letrandom_value_is_uniform_in_rangerangedepthn=letk=Z.(range_at_depthdepth/range)inZ.ltnZ.(k*range)letreclarge_random_at_depthstaterangedepth=letresult=random_bigint_at_depthstatedepthinifrandom_value_is_uniform_in_rangerangedepthresultthenZ.(resultmodrange)elselarge_random_at_depthstaterangedepthletlarge_randomstaterange=lettolerance_factor=Z.of_int1000inletdepth=choose_bit_depth_for_rangeZ.(range*tolerance_factor)inlarge_random_at_depthstaterangedepthletrandomstaterange=ifZ.leqrangeZ.zerotheninvalid_arg(sprintf"random: %s is not positive"(Z.to_stringrange))elseifZ.ltrangeZ.(onelsl30)thenZ.of_int(R.State.intstate(Z.to_intrange))elselarge_randomstaterangeletrandomrange=random(R.get_state())rangeend