git.iko.soy/Idris-dev
on master help sign in
Moved `abs` from the `Neg` interface into its own `Abs` interface. (Issue 3500)
2a6dce9Niriel
CHANGELOG.md+2
compare with master
unifiedsplit
@@ -55,6 +55,8 @@
55+ `Prelude.Doubles.atan2` is now implemented as a primitive instead of
55+ `Prelude.Doubles.atan2` is now implemented as a primitive instead of
56 being coded in Idris.
56 being coded in Idris.
57+ Added `Test.Unit` to `contrib` for simple unit testing.
57+ Added `Test.Unit` to `contrib` for simple unit testing.
58++ Moved `abs` from the `Neg` interface into its own `Abs` interface. `Nat`
59+ implements `Abs` with `abs = id`.
58
60
59## Tool Updates
61## Tool Updates
60
62
libs/base/Data/Complex.idr+5−10
@@ -70,16 +70,11 @@ implementation Neg a => Num (Complex a) where
70 (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))
70 (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))
71 fromInteger x = (fromInteger x:+0)
71 fromInteger x = (fromInteger x:+0)
72
72
73−-- We can't do "implementation Neg a => Neg (Complex a)" because
73+implementation Neg a => Neg (Complex a) where
74−-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Double
75−implementation Neg (Complex Double) where
76 negate = map negate
74 negate = map negate
77 (-) (a:+b) (c:+d) = ((a-c):+(b-d))
75 (-) (a:+b) (c:+d) = ((a-c):+(b-d))
78− abs (a:+b) = (magnitude (a:+b):+0)
79−
80−-- As soon as abs moves out of Neg (issue #3500), the following would become a
81−-- valid instance:
82
76
77+-- Specific to Double because `abs` needs `magnitude` which needs `sqrt` which
78+-- operates on Double.
83−-- implementation Neg a => Neg (Complex a) where
79+implementation Abs (Complex Double) where
84−-- negate = map negate
80+ abs (a:+b) = (magnitude (a:+b):+0)
85−-- (-) (a:+b) (c:+d) = ((a-c):+(b-d))
libs/contrib/Data/Matrix/Numeric.idr+3−1
@@ -30,9 +30,11 @@ implementation Num a => Num (Vect n a) where
30
30
31implementation Neg a => Neg (Vect n a) where
31implementation Neg a => Neg (Vect n a) where
32 (-) = zipWith (-)
32 (-) = zipWith (-)
33− abs = map abs
34 negate = map negate
33 negate = map negate
35
34
35+implementation Abs a => Abs (Vect n a) where
36+ abs = map abs
37+
36-----------------------------------------------------------------------
38-----------------------------------------------------------------------
37-- Vector functions
39-- Vector functions
38-----------------------------------------------------------------------
40-----------------------------------------------------------------------
libs/contrib/Data/ZZ.idr+3−1
@@ -77,6 +77,9 @@ implementation Num ZZ where
77 (*) = multZ
77 (*) = multZ
78 fromInteger = fromInt
78 fromInteger = fromInt
79
79
80+implementation Abs ZZ where
81+ abs = cast . absZ
82+
80mutual
83mutual
81 implementation Neg ZZ where
84 implementation Neg ZZ where
82 negate (Pos Z) = Pos Z
85 negate (Pos Z) = Pos Z
@@ -84,7 +87,6 @@ mutual
84 negate (NegS n) = Pos (S n)
87 negate (NegS n) = Pos (S n)
85
88
86 (-) = subZ
89 (-) = subZ
87− abs = cast . absZ
88
90
89 ||| Subtract two `ZZ`s. Consider using `(-) {a=ZZ}`.
91 ||| Subtract two `ZZ`s. Consider using `(-) {a=ZZ}`.
90 subZ : ZZ -> ZZ -> ZZ
92 subZ : ZZ -> ZZ -> ZZ
libs/prelude/Prelude/Interfaces.idr+15−4
@@ -203,22 +203,33 @@ interface Num ty => Neg ty where
203 ||| The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.
203 ||| The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.
204 negate : ty -> ty
204 negate : ty -> ty
205 (-) : ty -> ty -> ty
205 (-) : ty -> ty -> ty
206− ||| Absolute value
206+
207− abs : ty -> ty
208
207
209Neg Integer where
208Neg Integer where
210 negate x = prim__subBigInt 0 x
209 negate x = prim__subBigInt 0 x
211 (-) = prim__subBigInt
210 (-) = prim__subBigInt
212− abs x = if x < 0 then -x else x
213
211
214Neg Int where
212Neg Int where
215 negate x = prim__subInt 0 x
213 negate x = prim__subInt 0 x
216 (-) = prim__subInt
214 (-) = prim__subInt
217− abs x = if x < (prim__truncBigInt_Int 0) then -x else x
218
215
219Neg Double where
216Neg Double where
220 negate x = prim__negFloat x
217 negate x = prim__negFloat x
221 (-) = prim__subFloat
218 (-) = prim__subFloat
219+
220+-- ---------------------------------------------------- [ Absolute Value Interface ]
221+||| Numbers for which the absolute value is defined should implement `Abs`.
222+interface Num ty => Abs ty where
223+ ||| Absolute value
224+ abs : ty -> ty
225+
226+Abs Integer where
227+ abs x = if x < 0 then -x else x
228+
229+Abs Int where
230+ abs x = if x < (prim__truncBigInt_Int 0) then -x else x
231+
232+Abs Double where
222 abs x = if x < (prim__toFloatBigInt 0) then -x else x
233 abs x = if x < (prim__toFloatBigInt 0) then -x else x
223
234
224-- ------------------------------------------------------------
235-- ------------------------------------------------------------
libs/prelude/Prelude/Nat.idr+5−2
@@ -25,9 +25,9 @@ import Prelude.Uninhabited
25
25
26Uninhabited (Z = S n) where
26Uninhabited (Z = S n) where
27 uninhabited Refl impossible
27 uninhabited Refl impossible
28−
28+
29Uninhabited (S n = Z) where
29Uninhabited (S n = Z) where
30− uninhabited Refl impossible
30+ uninhabited Refl impossible
31
31
32--------------------------------------------------------------------------------
32--------------------------------------------------------------------------------
33-- Syntactic tests
33-- Syntactic tests
@@ -244,6 +244,9 @@ Num Nat where
244
244
245 fromInteger = fromIntegerNat
245 fromInteger = fromIntegerNat
246
246
247+Abs Nat where
248+ abs = id
249+
247MinBound Nat where
250MinBound Nat where
248 minBound = Z
251 minBound = Z
249
252