git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4118 from rbarreiro/random_st

random numbers for ST

commitca861967e3ab4d4c54ea1e0bbeb7b406bc1acc64 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateThu 12 Oct 2017, 12:32 (9 years ago) parent1be3ed7b65122a
2 files changed+17−1
compare with master
unifiedsplit
libs/contrib/Control/ST/Random.idr+16 libs/contrib/contrib.ipkg+1−1
libs/contrib/Control/ST/Random.idrnew file+16
@@ -0,0 +1,16 @@
1+module Control.ST.Random
2+
3+import Control.ST
4+
5+public export
6+Random : Type
7+Random = State Integer
8+
9+export
10+getRandom : (rnd : Var) -> ST m Integer [rnd ::: Random]
11+getRandom rnd =
12+ do
13+ st <- read rnd
14+ let st' = assert_total ((1664525 * st + 1013904223) `prim__sremBigInt` (pow 2 32))
15+ write rnd st'
16+ pure st'
libs/contrib/contrib.ipkg+1−1
@@ -9,7 +9,7 @@ modules = CFFI, CFFI.Types, CFFI.Memory,
99 Control.Isomorphism.Primitives,
1010 Control.Partial,
1111 Control.Pipeline,
12− Control.ST, Control.ST.ImplicitCall, Control.ST.Exception,
12+ Control.ST, Control.ST.ImplicitCall, Control.ST.Exception, Control.ST.Random,
1313
1414 Interfaces.Correlative,
1515 Interfaces.Verified,