git.iko.soy/Idris-dev
on master help sign in
Partial support for Integral Classes.
ed8d233Jan de Muijnck-Hughes
libs/prelude/Prelude/Classes.idr+82−10
compare with master
unifiedsplit
@@ -11,7 +11,7 @@ infixl 7 <<, >>
11infixl 8 +,-
11infixl 8 +,-
12infixl 9 *,/
12infixl 9 *,/
13
13
14−-- ------------------------------------------------------- [ Numeric Operators ]
14+-- ------------------------------------------------------------- [ Boolean Ops ]
15intToBool : Int -> Bool
15intToBool : Int -> Bool
16intToBool 0 = False
16intToBool 0 = False
17intToBool x = True
17intToBool x = True
@@ -19,6 +19,7 @@ intToBool x = True
19boolOp : (a -> a -> Int) -> a -> a -> Bool
19boolOp : (a -> a -> Int) -> a -> a -> Bool
20boolOp op x y = intToBool (op x y)
20boolOp op x y = intToBool (op x y)
21
21
22+-- ---------------------------------------------------------- [ Equality Class ]
22-- | The Eq class defines inequality and equality.
23-- | The Eq class defines inequality and equality.
23class Eq a where
24class Eq a where
24 (==) : a -> a -> Bool
25 (==) : a -> a -> Bool
@@ -47,11 +48,12 @@ instance Eq Bool where
47 True == False = False
48 True == False = False
48 False == True = False
49 False == True = False
49 False == False = True
50 False == False = True
50−
51+
51instance (Eq a, Eq b) => Eq (a, b) where
52instance (Eq a, Eq b) => Eq (a, b) where
52 (==) (a, c) (b, d) = (a == b) && (c == d)
53 (==) (a, c) (b, d) = (a == b) && (c == d)
53
54
54
55
56+-- ---------------------------------------------------------- [ Ordering Class ]
55data Ordering = LT | EQ | GT
57data Ordering = LT | EQ | GT
56
58
57instance Eq Ordering where
59instance Eq Ordering where
@@ -123,6 +125,7 @@ instance (Ord a, Ord b) => Ord (a, b) where
123 then compare xl yl
125 then compare xl yl
124 else compare xr yr
126 else compare xr yr
125
127
128+-- --------------------------------------------------------- [ Numerical Class ]
126-- | The Num class defines basic numerical arithmetic.
129-- | The Num class defines basic numerical arithmetic.
127class Num a where
130class Num a where
128 (+) : a -> a -> a
131 (+) : a -> a -> a
@@ -234,17 +237,86 @@ instance Ord Bits64 where
234 else if l > r then GT
237 else if l > r then GT
235 else EQ
238 else EQ
236
239
237−-- | Integer division.
238−partial
239−div : Integer -> Integer -> Integer
240−div = prim__sdivBigInt
241
240
242−-- | Integer modulus.
241+-- ------------------------------------------------------------- [ Fractionals ]
243−partial
244−mod : Integer -> Integer -> Integer
245−mod = prim__sremBigInt
246
242
247-- | Fractional division of two Floats.
243-- | Fractional division of two Floats.
248(/) : Float -> Float -> Float
244(/) : Float -> Float -> Float
249(/) = prim__divFloat
245(/) = prim__divFloat
250
246
247+
248+-- --------------------------------------------------------------- [ Integrals ]
249+%default partial
250+
251+class Integral a where
252+ div : a -> a -> a
253+ mod : a -> a -> a
254+
255+-- ---------------------------------------------------------------- [ Integers ]
256+divBigInt : Integer -> Integer -> Integer
257+divBigInt = prim__sdivBigInt
258+
259+modBigInt : Integer -> Integer -> Integer
260+modBigInt = prim__sremBigInt
261+
262+instance Integral Integer where
263+ div = divBigInt
264+ mod = modBigInt
265+
266+-- --------------------------------------------------------------------- [ Int ]
267+
268+divInt : Int -> Int -> Int
269+divInt = prim__sdivInt
270+
271+modInt : Int -> Int -> Int
272+modInt = prim__sremInt
273+
274+instance Integral Int where
275+ div = divInt
276+ mod = modInt
277+
278+-- ------------------------------------------------------------------- [ Bits8 ]
279+divB8 : Bits8 -> Bits8 -> Bits8
280+divB8 = prim__sdivB8
281+
282+modB8 : Bits8 -> Bits8 -> Bits8
283+modB8 = prim__sremB8
284+
285+instance Integral Bits8 where
286+ div = divB8
287+ mod = modB8
288+
289+-- ------------------------------------------------------------------ [ Bits16 ]
290+divB16 : Bits16 -> Bits16 -> Bits16
291+divB16 = prim__sdivB16
292+
293+modB16 : Bits16 -> Bits16 -> Bits16
294+modB16 = prim__sremB16
295+
296+instance Integral Bits16 where
297+ div = divB16
298+ mod = modB16
299+
300+-- ------------------------------------------------------------------ [ Bits32 ]
301+divB32 : Bits32 -> Bits32 -> Bits32
302+divB32 = prim__sdivB32
303+
304+modB32 : Bits32 -> Bits32 -> Bits32
305+modB32 = prim__sremB32
306+
307+instance Integral Bits32 where
308+ div = divB32
309+ mod = modB32
310+
311+-- ------------------------------------------------------------------ [ Bits64 ]
312+divB64 : Bits64 -> Bits64 -> Bits64
313+divB64 = prim__sdivB64
314+
315+modB64 : Bits64 -> Bits64 -> Bits64
316+modB64 = prim__sremB64
317+
318+instance Integral Bits64 where
319+ div = divB64
320+ mod = modB64
321+
322+
libs/prelude/Prelude/Nat.idr+15−9
@@ -227,9 +227,10 @@ fact (S n) = (S n) * fact n
227-- Division and modulus
227-- Division and modulus
228--------------------------------------------------------------------------------
228--------------------------------------------------------------------------------
229
229
230+total
230−total mod : Nat -> Nat -> Nat
231+modNat : Nat -> Nat -> Nat
231−mod left Z = left
232+modNat left Z = left
232−mod left (S right) = mod' left left right
233+modNat left (S right) = mod' left left right
233 where
234 where
234 total mod' : Nat -> Nat -> Nat -> Nat
235 total mod' : Nat -> Nat -> Nat -> Nat
235 mod' Z centre right = centre
236 mod' Z centre right = centre
@@ -239,9 +240,10 @@ mod left (S right) = mod' left left right
239 else
240 else
240 mod' left (centre - (S right)) right
241 mod' left (centre - (S right)) right
241
242
243+total
242−total div : Nat -> Nat -> Nat
244+divNat : Nat -> Nat -> Nat
243−div left Z = S left -- div by zero
245+divNat left Z = S left -- div by zero
244−div left (S right) = div' left left right
246+divNat left (S right) = div' left left right
245 where
247 where
246 total div' : Nat -> Nat -> Nat -> Nat
248 total div' : Nat -> Nat -> Nat -> Nat
247 div' Z centre right = Z
249 div' Z centre right = Z
@@ -251,11 +253,15 @@ div left (S right) = div' left left right
251 else
253 else
252 S (div' left (centre - (S right)) right)
254 S (div' left (centre - (S right)) right)
253
255
256+instance Integral Nat where
257+ div = divNat
258+ mod = modNat
259+
254%assert_total
260%assert_total
255log2 : Nat -> Nat
261log2 : Nat -> Nat
256log2 Z = Z
262log2 Z = Z
257log2 (S Z) = Z
263log2 (S Z) = Z
258−log2 n = S (log2 (n `div` 2))
264+log2 n = S (log2 (n `divNat` 2))
259
265
260--------------------------------------------------------------------------------
266--------------------------------------------------------------------------------
261-- GCD and LCM
267-- GCD and LCM
@@ -263,12 +269,12 @@ log2 n = S (log2 (n `div` 2))
263%assert_total
269%assert_total
264gcd : Nat -> Nat -> Nat
270gcd : Nat -> Nat -> Nat
265gcd a Z = a
271gcd a Z = a
266−gcd a b = gcd b (a `mod` b)
272+gcd a b = gcd b (a `modNat` b)
267
273
268total lcm : Nat -> Nat -> Nat
274total lcm : Nat -> Nat -> Nat
269lcm _ Z = Z
275lcm _ Z = Z
270lcm Z _ = Z
276lcm Z _ = Z
271−lcm x y = div (x * y) (gcd x y)
277+lcm x y = divNat (x * y) (gcd x y)
272
278
273--------------------------------------------------------------------------------
279--------------------------------------------------------------------------------
274-- Properties
280-- Properties