0d44c3f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Extensive style and naming cleanup

0d44c3fBenjamin Saunders14 years ago

lib/Prelude/Bits.idr+95−103

compare with master

unifiedsplit

@@ -89,233 +89,214 @@ intToBits n = MkBits (intToBits' n)

89instance Cast Int (Bits n) where

90 cast = intToBits

92−unsafeBitsToInt' : machineTy n -> Int

92+bitsToInt' : machineTy n -> Int

93−unsafeBitsToInt' {n=n} x with n

93+bitsToInt' {n=n} x with n

94 | O = prim__B32ToInt (prim__zextB8_32 x)

95 | S O = prim__B32ToInt (prim__zextB16_32 x)

96 | S (S O) = prim__B32ToInt x

97 | S (S (S _)) = prim__B32ToInt (prim__truncB64_32 x)

99public

100−unsafeBitsToInt : Bits n -> Int

100+bitsToInt : Bits n -> Int

101−unsafeBitsToInt (MkBits x) = unsafeBitsToInt' x

101+bitsToInt (MkBits x) = bitsToInt' x

102

103−bitsShl' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

103+shiftLeft' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

104−bitsShl' {n=n} x c with (log2Bytes n)

104+shiftLeft' {n=n} x c with (log2Bytes n)

105 | O = pad8' n prim__shlB8 x c

106 | S O = pad16' n prim__shlB16 x c

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

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

109

110public

111−bitsShl : Bits n -> Bits n -> Bits n

111+shiftLeft : Bits n -> Bits n -> Bits n

112−bitsShl (MkBits x) (MkBits y) = MkBits (bitsShl' x y)

112+shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)

113

114−bitsLShr' : machineTy n -> machineTy n -> machineTy n

114+shiftRightLogical' : machineTy n -> machineTy n -> machineTy n

115−bitsLShr' {n=n} x c with n

115+shiftRightLogical' {n=n} x c with n

116 | O = prim__lshrB8 x c

117 | S O = prim__lshrB16 x c

118 | S (S O) = prim__lshrB32 x c

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

120

121public

122−bitsLShr : Bits n -> Bits n -> Bits n

122+shiftRightLogical : Bits n -> Bits n -> Bits n

123−bitsLShr (MkBits x) (MkBits y) = MkBits (bitsLShr' x y)

123+shiftRightLogical (MkBits x) (MkBits y) = MkBits (shiftRightLogical' x y)

124

125−bitsAShr' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

125+shiftRightArithmetic' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

126−bitsAShr' {n=n} x c with (log2Bytes n)

126+shiftRightArithmetic' {n=n} x c with (log2Bytes n)

127 | O = pad8' n prim__ashrB8 x c

128 | S O = pad16' n prim__ashrB16 x c

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

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

131

132public

133−bitsAShr : Bits n -> Bits n -> Bits n

133+shiftRightArithmetic : Bits n -> Bits n -> Bits n

134−bitsAShr (MkBits x) (MkBits y) = MkBits (bitsAShr' x y)

134+shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)

135

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

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

137−bitsAnd' {n=n} x y with n

137+and' {n=n} x y with n

138 | O = prim__andB8 x y

139 | S O = prim__andB16 x y

140 | S (S O) = prim__andB32 x y

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

142

143public

144−bitsAnd : Bits n -> Bits n -> Bits n

144+and : Bits n -> Bits n -> Bits n

145−bitsAnd (MkBits x) (MkBits y) = MkBits (bitsAnd' x y)

145+and (MkBits x) (MkBits y) = MkBits (and' x y)

146

147−bitsOr' : machineTy n -> machineTy n -> machineTy n

147+or' : machineTy n -> machineTy n -> machineTy n

148−bitsOr' {n=n} x y with n

148+or' {n=n} x y with n

149 | O = prim__orB8 x y

150 | S O = prim__orB16 x y

151 | S (S O) = prim__orB32 x y

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

153

154public

155−bitsOr : Bits n -> Bits n -> Bits n

155+or : Bits n -> Bits n -> Bits n

156−bitsOr (MkBits x) (MkBits y) = MkBits (bitsOr' x y)

156+or (MkBits x) (MkBits y) = MkBits (or' x y)

157

158−bitsXOr' : machineTy n -> machineTy n -> machineTy n

158+xor' : machineTy n -> machineTy n -> machineTy n

159−bitsXOr' {n=n} x y with n

159+xor' {n=n} x y with n

160 | O = prim__xorB8 x y

161 | S O = prim__xorB16 x y

162 | S (S O) = prim__xorB32 x y

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

164

165public

166−bitsXOr : Bits n -> Bits n -> Bits n

166+xor : Bits n -> Bits n -> Bits n

167−bitsXOr (MkBits x) (MkBits y) = MkBits (bitsXOr' x y)

167+xor (MkBits x) (MkBits y) = MkBits (xor' x y)

168

169−bitsAdd' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

169+plus' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

170−bitsAdd' {n=n} x y with (log2Bytes n)

170+plus' {n=n} x y with (log2Bytes n)

171 | O = pad8 n prim__addB8 x y

172 | S O = pad16 n prim__addB16 x y

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

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

175

176public

177−bitsAdd : Bits n -> Bits n -> Bits n

177+plus : Bits n -> Bits n -> Bits n

178−bitsAdd (MkBits x) (MkBits y) = MkBits (bitsAdd' x y)

178+plus (MkBits x) (MkBits y) = MkBits (plus' x y)

179

180−bitsSub' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

180+minus' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

181−bitsSub' {n=n} x y with (log2Bytes n)

181+minus' {n=n} x y with (log2Bytes n)

182 | O = pad8 n prim__subB8 x y

183 | S O = pad16 n prim__subB16 x y

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

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

186

187public

188−bitsSub : Bits n -> Bits n -> Bits n

188+minus : Bits n -> Bits n -> Bits n

189−bitsSub (MkBits x) (MkBits y) = MkBits (bitsSub' x y)

189+minus (MkBits x) (MkBits y) = MkBits (minus' x y)

190

191−bitsMul' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

191+times' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

192−bitsMul' {n=n} x y with (log2Bytes n)

192+times' {n=n} x y with (log2Bytes n)

193 | O = pad8 n prim__mulB8 x y

194 | S O = pad16 n prim__mulB16 x y

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

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

197

198public

199−bitsMul : Bits n -> Bits n -> Bits n

199+times : Bits n -> Bits n -> Bits n

200−bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)

200+times (MkBits x) (MkBits y) = MkBits (times' x y)

201

202partial

203−bitsSDiv' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

203+sdiv' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

204−bitsSDiv' {n=n} x y with (log2Bytes n)

204+sdiv' {n=n} x y with (log2Bytes n)

205 | O = prim__sdivB8 x y

206 | S O = prim__sdivB16 x y

207 | S (S O) = prim__sdivB32 x y

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

209

210public partial

211−bitsSDiv : Bits n -> Bits n -> Bits n

211+sdiv : Bits n -> Bits n -> Bits n

212−bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)

212+sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)

213

214partial

215−bitsUDiv' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

215+udiv' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

216−bitsUDiv' {n=n} x y with (log2Bytes n)

216+udiv' {n=n} x y with (log2Bytes n)

217 | O = prim__udivB8 x y

218 | S O = prim__udivB16 x y

219 | S (S O) = prim__udivB32 x y

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

221

222public partial

223−bitsUDiv : Bits n -> Bits n -> Bits n

223+udiv : Bits n -> Bits n -> Bits n

224−bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)

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

225

226partial

227−bitsSRem' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

227+srem' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

228−bitsSRem' {n=n} x y with (log2Bytes n)

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

229 | O = prim__sremB8 x y

230 | S O = prim__sremB16 x y

231 | S (S O) = prim__sremB32 x y

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

233

234public partial

235−bitsSRem : Bits n -> Bits n -> Bits n

235+srem : Bits n -> Bits n -> Bits n

236−bitsSRem (MkBits x) (MkBits y) = MkBits (bitsSRem' x y)

236+srem (MkBits x) (MkBits y) = MkBits (srem' x y)

237

238partial

239−bitsURem' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

239+urem' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

240−bitsURem' {n=n} x y with (log2Bytes n)

240+urem' {n=n} x y with (log2Bytes n)

241 | O = prim__uremB8 x y

242 | S O = prim__uremB16 x y

243 | S (S O) = prim__uremB32 x y

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

245

246public partial

247−bitsURem : Bits n -> Bits n -> Bits n

247+urem : Bits n -> Bits n -> Bits n

248−bitsURem (MkBits x) (MkBits y) = MkBits (bitsURem' x y)

248+urem (MkBits x) (MkBits y) = MkBits (urem' x y)

249

250-- TODO: Proofy comparisons via postulates

251−bitsLt' : machineTy n -> machineTy n -> Int

251+lt : machineTy n -> machineTy n -> Int

252−bitsLt' {n=n} x y with n

252+lt {n=n} x y with n

253 | O = prim__ltB8 x y

254 | S O = prim__ltB16 x y

255 | S (S O) = prim__ltB32 x y

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

257

258−public

259−bitsLt : Bits n -> Bits n -> Bool

260−bitsLt (MkBits x) (MkBits y) = bitsLt' x y /= 0

261−

262−bitsLte' : machineTy n -> machineTy n -> Int

258+lte : machineTy n -> machineTy n -> Int

263−bitsLte' {n=n} x y with n

259+lte {n=n} x y with n

264 | O = prim__lteB8 x y

260 | O = prim__lteB8 x y

265 | S O = prim__lteB16 x y

261 | S O = prim__lteB16 x y

266 | S (S O) = prim__lteB32 x y

262 | S (S O) = prim__lteB32 x y

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

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

268

264

269−public

270−bitsLte : Bits n -> Bits n -> Bool

271−bitsLte (MkBits x) (MkBits y) = bitsLte' x y /= 0

272−

273−bitsEq' : machineTy n -> machineTy n -> Int

265+eq : machineTy n -> machineTy n -> Int

274−bitsEq' {n=n} x y with n

266+eq {n=n} x y with n

275 | O = prim__eqB8 x y

267 | O = prim__eqB8 x y

276 | S O = prim__eqB16 x y

268 | S O = prim__eqB16 x y

277 | S (S O) = prim__eqB32 x y

269 | S (S O) = prim__eqB32 x y

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

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

279

271

280−public

281−bitsEq : Bits n -> Bits n -> Bool

282−bitsEq (MkBits x) (MkBits y) = bitsEq' x y /= 0

283−

284−bitsGte' : machineTy n -> machineTy n -> Int

272+gte : machineTy n -> machineTy n -> Int

285−bitsGte' {n=n} x y with n

273+gte {n=n} x y with n

286 | O = prim__gteB8 x y

274 | O = prim__gteB8 x y

287 | S O = prim__gteB16 x y

275 | S O = prim__gteB16 x y

288 | S (S O) = prim__gteB32 x y

276 | S (S O) = prim__gteB32 x y

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

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

290

278

291−public

292−bitsGte : Bits n -> Bits n -> Bool

293−bitsGte (MkBits x) (MkBits y) = bitsGte' x y /= 0

294−

295−bitsGt' : machineTy n -> machineTy n -> Int

279+gt : machineTy n -> machineTy n -> Int

296−bitsGt' {n=n} x y with n

280+gt {n=n} x y with n

297 | O = prim__gtB8 x y

281 | O = prim__gtB8 x y

298 | S O = prim__gtB16 x y

282 | S O = prim__gtB16 x y

299 | S (S O) = prim__gtB32 x y

283 | S (S O) = prim__gtB32 x y

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

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

301

285

302−public

303−bitsGt : Bits n -> Bits n -> Bool

304−bitsGt (MkBits x) (MkBits y) = bitsGt' x y /= 0

305−

306instance Eq (Bits n) where

286instance Eq (Bits n) where

307− (==) = bitsEq

287+ (MkBits x) == (MkBits y) = boolOp eq x y

308

288

309instance Ord (Bits n) where

289instance Ord (Bits n) where

310− (<) = bitsLt

290+ (MkBits x) < (MkBits y) = boolOp lt x y

311− (<=) = bitsLte

291+ (MkBits x) <= (MkBits y) = boolOp lte x y

312− (>=) = bitsGte

292+ (MkBits x) >= (MkBits y) = boolOp gte x y

313− (>) = bitsGt

293+ (MkBits x) > (MkBits y) = boolOp gt x y

314− compare x y = if x `bitsLt` y

294+ compare (MkBits x) (MkBits y) =

295+ if (x `lt` y) /= 0

315− then LT

296+ then LT

316− else if x `bitsEq` y

297+ else if (x `eq` y) /= 0

317− then EQ

298+ then EQ

318− else GT

299+ else GT

319

300

320complement' : machineTy n -> machineTy n

301complement' : machineTy n -> machineTy n

321complement' {n=n} x with n

302complement' {n=n} x with n

@@ -344,8 +325,8 @@ zext' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))

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

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

345

326

346public partial

327public partial

347−zext : Bits n -> Bits (n+m)

328+zeroExtend : Bits n -> Bits (n+m)

348−zext (MkBits x) = MkBits (zext' x)

329+zeroExtend (MkBits x) = MkBits (zext' x)

349

330

350-- TODO: Prove

331-- TODO: Prove

351%assert_total

332%assert_total

@@ -363,8 +344,8 @@ sext' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))

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

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

364

345

365public partial

346public partial

366−sext : Bits n -> Bits (n+m)

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

367−sext (MkBits x) = MkBits (sext' x)

348+signExtend (MkBits x) = MkBits (sext' x)

368

349

369-- TODO: Prove

350-- TODO: Prove

370%assert_total

351%assert_total

@@ -385,9 +366,20 @@ public partial

385truncate : Bits (n+m) -> Bits n

366truncate : Bits (n+m) -> Bits n

386truncate (MkBits x) = MkBits (trunc' x)

367truncate (MkBits x) = MkBits (trunc' x)

387

368

369+bitAt : Fin n -> Bits n

370+bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)

371+

372+public

373+getBit : Fin n -> Bits n -> Bool

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

375+

376+public

377+setBit : Fin n -> Bits n -> Bits n

378+setBit n x = x `or` (bitAt n)

379+

388public

380public

389−bitSet : Fin n -> Bits n -> Bool

381+unsetBit : Fin n -> Bits n -> Bits n

390−bitSet n x = bitsAnd (intToBits 1 `bitsShl` intToBits (cast (finToNat n))) x /= intToBits 0

382+unsetBit n x = x `and` complement (bitAt n)

391

383

392public

384public

393bitsToStr : Bits n -> String

385bitsToStr : Bits n -> String

@@ -396,4 +388,4 @@ bitsToStr x = pack (helper last x)

396 %assert_total

388 %assert_total

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

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

398 helper fO _ = []

390 helper fO _ = []

399− helper (fS x) b = (if bitSet x b then '1' else '0') :: helper (weaken x) b

391+ helper (fS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b

lib/Prelude/Fin.idr+11−4

@@ -14,12 +14,19 @@ instance Eq (Fin n) where

14 eq (fS k) (fS k') = eq k k'

15 eq _ _ = False

17−finToNat : Fin n -> Nat

17+finToNat : Fin n -> Nat -> Nat

18−finToNat fO = O

18+finToNat fO a = a

19−finToNat (fS x) = S (finToNat x)

19+finToNat (fS x) a = finToNat x (S a)

21instance Cast (Fin n) Nat where

22− cast = finToNat

22+ cast x = finToNat x O

23+

24+finToInt : Fin n -> Int -> Int

25+finToInt fO a = a

26+finToInt (fS x) a = finToInt x (a + 1)

27+

28+instance Cast (Fin n) Int where

29+ cast x = finToInt x 0

24weaken : Fin n -> Fin (S n)

31weaken : Fin n -> Fin (S n)

25weaken fO = fO

32weaken fO = fO

lib/Prelude/Modular.idr+9−21

@@ -15,25 +15,13 @@ modBin f (MkMod2 x) (MkMod2 y) = MkMod2 (f x y)

15modComp : (Bits n -> Bits n -> a) -> Mod2 n -> Mod2 n -> a

16modComp f (MkMod2 x) (MkMod2 y) = f x y

18−public

19−modAdd : Mod2 n -> Mod2 n -> Mod2 n

20−modAdd = modBin bitsAdd

21−

22−public

23−modSub : Mod2 n -> Mod2 n -> Mod2 n

24−modSub = modBin bitsSub

25−

26−public

27−modMul : Mod2 n -> Mod2 n -> Mod2 n

28−modMul = modBin bitsMul

29−

30public partial

18public partial

31−modDiv : Mod2 n -> Mod2 n -> Mod2 n

19+div : Mod2 n -> Mod2 n -> Mod2 n

32−modDiv = modBin bitsUDiv

20+div = modBin udiv

34public partial

22public partial

35−modRem : Mod2 n -> Mod2 n -> Mod2 n

23+rem : Mod2 n -> Mod2 n -> Mod2 n

36−modRem = modBin bitsURem

24+rem = modBin urem

38%assert_total

26%assert_total

39public

27public

@@ -59,9 +47,9 @@ instance Ord (Mod2 n) where

59 compare = modComp compare

47 compare = modComp compare

61instance Num (Mod2 n) where

49instance Num (Mod2 n) where

62− (+) = modAdd

50+ (+) = modBin plus

63− (-) = modSub

51+ (-) = modBin minus

64− (*) = modMul

52+ (*) = modBin times

65 abs = id

53 abs = id

66 fromInteger = intToMod

54 fromInteger = intToMod

@@ -78,5 +66,5 @@ modToStr x = pack (reverse (helper x))

78 where

66 where

79 %assert_total

67 %assert_total

80 helper : Mod2 n -> List Char

68 helper : Mod2 n -> List Char

81− helper x = strIndex "0123456789" (unsafeBitsToInt (modToBits (x `modRem` 10)))

69+ helper x = strIndex "0123456789" (bitsToInt (modToBits (x `rem` 10)))

82− :: (if x < 10 then [] else helper (x `modDiv` 10))

70+ :: (if x < 10 then [] else helper (x `div` 10))