on master help sign in
Removed unreliable machine ints from Random effect
commitc05479ed7143c846acd0b0e7c4f0f5f680c101b9 authorJan Bessai <Jan.Bessai@tu-dortmund.de> dateThu 9 May 2013, 22:03 (13 years ago) parenta9c55de
2 files changed+12−12
effects/Effect/Random.idr+7−7 test/test021/test021a.idr+5−5
effects/Effect/Random.idr+7−7
@@ -3,19 +3,19 @@ module Effect.Random
33import Effects
44
55data Random : Type -> Type -> Type -> Type where
6− getRandom : Random Int Int Int
6+ getRandom : Random Integer Integer Integer
77
88using (m : Type -> Type)
99 instance Handler Random m where
1010 handle seed getRandom k
11− = let seed' = 1664525 * seed + 1013904223 in
11+ = let seed' = (1664525 * seed + 1013904223) `prim__modBigInt` (pow 2 32) in
1212 k seed' seed'
13−
13+
1414RND : EFFECT
15−RND = MkEff Int Random
15+RND = MkEff Integer Random
1616
17−rndInt : Int -> Int -> Eff m [RND] Int
18−rndInt lower upper = do v <- getRandom
19− return (v `mod` (upper - lower) + lower)
17+rndInt : Integer -> Integer -> Eff m [RND] Integer
18+rndInt lower upper = do v <- getRandom
19+ return (v `prim__modBigInt` (upper - lower) + lower)
2020
2121
test/test021/test021a.idr+5−5
@@ -6,18 +6,18 @@ import Effect.Random
66import Effect.StdIO
77
88data Expr = Var String
9− | Val Int
9+ | Val Integer
1010 | Add Expr Expr
11− | Random Int
11+ | Random Integer
1212
1313Env : Type
14−Env = List (String, Int)
14+Env = List (String, Integer)
1515
1616-- Evaluator : Type -> Type
1717-- Evaluator t
1818-- = Eff m [EXCEPTION String, RND, STATE Env] t
1919
20−eval : Expr -> Eff IO [EXCEPTION String, STDIO, RND, STATE Env] Int
20+eval : Expr -> Eff IO [EXCEPTION String, STDIO, RND, STATE Env] Integer
2121eval (Var x) = do vs <- get
2222 case lookup x vs of
2323 Nothing => raise ("No such variable " ++ x)
@@ -31,7 +31,7 @@ eval (Random upper) = do val <- rndInt 0 upper
3131testExpr : Expr
3232testExpr = Add (Add (Var "foo") (Val 42)) (Random 100)
3333
34−runEval : List (String, Int) -> Expr -> IO Int
34+runEval : List (String, Integer) -> Expr -> IO Integer
3535runEval args expr = run [(), (), 123456, args] (eval expr)
3636
3737main : IO ()