git.iko.soy/Idris-dev
on master help sign in
Fix ashr behavior on non-native bitfield widths
bee324cBenjamin Saunders
lib/Prelude/Bits.idr+5−5
compare with master
unifiedsplit
@@ -122,12 +122,12 @@ public
122bitsLShr : Bits n -> Bits n -> Bits n
122bitsLShr : Bits n -> Bits n -> Bits n
123bitsLShr (MkBits x) (MkBits y) = MkBits (bitsLShr' x y)
123bitsLShr (MkBits x) (MkBits y) = MkBits (bitsLShr' x y)
124
124
125−bitsAShr' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
125+bitsAShr' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
126bitsAShr' {n=n} x c with (log2Bytes n)
126bitsAShr' {n=n} x c with (log2Bytes n)
127− | O = prim__ashrB8 x c
127+ | O = pad8' n prim__ashrB8 x c
128− | S O = prim__ashrB16 x c
128+ | S O = pad16' n prim__ashrB16 x c
129− | S (S O) = prim__ashrB32 x c
129+ | S (S O) = pad32' n prim__ashrB32 x c
130− | S (S (S _)) = prim__ashrB64 x c
130+ | S (S (S _)) = pad64' n prim__ashrB64 x c
131
131
132public
132public
133bitsAShr : Bits n -> Bits n -> Bits n
133bitsAShr : Bits n -> Bits n -> Bits n