@@ -2,12 +2,14 @@ module Prelude.Bits
22
33import Builtins
44
5+import Prelude.Algebra
56import Prelude.Basics
67import Prelude.Bool
78import Prelude.Cast
89import Prelude.Chars
910import Prelude.Interfaces
1011import Prelude.Foldable
12+import Prelude.Functor
1113import Prelude.Nat
1214import Prelude.List
1315import Prelude.Strings
@@ -15,8 +17,54 @@ import Prelude.Strings
1517%access public export
1618%default total
1719
18−b8ToString : Bits8 -> String
19−b8ToString c = pack (with List [c1, c2])
20+--------------------------------------------------------------------------------
21+-- Convert to `List Bits8`
22+--------------------------------------------------------------------------------
23+
24+||| Convert to list of `Bits8` with the most signficant byte at the
25+||| head.
26+b8ToBytes : Bits8 -> List Bits8
27+b8ToBytes b = [b]
28+
29+||| Convert to list of `Bits8` with the most signficant byte at the
30+||| head.
31+b16ToBytes : Bits16 -> List Bits8
32+b16ToBytes b =
33+ [ prim__truncB16_B8 (prim__lshrB16 b 8)
34+ , prim__truncB16_B8 b
35+ ]
36+
37+||| Convert to list of `Bits8` with the most signficant byte at the
38+||| head.
39+b32ToBytes : Bits32 -> List Bits8
40+b32ToBytes b =
41+ [ prim__truncB32_B8 (prim__lshrB32 b 24)
42+ , prim__truncB32_B8 (prim__lshrB32 b 16)
43+ , prim__truncB32_B8 (prim__lshrB32 b 8)
44+ , prim__truncB32_B8 b
45+ ]
46+
47+||| Convert to list of `Bits8` with the most signficant byte at the
48+||| head.
49+b64ToBytes : Bits64 -> List Bits8
50+b64ToBytes b =
51+ [ prim__truncB64_B8 (prim__lshrB64 b 56)
52+ , prim__truncB64_B8 (prim__lshrB64 b 48)
53+ , prim__truncB64_B8 (prim__lshrB64 b 40)
54+ , prim__truncB64_B8 (prim__lshrB64 b 32)
55+ , prim__truncB64_B8 (prim__lshrB64 b 24)
56+ , prim__truncB64_B8 (prim__lshrB64 b 16)
57+ , prim__truncB64_B8 (prim__lshrB64 b 8)
58+ , prim__truncB64_B8 b
59+ ]
60+
61+--------------------------------------------------------------------------------
62+-- Hex Strings
63+--------------------------------------------------------------------------------
64+
65+||| Encode `Bits8` as a 2-character hex string.
66+b8ToHexString : Bits8 -> String
67+b8ToHexString c = pack [c1, c2]
2068 where getDigit : Bits8 -> Char
2169 getDigit b = let n = prim__zextB8_Int b in
2270 if n >= 0 && n <= 9
@@ -27,30 +75,64 @@ b8ToString c = pack (with List [c1, c2])
2775 c1 = getDigit (prim__andB8 (prim__lshrB8 c 4) 15)
2876 c2 = getDigit (prim__andB8 c 15)
2977
78+||| Encode `Bits16` as a 4-character hex string.
79+b16ToHexString : Bits16 -> String
80+b16ToHexString c = concatMap b8ToHexString (b16ToBytes c)
81+
82+||| Encode `Bits32` as an 8-character hex string.
83+b32ToHexString : Bits32 -> String
84+b32ToHexString c = concatMap b8ToHexString (b32ToBytes c)
85+
86+||| Encode `Bits64` as a 16-character hex string.
87+b64ToHexString : Bits64 -> String
88+b64ToHexString c = concatMap b8ToHexString (b64ToBytes c)
89+
90+
91+--------------------------------------------------------------------------------
92+-- Binary Strings
93+--------------------------------------------------------------------------------
94+
95+||| Encode `Bits8` as an 8-character binary string.
96+b8ToBinString : Bits8 -> String
97+b8ToBinString b = pack $ map (bitChar b) [7,6,5,4,3,2,1,0]
98+ where bitChar : Bits8 -> Bits8 -> Char
99+ bitChar b i = case b `prim__andB8` (1 `prim__shlB8` i) of
100+ 0 => '0'
101+ _ => '1'
102+
103+||| Encode `Bits16` as a 16-character binary string.
104+b16ToBinString : Bits16 -> String
105+b16ToBinString c = concatMap b8ToBinString (b16ToBytes c)
106+
107+||| Encode `Bits32` as a 32-character binary string.
108+b32ToBinString : Bits32 -> String
109+b32ToBinString c = concatMap b8ToBinString (b32ToBytes c)
110+
111+||| Encode `Bits64` as a 64-character binary string.
112+b64ToBinString : Bits64 -> String
113+b64ToBinString c = concatMap b8ToBinString (b64ToBytes c)
114+
115+
116+--------------------------------------------------------------------------------
117+-- Deprecated String Functions
118+--------------------------------------------------------------------------------
119+
120+||| Encode `Bits8` as a 2-character hex string.
121+b8ToString : Bits8 -> String
122+b8ToString = b8ToHexString
123+%deprecate b8ToString "Please use `b8ToHexString` instead."
30124
125+||| Encode `Bits16` as a 4-character hex string.
31126b16ToString : 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
127+b16ToString = b16ToHexString
128+%deprecate b16ToString "Please use `b16ToHexString` instead."
39129
130+||| Encode `Bits32` as a 8-character hex string.
40131b32ToString : Bits32 -> String
41−b32ToString c = c1 ++ c2 where
42− c1 = b16ToString upper where
43− upper : Bits16
44− upper = prim__truncB32_B16 (prim__andB32 (prim__lshrB32 c 16) 0x0000ffff)
45− c2 = b16ToString lower where
46− lower : Bits16
47− lower = prim__truncB32_B16 c
132+b32ToString = b32ToHexString
133+%deprecate b32ToString "Please use `b32ToHexString` instead."
48134
135+||| Encode `Bits64` as a 16-character hex string.
49136b64ToString : Bits64 -> String
50−b64ToString c = c1 ++ c2 where
51− c1 = b32ToString upper where
52− upper : Bits32
53− upper = prim__truncB64_B32 (prim__andB64 (prim__lshrB64 c 32) 0x00000000ffffffff)
54− c2 = b32ToString lower where
55− lower : Bits32
56− lower = prim__truncB64_B32 c
137+b64ToString = b64ToHexString
138+%deprecate b64ToString "Please use `b64ToHexString` instead."