@@ -21,7 +21,7 @@ machineTy (S (S (S _))) = Bits64
2121
2222public
2323data Bits : Nat -> Type where
24− MkBits : {n : Nat} -> machineTy (log2Bytes n) -> Bits n
24+ MkBits : machineTy (log2Bytes n) -> Bits n
2525
2626pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
2727pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
@@ -71,7 +71,7 @@ pow x y = if y > 0
7171 else 1
7272
7373%assert_total
74−intToBits' : {n : Nat} -> Int -> machineTy (log2Bytes n)
74+intToBits' : Int -> machineTy (log2Bytes n)
7575intToBits' {n=n} x with (log2Bytes n)
7676 | O = let pad = (prim__intToB8 (cast (8-n))) in
7777 prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad
@@ -83,14 +83,14 @@ intToBits' {n=n} x with (log2Bytes n)
8383 prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad
8484
8585public
86−intToBits : {n : Nat} -> Int -> Bits n
86+intToBits : Int -> Bits n
8787intToBits n = MkBits (intToBits' n)
8888
8989instance Cast Int (Bits n) where
9090 cast = intToBits
9191
92−unsafeBitsToInt' : {n : Nat} -> machineTy (log2Bytes n) -> Int
93−unsafeBitsToInt' {n=n} x with (log2Bytes n)
92+unsafeBitsToInt' : machineTy n -> Int
93+unsafeBitsToInt' {n=n} x with n
9494 | O = prim__B32ToInt (prim__zextB8_32 x)
9595 | S O = prim__B32ToInt (prim__zextB16_32 x)
9696 | S (S O) = prim__B32ToInt x
@@ -100,7 +100,7 @@ public
100100unsafeBitsToInt : Bits n -> Int
101101unsafeBitsToInt (MkBits x) = unsafeBitsToInt' x
102102
103−bitsShl' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
103+bitsShl' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
104104bitsShl' {n=n} x c with (log2Bytes n)
105105 | O = pad8' n prim__shlB8 x c
106106 | S O = pad16' n prim__shlB16 x c
@@ -111,8 +111,8 @@ public
111111bitsShl : Bits n -> Bits n -> Bits n
112112bitsShl (MkBits x) (MkBits y) = MkBits (bitsShl' x y)
113113
114−bitsLShr' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
115−bitsLShr' {n=n} x c with (log2Bytes n)
114+bitsLShr' : machineTy n -> machineTy n -> machineTy n
115+bitsLShr' {n=n} x c with n
116116 | O = prim__lshrB8 x c
117117 | S O = prim__lshrB16 x c
118118 | S (S O) = prim__lshrB32 x c
@@ -133,8 +133,8 @@ public
133133bitsAShr : Bits n -> Bits n -> Bits n
134134bitsAShr (MkBits x) (MkBits y) = MkBits (bitsAShr' x y)
135135
136−bitsAnd' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
137−bitsAnd' {n=n} x y with (log2Bytes n)
136+bitsAnd' : machineTy n -> machineTy n -> machineTy n
137+bitsAnd' {n=n} x y with n
138138 | O = prim__andB8 x y
139139 | S O = prim__andB16 x y
140140 | S (S O) = prim__andB32 x y
@@ -144,8 +144,8 @@ public
144144bitsAnd : Bits n -> Bits n -> Bits n
145145bitsAnd (MkBits x) (MkBits y) = MkBits (bitsAnd' x y)
146146
147−bitsOr' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
148−bitsOr' {n=n} x y with (log2Bytes n)
147+bitsOr' : machineTy n -> machineTy n -> machineTy n
148+bitsOr' {n=n} x y with n
149149 | O = prim__orB8 x y
150150 | S O = prim__orB16 x y
151151 | S (S O) = prim__orB32 x y
@@ -155,8 +155,8 @@ public
155155bitsOr : Bits n -> Bits n -> Bits n
156156bitsOr (MkBits x) (MkBits y) = MkBits (bitsOr' x y)
157157
158−bitsXOr' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
159−bitsXOr' {n=n} x y with (log2Bytes n)
158+bitsXOr' : machineTy n -> machineTy n -> machineTy n
159+bitsXOr' {n=n} x y with n
160160 | O = prim__xorB8 x y
161161 | S O = prim__xorB16 x y
162162 | S (S O) = prim__xorB32 x y
@@ -166,7 +166,7 @@ public
166166bitsXOr : Bits n -> Bits n -> Bits n
167167bitsXOr (MkBits x) (MkBits y) = MkBits (bitsXOr' x y)
168168
169−bitsAdd' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
169+bitsAdd' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
170170bitsAdd' {n=n} x y with (log2Bytes n)
171171 | O = pad8 n prim__addB8 x y
172172 | S O = pad16 n prim__addB16 x y
@@ -177,7 +177,7 @@ public
177177bitsAdd : Bits n -> Bits n -> Bits n
178178bitsAdd (MkBits x) (MkBits y) = MkBits (bitsAdd' x y)
179179
180−bitsSub' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
180+bitsSub' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
181181bitsSub' {n=n} x y with (log2Bytes n)
182182 | O = pad8 n prim__subB8 x y
183183 | S O = pad16 n prim__subB16 x y
@@ -188,7 +188,7 @@ public
188188bitsSub : Bits n -> Bits n -> Bits n
189189bitsSub (MkBits x) (MkBits y) = MkBits (bitsSub' x y)
190190
191−bitsMul' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
191+bitsMul' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
192192bitsMul' {n=n} x y with (log2Bytes n)
193193 | O = pad8 n prim__mulB8 x y
194194 | S O = pad16 n prim__mulB16 x y
@@ -200,7 +200,7 @@ bitsMul : Bits n -> Bits n -> Bits n
200200bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)
201201
202202partial
203−bitsSDiv' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
203+bitsSDiv' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
204204bitsSDiv' {n=n} x y with (log2Bytes n)
205205 | O = prim__sdivB8 x y
206206 | S O = prim__sdivB16 x y
@@ -212,7 +212,7 @@ bitsSDiv : Bits n -> Bits n -> Bits n
212212bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)
213213
214214partial
215−bitsUDiv' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
215+bitsUDiv' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
216216bitsUDiv' {n=n} x y with (log2Bytes n)
217217 | O = prim__udivB8 x y
218218 | S O = prim__udivB16 x y
@@ -224,7 +224,7 @@ bitsUDiv : Bits n -> Bits n -> Bits n
224224bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)
225225
226226partial
227−bitsSRem' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
227+bitsSRem' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
228228bitsSRem' {n=n} x y with (log2Bytes n)
229229 | O = prim__sremB8 x y
230230 | S O = prim__sremB16 x y
@@ -236,7 +236,7 @@ bitsSRem : Bits n -> Bits n -> Bits n
236236bitsSRem (MkBits x) (MkBits y) = MkBits (bitsSRem' x y)
237237
238238partial
239−bitsURem' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
239+bitsURem' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
240240bitsURem' {n=n} x y with (log2Bytes n)
241241 | O = prim__uremB8 x y
242242 | S O = prim__uremB16 x y
@@ -248,59 +248,59 @@ bitsURem : Bits n -> Bits n -> Bits n
248248bitsURem (MkBits x) (MkBits y) = MkBits (bitsURem' x y)
249249
250250-- TODO: Proofy comparisons via postulates
251−bitsLt' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int
252−bitsLt' {n=n} x y with (log2Bytes n)
251+bitsLt' : machineTy n -> machineTy n -> Int
252+bitsLt' {n=n} x y with n
253253 | O = prim__ltB8 x y
254254 | S O = prim__ltB16 x y
255255 | S (S O) = prim__ltB32 x y
256256 | S (S (S _)) = prim__ltB64 x y
257257
258258public
259−bitsLt : (x : Bits n) -> (y : Bits n) -> Bool
259+bitsLt : Bits n -> Bits n -> Bool
260260bitsLt (MkBits x) (MkBits y) = bitsLt' x y /= 0
261261
262−bitsLte' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int
263−bitsLte' {n=n} x y with (log2Bytes n)
262+bitsLte' : machineTy n -> machineTy n -> Int
263+bitsLte' {n=n} x y with n
264264 | O = prim__lteB8 x y
265265 | S O = prim__lteB16 x y
266266 | S (S O) = prim__lteB32 x y
267267 | S (S (S _)) = prim__lteB64 x y
268268
269269public
270−bitsLte : (x : Bits n) -> (y : Bits n) -> Bool
270+bitsLte : Bits n -> Bits n -> Bool
271271bitsLte (MkBits x) (MkBits y) = bitsLte' x y /= 0
272272
273−bitsEq' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int
274−bitsEq' {n=n} x y with (log2Bytes n)
273+bitsEq' : machineTy n -> machineTy n -> Int
274+bitsEq' {n=n} x y with n
275275 | O = prim__eqB8 x y
276276 | S O = prim__eqB16 x y
277277 | S (S O) = prim__eqB32 x y
278278 | S (S (S _)) = prim__eqB64 x y
279279
280280public
281−bitsEq : (x : Bits n) -> (y : Bits n) -> Bool
281+bitsEq : Bits n -> Bits n -> Bool
282282bitsEq (MkBits x) (MkBits y) = bitsEq' x y /= 0
283283
284−bitsGte' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int
285−bitsGte' {n=n} x y with (log2Bytes n)
284+bitsGte' : machineTy n -> machineTy n -> Int
285+bitsGte' {n=n} x y with n
286286 | O = prim__gteB8 x y
287287 | S O = prim__gteB16 x y
288288 | S (S O) = prim__gteB32 x y
289289 | S (S (S _)) = prim__gteB64 x y
290290
291291public
292−bitsGte : (x : Bits n) -> (y : Bits n) -> Bool
292+bitsGte : Bits n -> Bits n -> Bool
293293bitsGte (MkBits x) (MkBits y) = bitsGte' x y /= 0
294294
295−bitsGt' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int
296−bitsGt' {n=n} x y with (log2Bytes n)
295+bitsGt' : machineTy n -> machineTy n -> Int
296+bitsGt' {n=n} x y with n
297297 | O = prim__gtB8 x y
298298 | S O = prim__gtB16 x y
299299 | S (S O) = prim__gtB32 x y
300300 | S (S (S _)) = prim__gtB64 x y
301301
302302public
303−bitsGt : (x : Bits n) -> (y : Bits n) -> Bool
303+bitsGt : Bits n -> Bits n -> Bool
304304bitsGt (MkBits x) (MkBits y) = bitsGt' x y /= 0
305305
306306instance Eq (Bits n) where