git.iko.soy/Idris-dev
on 0875310 help sign in
Idris-dev/libs/base/Data/Mod2.idr
64 lines 1.4 kB history raw
1module Data.Mod2
3import Data.Bits
5%default total
7-- Integers modulo 2^n
8public
9data Mod2 : Nat -> Type where
10 MkMod2 : {n : Nat} -> Bits n -> Mod2 n
12modBin : (Bits n -> Bits n -> Bits n) -> Mod2 n -> Mod2 n -> Mod2 n
13modBin f (MkMod2 x) (MkMod2 y) = MkMod2 (f x y)
15modComp : (Bits n -> Bits n -> a) -> Mod2 n -> Mod2 n -> a
16modComp f (MkMod2 x) (MkMod2 y) = f x y
18public partial
19div : Mod2 n -> Mod2 n -> Mod2 n
20div = modBin udiv
22public partial
23rem : Mod2 n -> Mod2 n -> Mod2 n
24rem = modBin urem
26%assert_total
27public
28intToMod : {n : Nat} -> Integer -> Mod2 n
29intToMod {n=n} x = MkMod2 (intToBits x)
31instance Eq (Mod2 n) where
32 (==) = modComp (==)
34instance Ord (Mod2 n) where
35 (<) = modComp (<)
36 (<=) = modComp (<=)
37 (>=) = modComp (>=)
38 (>) = modComp (>)
39 compare = modComp compare
41instance Num (Mod2 n) where
42 (+) = modBin plus
43 (-) = modBin minus
44 (*) = modBin times
45 abs = id
46 fromInteger = intToMod
48instance Cast (Mod2 n) (Bits n) where
49 cast (MkMod2 x) = x
51instance Cast (Bits n) (Mod2 n) where
52 cast x = MkMod2 x
54modToStr : Mod2 n -> String
55modToStr x = pack (reverse (helper x))
56 where
57 %assert_total
58 helper : Mod2 n -> List Char
59 helper x = strIndex "0123456789" (prim__truncBigInt_Int (bitsToInt (cast (x `rem` 10))))
60 :: (if x < 10 then [] else helper (x `div` 10))
63instance Show (Mod2 n) where
64 show = modToStr