git.iko.soy/Idris-dev
on e24baaa help sign in
Idris-dev/lib/Data/Mod2.idr
66 lines 1.4 kB history raw
1module Data.Mod2
3import Data.Bits
5%default total
7{-
8-- Integers modulo 2^n
9public
10data Mod2 : Nat -> Type where
11 MkMod2 : {n : Nat} -> Bits n -> Mod2 n
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 partial
20div : Mod2 n -> Mod2 n -> Mod2 n
21div = modBin udiv
23public partial
24rem : Mod2 n -> Mod2 n -> Mod2 n
25rem = modBin urem
27%assert_total
28public
29intToMod : {n : Nat} -> Int -> Mod2 n
30intToMod {n=n} x = MkMod2 (intToBits x)
32instance Eq (Mod2 n) where
33 (==) = modComp (==)
35instance Ord (Mod2 n) where
36 (<) = modComp (<)
37 (<=) = modComp (<=)
38 (>=) = modComp (>=)
39 (>) = modComp (>)
40 compare = modComp compare
42instance Num (Mod2 n) where
43 (+) = modBin plus
44 (-) = modBin minus
45 (*) = modBin times
46 abs = id
47 fromInteger = intToMod
49instance Cast (Mod2 n) (Bits n) where
50 cast (MkMod2 x) = x
52instance Cast (Bits n) (Mod2 n) where
53 cast x = MkMod2 x
55modToStr : Mod2 n -> String
56modToStr x = pack (reverse (helper x))
57 where
58 %assert_total
59 helper : Mod2 n -> List Char
60 helper x = strIndex "0123456789" (bitsToInt (cast (x `rem` 10)))
61 :: (if x < 10 then [] else helper (x `div` 10))
64instance Show (Mod2 n) where
65 show = modToStr
66-}