@@ -89,233 +89,214 @@ intToBits n = MkBits (intToBits' n)
8989instance Cast Int (Bits n) where
9090 cast = intToBits
9191
92−unsafeBitsToInt' : machineTy n -> Int
93−unsafeBitsToInt' {n=n} x with n
92+bitsToInt' : machineTy n -> Int
93+bitsToInt' {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
9797 | S (S (S _)) = prim__B32ToInt (prim__truncB64_32 x)
9898
9999public
100−unsafeBitsToInt : Bits n -> Int
101−unsafeBitsToInt (MkBits x) = unsafeBitsToInt' x
100+bitsToInt : Bits n -> Int
101+bitsToInt (MkBits x) = bitsToInt' x
102102
103−bitsShl' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
104−bitsShl' {n=n} x c with (log2Bytes n)
103+shiftLeft' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
104+shiftLeft' {n=n} x c with (log2Bytes n)
105105 | O = pad8' n prim__shlB8 x c
106106 | S O = pad16' n prim__shlB16 x c
107107 | S (S O) = pad32' n prim__shlB32 x c
108108 | S (S (S _)) = pad64' n prim__shlB64 x c
109109
110110public
111−bitsShl : Bits n -> Bits n -> Bits n
112−bitsShl (MkBits x) (MkBits y) = MkBits (bitsShl' x y)
111+shiftLeft : Bits n -> Bits n -> Bits n
112+shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
113113
114−bitsLShr' : machineTy n -> machineTy n -> machineTy n
115−bitsLShr' {n=n} x c with n
114+shiftRightLogical' : machineTy n -> machineTy n -> machineTy n
115+shiftRightLogical' {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
119119 | S (S (S _)) = prim__lshrB64 x c
120120
121121public
122−bitsLShr : Bits n -> Bits n -> Bits n
123−bitsLShr (MkBits x) (MkBits y) = MkBits (bitsLShr' x y)
122+shiftRightLogical : Bits n -> Bits n -> Bits n
123+shiftRightLogical (MkBits x) (MkBits y) = MkBits (shiftRightLogical' x y)
124124
125−bitsAShr' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
126−bitsAShr' {n=n} x c with (log2Bytes n)
125+shiftRightArithmetic' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
126+shiftRightArithmetic' {n=n} x c with (log2Bytes n)
127127 | O = pad8' n prim__ashrB8 x c
128128 | S O = pad16' n prim__ashrB16 x c
129129 | S (S O) = pad32' n prim__ashrB32 x c
130130 | S (S (S _)) = pad64' n prim__ashrB64 x c
131131
132132public
133−bitsAShr : Bits n -> Bits n -> Bits n
134−bitsAShr (MkBits x) (MkBits y) = MkBits (bitsAShr' x y)
133+shiftRightArithmetic : Bits n -> Bits n -> Bits n
134+shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
135135
136−bitsAnd' : machineTy n -> machineTy n -> machineTy n
137−bitsAnd' {n=n} x y with n
136+and' : machineTy n -> machineTy n -> machineTy n
137+and' {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
141141 | S (S (S _)) = prim__andB64 x y
142142
143143public
144−bitsAnd : Bits n -> Bits n -> Bits n
145−bitsAnd (MkBits x) (MkBits y) = MkBits (bitsAnd' x y)
144+and : Bits n -> Bits n -> Bits n
145+and (MkBits x) (MkBits y) = MkBits (and' x y)
146146
147−bitsOr' : machineTy n -> machineTy n -> machineTy n
148−bitsOr' {n=n} x y with n
147+or' : machineTy n -> machineTy n -> machineTy n
148+or' {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
152152 | S (S (S _)) = prim__orB64 x y
153153
154154public
155−bitsOr : Bits n -> Bits n -> Bits n
156−bitsOr (MkBits x) (MkBits y) = MkBits (bitsOr' x y)
155+or : Bits n -> Bits n -> Bits n
156+or (MkBits x) (MkBits y) = MkBits (or' x y)
157157
158−bitsXOr' : machineTy n -> machineTy n -> machineTy n
159−bitsXOr' {n=n} x y with n
158+xor' : machineTy n -> machineTy n -> machineTy n
159+xor' {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
163163 | S (S (S _)) = prim__xorB64 x y
164164
165165public
166−bitsXOr : Bits n -> Bits n -> Bits n
167−bitsXOr (MkBits x) (MkBits y) = MkBits (bitsXOr' x y)
166+xor : Bits n -> Bits n -> Bits n
167+xor (MkBits x) (MkBits y) = MkBits (xor' x y)
168168
169−bitsAdd' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
170−bitsAdd' {n=n} x y with (log2Bytes n)
169+plus' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
170+plus' {n=n} x y with (log2Bytes n)
171171 | O = pad8 n prim__addB8 x y
172172 | S O = pad16 n prim__addB16 x y
173173 | S (S O) = pad32 n prim__addB32 x y
174174 | S (S (S _)) = pad64 n prim__addB64 x y
175175
176176public
177−bitsAdd : Bits n -> Bits n -> Bits n
178−bitsAdd (MkBits x) (MkBits y) = MkBits (bitsAdd' x y)
177+plus : Bits n -> Bits n -> Bits n
178+plus (MkBits x) (MkBits y) = MkBits (plus' x y)
179179
180−bitsSub' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
181−bitsSub' {n=n} x y with (log2Bytes n)
180+minus' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
181+minus' {n=n} x y with (log2Bytes n)
182182 | O = pad8 n prim__subB8 x y
183183 | S O = pad16 n prim__subB16 x y
184184 | S (S O) = pad32 n prim__subB32 x y
185185 | S (S (S _)) = pad64 n prim__subB64 x y
186186
187187public
188−bitsSub : Bits n -> Bits n -> Bits n
189−bitsSub (MkBits x) (MkBits y) = MkBits (bitsSub' x y)
188+minus : Bits n -> Bits n -> Bits n
189+minus (MkBits x) (MkBits y) = MkBits (minus' x y)
190190
191−bitsMul' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
192−bitsMul' {n=n} x y with (log2Bytes n)
191+times' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
192+times' {n=n} x y with (log2Bytes n)
193193 | O = pad8 n prim__mulB8 x y
194194 | S O = pad16 n prim__mulB16 x y
195195 | S (S O) = pad32 n prim__mulB32 x y
196196 | S (S (S _)) = pad64 n prim__mulB64 x y
197197
198198public
199−bitsMul : Bits n -> Bits n -> Bits n
200−bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)
199+times : Bits n -> Bits n -> Bits n
200+times (MkBits x) (MkBits y) = MkBits (times' x y)
201201
202202partial
203−bitsSDiv' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
204−bitsSDiv' {n=n} x y with (log2Bytes n)
203+sdiv' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
204+sdiv' {n=n} x y with (log2Bytes n)
205205 | O = prim__sdivB8 x y
206206 | S O = prim__sdivB16 x y
207207 | S (S O) = prim__sdivB32 x y
208208 | S (S (S _)) = prim__sdivB64 x y
209209
210210public partial
211−bitsSDiv : Bits n -> Bits n -> Bits n
212−bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)
211+sdiv : Bits n -> Bits n -> Bits n
212+sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)
213213
214214partial
215−bitsUDiv' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
216−bitsUDiv' {n=n} x y with (log2Bytes n)
215+udiv' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
216+udiv' {n=n} x y with (log2Bytes n)
217217 | O = prim__udivB8 x y
218218 | S O = prim__udivB16 x y
219219 | S (S O) = prim__udivB32 x y
220220 | S (S (S _)) = prim__udivB64 x y
221221
222222public partial
223−bitsUDiv : Bits n -> Bits n -> Bits n
224−bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)
223+udiv : Bits n -> Bits n -> Bits n
224+udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)
225225
226226partial
227−bitsSRem' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
228−bitsSRem' {n=n} x y with (log2Bytes n)
227+srem' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
228+srem' {n=n} x y with (log2Bytes n)
229229 | O = prim__sremB8 x y
230230 | S O = prim__sremB16 x y
231231 | S (S O) = prim__sremB32 x y
232232 | S (S (S _)) = prim__sremB64 x y
233233
234234public partial
235−bitsSRem : Bits n -> Bits n -> Bits n
236−bitsSRem (MkBits x) (MkBits y) = MkBits (bitsSRem' x y)
235+srem : Bits n -> Bits n -> Bits n
236+srem (MkBits x) (MkBits y) = MkBits (srem' x y)
237237
238238partial
239−bitsURem' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
240−bitsURem' {n=n} x y with (log2Bytes n)
239+urem' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
240+urem' {n=n} x y with (log2Bytes n)
241241 | O = prim__uremB8 x y
242242 | S O = prim__uremB16 x y
243243 | S (S O) = prim__uremB32 x y
244244 | S (S (S _)) = prim__uremB64 x y
245245
246246public partial
247−bitsURem : Bits n -> Bits n -> Bits n
248−bitsURem (MkBits x) (MkBits y) = MkBits (bitsURem' x y)
247+urem : Bits n -> Bits n -> Bits n
248+urem (MkBits x) (MkBits y) = MkBits (urem' x y)
249249
250250-- TODO: Proofy comparisons via postulates
251−bitsLt' : machineTy n -> machineTy n -> Int
252−bitsLt' {n=n} x y with n
251+lt : machineTy n -> machineTy n -> Int
252+lt {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
258−public
259−bitsLt : Bits n -> Bits n -> Bool
260−bitsLt (MkBits x) (MkBits y) = bitsLt' x y /= 0
261−
262−bitsLte' : machineTy n -> machineTy n -> Int
263−bitsLte' {n=n} x y with n
258+lte : machineTy n -> machineTy n -> Int
259+lte {n=n} x y with n
264260 | O = prim__lteB8 x y
265261 | S O = prim__lteB16 x y
266262 | S (S O) = prim__lteB32 x y
267263 | S (S (S _)) = prim__lteB64 x y
268264
269−public
270−bitsLte : Bits n -> Bits n -> Bool
271−bitsLte (MkBits x) (MkBits y) = bitsLte' x y /= 0
272−
273−bitsEq' : machineTy n -> machineTy n -> Int
274−bitsEq' {n=n} x y with n
265+eq : machineTy n -> machineTy n -> Int
266+eq {n=n} x y with n
275267 | O = prim__eqB8 x y
276268 | S O = prim__eqB16 x y
277269 | S (S O) = prim__eqB32 x y
278270 | S (S (S _)) = prim__eqB64 x y
279271
280−public
281−bitsEq : Bits n -> Bits n -> Bool
282−bitsEq (MkBits x) (MkBits y) = bitsEq' x y /= 0
283−
284−bitsGte' : machineTy n -> machineTy n -> Int
285−bitsGte' {n=n} x y with n
272+gte : machineTy n -> machineTy n -> Int
273+gte {n=n} x y with n
286274 | O = prim__gteB8 x y
287275 | S O = prim__gteB16 x y
288276 | S (S O) = prim__gteB32 x y
289277 | S (S (S _)) = prim__gteB64 x y
290278
291−public
292−bitsGte : Bits n -> Bits n -> Bool
293−bitsGte (MkBits x) (MkBits y) = bitsGte' x y /= 0
294−
295−bitsGt' : machineTy n -> machineTy n -> Int
296−bitsGt' {n=n} x y with n
279+gt : machineTy n -> machineTy n -> Int
280+gt {n=n} x y with n
297281 | O = prim__gtB8 x y
298282 | S O = prim__gtB16 x y
299283 | S (S O) = prim__gtB32 x y
300284 | S (S (S _)) = prim__gtB64 x y
301285
302−public
303−bitsGt : Bits n -> Bits n -> Bool
304−bitsGt (MkBits x) (MkBits y) = bitsGt' x y /= 0
305−
306286instance Eq (Bits n) where
307− (==) = bitsEq
287+ (MkBits x) == (MkBits y) = boolOp eq x y
308288
309289instance Ord (Bits n) where
310− (<) = bitsLt
311− (<=) = bitsLte
312− (>=) = bitsGte
313− (>) = bitsGt
314− compare x y = if x `bitsLt` y
315− then LT
316− else if x `bitsEq` y
317− then EQ
318− else GT
290+ (MkBits x) < (MkBits y) = boolOp lt x y
291+ (MkBits x) <= (MkBits y) = boolOp lte x y
292+ (MkBits x) >= (MkBits y) = boolOp gte x y
293+ (MkBits x) > (MkBits y) = boolOp gt x y
294+ compare (MkBits x) (MkBits y) =
295+ if (x `lt` y) /= 0
296+ then LT
297+ else if (x `eq` y) /= 0
298+ then EQ
299+ else GT
319300
320301complement' : machineTy n -> machineTy n
321302complement' {n=n} x with n
@@ -344,8 +325,8 @@ zext' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))
344325 | (S (S (S _)), S (S (S _))) = believe_me x
345326
346327public partial
347−zext : Bits n -> Bits (n+m)
348−zext (MkBits x) = MkBits (zext' x)
328+zeroExtend : Bits n -> Bits (n+m)
329+zeroExtend (MkBits x) = MkBits (zext' x)
349330
350331-- TODO: Prove
351332%assert_total
@@ -363,8 +344,8 @@ sext' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))
363344 | (S (S (S _)), S (S (S _))) = believe_me x
364345
365346public partial
366−sext : Bits n -> Bits (n+m)
367−sext (MkBits x) = MkBits (sext' x)
347+signExtend : Bits n -> Bits (n+m)
348+signExtend (MkBits x) = MkBits (sext' x)
368349
369350-- TODO: Prove
370351%assert_total
@@ -385,9 +366,20 @@ public partial
385366truncate : Bits (n+m) -> Bits n
386367truncate (MkBits x) = MkBits (trunc' x)
387368
369+bitAt : Fin n -> Bits n
370+bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)
371+
372+public
373+getBit : Fin n -> Bits n -> Bool
374+getBit n x = (x `and` (bitAt n)) /= intToBits 0
375+
376+public
377+setBit : Fin n -> Bits n -> Bits n
378+setBit n x = x `or` (bitAt n)
379+
388380public
389−bitSet : Fin n -> Bits n -> Bool
390−bitSet n x = bitsAnd (intToBits 1 `bitsShl` intToBits (cast (finToNat n))) x /= intToBits 0
381+unsetBit : Fin n -> Bits n -> Bits n
382+unsetBit n x = x `and` complement (bitAt n)
391383
392384public
393385bitsToStr : Bits n -> String
@@ -396,4 +388,4 @@ bitsToStr x = pack (helper last x)
396388 %assert_total
397389 helper : Fin (S n) -> Bits n -> List Char
398390 helper fO _ = []
399− helper (fS x) b = (if bitSet x b then '1' else '0') :: helper (weaken x) b
391+ helper (fS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b