@@ -0,0 +1,58 @@
1+module Bits
2+
3+%default total
4+
5+log2ceil : Nat -> Nat
6+log2ceil n = let x = log2 n in
7+ if x == log2 (n-1)
8+ then x+1
9+ else x
10+
11+Bits : Nat -> Type
12+Bits x with (log2ceil x)
13+ | (S (S (S (S (S (S _)))))) = Bits64
14+ | (S (S (S (S (S O))))) = Bits32
15+ | (S (S (S (S O)))) = Bits16
16+ | _ = Bits8
17+
18+intToBits : {n: Nat} -> Int -> Bits n
19+intToBits {n=n} x with (Bits n)
20+ | Bits8 = prim__intToB8 x
21+ | Bits16 = prim__intToB16 x
22+ | Bits32 = prim__intToB32 x
23+ | Bits64 = prim__intToB64 x
24+
25+bitsAdd : {n : Nat} -> Bits n -> Bits n -> Bits n
26+bitsAdd {n=m} x y with (Bits m)
27+ | Bits8 = prim__addB8 x y
28+ | Bits16 = prim__addB16 x y
29+ | Bits32 = prim__addB32 x y
30+ | Bits64 = prim__addB64 x y
31+
32+bitsSub : {n : Nat} -> Bits n -> Bits n -> Bits n
33+bitsSub {n=m} x y with (Bits m)
34+ | Bits8 = prim__subB8 x y
35+ | Bits16 = prim__subB16 x y
36+ | Bits32 = prim__subB32 x y
37+ | Bits64 = prim__subB64 x y
38+
39+bitsMul : {n : Nat} -> Bits n -> Bits n -> Bits n
40+bitsMul {n=m} x y with (Bits m)
41+ | Bits8 = prim__mulB8 x y
42+ | Bits16 = prim__mulB16 x y
43+ | Bits32 = prim__mulB32 x y
44+ | Bits64 = prim__mulB64 x y
45+
46+bitsSDiv : {n : Nat} -> Bits n -> Bits n -> Bits n
47+bitsSDiv {n=m} x y with (Bits m)
48+ | Bits8 = prim__sdivB8 x y
49+ | Bits16 = prim__sdivB16 x y
50+ | Bits32 = prim__sdivB32 x y
51+ | Bits64 = prim__sdivB64 x y
52+
53+bitsUDiv : {n : Nat} -> Bits n -> Bits n -> Bits n
54+bitsUDiv {n=m} x y with (Bits m)
55+ | Bits8 = prim__udivB8 x y
56+ | Bits16 = prim__udivB16 x y
57+ | Bits32 = prim__udivB32 x y
58+ | Bits64 = prim__udivB64 x y