@@ -15,7 +15,6 @@ nextBits x with (log2ceil x)
1515 | (S (S (S (S O)))) = Bits16
1616 | _ = Bits8
1717
18−abstract
1918data Bits : Nat -> Type where
2019 MkBits : {n : Nat} -> nextBits n -> Bits n
2120
@@ -57,7 +56,6 @@ intToBits' {n=n} x with (nextBits n)
5756 | Bits64 = let pad = (prim__intToB64 (cast (64-n))) in
5857 prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad
5958
60−public
6159intToBits : {n : Nat} -> Int -> Bits n
6260intToBits n = MkBits (intToBits' n)
6361
@@ -71,7 +69,6 @@ bitsShl' {n=n} x c with (nextBits n)
7169 | Bits32 = pad32 n prim__shlB32 x c
7270 | Bits64 = pad64 n prim__shlB64 x c
7371
74−public
7572bitsShl : Bits n -> Bits n -> Bits n
7673bitsShl (MkBits x) (MkBits y) = MkBits (bitsShl' x y)
7774
@@ -82,7 +79,6 @@ bitsLShr' {n=n} x c with (nextBits n)
8279 | Bits32 = prim__lshrB32 x c
8380 | Bits64 = prim__lshrB64 x c
8481
85−public
8682bitsLShr : Bits n -> Bits n -> Bits n
8783bitsLShr (MkBits x) (MkBits y) = MkBits (bitsLShr' x y)
8884
@@ -93,7 +89,6 @@ bitsAShr' {n=n} x c with (nextBits n)
9389 | Bits32 = prim__ashrB32 x c
9490 | Bits64 = prim__ashrB64 x c
9591
96−public
9792bitsAShr : Bits n -> Bits n -> Bits n
9893bitsAShr (MkBits x) (MkBits y) = MkBits (bitsAShr' x y)
9994
@@ -104,7 +99,6 @@ bitsAnd' {n=n} x y with (nextBits n)
10499 | Bits32 = prim__andB32 x y
105100 | Bits64 = prim__andB64 x y
106101
107−public
108102bitsAnd : Bits n -> Bits n -> Bits n
109103bitsAnd (MkBits x) (MkBits y) = MkBits (bitsAnd' x y)
110104
@@ -115,7 +109,6 @@ bitsOr' {n=n} x y with (nextBits n)
115109 | Bits32 = prim__orB32 x y
116110 | Bits64 = prim__orB64 x y
117111
118−public
119112bitsOr : Bits n -> Bits n -> Bits n
120113bitsOr (MkBits x) (MkBits y) = MkBits (bitsOr' x y)
121114
@@ -126,7 +119,6 @@ bitsXOr' {n=n} x y with (nextBits n)
126119 | Bits32 = prim__xorB32 x y
127120 | Bits64 = prim__xorB64 x y
128121
129−public
130122bitsXOr : Bits n -> Bits n -> Bits n
131123bitsXOr (MkBits x) (MkBits y) = MkBits (bitsXOr' x y)
132124
@@ -137,7 +129,6 @@ bitsAdd' {n=n} x y with (nextBits n)
137129 | Bits32 = pad32 n prim__addB32 x y
138130 | Bits64 = pad64 n prim__addB64 x y
139131
140−public
141132bitsAdd : Bits n -> Bits n -> Bits n
142133bitsAdd (MkBits x) (MkBits y) = MkBits (bitsAdd' x y)
143134
@@ -148,7 +139,6 @@ bitsSub' {n=n} x y with (nextBits n)
148139 | Bits32 = pad32 n prim__subB32 x y
149140 | Bits64 = pad64 n prim__subB64 x y
150141
151−public
152142bitsSub : Bits n -> Bits n -> Bits n
153143bitsSub (MkBits x) (MkBits y) = MkBits (bitsSub' x y)
154144
@@ -159,7 +149,6 @@ bitsMul' {n=n} x y with (nextBits n)
159149 | Bits32 = pad32 n prim__mulB32 x y
160150 | Bits64 = pad64 n prim__mulB64 x y
161151
162−public
163152bitsMul : Bits n -> Bits n -> Bits n
164153bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)
165154
@@ -170,7 +159,6 @@ bitsSDiv' {n=n} x y with (nextBits n)
170159 | Bits32 = prim__sdivB32 x y
171160 | Bits64 = prim__sdivB64 x y
172161
173−public
174162bitsSDiv : Bits n -> Bits n -> Bits n
175163bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)
176164
@@ -181,7 +169,6 @@ bitsUDiv' {n=n} x y with (nextBits n)
181169 | Bits32 = prim__udivB32 x y
182170 | Bits64 = prim__udivB64 x y
183171
184−public
185172bitsUDiv : Bits n -> Bits n -> Bits n
186173bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)
187174
@@ -192,7 +179,6 @@ bitsToStr' {n=n} x with (nextBits n)
192179 | Bits32 = prim__b32ToStr x
193180 | Bits64 = prim__b64ToStr x
194181
195−public
196182bitsToStr : Bits n -> String
197183bitsToStr (MkBits x) = bitsToStr' x
198184
@@ -203,12 +189,8 @@ bitsEq' {n=n} x y with (nextBits n)
203189 | Bits32 = prim__eqB32 x y
204190 | Bits64 = prim__eqB64 x y
205191
206−public
207−bitsEq : (x : Bits n) -> (y : Bits n) -> Equality x y
192+bitsEq : (x : Bits n) -> (y : Bits n) -> Bool
208193bitsEq (MkBits x) (MkBits y) =
209194 case (bitsEq' x y) of
210− 0 => Unequal uneq
211− _ => Equal eq
212− where
213− postulate uneq : {x : Bits n} -> {y : Bits n} -> x = y -> _|_
214− postulate eq : {x : Bits n} -> {y : Bits n} -> x = y
195+ 0 => False
196+ _ => True