45bbe39 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Mark bit divisions/remainders as partial

commit45bbe399cb865e617436f6c39e80074c75870a0c authorBenjamin Saunders <besaunde@sfu.ca> dateWed 9 Jan 2013, 15:03 (14 years ago) parent9e543e6

2 files changed+24−16

compare with master

unifiedsplit

lib/Prelude/Bits.idr+8 src/Idris/Primitives.hs+16−16

lib/Prelude/Bits.idr+8

@@ -163,6 +163,7 @@ public

163163bitsMul : Bits n -> Bits n -> Bits n

164164bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)

165165

166+partial

166167bitsSDiv' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n

167168bitsSDiv' {n=n} x y with (nextBits n)

168169 | Bits8 = prim__sdivB8 x y

@@ -171,9 +172,11 @@ bitsSDiv' {n=n} x y with (nextBits n)

171172 | Bits64 = prim__sdivB64 x y

172173

173174public

175+partial

174176bitsSDiv : Bits n -> Bits n -> Bits n

175177bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)

176178

179+partial

177180bitsUDiv' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n

178181bitsUDiv' {n=n} x y with (nextBits n)

179182 | Bits8 = prim__udivB8 x y

@@ -182,9 +185,11 @@ bitsUDiv' {n=n} x y with (nextBits n)

182185 | Bits64 = prim__udivB64 x y

183186

184187public

188+partial

185189bitsUDiv : Bits n -> Bits n -> Bits n

186190bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)

187191

192+partial

188193bitsSRem' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n

189194bitsSRem' {n=n} x y with (nextBits n)

190195 | Bits8 = prim__sremB8 x y

@@ -193,9 +198,11 @@ bitsSRem' {n=n} x y with (nextBits n)

193198 | Bits64 = prim__sremB64 x y

194199

195200public

201+partial

196202bitsSRem : Bits n -> Bits n -> Bits n

197203bitsSRem (MkBits x) (MkBits y) = MkBits (bitsSRem' x y)

198204

205+partial

199206bitsURem' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n

200207bitsURem' {n=n} x y with (nextBits n)

201208 | Bits8 = prim__uremB8 x y

@@ -204,6 +211,7 @@ bitsURem' {n=n} x y with (nextBits n)

204211 | Bits64 = prim__uremB64 x y

205212

206213public

214+partial

207215bitsURem : Bits n -> Bits n -> Bits n

208216bitsURem (MkBits x) (MkBits y) = MkBits (bitsURem' x y)

209217

src/Idris/Primitives.hs+16−16

@@ -94,13 +94,13 @@ primitives =

9494 Prim (UN "prim__mulB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (*))

9595 (2, LB8Times) total,

9696 Prim (UN "prim__udivB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin div)

97− (2, LB8UDiv) total,

97+ (2, LB8UDiv) partial,

9898 Prim (UN "prim__sdivB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin s8div)

99− (2, LB8SDiv) total,

99+ (2, LB8SDiv) partial,

100100 Prim (UN "prim__uremB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin rem)

101− (2, LB8URem) total,

101+ (2, LB8URem) partial,

102102 Prim (UN "prim__sremB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin s8rem)

103− (2, LB8SRem) total,

103+ (2, LB8SRem) partial,

104104 Prim (UN "prim__shlB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> shiftL x (fromIntegral y)))

105105 (2, LB8Shl) total,

106106 Prim (UN "prim__lshrB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> shiftR x (fromIntegral y)))

@@ -147,13 +147,13 @@ primitives =

147147 Prim (UN "prim__mulB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (*))

148148 (2, LB16Times) total,

149149 Prim (UN "prim__udivB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin div)

150− (2, LB16UDiv) total,

150+ (2, LB16UDiv) partial,

151151 Prim (UN "prim__sdivB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin s16div)

152− (2, LB16SDiv) total,

152+ (2, LB16SDiv) partial,

153153 Prim (UN "prim__uremB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin rem)

154− (2, LB16URem) total,

154+ (2, LB16URem) partial,

155155 Prim (UN "prim__sremB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin s16rem)

156− (2, LB16SRem) total,

156+ (2, LB16SRem) partial,

157157 Prim (UN "prim__shlB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> shiftL x (fromIntegral y)))

158158 (2, LB16Shl) total,

159159 Prim (UN "prim__lshrB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> shiftR x (fromIntegral y)))

@@ -198,13 +198,13 @@ primitives =

198198 Prim (UN "prim__mulB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (*))

199199 (2, LB32Times) total,

200200 Prim (UN "prim__udivB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin div)

201− (2, LB32UDiv) total,

201+ (2, LB32UDiv) partial,

202202 Prim (UN "prim__sdivB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin s32div)

203− (2, LB32SDiv) total,

203+ (2, LB32SDiv) partial,

204204 Prim (UN "prim__uremB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin rem)

205− (2, LB32URem) total,

205+ (2, LB32URem) partial,

206206 Prim (UN "prim__sremB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin s32rem)

207− (2, LB32SRem) total,

207+ (2, LB32SRem) partial,

208208 Prim (UN "prim__shlB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> shiftL x (fromIntegral y)))

209209 (2, LB32Shl) total,

210210 Prim (UN "prim__lshrB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> shiftR x (fromIntegral y)))

@@ -247,13 +247,13 @@ primitives =

247247 Prim (UN "prim__mulB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (*))

248248 (2, LB64Times) total,

249249 Prim (UN "prim__udivB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin div)

250− (2, LB64UDiv) total,

250+ (2, LB64UDiv) partial,

251251 Prim (UN "prim__sdivB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin s64div)

252− (2, LB64SDiv) total,

252+ (2, LB64SDiv) partial,

253253 Prim (UN "prim__uremB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin rem)

254− (2, LB64URem) total,

254+ (2, LB64URem) partial,

255255 Prim (UN "prim__sremB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin s64rem)

256− (2, LB64SRem) total,

256+ (2, LB64SRem) partial,

257257 Prim (UN "prim__shlB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> shiftL x (fromIntegral y)))

258258 (2, LB64Shl) total,

259259 Prim (UN "prim__lshrB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> shiftR x (fromIntegral y)))