5e22753 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

More docs

5e22753Synthetica910 years ago

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

compare with master

unifiedsplit

@@ -72,22 +72,29 @@ data Bits : Nat -> Type where

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

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

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

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

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

76−pad8 : (n : Nat) -> (f :(Bits8 -> Bits8 -> Bits8)) -> Bits8 -> Bits8 -> Bits8

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

77pad8 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

78 where

79 where

79 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)

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

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

82pad16 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

83 where

86 where

84 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)

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

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

87pad32 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

88 where

93 where

89 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)

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

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

92pad64 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

93 where

100 where

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

114 where

121 where

115 pad = getPad {n=3} n

122 pad = getPad {n=3} n

116

123

117−-- 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

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

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

119shiftLeft' : %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)

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

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

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

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

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

125 | _ = assert_unreachable

132 | _ = assert_unreachable

126

133

134+||| Binary left shift

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

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

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

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

129

137

138+||| Logical binary right shift

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

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

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

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

132 | Z = prim__lshrB8 x c

141 | Z = prim__lshrB8 x c

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

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

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

136 | _ = assert_unreachable

145 | _ = assert_unreachable

137

146

147+||| Logical binary right shift

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

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

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

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

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

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

141

151

152+||| Arithematic binary right shift

142shiftRightArithmetic' : %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)

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

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

144 | Z = pad8' n prim__ashrB8 x c

155 | Z = pad8' n prim__ashrB8 x c

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

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

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

148 | _ = assert_unreachable

159 | _ = assert_unreachable

149

160

161+||| Arithematic binary right shift

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

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

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

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

152

164

165+||| Binary and

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

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

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

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

155 | Z = prim__andB8 x y

168 | Z = prim__andB8 x y

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

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

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

159 | _ = assert_unreachable

172 | _ = assert_unreachable

160

173

174+||| Binary and

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

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

162and {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)

163

177

178+||| Binary or

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

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

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

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

166 | Z = prim__orB8 x y

181 | Z = prim__orB8 x y

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

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

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

170 | _ = assert_unreachable

185 | _ = assert_unreachable

171

186

187+||| Binary or

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

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

173or {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)

174

190

191+||| Binary xor

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

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

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

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

177 | Z = prim__xorB8 x y

194 | Z = prim__xorB8 x y

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

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

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

181 | _ = assert_unreachable

198 | _ = assert_unreachable

182

199

200+||| Binary xor

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

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

184xor {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)

185

203

204+||| Overflowing addition

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

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

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

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

188 | Z = pad8 n prim__addB8 x y

207 | Z = pad8 n prim__addB8 x y

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

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

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

192 | _ = assert_unreachable

211 | _ = assert_unreachable

193

212

213+||| Overflowing addition

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

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

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

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

196

216

217+||| Subtraction

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

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

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

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

199 | Z = pad8 n prim__subB8 x y

220 | Z = pad8 n prim__subB8 x y

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

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

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

203 | _ = assert_unreachable

224 | _ = assert_unreachable

204

225

226+||| Subtraction

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

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

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

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

207

229

230+||| Multiplication

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

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

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

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

210 | Z = pad8 n prim__mulB8 x y

233 | Z = pad8 n prim__mulB8 x y

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

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

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

214 | _ = assert_unreachable

237 | _ = assert_unreachable

215

238

239+||| Multiplication

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

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

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

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

218

242

243+||| Signed integer division

219partial

244partial

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

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

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

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

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

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

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

226 | _ = assert_unreachable

251 | _ = assert_unreachable

227

252

253+||| Signed integer division

228partial

254partial

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

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

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

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

231

257

258+||| Unsigned integer division

232partial

259partial

233udiv' : %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)

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

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

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

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

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

239 | _ = assert_unreachable

266 | _ = assert_unreachable

240

267

268+||| Unsigned integer division

241partial

269partial

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

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

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

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

244

272

273+||| Signed remainder (mod)

245partial

274partial

246srem' : %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)

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

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

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

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

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

252 | _ = assert_unreachable

281 | _ = assert_unreachable

253

282

283+||| Signed remainder (mod)

254partial

284partial

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

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

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

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

257

287

288+||| Unsigned remainder (mod)

258partial

289partial

259urem' : %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)

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

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

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

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

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

265 | _ = assert_unreachable

296 | _ = assert_unreachable

266

297

298+||| Unsigned remainder (mod)

267partial

299partial

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

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

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

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