git.iko.soy/Idris-dev
on master help sign in
More general safe bitsToStr
commitb2b4d1e770af6914a87107aef4328a657c5b16d7 authorBenjamin Saunders <besaunde@sfu.ca> dateSun 13 Jan 2013, 14:31 (14 years ago) parent01771e6
2 files changed+9−5
compare with master
unifiedsplit
lib/Prelude.idr+3 lib/Prelude/Bits.idr+6−5
lib/Prelude.idr+3
@@ -32,6 +32,9 @@ instance Show Nat where
3232instance Show Int where
3333 show = prim__intToStr
3434
35+instance Show (Bits n) where
36+ show = bitsToStr
37+
3538-- TODO: Base 10
3639instance Show (Mod2 n) where
3740 show (MkMod2 x) = bitsToStr x
lib/Prelude/Bits.idr+6−5
@@ -307,11 +307,12 @@ bitSet : Fin n -> Bits n -> Bool
307307bitSet n x = bitsAnd (intToBits 1 `bitsShl` intToBits (cast (finToNat n))) x /= intToBits 0
308308
309309public
310−bitsToStr : Bits (S n) -> String
311−bitsToStr {n=n} x = helper (the (Fin (S n)) last) x
310+bitsToStr : Bits n -> String
311+bitsToStr x = helper last x
312312 where
313313 %assert_total
314− helper : Fin (S n) -> Bits (S n) -> String
314+ helper : Fin (S n) -> Bits n -> String
315315 helper fO _ = ""
316− helper (fS x) b = (if bitSet (weaken x) b then "1" else "0")
317− ++ helper (weaken x) b
316+ helper (fS x) b =
317+ (if bitSet x b then "1" else "0")
318+ ++ helper (weaken x) b