@@ -48,10 +48,14 @@ pow x y = if y > 0
48%assert_total
48%assert_total
49intToBits' : {n: Nat} -> Int -> nextBits n
49intToBits' : {n: Nat} -> Int -> nextBits n
50intToBits' {n=n} x with (nextBits n)
50intToBits' {n=n} x with (nextBits n)
51− | Bits8 = prim__intToB8 (x `mod` (pow 2 (cast n)))
51+ | Bits8 = let pad = (prim__intToB8 (cast (8-n))) in
52− | Bits16 = prim__intToB16 (x `mod` (pow 2 (cast n)))
52+ prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad
53− | Bits32 = prim__intToB32 (x `mod` (pow 2 (cast n)))
53+ | Bits16 = let pad = (prim__intToB16 (cast (16-n))) in
54− | Bits64 = prim__intToB64 (x `mod` (pow 2 (cast n)))
54+ prim__lshrB16 (prim__shlB16 (prim__intToB16 x) pad) pad
55+ | Bits32 = let pad = (prim__intToB32 (cast (32-n))) in
56+ prim__lshrB32 (prim__shlB32 (prim__intToB32 x) pad) pad
57+ | Bits64 = let pad = (prim__intToB64 (cast (64-n))) in
58+ prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad
57intToBits : {n : Nat} -> Int -> Bits n
61intToBits : {n : Nat} -> Int -> Bits n