@@ -8,103 +8,160 @@ log2ceil n = let x = log2 n in
88 then x+1
99 else x
1010
11−Bits : Nat -> Type
12−Bits x with (log2ceil x)
11+nextBits : Nat -> Type
12+nextBits x with (log2ceil x)
1313 | (S (S (S (S (S (S _)))))) = Bits64
1414 | (S (S (S (S (S O))))) = Bits32
1515 | (S (S (S (S O)))) = Bits16
1616 | _ = Bits8
1717
18−intToBits : {n: Nat} -> Int -> Bits n
19−intToBits {n=n} x with (Bits n)
18+abstract
19+data Bits : Nat -> Type where
20+ MkBits : {n : Nat} -> nextBits n -> Bits n
21+
22+intToBits' : {n: Nat} -> Int -> nextBits n
23+intToBits' {n=n} x with (nextBits n)
2024 | Bits8 = prim__intToB8 x
2125 | Bits16 = prim__intToB16 x
2226 | Bits32 = prim__intToB32 x
2327 | Bits64 = prim__intToB64 x
2428
25−instance Cast Int (Bits n) where
26− cast = intToBits
29+public
30+intToBits : {n : Nat} -> Int -> Bits n
31+intToBits n = MkBits (intToBits' n)
2732
28−bitsShl : {n: Nat} -> Bits n -> Bits n -> Bits n
29−bitsShl {n=n} x c with (Bits n)
33+bitsShl' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
34+bitsShl' {n=n} x c with (nextBits n)
3035 | Bits8 = prim__shlB8 x c
3136 | Bits16 = prim__shlB16 x c
3237 | Bits32 = prim__shlB32 x c
3338 | Bits64 = prim__shlB64 x c
3439
35−bitsLShr : {n: Nat} -> Bits n -> Bits n -> Bits n
36−bitsLShr {n=n} x c with (Bits n)
40+public
41+bitsShl : Bits n -> Bits n -> Bits n
42+bitsShl (MkBits x) (MkBits y) = MkBits (bitsShl' x y)
43+
44+bitsLShr' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
45+bitsLShr' {n=n} x c with (nextBits n)
3746 | Bits8 = prim__lshrB8 x c
3847 | Bits16 = prim__lshrB16 x c
3948 | Bits32 = prim__lshrB32 x c
4049 | Bits64 = prim__lshrB64 x c
4150
42−bitsAShr : {n: Nat} -> Bits n -> Bits n -> Bits n
43−bitsAShr {n=n} x c with (Bits n)
51+public
52+bitsLShr : Bits n -> Bits n -> Bits n
53+bitsLShr (MkBits x) (MkBits y) = MkBits (bitsLShr' x y)
54+
55+bitsAShr' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
56+bitsAShr' {n=n} x c with (nextBits n)
4457 | Bits8 = prim__ashrB8 x c
4558 | Bits16 = prim__ashrB16 x c
4659 | Bits32 = prim__ashrB32 x c
4760 | Bits64 = prim__ashrB64 x c
4861
49−bitsAnd : {n: Nat} -> Bits n -> Bits n -> Bits n
50−bitsAnd {n=n} x y with (Bits n)
62+public
63+bitsAShr : Bits n -> Bits n -> Bits n
64+bitsAShr (MkBits x) (MkBits y) = MkBits (bitsAShr' x y)
65+
66+bitsAnd' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
67+bitsAnd' {n=n} x y with (nextBits n)
5168 | Bits8 = prim__andB8 x y
5269 | Bits16 = prim__andB16 x y
5370 | Bits32 = prim__andB32 x y
5471 | Bits64 = prim__andB64 x y
5572
56−bitsOr : {n: Nat} -> Bits n -> Bits n -> Bits n
57−bitsOr {n=n} x y with (Bits n)
73+public
74+bitsAnd : Bits n -> Bits n -> Bits n
75+bitsAnd (MkBits x) (MkBits y) = MkBits (bitsAnd' x y)
76+
77+bitsOr' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
78+bitsOr' {n=n} x y with (nextBits n)
5879 | Bits8 = prim__orB8 x y
5980 | Bits16 = prim__orB16 x y
6081 | Bits32 = prim__orB32 x y
6182 | Bits64 = prim__orB64 x y
6283
63−bitsXOr : {n: Nat} -> Bits n -> Bits n -> Bits n
64−bitsXOr {n=n} x y with (Bits n)
84+public
85+bitsOr : Bits n -> Bits n -> Bits n
86+bitsOr (MkBits x) (MkBits y) = MkBits (bitsOr' x y)
87+
88+bitsXOr' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
89+bitsXOr' {n=n} x y with (nextBits n)
6590 | Bits8 = prim__xorB8 x y
6691 | Bits16 = prim__xorB16 x y
6792 | Bits32 = prim__xorB32 x y
6893 | Bits64 = prim__xorB64 x y
6994
70−bitsAdd : {n : Nat} -> Bits n -> Bits n -> Bits n
71−bitsAdd {n=n} x y with (Bits n)
72− | Bits8 = prim__addB8 x y
73− | Bits16 = prim__addB16 x y
74− | Bits32 = prim__addB32 x y
75− | Bits64 = prim__addB64 x y
76−
77−bitsSub : {n : Nat} -> Bits n -> Bits n -> Bits n
78−bitsSub {n=n} x y with (Bits n)
95+public
96+bitsXOr : Bits n -> Bits n -> Bits n
97+bitsXOr (MkBits x) (MkBits y) = MkBits (bitsXOr' x y)
98+
99+bitsAdd' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
100+bitsAdd' {n=n} x y with (nextBits n)
101+ | Bits8 = let pad = prim__intToB8 (the Int (cast (8-n))) in
102+ prim__lshrB8 (prim__addB8 (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
103+ | Bits16 = let pad = prim__intToB16 (the Int (cast (16-n))) in
104+ prim__lshrB16 (prim__addB16 (prim__shlB16 x pad) (prim__shlB16 y pad)) pad
105+ | Bits32 = let pad = prim__intToB32 (the Int (cast (32-n))) in
106+ prim__lshrB32 (prim__addB32 (prim__shlB32 x pad) (prim__shlB32 y pad)) pad
107+ | Bits64 = let pad = prim__intToB64 (the Int (cast (64-n))) in
108+ prim__lshrB64 (prim__addB64 (prim__shlB64 x pad) (prim__shlB64 y pad)) pad
109+
110+public
111+bitsAdd : Bits n -> Bits n -> Bits n
112+bitsAdd (MkBits x) (MkBits y) = MkBits (bitsAdd' x y)
113+
114+bitsSub' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
115+bitsSub' {n=n} x y with (nextBits n)
79116 | Bits8 = prim__subB8 x y
80117 | Bits16 = prim__subB16 x y
81118 | Bits32 = prim__subB32 x y
82119 | Bits64 = prim__subB64 x y
83120
84−bitsMul : {n : Nat} -> Bits n -> Bits n -> Bits n
85−bitsMul {n=n} x y with (Bits n)
121+public
122+bitsSub : Bits n -> Bits n -> Bits n
123+bitsSub (MkBits x) (MkBits y) = MkBits (bitsSub' x y)
124+
125+bitsMul' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
126+bitsMul' {n=n} x y with (nextBits n)
86127 | Bits8 = prim__mulB8 x y
87128 | Bits16 = prim__mulB16 x y
88129 | Bits32 = prim__mulB32 x y
89130 | Bits64 = prim__mulB64 x y
90131
91−bitsSDiv : {n : Nat} -> Bits n -> Bits n -> Bits n
92−bitsSDiv {n=n} x y with (Bits n)
132+public
133+bitsMul : Bits n -> Bits n -> Bits n
134+bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)
135+
136+bitsSDiv' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
137+bitsSDiv' {n=n} x y with (nextBits n)
93138 | Bits8 = prim__sdivB8 x y
94139 | Bits16 = prim__sdivB16 x y
95140 | Bits32 = prim__sdivB32 x y
96141 | Bits64 = prim__sdivB64 x y
97142
98−bitsUDiv : {n : Nat} -> Bits n -> Bits n -> Bits n
99−bitsUDiv {n=n} x y with (Bits n)
143+public
144+bitsSDiv : Bits n -> Bits n -> Bits n
145+bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)
146+
147+bitsUDiv' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
148+bitsUDiv' {n=n} x y with (nextBits n)
100149 | Bits8 = prim__udivB8 x y
101150 | Bits16 = prim__udivB16 x y
102151 | Bits32 = prim__udivB32 x y
103152 | Bits64 = prim__udivB64 x y
104153
105−bitsToStr : {n : Nat} -> Bits n -> String
106−bitsToStr {n=n} x with (Bits n)
154+public
155+bitsUDiv : Bits n -> Bits n -> Bits n
156+bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)
157+
158+bitsToStr' : {n : Nat} -> nextBits n -> String
159+bitsToStr' {n=n} x with (nextBits n)
107160 | Bits8 = prim__b8ToStr x
108161 | Bits16 = prim__b16ToStr x
109162 | Bits32 = prim__b32ToStr x
110163 | Bits64 = prim__b64ToStr x
164+
165+public
166+bitsToStr : Bits n -> String
167+bitsToStr (MkBits x) = bitsToStr' x