git.iko.soy/Idris-dev
on master help sign in
Fix primitive references in test025
1ce70ccBenjamin Saunders
effects/Effect/Random.idr+2−2
compare with master
unifiedsplit
@@ -8,7 +8,7 @@ data Random : Type -> Type -> Type -> Type where
8using (m : Type -> Type)
8using (m : Type -> Type)
9 instance Handler Random m where
9 instance Handler Random m where
10 handle seed getRandom k
10 handle seed getRandom k
11− = let seed' = (1664525 * seed + 1013904223) `prim__modBigInt` (pow 2 32) in
11+ = let seed' = (1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32) in
12 k seed' seed'
12 k seed' seed'
13
13
14RND : EFFECT
14RND : EFFECT
@@ -16,6 +16,6 @@ RND = MkEff Integer Random
16
16
17rndInt : Integer -> Integer -> Eff m [RND] Integer
17rndInt : Integer -> Integer -> Eff m [RND] Integer
18rndInt lower upper = do v <- getRandom
18rndInt lower upper = do v <- getRandom
19− return (v `prim__modBigInt` (upper - lower) + lower)
19+ return (v `prim__sremBigInt` (upper - lower) + lower)
20
20
21
21
test/test025/test025.idr+4−4
@@ -9,23 +9,23 @@ MemoryIO td ts r = Eff (IOExcept String) [ Dst ::: RAW_MEMORY td
9 , Src ::: RAW_MEMORY ts ] r
9 , Src ::: RAW_MEMORY ts ] r
10
10
11inpVect : Vect Bits8 5
11inpVect : Vect Bits8 5
12−inpVect = map prim__intToB8 [0, 1, 2, 3, 5]
12+inpVect = map prim__truncInt_B8 [0, 1, 2, 3, 5]
13
13
14sub1 : Vect Bits8 n -> Vect Bits8 n
14sub1 : Vect Bits8 n -> Vect Bits8 n
15−sub1 xs = map (prim__intToB8 . (\ x => x - 1) . prim__B32ToInt . prim__sextB8_32) xs
15+sub1 xs = map (prim__truncInt_B8 . (\ x => x - 1) . prim__zextB8_Int) xs
16
16
17testMemory : MemoryIO () () (Vect Int 4)
17testMemory : MemoryIO () () (Vect Int 4)
18testMemory = do Src :- allocate 5
18testMemory = do Src :- allocate 5
19 Src :- poke 0 inpVect oh
19 Src :- poke 0 inpVect oh
20 Dst :- allocate 5
20 Dst :- allocate 5
21− Dst :- initialize (prim__intToB8 1) 2 oh
21+ Dst :- initialize (prim__truncInt_B8 1) 2 oh
22 move 2 2 3 oh oh
22 move 2 2 3 oh oh
23 Src :- free
23 Src :- free
24 end <- Dst :- peek 4 1 oh
24 end <- Dst :- peek 4 1 oh
25 Dst :- poke 4 (sub1 end) oh
25 Dst :- poke 4 (sub1 end) oh
26 res <- Dst :- peek 1 4 oh
26 res <- Dst :- peek 1 4 oh
27 Dst :- free
27 Dst :- free
28− return (map (prim__B32ToInt . prim__sextB8_32) res)
28+ return (map (prim__zextB8_Int) res)
29
29
30main : IO ()
30main : IO ()
31main = do ioe_run (run [Dst := (), Src := ()] testMemory)
31main = do ioe_run (run [Dst := (), Src := ()] testMemory)