git.iko.soy/Idris-dev
on 87fb53a help sign in
Idris-dev/libs/base/Data/Mod2.idr
63 lines 1.5 kB history raw
1module Data.Mod2
3import Data.Bits
5%default total
7||| Integers modulo 2^n
8public export
9data Mod2 : Nat -> Type where
10 MkMod2 : {n : Nat} -> Bits n -> Mod2 n
12public export
13modBin : (Bits n -> Bits n -> Bits n) -> Mod2 n -> Mod2 n -> Mod2 n
14modBin f (MkMod2 x) (MkMod2 y) = MkMod2 (f x y)
16modComp : (Bits n -> Bits n -> a) -> Mod2 n -> Mod2 n -> a
17modComp f (MkMod2 x) (MkMod2 y) = f x y
19public export partial
20div : Mod2 n -> Mod2 n -> Mod2 n
21div = modBin udiv
23public export partial
24rem : Mod2 n -> Mod2 n -> Mod2 n
25rem = modBin urem
27%assert_total
28public export
29intToMod : {n : Nat} -> Integer -> Mod2 n
30intToMod {n=n} x = MkMod2 (intToBits x)
32implementation Eq (Mod2 n) where
33 (==) = modComp (==)
35implementation Ord (Mod2 n) where
36 (<) = modComp (<)
37 (<=) = modComp (<=)
38 (>=) = modComp (>=)
39 (>) = modComp (>)
40 compare = modComp compare
42implementation Num (Mod2 n) where
43 (+) = modBin plus
44 (*) = modBin times
45 fromInteger = intToMod
47implementation Cast (Mod2 n) (Bits n) where
48 cast (MkMod2 x) = x
50implementation Cast (Bits n) (Mod2 n) where
51 cast x = MkMod2 x
53modToStr : Mod2 n -> String
54modToStr x = pack (reverse (helper x))
55 where
56 %assert_total
57 helper : Mod2 n -> List Char
58 helper x = strIndex "0123456789" (prim__truncBigInt_Int (bitsToInt (cast (x `rem` 10))))
59 :: (if x < 10 then [] else helper (x `div` 10))
62implementation Show (Mod2 n) where
63 show = modToStr