git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4118 from rbarreiro/random_st
ca86196Ahmad Salim Al-Sibahi
libs/contrib/Control/ST/Random.idrnew file+16
compare with master
unifiedsplit
@@ -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,
9 Control.Isomorphism.Primitives,
9 Control.Isomorphism.Primitives,
10 Control.Partial,
10 Control.Partial,
11 Control.Pipeline,
11 Control.Pipeline,
12− Control.ST, Control.ST.ImplicitCall, Control.ST.Exception,
12+ Control.ST, Control.ST.ImplicitCall, Control.ST.Exception, Control.ST.Random,
13
13
14 Interfaces.Correlative,
14 Interfaces.Correlative,
15 Interfaces.Verified,
15 Interfaces.Verified,