@@ -4,12 +4,14 @@ import Effects
5data Random : Type -> Type -> Type -> Type where
5data Random : Type -> Type -> Type -> Type where
6 getRandom : Random Integer Integer Integer
6 getRandom : Random Integer Integer Integer
7+ setSeed : Integer -> Random Integer Integer ()
8using (m : Type -> Type)
9using (m : Type -> Type)
9 instance Handler Random m where
10 instance Handler Random m where
10 handle seed getRandom k
11 handle seed getRandom k
11 = let seed' = (1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32) in
12 = let seed' = (1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32) in
12 k seed' seed'
13 k seed' seed'
14+ handle seed (setSeed n) k = k n ()
14RND : EFFECT
16RND : EFFECT
15RND = MkEff Integer Random
17RND = MkEff Integer Random
@@ -18,4 +20,6 @@ rndInt : Integer -> Integer -> Eff m [RND] Integer
18rndInt lower upper = do v <- getRandom
20rndInt lower upper = do v <- getRandom
19 return (v `prim__sremBigInt` (upper - lower) + lower)
21 return (v `prim__sremBigInt` (upper - lower) + lower)
23+srand : Integer -> Eff m [RND] ()