git.iko.soy/Idris-dev
on master help sign in
Prelude.Bits: clarify serialization of BitsX for X={8,16,32,64}
9fdbb72Jacob Mitchell
libs/prelude/Prelude/Bits.idr+105−23
compare with master
unifiedsplit
@@ -2,12 +2,14 @@ module Prelude.Bits
2
2
3import Builtins
3import Builtins
4
4
5+import Prelude.Algebra
5import Prelude.Basics
6import Prelude.Basics
6import Prelude.Bool
7import Prelude.Bool
7import Prelude.Cast
8import Prelude.Cast
8import Prelude.Chars
9import Prelude.Chars
9import Prelude.Interfaces
10import Prelude.Interfaces
10import Prelude.Foldable
11import Prelude.Foldable
12+import Prelude.Functor
11import Prelude.Nat
13import Prelude.Nat
12import Prelude.List
14import Prelude.List
13import Prelude.Strings
15import Prelude.Strings
@@ -15,8 +17,54 @@ import Prelude.Strings
15%access public export
17%access public export
16%default total
18%default total
17
19
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.
18−b8ToString : Bits8 -> String
66+b8ToHexString : Bits8 -> String
19−b8ToString c = pack (with List [c1, c2])
67+b8ToHexString c = pack [c1, c2]
20 where getDigit : Bits8 -> Char
68 where getDigit : Bits8 -> Char
21 getDigit b = let n = prim__zextB8_Int b in
69 getDigit b = let n = prim__zextB8_Int b in
22 if n >= 0 && n <= 9
70 if n >= 0 && n <= 9
@@ -27,30 +75,64 @@ b8ToString c = pack (with List [c1, c2])
27 c1 = getDigit (prim__andB8 (prim__lshrB8 c 4) 15)
75 c1 = getDigit (prim__andB8 (prim__lshrB8 c 4) 15)
28 c2 = getDigit (prim__andB8 c 15)
76 c2 = getDigit (prim__andB8 c 15)
29
77
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."
30
124
125+||| Encode `Bits16` as a 4-character hex string.
31b16ToString : Bits16 -> String
126b16ToString : Bits16 -> String
32−b16ToString c = c1 ++ c2 where
127+b16ToString = b16ToHexString
33− c1 = b8ToString upper where
128+%deprecate b16ToString "Please use `b16ToHexString` instead."
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
129
130+||| Encode `Bits32` as a 8-character hex string.
40b32ToString : Bits32 -> String
131b32ToString : Bits32 -> String
41−b32ToString c = c1 ++ c2 where
132+b32ToString = b32ToHexString
42− c1 = b16ToString upper where
133+%deprecate b32ToString "Please use `b32ToHexString` instead."
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
48
134
135+||| Encode `Bits64` as a 16-character hex string.
49b64ToString : Bits64 -> String
136b64ToString : Bits64 -> String
50−b64ToString c = c1 ++ c2 where
137+b64ToString = b64ToHexString
51− c1 = b32ToString upper where
138+%deprecate b64ToString "Please use `b64ToHexString` instead."
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
libs/prelude/Prelude/Show.idr+4−4
@@ -164,16 +164,16 @@ Show () where
164 show () = "()"
164 show () = "()"
165
165
166Show Bits8 where
166Show Bits8 where
167− show b = b8ToString b
167+ show b = b8ToHexString b
168
168
169Show Bits16 where
169Show Bits16 where
170− show b = b16ToString b
170+ show b = b16ToHexString b
171
171
172Show Bits32 where
172Show Bits32 where
173− show b = b32ToString b
173+ show b = b32ToHexString b
174
174
175Show Bits64 where
175Show Bits64 where
176− show b = b64ToString b
176+ show b = b64ToHexString b
177
177
178(Show a, Show b) => Show (a, b) where
178(Show a, Show b) => Show (a, b) where
179 show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
179 show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"