git.iko.soy/Idris-dev
on master help sign in
Replace general modulo type with modulo 2^n type
ef96397Benjamin Saunders
lib/Prelude.idr+1−1
compare with master
unifiedsplit
@@ -32,7 +32,7 @@ instance Show Nat where
32instance Show Int where
32instance Show Int where
33 show = prim__intToStr
33 show = prim__intToStr
34
34
35−instance Show (Modulo (S n)) where
35+instance Show (Mod2 n) where
36 show = modToStr
36 show = modToStr
37
37
38instance Show Integer where
38instance Show Integer where
lib/Prelude/Modular.idr+28−14
@@ -3,33 +3,47 @@ import Prelude.Bits
3
3
4%default total
4%default total
5
5
6+-- Integers modulo 2^n
6abstract
7abstract
7−data Modulo : Nat -> Type where
8+data Mod2 : Nat -> Type where
8− MkModulo : {n : Nat} -> Bits (log2 (2*n)) -> Modulo (S n)
9+ MkMod2 : {n : Nat} -> Bits n -> Mod2 n
9
10
10public
11public
11−modAdd : Modulo n -> Modulo n -> Modulo n
12+modAdd : Mod2 n -> Mod2 n -> Mod2 n
12−modAdd (MkModulo x) (MkModulo y) = MkModulo (bitsAdd x y)
13+modAdd (MkMod2 x) (MkMod2 y) = MkMod2 (bitsAdd x y)
13
14
14public
15public
15−modSub : Modulo n -> Modulo n -> Modulo n
16+modSub : Mod2 n -> Mod2 n -> Mod2 n
16−modSub (MkModulo x) (MkModulo y) = MkModulo (bitsSub x y)
17+modSub (MkMod2 x) (MkMod2 y) = MkMod2 (bitsSub x y)
17
18
18public
19public
19−modMul : Modulo n -> Modulo n -> Modulo n
20+modMul : Mod2 n -> Mod2 n -> Mod2 n
20−modMul (MkModulo x) (MkModulo y) = MkModulo (bitsMul x y)
21+modMul (MkMod2 x) (MkMod2 y) = MkMod2 (bitsMul x y)
21
22
22public
23public
23−modDiv : Modulo n -> Modulo n -> Modulo n
24+modDiv : Mod2 n -> Mod2 n -> Mod2 n
24−modDiv (MkModulo x) (MkModulo y) = MkModulo (bitsUDiv x y)
25+modDiv (MkMod2 x) (MkMod2 y) = MkMod2 (bitsUDiv x y)
25
26
26public
27public
27−modToStr : Modulo n -> String
28+modToStr : Mod2 n -> String
28−modToStr (MkModulo x) = bitsToStr x
29+modToStr (MkMod2 x) = bitsToStr x
29
30
31+%assert_total
32+public
33+intToMod : {n : Nat} -> Int -> Mod2 n
34+intToMod {n=n} x = MkMod2 (intToBits x)
35+
36+public
37+modToBits : Mod2 n -> Bits n
38+modToBits (MkMod2 x) = x
39+
40+public
41+bitsToMod : Bits n -> Mod2 n
42+bitsToMod x = MkMod2 x
43+
30−instance Num (Modulo (S n)) where
44+instance Num (Mod2 n) where
31 (+) = modAdd
45 (+) = modAdd
32 (-) = modSub
46 (-) = modSub
33 (*) = modMul
47 (*) = modMul
34 abs = id
48 abs = id
35− fromInteger x = MkModulo (intToBits x)
49+ fromInteger = intToMod