git.iko.soy/Idris-dev
on master help sign in
Neg and Nat adjustments
f7ccfb3Edwin Brady
CHANGELOG+5−1
compare with master
unifiedsplit
@@ -9,7 +9,11 @@ Language updates
9Library updates
9Library updates
10---------------
10---------------
11
11
12−[None so far]
12+* The 'Neg' class now represents numeric types which can be negative. As
13+such, the (-) operator and 'abs' have been moved there from 'Num'.
14+* A special version of (-) on 'Nat' requires that the second argument is
15+smaller than or equal to the first. 'minus' retains the old behaviour,
16+returning Z if there is an underflow.
13
17
14Tool updates
18Tool updates
15------------
19------------
libs/base/Data/Bits.idr+1−1
@@ -42,7 +42,7 @@ natToBits {n=n} x with (n)
42 | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x
42 | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x
43
43
44getPad : Nat -> machineTy n
44getPad : Nat -> machineTy n
45−getPad n = natToBits ((bitsUsed (nextBytes n)) - n)
45+getPad n = natToBits (minus (bitsUsed (nextBytes n)) n)
46
46
47public
47public
48data Bits : Nat -> Type where
48data Bits : Nat -> Type where
libs/base/Data/Complex.idr+7−6
@@ -57,20 +57,21 @@ phase (x:+y) = atan2 y x
57
57
58------------------------------ Conjugate
58------------------------------ Conjugate
59
59
60−conjugate : Num a => Complex a -> Complex a
60+conjugate : Neg a => Complex a -> Complex a
61conjugate (r:+i) = (r :+ (0-i))
61conjugate (r:+i) = (r :+ (0-i))
62
62
63instance Functor Complex where
63instance Functor Complex where
64− map f (r :+ i) = f r :+ f i
64+ map f (r :+ i) = f r :+ f i
65−
66−instance Neg a => Neg (Complex a) where
67− negate = map negate
68
65
69-- We can't do "instance Num a => Num (Complex a)" because
66-- We can't do "instance Num a => Num (Complex a)" because
70-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Float
67-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Float
71instance Num (Complex Float) where
68instance Num (Complex Float) where
72 (+) (a:+b) (c:+d) = ((a+c):+(b+d))
69 (+) (a:+b) (c:+d) = ((a+c):+(b+d))
73− (-) (a:+b) (c:+d) = ((a-c):+(b-d))
74 (*) (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))
75 fromInteger x = (fromInteger x:+0)
71 fromInteger x = (fromInteger x:+0)
72+
73+instance Neg (Complex Float) where
74+ negate = map negate
75+ (-) (a:+b) (c:+d) = ((a-c):+(b-d))
76 abs (a:+b) = (magnitude (a:+b):+0)
76 abs (a:+b) = (magnitude (a:+b):+0)
77+
libs/base/Data/Mod2.idr−2
@@ -40,9 +40,7 @@ instance Ord (Mod2 n) where
40
40
41instance Num (Mod2 n) where
41instance Num (Mod2 n) where
42 (+) = modBin plus
42 (+) = modBin plus
43− (-) = modBin minus
44 (*) = modBin times
43 (*) = modBin times
45− abs = id
46 fromInteger = intToMod
44 fromInteger = intToMod
47
45
48instance Cast (Mod2 n) (Bits n) where
46instance Cast (Mod2 n) (Bits n) where
libs/contrib/Data/Matrix/Numeric.idr+9−6
@@ -24,11 +24,14 @@ infixr 7 <&> -- matrix tensor product
24
24
25instance Num a => Num (Vect n a) where
25instance Num a => Num (Vect n a) where
26 (+) = zipWith (+)
26 (+) = zipWith (+)
27− (-) = zipWith (+)
28 (*) = zipWith (*)
27 (*) = zipWith (*)
29− abs = id
30 fromInteger n = replicate _ (fromInteger n)
28 fromInteger n = replicate _ (fromInteger n)
31
29
30+instance Neg a => Neg (Vect n a) where
31+ (-) = zipWith (-)
32+ abs = map abs
33+ negate = map negate
34+
32-----------------------------------------------------------------------
35-----------------------------------------------------------------------
33-- Vector functions
36-- Vector functions
34-----------------------------------------------------------------------
37-----------------------------------------------------------------------
@@ -88,7 +91,7 @@ basis i = replaceAt i 1 0
88(><) x y = col x <> row y
91(><) x y = col x <> row y
89
92
90||| Matrix commutator
93||| Matrix commutator
91−(<<>>) : Num a => Matrix n n a -> Matrix n n a -> Matrix n n a
94+(<<>>) : Neg a => Matrix n n a -> Matrix n n a -> Matrix n n a
92(<<>>) m1 m2 = (m1 <> m2) - (m2 <> m1)
95(<<>>) m1 m2 = (m1 <> m2) - (m2 <> m1)
93
96
94||| Matrix anti-commutator
97||| Matrix anti-commutator
@@ -112,17 +115,17 @@ blockDiag {n} {m} g h = map (++ replicate m 0) g ++ map ((replicate n 0) ++) h
112-----------------------------------------------------------------------
115-----------------------------------------------------------------------
113
116
114||| Alternating sum
117||| Alternating sum
115−altSum : Num a => Vect n a -> a
118+altSum : Neg a => Vect n a -> a
116altSum (x::y::zs) = (x - y) + altSum zs
119altSum (x::y::zs) = (x - y) + altSum zs
117altSum [x] = x
120altSum [x] = x
118altSum [] = 0
121altSum [] = 0
119
122
120||| Determinant of a 2-by-2 matrix
123||| Determinant of a 2-by-2 matrix
121−det2 : Num a => Matrix 2 2 a -> a
124+det2 : Neg a => Matrix 2 2 a -> a
122det2 [[x1,x2],[y1,y2]] = x1*y2 - x2*y1
125det2 [[x1,x2],[y1,y2]] = x1*y2 - x2*y1
123
126
124||| Determinant of a square matrix
127||| Determinant of a square matrix
125−det : Num a => Matrix (S (S n)) (S (S n)) a -> a
128+det : Neg a => Matrix (S (S n)) (S (S n)) a -> a
126det {n} m = case n of
129det {n} m = case n of
127 Z => det2 m
130 Z => det2 m
128 (S k) => altSum . map (\c => indices FZ c m * det (subMatrix FZ c m))
131 (S k) => altSum . map (\c => indices FZ c m * det (subMatrix FZ c m))
libs/contrib/Data/Nat/DivMod/IteratedSubtraction.idr+1−1
@@ -47,7 +47,7 @@ ltToLTE LTSucc = lteRefl
47ltToLTE (LTStep lt) = lteSuccRight $ ltToLTE lt
47ltToLTE (LTStep lt) = lteSuccRight $ ltToLTE lt
48
48
49||| Subtraction gives a result that is actually smaller.
49||| Subtraction gives a result that is actually smaller.
50−minusLT' : (x,y : Nat) -> x - y `LT'` S x
50+minusLT' : (x,y : Nat) -> minus x y `LT'` S x
51minusLT' Z y = LTSucc
51minusLT' Z y = LTSucc
52minusLT' (S k) Z = LTSucc
52minusLT' (S k) Z = LTSucc
53minusLT' (S k) (S j) = LTStep (minusLT' k j)
53minusLT' (S k) (S j) = LTStep (minusLT' k j)
libs/contrib/Data/ZZ.idr+14−11
@@ -28,11 +28,6 @@ instance Show ZZ where
28 show (Pos n) = show n
28 show (Pos n) = show n
29 show (NegS n) = "-" ++ show (S n)
29 show (NegS n) = "-" ++ show (S n)
30
30
31−instance Neg ZZ where
32− negate (Pos Z) = Pos Z
33− negate (Pos (S n)) = NegS n
34− negate (NegS n) = Pos (S n)
35−
36negNat : Nat -> ZZ
31negNat : Nat -> ZZ
37negNat Z = Pos Z
32negNat Z = Pos Z
38negNat (S n) = NegS n
33negNat (S n) = NegS n
@@ -51,10 +46,6 @@ plusZ (NegS n) (NegS m) = NegS (S (n + m))
51plusZ (Pos n) (NegS m) = minusNatZ n (S m)
46plusZ (Pos n) (NegS m) = minusNatZ n (S m)
52plusZ (NegS n) (Pos m) = minusNatZ m (S n)
47plusZ (NegS n) (Pos m) = minusNatZ m (S n)
53
48
54−||| Subtract two `ZZ`s. Consider using `(-) {a=ZZ}`.
55−subZ : ZZ -> ZZ -> ZZ
56−subZ n m = plusZ n (negate m)
57−
58instance Eq ZZ where
49instance Eq ZZ where
59 (Pos n) == (Pos m) = n == m
50 (Pos n) == (Pos m) = n == m
60 (NegS n) == (NegS m) = n == m
51 (NegS n) == (NegS m) = n == m
@@ -85,11 +76,23 @@ instance Cast Nat ZZ where
85
76
86instance Num ZZ where
77instance Num ZZ where
87 (+) = plusZ
78 (+) = plusZ
88− (-) = subZ
89 (*) = multZ
79 (*) = multZ
90− abs = cast . absZ
91 fromInteger = fromInt
80 fromInteger = fromInt
92
81
82+mutual
83+ instance Neg ZZ where
84+ negate (Pos Z) = Pos Z
85+ negate (Pos (S n)) = NegS n
86+ negate (NegS n) = Pos (S n)
87+
88+ (-) = subZ
89+ abs = cast . absZ
90+
91+ ||| Subtract two `ZZ`s. Consider using `(-) {a=ZZ}`.
92+ subZ : ZZ -> ZZ -> ZZ
93+ subZ n m = plusZ n (negate m)
94+
95+
93instance Cast ZZ Integer where
96instance Cast ZZ Integer where
94 cast (Pos n) = cast n
97 cast (Pos n) = cast n
95 cast (NegS n) = (-1) * (cast n + 1)
98 cast (NegS n) = (-1) * (cast n + 1)
libs/prelude/Prelude.idr+2−2
@@ -134,10 +134,10 @@ natRange n = List.reverse (go n)
134total natEnumFromThen : Nat -> Nat -> Stream Nat
134total natEnumFromThen : Nat -> Nat -> Stream Nat
135natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc
135natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc
136total natEnumFromTo : Nat -> Nat -> List Nat
136total natEnumFromTo : Nat -> Nat -> List Nat
137−natEnumFromTo n m = map (plus n) (natRange ((S m) - n))
137+natEnumFromTo n m = map (plus n) (natRange (minus (S m) n))
138total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
138total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
139natEnumFromThenTo _ Z _ = []
139natEnumFromThenTo _ Z _ = []
140−natEnumFromThenTo n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (m - n) (S inc) SIsNotZ)))
140+natEnumFromThenTo n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (minus m n) (S inc) SIsNotZ)))
141
141
142class Enum a where
142class Enum a where
143 total pred : a -> a
143 total pred : a -> a
libs/prelude/Prelude/Classes.idr+25−32
@@ -143,85 +143,78 @@ instance (Ord a, Ord b) => Ord (a, b) where
143 then compare xl yl
143 then compare xl yl
144 else compare xr yr
144 else compare xr yr
145
145
146−-- --------------------------------------------------------- [ Negatable Class ]
147−||| The `Neg` class defines unary negation (-).
148−class Neg a where
149− ||| The underlying implementation of unary minus. `-5` desugars to `negate (fromInteger 5)`.
150− negate : a -> a
151−
152−instance Neg Integer where
153− negate x = prim__subBigInt 0 x
154−
155−instance Neg Int where
156− negate x = prim__subInt 0 x
157−
158−instance Neg Float where
159− negate x = prim__negFloat x
160−
161-- --------------------------------------------------------- [ Numerical Class ]
146-- --------------------------------------------------------- [ Numerical Class ]
162||| The Num class defines basic numerical arithmetic.
147||| The Num class defines basic numerical arithmetic.
163class Num a where
148class Num a where
164 (+) : a -> a -> a
149 (+) : a -> a -> a
165− (-) : a -> a -> a
166 (*) : a -> a -> a
150 (*) : a -> a -> a
167− ||| Absolute value
168− abs : a -> a
169 ||| Conversion from Integer.
151 ||| Conversion from Integer.
170 fromInteger : Integer -> a
152 fromInteger : Integer -> a
171
153
172instance Num Integer where
154instance Num Integer where
173 (+) = prim__addBigInt
155 (+) = prim__addBigInt
174− (-) = prim__subBigInt
175 (*) = prim__mulBigInt
156 (*) = prim__mulBigInt
176
157
177− abs x = if x < 0 then -x else x
178 fromInteger = id
158 fromInteger = id
179
159
180instance Num Int where
160instance Num Int where
181 (+) = prim__addInt
161 (+) = prim__addInt
182− (-) = prim__subInt
183 (*) = prim__mulInt
162 (*) = prim__mulInt
184
163
185 fromInteger = prim__truncBigInt_Int
164 fromInteger = prim__truncBigInt_Int
186− abs x = if x < (prim__truncBigInt_Int 0) then -x else x
187
165
188
166
189instance Num Float where
167instance Num Float where
190 (+) = prim__addFloat
168 (+) = prim__addFloat
191− (-) = prim__subFloat
192 (*) = prim__mulFloat
169 (*) = prim__mulFloat
193
170
194− abs x = if x < (prim__toFloatBigInt 0) then -x else x
195 fromInteger = prim__toFloatBigInt
171 fromInteger = prim__toFloatBigInt
196
172
197instance Num Bits8 where
173instance Num Bits8 where
198 (+) = prim__addB8
174 (+) = prim__addB8
199− (-) = prim__subB8
200 (*) = prim__mulB8
175 (*) = prim__mulB8
201− abs = id
202 fromInteger = prim__truncBigInt_B8
176 fromInteger = prim__truncBigInt_B8
203
177
204instance Num Bits16 where
178instance Num Bits16 where
205 (+) = prim__addB16
179 (+) = prim__addB16
206− (-) = prim__subB16
207 (*) = prim__mulB16
180 (*) = prim__mulB16
208− abs = id
209 fromInteger = prim__truncBigInt_B16
181 fromInteger = prim__truncBigInt_B16
210
182
211instance Num Bits32 where
183instance Num Bits32 where
212 (+) = prim__addB32
184 (+) = prim__addB32
213− (-) = prim__subB32
214 (*) = prim__mulB32
185 (*) = prim__mulB32
215− abs = id
216 fromInteger = prim__truncBigInt_B32
186 fromInteger = prim__truncBigInt_B32
217
187
218instance Num Bits64 where
188instance Num Bits64 where
219 (+) = prim__addB64
189 (+) = prim__addB64
220− (-) = prim__subB64
221 (*) = prim__mulB64
190 (*) = prim__mulB64
222− abs = id
223 fromInteger = prim__truncBigInt_B64
191 fromInteger = prim__truncBigInt_B64
224
192
193+-- --------------------------------------------------------- [ Negatable Class ]
194+||| The `Neg` class defines operations on numbers which can be negative.
195+class Num a => Neg a where
196+ ||| The underlying implementation of unary minus. `-5` desugars to `negate (fromInteger 5)`.
197+ negate : a -> a
198+ (-) : a -> a -> a
199+ ||| Absolute value
200+ abs : a -> a
201+
202+instance Neg Integer where
203+ negate x = prim__subBigInt 0 x
204+ (-) = prim__subBigInt
205+ abs x = if x < 0 then -x else x
206+
207+instance Neg Int where
208+ negate x = prim__subInt 0 x
209+ (-) = prim__subInt
210+ abs x = if x < (prim__truncBigInt_Int 0) then -x else x
211+
212+instance Neg Float where
213+ negate x = prim__negFloat x
214+ (-) = prim__subFloat
215+ abs x = if x < (prim__toFloatBigInt 0) then -x else x
216+
217+-- ------------------------------------------------------------
225instance Eq Bits8 where
218instance Eq Bits8 where
226 x == y = intToBool (prim__eqB8 x y)
219 x == y = intToBool (prim__eqB8 x y)
227
220
libs/prelude/Prelude/Nat.idr+17−17
@@ -180,6 +180,9 @@ toIntNat n = toIntNat' n 0 where
180 toIntNat' Z x = x
180 toIntNat' Z x = x
181 toIntNat' (S n) x = toIntNat' n (x + 1)
181 toIntNat' (S n) x = toIntNat' n (x + 1)
182
182
183+(-) : (m : Nat) -> (n : Nat) -> {auto smaller : LTE n m} -> Nat
184+(-) m n {smaller} = minus m n
185+
183--------------------------------------------------------------------------------
186--------------------------------------------------------------------------------
184-- Type class instances
187-- Type class instances
185--------------------------------------------------------------------------------
188--------------------------------------------------------------------------------
@@ -200,11 +203,8 @@ instance Ord Nat where
200
203
201instance Num Nat where
204instance Num Nat where
202 (+) = plus
205 (+) = plus
203− (-) = minus
204 (*) = mult
206 (*) = mult
205
207
206− abs x = x
207−
208 fromInteger = fromIntegerNat
208 fromInteger = fromIntegerNat
209
209
210instance MinBound Nat where
210instance MinBound Nat where
@@ -307,7 +307,7 @@ modNatNZ left (S right) _ = mod' left left right
307 if lte centre right then
307 if lte centre right then
308 centre
308 centre
309 else
309 else
310− mod' left (centre - (S right)) right
310+ mod' left (minus centre (S right)) right
311
311
312partial
312partial
313modNat : Nat -> Nat -> Nat
313modNat : Nat -> Nat -> Nat
@@ -323,7 +323,7 @@ divNatNZ left (S right) _ = div' left left right
323 if lte centre right then
323 if lte centre right then
324 Z
324 Z
325 else
325 else
326− S (div' left (centre - (S right)) right)
326+ S (div' left (minus centre (S right)) right)
327
327
328partial
328partial
329divNat : Nat -> Nat -> Nat
329divNat : Nat -> Nat -> Nat
@@ -544,34 +544,34 @@ multOneRightNeutral (S left) =
544
544
545-- Minus
545-- Minus
546total minusSuccSucc : (left : Nat) -> (right : Nat) ->
546total minusSuccSucc : (left : Nat) -> (right : Nat) ->
547− (S left) - (S right) = left - right
547+ minus (S left) (S right) = minus left right
548minusSuccSucc left right = Refl
548minusSuccSucc left right = Refl
549
549
550−total minusZeroLeft : (right : Nat) -> 0 - right = Z
550+total minusZeroLeft : (right : Nat) -> minus 0 right = Z
551minusZeroLeft right = Refl
551minusZeroLeft right = Refl
552
552
553−total minusZeroRight : (left : Nat) -> left - 0 = left
553+total minusZeroRight : (left : Nat) -> minus left 0 = left
554minusZeroRight Z = Refl
554minusZeroRight Z = Refl
555minusZeroRight (S left) = Refl
555minusZeroRight (S left) = Refl
556
556
557−total minusZeroN : (n : Nat) -> Z = n - n
557+total minusZeroN : (n : Nat) -> Z = minus n n
558minusZeroN Z = Refl
558minusZeroN Z = Refl
559minusZeroN (S n) = minusZeroN n
559minusZeroN (S n) = minusZeroN n
560
560
561−total minusOneSuccN : (n : Nat) -> S Z = (S n) - n
561+total minusOneSuccN : (n : Nat) -> S Z = minus (S n) n
562minusOneSuccN Z = Refl
562minusOneSuccN Z = Refl
563minusOneSuccN (S n) = minusOneSuccN n
563minusOneSuccN (S n) = minusOneSuccN n
564
564
565−total minusSuccOne : (n : Nat) -> S n - 1 = n
565+total minusSuccOne : (n : Nat) -> minus (S n) 1 = n
566minusSuccOne Z = Refl
566minusSuccOne Z = Refl
567minusSuccOne (S n) = Refl
567minusSuccOne (S n) = Refl
568
568
569−total minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = Z
569+total minusPlusZero : (n : Nat) -> (m : Nat) -> minus n (n + m) = Z
570minusPlusZero Z m = Refl
570minusPlusZero Z m = Refl
571minusPlusZero (S n) m = minusPlusZero n m
571minusPlusZero (S n) m = minusPlusZero n m
572
572
573total minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
573total minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
574− left - centre - right = left - (centre + right)
574+ minus (minus left centre) right = minus left (centre + right)
575minusMinusMinusPlus Z Z right = Refl
575minusMinusMinusPlus Z Z right = Refl
576minusMinusMinusPlus (S left) Z right = Refl
576minusMinusMinusPlus (S left) Z right = Refl
577minusMinusMinusPlus Z (S centre) right = Refl
577minusMinusMinusPlus Z (S centre) right = Refl
@@ -581,7 +581,7 @@ minusMinusMinusPlus (S left) (S centre) right =
581 Refl
581 Refl
582
582
583total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
583total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
584− (left + right) - (left + right') = right - right'
584+ minus (left + right) (left + right') = minus right right'
585plusMinusLeftCancel Z right right' = Refl
585plusMinusLeftCancel Z right right' = Refl
586plusMinusLeftCancel (S left) right right' =
586plusMinusLeftCancel (S left) right right' =
587 let inductiveHypothesis = plusMinusLeftCancel left right right' in
587 let inductiveHypothesis = plusMinusLeftCancel left right right' in
@@ -589,7 +589,7 @@ plusMinusLeftCancel (S left) right right' =
589 Refl
589 Refl
590
590
591total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
591total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
592− (left - centre) * right = (left * right) - (centre * right)
592+ (minus left centre) * right = minus (left * right) (centre * right)
593multDistributesOverMinusLeft Z Z right = Refl
593multDistributesOverMinusLeft Z Z right = Refl
594multDistributesOverMinusLeft (S left) Z right =
594multDistributesOverMinusLeft (S left) Z right =
595 rewrite (minusZeroRight (plus right (mult left right))) in Refl
595 rewrite (minusZeroRight (plus right (mult left right))) in Refl
@@ -601,7 +601,7 @@ multDistributesOverMinusLeft (S left) (S centre) right =
601 Refl
601 Refl
602
602
603total multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
603total multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
604− left * (centre - right) = (left * centre) - (left * right)
604+ left * (minus centre right) = minus (left * centre) (left * right)
605multDistributesOverMinusRight left centre right =
605multDistributesOverMinusRight left centre right =
606 rewrite multCommutative left (minus centre right) in
606 rewrite multCommutative left (minus centre right) in
607 rewrite multDistributesOverMinusLeft centre right left in
607 rewrite multDistributesOverMinusLeft centre right left in
@@ -658,7 +658,7 @@ total predSucc : (n : Nat) -> pred (S n) = n
658predSucc n = Refl
658predSucc n = Refl
659
659
660total minusSuccPred : (left : Nat) -> (right : Nat) ->
660total minusSuccPred : (left : Nat) -> (right : Nat) ->
661− left - (S right) = pred (left - right)
661+ minus left (S right) = pred (minus left right)
662minusSuccPred Z right = Refl
662minusSuccPred Z right = Refl
663minusSuccPred (S left) Z =
663minusSuccPred (S left) Z =
664 rewrite minusZeroRight left in Refl
664 rewrite minusZeroRight left in Refl