git.iko.soy/Idris-dev
on master help sign in
Base 10 show for Mod2 and various cleanup
commit980493881e0f9f091735a1e6f3610bd0a5e367d7 authorBenjamin Saunders <besaunde@sfu.ca> dateSun 13 Jan 2013, 15:37 (14 years ago) parentb2b4d1e
3 files changed+30−9
compare with master
unifiedsplit
lib/Prelude.idr+1−2 lib/Prelude/Bits.idr+18−7 lib/Prelude/Modular.idr+11
lib/Prelude.idr+1−2
@@ -35,9 +35,8 @@ instance Show Int where
3535instance Show (Bits n) where
3636 show = bitsToStr
3737
38−-- TODO: Base 10
3938instance Show (Mod2 n) where
40− show (MkMod2 x) = bitsToStr x
39+ show = modToStr
4140
4241instance Show Integer where
4342 show = prim__bigIntToStr
lib/Prelude/Bits.idr+18−7
@@ -1,5 +1,7 @@
11module Prelude.Bits
22
3+import Prelude.Strings
4+
35%default total
46
57log2ceil : Nat -> Nat
@@ -67,7 +69,7 @@ pow x y = if y > 0
6769 else 1
6870
6971%assert_total
70−intToBits' : {n: Nat} -> Int -> nextBits n
72+intToBits' : {n : Nat} -> Int -> nextBits n
7173intToBits' {n=n} x with (nextBits n)
7274 | Bits8 = let pad = (prim__intToB8 (cast (8-n))) in
7375 prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad
@@ -85,6 +87,17 @@ intToBits n = MkBits (intToBits' n)
8587instance Cast Int (Bits n) where
8688 cast = intToBits
8789
90+unsafeBitsToInt' : {n : Nat} -> nextBits n -> Int
91+unsafeBitsToInt' {n=n} x with (nextBits n)
92+ | Bits8 = prim__B32ToInt (prim__zextB8_32 x)
93+ | Bits16 = prim__B32ToInt (prim__zextB16_32 x)
94+ | Bits32 = prim__B32ToInt x
95+ | Bits64 = prim__B32ToInt (prim__truncB64_32 x)
96+
97+public
98+unsafeBitsToInt : Bits n -> Int
99+unsafeBitsToInt (MkBits x) = unsafeBitsToInt' x
100+
88101bitsShl' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
89102bitsShl' {n=n} x c with (nextBits n)
90103 | Bits8 = pad8' n prim__shlB8 x c
@@ -308,11 +321,9 @@ bitSet n x = bitsAnd (intToBits 1 `bitsShl` intToBits (cast (finToNat n))) x /=
308321
309322public
310323bitsToStr : Bits n -> String
311−bitsToStr x = helper last x
324+bitsToStr x = pack (helper last x)
312325 where
313326 %assert_total
314− helper : Fin (S n) -> Bits n -> String
315− helper fO _ = ""
316− helper (fS x) b =
317− (if bitSet x b then "1" else "0")
318− ++ helper (weaken x) b
327+ helper : Fin (S n) -> Bits n -> List Char
328+ helper fO _ = []
329+ helper (fS x) b = (if bitSet x b then '1' else '0') :: helper (weaken x) b
lib/Prelude/Modular.idr+11
@@ -70,3 +70,14 @@ instance Cast (Mod2 n) (Bits n) where
7070
7171instance Cast (Bits n) (Mod2 n) where
7272 cast = bitsToMod
73+
74+-- TODO: Other bases
75+public
76+modToStr : Mod2 n -> String
77+modToStr x = pack (reverse (helper x))
78+ where
79+ %assert_total
80+ helper : Mod2 n -> List Char
81+ helper x = strIndex "0123456789" (unsafeBitsToInt (modToBits (x `modRem` 10)))
82+ :: (let q = (x `modDiv` 10) in
83+ if q == 0 then [] else helper q)