Prevention of Overflow exception (for SML/NJ) in gensym
authorpaulson
Wed Sep 25 15:03:13 1996 +0200 (1996-09-25)
changeset 20259acc10ac1e1d
parent 2024 909153d8318f
child 2026 0df5a96bf77e
Prevention of Overflow exception (for SML/NJ) in gensym
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Wed Sep 25 11:14:18 1996 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Sep 25 15:03:13 1996 +0200
     1.3 @@ -910,7 +910,7 @@
     1.4        CACM 31 (1988), 1192-1201. 
     1.5      Real number version for systems with 46-bit mantissae
     1.6      Computes  (a*seed) mod m ;  should be applied to integers only! **)
     1.7 -local val a = 16807.0  and  m = 2147483647.0
     1.8 +local val a = 16807.0  and  m = 2147483647.0  (* 2^31 - 1 *)
     1.9  in  fun nextrandom seed =
    1.10            let val t = a*seed
    1.11            in  t - m * real(floor(t/m))  end
    1.12 @@ -935,9 +935,11 @@
    1.13            else  (*i=63*)    "'"
    1.14    in  implode (map char (radixpand (64,n)))  end;
    1.15  
    1.16 -(*Randomly generated identifiers with given prefix; MUST start with a letter*)
    1.17 +(*Randomly generated identifiers with given prefix; MUST start with a letter
    1.18 +    [division by two avoids overflow for ML systems whose maxint is 2^30 - 1 *)
    1.19  fun gensym pre = pre ^ 
    1.20 -                 (#1(newid (floor (!seedr)), seedr := nextrandom (!seedr)))
    1.21 +                 (#1(newid (floor (!seedr/2.0)), 
    1.22 +		     seedr := nextrandom (!seedr)))
    1.23  
    1.24  (*Increment a list of letters like a reversed base 26 number.
    1.25    If head is "z", bumps chars in tail.