@@ -39,6 +39,27 @@ pad64 n f x y = prim__lshrB64 (f (prim__shlB64 x pad) (prim__shlB64 y pad)) pad
3939 where
4040 pad = (prim__intToB64 (cast (64-n)))
4141
42+-- These versions only pad the first operand
43+pad8' : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
44+pad8' n f x y = prim__lshrB8 (f (prim__shlB8 x pad) y) pad
45+ where
46+ pad = (prim__intToB8 (cast (8-n)))
47+
48+pad16' : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
49+pad16' n f x y = prim__lshrB16 (f (prim__shlB16 x pad) y) pad
50+ where
51+ pad = (prim__intToB16 (cast (16-n)))
52+
53+pad32' : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
54+pad32' n f x y = prim__lshrB32 (f (prim__shlB32 x pad) y) pad
55+ where
56+ pad = (prim__intToB32 (cast (32-n)))
57+
58+pad64' : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
59+pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad
60+ where
61+ pad = (prim__intToB64 (cast (64-n)))
62+
4263%assert_total
4364pow : Int -> Int -> Int
4465pow x y = if y > 0
@@ -66,10 +87,10 @@ instance Cast Int (Bits n) where
6687
6788bitsShl' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
6889bitsShl' {n=n} x c with (nextBits n)
69− | Bits8 = pad8 n prim__shlB8 x c
70− | Bits16 = pad16 n prim__shlB16 x c
71− | Bits32 = pad32 n prim__shlB32 x c
72− | Bits64 = pad64 n prim__shlB64 x c
90+ | Bits8 = pad8' n prim__shlB8 x c
91+ | Bits16 = pad16' n prim__shlB16 x c
92+ | Bits32 = pad32' n prim__shlB32 x c
93+ | Bits64 = pad64' n prim__shlB64 x c
7394
7495public
7596bitsShl : Bits n -> Bits n -> Bits n
@@ -282,12 +303,15 @@ instance Ord (Bits n) where
282303 else GT
283304
284305public
285−bitsToStr : Bits n -> String
286−bitsToStr {n=n} x = helper n x
306+bitSet : Fin n -> Bits n -> Bool
307+bitSet n x = bitsAnd (intToBits 1 `bitsShl` intToBits (cast (finToNat n))) x /= intToBits 0
308+
309+public
310+bitsToStr : Bits (S n) -> String
311+bitsToStr {n=n} x = helper (the (Fin (S n)) last) x
287312 where
288− helper : Nat -> Bits n -> String
289− helper (S x) b = (if bitsAnd (bitsShl (intToBits 1) (intToBits (cast x))) b == (intToBits 0)
290− then "0"
291− else "1"
292− ) ++ helper x b
293− helper O _ = ""
313+ %assert_total
314+ helper : Fin (S n) -> Bits (S n) -> String
315+ helper fO _ = ""
316+ helper (fS x) b = (if bitSet (weaken x) b then "1" else "0")
317+ ++ helper (weaken x) b