@@ -3,33 +3,47 @@ import Prelude.Bits
33
44%default total
55
6+-- Integers modulo 2^n
67abstract
7−data Modulo : Nat -> Type where
8− MkModulo : {n : Nat} -> Bits (log2 (2*n)) -> Modulo (S n)
8+data Mod2 : Nat -> Type where
9+ MkMod2 : {n : Nat} -> Bits n -> Mod2 n
910
1011public
11−modAdd : Modulo n -> Modulo n -> Modulo n
12−modAdd (MkModulo x) (MkModulo y) = MkModulo (bitsAdd x y)
12+modAdd : Mod2 n -> Mod2 n -> Mod2 n
13+modAdd (MkMod2 x) (MkMod2 y) = MkMod2 (bitsAdd x y)
1314
1415public
15−modSub : Modulo n -> Modulo n -> Modulo n
16−modSub (MkModulo x) (MkModulo y) = MkModulo (bitsSub x y)
16+modSub : Mod2 n -> Mod2 n -> Mod2 n
17+modSub (MkMod2 x) (MkMod2 y) = MkMod2 (bitsSub x y)
1718
1819public
19−modMul : Modulo n -> Modulo n -> Modulo n
20−modMul (MkModulo x) (MkModulo y) = MkModulo (bitsMul x y)
20+modMul : Mod2 n -> Mod2 n -> Mod2 n
21+modMul (MkMod2 x) (MkMod2 y) = MkMod2 (bitsMul x y)
2122
2223public
23−modDiv : Modulo n -> Modulo n -> Modulo n
24−modDiv (MkModulo x) (MkModulo y) = MkModulo (bitsUDiv x y)
24+modDiv : Mod2 n -> Mod2 n -> Mod2 n
25+modDiv (MkMod2 x) (MkMod2 y) = MkMod2 (bitsUDiv x y)
2526
2627public
27−modToStr : Modulo n -> String
28−modToStr (MkModulo x) = bitsToStr x
28+modToStr : Mod2 n -> String
29+modToStr (MkMod2 x) = bitsToStr x
2930
30−instance Num (Modulo (S n)) where
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+
44+instance Num (Mod2 n) where
3145 (+) = modAdd
3246 (-) = modSub
3347 (*) = modMul
3448 abs = id
35− fromInteger x = MkModulo (intToBits x)
49+ fromInteger = intToMod