git.iko.soy/Idris-dev
on master help sign in
Eq and Ord instances for Bits
5634a77Benjamin Saunders
lib/Prelude/Bits.idr+19−9
compare with master
unifiedsplit
@@ -171,8 +171,7 @@ bitsSDiv' {n=n} x y with (nextBits n)
171 | Bits32 = prim__sdivB32 x y
171 | Bits32 = prim__sdivB32 x y
172 | Bits64 = prim__sdivB64 x y
172 | Bits64 = prim__sdivB64 x y
173
173
174−public
175−partial
174+public partial
176bitsSDiv : Bits n -> Bits n -> Bits n
175bitsSDiv : Bits n -> Bits n -> Bits n
177bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)
176bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)
178
177
@@ -184,8 +183,7 @@ bitsUDiv' {n=n} x y with (nextBits n)
184 | Bits32 = prim__udivB32 x y
183 | Bits32 = prim__udivB32 x y
185 | Bits64 = prim__udivB64 x y
184 | Bits64 = prim__udivB64 x y
186
185
187−public
188−partial
186+public partial
189bitsUDiv : Bits n -> Bits n -> Bits n
187bitsUDiv : Bits n -> Bits n -> Bits n
190bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)
188bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)
191
189
@@ -197,8 +195,7 @@ bitsSRem' {n=n} x y with (nextBits n)
197 | Bits32 = prim__sremB32 x y
195 | Bits32 = prim__sremB32 x y
198 | Bits64 = prim__sremB64 x y
196 | Bits64 = prim__sremB64 x y
199
197
200−public
201−partial
198+public partial
202bitsSRem : Bits n -> Bits n -> Bits n
199bitsSRem : Bits n -> Bits n -> Bits n
203bitsSRem (MkBits x) (MkBits y) = MkBits (bitsSRem' x y)
200bitsSRem (MkBits x) (MkBits y) = MkBits (bitsSRem' x y)
204
201
@@ -210,8 +207,7 @@ bitsURem' {n=n} x y with (nextBits n)
210 | Bits32 = prim__uremB32 x y
207 | Bits32 = prim__uremB32 x y
211 | Bits64 = prim__uremB64 x y
208 | Bits64 = prim__uremB64 x y
212
209
213−public
214−partial
210+public partial
215bitsURem : Bits n -> Bits n -> Bits n
211bitsURem : Bits n -> Bits n -> Bits n
216bitsURem (MkBits x) (MkBits y) = MkBits (bitsURem' x y)
212bitsURem (MkBits x) (MkBits y) = MkBits (bitsURem' x y)
217
213
@@ -271,12 +267,26 @@ public
271bitsGt : (x : Bits n) -> (y : Bits n) -> Bool
267bitsGt : (x : Bits n) -> (y : Bits n) -> Bool
272bitsGt (MkBits x) (MkBits y) = bitsGt' x y /= 0
268bitsGt (MkBits x) (MkBits y) = bitsGt' x y /= 0
273
269
270+instance Eq (Bits n) where
271+ (==) = bitsEq
272+
273+instance Ord (Bits n) where
274+ (<) = bitsLt
275+ (<=) = bitsLte
276+ (>=) = bitsGte
277+ (>) = bitsGt
278+ compare x y = if x `bitsLt` y
279+ then LT
280+ else if x `bitsEq` y
281+ then EQ
282+ else GT
283+
274public
284public
275bitsToStr : Bits n -> String
285bitsToStr : Bits n -> String
276bitsToStr {n=n} x = helper n x
286bitsToStr {n=n} x = helper n x
277 where
287 where
278 helper : Nat -> Bits n -> String
288 helper : Nat -> Bits n -> String
279− helper (S x) b = (if bitsAnd (bitsShl (intToBits 1) (intToBits (cast x))) b `bitsEq` (intToBits 0)
289+ helper (S x) b = (if bitsAnd (bitsShl (intToBits 1) (intToBits (cast x))) b == (intToBits 0)
280 then "0"
290 then "0"
281 else "1"
291 else "1"
282 ) ++ helper x b
292 ) ++ helper x b
lib/Prelude/Modular.idr+4−4
@@ -21,13 +21,13 @@ public
21modMul : Mod2 n -> Mod2 n -> Mod2 n
21modMul : Mod2 n -> Mod2 n -> Mod2 n
22modMul (MkMod2 x) (MkMod2 y) = MkMod2 (bitsMul x y)
22modMul (MkMod2 x) (MkMod2 y) = MkMod2 (bitsMul x y)
23
23
24−public
24+public partial
25modDiv : Mod2 n -> Mod2 n -> Mod2 n
25modDiv : Mod2 n -> Mod2 n -> Mod2 n
26modDiv (MkMod2 x) (MkMod2 y) = MkMod2 (bitsUDiv x y)
26modDiv (MkMod2 x) (MkMod2 y) = MkMod2 (bitsUDiv x y)
27
27
28−public
28+public partial
29−modToStr : Mod2 n -> String
29+modRem : Mod2 n -> Mod2 n -> Mod2 n
30−modToStr (MkMod2 x) = bitsToStr x
30+modRem (MkMod2 x) (MkMod2 y) = MkMod2 (bitsURem x y)
31
31
32%assert_total
32%assert_total
33public
33public