forked from idris-lang/Idris-dev
/
Bits.idr
56 lines (48 loc) · 1.45 KB
/
Bits.idr
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
module Prelude.Bits
import Prelude.Strings
import Prelude.Vect
%access public
%default total
private
toHexDigit : Fin 16 -> Char
toHexDigit n = index n hexVect where
hexVect : Vect 16 Char
hexVect = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',
'A', 'B', 'C', 'D', 'E', 'F']
b8ToString : Bits8 -> String
b8ToString c = pack [c1, c2] where
%assert_total -- We will only supply numbers that can fit in 4 bits
toFin16 : Bits8 -> Fin 16
toFin16 n = if n == 0
then fZ
else believe_me (fS (toFin16 (n-1)))
c1 = toHexDigit upper where
upper : Fin 16
upper = toFin16 (prim__lshrB8 c 4)
c2 = toHexDigit lower where
lower : Fin 16
lower = toFin16 (prim__andB8 c 0xf)
b16ToString : Bits16 -> String
b16ToString c = c1 ++ c2 where
c1 = b8ToString upper where
upper : Bits8
upper = prim__truncB16_B8 (prim__lshrB16 c 8)
c2 = b8ToString lower where
lower : Bits8
lower = prim__truncB16_B8 c
b32ToString : Bits32 -> String
b32ToString c = c1 ++ c2 where
c1 = b16ToString upper where
upper : Bits16
upper = prim__truncB32_B16 (prim__lshrB32 c 16)
c2 = b16ToString lower where
lower : Bits16
lower = prim__truncB32_B16 c
b64ToString : Bits64 -> String
b64ToString c = c1 ++ c2 where
c1 = b32ToString upper where
upper : Bits32
upper = prim__truncB64_B32 (prim__lshrB64 c 32)
c2 = b32ToString lower where
lower : Bits32
lower = prim__truncB64_B32 c