66f4ddd · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #3634 from Synthetica9/BitsComments

66f4dddNiklas Larsson10 years ago

libs/base/Data/Bits.idr+54−4

compare with master

unifiedsplit

@@ -6,6 +6,9 @@ import Data.Fin

6 -- to improve it! (EB)

7%access export

9+||| Finds the next exponent of a power of two.

10+||| For example `nextPow2 200 = 8`, because 2^8 = 256.

11+||| If it is an exact match, it is not rounded up: `nextPow2 256 = 8` because 2^8 = 256.

9public export

12public export

10nextPow2 : Nat -> Nat

13nextPow2 : Nat -> Nat

11nextPow2 Z = Z

14nextPow2 Z = Z

@@ -15,10 +18,17 @@ nextPow2 (S x) = if (S x) == (2 `power` l2x)

15 where

18 where

16 l2x = log2NZ (S x) SIsNotZ

19 l2x = log2NZ (S x) SIsNotZ

21+||| Gets the lowest n for which "8 * 2 ^ n" is larger than or equal to the input.

22+||| For example, `nextBytes 10 = 16`.

23+||| Like with nextPow2, the result is not rounded up, so `nextBytes 16 = 16`.

18public export

24public export

19nextBytes : Nat -> Nat

25nextBytes : Nat -> Nat

20nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))

26nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))

28+||| An index function to access the Bits* types in order.

29+||| machineTy 0 = Bits8, machineTy 1 = Bits16, etc.

30+||| Any input that would result in getting a type that is larger than supported

31+||| will result in the largest supported type instead (currently 64 bits).

22public export

32public export

23machineTy : Nat -> Type

33machineTy : Nat -> Type

24machineTy Z = Bits8

34machineTy Z = Bits8

@@ -26,9 +36,13 @@ machineTy (S Z) = Bits16

26machineTy (S (S Z)) = Bits32

36machineTy (S (S Z)) = Bits32

27machineTy (S (S (S _))) = Bits64

37machineTy (S (S (S _))) = Bits64

39+||| Finds the number of bits used by `machineTy n`.

40+||| For example, bitsUsed 2 = 16

29bitsUsed : Nat -> Nat

41bitsUsed : Nat -> Nat

30bitsUsed n = 8 * (2 `power` n)

42bitsUsed n = 8 * (2 `power` n)

44+||| Converts a Nat to a machineTy n, with the first argument as an accumulator.

45+||| You shouldn't have to call this manually, use natToBits (without ') instead.

32natToBits' : %static {n : Nat} -> machineTy n -> Nat -> machineTy n

46natToBits' : %static {n : Nat} -> machineTy n -> Nat -> machineTy n

33natToBits' a Z = a

47natToBits' a Z = a

34natToBits' {n=n} a x with (n)

48natToBits' {n=n} a x with (n)

@@ -39,6 +53,7 @@ natToBits' {n=n} a x with (n)

39 natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'

53 natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'

40 natToBits' a _ | _ = assert_unreachable

54 natToBits' a _ | _ = assert_unreachable

56+||| Converts a Nat to a machineTy n.

42natToBits : %static {n : Nat} -> Nat -> machineTy n

57natToBits : %static {n : Nat} -> Nat -> machineTy n

43natToBits {n=n} x with (n)

58natToBits {n=n} x with (n)

44 | Z = natToBits' {n=0} (prim__truncInt_B8 0) x

59 | Z = natToBits' {n=0} (prim__truncInt_B8 0) x

@@ -50,25 +65,36 @@ natToBits {n=n} x with (n)

50getPad : %static {n : Nat} -> Nat -> machineTy n

65getPad : %static {n : Nat} -> Nat -> machineTy n

51getPad n = assert_total $ natToBits (minus (bitsUsed (nextBytes n)) n)

66getPad n = assert_total $ natToBits (minus (bitsUsed (nextBytes n)) n)

68+||| A "high-level" wrapper to the types defined by `machineTy`.

53public export

69public export

54data Bits : Nat -> Type where

70data Bits : Nat -> Type where

71+ ||| An bits type that has at least n bits available,

72+ ||| up to the maximum supported by `machineTy`.

55 MkBits : machineTy (nextBytes n) -> Bits n

73 MkBits : machineTy (nextBytes n) -> Bits n

75+||| Perform a function over Bits8 as if it is carried out on n bits.

76+||| (n should be 8 or lower)

57−pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8

77+pad8 : (n : Nat) -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8

58pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad

78pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad

59 where

79 where

60 pad = getPad {n=0} n

80 pad = getPad {n=0} n

82+||| Perform a function over Bits16 as if it is carried out on n bits.

83+||| (n should be 16 or lower)

62−pad16 : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16

84+pad16 : (n: Nat) -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16

63pad16 n f x y = prim__lshrB16 (f (prim__shlB16 x pad) (prim__shlB16 y pad)) pad

85pad16 n f x y = prim__lshrB16 (f (prim__shlB16 x pad) (prim__shlB16 y pad)) pad

64 where

86 where

65 pad = getPad {n=1} n

87 pad = getPad {n=1} n

89+||| Perform a function over Bits32 as if it is carried out on n bits.

90+||| (n should be 32 or lower)

67pad32 : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32

91pad32 : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32

68pad32 n f x y = prim__lshrB32 (f (prim__shlB32 x pad) (prim__shlB32 y pad)) pad

92pad32 n f x y = prim__lshrB32 (f (prim__shlB32 x pad) (prim__shlB32 y pad)) pad

69 where

93 where

70 pad = getPad {n=2} n

94 pad = getPad {n=2} n

96+||| Perform a function over Bits64 as if it is carried out on n bits.

97+||| (n should be 64 or lower)

72pad64 : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64

98pad64 : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64

73pad64 n f x y = prim__lshrB64 (f (prim__shlB64 x pad) (prim__shlB64 y pad)) pad

99pad64 n f x y = prim__lshrB64 (f (prim__shlB64 x pad) (prim__shlB64 y pad)) pad

74 where

100 where

@@ -95,7 +121,7 @@ pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad

95 where

121 where

96 pad = getPad {n=3} n

122 pad = getPad {n=3} n

123

98−-- TODO: This (and all the other functions along these lings) is -- because it is used by things. Do they really need to be

124+-- TODO: This (and all the other functions along these lines) is -- because it is used by things. Do they really need to be

99-- public export, or is export good enough?

125-- public export, or is export good enough?

100shiftLeft' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

126shiftLeft' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

101shiftLeft' {n=n} x c with (nextBytes n)

127shiftLeft' {n=n} x c with (nextBytes n)

@@ -105,9 +131,11 @@ shiftLeft' {n=n} x c with (nextBytes n)

105 | S (S (S _)) = pad64' n prim__shlB64 x c

131 | S (S (S _)) = pad64' n prim__shlB64 x c

106 | _ = assert_unreachable

132 | _ = assert_unreachable

107

133

134+||| Binary left shift

108shiftLeft : %static {n : Nat} -> Bits n -> Bits n -> Bits n

135shiftLeft : %static {n : Nat} -> Bits n -> Bits n -> Bits n

109shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)

136shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)

110

137

138+||| Logical binary right shift

111shiftRightLogical' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n

139shiftRightLogical' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n

112shiftRightLogical' {n=n} x c with (n)

140shiftRightLogical' {n=n} x c with (n)

113 | Z = prim__lshrB8 x c

141 | Z = prim__lshrB8 x c

@@ -116,10 +144,12 @@ shiftRightLogical' {n=n} x c with (n)

116 | S (S (S _)) = prim__lshrB64 x c

144 | S (S (S _)) = prim__lshrB64 x c

117 | _ = assert_unreachable

145 | _ = assert_unreachable

118

146

147+||| Logical binary right shift

119shiftRightLogical : %static {n : Nat} -> Bits n -> Bits n -> Bits n

148shiftRightLogical : %static {n : Nat} -> Bits n -> Bits n -> Bits n

120shiftRightLogical {n} (MkBits x) (MkBits y)

149shiftRightLogical {n} (MkBits x) (MkBits y)

121 = MkBits {n} (shiftRightLogical' {n=nextBytes n} x y)

150 = MkBits {n} (shiftRightLogical' {n=nextBytes n} x y)

122

151

152+||| Arithematic binary right shift

123shiftRightArithmetic' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

153shiftRightArithmetic' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

124shiftRightArithmetic' {n=n} x c with (nextBytes n)

154shiftRightArithmetic' {n=n} x c with (nextBytes n)

125 | Z = pad8' n prim__ashrB8 x c

155 | Z = pad8' n prim__ashrB8 x c

@@ -128,9 +158,11 @@ shiftRightArithmetic' {n=n} x c with (nextBytes n)

128 | S (S (S _)) = pad64' n prim__ashrB64 x c

158 | S (S (S _)) = pad64' n prim__ashrB64 x c

129 | _ = assert_unreachable

159 | _ = assert_unreachable

130

160

161+||| Arithematic binary right shift

131shiftRightArithmetic : %static {n : Nat} -> Bits n -> Bits n -> Bits n

162shiftRightArithmetic : %static {n : Nat} -> Bits n -> Bits n -> Bits n

132shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)

163shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)

133

164

165+||| Binary and

134and' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n

166and' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n

135and' {n=n} x y with (n)

167and' {n=n} x y with (n)

136 | Z = prim__andB8 x y

168 | Z = prim__andB8 x y

@@ -139,9 +171,11 @@ and' {n=n} x y with (n)

139 | S (S (S _)) = prim__andB64 x y

171 | S (S (S _)) = prim__andB64 x y

140 | _ = assert_unreachable

172 | _ = assert_unreachable

141

173

174+||| Binary and

142and : %static {n : Nat} -> Bits n -> Bits n -> Bits n

175and : %static {n : Nat} -> Bits n -> Bits n -> Bits n

143and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)

176and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)

144

177

178+||| Binary or

145or' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n

179or' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n

146or' {n=n} x y with (n)

180or' {n=n} x y with (n)

147 | Z = prim__orB8 x y

181 | Z = prim__orB8 x y

@@ -150,9 +184,11 @@ or' {n=n} x y with (n)

150 | S (S (S _)) = prim__orB64 x y

184 | S (S (S _)) = prim__orB64 x y

151 | _ = assert_unreachable

185 | _ = assert_unreachable

152

186

187+||| Binary or

153or : %static {n : Nat} -> Bits n -> Bits n -> Bits n

188or : %static {n : Nat} -> Bits n -> Bits n -> Bits n

154or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)

189or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)

155

190

191+||| Binary xor

156xor' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n

192xor' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n

157xor' {n=n} x y with (n)

193xor' {n=n} x y with (n)

158 | Z = prim__xorB8 x y

194 | Z = prim__xorB8 x y

@@ -161,9 +197,11 @@ xor' {n=n} x y with (n)

161 | S (S (S _)) = prim__xorB64 x y

197 | S (S (S _)) = prim__xorB64 x y

162 | _ = assert_unreachable

198 | _ = assert_unreachable

163

199

200+||| Binary xor

164xor : %static {n : Nat} -> Bits n -> Bits n -> Bits n

201xor : %static {n : Nat} -> Bits n -> Bits n -> Bits n

165xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)

202xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)

166

203

204+||| Overflowing addition

167plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

205plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

168plus' {n=n} x y with (nextBytes n)

206plus' {n=n} x y with (nextBytes n)

169 | Z = pad8 n prim__addB8 x y

207 | Z = pad8 n prim__addB8 x y

@@ -172,9 +210,11 @@ plus' {n=n} x y with (nextBytes n)

172 | S (S (S _)) = pad64 n prim__addB64 x y

210 | S (S (S _)) = pad64 n prim__addB64 x y

173 | _ = assert_unreachable

211 | _ = assert_unreachable

174

212

213+||| Overflowing addition

175plus : %static {n : Nat} -> Bits n -> Bits n -> Bits n

214plus : %static {n : Nat} -> Bits n -> Bits n -> Bits n

176plus (MkBits x) (MkBits y) = MkBits (plus' x y)

215plus (MkBits x) (MkBits y) = MkBits (plus' x y)

177

216

217+||| Subtraction

178minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

218minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

179minus' {n=n} x y with (nextBytes n)

219minus' {n=n} x y with (nextBytes n)

180 | Z = pad8 n prim__subB8 x y

220 | Z = pad8 n prim__subB8 x y

@@ -183,9 +223,11 @@ minus' {n=n} x y with (nextBytes n)

183 | S (S (S _)) = pad64 n prim__subB64 x y

223 | S (S (S _)) = pad64 n prim__subB64 x y

184 | _ = assert_unreachable

224 | _ = assert_unreachable

185

225

226+||| Subtraction

186minus : %static {n : Nat} -> Bits n -> Bits n -> Bits n

227minus : %static {n : Nat} -> Bits n -> Bits n -> Bits n

187minus (MkBits x) (MkBits y) = MkBits (minus' x y)

228minus (MkBits x) (MkBits y) = MkBits (minus' x y)

188

229

230+||| Multiplication

189times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

231times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

190times' {n=n} x y with (nextBytes n)

232times' {n=n} x y with (nextBytes n)

191 | Z = pad8 n prim__mulB8 x y

233 | Z = pad8 n prim__mulB8 x y

@@ -194,9 +236,11 @@ times' {n=n} x y with (nextBytes n)

194 | S (S (S _)) = pad64 n prim__mulB64 x y

236 | S (S (S _)) = pad64 n prim__mulB64 x y

195 | _ = assert_unreachable

237 | _ = assert_unreachable

196

238

239+||| Multiplication

197times : %static {n : Nat} -> Bits n -> Bits n -> Bits n

240times : %static {n : Nat} -> Bits n -> Bits n -> Bits n

198times (MkBits x) (MkBits y) = MkBits (times' x y)

241times (MkBits x) (MkBits y) = MkBits (times' x y)

199

242

243+||| Signed integer division

200partial

244partial

201sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

245sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

202sdiv' {n=n} x y with (nextBytes n)

246sdiv' {n=n} x y with (nextBytes n)

@@ -206,10 +250,12 @@ sdiv' {n=n} x y with (nextBytes n)

206 | S (S (S _)) = prim__sdivB64 x y

250 | S (S (S _)) = prim__sdivB64 x y

207 | _ = assert_unreachable

251 | _ = assert_unreachable

208

252

253+||| Signed integer division

209partial

254partial

210sdiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n

255sdiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n

211sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)

256sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)

212

257

258+||| Unsigned integer division

213partial

259partial

214udiv' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

260udiv' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

215udiv' {n=n} x y with (nextBytes n)

261udiv' {n=n} x y with (nextBytes n)

@@ -219,10 +265,12 @@ udiv' {n=n} x y with (nextBytes n)

219 | S (S (S _)) = prim__udivB64 x y

265 | S (S (S _)) = prim__udivB64 x y

220 | _ = assert_unreachable

266 | _ = assert_unreachable

221

267

268+||| Unsigned integer division

222partial

269partial

223udiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n

270udiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n

224udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)

271udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)

225

272

273+||| Signed remainder (mod)

226partial

274partial

227srem' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

275srem' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

228srem' {n=n} x y with (nextBytes n)

276srem' {n=n} x y with (nextBytes n)

@@ -232,10 +280,12 @@ srem' {n=n} x y with (nextBytes n)

232 | S (S (S _)) = prim__sremB64 x y

280 | S (S (S _)) = prim__sremB64 x y

233 | _ = assert_unreachable

281 | _ = assert_unreachable

234

282

283+||| Signed remainder (mod)

235partial

284partial

236srem : %static {n : Nat} -> Bits n -> Bits n -> Bits n

285srem : %static {n : Nat} -> Bits n -> Bits n -> Bits n

237srem (MkBits x) (MkBits y) = MkBits (srem' x y)

286srem (MkBits x) (MkBits y) = MkBits (srem' x y)

238

287

288+||| Unsigned remainder (mod)

239partial

289partial

240urem' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

290urem' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

241urem' {n=n} x y with (nextBytes n)

291urem' {n=n} x y with (nextBytes n)

@@ -245,6 +295,7 @@ urem' {n=n} x y with (nextBytes n)

245 | S (S (S _)) = prim__uremB64 x y

295 | S (S (S _)) = prim__uremB64 x y

246 | _ = assert_unreachable

296 | _ = assert_unreachable

247

297

298+||| Unsigned remainder (mod)

248partial

299partial

249urem : %static {n : Nat} -> Bits n -> Bits n -> Bits n

300urem : %static {n : Nat} -> Bits n -> Bits n -> Bits n

250urem (MkBits x) (MkBits y) = MkBits (urem' x y)

301urem (MkBits x) (MkBits y) = MkBits (urem' x y)

@@ -447,4 +498,3 @@ bitsToStr x = pack (helper last x)

447

498

448implementation Show (Bits n) where

499implementation Show (Bits n) where

449 show = bitsToStr

500 show = bitsToStr

450−