fe963e8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fixed byte counting math in bitstring code

fe963e8Benjamin Saunders14 years ago

lib/Prelude/Bits.idr+45−38

compare with master

unifiedsplit

@@ -4,14 +4,21 @@ import Prelude.Strings

5%default total

7−log2ceil : Nat -> Nat

7+divCeil : Nat -> Nat -> Nat

8−log2ceil n = let x = log2 n in

8+divCeil x y = case x `mod` y of

9− if x == log2 (n-1)

9+ O => x `div` y

10+ S _ => S (x `div` y)

11+

12+nextPow2 : Nat -> Nat

13+nextPow2 O = O

14+nextPow2 x = if x == (2 `power` l2x)

10− then x+1

15+ then l2x

11− else x

16+ else S l2x

17+ where

18+ l2x = log2 x

13−log2Bytes : Nat -> Nat

20+nextBytes : Nat -> Nat

14−log2Bytes bits = (log2ceil (bits `div` 8))

21+nextBytes bits = (nextPow2 (bits `divCeil` 8))

16machineTy : Nat -> Type

23machineTy : Nat -> Type

17machineTy O = Bits8

24machineTy O = Bits8

@@ -21,7 +28,7 @@ machineTy (S (S (S _))) = Bits64

22public

29public

23data Bits : Nat -> Type where

30data Bits : Nat -> Type where

24− MkBits : machineTy (log2Bytes n) -> Bits n

31+ MkBits : machineTy (nextBytes n) -> Bits n

26pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8

33pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8

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

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

@@ -65,8 +72,8 @@ pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad

65 pad = (prim__intToB64 (cast (64-n)))

72 pad = (prim__intToB64 (cast (64-n)))

67%assert_total

74%assert_total

68−intToBits' : Int -> machineTy (log2Bytes n)

75+intToBits' : Int -> machineTy (nextBytes n)

69−intToBits' {n=n} x with (log2Bytes n)

76+intToBits' {n=n} x with (nextBytes n)

70 | O = let pad = (prim__intToB8 (cast (8-n))) in

77 | O = let pad = (prim__intToB8 (cast (8-n))) in

71 prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad

78 prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad

72 | S O = let pad = (prim__intToB16 (cast (16-n))) in

79 | S O = let pad = (prim__intToB16 (cast (16-n))) in

@@ -94,8 +101,8 @@ public

94bitsToInt : Bits n -> Int

101bitsToInt : Bits n -> Int

95bitsToInt (MkBits x) = bitsToInt' x

102bitsToInt (MkBits x) = bitsToInt' x

103

97−shiftLeft' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

104+shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

98−shiftLeft' {n=n} x c with (log2Bytes n)

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

99 | O = pad8' n prim__shlB8 x c

106 | O = pad8' n prim__shlB8 x c

100 | S O = pad16' n prim__shlB16 x c

107 | S O = pad16' n prim__shlB16 x c

101 | S (S O) = pad32' n prim__shlB32 x c

108 | S (S O) = pad32' n prim__shlB32 x c

@@ -116,8 +123,8 @@ public

116shiftRightLogical : Bits n -> Bits n -> Bits n

123shiftRightLogical : Bits n -> Bits n -> Bits n

117shiftRightLogical (MkBits x) (MkBits y) = MkBits (shiftRightLogical' x y)

124shiftRightLogical (MkBits x) (MkBits y) = MkBits (shiftRightLogical' x y)

118

125

119−shiftRightArithmetic' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

126+shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

120−shiftRightArithmetic' {n=n} x c with (log2Bytes n)

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

121 | O = pad8' n prim__ashrB8 x c

128 | O = pad8' n prim__ashrB8 x c

122 | S O = pad16' n prim__ashrB16 x c

129 | S O = pad16' n prim__ashrB16 x c

123 | S (S O) = pad32' n prim__ashrB32 x c

130 | S (S O) = pad32' n prim__ashrB32 x c

@@ -160,8 +167,8 @@ public

160xor : Bits n -> Bits n -> Bits n

167xor : Bits n -> Bits n -> Bits n

161xor (MkBits x) (MkBits y) = MkBits (xor' x y)

168xor (MkBits x) (MkBits y) = MkBits (xor' x y)

162

169

163−plus' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

170+plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

164−plus' {n=n} x y with (log2Bytes n)

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

165 | O = pad8 n prim__addB8 x y

172 | O = pad8 n prim__addB8 x y

166 | S O = pad16 n prim__addB16 x y

173 | S O = pad16 n prim__addB16 x y

167 | S (S O) = pad32 n prim__addB32 x y

174 | S (S O) = pad32 n prim__addB32 x y

@@ -171,8 +178,8 @@ public

171plus : Bits n -> Bits n -> Bits n

178plus : Bits n -> Bits n -> Bits n

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

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

173

180

174−minus' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

181+minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

175−minus' {n=n} x y with (log2Bytes n)

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

176 | O = pad8 n prim__subB8 x y

183 | O = pad8 n prim__subB8 x y

177 | S O = pad16 n prim__subB16 x y

184 | S O = pad16 n prim__subB16 x y

178 | S (S O) = pad32 n prim__subB32 x y

185 | S (S O) = pad32 n prim__subB32 x y

@@ -182,8 +189,8 @@ public

182minus : Bits n -> Bits n -> Bits n

189minus : Bits n -> Bits n -> Bits n

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

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

184

191

185−times' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

192+times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

186−times' {n=n} x y with (log2Bytes n)

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

187 | O = pad8 n prim__mulB8 x y

194 | O = pad8 n prim__mulB8 x y

188 | S O = pad16 n prim__mulB16 x y

195 | S O = pad16 n prim__mulB16 x y

189 | S (S O) = pad32 n prim__mulB32 x y

196 | S (S O) = pad32 n prim__mulB32 x y

@@ -194,8 +201,8 @@ times : Bits n -> Bits n -> Bits n

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

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

195

202

196partial

203partial

197−sdiv' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

204+sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

198−sdiv' {n=n} x y with (log2Bytes n)

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

199 | O = prim__sdivB8 x y

206 | O = prim__sdivB8 x y

200 | S O = prim__sdivB16 x y

207 | S O = prim__sdivB16 x y

201 | S (S O) = prim__sdivB32 x y

208 | S (S O) = prim__sdivB32 x y

@@ -206,8 +213,8 @@ sdiv : Bits n -> Bits n -> Bits n

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

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

207

214

208partial

215partial

209−udiv' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

216+udiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

210−udiv' {n=n} x y with (log2Bytes n)

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

211 | O = prim__udivB8 x y

218 | O = prim__udivB8 x y

212 | S O = prim__udivB16 x y

219 | S O = prim__udivB16 x y

213 | S (S O) = prim__udivB32 x y

220 | S (S O) = prim__udivB32 x y

@@ -218,8 +225,8 @@ udiv : Bits n -> Bits n -> Bits n

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

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

219

226

220partial

227partial

221−srem' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

228+srem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

222−srem' {n=n} x y with (log2Bytes n)

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

223 | O = prim__sremB8 x y

230 | O = prim__sremB8 x y

224 | S O = prim__sremB16 x y

231 | S O = prim__sremB16 x y

225 | S (S O) = prim__sremB32 x y

232 | S (S O) = prim__sremB32 x y

@@ -230,8 +237,8 @@ srem : Bits n -> Bits n -> Bits n

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

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

231

238

232partial

239partial

233−urem' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

240+urem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

234−urem' {n=n} x y with (log2Bytes n)

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

235 | O = prim__uremB8 x y

242 | O = prim__uremB8 x y

236 | S O = prim__uremB16 x y

243 | S O = prim__uremB16 x y

237 | S (S O) = prim__uremB32 x y

244 | S (S O) = prim__uremB32 x y

@@ -292,8 +299,8 @@ instance Ord (Bits n) where

292 then EQ

299 then EQ

293 else GT

300 else GT

294

301

295−complement' : machineTy (log2Bytes n) -> machineTy (log2Bytes n)

302+complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)

296−complement' {n=n} x with (log2Bytes n)

303+complement' {n=n} x with (nextBytes n)

297 | O = let pad = prim__intToB8 (8 - cast n) in

304 | O = let pad = prim__intToB8 (8 - cast n) in

298 prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad

305 prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad

299 | S O = let pad = prim__intToB16 (16 - cast n) in

306 | S O = let pad = prim__intToB16 (16 - cast n) in

@@ -309,8 +316,8 @@ complement (MkBits x) = MkBits (complement' x)

309

316

310-- TODO: Prove

317-- TODO: Prove

311%assert_total

318%assert_total

312−zext' : machineTy (log2Bytes n) -> machineTy (log2Bytes (n+m))

319+zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

313−zext' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))

320+zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

314 | (O, O) = believe_me x

321 | (O, O) = believe_me x

315 | (O, S O) = believe_me (prim__zextB8_16 (believe_me x))

322 | (O, S O) = believe_me (prim__zextB8_16 (believe_me x))

316 | (O, S (S O)) = believe_me (prim__zextB8_32 (believe_me x))

323 | (O, S (S O)) = believe_me (prim__zextB8_32 (believe_me x))

@@ -327,13 +334,13 @@ zeroExtend : Bits n -> Bits (n+m)

327zeroExtend (MkBits x) = MkBits (zext' x)

334zeroExtend (MkBits x) = MkBits (zext' x)

328

335

329-- Fill in the high bits of a sign-extended bitstring

336-- Fill in the high bits of a sign-extended bitstring

330−fixupSE : (m : Nat) -> machineTy (log2Bytes (n+m)) -> machineTy (log2Bytes (n+m))

337+fixupSE : (m : Nat) -> machineTy (nextBytes (n+m)) -> machineTy (nextBytes (n+m))

331fixupSE m x = x `or'` complement' (zext' {m=m} (complement' (intToBits' 0)))

338fixupSE m x = x `or'` complement' (zext' {m=m} (complement' (intToBits' 0)))

332

339

333-- TODO: Prove

340-- TODO: Prove

334%assert_total

341%assert_total

335−sext' : machineTy (log2Bytes n) -> machineTy (log2Bytes (n+m))

342+sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

336−sext' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))

343+sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

337 | (O, O) = fixupSE m (believe_me x)

344 | (O, O) = fixupSE m (believe_me x)

338 | (O, S O) = fixupSE m (believe_me (prim__sextB8_16 (believe_me x)))

345 | (O, S O) = fixupSE m (believe_me (prim__sextB8_16 (believe_me x)))

339 | (O, S (S O)) = fixupSE m (believe_me (prim__sextB8_32 (believe_me x)))

346 | (O, S (S O)) = fixupSE m (believe_me (prim__sextB8_32 (believe_me x)))

@@ -350,13 +357,13 @@ signExtend : Bits n -> Bits (n+m)

350signExtend (MkBits x) = MkBits (sext' x)

357signExtend (MkBits x) = MkBits (sext' x)

351

358

352-- Zero out the high bits of a truncated bitstring

359-- Zero out the high bits of a truncated bitstring

353−fixupTR : machineTy (log2Bytes n) -> machineTy (log2Bytes n)

360+fixupTR : machineTy (nextBytes n) -> machineTy (nextBytes n)

354fixupTR x = x `and'` complement' (intToBits' 0)

361fixupTR x = x `and'` complement' (intToBits' 0)

355

362

356-- TODO: Prove

363-- TODO: Prove

357%assert_total

364%assert_total

358−trunc' : machineTy (log2Bytes (n+m)) -> machineTy (log2Bytes n)

365+trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)

359−trunc' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))

366+trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

360 | (O, O) = fixupTR (believe_me x)

367 | (O, O) = fixupTR (believe_me x)

361 | (O, S O) = believe_me (prim__truncB16_8 (believe_me x))

368 | (O, S O) = believe_me (prim__truncB16_8 (believe_me x))

362 | (O, S (S O)) = believe_me (prim__truncB32_8 (believe_me x))

369 | (O, S (S O)) = believe_me (prim__truncB32_8 (believe_me x))