@@ -15,6 +15,7 @@ nextBits x with (log2ceil x)
1515 | (S (S (S (S O)))) = Bits16
1616 | _ = Bits8
1717
18+public
1819data Bits : Nat -> Type where
1920 MkBits : {n : Nat} -> nextBits n -> Bits n
2021
@@ -56,6 +57,7 @@ intToBits' {n=n} x with (nextBits n)
5657 | Bits64 = let pad = (prim__intToB64 (cast (64-n))) in
5758 prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad
5859
60+public
5961intToBits : {n : Nat} -> Int -> Bits n
6062intToBits n = MkBits (intToBits' n)
6163
@@ -69,6 +71,7 @@ bitsShl' {n=n} x c with (nextBits n)
6971 | Bits32 = pad32 n prim__shlB32 x c
7072 | Bits64 = pad64 n prim__shlB64 x c
7173
74+public
7275bitsShl : Bits n -> Bits n -> Bits n
7376bitsShl (MkBits x) (MkBits y) = MkBits (bitsShl' x y)
7477
@@ -79,6 +82,7 @@ bitsLShr' {n=n} x c with (nextBits n)
7982 | Bits32 = prim__lshrB32 x c
8083 | Bits64 = prim__lshrB64 x c
8184
85+public
8286bitsLShr : Bits n -> Bits n -> Bits n
8387bitsLShr (MkBits x) (MkBits y) = MkBits (bitsLShr' x y)
8488
@@ -89,6 +93,7 @@ bitsAShr' {n=n} x c with (nextBits n)
8993 | Bits32 = prim__ashrB32 x c
9094 | Bits64 = prim__ashrB64 x c
9195
96+public
9297bitsAShr : Bits n -> Bits n -> Bits n
9398bitsAShr (MkBits x) (MkBits y) = MkBits (bitsAShr' x y)
9499
@@ -99,6 +104,7 @@ bitsAnd' {n=n} x y with (nextBits n)
99104 | Bits32 = prim__andB32 x y
100105 | Bits64 = prim__andB64 x y
101106
107+public
102108bitsAnd : Bits n -> Bits n -> Bits n
103109bitsAnd (MkBits x) (MkBits y) = MkBits (bitsAnd' x y)
104110
@@ -109,6 +115,7 @@ bitsOr' {n=n} x y with (nextBits n)
109115 | Bits32 = prim__orB32 x y
110116 | Bits64 = prim__orB64 x y
111117
118+public
112119bitsOr : Bits n -> Bits n -> Bits n
113120bitsOr (MkBits x) (MkBits y) = MkBits (bitsOr' x y)
114121
@@ -119,6 +126,7 @@ bitsXOr' {n=n} x y with (nextBits n)
119126 | Bits32 = prim__xorB32 x y
120127 | Bits64 = prim__xorB64 x y
121128
129+public
122130bitsXOr : Bits n -> Bits n -> Bits n
123131bitsXOr (MkBits x) (MkBits y) = MkBits (bitsXOr' x y)
124132
@@ -129,6 +137,7 @@ bitsAdd' {n=n} x y with (nextBits n)
129137 | Bits32 = pad32 n prim__addB32 x y
130138 | Bits64 = pad64 n prim__addB64 x y
131139
140+public
132141bitsAdd : Bits n -> Bits n -> Bits n
133142bitsAdd (MkBits x) (MkBits y) = MkBits (bitsAdd' x y)
134143
@@ -139,6 +148,7 @@ bitsSub' {n=n} x y with (nextBits n)
139148 | Bits32 = pad32 n prim__subB32 x y
140149 | Bits64 = pad64 n prim__subB64 x y
141150
151+public
142152bitsSub : Bits n -> Bits n -> Bits n
143153bitsSub (MkBits x) (MkBits y) = MkBits (bitsSub' x y)
144154
@@ -149,6 +159,7 @@ bitsMul' {n=n} x y with (nextBits n)
149159 | Bits32 = pad32 n prim__mulB32 x y
150160 | Bits64 = pad64 n prim__mulB64 x y
151161
162+public
152163bitsMul : Bits n -> Bits n -> Bits n
153164bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)
154165
@@ -159,6 +170,7 @@ bitsSDiv' {n=n} x y with (nextBits n)
159170 | Bits32 = prim__sdivB32 x y
160171 | Bits64 = prim__sdivB64 x y
161172
173+public
162174bitsSDiv : Bits n -> Bits n -> Bits n
163175bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)
164176
@@ -169,6 +181,7 @@ bitsUDiv' {n=n} x y with (nextBits n)
169181 | Bits32 = prim__udivB32 x y
170182 | Bits64 = prim__udivB64 x y
171183
184+public
172185bitsUDiv : Bits n -> Bits n -> Bits n
173186bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)
174187
@@ -179,6 +192,7 @@ bitsToStr' {n=n} x with (nextBits n)
179192 | Bits32 = prim__b32ToStr x
180193 | Bits64 = prim__b64ToStr x
181194
195+public
182196bitsToStr : Bits n -> String
183197bitsToStr (MkBits x) = bitsToStr' x
184198
@@ -190,6 +204,7 @@ bitsLt' {n=n} x y with (nextBits n)
190204 | Bits32 = prim__ltB32 x y
191205 | Bits64 = prim__ltB64 x y
192206
207+public
193208bitsLt : (x : Bits n) -> (y : Bits n) -> Bool
194209bitsLt (MkBits x) (MkBits y) =
195210 case (bitsLt' x y) of
@@ -203,6 +218,7 @@ bitsLte' {n=n} x y with (nextBits n)
203218 | Bits32 = prim__lteB32 x y
204219 | Bits64 = prim__lteB64 x y
205220
221+public
206222bitsLte : (x : Bits n) -> (y : Bits n) -> Bool
207223bitsLte (MkBits x) (MkBits y) =
208224 case (bitsLte' x y) of
@@ -216,6 +232,7 @@ bitsEq' {n=n} x y with (nextBits n)
216232 | Bits32 = prim__eqB32 x y
217233 | Bits64 = prim__eqB64 x y
218234
235+public
219236bitsEq : (x : Bits n) -> (y : Bits n) -> Bool
220237bitsEq (MkBits x) (MkBits y) =
221238 case (bitsEq' x y) of
@@ -229,6 +246,7 @@ bitsGte' {n=n} x y with (nextBits n)
229246 | Bits32 = prim__gteB32 x y
230247 | Bits64 = prim__gteB64 x y
231248
249+public
232250bitsGte : (x : Bits n) -> (y : Bits n) -> Bool
233251bitsGte (MkBits x) (MkBits y) =
234252 case (bitsGte' x y) of
@@ -242,6 +260,7 @@ bitsGt' {n=n} x y with (nextBits n)
242260 | Bits32 = prim__gtB32 x y
243261 | Bits64 = prim__gtB64 x y
244262
263+public
245264bitsGt : (x : Bits n) -> (y : Bits n) -> Bool
246265bitsGt (MkBits x) (MkBits y) =
247266 case (bitsGt' x y) of