@@ -347,6 +347,25 @@ public partial
347zext : Bits n -> Bits (n+m)
347zext : Bits n -> Bits (n+m)
348zext (MkBits x) = MkBits (zext' x)
348zext (MkBits x) = MkBits (zext' x)
352+sext' : machineTy (log2Bytes n) -> machineTy (log2Bytes (n+m))
353+sext' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))
354+ | (O, O) = believe_me x
355+ | (O, S O) = believe_me (prim__sextB8_16 (believe_me x))
356+ | (O, S (S O)) = believe_me (prim__sextB8_32 (believe_me x))
357+ | (O, S (S (S _))) = believe_me (prim__sextB8_64 (believe_me x))
358+ | (S O, S O) = believe_me x
359+ | (S O, S (S O)) = believe_me (prim__sextB16_32 (believe_me x))
360+ | (S O, S (S (S _))) = believe_me (prim__sextB16_64 (believe_me x))
361+ | (S (S O), S (S O)) = believe_me x
362+ | (S (S O), S (S (S _))) = believe_me (prim__sextB32_64 (believe_me x))
363+ | (S (S (S _)), S (S (S _))) = believe_me x
366+sext : Bits n -> Bits (n+m)
367+sext (MkBits x) = MkBits (sext' x)
351bitSet : Fin n -> Bits n -> Bool
370bitSet : Fin n -> Bits n -> Bool
352bitSet n x = bitsAnd (intToBits 1 `bitsShl` intToBits (cast (finToNat n))) x /= intToBits 0
371bitSet n x = bitsAnd (intToBits 1 `bitsShl` intToBits (cast (finToNat n))) x /= intToBits 0