@@ -298,12 +298,16 @@ instance Ord (Bits n) where
301−complement' : machineTy n -> machineTy n
301+complement' : machineTy (log2Bytes n) -> machineTy (log2Bytes n)
302−complement' {n=n} x with n
302+complement' {n=n} x with (log2Bytes n)
303+ | O = let pad = prim__intToB8 (8 - cast n) in
303− | O = prim__complB8 x
304+ prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad
305+ | S O = let pad = prim__intToB16 (16 - cast n) in
304− | S O = prim__complB16 x
306+ prim__complB16 (x `prim__shlB16` pad) `prim__lshrB16` pad
307+ | S (S O) = let pad = prim__intToB32 (32 - cast n) in
305− | S (S O) = prim__complB32 x
308+ prim__complB32 (x `prim__shlB32` pad) `prim__lshrB32` pad
309+ | S (S (S _)) = let pad = prim__intToB64 (64 - cast n) in
306− | S (S (S _)) = prim__complB64 x
310+ prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
309complement : Bits n -> Bits n
313complement : Bits n -> Bits n
@@ -328,39 +332,47 @@ public partial
328zeroExtend : Bits n -> Bits (n+m)
332zeroExtend : Bits n -> Bits (n+m)
329zeroExtend (MkBits x) = MkBits (zext' x)
333zeroExtend (MkBits x) = MkBits (zext' x)
335+-- Fill in the high bits of a sign-extended bitstring
336+fixupSE : (m : Nat) -> machineTy (log2Bytes (n+m)) -> machineTy (log2Bytes (n+m))
337+fixupSE m x = x `or'` complement' (zext' {m=m} (complement' (intToBits' 0)))
331-- TODO: Prove
339-- TODO: Prove
332%assert_total
340%assert_total
333sext' : machineTy (log2Bytes n) -> machineTy (log2Bytes (n+m))
341sext' : machineTy (log2Bytes n) -> machineTy (log2Bytes (n+m))
334sext' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))
342sext' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))
335− | (O, O) = believe_me x
343+ | (O, O) = fixupSE m (believe_me x)
336− | (O, S O) = believe_me (prim__sextB8_16 (believe_me x))
344+ | (O, S O) = fixupSE m (believe_me (prim__sextB8_16 (believe_me x)))
337− | (O, S (S O)) = believe_me (prim__sextB8_32 (believe_me x))
345+ | (O, S (S O)) = fixupSE m (believe_me (prim__sextB8_32 (believe_me x)))
338− | (O, S (S (S _))) = believe_me (prim__sextB8_64 (believe_me x))
346+ | (O, S (S (S _))) = fixupSE m (believe_me (prim__sextB8_64 (believe_me x)))
339− | (S O, S O) = believe_me x
347+ | (S O, S O) = fixupSE m (believe_me x)
340− | (S O, S (S O)) = believe_me (prim__sextB16_32 (believe_me x))
348+ | (S O, S (S O)) = fixupSE m (believe_me (prim__sextB16_32 (believe_me x)))
341− | (S O, S (S (S _))) = believe_me (prim__sextB16_64 (believe_me x))
349+ | (S O, S (S (S _))) = fixupSE m (believe_me (prim__sextB16_64 (believe_me x)))
342− | (S (S O), S (S O)) = believe_me x
350+ | (S (S O), S (S O)) = fixupSE m (believe_me x)
343− | (S (S O), S (S (S _))) = believe_me (prim__sextB32_64 (believe_me x))
351+ | (S (S O), S (S (S _))) = fixupSE m (believe_me (prim__sextB32_64 (believe_me x)))
344− | (S (S (S _)), S (S (S _))) = believe_me x
352+ | (S (S (S _)), S (S (S _))) = fixupSE m (believe_me x)
346public partial
354public partial
347signExtend : Bits n -> Bits (n+m)
355signExtend : Bits n -> Bits (n+m)
348signExtend (MkBits x) = MkBits (sext' x)
356signExtend (MkBits x) = MkBits (sext' x)
358+-- Zero out the high bits of a truncated bitstring
359+fixupTR : machineTy (log2Bytes n) -> machineTy (log2Bytes n)
360+fixupTR x = x `and'` complement' (intToBits' 0)
350-- TODO: Prove
362-- TODO: Prove
351%assert_total
363%assert_total
352trunc' : machineTy (log2Bytes (n+m)) -> machineTy (log2Bytes n)
364trunc' : machineTy (log2Bytes (n+m)) -> machineTy (log2Bytes n)
353trunc' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))
365trunc' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))
354− | (O, O) = believe_me x
366+ | (O, O) = fixupTR (believe_me x)
355 | (O, S O) = believe_me (prim__truncB16_8 (believe_me x))
367 | (O, S O) = believe_me (prim__truncB16_8 (believe_me x))
356 | (O, S (S O)) = believe_me (prim__truncB32_8 (believe_me x))
368 | (O, S (S O)) = believe_me (prim__truncB32_8 (believe_me x))
357 | (O, S (S (S _))) = believe_me (prim__truncB64_8 (believe_me x))
369 | (O, S (S (S _))) = believe_me (prim__truncB64_8 (believe_me x))
358− | (S O, S O) = believe_me x
370+ | (S O, S O) = fixupTR (believe_me x)
359 | (S O, S (S O)) = believe_me (prim__truncB32_16 (believe_me x))
371 | (S O, S (S O)) = believe_me (prim__truncB32_16 (believe_me x))
360 | (S O, S (S (S _))) = believe_me (prim__truncB64_16 (believe_me x))
372 | (S O, S (S (S _))) = believe_me (prim__truncB64_16 (believe_me x))
361− | (S (S O), S (S O)) = believe_me x
373+ | (S (S O), S (S O)) = fixupTR (believe_me x)
362 | (S (S O), S (S (S _))) = believe_me (prim__truncB64_32 (believe_me x))
374 | (S (S O), S (S (S _))) = believe_me (prim__truncB64_32 (believe_me x))
363− | (S (S (S _)), S (S (S _))) = believe_me x
375+ | (S (S (S _)), S (S (S _))) = fixupTR (believe_me x)
365public partial
377public partial
366truncate : Bits (n+m) -> Bits n
378truncate : Bits (n+m) -> Bits n