0222012 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2911 from ziman/bits-static

0222012Jan de Muijnck-Hughes11 years ago

libs/base/Data/Bits.idr+60−95

compare with master

unifiedsplit

@@ -3,6 +3,7 @@ module Data.Bits

3import Data.Fin

5%default total

6+%access export

7public export

8public export

8nextPow2 : Nat -> Nat

9nextPow2 : Nat -> Nat

@@ -28,7 +29,7 @@ bitsUsed : Nat -> Nat

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

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

30%assert_total

31%assert_total

31−natToBits' : machineTy n -> Nat -> machineTy n

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

32natToBits' a Z = a

33natToBits' a Z = a

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

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

34 -- it seems I have to manually recover the value of n here, instead of being able to reference it

35 -- it seems I have to manually recover the value of n here, instead of being able to reference it

@@ -37,14 +38,14 @@ natToBits' {n=n} a x with (n)

37 natToBits' a (S x') | S (S Z) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x'

38 natToBits' a (S x') | S (S Z) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x'

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

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

40−natToBits : Nat -> machineTy n

41+natToBits : %static {n : Nat} -> Nat -> machineTy n

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

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

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

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

43 | S Z = natToBits' {n=1} (prim__truncInt_B16 0) x

44 | S Z = natToBits' {n=1} (prim__truncInt_B16 0) x

44 | S (S Z) = natToBits' {n=2} (prim__truncInt_B32 0) x

45 | S (S Z) = natToBits' {n=2} (prim__truncInt_B32 0) x

45 | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x

46 | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x

47−getPad : Nat -> machineTy n

48+getPad : %static {n : Nat} -> Nat -> machineTy n

48getPad n = natToBits (minus (bitsUsed (nextBytes n)) n)

49getPad n = natToBits (minus (bitsUsed (nextBytes n)) n)

50public export

51public export

@@ -92,83 +93,69 @@ pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad

92 where

93 where

93 pad = getPad {n=3} n

94 pad = getPad {n=3} n

95−-- TODO: This (and all the other functions along these lings) is public export

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

96−-- because it is used by public export things. Do they really need to be

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

98−public export

99−shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

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

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

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

101 | Z = pad8' n prim__shlB8 x c

100 | Z = pad8' n prim__shlB8 x c

102 | S Z = pad16' n prim__shlB16 x c

101 | S Z = pad16' n prim__shlB16 x c

103 | S (S Z) = pad32' n prim__shlB32 x c

102 | S (S Z) = pad32' n prim__shlB32 x c

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

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

105

104

106−public export

107−shiftLeft : Bits n -> Bits n -> Bits n

105+shiftLeft : %static {n : Nat} -> Bits n -> Bits n -> Bits n

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

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

109

107

110−public export

111−shiftRightLogical' : machineTy n -> machineTy n -> machineTy n

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

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

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

113 | Z = prim__lshrB8 x c

110 | Z = prim__lshrB8 x c

114 | S Z = prim__lshrB16 x c

111 | S Z = prim__lshrB16 x c

115 | S (S Z) = prim__lshrB32 x c

112 | S (S Z) = prim__lshrB32 x c

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

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

117

114

118−public export

119−shiftRightLogical : Bits n -> Bits n -> Bits n

115+shiftRightLogical : %static {n : Nat} -> Bits n -> Bits n -> Bits n

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

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

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

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

122

118

123−public export

124−shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

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

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

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

126 | Z = pad8' n prim__ashrB8 x c

121 | Z = pad8' n prim__ashrB8 x c

127 | S Z = pad16' n prim__ashrB16 x c

122 | S Z = pad16' n prim__ashrB16 x c

128 | S (S Z) = pad32' n prim__ashrB32 x c

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

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

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

130

125

131−public export

132−shiftRightArithmetic : Bits n -> Bits n -> Bits n

126+shiftRightArithmetic : %static {n : Nat} -> Bits n -> Bits n -> Bits n

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

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

134

128

135−public export

136−and' : machineTy n -> machineTy n -> machineTy n

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

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

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

138 | Z = prim__andB8 x y

131 | Z = prim__andB8 x y

139 | S Z = prim__andB16 x y

132 | S Z = prim__andB16 x y

140 | S (S Z) = prim__andB32 x y

133 | S (S Z) = prim__andB32 x y

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

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

142

135

143−public export

144−and : Bits n -> Bits n -> Bits n

136+and : %static {n : Nat} -> Bits n -> Bits n -> Bits n

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

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

146

138

147−public export

148−or' : machineTy n -> machineTy n -> machineTy n

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

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

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

150 | Z = prim__orB8 x y

141 | Z = prim__orB8 x y

151 | S Z = prim__orB16 x y

142 | S Z = prim__orB16 x y

152 | S (S Z) = prim__orB32 x y

143 | S (S Z) = prim__orB32 x y

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

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

154

145

155−public export

156−or : Bits n -> Bits n -> Bits n

146+or : %static {n : Nat} -> Bits n -> Bits n -> Bits n

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

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

158

148

159−public export

160−xor' : machineTy n -> machineTy n -> machineTy n

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

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

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

162 | Z = prim__xorB8 x y

151 | Z = prim__xorB8 x y

163 | S Z = prim__xorB16 x y

152 | S Z = prim__xorB16 x y

164 | S (S Z) = prim__xorB32 x y

153 | S (S Z) = prim__xorB32 x y

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

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

166

155

167−public export

168−xor : Bits n -> Bits n -> Bits n

156+xor : %static {n : Nat} -> Bits n -> Bits n -> Bits n

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

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

170

158

171−public export

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

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

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

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

174 | Z = pad8 n prim__addB8 x y

161 | Z = pad8 n prim__addB8 x y

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

176 | S (S Z) = pad32 n prim__addB32 x y

163 | S (S Z) = pad32 n prim__addB32 x y

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

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

178

165

179−public export

180−plus : Bits n -> Bits n -> Bits n

166+plus : %static {n : Nat} -> Bits n -> Bits n -> Bits n

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

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

182

168

183−public export

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

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

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

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

186 | Z = pad8 n prim__subB8 x y

171 | Z = pad8 n prim__subB8 x y

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

188 | S (S Z) = pad32 n prim__subB32 x y

173 | S (S Z) = pad32 n prim__subB32 x y

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

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

190

175

191−public export

192−minus : Bits n -> Bits n -> Bits n

176+minus : %static {n : Nat} -> Bits n -> Bits n -> Bits n

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

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

194

178

195−public export

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

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

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

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

198 | Z = pad8 n prim__mulB8 x y

181 | Z = pad8 n prim__mulB8 x y

@@ -200,12 +183,10 @@ times' {n=n} x y with (nextBytes n)

200 | S (S Z) = pad32 n prim__mulB32 x y

183 | S (S Z) = pad32 n prim__mulB32 x y

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

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

202

185

203−public export

204−times : Bits n -> Bits n -> Bits n

186+times : %static {n : Nat} -> Bits n -> Bits n -> Bits n

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

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

206

188

207partial

189partial

208−public export

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

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

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

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

211 | Z = prim__sdivB8 x y

192 | Z = prim__sdivB8 x y

@@ -213,88 +194,85 @@ sdiv' {n=n} x y with (nextBytes n)

213 | S (S Z) = prim__sdivB32 x y

194 | S (S Z) = prim__sdivB32 x y

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

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

215

196

216−public export partial

197+partial

217−sdiv : Bits n -> Bits n -> Bits n

198+sdiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n

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

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

219

200

220partial

201partial

221−public export

222−udiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

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

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

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

224 | Z = prim__udivB8 x y

204 | Z = prim__udivB8 x y

225 | S Z = prim__udivB16 x y

205 | S Z = prim__udivB16 x y

226 | S (S Z) = prim__udivB32 x y

206 | S (S Z) = prim__udivB32 x y

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

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

228

208

229−public export partial

209+partial

230−udiv : Bits n -> Bits n -> Bits n

210+udiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n

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

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

232

212

233−public export partial

213+partial

234−srem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

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

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

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

236 | Z = prim__sremB8 x y

216 | Z = prim__sremB8 x y

237 | S Z = prim__sremB16 x y

217 | S Z = prim__sremB16 x y

238 | S (S Z) = prim__sremB32 x y

218 | S (S Z) = prim__sremB32 x y

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

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

240

220

241−public export partial

221+partial

242−srem : Bits n -> Bits n -> Bits n

222+srem : %static {n : Nat} -> Bits n -> Bits n -> Bits n

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

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

244

224

245−public export partial

225+partial

246−urem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

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

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

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

248 | Z = prim__uremB8 x y

228 | Z = prim__uremB8 x y

249 | S Z = prim__uremB16 x y

229 | S Z = prim__uremB16 x y

250 | S (S Z) = prim__uremB32 x y

230 | S (S Z) = prim__uremB32 x y

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

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

252

232

253−public export partial

233+partial

254−urem : Bits n -> Bits n -> Bits n

234+urem : %static {n : Nat} -> Bits n -> Bits n -> Bits n

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

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

256

236

257-- TODO: Proofy comparisons via postulates

237-- TODO: Proofy comparisons via postulates

258−lt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

238+lt : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

259lt {n=n} x y with (nextBytes n)

239lt {n=n} x y with (nextBytes n)

260 | Z = prim__ltB8 x y

240 | Z = prim__ltB8 x y

261 | S Z = prim__ltB16 x y

241 | S Z = prim__ltB16 x y

262 | S (S Z) = prim__ltB32 x y

242 | S (S Z) = prim__ltB32 x y

263 | S (S (S _)) = prim__ltB64 x y

243 | S (S (S _)) = prim__ltB64 x y

264

244

265−lte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

245+lte : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

266lte {n=n} x y with (nextBytes n)

246lte {n=n} x y with (nextBytes n)

267 | Z = prim__lteB8 x y

247 | Z = prim__lteB8 x y

268 | S Z = prim__lteB16 x y

248 | S Z = prim__lteB16 x y

269 | S (S Z) = prim__lteB32 x y

249 | S (S Z) = prim__lteB32 x y

270 | S (S (S _)) = prim__lteB64 x y

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

271

251

272−eq : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

252+eq : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

273eq {n=n} x y with (nextBytes n)

253eq {n=n} x y with (nextBytes n)

274 | Z = prim__eqB8 x y

254 | Z = prim__eqB8 x y

275 | S Z = prim__eqB16 x y

255 | S Z = prim__eqB16 x y

276 | S (S Z) = prim__eqB32 x y

256 | S (S Z) = prim__eqB32 x y

277 | S (S (S _)) = prim__eqB64 x y

257 | S (S (S _)) = prim__eqB64 x y

278

258

279−gte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

259+gte : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

280gte {n=n} x y with (nextBytes n)

260gte {n=n} x y with (nextBytes n)

281 | Z = prim__gteB8 x y

261 | Z = prim__gteB8 x y

282 | S Z = prim__gteB16 x y

262 | S Z = prim__gteB16 x y

283 | S (S Z) = prim__gteB32 x y

263 | S (S Z) = prim__gteB32 x y

284 | S (S (S _)) = prim__gteB64 x y

264 | S (S (S _)) = prim__gteB64 x y

285

265

286−gt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

266+gt : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

287gt {n=n} x y with (nextBytes n)

267gt {n=n} x y with (nextBytes n)

288 | Z = prim__gtB8 x y

268 | Z = prim__gtB8 x y

289 | S Z = prim__gtB16 x y

269 | S Z = prim__gtB16 x y

290 | S (S Z) = prim__gtB32 x y

270 | S (S Z) = prim__gtB32 x y

291 | S (S (S _)) = prim__gtB64 x y

271 | S (S (S _)) = prim__gtB64 x y

292

272

293−public export

294implementation Eq (Bits n) where

273implementation Eq (Bits n) where

295 (MkBits x) == (MkBits y) = boolOp eq x y

274 (MkBits x) == (MkBits y) = boolOp eq x y

296

275

297−public export

298implementation Ord (Bits n) where

276implementation Ord (Bits n) where

299 (MkBits x) < (MkBits y) = boolOp lt x y

277 (MkBits x) < (MkBits y) = boolOp lt x y

300 (MkBits x) <= (MkBits y) = boolOp lte x y

278 (MkBits x) <= (MkBits y) = boolOp lte x y

@@ -307,8 +285,7 @@ implementation Ord (Bits n) where

307 then EQ

285 then EQ

308 else GT

286 else GT

309

287

310−public export

311−complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)

288+complement' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)

312complement' {n=n} x with (nextBytes n)

289complement' {n=n} x with (nextBytes n)

313 | Z = let pad = getPad {n=0} n in

290 | Z = let pad = getPad {n=0} n in

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

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

@@ -319,13 +296,12 @@ complement' {n=n} x with (nextBytes n)

319 | S (S (S _)) = let pad = getPad {n=3} n in

296 | S (S (S _)) = let pad = getPad {n=3} n in

320 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad

297 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad

321

298

322−public export

323−complement : Bits n -> Bits n

299+complement : %static {n : Nat} -> Bits n -> Bits n

324complement (MkBits x) = MkBits (complement' x)

300complement (MkBits x) = MkBits (complement' x)

325

301

326-- TODO: Prove

302-- TODO: Prove

327−public export %assert_total -- can't verify coverage of with block

303+%assert_total -- can't verify coverage of with block

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

304+zext' : %static {n : Nat} -> %static {m : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

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

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

330 | (Z, Z) = believe_me x

306 | (Z, Z) = believe_me x

331 | (Z, S Z) = believe_me (prim__zextB8_B16 (believe_me x))

307 | (Z, S Z) = believe_me (prim__zextB8_B16 (believe_me x))

@@ -338,12 +314,11 @@ zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

338 | (S (S Z), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))

314 | (S (S Z), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))

339 | (S (S (S _)), S (S (S _))) = believe_me x

315 | (S (S (S _)), S (S (S _))) = believe_me x

340

316

341−public export

342−zeroExtend : Bits n -> Bits (n+m)

317+zeroExtend : %static {n : Nat} -> %static {m : Nat} -> Bits n -> Bits (n+m)

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

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

344

319

345−public export %assert_total

320+%assert_total

346−intToBits' : Integer -> machineTy (nextBytes n)

321+intToBits' : %static {n : Nat} -> Integer -> machineTy (nextBytes n)

347intToBits' {n=n} x with (nextBytes n)

322intToBits' {n=n} x with (nextBytes n)

348 | Z = let pad = getPad {n=0} n in

323 | Z = let pad = getPad {n=0} n in

349 prim__lshrB8 (prim__shlB8 (prim__truncBigInt_B8 x) pad) pad

324 prim__lshrB8 (prim__shlB8 (prim__truncBigInt_B8 x) pad) pad

@@ -354,28 +329,24 @@ intToBits' {n=n} x with (nextBytes n)

354 | S (S (S _)) = let pad = getPad {n=3} n in

329 | S (S (S _)) = let pad = getPad {n=3} n in

355 prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad

330 prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad

356

331

357−public export

358−intToBits : Integer -> Bits n

332+intToBits : %static {n : Nat} -> Integer -> Bits n

359intToBits n = MkBits (intToBits' n)

333intToBits n = MkBits (intToBits' n)

360

334

361implementation Cast Integer (Bits n) where

335implementation Cast Integer (Bits n) where

362 cast = intToBits

336 cast = intToBits

363

337

364−public export

365−bitsToInt' : machineTy (nextBytes n) -> Integer

338+bitsToInt' : %static {n : Nat} -> machineTy (nextBytes n) -> Integer

366bitsToInt' {n=n} x with (nextBytes n)

339bitsToInt' {n=n} x with (nextBytes n)

367 | Z = prim__zextB8_BigInt x

340 | Z = prim__zextB8_BigInt x

368 | S Z = prim__zextB16_BigInt x

341 | S Z = prim__zextB16_BigInt x

369 | S (S Z) = prim__zextB32_BigInt x

342 | S (S Z) = prim__zextB32_BigInt x

370 | S (S (S _)) = prim__zextB64_BigInt x

343 | S (S (S _)) = prim__zextB64_BigInt x

371

344

372−public export

373−bitsToInt : Bits n -> Integer

345+bitsToInt : %static {n : Nat} -> Bits n -> Integer

374bitsToInt (MkBits x) = bitsToInt' x

346bitsToInt (MkBits x) = bitsToInt' x

375

347

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

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

377−public export

378−zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)

349+zeroUnused : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)

379zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)

350zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)

380

351

381--implementation Cast Nat (Bits n) where

352--implementation Cast Nat (Bits n) where

@@ -383,7 +354,7 @@ zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)

383

354

384-- TODO: Prove

355-- TODO: Prove

385%assert_total -- can't verify coverage of with block

356%assert_total -- can't verify coverage of with block

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

357+sext' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

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

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

388 | (Z, Z) = let pad = getPad {n=0} n in

359 | (Z, Z) = let pad = getPad {n=0} n in

389 believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)

360 believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)

@@ -412,13 +383,12 @@ sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

412 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in

383 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in

413 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)

384 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)

414

385

415−--public export

416−--signExtend : Bits n -> Bits (n+m)

386+----signExtend : Bits n -> Bits (n+m)

417--signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))

387--signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))

418

388

419-- TODO: Prove

389-- TODO: Prove

420−public export %assert_total -- can't verify coverage of with block

390+%assert_total -- can't verify coverage of with block

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

391+trunc' : %static {m : Nat} -> %static {n : Nat} -> machineTy (nextBytes (m+n)) -> machineTy (nextBytes n)

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

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

423 | (Z, Z) = believe_me x

393 | (Z, Z) = believe_me x

424 | (Z, S Z) = believe_me (prim__truncB16_B8 (believe_me x))

394 | (Z, S Z) = believe_me (prim__truncB16_B8 (believe_me x))

@@ -431,31 +401,26 @@ trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))

431 | (S (S Z), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))

401 | (S (S Z), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))

432 | (S (S (S _)), S (S (S _))) = believe_me x

402 | (S (S (S _)), S (S (S _))) = believe_me x

433

403

434−public export

435−truncate : Bits (m+n) -> Bits n

404+truncate : %static {m : Nat} -> %static {n : Nat} -> Bits (m+n) -> Bits n

436truncate (MkBits x) = MkBits (zeroUnused (trunc' x))

405truncate (MkBits x) = MkBits (zeroUnused (trunc' x))

437

406

438−public export

439−bitAt : Fin n -> Bits n

407+bitAt : %static {n : Nat} -> Fin n -> Bits n

440bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)

408bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)

441

409

442−public export

443−getBit : Fin n -> Bits n -> Bool

410+getBit : %static {n : Nat} -> Fin n -> Bits n -> Bool

444getBit n x = (x `and` (bitAt n)) /= intToBits 0

411getBit n x = (x `and` (bitAt n)) /= intToBits 0

445

412

446−public export

447−setBit : Fin n -> Bits n -> Bits n

413+setBit : %static {n : Nat} -> Fin n -> Bits n -> Bits n

448setBit n x = x `or` (bitAt n)

414setBit n x = x `or` (bitAt n)

449

415

450−public export

451−unsetBit : Fin n -> Bits n -> Bits n

416+unsetBit : %static {n : Nat} -> Fin n -> Bits n -> Bits n

452unsetBit n x = x `and` complement (bitAt n)

417unsetBit n x = x `and` complement (bitAt n)

453

418

454−bitsToStr : Bits n -> String

419+bitsToStr : %static {n : Nat} -> Bits n -> String

455bitsToStr x = pack (helper last x)

420bitsToStr x = pack (helper last x)

456 where

421 where

457 %assert_total

422 %assert_total

458− helper : Fin (S n) -> Bits n -> List Char

423+ helper : %static {n : Nat} -> Fin (S n) -> Bits n -> List Char

459 helper FZ _ = []

424 helper FZ _ = []

460 helper (FS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b

425 helper (FS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b

461

426