src/Pure/library.ML
changeset 2003 b48f066d52dc
parent 1628 60136fdd80c4
child 2025 9acc10ac1e1d
equal deleted inserted replaced
2002:ed423882c6a9 2003:b48f066d52dc
   903           val zs = foldl (fn (zs, y) => assocs qs y union zs) (ys, ys)
   903           val zs = foldl (fn (zs, y) => assocs qs y union zs) (ys, ys)
   904           fun step(u, us) = (u, if x mem us then zs union us else us)
   904           fun step(u, us) = (u, if x mem us then zs union us else us)
   905       in (x, zs) :: map step qs end;
   905       in (x, zs) :: map step qs end;
   906 
   906 
   907 
   907 
       
   908 (** Recommended by Stephen K. Park and Keith W. Miller, 
       
   909       Random number generators: good ones are hard to find,
       
   910       CACM 31 (1988), 1192-1201. 
       
   911     Real number version for systems with 46-bit mantissae
       
   912     Computes  (a*seed) mod m ;  should be applied to integers only! **)
       
   913 local val a = 16807.0  and  m = 2147483647.0
       
   914 in  fun nextrandom seed =
       
   915           let val t = a*seed
       
   916           in  t - m * real(floor(t/m))  end
       
   917 end;
       
   918 
   908 (* generating identifiers *)
   919 (* generating identifiers *)
   909 
   920 
   910 local
   921 local
   911   val a = ord "a" and z = ord "z" and A = ord "A" and Z = ord "Z"
   922   val a = ord "a" and z = ord "z" and A = ord "A" and Z = ord "Z"
   912   and k0 = ord "0" and k9 = ord "9"
   923   and k0 = ord "0" and k9 = ord "9"
       
   924 
       
   925   val seedr = ref 10000.0;
   913 in
   926 in
       
   927 
       
   928 (*Maps 0-63 to A-Z, a-z, 0-9 or _ or ' for generating random identifiers*)
       
   929 fun newid n = 
       
   930   let fun char i =
       
   931                if i<26 then chr (A+i)
       
   932           else if i<52 then chr (a+i-26)
       
   933           else if i<62 then chr (k0+i-52)
       
   934           else if i=62 then "_"
       
   935           else  (*i=63*)    "'"
       
   936   in  implode (map char (radixpand (64,n)))  end;
       
   937 
       
   938 (*Randomly generated identifiers with given prefix; MUST start with a letter*)
       
   939 fun gensym pre = pre ^ 
       
   940                  (#1(newid (floor (!seedr)), seedr := nextrandom (!seedr)))
   914 
   941 
   915 (*Increment a list of letters like a reversed base 26 number.
   942 (*Increment a list of letters like a reversed base 26 number.
   916   If head is "z", bumps chars in tail.
   943   If head is "z", bumps chars in tail.
   917   Digits are incremented as if they were integers.
   944   Digits are incremented as if they were integers.
   918   "_" and "'" are not changed.
   945   "_" and "'" are not changed.