equal
deleted
inserted
replaced
129 run_random :: "(randseed \<Rightarrow> 'a * randseed) \<Rightarrow> 'a" |
129 run_random :: "(randseed \<Rightarrow> 'a * randseed) \<Rightarrow> 'a" |
130 |
130 |
131 ML {* |
131 ML {* |
132 signature RANDOM = |
132 signature RANDOM = |
133 sig |
133 sig |
134 type seed = IntInf.int; |
134 type seed = int; |
135 val seed: unit -> seed; |
135 val seed: unit -> seed; |
136 val value: IntInf.int -> seed -> IntInf.int * seed; |
136 val value: int -> seed -> int * seed; |
137 end; |
137 end; |
138 |
138 |
139 structure Random : RANDOM = |
139 structure Random : RANDOM = |
140 struct |
140 struct |
141 |
|
142 open IntInf; |
|
143 |
141 |
144 exception RANDOM; |
142 exception RANDOM; |
145 |
143 |
146 type seed = int; |
144 type seed = int; |
147 |
145 |
148 local |
146 local |
149 val a = fromInt 16807; |
147 val a = 16807; |
150 (*greetings to SML/NJ*) |
148 val m = 2147483647; |
151 val m = (the o fromString) "2147483647"; |
|
152 in |
149 in |
153 fun next s = (a * s) mod m; |
150 fun next s = (a * s) mod m; |
154 end; |
151 end; |
155 |
152 |
156 local |
153 local |
157 val seed_ref = ref (fromInt 1); |
154 val seed_ref = ref 1; |
158 in |
155 in |
159 fun seed () = CRITICAL (fn () => |
156 fun seed () = CRITICAL (fn () => |
160 let |
157 let |
161 val r = next (!seed_ref) |
158 val r = next (!seed_ref) |
162 in |
159 in |