author  wenzelm 
Wed, 19 Dec 2007 23:49:28 +0100  
changeset 25720  71e0a5cb2885 
parent 25719  a51430528fe0 
child 25721  5ae1dc2bb5ea 
permissions  rwrr 
25714
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/General/random_word.ML 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

3 
Author: Makarius 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

4 

76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

5 
Simple generator for pseudorandom numbers, using unboxed word 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

6 
arithmetic only. Unprotected concurrency introduces some true 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

7 
randomness. 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

8 
*) 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

9 

76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

10 
signature RANDOM_WORD = 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

11 
sig 
25719  12 
val range: int 
25714
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

13 
val next: unit > word 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

14 
val next_bit: unit > bool 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

15 
end; 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

16 

76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

17 
structure RandomWord: RANDOM_WORD = 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

18 
struct 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

19 

25720  20 
(*minimum length of unboxed words on all supported ML platforms*) 
25719  21 
val _ = Word.wordSize >= 30 orelse raise Fail ("Bad platform word size"); 
25714
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

22 

25719  23 
val range = 0x40000000; 
24 
val mask = Word.fromInt (range  1); 

25 
val max_bit = Word.fromInt (range div 2); 

25714
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

26 

76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

27 
(*multiplier according to Borosh and Niederreiter (for m = 2^30), 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

28 
cf. http://random.mat.sbg.ac.at/~charly/server/server.html*) 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

29 
val a = 0w777138309; 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

30 

76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

31 
(*generator*) 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

32 
val rand = ref 0w0; 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

33 
fun next () = (rand := Word.andb (a * ! rand + 0w1, mask); ! rand); 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

34 
fun next_bit () = Word.andb (next (), max_bit) = 0w0; 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

35 

76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

36 
end; 
76fa068a021f
Simple generator for pseudorandom numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff
changeset

37 