git.iko.soy/Idris-dev
on master help sign in
In-language implementation of Show BitsN
53376fcReynir Reynisson
lib/Prelude.idr+5−4
compare with master
unifiedsplit
@@ -16,6 +16,7 @@ import Prelude.Vect
16import Prelude.Strings
16import Prelude.Strings
17import Prelude.Chars
17import Prelude.Chars
18import Prelude.Traversable
18import Prelude.Traversable
19+import Prelude.Bits
19
20
20%access public
21%access public
21%default total
22%default total
@@ -48,16 +49,16 @@ instance Show Bool where
48 show False = "False"
49 show False = "False"
49
50
50instance Show Bits8 where
51instance Show Bits8 where
51− show = prim__toStrB8
52+ show b = b8ToString b
52
53
53instance Show Bits16 where
54instance Show Bits16 where
54− show = prim__toStrB16
55+ show b = b16ToString b
55
56
56instance Show Bits32 where
57instance Show Bits32 where
57− show = prim__toStrB32
58+ show b = b32ToString b
58
59
59instance Show Bits64 where
60instance Show Bits64 where
60− show = prim__toStrB64
61+ show b = b64ToString b
61
62
62%assert_total
63%assert_total
63viewB8x16 : Bits8x16 -> (Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8)
64viewB8x16 : Bits8x16 -> (Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8)
lib/Prelude/Bits.idrnew file+56
@@ -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
lib/Prelude/Chars.idr+7
@@ -1,6 +1,7 @@
1module Prelude.Char
1module Prelude.Char
2
2
3import Builtins
3import Builtins
4+import Prelude.Vect
4
5
5isUpper : Char -> Bool
6isUpper : Char -> Bool
6isUpper x = x >= 'A' && x <= 'Z'
7isUpper x = x >= 'A' && x <= 'Z'
@@ -35,3 +36,9 @@ toLower x = if (isUpper x)
35 then (prim__intToChar (prim__charToInt x + 32))
36 then (prim__intToChar (prim__charToInt x + 32))
36 else x
37 else x
37
38
39+isHexDigit : Char -> Bool
40+isHexDigit x = elem (toUpper x) hexChars where
41+ hexChars : Vect 16 Char
42+ hexChars = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',
43+ 'A', 'B', 'C', 'D', 'E', 'F']
44+