git.iko.soy/Idris-dev
on fa29447 help sign in
Idris-dev/lib/Data/Bits.idr
442 lines 16 kB history raw
1module Data.Bits
3%default total
5divCeil : Nat -> Nat -> Nat
6divCeil x y = case x `mod` y of
7 O => x `div` y
8 S _ => S (x `div` y)
10nextPow2 : Nat -> Nat
11nextPow2 O = O
12nextPow2 x = if x == (2 `power` l2x)
13 then l2x
14 else S l2x
15 where
16 l2x = log2 x
18nextBytes : Nat -> Nat
19nextBytes bits = (nextPow2 (bits `divCeil` 8))
21machineTy : Nat -> Type
22machineTy O = Bits8
23machineTy (S O) = Bits16
24machineTy (S (S O)) = Bits32
25machineTy (S (S (S _))) = Bits64
27bitsUsed : Nat -> Nat
28bitsUsed n = 8 * (2 `power` n)
30%assert_total
31natToBits' : machineTy n -> Nat -> machineTy n
32natToBits' a O = a
33natToBits' {n=n} a x with n
34 -- it seems I have to manually recover the value of n here, instead of being able to reference it
35 natToBits' a (S x') | O = natToBits' {n=0} (prim__addB8 a (prim__truncInt_B8 1)) x'
36 natToBits' a (S x') | S O = natToBits' {n=1} (prim__addB16 a (prim__truncInt_B16 1)) x'
37 natToBits' a (S x') | S (S O) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x'
38 natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'
40natToBits : Nat -> machineTy n
41natToBits {n=n} x with n
42 | O = natToBits' {n=0} (prim__truncInt_B8 0) x
43 | S O = natToBits' {n=1} (prim__truncInt_B16 0) x
44 | S (S O) = natToBits' {n=2} (prim__truncInt_B32 0) x
45 | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x
47getPad : Nat -> machineTy n
48getPad n = natToBits ((bitsUsed (nextBytes n)) - n)
50public
51data Bits : Nat -> Type where
52 MkBits : machineTy (nextBytes n) -> Bits n
54pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
55pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
56 where
57 pad = getPad {n=0} n
59pad16 : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
60pad16 n f x y = prim__lshrB16 (f (prim__shlB16 x pad) (prim__shlB16 y pad)) pad
61 where
62 pad = getPad {n=1} n
64pad32 : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
65pad32 n f x y = prim__lshrB32 (f (prim__shlB32 x pad) (prim__shlB32 y pad)) pad
66 where
67 pad = getPad {n=2} n
69pad64 : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
70pad64 n f x y = prim__lshrB64 (f (prim__shlB64 x pad) (prim__shlB64 y pad)) pad
71 where
72 pad = getPad {n=3} n
74-- These versions only pad the first operand
75pad8' : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
76pad8' n f x y = prim__lshrB8 (f (prim__shlB8 x pad) y) pad
77 where
78 pad = getPad {n=0} n
80pad16' : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
81pad16' n f x y = prim__lshrB16 (f (prim__shlB16 x pad) y) pad
82 where
83 pad = getPad {n=1} n
85pad32' : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
86pad32' n f x y = prim__lshrB32 (f (prim__shlB32 x pad) y) pad
87 where
88 pad = getPad {n=2} n
90pad64' : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
91pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad
92 where
93 pad = getPad {n=3} n
95shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
96shiftLeft' {n=n} x c with (nextBytes n)
97 | O = pad8' n prim__shlB8 x c
98 | S O = pad16' n prim__shlB16 x c
99 | S (S O) = pad32' n prim__shlB32 x c
100 | S (S (S _)) = pad64' n prim__shlB64 x c
102public
103shiftLeft : Bits n -> Bits n -> Bits n
104shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
106shiftRightLogical' : machineTy n -> machineTy n -> machineTy n
107shiftRightLogical' {n=n} x c with n
108 | O = prim__lshrB8 x c
109 | S O = prim__lshrB16 x c
110 | S (S O) = prim__lshrB32 x c
111 | S (S (S _)) = prim__lshrB64 x c
113public
114shiftRightLogical : Bits n -> Bits n -> Bits n
115shiftRightLogical {n} (MkBits x) (MkBits y)
116 = MkBits {n} (shiftRightLogical' {n=nextBytes n} x y)
118shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
119shiftRightArithmetic' {n=n} x c with (nextBytes n)
120 | O = pad8' n prim__ashrB8 x c
121 | S O = pad16' n prim__ashrB16 x c
122 | S (S O) = pad32' n prim__ashrB32 x c
123 | S (S (S _)) = pad64' n prim__ashrB64 x c
125public
126shiftRightArithmetic : Bits n -> Bits n -> Bits n
127shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
129and' : machineTy n -> machineTy n -> machineTy n
130and' {n=n} x y with n
131 | O = prim__andB8 x y
132 | S O = prim__andB16 x y
133 | S (S O) = prim__andB32 x y
134 | S (S (S _)) = prim__andB64 x y
136public
137and : Bits n -> Bits n -> Bits n
138and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)
140or' : machineTy n -> machineTy n -> machineTy n
141or' {n=n} x y with n
142 | O = prim__orB8 x y
143 | S O = prim__orB16 x y
144 | S (S O) = prim__orB32 x y
145 | S (S (S _)) = prim__orB64 x y
147public
148or : Bits n -> Bits n -> Bits n
149or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)
151xor' : machineTy n -> machineTy n -> machineTy n
152xor' {n=n} x y with n
153 | O = prim__xorB8 x y
154 | S O = prim__xorB16 x y
155 | S (S O) = prim__xorB32 x y
156 | S (S (S _)) = prim__xorB64 x y
158public
159xor : Bits n -> Bits n -> Bits n
160xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)
162plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
163plus' {n=n} x y with (nextBytes n)
164 | O = pad8 n prim__addB8 x y
165 | S O = pad16 n prim__addB16 x y
166 | S (S O) = pad32 n prim__addB32 x y
167 | S (S (S _)) = pad64 n prim__addB64 x y
169public
170plus : Bits n -> Bits n -> Bits n
171plus (MkBits x) (MkBits y) = MkBits (plus' x y)
173minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
174minus' {n=n} x y with (nextBytes n)
175 | O = pad8 n prim__subB8 x y
176 | S O = pad16 n prim__subB16 x y
177 | S (S O) = pad32 n prim__subB32 x y
178 | S (S (S _)) = pad64 n prim__subB64 x y
180public
181minus : Bits n -> Bits n -> Bits n
182minus (MkBits x) (MkBits y) = MkBits (minus' x y)
184times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
185times' {n=n} x y with (nextBytes n)
186 | O = pad8 n prim__mulB8 x y
187 | S O = pad16 n prim__mulB16 x y
188 | S (S O) = pad32 n prim__mulB32 x y
189 | S (S (S _)) = pad64 n prim__mulB64 x y
191public
192times : Bits n -> Bits n -> Bits n
193times (MkBits x) (MkBits y) = MkBits (times' x y)
195partial
196sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
197sdiv' {n=n} x y with (nextBytes n)
198 | O = prim__sdivB8 x y
199 | S O = prim__sdivB16 x y
200 | S (S O) = prim__sdivB32 x y
201 | S (S (S _)) = prim__sdivB64 x y
203public partial
204sdiv : Bits n -> Bits n -> Bits n
205sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)
207partial
208udiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
209udiv' {n=n} x y with (nextBytes n)
210 | O = prim__udivB8 x y
211 | S O = prim__udivB16 x y
212 | S (S O) = prim__udivB32 x y
213 | S (S (S _)) = prim__udivB64 x y
215public partial
216udiv : Bits n -> Bits n -> Bits n
217udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)
219partial
220srem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
221srem' {n=n} x y with (nextBytes n)
222 | O = prim__sremB8 x y
223 | S O = prim__sremB16 x y
224 | S (S O) = prim__sremB32 x y
225 | S (S (S _)) = prim__sremB64 x y
227public partial
228srem : Bits n -> Bits n -> Bits n
229srem (MkBits x) (MkBits y) = MkBits (srem' x y)
231partial
232urem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
233urem' {n=n} x y with (nextBytes n)
234 | O = prim__uremB8 x y
235 | S O = prim__uremB16 x y
236 | S (S O) = prim__uremB32 x y
237 | S (S (S _)) = prim__uremB64 x y
239public partial
240urem : Bits n -> Bits n -> Bits n
241urem (MkBits x) (MkBits y) = MkBits (urem' x y)
243-- TODO: Proofy comparisons via postulates
244lt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
245lt {n=n} x y with (nextBytes n)
246 | O = prim__ltB8 x y
247 | S O = prim__ltB16 x y
248 | S (S O) = prim__ltB32 x y
249 | S (S (S _)) = prim__ltB64 x y
251lte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
252lte {n=n} x y with (nextBytes n)
253 | O = prim__lteB8 x y
254 | S O = prim__lteB16 x y
255 | S (S O) = prim__lteB32 x y
256 | S (S (S _)) = prim__lteB64 x y
258eq : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
259eq {n=n} x y with (nextBytes n)
260 | O = prim__eqB8 x y
261 | S O = prim__eqB16 x y
262 | S (S O) = prim__eqB32 x y
263 | S (S (S _)) = prim__eqB64 x y
265gte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
266gte {n=n} x y with (nextBytes n)
267 | O = prim__gteB8 x y
268 | S O = prim__gteB16 x y
269 | S (S O) = prim__gteB32 x y
270 | S (S (S _)) = prim__gteB64 x y
272gt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
273gt {n=n} x y with (nextBytes n)
274 | O = prim__gtB8 x y
275 | S O = prim__gtB16 x y
276 | S (S O) = prim__gtB32 x y
277 | S (S (S _)) = prim__gtB64 x y
279instance Eq (Bits n) where
280 (MkBits x) == (MkBits y) = boolOp eq x y
282instance Ord (Bits n) where
283 (MkBits x) < (MkBits y) = boolOp lt x y
284 (MkBits x) <= (MkBits y) = boolOp lte x y
285 (MkBits x) >= (MkBits y) = boolOp gte x y
286 (MkBits x) > (MkBits y) = boolOp gt x y
287 compare (MkBits x) (MkBits y) =
288 if boolOp lt x y
289 then LT
290 else if boolOp eq x y
291 then EQ
292 else GT
294complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)
295complement' {n=n} x with (nextBytes n)
296 | O = let pad = getPad {n=0} n in
297 prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad
298 | S O = let pad = getPad {n=1} n in
299 prim__complB16 (x `prim__shlB16` pad) `prim__lshrB16` pad
300 | S (S O) = let pad = getPad {n=2} n in
301 prim__complB32 (x `prim__shlB32` pad) `prim__lshrB32` pad
302 | S (S (S _)) = let pad = getPad {n=3} n in
303 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
305public
306complement : Bits n -> Bits n
307complement (MkBits x) = MkBits (complement' x)
309-- TODO: Prove
310zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
311zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
312 | (O, O) = believe_me x
313 | (O, S O) = believe_me (prim__zextB8_B16 (believe_me x))
314 | (O, S (S O)) = believe_me (prim__zextB8_B32 (believe_me x))
315 | (O, S (S (S _))) = believe_me (prim__zextB8_B64 (believe_me x))
316 | (S O, S O) = believe_me x
317 | (S O, S (S O)) = believe_me (prim__zextB16_B32 (believe_me x))
318 | (S O, S (S (S _))) = believe_me (prim__zextB16_B64 (believe_me x))
319 | (S (S O), S (S O)) = believe_me x
320 | (S (S O), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))
321 | (S (S (S _)), S (S (S _))) = believe_me x
323public
324zeroExtend : Bits n -> Bits (n+m)
325zeroExtend (MkBits x) = MkBits (zext' x)
327%assert_total
328intToBits' : Int -> machineTy (nextBytes n)
329intToBits' {n=n} x with (nextBytes n)
330 | O = let pad = getPad {n=0} n in
331 prim__lshrB8 (prim__shlB8 (prim__truncInt_B8 x) pad) pad
332 | S O = let pad = getPad {n=1} n in
333 prim__lshrB16 (prim__shlB16 (prim__truncInt_B16 x) pad) pad
334 | S (S O) = let pad = getPad {n=2} n in
335 prim__lshrB32 (prim__shlB32 (prim__truncInt_B32 x) pad) pad
336 | S (S (S _)) = let pad = getPad {n=3} n in
337 prim__lshrB64 (prim__shlB64 (prim__truncInt_B64 x) pad) pad
339public
340intToBits : Int -> Bits n
341intToBits n = MkBits (intToBits' n)
343instance Cast Int (Bits n) where
344 cast = intToBits
346bitsToInt' : machineTy (nextBytes n) -> Int
347bitsToInt' {n=n} x with (nextBytes n)
348 | O = prim__zextB8_Int x
349 | S O = prim__zextB16_Int x
350 | S (S O) = prim__zextB32_Int x
351 | S (S (S _)) = prim__truncB64_Int x
353public
354bitsToInt : Bits n -> Int
355bitsToInt (MkBits x) = bitsToInt' x
357-- Zero out the high bits of a truncated bitstring
358--zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)
359--zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
361--instance Cast Nat (Bits n) where
362-- cast x = MkBits (zeroUnused (natToBits n))
364-- TODO: Prove
365sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
366sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
367 | (O, O) = let pad = getPad {n=0} n in
368 believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)
369 | (O, S O) = let pad = getPad {n=0} n in
370 believe_me (prim__ashrB16 (prim__sextB8_B16 (prim__shlB8 (believe_me x) pad))
371 (prim__zextB8_B16 pad))
372 | (O, S (S O)) = let pad = getPad {n=0} n in
373 believe_me (prim__ashrB32 (prim__sextB8_B32 (prim__shlB8 (believe_me x) pad))
374 (prim__zextB8_B32 pad))
375 | (O, S (S (S _))) = let pad = getPad {n=0} n in
376 believe_me (prim__ashrB64 (prim__sextB8_B64 (prim__shlB8 (believe_me x) pad))
377 (prim__zextB8_B64 pad))
378 | (S O, S O) = let pad = getPad {n=1} n in
379 believe_me (prim__ashrB16 (prim__shlB16 (believe_me x) pad) pad)
380 | (S O, S (S O)) = let pad = getPad {n=1} n in
381 believe_me (prim__ashrB32 (prim__sextB16_B32 (prim__shlB16 (believe_me x) pad))
382 (prim__zextB16_B32 pad))
383 | (S O, S (S (S _))) = let pad = getPad {n=1} n in
384 believe_me (prim__ashrB64 (prim__sextB16_B64 (prim__shlB16 (believe_me x) pad))
385 (prim__zextB16_B64 pad))
386 | (S (S O), S (S O)) = let pad = getPad {n=2} n in
387 believe_me (prim__ashrB32 (prim__shlB32 (believe_me x) pad) pad)
388 | (S (S O), S (S (S _))) = let pad = getPad {n=2} n in
389 believe_me (prim__ashrB64 (prim__sextB32_B64 (prim__shlB32 (believe_me x) pad))
390 (prim__zextB32_B64 pad))
391 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in
392 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)
394--public
395--signExtend : Bits n -> Bits (n+m)
396--signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))
398-- TODO: Prove
399trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)
400trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
401 | (O, O) = believe_me x
402 | (O, S O) = believe_me (prim__truncB16_B8 (believe_me x))
403 | (O, S (S O)) = believe_me (prim__truncB32_B8 (believe_me x))
404 | (O, S (S (S _))) = believe_me (prim__truncB64_B8 (believe_me x))
405 | (S O, S O) = believe_me x
406 | (S O, S (S O)) = believe_me (prim__truncB32_B16 (believe_me x))
407 | (S O, S (S (S _))) = believe_me (prim__truncB64_B16 (believe_me x))
408 | (S (S O), S (S O)) = believe_me x
409 | (S (S O), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))
410 | (S (S (S _)), S (S (S _))) = believe_me x
412--public
413--truncate : Bits (n+m) -> Bits n
414--truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
416public
417bitAt : Fin n -> Bits n
418bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)
420public
421getBit : Fin n -> Bits n -> Bool
422getBit n x = (x `and` (bitAt n)) /= intToBits 0
424public
425setBit : Fin n -> Bits n -> Bits n
426setBit n x = x `or` (bitAt n)
428public
429unsetBit : Fin n -> Bits n -> Bits n
430unsetBit n x = x `and` complement (bitAt n)
432bitsToStr : Bits n -> String
433bitsToStr x = pack (helper last x)
434 where
435 %assert_total
436 helper : Fin (S n) -> Bits n -> List Char
437 helper fO _ = []
438 helper (fS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b
440instance Show (Bits n) where
441 show = bitsToStr