add minimum/maximum

This commit is contained in:
rnhmjoj 2016-11-16 22:24:15 +01:00
parent a8291ccf9f
commit f8365ca381
No known key found for this signature in database
GPG Key ID: 362BB82B7E496B7C

View File

@ -22,7 +22,7 @@ import Data.Nat
import Data.Bool import Data.Bool
import Data.Char (Char) import Data.Char (Char)
import Data.Function ((), ($)) import Data.Function ((), ($))
import Data.TypeClass (Show, IsList, IsString, Eq, Num) import Data.TypeClass (Show, Eq, Ord, Num, IsList, IsString)
import Data.Singletons (SingI, sing) import Data.Singletons (SingI, sing)
import qualified Data.TypeClass as T import qualified Data.TypeClass as T
@ -174,7 +174,7 @@ intercalate xs xss = concat (intersperse xs xss)
-- > transpose [[1,2,3],[4,5,6]] == [[1,4],[2,5],[3,6]] -- > transpose [[1,2,3],[4,5,6]] == [[1,4],[2,5],[3,6]]
-- --
transpose SingI n Vec (Vec a n) m Vec (Vec a m) n transpose SingI n Vec (Vec a n) m Vec (Vec a m) n
transpose Nil = replicate Nil transpose Nil = replicate Nil
transpose (xs :- xss) = gcastWith proof (zipWith (:-) xs (transpose xss)) transpose (xs :- xss) = gcastWith proof (zipWith (:-) xs (transpose xss))
where proof = min_self (sLength xs) where proof = min_self (sLength xs)
@ -197,16 +197,17 @@ foldr (⊗) x (y:-ys) = y ⊗ (foldr (⊗) x ys)
-- | Variant of 'foldl' which requires no starting value but -- | Variant of 'foldl' which requires no starting value but
-- applies only on nonempty 'Vec' -- applies only on nonempty 'Vec'
foldl (a a a) Vec a (S n) a foldl (a a a) Vec a (S n) a
foldl _ (x :- Nil) = x foldl _ (x :- Nil) = x
foldl () (x :- y :- ys) = foldl () (x y :- ys) foldl () (x :- y :- ys) = foldl () (x y :- ys)
-- | As for 'foldl', a variant of 'foldr' with no starting point -- | As for 'foldl', a variant of 'foldr' with no starting point
foldr (a a a) Vec a (S n) a foldr (a a a) Vec a (S n) a
foldr () (x :- Nil) = x foldr _ (x :- Nil) = x
foldr () (x :- y :- ys) = x (foldr () (y :- ys)) foldr () (x :- y :- ys) = x (foldr () (y :- ys))
-- * Special folds -- * Special folds
-- | The concatenation of all the elements of a vector of vectors. -- | The concatenation of all the elements of a vector of vectors.
@ -259,6 +260,16 @@ all _ Nil = T
all p (x :- xs) = and (map p (x :- xs)) all p (x :- xs) = and (map p (x :- xs))
-- | The least element of a vector.
minimum Ord a Vec a (S n) a
minimum = foldr T.min
-- | The largest element of a vector.
maximum Ord a Vec a (S n) a
maximum = foldr T.max
-- | The 'sum' function computes the sum of the numbers of a vector. -- | The 'sum' function computes the sum of the numbers of a vector.
sum Num a Vec a n a sum Num a Vec a n a
sum = foldr (T.+) 0 sum = foldr (T.+) 0
@ -283,6 +294,7 @@ drop SZ x = x
drop (SS n) (x :- xs) = drop n xs drop (SS n) (x :- xs) = drop n xs
-- * Zipping and unzipping vectors -- * Zipping and unzipping vectors
-- | 'zip' takes two vectors and returns a vector of corresponding pairs. -- | 'zip' takes two vectors and returns a vector of corresponding pairs.
@ -310,8 +322,8 @@ zipWith _ _ Nil = Nil
zipWith () (x :- xs) (y :- ys) = x y :- zipWith () xs ys zipWith () (x :- xs) (y :- ys) = x y :- zipWith () xs ys
-- | 'unzip' transforms a list of pairs into a list of first components -- | 'unzip' transforms a vectors of pairs into a vector of first components
-- and a list of second components. -- and a vector of second components.
unzip Vec (a, b) n (Vec a n, Vec b n) unzip Vec (a, b) n (Vec a n, Vec b n)
unzip Nil = (Nil, Nil) unzip Nil = (Nil, Nil)
unzip ((x, y) :- xys) = (x :- xs, y :- ys) unzip ((x, y) :- xys) = (x :- xs, y :- ys)