git.iko.soy/Idris-dev
on master help sign in
More general safe bitsToStr
b2b4d1eBenjamin Saunders
lib/Prelude.idr+3
compare with master
unifiedsplit
@@ -32,6 +32,9 @@ instance Show Nat where
32instance Show Int where
32instance Show Int where
33 show = prim__intToStr
33 show = prim__intToStr
34
34
35+instance Show (Bits n) where
36+ show = bitsToStr
37+
35-- TODO: Base 10
38-- TODO: Base 10
36instance Show (Mod2 n) where
39instance Show (Mod2 n) where
37 show (MkMod2 x) = bitsToStr x
40 show (MkMod2 x) = bitsToStr x
lib/Prelude/Bits.idr+6−5
@@ -307,11 +307,12 @@ bitSet : Fin n -> Bits n -> Bool
307bitSet n x = bitsAnd (intToBits 1 `bitsShl` intToBits (cast (finToNat n))) x /= intToBits 0
307bitSet n x = bitsAnd (intToBits 1 `bitsShl` intToBits (cast (finToNat n))) x /= intToBits 0
308
308
309public
309public
310−bitsToStr : Bits (S n) -> String
310+bitsToStr : Bits n -> String
311−bitsToStr {n=n} x = helper (the (Fin (S n)) last) x
311+bitsToStr x = helper last x
312 where
312 where
313 %assert_total
313 %assert_total
314− helper : Fin (S n) -> Bits (S n) -> String
314+ helper : Fin (S n) -> Bits n -> String
315 helper fO _ = ""
315 helper fO _ = ""
316+ helper (fS x) b =
316− helper (fS x) b = (if bitSet (weaken x) b then "1" else "0")
317+ (if bitSet x b then "1" else "0")
317− ++ helper (weaken x) b
318+ ++ helper (weaken x) b