@@ -19,12 +19,39 @@ abstract
1919data Bits : Nat -> Type where
2020 MkBits : {n : Nat} -> nextBits n -> Bits n
2121
22+pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
23+pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
24+ where
25+ pad = (prim__intToB8 (cast (8-n)))
26+
27+pad16 : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
28+pad16 n f x y = prim__lshrB16 (f (prim__shlB16 x pad) (prim__shlB16 y pad)) pad
29+ where
30+ pad = (prim__intToB16 (cast (16-n)))
31+
32+pad32 : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
33+pad32 n f x y = prim__lshrB32 (f (prim__shlB32 x pad) (prim__shlB32 y pad)) pad
34+ where
35+ pad = (prim__intToB32 (cast (32-n)))
36+
37+pad64 : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
38+pad64 n f x y = prim__lshrB64 (f (prim__shlB64 x pad) (prim__shlB64 y pad)) pad
39+ where
40+ pad = (prim__intToB64 (cast (64-n)))
41+
42+%assert_total
43+pow : Int -> Int -> Int
44+pow x y = if y > 0
45+ then x * (pow x (y - 1))
46+ else 1
47+
48+%assert_total
2249intToBits' : {n: Nat} -> Int -> nextBits n
2350intToBits' {n=n} x with (nextBits n)
24− | Bits8 = prim__intToB8 x
25− | Bits16 = prim__intToB16 x
26− | Bits32 = prim__intToB32 x
27− | Bits64 = prim__intToB64 x
51+ | Bits8 = prim__intToB8 (x `mod` (pow 2 (cast n)))
52+ | Bits16 = prim__intToB16 (x `mod` (pow 2 (cast n)))
53+ | Bits32 = prim__intToB32 (x `mod` (pow 2 (cast n)))
54+ | Bits64 = prim__intToB64 (x `mod` (pow 2 (cast n)))
2855
2956public
3057intToBits : {n : Nat} -> Int -> Bits n
@@ -32,10 +59,10 @@ intToBits n = MkBits (intToBits' n)
3259
3360bitsShl' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
3461bitsShl' {n=n} x c with (nextBits n)
35− | Bits8 = prim__shlB8 x c
36− | Bits16 = prim__shlB16 x c
37− | Bits32 = prim__shlB32 x c
38− | Bits64 = prim__shlB64 x c
62+ | Bits8 = pad8 n prim__shlB8 x c
63+ | Bits16 = pad16 n prim__shlB16 x c
64+ | Bits32 = pad32 n prim__shlB32 x c
65+ | Bits64 = pad64 n prim__shlB64 x c
3966
4067public
4168bitsShl : Bits n -> Bits n -> Bits n
@@ -98,14 +125,10 @@ bitsXOr (MkBits x) (MkBits y) = MkBits (bitsXOr' x y)
98125
99126bitsAdd' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
100127bitsAdd' {n=n} x y with (nextBits n)
101− | Bits8 = let pad = prim__intToB8 (the Int (cast (8-n))) in
102− prim__lshrB8 (prim__addB8 (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
103− | Bits16 = let pad = prim__intToB16 (the Int (cast (16-n))) in
104− prim__lshrB16 (prim__addB16 (prim__shlB16 x pad) (prim__shlB16 y pad)) pad
105− | Bits32 = let pad = prim__intToB32 (the Int (cast (32-n))) in
106− prim__lshrB32 (prim__addB32 (prim__shlB32 x pad) (prim__shlB32 y pad)) pad
107− | Bits64 = let pad = prim__intToB64 (the Int (cast (64-n))) in
108− prim__lshrB64 (prim__addB64 (prim__shlB64 x pad) (prim__shlB64 y pad)) pad
128+ | Bits8 = pad8 n prim__addB8 x y
129+ | Bits16 = pad16 n prim__addB16 x y
130+ | Bits32 = pad32 n prim__addB32 x y
131+ | Bits64 = pad64 n prim__addB64 x y
109132
110133public
111134bitsAdd : Bits n -> Bits n -> Bits n
@@ -113,10 +136,10 @@ bitsAdd (MkBits x) (MkBits y) = MkBits (bitsAdd' x y)
113136
114137bitsSub' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
115138bitsSub' {n=n} x y with (nextBits n)
116− | Bits8 = prim__subB8 x y
117− | Bits16 = prim__subB16 x y
118− | Bits32 = prim__subB32 x y
119− | Bits64 = prim__subB64 x y
139+ | Bits8 = pad8 n prim__subB8 x y
140+ | Bits16 = pad16 n prim__subB16 x y
141+ | Bits32 = pad32 n prim__subB32 x y
142+ | Bits64 = pad64 n prim__subB64 x y
120143
121144public
122145bitsSub : Bits n -> Bits n -> Bits n
@@ -124,10 +147,10 @@ bitsSub (MkBits x) (MkBits y) = MkBits (bitsSub' x y)
124147
125148bitsMul' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
126149bitsMul' {n=n} x y with (nextBits n)
127− | Bits8 = prim__mulB8 x y
128− | Bits16 = prim__mulB16 x y
129− | Bits32 = prim__mulB32 x y
130− | Bits64 = prim__mulB64 x y
150+ | Bits8 = pad8 n prim__mulB8 x y
151+ | Bits16 = pad16 n prim__mulB16 x y
152+ | Bits32 = pad32 n prim__mulB32 x y
153+ | Bits64 = pad64 n prim__mulB64 x y
131154
132155public
133156bitsMul : Bits n -> Bits n -> Bits n