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