0 | module Data.Bits

  2 | import public Data.Fin

  3 | import Data.Vect

  5 | %default total

  7 | export infixl 8 `shiftL`, `shiftR`

  8 | export infixl 7 .&.

  9 | export infixl 6 `xor`

 10 | export infixl 5 .|.

 17 | public export

 18 | interface Bits a where

 19 |   0 Index : Type

 21 |   ||| Bitwise "and"

 22 |   (.&.) : a -> a -> a

 24 |   ||| Bitwise "or"

 25 |   (.|.) : a -> a -> a

 27 |   ||| Bitwise "xor".

 28 |   xor : a -> a -> a

 30 |   ||| Shift the argument left by the specified number of bits.

 31 |   shiftL : a -> Index -> a

 33 |   ||| Shift the argument right by the specified number of bits.

 34 |   shiftR : a -> Index -> a

 36 |   ||| Sets the `i`-th bit.

 37 |   bit : (i : Index) -> a

 39 |   ||| The value with all bits unset.

 40 |   zeroBits : a

 42 |   ||| Returns the bitwise complement of a value.

 43 |   complement : a -> a

 44 |   complement = xor oneBits

 46 |   ||| The value with all bits set..

 47 |   oneBits : a

 48 |   oneBits = complement zeroBits

 50 |   ||| `complementBit x i` is the same as `xor x (bit i)`.

 51 |   complementBit : (x : a) -> (i : Index) -> a

 52 |   complementBit x i = x `xor` bit i

 54 |   ||| `clearBit x i` is the same as `x .&. complement (bit i)`

 55 |   clearBit : (x : a) -> (i : Index) -> a

 56 |   clearBit x i = x `xor` (bit i .&. x)

 58 |   ||| Tests, whether the i-th bit is set in the given value.

 59 |   testBit : a -> Index -> Bool

 61 |   ||| Sets the i-th bit of a value.

 62 |   setBit : a -> (i : Index) -> a

 63 |   setBit x i = x .|. bit i

 65 | public export %inline

 66 | Bits Bits8 where

 67 |   Index       = Fin 8

 68 |   (.&.)       = prim__and_Bits8

 69 |   (.|.)       = prim__or_Bits8

 70 |   xor         = prim__xor_Bits8

 71 |   bit         = (1 `shiftL`)

 72 |   zeroBits    = 0

 73 |   testBit x i = (x .&. bit i) /= 0

 74 |   shiftR x    = prim__shr_Bits8 x . cast . finToNat

 75 |   shiftL x    = prim__shl_Bits8 x . cast . finToNat

 76 |   oneBits     = 0xff

 78 | public export %inline

 79 | Bits Bits16 where

 80 |   Index       = Fin 16

 81 |   (.&.)       = prim__and_Bits16

 82 |   (.|.)       = prim__or_Bits16

 83 |   xor         = prim__xor_Bits16

 84 |   bit         = (1 `shiftL`)

 85 |   zeroBits    = 0

 86 |   testBit x i = (x .&. bit i) /= 0

 87 |   shiftR x    = prim__shr_Bits16 x . cast . finToNat

 88 |   shiftL x    = prim__shl_Bits16 x . cast . finToNat

 89 |   oneBits     = 0xffff

 91 | public export %inline

 92 | Bits Bits32 where

 93 |   Index       = Fin 32

 94 |   (.&.)       = prim__and_Bits32

 95 |   (.|.)       = prim__or_Bits32

 96 |   xor         = prim__xor_Bits32

 97 |   bit         = (1 `shiftL`)

 98 |   zeroBits    = 0

 99 |   testBit x i = (x .&. bit i) /= 0

100 |   shiftR x    = prim__shr_Bits32 x . cast . finToNat

101 |   shiftL x    = prim__shl_Bits32 x . cast . finToNat

102 |   oneBits     = 0xffffffff

104 | public export %inline

105 | Bits Bits64 where

106 |   Index       = Fin 64

107 |   (.&.)       = prim__and_Bits64

108 |   (.|.)       = prim__or_Bits64

109 |   xor         = prim__xor_Bits64

110 |   bit         = (1 `shiftL`)

111 |   zeroBits    = 0

112 |   testBit x i = (x .&. bit i) /= 0

113 |   shiftR x    = prim__shr_Bits64 x . cast . finToNat

114 |   shiftL x    = prim__shl_Bits64 x . cast . finToNat

115 |   oneBits     = 0xffffffffffffffff

117 | public export %inline

118 | Bits Int where

119 |   Index       = Fin 64

120 |   (.&.)       = prim__and_Int

121 |   (.|.)       = prim__or_Int

122 |   xor         = prim__xor_Int

123 |   bit         = (1 `shiftL`)

124 |   zeroBits    = 0

125 |   testBit x i = (x .&. bit i) /= 0

126 |   shiftR x    = prim__shr_Int x . cast . finToNat

127 |   shiftL x    = prim__shl_Int x . cast . finToNat

128 |   oneBits     = (-1)

130 | public export %inline

131 | Bits Int8 where

132 |   Index       = Fin 8

133 |   (.&.)       = prim__and_Int8

134 |   (.|.)       = prim__or_Int8

135 |   xor         = prim__xor_Int8

136 |   bit         = (1 `shiftL`)

137 |   zeroBits    = 0

138 |   testBit x i = (x .&. bit i) /= 0

139 |   shiftR x    = prim__shr_Int8 x . cast . finToNat

140 |   shiftL x    = prim__shl_Int8 x . cast . finToNat

141 |   oneBits     = (-1)

143 | public export %inline

144 | Bits Int16 where

145 |   Index       = Fin 16

146 |   (.&.)       = prim__and_Int16

147 |   (.|.)       = prim__or_Int16

148 |   xor         = prim__xor_Int16

149 |   bit         = (1 `shiftL`)

150 |   zeroBits    = 0

151 |   testBit x i = (x .&. bit i) /= 0

152 |   shiftR x    = prim__shr_Int16 x . cast . finToNat

153 |   shiftL x    = prim__shl_Int16 x . cast . finToNat

154 |   oneBits     = (-1)

156 | public export %inline

157 | Bits Int32 where

158 |   Index       = Fin 32

159 |   (.&.)       = prim__and_Int32

160 |   (.|.)       = prim__or_Int32

161 |   xor         = prim__xor_Int32

162 |   bit         = (1 `shiftL`)

163 |   zeroBits    = 0

164 |   testBit x i = (x .&. bit i) /= 0

165 |   shiftR x    = prim__shr_Int32 x . cast . finToNat

166 |   shiftL x    = prim__shl_Int32 x . cast . finToNat

167 |   oneBits     = (-1)

169 | public export %inline

170 | Bits Int64 where

171 |   Index       = Fin 64

172 |   (.&.)       = prim__and_Int64

173 |   (.|.)       = prim__or_Int64

174 |   xor         = prim__xor_Int64

175 |   bit         = (1 `shiftL`)

176 |   zeroBits    = 0

177 |   testBit x i = (x .&. bit i) /= 0

178 |   shiftR x    = prim__shr_Int64 x . cast . finToNat

179 |   shiftL x    = prim__shl_Int64 x . cast . finToNat

180 |   oneBits     = (-1)

182 | public export %inline

183 | Bits Integer where

184 |   Index       = Nat

185 |   (.&.)       = prim__and_Integer

186 |   (.|.)       = prim__or_Integer

187 |   xor         = prim__xor_Integer

188 |   bit         = (1 `shiftL`)

189 |   zeroBits    = 0

190 |   testBit x i = (x .&. bit i) /= 0

191 |   shiftR x    = prim__shr_Integer x . natToInteger

192 |   shiftL x    = prim__shl_Integer x . natToInteger

193 |   oneBits     = (-1)

199 | public export

200 | interface Bits a => FiniteBits a where

201 |   ||| Return the number of bits in values of type `t`.

202 |   bitSize : Nat

204 |   ||| Properly correlates `bitSize` and `Index`.

205 |   bitsToIndex : Fin bitSize -> Index {a}

207 |   ||| Return the number of set bits in the argument.  This number is

209 |   popCount : a -> Nat

211 |   ||| Rotate the argument right by the specified number of bits.

212 |   rotR : a -> Fin bitSize -> a

213 |   rotR x i =

214 |     (x `shiftR` (bitsToIndex i)) .|. (x `shiftL` (bitsToIndex $ finS (complement i)))

216 |   ||| Rotate the argument left by the specified number of bits.

217 |   rotL : a -> Fin bitSize -> a

218 |   rotL x i =

219 |     (x `shiftL` (bitsToIndex i)) .|. (x `shiftR` (bitsToIndex $ finS (complement i)))

221 | public export

222 | asBitVector : FiniteBits a => a -> Vect (bitSize {a}) Bool

223 | asBitVector v = testBit v . bitsToIndex <$> allFins _

225 | public export

226 | asString : FiniteBits a => a -> String

227 | asString = pack . toList . map (\ b => ifThenElse b '1' '0') . reverse . asBitVector

229 | public export %inline

230 | FiniteBits Bits8 where

231 |   bitSize     = 8

232 |   bitsToIndex = id

234 |   popCount x0 =

235 |     -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-32-bit-integer

236 |     let x1 = (x0 .&. 0x55) + ((x0 `shiftR` 1) .&. 0x55)

237 |         x2 = (x1 .&. 0x33) + ((x1 `shiftR` 2) .&. 0x33)

238 |         x3 = ((x2 + (x2 `shiftR` 4)) .&. 0x0F)

239 |      in cast x3

241 | public export %inline

242 | FiniteBits Bits16 where

243 |   bitSize     = 16

244 |   bitsToIndex = id

246 |   popCount x0 =

247 |     -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-32-bit-integer

248 |     let x1 = (x0 .&. 0x5555) + ((x0 `shiftR` 1) .&. 0x5555)

249 |         x2 = (x1 .&. 0x3333) + ((x1 `shiftR` 2) .&. 0x3333)

250 |         x3 = ((x2 + (x2 `shiftR` 4)) .&. 0x0F0F)

251 |         x4 = (x3 * 0x0101) `shiftR` 8

252 |      in cast x4

254 | public export %inline

255 | FiniteBits Bits32 where

256 |   bitSize     = 32

257 |   bitsToIndex = id

259 |   popCount x0 =

260 |     -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-32-bit-integer

261 |     let x1 = (x0 .&. 0x55555555) + ((x0 `shiftR` 1) .&. 0x55555555)

262 |         x2 = (x1 .&. 0x33333333) + ((x1 `shiftR` 2) .&. 0x33333333)

263 |         x3 = ((x2 + (x2 `shiftR` 4)) .&. 0x0F0F0F0F)

264 |         x4 = (x3 * 0x01010101) `shiftR` 24

265 |      in cast x4

267 | public export %inline

268 | FiniteBits Bits64 where

269 |   bitSize     = 64

270 |   bitsToIndex = id

272 |   popCount x0 =

273 |     -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-64-bit-integer

274 |     let x1 = (x0 .&. 0x5555555555555555) +

275 |              ((x0 `shiftR` 1) .&. 0x5555555555555555)

276 |         x2 = (x1 .&. 0x3333333333333333)

277 |              + ((x1 `shiftR` 2) .&. 0x3333333333333333)

278 |         x3 = ((x2 + (x2 `shiftR` 4)) .&. 0x0F0F0F0F0F0F0F0F)

279 |         x4 = (x3 * 0x0101010101010101) `shiftR` 56

280 |      in cast x4

282 | public export %inline

283 | FiniteBits Int where

284 |   bitSize     = 64

285 |   bitsToIndex = id

287 |   popCount x =

288 |     -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-32-bit-integer

289 |     -- We have to treat negative numbers separately in order to

290 |     -- prevent overflows in the first addition.

291 |     -- The top bit is therefore cleared and 1 is added in the end

292 |     -- in case of a negative number

293 |     let x0 = x `clearBit` 63

294 |         x1 = (x0 .&. 0x5555555555555555)

295 |            + ((x0 `shiftR` 1) .&. 0x5555555555555555)

296 |         x2 = (x1 .&. 0x3333333333333333)

297 |            + ((x1 `shiftR` 2) .&. 0x3333333333333333)

298 |         x3 = ((x2 + (x2 `shiftR` 4)) .&. 0x0F0F0F0F0F0F0F0F)

299 |         x4 = (x3 * 0x0101010101010101) `shiftR` 56

300 |         x5 = if x < 0 then x4 + 1 else x4

301 |      in cast x5

303 |   -- Rotating signed integers is tricky because right-shifting a signed integer

304 |   -- inserts the signed bit rather than a 0-bit. We can work around this by

305 |   -- casting to (unsigned) Bits64, rotating, and casting back.

306 |   rotR x i =

307 |     let ux : Bits64

308 |         ux = cast x

309 |     in cast $ ux `rotR` i

311 |   rotL x i =

312 |     let ux : Bits64

313 |         ux = cast x

314 |     in cast $ ux `rotL` i

316 | public export %inline

317 | FiniteBits Int8 where

318 |   bitSize     = 8

319 |   bitsToIndex = id

321 |   popCount x =

322 |     -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-32-bit-integer

323 |     -- We have to treat negative numbers separately in order to

324 |     -- prevent overflows in the first addition.

325 |     -- The top bit is therefore cleared and 1 is added in the end

326 |     -- in case of a negative number

327 |     let x0 = x `clearBit` 7

328 |         x1 = (x0 .&. 0x55) + ((x0 `shiftR` 1) .&. 0x55)

329 |         x2 = (x1 .&. 0x33) + ((x1 `shiftR` 2) .&. 0x33)

330 |         x3 = ((x2 + (x2 `shiftR` 4)) .&. 0x0F)

331 |         x4 = if x < 0 then x3 + 1 else x3

332 |      in cast x4

334 |   -- Rotating signed integers is tricky because right-shifting a signed integer

335 |   -- inserts the signed bit rather than a 0-bit. We can work around this by

336 |   -- casting to (unsigned) Bits, rotating, and casting back.

337 |   rotR x i =

338 |     let ux : Bits8

339 |         ux = cast x

340 |     in cast $ ux `rotR` i

342 |   rotL x i =

343 |     let ux : Bits8

344 |         ux = cast x

345 |     in cast $ ux `rotL` i

347 | public export %inline

348 | FiniteBits Int16 where

349 |   bitSize     = 16

350 |   bitsToIndex = id

352 |   popCount x =

353 |     -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-32-bit-integer

354 |     -- We have to treat negative numbers separately in order to

355 |     -- prevent overflows in the first addition.

356 |     -- The top bit is therefore cleared and 1 is added in the end

357 |     -- in case of a negative number

358 |     let x0 = x `clearBit` 15

359 |         x1 = (x0 .&. 0x5555) + ((x0 `shiftR` 1) .&. 0x5555)

360 |         x2 = (x1 .&. 0x3333) + ((x1 `shiftR` 2) .&. 0x3333)

361 |         x3 = ((x2 + (x2 `shiftR` 4)) .&. 0x0F0F)

362 |         x4 = (x3 * 0x0101) `shiftR` 8

363 |         x5 = if x < 0 then x4 + 1 else x4

364 |      in cast x5

366 |   -- Rotating signed integers is tricky because right-shifting a signed integer

367 |   -- inserts the signed bit rather than a 0-bit. We can work around this by

368 |   -- casting to (unsigned) Bits, rotating, and casting back.

369 |   rotR x i =

370 |     let ux : Bits16

371 |         ux = cast x

372 |     in cast $ ux `rotR` i

374 |   rotL x i =

375 |     let ux : Bits16

376 |         ux = cast x

377 |     in cast $ ux `rotL` i

379 | public export %inline

380 | FiniteBits Int32 where

381 |   bitSize     = 32

382 |   bitsToIndex = id

384 |   popCount x =

385 |     -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-32-bit-integer

386 |     -- We have to treat negative numbers separately in order to

387 |     -- prevent overflows in the first addition.

388 |     -- The top bit is therefore cleared and 1 is added in the end

389 |     -- in case of a negative number

390 |     let x0 = x `clearBit` 31

391 |         x1 = (x0 .&. 0x55555555) + ((x0 `shiftR` 1) .&. 0x55555555)

392 |         x2 = (x1 .&. 0x33333333) + ((x1 `shiftR` 2) .&. 0x33333333)

393 |         x3 = ((x2 + (x2 `shiftR` 4)) .&. 0x0F0F0F0F)

394 |         x4 = (x3 * 0x01010101) `shiftR` 24

395 |         x5 = if x < 0 then x4 + 1 else x4

396 |      in cast x5

398 |   -- Rotating signed integers is tricky because right-shifting a signed integer

399 |   -- inserts the signed bit rather than a 0-bit. We can work around this by

400 |   -- casting to (unsigned) Bits, rotating, and casting back.

401 |   rotR x i =

402 |     let ux : Bits32

403 |         ux = cast x

404 |     in cast $ ux `rotR` i

406 |   rotL x i =

407 |     let ux : Bits32

408 |         ux = cast x

409 |     in cast $ ux `rotL` i

411 | public export %inline

412 | FiniteBits Int64 where

413 |   bitSize     = 64

414 |   bitsToIndex = id

416 |   popCount x =

417 |     -- see https://stackoverflow.com/questions/109023/how-to-count-the-number-of-set-bits-in-a-32-bit-integer

418 |     -- We have to treat negative numbers separately in order to

419 |     -- prevent overflows in the first addition.

420 |     -- The top bit is therefore cleared and 1 is added in the end

421 |     -- in case of a negative number

422 |     let x0 = x `clearBit` 63

423 |         x1 = (x0 .&. 0x5555555555555555)

424 |            + ((x0 `shiftR` 1) .&. 0x5555555555555555)

425 |         x2 = (x1 .&. 0x3333333333333333)

426 |            + ((x1 `shiftR` 2) .&. 0x3333333333333333)

427 |         x3 = ((x2 + (x2 `shiftR` 4)) .&. 0x0F0F0F0F0F0F0F0F)

428 |         x4 = (x3 * 0x0101010101010101) `shiftR` 56

429 |         x5 = if x < 0 then x4 + 1 else x4

430 |      in cast x5

432 |   -- Rotating signed integers is tricky because right-shifting a signed integer

433 |   -- inserts the signed bit rather than a 0-bit. We can work around this by

434 |   -- casting to (unsigned) Bits, rotating, and casting back.

435 |   rotR x i =

436 |     let ux : Bits64

437 |         ux = cast x

438 |     in cast $ ux `rotR` i

440 |   rotL x i =

441 |     let ux : Bits64

442 |         ux = cast x

443 |     in cast $ ux `rotL` i