@@ -21,7 +21,7 @@ machineTy (S (S (S _))) = Bits64
23data Bits : Nat -> Type where
23data Bits : Nat -> Type where
24− MkBits : {n : Nat} -> machineTy (log2Bytes n) -> Bits n
24+ MkBits : machineTy (log2Bytes n) -> Bits n
26pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
26pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
27pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
27pad8 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
73%assert_total
73%assert_total
74−intToBits' : {n : Nat} -> Int -> machineTy (log2Bytes n)
74+intToBits' : Int -> machineTy (log2Bytes n)
75intToBits' {n=n} x with (log2Bytes n)
75intToBits' {n=n} x with (log2Bytes n)
76 | O = let pad = (prim__intToB8 (cast (8-n))) in
76 | O = let pad = (prim__intToB8 (cast (8-n))) in
77 prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad
77 prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad
@@ -83,14 +83,14 @@ intToBits' {n=n} x with (log2Bytes n)
83 prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad
83 prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad
86−intToBits : {n : Nat} -> Int -> Bits n
86+intToBits : Int -> Bits n
87intToBits n = MkBits (intToBits' n)
87intToBits n = MkBits (intToBits' n)
89instance Cast Int (Bits n) where
89instance Cast Int (Bits n) where
90 cast = intToBits
90 cast = intToBits
92−unsafeBitsToInt' : {n : Nat} -> machineTy (log2Bytes n) -> Int
92+unsafeBitsToInt' : machineTy n -> Int
93−unsafeBitsToInt' {n=n} x with (log2Bytes n)
93+unsafeBitsToInt' {n=n} x with n
94 | O = prim__B32ToInt (prim__zextB8_32 x)
94 | O = prim__B32ToInt (prim__zextB8_32 x)
95 | S O = prim__B32ToInt (prim__zextB16_32 x)
95 | S O = prim__B32ToInt (prim__zextB16_32 x)
96 | S (S O) = prim__B32ToInt x
96 | S (S O) = prim__B32ToInt x
@@ -100,7 +100,7 @@ public
100unsafeBitsToInt : Bits n -> Int
100unsafeBitsToInt : Bits n -> Int
101unsafeBitsToInt (MkBits x) = unsafeBitsToInt' x
101unsafeBitsToInt (MkBits x) = unsafeBitsToInt' x
103−bitsShl' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
103+bitsShl' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
104bitsShl' {n=n} x c with (log2Bytes n)
104bitsShl' {n=n} x c with (log2Bytes n)
105 | O = pad8' n prim__shlB8 x c
105 | O = pad8' n prim__shlB8 x c
106 | S O = pad16' n prim__shlB16 x c
106 | S O = pad16' n prim__shlB16 x c
@@ -111,8 +111,8 @@ public
111bitsShl : Bits n -> Bits n -> Bits n
111bitsShl : Bits n -> Bits n -> Bits n
112bitsShl (MkBits x) (MkBits y) = MkBits (bitsShl' x y)
112bitsShl (MkBits x) (MkBits y) = MkBits (bitsShl' x y)
114−bitsLShr' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
114+bitsLShr' : machineTy n -> machineTy n -> machineTy n
115−bitsLShr' {n=n} x c with (log2Bytes n)
115+bitsLShr' {n=n} x c with n
116 | O = prim__lshrB8 x c
116 | O = prim__lshrB8 x c
117 | S O = prim__lshrB16 x c
117 | S O = prim__lshrB16 x c
118 | S (S O) = prim__lshrB32 x c
118 | S (S O) = prim__lshrB32 x c
@@ -133,8 +133,8 @@ public
133bitsAShr : Bits n -> Bits n -> Bits n
133bitsAShr : Bits n -> Bits n -> Bits n
134bitsAShr (MkBits x) (MkBits y) = MkBits (bitsAShr' x y)
134bitsAShr (MkBits x) (MkBits y) = MkBits (bitsAShr' x y)
136−bitsAnd' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
136+bitsAnd' : machineTy n -> machineTy n -> machineTy n
137−bitsAnd' {n=n} x y with (log2Bytes n)
137+bitsAnd' {n=n} x y with n
138 | O = prim__andB8 x y
138 | O = prim__andB8 x y
139 | S O = prim__andB16 x y
139 | S O = prim__andB16 x y
140 | S (S O) = prim__andB32 x y
140 | S (S O) = prim__andB32 x y
@@ -144,8 +144,8 @@ public
144bitsAnd : Bits n -> Bits n -> Bits n
144bitsAnd : Bits n -> Bits n -> Bits n
145bitsAnd (MkBits x) (MkBits y) = MkBits (bitsAnd' x y)
145bitsAnd (MkBits x) (MkBits y) = MkBits (bitsAnd' x y)
147−bitsOr' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
147+bitsOr' : machineTy n -> machineTy n -> machineTy n
148−bitsOr' {n=n} x y with (log2Bytes n)
148+bitsOr' {n=n} x y with n
149 | O = prim__orB8 x y
149 | O = prim__orB8 x y
150 | S O = prim__orB16 x y
150 | S O = prim__orB16 x y
151 | S (S O) = prim__orB32 x y
151 | S (S O) = prim__orB32 x y
@@ -155,8 +155,8 @@ public
155bitsOr : Bits n -> Bits n -> Bits n
155bitsOr : Bits n -> Bits n -> Bits n
156bitsOr (MkBits x) (MkBits y) = MkBits (bitsOr' x y)
156bitsOr (MkBits x) (MkBits y) = MkBits (bitsOr' x y)
158−bitsXOr' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
158+bitsXOr' : machineTy n -> machineTy n -> machineTy n
159−bitsXOr' {n=n} x y with (log2Bytes n)
159+bitsXOr' {n=n} x y with n
160 | O = prim__xorB8 x y
160 | O = prim__xorB8 x y
161 | S O = prim__xorB16 x y
161 | S O = prim__xorB16 x y
162 | S (S O) = prim__xorB32 x y
162 | S (S O) = prim__xorB32 x y
@@ -166,7 +166,7 @@ public
166bitsXOr : Bits n -> Bits n -> Bits n
166bitsXOr : Bits n -> Bits n -> Bits n
167bitsXOr (MkBits x) (MkBits y) = MkBits (bitsXOr' x y)
167bitsXOr (MkBits x) (MkBits y) = MkBits (bitsXOr' x y)
169−bitsAdd' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
169+bitsAdd' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
170bitsAdd' {n=n} x y with (log2Bytes n)
170bitsAdd' {n=n} x y with (log2Bytes n)
171 | O = pad8 n prim__addB8 x y
171 | O = pad8 n prim__addB8 x y
172 | S O = pad16 n prim__addB16 x y
172 | S O = pad16 n prim__addB16 x y
@@ -177,7 +177,7 @@ public
177bitsAdd : Bits n -> Bits n -> Bits n
177bitsAdd : Bits n -> Bits n -> Bits n
178bitsAdd (MkBits x) (MkBits y) = MkBits (bitsAdd' x y)
178bitsAdd (MkBits x) (MkBits y) = MkBits (bitsAdd' x y)
180−bitsSub' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
180+bitsSub' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
181bitsSub' {n=n} x y with (log2Bytes n)
181bitsSub' {n=n} x y with (log2Bytes n)
182 | O = pad8 n prim__subB8 x y
182 | O = pad8 n prim__subB8 x y
183 | S O = pad16 n prim__subB16 x y
183 | S O = pad16 n prim__subB16 x y
@@ -188,7 +188,7 @@ public
188bitsSub : Bits n -> Bits n -> Bits n
188bitsSub : Bits n -> Bits n -> Bits n
189bitsSub (MkBits x) (MkBits y) = MkBits (bitsSub' x y)
189bitsSub (MkBits x) (MkBits y) = MkBits (bitsSub' x y)
191−bitsMul' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
191+bitsMul' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
192bitsMul' {n=n} x y with (log2Bytes n)
192bitsMul' {n=n} x y with (log2Bytes n)
193 | O = pad8 n prim__mulB8 x y
193 | O = pad8 n prim__mulB8 x y
194 | S O = pad16 n prim__mulB16 x y
194 | S O = pad16 n prim__mulB16 x y
@@ -200,7 +200,7 @@ bitsMul : Bits n -> Bits n -> Bits n
200bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)
200bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)
203−bitsSDiv' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
203+bitsSDiv' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
204bitsSDiv' {n=n} x y with (log2Bytes n)
204bitsSDiv' {n=n} x y with (log2Bytes n)
205 | O = prim__sdivB8 x y
205 | O = prim__sdivB8 x y
206 | S O = prim__sdivB16 x y
206 | S O = prim__sdivB16 x y
@@ -212,7 +212,7 @@ bitsSDiv : Bits n -> Bits n -> Bits n
212bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)
212bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)
215−bitsUDiv' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
215+bitsUDiv' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
216bitsUDiv' {n=n} x y with (log2Bytes n)
216bitsUDiv' {n=n} x y with (log2Bytes n)
217 | O = prim__udivB8 x y
217 | O = prim__udivB8 x y
218 | S O = prim__udivB16 x y
218 | S O = prim__udivB16 x y
@@ -224,7 +224,7 @@ bitsUDiv : Bits n -> Bits n -> Bits n
224bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)
224bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)
227−bitsSRem' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
227+bitsSRem' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
228bitsSRem' {n=n} x y with (log2Bytes n)
228bitsSRem' {n=n} x y with (log2Bytes n)
229 | O = prim__sremB8 x y
229 | O = prim__sremB8 x y
230 | S O = prim__sremB16 x y
230 | S O = prim__sremB16 x y
@@ -236,7 +236,7 @@ bitsSRem : Bits n -> Bits n -> Bits n
236bitsSRem (MkBits x) (MkBits y) = MkBits (bitsSRem' x y)
236bitsSRem (MkBits x) (MkBits y) = MkBits (bitsSRem' x y)
239−bitsURem' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
239+bitsURem' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
240bitsURem' {n=n} x y with (log2Bytes n)
240bitsURem' {n=n} x y with (log2Bytes n)
241 | O = prim__uremB8 x y
241 | O = prim__uremB8 x y
242 | S O = prim__uremB16 x y
242 | S O = prim__uremB16 x y
@@ -248,59 +248,59 @@ bitsURem : Bits n -> Bits n -> Bits n
248bitsURem (MkBits x) (MkBits y) = MkBits (bitsURem' x y)
248bitsURem (MkBits x) (MkBits y) = MkBits (bitsURem' x y)
250-- TODO: Proofy comparisons via postulates
250-- TODO: Proofy comparisons via postulates
251−bitsLt' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int
251+bitsLt' : machineTy n -> machineTy n -> Int
252−bitsLt' {n=n} x y with (log2Bytes n)
252+bitsLt' {n=n} x y with n
253 | O = prim__ltB8 x y
253 | O = prim__ltB8 x y
254 | S O = prim__ltB16 x y
254 | S O = prim__ltB16 x y
255 | S (S O) = prim__ltB32 x y
255 | S (S O) = prim__ltB32 x y
256 | S (S (S _)) = prim__ltB64 x y
256 | S (S (S _)) = prim__ltB64 x y
259−bitsLt : (x : Bits n) -> (y : Bits n) -> Bool
259+bitsLt : Bits n -> Bits n -> Bool
260bitsLt (MkBits x) (MkBits y) = bitsLt' x y /= 0
260bitsLt (MkBits x) (MkBits y) = bitsLt' x y /= 0
262−bitsLte' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int
262+bitsLte' : machineTy n -> machineTy n -> Int
263−bitsLte' {n=n} x y with (log2Bytes n)
263+bitsLte' {n=n} x y with n
264 | O = prim__lteB8 x y
264 | O = prim__lteB8 x y
265 | S O = prim__lteB16 x y
265 | S O = prim__lteB16 x y
266 | S (S O) = prim__lteB32 x y
266 | S (S O) = prim__lteB32 x y
267 | S (S (S _)) = prim__lteB64 x y
267 | S (S (S _)) = prim__lteB64 x y
270−bitsLte : (x : Bits n) -> (y : Bits n) -> Bool
270+bitsLte : Bits n -> Bits n -> Bool
271bitsLte (MkBits x) (MkBits y) = bitsLte' x y /= 0
271bitsLte (MkBits x) (MkBits y) = bitsLte' x y /= 0
273−bitsEq' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int
273+bitsEq' : machineTy n -> machineTy n -> Int
274−bitsEq' {n=n} x y with (log2Bytes n)
274+bitsEq' {n=n} x y with n
275 | O = prim__eqB8 x y
275 | O = prim__eqB8 x y
276 | S O = prim__eqB16 x y
276 | S O = prim__eqB16 x y
277 | S (S O) = prim__eqB32 x y
277 | S (S O) = prim__eqB32 x y
278 | S (S (S _)) = prim__eqB64 x y
278 | S (S (S _)) = prim__eqB64 x y
281−bitsEq : (x : Bits n) -> (y : Bits n) -> Bool
281+bitsEq : Bits n -> Bits n -> Bool
282bitsEq (MkBits x) (MkBits y) = bitsEq' x y /= 0
282bitsEq (MkBits x) (MkBits y) = bitsEq' x y /= 0
284−bitsGte' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int
284+bitsGte' : machineTy n -> machineTy n -> Int
285−bitsGte' {n=n} x y with (log2Bytes n)
285+bitsGte' {n=n} x y with n
286 | O = prim__gteB8 x y
286 | O = prim__gteB8 x y
287 | S O = prim__gteB16 x y
287 | S O = prim__gteB16 x y
288 | S (S O) = prim__gteB32 x y
288 | S (S O) = prim__gteB32 x y
289 | S (S (S _)) = prim__gteB64 x y
289 | S (S (S _)) = prim__gteB64 x y
292−bitsGte : (x : Bits n) -> (y : Bits n) -> Bool
292+bitsGte : Bits n -> Bits n -> Bool
293bitsGte (MkBits x) (MkBits y) = bitsGte' x y /= 0
293bitsGte (MkBits x) (MkBits y) = bitsGte' x y /= 0
295−bitsGt' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int
295+bitsGt' : machineTy n -> machineTy n -> Int
296−bitsGt' {n=n} x y with (log2Bytes n)
296+bitsGt' {n=n} x y with n
297 | O = prim__gtB8 x y
297 | O = prim__gtB8 x y
298 | S O = prim__gtB16 x y
298 | S O = prim__gtB16 x y
299 | S (S O) = prim__gtB32 x y
299 | S (S O) = prim__gtB32 x y
300 | S (S (S _)) = prim__gtB64 x y
300 | S (S (S _)) = prim__gtB64 x y
303−bitsGt : (x : Bits n) -> (y : Bits n) -> Bool
303+bitsGt : Bits n -> Bits n -> Bool
304bitsGt (MkBits x) (MkBits y) = bitsGt' x y /= 0
304bitsGt (MkBits x) (MkBits y) = bitsGt' x y /= 0
306instance Eq (Bits n) where
306instance Eq (Bits n) where