src/Pure/library.ML
changeset 2003 b48f066d52dc
parent 1628 60136fdd80c4
child 2025 9acc10ac1e1d
     1.1 --- a/src/Pure/library.ML	Mon Sep 23 17:41:57 1996 +0200
     1.2 +++ b/src/Pure/library.ML	Mon Sep 23 17:42:56 1996 +0200
     1.3 @@ -905,13 +905,40 @@
     1.4        in (x, zs) :: map step qs end;
     1.5  
     1.6  
     1.7 +(** Recommended by Stephen K. Park and Keith W. Miller, 
     1.8 +      Random number generators: good ones are hard to find,
     1.9 +      CACM 31 (1988), 1192-1201. 
    1.10 +    Real number version for systems with 46-bit mantissae
    1.11 +    Computes  (a*seed) mod m ;  should be applied to integers only! **)
    1.12 +local val a = 16807.0  and  m = 2147483647.0
    1.13 +in  fun nextrandom seed =
    1.14 +          let val t = a*seed
    1.15 +          in  t - m * real(floor(t/m))  end
    1.16 +end;
    1.17 +
    1.18  (* generating identifiers *)
    1.19  
    1.20  local
    1.21    val a = ord "a" and z = ord "z" and A = ord "A" and Z = ord "Z"
    1.22    and k0 = ord "0" and k9 = ord "9"
    1.23 +
    1.24 +  val seedr = ref 10000.0;
    1.25  in
    1.26  
    1.27 +(*Maps 0-63 to A-Z, a-z, 0-9 or _ or ' for generating random identifiers*)
    1.28 +fun newid n = 
    1.29 +  let fun char i =
    1.30 +               if i<26 then chr (A+i)
    1.31 +          else if i<52 then chr (a+i-26)
    1.32 +          else if i<62 then chr (k0+i-52)
    1.33 +          else if i=62 then "_"
    1.34 +          else  (*i=63*)    "'"
    1.35 +  in  implode (map char (radixpand (64,n)))  end;
    1.36 +
    1.37 +(*Randomly generated identifiers with given prefix; MUST start with a letter*)
    1.38 +fun gensym pre = pre ^ 
    1.39 +                 (#1(newid (floor (!seedr)), seedr := nextrandom (!seedr)))
    1.40 +
    1.41  (*Increment a list of letters like a reversed base 26 number.
    1.42    If head is "z", bumps chars in tail.
    1.43    Digits are incremented as if they were integers.