git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4196 from Niriel/issue_3500

Moved `abs` from the `Neg` interface into its own `Abs` interface.

commit21ab196bcbe4ea0209142bcb7b3994172c91d450 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateWed 15 Nov 2017, 19:56 (9 years ago) parenta92f2f8cc1c4ed
6 files changed+33−18
compare with master
unifiedsplit
CHANGELOG.md+2 libs/base/Data/Complex.idr+5−10 libs/contrib/Data/Matrix/Numeric.idr+3−1 libs/contrib/Data/ZZ.idr+3−1 libs/prelude/Prelude/Interfaces.idr+15−4 libs/prelude/Prelude/Nat.idr+5−2
CHANGELOG.md+2
@@ -56,6 +56,8 @@
5656 being coded in Idris.
5757+ Added `Test.Unit` to `contrib` for simple unit testing.
5858+ Removed several deprecated items from the libraries shipped with Idris.
59++ Moved `abs` from the `Neg` interface into its own `Abs` interface. `Nat`
60+ implements `Abs` with `abs = id`.
5961
6062## Tool Updates
6163
libs/base/Data/Complex.idr+5−10
@@ -70,16 +70,11 @@ implementation Neg a => Num (Complex a) where
7070 (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))
7171 fromInteger x = (fromInteger x:+0)
7272
73−-- We can't do "implementation Neg a => Neg (Complex a)" because
74−-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Double
75−implementation Neg (Complex Double) where
73+implementation Neg a => Neg (Complex a) where
7674 negate = map negate
7775 (-) (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:
8276
83−-- implementation Neg a => Neg (Complex a) where
84−-- negate = map negate
85−-- (-) (a:+b) (c:+d) = ((a-c):+(b-d))
77+-- Specific to Double because `abs` needs `magnitude` which needs `sqrt` which
78+-- operates on Double.
79+implementation Abs (Complex Double) where
80+ abs (a:+b) = (magnitude (a:+b):+0)
libs/contrib/Data/Matrix/Numeric.idr+3−1
@@ -30,9 +30,11 @@ implementation Num a => Num (Vect n a) where
3030
3131implementation Neg a => Neg (Vect n a) where
3232 (-) = zipWith (-)
33− abs = map abs
3433 negate = map negate
3534
35+implementation Abs a => Abs (Vect n a) where
36+ abs = map abs
37+
3638-----------------------------------------------------------------------
3739-- Vector functions
3840-----------------------------------------------------------------------
libs/contrib/Data/ZZ.idr+3−1
@@ -77,6 +77,9 @@ implementation Num ZZ where
7777 (*) = multZ
7878 fromInteger = fromInt
7979
80+implementation Abs ZZ where
81+ abs = cast . absZ
82+
8083mutual
8184 implementation Neg ZZ where
8285 negate (Pos Z) = Pos Z
@@ -84,7 +87,6 @@ mutual
8487 negate (NegS n) = Pos (S n)
8588
8689 (-) = subZ
87− abs = cast . absZ
8890
8991 ||| Subtract two `ZZ`s. Consider using `(-) {a=ZZ}`.
9092 subZ : ZZ -> ZZ -> ZZ
libs/prelude/Prelude/Interfaces.idr+15−4
@@ -203,22 +203,33 @@ interface Num ty => Neg ty where
203203 ||| The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.
204204 negate : ty -> ty
205205 (-) : ty -> ty -> ty
206− ||| Absolute value
207− abs : ty -> ty
206+
208207
209208Neg Integer where
210209 negate x = prim__subBigInt 0 x
211210 (-) = prim__subBigInt
212− abs x = if x < 0 then -x else x
213211
214212Neg Int where
215213 negate x = prim__subInt 0 x
216214 (-) = prim__subInt
217− abs x = if x < (prim__truncBigInt_Int 0) then -x else x
218215
219216Neg Double where
220217 negate x = prim__negFloat x
221218 (-) = 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
222233 abs x = if x < (prim__toFloatBigInt 0) then -x else x
223234
224235-- ------------------------------------------------------------
libs/prelude/Prelude/Nat.idr+5−2
@@ -25,9 +25,9 @@ import Prelude.Uninhabited
2525
2626Uninhabited (Z = S n) where
2727 uninhabited Refl impossible
28−
28+
2929Uninhabited (S n = Z) where
30− uninhabited Refl impossible
30+ uninhabited Refl impossible
3131
3232--------------------------------------------------------------------------------
3333-- Syntactic tests
@@ -244,6 +244,9 @@ Num Nat where
244244
245245 fromInteger = fromIntegerNat
246246
247+Abs Nat where
248+ abs = id
249+
247250MinBound Nat where
248251 minBound = Z
249252