git.iko.soy/Idris-dev
on master help sign in
Mark bit divisions/remainders as partial
45bbe39Benjamin Saunders
lib/Prelude/Bits.idr+8
compare with master
unifiedsplit
@@ -163,6 +163,7 @@ public
163bitsMul : Bits n -> Bits n -> Bits n
163bitsMul : Bits n -> Bits n -> Bits n
164bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)
164bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)
165
165
166+partial
166bitsSDiv' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
167bitsSDiv' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
167bitsSDiv' {n=n} x y with (nextBits n)
168bitsSDiv' {n=n} x y with (nextBits n)
168 | Bits8 = prim__sdivB8 x y
169 | Bits8 = prim__sdivB8 x y
@@ -171,9 +172,11 @@ bitsSDiv' {n=n} x y with (nextBits n)
171 | Bits64 = prim__sdivB64 x y
172 | Bits64 = prim__sdivB64 x y
172
173
173public
174public
175+partial
174bitsSDiv : Bits n -> Bits n -> Bits n
176bitsSDiv : Bits n -> Bits n -> Bits n
175bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)
177bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)
176
178
179+partial
177bitsUDiv' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
180bitsUDiv' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
178bitsUDiv' {n=n} x y with (nextBits n)
181bitsUDiv' {n=n} x y with (nextBits n)
179 | Bits8 = prim__udivB8 x y
182 | Bits8 = prim__udivB8 x y
@@ -182,9 +185,11 @@ bitsUDiv' {n=n} x y with (nextBits n)
182 | Bits64 = prim__udivB64 x y
185 | Bits64 = prim__udivB64 x y
183
186
184public
187public
188+partial
185bitsUDiv : Bits n -> Bits n -> Bits n
189bitsUDiv : Bits n -> Bits n -> Bits n
186bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)
190bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)
187
191
192+partial
188bitsSRem' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
193bitsSRem' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
189bitsSRem' {n=n} x y with (nextBits n)
194bitsSRem' {n=n} x y with (nextBits n)
190 | Bits8 = prim__sremB8 x y
195 | Bits8 = prim__sremB8 x y
@@ -193,9 +198,11 @@ bitsSRem' {n=n} x y with (nextBits n)
193 | Bits64 = prim__sremB64 x y
198 | Bits64 = prim__sremB64 x y
194
199
195public
200public
201+partial
196bitsSRem : Bits n -> Bits n -> Bits n
202bitsSRem : Bits n -> Bits n -> Bits n
197bitsSRem (MkBits x) (MkBits y) = MkBits (bitsSRem' x y)
203bitsSRem (MkBits x) (MkBits y) = MkBits (bitsSRem' x y)
198
204
205+partial
199bitsURem' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
206bitsURem' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
200bitsURem' {n=n} x y with (nextBits n)
207bitsURem' {n=n} x y with (nextBits n)
201 | Bits8 = prim__uremB8 x y
208 | Bits8 = prim__uremB8 x y
@@ -204,6 +211,7 @@ bitsURem' {n=n} x y with (nextBits n)
204 | Bits64 = prim__uremB64 x y
211 | Bits64 = prim__uremB64 x y
205
212
206public
213public
214+partial
207bitsURem : Bits n -> Bits n -> Bits n
215bitsURem : Bits n -> Bits n -> Bits n
208bitsURem (MkBits x) (MkBits y) = MkBits (bitsURem' x y)
216bitsURem (MkBits x) (MkBits y) = MkBits (bitsURem' x y)
209
217
src/Idris/Primitives.hs+16−16
@@ -94,13 +94,13 @@ primitives =
94 Prim (UN "prim__mulB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (*))
94 Prim (UN "prim__mulB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (*))
95 (2, LB8Times) total,
95 (2, LB8Times) total,
96 Prim (UN "prim__udivB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin div)
96 Prim (UN "prim__udivB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin div)
97− (2, LB8UDiv) total,
97+ (2, LB8UDiv) partial,
98 Prim (UN "prim__sdivB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin s8div)
98 Prim (UN "prim__sdivB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin s8div)
99− (2, LB8SDiv) total,
99+ (2, LB8SDiv) partial,
100 Prim (UN "prim__uremB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin rem)
100 Prim (UN "prim__uremB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin rem)
101− (2, LB8URem) total,
101+ (2, LB8URem) partial,
102 Prim (UN "prim__sremB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin s8rem)
102 Prim (UN "prim__sremB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin s8rem)
103− (2, LB8SRem) total,
103+ (2, LB8SRem) partial,
104 Prim (UN "prim__shlB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> shiftL x (fromIntegral y)))
104 Prim (UN "prim__shlB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> shiftL x (fromIntegral y)))
105 (2, LB8Shl) total,
105 (2, LB8Shl) total,
106 Prim (UN "prim__lshrB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> shiftR x (fromIntegral y)))
106 Prim (UN "prim__lshrB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> shiftR x (fromIntegral y)))
@@ -147,13 +147,13 @@ primitives =
147 Prim (UN "prim__mulB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (*))
147 Prim (UN "prim__mulB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (*))
148 (2, LB16Times) total,
148 (2, LB16Times) total,
149 Prim (UN "prim__udivB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin div)
149 Prim (UN "prim__udivB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin div)
150− (2, LB16UDiv) total,
150+ (2, LB16UDiv) partial,
151 Prim (UN "prim__sdivB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin s16div)
151 Prim (UN "prim__sdivB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin s16div)
152− (2, LB16SDiv) total,
152+ (2, LB16SDiv) partial,
153 Prim (UN "prim__uremB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin rem)
153 Prim (UN "prim__uremB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin rem)
154− (2, LB16URem) total,
154+ (2, LB16URem) partial,
155 Prim (UN "prim__sremB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin s16rem)
155 Prim (UN "prim__sremB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin s16rem)
156− (2, LB16SRem) total,
156+ (2, LB16SRem) partial,
157 Prim (UN "prim__shlB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> shiftL x (fromIntegral y)))
157 Prim (UN "prim__shlB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> shiftL x (fromIntegral y)))
158 (2, LB16Shl) total,
158 (2, LB16Shl) total,
159 Prim (UN "prim__lshrB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> shiftR x (fromIntegral y)))
159 Prim (UN "prim__lshrB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> shiftR x (fromIntegral y)))
@@ -198,13 +198,13 @@ primitives =
198 Prim (UN "prim__mulB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (*))
198 Prim (UN "prim__mulB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (*))
199 (2, LB32Times) total,
199 (2, LB32Times) total,
200 Prim (UN "prim__udivB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin div)
200 Prim (UN "prim__udivB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin div)
201− (2, LB32UDiv) total,
201+ (2, LB32UDiv) partial,
202 Prim (UN "prim__sdivB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin s32div)
202 Prim (UN "prim__sdivB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin s32div)
203− (2, LB32SDiv) total,
203+ (2, LB32SDiv) partial,
204 Prim (UN "prim__uremB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin rem)
204 Prim (UN "prim__uremB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin rem)
205− (2, LB32URem) total,
205+ (2, LB32URem) partial,
206 Prim (UN "prim__sremB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin s32rem)
206 Prim (UN "prim__sremB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin s32rem)
207− (2, LB32SRem) total,
207+ (2, LB32SRem) partial,
208 Prim (UN "prim__shlB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> shiftL x (fromIntegral y)))
208 Prim (UN "prim__shlB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> shiftL x (fromIntegral y)))
209 (2, LB32Shl) total,
209 (2, LB32Shl) total,
210 Prim (UN "prim__lshrB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> shiftR x (fromIntegral y)))
210 Prim (UN "prim__lshrB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> shiftR x (fromIntegral y)))
@@ -247,13 +247,13 @@ primitives =
247 Prim (UN "prim__mulB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (*))
247 Prim (UN "prim__mulB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (*))
248 (2, LB64Times) total,
248 (2, LB64Times) total,
249 Prim (UN "prim__udivB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin div)
249 Prim (UN "prim__udivB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin div)
250− (2, LB64UDiv) total,
250+ (2, LB64UDiv) partial,
251 Prim (UN "prim__sdivB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin s64div)
251 Prim (UN "prim__sdivB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin s64div)
252− (2, LB64SDiv) total,
252+ (2, LB64SDiv) partial,
253 Prim (UN "prim__uremB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin rem)
253 Prim (UN "prim__uremB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin rem)
254− (2, LB64URem) total,
254+ (2, LB64URem) partial,
255 Prim (UN "prim__sremB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin s64rem)
255 Prim (UN "prim__sremB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin s64rem)
256− (2, LB64SRem) total,
256+ (2, LB64SRem) partial,
257 Prim (UN "prim__shlB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> shiftL x (fromIntegral y)))
257 Prim (UN "prim__shlB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> shiftL x (fromIntegral y)))
258 (2, LB64Shl) total,
258 (2, LB64Shl) total,
259 Prim (UN "prim__lshrB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> shiftR x (fromIntegral y)))
259 Prim (UN "prim__lshrB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> shiftR x (fromIntegral y)))