ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-11 14:57:30 +03:00
Code Issues Projects Releases Wiki Activity

Neg and Nat adjustments

Browse Source 
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
-).
This commit is contained in:
Edwin Brady 2015-09-03 17:36:24 +01:00
parent 22ef96b21f
commit f7ccfb35ea
10 changed files with 81 additions and 79 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
CHANGELOG
View File

@ -9,7 +9,11 @@ Language updates
Library updates
---------------
[None so far]
* The 'Neg' class now represents numeric types which can be negative. As
such, the (-) operator and 'abs' have been moved there from 'Num'.
* A special version of (-) on 'Nat' requires that the second argument is
smaller than or equal to the first. 'minus' retains the old behaviour,
returning Z if there is an underflow.
Tool updates
------------

2
libs/base/Data/Bits.idr
View File

@ -42,7 +42,7 @@ natToBits {n=n} x with (n)
| S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x
getPad : Nat -> machineTy n
getPad n = natToBits ((bitsUsed (nextBytes n)) - n)
getPad n = natToBits (minus (bitsUsed (nextBytes n)) n)
public
data Bits : Nat -> Type where

13
libs/base/Data/Complex.idr
View File

@ -57,20 +57,21 @@ phase (x:+y) = atan2 y x
------------------------------ Conjugate
conjugate : Num a => Complex a -> Complex a
conjugate : Neg a => Complex a -> Complex a
conjugate (r:+i) = (r :+ (0-i))
instance Functor Complex where
map f (r :+ i) = f r :+ f i
instance Neg a => Neg (Complex a) where
negate = map negate
map f (r :+ i) = f r :+ f i
-- We can't do "instance Num a => Num (Complex a)" because
-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Float
instance Num (Complex Float) where
(+) (a:+b) (c:+d) = ((a+c):+(b+d))
(-) (a:+b) (c:+d) = ((a-c):+(b-d))
(*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))
fromInteger x = (fromInteger x:+0)
instance Neg (Complex Float) where
negate = map negate
(-) (a:+b) (c:+d) = ((a-c):+(b-d))
abs (a:+b) = (magnitude (a:+b):+0)

2
libs/base/Data/Mod2.idr
View File

@ -40,9 +40,7 @@ instance Ord (Mod2 n) where
instance Num (Mod2 n) where
(+) = modBin plus
(-) = modBin minus
(*) = modBin times
abs = id
fromInteger = intToMod
instance Cast (Mod2 n) (Bits n) where

15
libs/contrib/Data/Matrix/Numeric.idr
View File

@ -24,11 +24,14 @@ infixr 7 <&> -- matrix tensor product
instance Num a => Num (Vect n a) where
(+) = zipWith (+)
(-) = zipWith (+)
(*) = zipWith (*)
abs = id
fromInteger n = replicate _ (fromInteger n)
instance Neg a => Neg (Vect n a) where
(-) = zipWith (-)
abs = map abs
negate = map negate
-----------------------------------------------------------------------
-- Vector functions
-----------------------------------------------------------------------
@ -88,7 +91,7 @@ basis i = replaceAt i 1 0
(><) x y = col x <> row y
||| Matrix commutator
(<<>>) : Num a => Matrix n n a -> Matrix n n a -> Matrix n n a
(<<>>) : Neg a => Matrix n n a -> Matrix n n a -> Matrix n n a
(<<>>) m1 m2 = (m1 <> m2) - (m2 <> m1)
||| Matrix anti-commutator
@ -112,17 +115,17 @@ blockDiag {n} {m} g h = map (++ replicate m 0) g ++ map ((replicate n 0) ++) h
-----------------------------------------------------------------------
||| Alternating sum
altSum : Num a => Vect n a -> a
altSum : Neg a => Vect n a -> a
altSum (x::y::zs) = (x - y) + altSum zs
altSum [x] = x
altSum [] = 0
||| Determinant of a 2-by-2 matrix
det2 : Num a => Matrix 2 2 a -> a
det2 : Neg a => Matrix 2 2 a -> a
det2 [[x1,x2],[y1,y2]] = x1*y2 - x2*y1
||| Determinant of a square matrix
det : Num a => Matrix (S (S n)) (S (S n)) a -> a
det : Neg a => Matrix (S (S n)) (S (S n)) a -> a
det {n} m = case n of
Z => det2 m
(S k) => altSum . map (\c => indices FZ c m * det (subMatrix FZ c m))

2
libs/contrib/Data/Nat/DivMod/IteratedSubtraction.idr
View File

@ -47,7 +47,7 @@ ltToLTE LTSucc = lteRefl
ltToLTE (LTStep lt) = lteSuccRight $ ltToLTE lt
||| Subtraction gives a result that is actually smaller.
minusLT' : (x,y : Nat) -> x - y `LT'` S x
minusLT' : (x,y : Nat) -> minus x y `LT'` S x
minusLT' Z y = LTSucc
minusLT' (S k) Z = LTSucc
minusLT' (S k) (S j) = LTStep (minusLT' k j)

25
libs/contrib/Data/ZZ.idr
View File

@ -28,11 +28,6 @@ instance Show ZZ where
show (Pos n) = show n
show (NegS n) = "-" ++ show (S n)
instance Neg ZZ where
negate (Pos Z) = Pos Z
negate (Pos (S n)) = NegS n
negate (NegS n) = Pos (S n)
negNat : Nat -> ZZ
negNat Z = Pos Z
negNat (S n) = NegS n
@ -51,10 +46,6 @@ plusZ (NegS n) (NegS m) = NegS (S (n + m))
plusZ (Pos n) (NegS m) = minusNatZ n (S m)
plusZ (NegS n) (Pos m) = minusNatZ m (S n)
||| Subtract two `ZZ`s. Consider using `(-) {a=ZZ}`.
subZ : ZZ -> ZZ -> ZZ
subZ n m = plusZ n (negate m)
instance Eq ZZ where
(Pos n) == (Pos m) = n == m
(NegS n) == (NegS m) = n == m
@ -85,11 +76,23 @@ instance Cast Nat ZZ where
instance Num ZZ where
(+) = plusZ
(-) = subZ
(*) = multZ
abs = cast . absZ
fromInteger = fromInt
mutual
instance Neg ZZ where
negate (Pos Z) = Pos Z
negate (Pos (S n)) = NegS n
negate (NegS n) = Pos (S n)
(-) = subZ
abs = cast . absZ
||| Subtract two `ZZ`s. Consider using `(-) {a=ZZ}`.
subZ : ZZ -> ZZ -> ZZ
subZ n m = plusZ n (negate m)
instance Cast ZZ Integer where
cast (Pos n) = cast n
cast (NegS n) = (-1) * (cast n + 1)

4
libs/prelude/Prelude.idr
View File

@ -134,10 +134,10 @@ natRange n = List.reverse (go n)
total natEnumFromThen : Nat -> Nat -> Stream Nat
natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc
total natEnumFromTo : Nat -> Nat -> List Nat
natEnumFromTo n m = map (plus n) (natRange ((S m) - n))
natEnumFromTo n m = map (plus n) (natRange (minus (S m) n))
total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
natEnumFromThenTo _ Z _ = []
natEnumFromThenTo n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (m - n) (S inc) SIsNotZ)))
natEnumFromThenTo n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (minus m n) (S inc) SIsNotZ)))
class Enum a where
total pred : a -> a

57
libs/prelude/Prelude/Classes.idr
View File

@ -143,85 +143,78 @@ instance (Ord a, Ord b) => Ord (a, b) where
then compare xl yl
else compare xr yr
-- --------------------------------------------------------- [ Negatable Class ]
||| The `Neg` class defines unary negation (-).
class Neg a where
||| The underlying implementation of unary minus. `-5` desugars to `negate (fromInteger 5)`.
negate : a -> a
instance Neg Integer where
negate x = prim__subBigInt 0 x
instance Neg Int where
negate x = prim__subInt 0 x
instance Neg Float where
negate x = prim__negFloat x
-- --------------------------------------------------------- [ Numerical Class ]
||| The Num class defines basic numerical arithmetic.
class Num a where
(+) : a -> a -> a
(-) : a -> a -> a
(*) : a -> a -> a
||| Absolute value
abs : a -> a
||| Conversion from Integer.
fromInteger : Integer -> a
instance Num Integer where
(+) = prim__addBigInt
(-) = prim__subBigInt
(*) = prim__mulBigInt
abs x = if x < 0 then -x else x
fromInteger = id
instance Num Int where
(+) = prim__addInt
(-) = prim__subInt
(*) = prim__mulInt
fromInteger = prim__truncBigInt_Int
abs x = if x < (prim__truncBigInt_Int 0) then -x else x
instance Num Float where
(+) = prim__addFloat
(-) = prim__subFloat
(*) = prim__mulFloat
abs x = if x < (prim__toFloatBigInt 0) then -x else x
fromInteger = prim__toFloatBigInt
instance Num Bits8 where
(+) = prim__addB8
(-) = prim__subB8
(*) = prim__mulB8
abs = id
fromInteger = prim__truncBigInt_B8
instance Num Bits16 where
(+) = prim__addB16
(-) = prim__subB16
(*) = prim__mulB16
abs = id
fromInteger = prim__truncBigInt_B16
instance Num Bits32 where
(+) = prim__addB32
(-) = prim__subB32
(*) = prim__mulB32
abs = id
fromInteger = prim__truncBigInt_B32
instance Num Bits64 where
(+) = prim__addB64
(-) = prim__subB64
(*) = prim__mulB64
abs = id
fromInteger = prim__truncBigInt_B64
-- --------------------------------------------------------- [ Negatable Class ]
||| The `Neg` class defines operations on numbers which can be negative.
class Num a => Neg a where
||| The underlying implementation of unary minus. `-5` desugars to `negate (fromInteger 5)`.
negate : a -> a
(-) : a -> a -> a
||| Absolute value
abs : a -> a
instance Neg Integer where
negate x = prim__subBigInt 0 x
(-) = prim__subBigInt
abs x = if x < 0 then -x else x
instance Neg Int where
negate x = prim__subInt 0 x
(-) = prim__subInt
abs x = if x < (prim__truncBigInt_Int 0) then -x else x
instance Neg Float where
negate x = prim__negFloat x
(-) = prim__subFloat
abs x = if x < (prim__toFloatBigInt 0) then -x else x
-- ------------------------------------------------------------
instance Eq Bits8 where
x == y = intToBool (prim__eqB8 x y)

34
libs/prelude/Prelude/Nat.idr
View File

@ -180,6 +180,9 @@ toIntNat n = toIntNat' n 0 where
toIntNat' Z x = x
toIntNat' (S n) x = toIntNat' n (x + 1)
(-) : (m : Nat) -> (n : Nat) -> {auto smaller : LTE n m} -> Nat
(-) m n {smaller} = minus m n
--------------------------------------------------------------------------------
-- Type class instances
--------------------------------------------------------------------------------
@ -200,11 +203,8 @@ instance Ord Nat where
instance Num Nat where
(+) = plus
(-) = minus
(*) = mult
abs x = x
fromInteger = fromIntegerNat
instance MinBound Nat where
@ -307,7 +307,7 @@ modNatNZ left (S right) _ = mod' left left right
if lte centre right then
centre
else
mod' left (centre - (S right)) right
mod' left (minus centre (S right)) right
partial
modNat : Nat -> Nat -> Nat
@ -323,7 +323,7 @@ divNatNZ left (S right) _ = div' left left right
if lte centre right then
Z
else
S (div' left (centre - (S right)) right)
S (div' left (minus centre (S right)) right)
partial
divNat : Nat -> Nat -> Nat
@ -544,34 +544,34 @@ multOneRightNeutral (S left) =
-- Minus
total minusSuccSucc : (left : Nat) -> (right : Nat) ->
(S left) - (S right) = left - right
minus (S left) (S right) = minus left right
minusSuccSucc left right = Refl
total minusZeroLeft : (right : Nat) -> 0 - right = Z
total minusZeroLeft : (right : Nat) -> minus 0 right = Z
minusZeroLeft right = Refl
total minusZeroRight : (left : Nat) -> left - 0 = left
total minusZeroRight : (left : Nat) -> minus left 0 = left
minusZeroRight Z = Refl
minusZeroRight (S left) = Refl
total minusZeroN : (n : Nat) -> Z = n - n
total minusZeroN : (n : Nat) -> Z = minus n n
minusZeroN Z = Refl
minusZeroN (S n) = minusZeroN n
total minusOneSuccN : (n : Nat) -> S Z = (S n) - n
total minusOneSuccN : (n : Nat) -> S Z = minus (S n) n
minusOneSuccN Z = Refl
minusOneSuccN (S n) = minusOneSuccN n
total minusSuccOne : (n : Nat) -> S n - 1 = n
total minusSuccOne : (n : Nat) -> minus (S n) 1 = n
minusSuccOne Z = Refl
minusSuccOne (S n) = Refl
total minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = Z
total minusPlusZero : (n : Nat) -> (m : Nat) -> minus n (n + m) = Z
minusPlusZero Z m = Refl
minusPlusZero (S n) m = minusPlusZero n m
total minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
left - centre - right = left - (centre + right)
minus (minus left centre) right = minus left (centre + right)
minusMinusMinusPlus Z Z right = Refl
minusMinusMinusPlus (S left) Z right = Refl
minusMinusMinusPlus Z (S centre) right = Refl
@ -581,7 +581,7 @@ minusMinusMinusPlus (S left) (S centre) right =
Refl
total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
(left + right) - (left + right') = right - right'
minus (left + right) (left + right') = minus right right'
plusMinusLeftCancel Z right right' = Refl
plusMinusLeftCancel (S left) right right' =
let inductiveHypothesis = plusMinusLeftCancel left right right' in
@ -589,7 +589,7 @@ plusMinusLeftCancel (S left) right right' =
Refl
total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
(left - centre) * right = (left * right) - (centre * right)
(minus left centre) * right = minus (left * right) (centre * right)
multDistributesOverMinusLeft Z Z right = Refl
multDistributesOverMinusLeft (S left) Z right =
rewrite (minusZeroRight (plus right (mult left right))) in Refl
@ -601,7 +601,7 @@ multDistributesOverMinusLeft (S left) (S centre) right =
Refl
total multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
left * (centre - right) = (left * centre) - (left * right)
left * (minus centre right) = minus (left * centre) (left * right)
multDistributesOverMinusRight left centre right =
rewrite multCommutative left (minus centre right) in
rewrite multDistributesOverMinusLeft centre right left in
@ -658,7 +658,7 @@ total predSucc : (n : Nat) -> pred (S n) = n
predSucc n = Refl
total minusSuccPred : (left : Nat) -> (right : Nat) ->
left - (S right) = pred (left - right)
minus left (S right) = pred (minus left right)
minusSuccPred Z right = Refl
minusSuccPred (S left) Z =
rewrite minusZeroRight left in Refl