git.iko.soy/Idris-dev
on master help sign in
Base 10 show for Mod2 and various cleanup
9804938Benjamin Saunders
lib/Prelude.idr+1−2
compare with master
unifiedsplit
@@ -35,9 +35,8 @@ instance Show Int where
35instance Show (Bits n) where
35instance Show (Bits n) where
36 show = bitsToStr
36 show = bitsToStr
37
37
38−-- TODO: Base 10
39instance Show (Mod2 n) where
38instance Show (Mod2 n) where
40− show (MkMod2 x) = bitsToStr x
39+ show = modToStr
41
40
42instance Show Integer where
41instance Show Integer where
43 show = prim__bigIntToStr
42 show = prim__bigIntToStr
lib/Prelude/Bits.idr+18−7
@@ -1,5 +1,7 @@
1module Prelude.Bits
1module Prelude.Bits
2
2
3+import Prelude.Strings
4+
3%default total
5%default total
4
6
5log2ceil : Nat -> Nat
7log2ceil : Nat -> Nat
@@ -67,7 +69,7 @@ pow x y = if y > 0
67 else 1
69 else 1
68
70
69%assert_total
71%assert_total
70−intToBits' : {n: Nat} -> Int -> nextBits n
72+intToBits' : {n : Nat} -> Int -> nextBits n
71intToBits' {n=n} x with (nextBits n)
73intToBits' {n=n} x with (nextBits n)
72 | Bits8 = let pad = (prim__intToB8 (cast (8-n))) in
74 | Bits8 = let pad = (prim__intToB8 (cast (8-n))) in
73 prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad
75 prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad
@@ -85,6 +87,17 @@ intToBits n = MkBits (intToBits' n)
85instance Cast Int (Bits n) where
87instance Cast Int (Bits n) where
86 cast = intToBits
88 cast = intToBits
87
89
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+
88bitsShl' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
101bitsShl' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
89bitsShl' {n=n} x c with (nextBits n)
102bitsShl' {n=n} x c with (nextBits n)
90 | Bits8 = pad8' n prim__shlB8 x c
103 | Bits8 = pad8' n prim__shlB8 x c
@@ -308,11 +321,9 @@ bitSet n x = bitsAnd (intToBits 1 `bitsShl` intToBits (cast (finToNat n))) x /=
308
321
309public
322public
310bitsToStr : Bits n -> String
323bitsToStr : Bits n -> String
311−bitsToStr x = helper last x
324+bitsToStr x = pack (helper last x)
312 where
325 where
313 %assert_total
326 %assert_total
314− helper : Fin (S n) -> Bits n -> String
327+ helper : Fin (S n) -> Bits n -> List Char
315− helper fO _ = ""
328+ helper fO _ = []
316− helper (fS x) b =
317− (if bitSet x b then "1" else "0")
329+ helper (fS x) b = (if bitSet x b then '1' else '0') :: helper (weaken x) b
318− ++ helper (weaken x) b
lib/Prelude/Modular.idr+11
@@ -70,3 +70,14 @@ instance Cast (Mod2 n) (Bits n) where
70
70
71instance Cast (Bits n) (Mod2 n) where
71instance Cast (Bits n) (Mod2 n) where
72 cast = bitsToMod
72 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)