git.iko.soy/Idris-dev
on master help sign in
Merge branch 'show-bits-in-language' of https://github.com/reynir/Idris-dev into reynir-show-bits-in-language
b75246bEdwin Brady
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
@@ -51,16 +52,16 @@ instance Show () where
51 show () = "()"
52 show () = "()"
52
53
53instance Show Bits8 where
54instance Show Bits8 where
54− show = prim__toStrB8
55+ show b = b8ToString b
55
56
56instance Show Bits16 where
57instance Show Bits16 where
57− show = prim__toStrB16
58+ show b = b16ToString b
58
59
59instance Show Bits32 where
60instance Show Bits32 where
60− show = prim__toStrB32
61+ show b = b32ToString b
61
62
62instance Show Bits64 where
63instance Show Bits64 where
63− show = prim__toStrB64
64+ show b = b64ToString b
64
65
65%assert_total
66%assert_total
66viewB8x16 : Bits8x16 -> (Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8)
67viewB8x16 : 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+import Prelude.Vect
5+
6+%access public
7+%default total
8+
9+
10+private
11+toHexDigit : Fin 16 -> Char
12+toHexDigit n = index n hexVect where
13+ hexVect : Vect 16 Char
14+ hexVect = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',
15+ 'A', 'B', 'C', 'D', 'E', 'F']
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+6
@@ -35,3 +35,9 @@ toLower x = if (isUpper x)
35 then (prim__intToChar (prim__charToInt x + 32))
35 then (prim__intToChar (prim__charToInt x + 32))
36 else x
36 else x
37
37
38+isHexDigit : Char -> Bool
39+isHexDigit x = elem (toUpper x) hexChars where
40+ hexChars : List Char
41+ hexChars = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',
42+ 'A', 'B', 'C', 'D', 'E', 'F']
43+
lib/base.ipkg+1−1
@@ -7,7 +7,7 @@ modules = Builtins, Prelude, IO, System,
7 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
7 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
8 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
8 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
9 Prelude.Heap, Prelude.Complex, Prelude.Functor, Prelude.Foldable,
9 Prelude.Heap, Prelude.Complex, Prelude.Functor, Prelude.Foldable,
10− Prelude.Traversable,
10+ Prelude.Traversable, Prelude.Bits,
11
11
12 Network.Cgi,
12 Network.Cgi,
13 Debug.Trace,
13 Debug.Trace,