git.iko.soy/Idris-dev
on master help sign in
Neg and Nat adjustments

Neg now means "Numbers with possible negative values" and the methods which deal with negative numbrs (abs, - and negate) are now part of this rather than Num. This means, in particular, that - on Nat can now require a proof. 'minus' on Nat behaves as before (and the proofs use minus rather than -).

commitf7ccfb35eaf53f79037913e974a08a83808d0b5e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 3 Sep 2015, 17:36 (11 years ago) parent22ef96b
10 files changed+81−79
compare with master
unifiedsplit
CHANGELOG+5−1 libs/base/Data/Bits.idr+1−1 libs/base/Data/Complex.idr+7−6 libs/base/Data/Mod2.idr−2 libs/contrib/Data/Matrix/Numeric.idr+9−6 libs/contrib/Data/Nat/DivMod/IteratedSubtraction.idr+1−1 libs/contrib/Data/ZZ.idr+14−11 libs/prelude/Prelude.idr+2−2 libs/prelude/Prelude/Classes.idr+25−32 libs/prelude/Prelude/Nat.idr+17−17
CHANGELOG+5−1
@@ -9,7 +9,11 @@ Language updates
99Library updates
1010---------------
1111
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.
1317
1418Tool updates
1519------------
libs/base/Data/Bits.idr+1−1
@@ -42,7 +42,7 @@ natToBits {n=n} x with (n)
4242 | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x
4343
4444getPad : Nat -> machineTy n
45−getPad n = natToBits ((bitsUsed (nextBytes n)) - n)
45+getPad n = natToBits (minus (bitsUsed (nextBytes n)) n)
4646
4747public
4848data Bits : Nat -> Type where
libs/base/Data/Complex.idr+7−6
@@ -57,20 +57,21 @@ phase (x:+y) = atan2 y x
5757
5858------------------------------ Conjugate
5959
60−conjugate : Num a => Complex a -> Complex a
60+conjugate : Neg a => Complex a -> Complex a
6161conjugate (r:+i) = (r :+ (0-i))
6262
6363instance Functor Complex where
64− map f (r :+ i) = f r :+ f i
65−
66−instance Neg a => Neg (Complex a) where
67− negate = map negate
64+ map f (r :+ i) = f r :+ f i
6865
6966-- We can't do "instance Num a => Num (Complex a)" because
7067-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Float
7168instance Num (Complex Float) where
7269 (+) (a:+b) (c:+d) = ((a+c):+(b+d))
73− (-) (a:+b) (c:+d) = ((a-c):+(b-d))
7470 (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))
7571 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))
7676 abs (a:+b) = (magnitude (a:+b):+0)
77+
libs/base/Data/Mod2.idr−2
@@ -40,9 +40,7 @@ instance Ord (Mod2 n) where
4040
4141instance Num (Mod2 n) where
4242 (+) = modBin plus
43− (-) = modBin minus
4443 (*) = modBin times
45− abs = id
4644 fromInteger = intToMod
4745
4846instance Cast (Mod2 n) (Bits n) where
libs/contrib/Data/Matrix/Numeric.idr+9−6
@@ -24,11 +24,14 @@ infixr 7 <&> -- matrix tensor product
2424
2525instance Num a => Num (Vect n a) where
2626 (+) = zipWith (+)
27− (-) = zipWith (+)
2827 (*) = zipWith (*)
29− abs = id
3028 fromInteger n = replicate _ (fromInteger n)
3129
30+instance Neg a => Neg (Vect n a) where
31+ (-) = zipWith (-)
32+ abs = map abs
33+ negate = map negate
34+
3235-----------------------------------------------------------------------
3336-- Vector functions
3437-----------------------------------------------------------------------
@@ -88,7 +91,7 @@ basis i = replaceAt i 1 0
8891(><) x y = col x <> row y
8992
9093||| 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
9295(<<>>) m1 m2 = (m1 <> m2) - (m2 <> m1)
9396
9497||| Matrix anti-commutator
@@ -112,17 +115,17 @@ blockDiag {n} {m} g h = map (++ replicate m 0) g ++ map ((replicate n 0) ++) h
112115-----------------------------------------------------------------------
113116
114117||| Alternating sum
115−altSum : Num a => Vect n a -> a
118+altSum : Neg a => Vect n a -> a
116119altSum (x::y::zs) = (x - y) + altSum zs
117120altSum [x] = x
118121altSum [] = 0
119122
120123||| 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
122125det2 [[x1,x2],[y1,y2]] = x1*y2 - x2*y1
123126
124127||| 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
126129det {n} m = case n of
127130 Z => det2 m
128131 (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
4747ltToLTE (LTStep lt) = lteSuccRight $ ltToLTE lt
4848
4949||| 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
5151minusLT' Z y = LTSucc
5252minusLT' (S k) Z = LTSucc
5353minusLT' (S k) (S j) = LTStep (minusLT' k j)
libs/contrib/Data/ZZ.idr+14−11
@@ -28,11 +28,6 @@ instance Show ZZ where
2828 show (Pos n) = show n
2929 show (NegS n) = "-" ++ show (S n)
3030
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−
3631negNat : Nat -> ZZ
3732negNat Z = Pos Z
3833negNat (S n) = NegS n
@@ -51,10 +46,6 @@ plusZ (NegS n) (NegS m) = NegS (S (n + m))
5146plusZ (Pos n) (NegS m) = minusNatZ n (S m)
5247plusZ (NegS n) (Pos m) = minusNatZ m (S n)
5348
54−||| Subtract two `ZZ`s. Consider using `(-) {a=ZZ}`.
55−subZ : ZZ -> ZZ -> ZZ
56−subZ n m = plusZ n (negate m)
57−
5849instance Eq ZZ where
5950 (Pos n) == (Pos m) = n == m
6051 (NegS n) == (NegS m) = n == m
@@ -85,11 +76,23 @@ instance Cast Nat ZZ where
8576
8677instance Num ZZ where
8778 (+) = plusZ
88− (-) = subZ
8979 (*) = multZ
90− abs = cast . absZ
9180 fromInteger = fromInt
9281
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+
9396instance Cast ZZ Integer where
9497 cast (Pos n) = cast n
9598 cast (NegS n) = (-1) * (cast n + 1)
libs/prelude/Prelude.idr+2−2
@@ -134,10 +134,10 @@ natRange n = List.reverse (go n)
134134total natEnumFromThen : Nat -> Nat -> Stream Nat
135135natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc
136136total 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))
138138total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
139139natEnumFromThenTo _ 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)))
141141
142142class Enum a where
143143 total pred : a -> a
libs/prelude/Prelude/Classes.idr+25−32
@@ -143,85 +143,78 @@ instance (Ord a, Ord b) => Ord (a, b) where
143143 then compare xl yl
144144 else compare xr yr
145145
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−
161146-- --------------------------------------------------------- [ Numerical Class ]
162147||| The Num class defines basic numerical arithmetic.
163148class Num a where
164149 (+) : a -> a -> a
165− (-) : a -> a -> a
166150 (*) : a -> a -> a
167− ||| Absolute value
168− abs : a -> a
169151 ||| Conversion from Integer.
170152 fromInteger : Integer -> a
171153
172154instance Num Integer where
173155 (+) = prim__addBigInt
174− (-) = prim__subBigInt
175156 (*) = prim__mulBigInt
176157
177− abs x = if x < 0 then -x else x
178158 fromInteger = id
179159
180160instance Num Int where
181161 (+) = prim__addInt
182− (-) = prim__subInt
183162 (*) = prim__mulInt
184163
185164 fromInteger = prim__truncBigInt_Int
186− abs x = if x < (prim__truncBigInt_Int 0) then -x else x
187165
188166
189167instance Num Float where
190168 (+) = prim__addFloat
191− (-) = prim__subFloat
192169 (*) = prim__mulFloat
193170
194− abs x = if x < (prim__toFloatBigInt 0) then -x else x
195171 fromInteger = prim__toFloatBigInt
196172
197173instance Num Bits8 where
198174 (+) = prim__addB8
199− (-) = prim__subB8
200175 (*) = prim__mulB8
201− abs = id
202176 fromInteger = prim__truncBigInt_B8
203177
204178instance Num Bits16 where
205179 (+) = prim__addB16
206− (-) = prim__subB16
207180 (*) = prim__mulB16
208− abs = id
209181 fromInteger = prim__truncBigInt_B16
210182
211183instance Num Bits32 where
212184 (+) = prim__addB32
213− (-) = prim__subB32
214185 (*) = prim__mulB32
215− abs = id
216186 fromInteger = prim__truncBigInt_B32
217187
218188instance Num Bits64 where
219189 (+) = prim__addB64
220− (-) = prim__subB64
221190 (*) = prim__mulB64
222− abs = id
223191 fromInteger = prim__truncBigInt_B64
224192
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+-- ------------------------------------------------------------
225218instance Eq Bits8 where
226219 x == y = intToBool (prim__eqB8 x y)
227220
libs/prelude/Prelude/Nat.idr+17−17
@@ -180,6 +180,9 @@ toIntNat n = toIntNat' n 0 where
180180 toIntNat' Z x = x
181181 toIntNat' (S n) x = toIntNat' n (x + 1)
182182
183+(-) : (m : Nat) -> (n : Nat) -> {auto smaller : LTE n m} -> Nat
184+(-) m n {smaller} = minus m n
185+
183186--------------------------------------------------------------------------------
184187-- Type class instances
185188--------------------------------------------------------------------------------
@@ -200,11 +203,8 @@ instance Ord Nat where
200203
201204instance Num Nat where
202205 (+) = plus
203− (-) = minus
204206 (*) = mult
205207
206− abs x = x
207−
208208 fromInteger = fromIntegerNat
209209
210210instance MinBound Nat where
@@ -307,7 +307,7 @@ modNatNZ left (S right) _ = mod' left left right
307307 if lte centre right then
308308 centre
309309 else
310− mod' left (centre - (S right)) right
310+ mod' left (minus centre (S right)) right
311311
312312partial
313313modNat : Nat -> Nat -> Nat
@@ -323,7 +323,7 @@ divNatNZ left (S right) _ = div' left left right
323323 if lte centre right then
324324 Z
325325 else
326− S (div' left (centre - (S right)) right)
326+ S (div' left (minus centre (S right)) right)
327327
328328partial
329329divNat : Nat -> Nat -> Nat
@@ -544,34 +544,34 @@ multOneRightNeutral (S left) =
544544
545545-- Minus
546546total minusSuccSucc : (left : Nat) -> (right : Nat) ->
547− (S left) - (S right) = left - right
547+ minus (S left) (S right) = minus left right
548548minusSuccSucc left right = Refl
549549
550−total minusZeroLeft : (right : Nat) -> 0 - right = Z
550+total minusZeroLeft : (right : Nat) -> minus 0 right = Z
551551minusZeroLeft right = Refl
552552
553−total minusZeroRight : (left : Nat) -> left - 0 = left
553+total minusZeroRight : (left : Nat) -> minus left 0 = left
554554minusZeroRight Z = Refl
555555minusZeroRight (S left) = Refl
556556
557−total minusZeroN : (n : Nat) -> Z = n - n
557+total minusZeroN : (n : Nat) -> Z = minus n n
558558minusZeroN Z = Refl
559559minusZeroN (S n) = minusZeroN n
560560
561−total minusOneSuccN : (n : Nat) -> S Z = (S n) - n
561+total minusOneSuccN : (n : Nat) -> S Z = minus (S n) n
562562minusOneSuccN Z = Refl
563563minusOneSuccN (S n) = minusOneSuccN n
564564
565−total minusSuccOne : (n : Nat) -> S n - 1 = n
565+total minusSuccOne : (n : Nat) -> minus (S n) 1 = n
566566minusSuccOne Z = Refl
567567minusSuccOne (S n) = Refl
568568
569−total minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = Z
569+total minusPlusZero : (n : Nat) -> (m : Nat) -> minus n (n + m) = Z
570570minusPlusZero Z m = Refl
571571minusPlusZero (S n) m = minusPlusZero n m
572572
573573total minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
574− left - centre - right = left - (centre + right)
574+ minus (minus left centre) right = minus left (centre + right)
575575minusMinusMinusPlus Z Z right = Refl
576576minusMinusMinusPlus (S left) Z right = Refl
577577minusMinusMinusPlus Z (S centre) right = Refl
@@ -581,7 +581,7 @@ minusMinusMinusPlus (S left) (S centre) right =
581581 Refl
582582
583583total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
584− (left + right) - (left + right') = right - right'
584+ minus (left + right) (left + right') = minus right right'
585585plusMinusLeftCancel Z right right' = Refl
586586plusMinusLeftCancel (S left) right right' =
587587 let inductiveHypothesis = plusMinusLeftCancel left right right' in
@@ -589,7 +589,7 @@ plusMinusLeftCancel (S left) right right' =
589589 Refl
590590
591591total 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)
593593multDistributesOverMinusLeft Z Z right = Refl
594594multDistributesOverMinusLeft (S left) Z right =
595595 rewrite (minusZeroRight (plus right (mult left right))) in Refl
@@ -601,7 +601,7 @@ multDistributesOverMinusLeft (S left) (S centre) right =
601601 Refl
602602
603603total 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)
605605multDistributesOverMinusRight left centre right =
606606 rewrite multCommutative left (minus centre right) in
607607 rewrite multDistributesOverMinusLeft centre right left in
@@ -658,7 +658,7 @@ total predSucc : (n : Nat) -> pred (S n) = n
658658predSucc n = Refl
659659
660660total minusSuccPred : (left : Nat) -> (right : Nat) ->
661− left - (S right) = pred (left - right)
661+ minus left (S right) = pred (minus left right)
662662minusSuccPred Z right = Refl
663663minusSuccPred (S left) Z =
664664 rewrite minusZeroRight left in Refl