@@ -366,6 +366,25 @@ public partial
366sext : Bits n -> Bits (n+m)
366sext : Bits n -> Bits (n+m)
367sext (MkBits x) = MkBits (sext' x)
367sext (MkBits x) = MkBits (sext' x)
371+trunc' : machineTy (log2Bytes (n+m)) -> machineTy (log2Bytes n)
372+trunc' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))
373+ | (O, O) = believe_me x
374+ | (O, S O) = believe_me (prim__truncB16_8 (believe_me x))
375+ | (O, S (S O)) = believe_me (prim__truncB32_8 (believe_me x))
376+ | (O, S (S (S _))) = believe_me (prim__truncB64_8 (believe_me x))
377+ | (S O, S O) = believe_me x
378+ | (S O, S (S O)) = believe_me (prim__truncB32_16 (believe_me x))
379+ | (S O, S (S (S _))) = believe_me (prim__truncB64_16 (believe_me x))
380+ | (S (S O), S (S O)) = believe_me x
381+ | (S (S O), S (S (S _))) = believe_me (prim__truncB64_32 (believe_me x))
382+ | (S (S (S _)), S (S (S _))) = believe_me x
385+truncate : Bits (n+m) -> Bits n
386+truncate (MkBits x) = MkBits (trunc' x)
370bitSet : Fin n -> Bits n -> Bool
389bitSet : Fin n -> Bits n -> Bool
371bitSet n x = bitsAnd (intToBits 1 `bitsShl` intToBits (cast (finToNat n))) x /= intToBits 0
390bitSet n x = bitsAnd (intToBits 1 `bitsShl` intToBits (cast (finToNat n))) x /= intToBits 0