git.iko.soy/Idris-dev
on cd58dfb help sign in
Idris-dev/libs/base/Data/Mod2.idr
62 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
27public export
28intToMod : {n : Nat} -> Integer -> Mod2 n
29intToMod {n=n} x = MkMod2 (intToBits x)
31implementation Eq (Mod2 n) where
32 (==) = modComp (==)
34implementation Ord (Mod2 n) where
35 (<) = modComp (<)
36 (<=) = modComp (<=)
37 (>=) = modComp (>=)
38 (>) = modComp (>)
39 compare = modComp compare
41implementation Num (Mod2 n) where
42 (+) = modBin plus
43 (*) = modBin times
44 fromInteger = intToMod
46implementation Cast (Mod2 n) (Bits n) where
47 cast (MkMod2 x) = x
49implementation Cast (Bits n) (Mod2 n) where
50 cast x = MkMod2 x
52modToStr : Mod2 n -> String
53modToStr x = pack (reverse (helper x))
54 where
55 helper : Mod2 n -> List Char
56 helper x = assert_total $
57 strIndex "0123456789" (prim__truncBigInt_Int (bitsToInt (cast (x `rem` 10))))
58 :: (if x < 10 then [] else helper (x `div` 10))
61implementation Show (Mod2 n) where
62 show = modToStr