diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,16 @@ Changelog for singletons project ================================ +2.0.1 +----- + * Lots more functions in `Data.Singletons.Prelude.List`: + `filter`, `find`, `elemIndex`, `elemIndices`, `findIndex`, `findIndices`, + `intersect`, `intersectBy`, `takeWhile`, `dropWhile`, `dropWhileEnd`, + `span`, `break`, `take`, `drop`, `splitAt`, `group`, `maximum`, + `minimum`, `insert`, `sort`, `groupBy`, `lookup`, `partition`, + `sum`, `product`, `length`, `replicate`, `transpose`, `(!!)`, + `nub`, `nubBy`, `unionBy`, `union`, `genericLength` + 2.0.0.2 ------- * Fix fixity of `*`. @@ -37,6 +47,8 @@ * Full support for fixity declarations. * A raft of bugfixes. + +* Drop support for GHC 7.8. You must have GHC 7.10.2. 1.1.2.1 ------- diff --git a/singletons.cabal b/singletons.cabal --- a/singletons.cabal +++ b/singletons.cabal @@ -1,9 +1,9 @@ name: singletons -version: 2.0.0.2 +version: 2.0.1 -- Remember to bump version in the Makefile as well cabal-version: >= 1.10 synopsis: A framework for generating singleton types -homepage: http://www.cis.upenn.edu/~eir/packages/singletons +homepage: http://www.github.com/goldfirere/singletons category: Dependent Types author: Richard Eisenberg , Jan Stolarek maintainer: Richard Eisenberg , Jan Stolarek @@ -38,11 +38,11 @@ source-repository this type: git location: https://github.com/goldfirere/singletons.git - tag: v2.0.0.2 + tag: v2.0.1 library hs-source-dirs: src - build-depends: base >= 4.7.0.1 && < 5, + build-depends: base >= 4.8.1.0 && < 5, mtl >= 2.1.2, template-haskell, containers >= 0.5, diff --git a/src/Data/Promotion/Prelude/List.hs b/src/Data/Promotion/Prelude/List.hs --- a/src/Data/Promotion/Prelude/List.hs +++ b/src/Data/Promotion/Prelude/List.hs @@ -226,149 +226,12 @@ import Data.Singletons.Prelude.Base import Data.Singletons.Prelude.Eq -import Data.Promotion.Prelude.Ord import Data.Singletons.Prelude.List import Data.Singletons.Prelude.Maybe -import Data.Singletons.Prelude.Tuple -import Data.Singletons.Prelude.Bool import Data.Singletons.TH -import Data.Singletons.TypeLits -import Data.Singletons.Prelude.Num -import Data.Maybe (listToMaybe) --- these imports are required fir functions that singletonize but are used --- in this module by a function that can't be singletonized -import Data.List (sortBy, insertBy, deleteBy) - $(promoteOnly [d| --- Can't be promoted because of limitations of Int promotion --- Below is a re-implementation using Nat --- length :: [a] -> Int --- length l = lenAcc l 0# --- --- lenAcc :: [a] -> Int# -> Int --- lenAcc [] a# = I# a# --- lenAcc (_:xs) a# = lenAcc xs (a# +# 1#) --- --- incLen :: a -> (Int# -> Int) -> Int# -> Int --- incLen _ g x = g (x +# 1#) - length :: [a] -> Nat - length [] = 0 - length (_:xs) = 1 + length xs - --- Can't be promoted because of limitations of Int promotion --- Below is a re-implementation using Nat --- sum :: (Num a) => [a] -> a --- sum l = sum' l 0 --- where --- sum' [] a = a --- sum' (x:xs) a = sum' xs (a+x) --- --- product :: (Num a) => [a] -> a --- product l = prod l 1 --- where --- prod [] a = a --- prod (x:xs) a = prod xs (a*x) - - sum :: [Nat] -> Nat - sum l = sum' l 0 - where - sum' [] a = a - sum' (x:xs) a = sum' xs (a+x) - - product :: [Nat] -> Nat - product l = prod l 1 - where - prod [] a = a - prod (x:xs) a = prod xs (a*x) - --- Functions working on infinite lists don't promote because they create --- infinite types. replicate also uses integers, but luckily it can be rewritten --- iterate :: (a -> a) -> a -> [a] --- iterate f x = x : iterate f (f x) --- --- repeat :: a -> [a] --- repeat x = xs where xs = x : xs --- --- replicate :: Int -> a -> [a] --- replicate n x = take n (repeat x) --- --- cycle :: [a] -> [a] --- cycle [] = error "Data.Singletons.List.cycle: empty list" --- cycle xs = xs' where xs' = xs ++ xs' - - replicate :: Nat -> a -> [a] - replicate 0 _ = [] - replicate n x = x : replicate (n-1) x - --- Uses list comprehensions --- transpose :: [[a]] -> [[a]] --- transpose [] = [] --- transpose ([] : xss) = transpose xss --- transpose ((x:xs) : xss) = (x : [h | (h:_) <- xss]) : transpose (xs : [ t | (_:t) <- xss]) - - transpose :: [[a]] -> [[a]] - transpose [] = [] - transpose ([] : xss) = transpose xss - transpose ((x:xs) : xss) = (x : (map head xss)) : transpose (xs : (map tail xss)) - --- Can't be promoted because of limitations of Int promotion --- Below is a re-implementation using Nat --- take :: Int -> [a] -> [a] --- take n _ | n <= 0 = [] --- take _ [] = [] --- take n (x:xs) = x : take (n-1) xs - --- drop :: Int -> [a] -> [a] --- drop n xs | n <= 0 = xs --- drop _ [] = [] --- drop n (_:xs) = drop (n-1) xs - --- splitAt :: Int -> [a] -> ([a],[a]) --- splitAt n xs = (take n xs, drop n xs) - - take :: Nat -> [a] -> [a] - take n _ | n <= 0 = [] - take _ [] = [] - take n (x:xs) = x : take (n-1) xs - - drop :: Nat -> [a] -> [a] - drop n xs | n <= 0 = xs - drop _ [] = [] - drop n (_:xs) = drop (n-1) xs - - splitAt :: Nat -> [a] -> ([a],[a]) - splitAt n xs = (take n xs, drop n xs) - - - takeWhile :: (a -> Bool) -> [a] -> [a] - takeWhile _ [] = [] - takeWhile p (x:xs) - | p x = x : takeWhile p xs - | otherwise = [] - - dropWhile :: (a -> Bool) -> [a] -> [a] - dropWhile _ [] = [] - dropWhile p xs@(x:xs') - | p x = dropWhile p xs' - | otherwise = xs - - dropWhileEnd :: (a -> Bool) -> [a] -> [a] - dropWhileEnd p = foldr (\x xs -> if p x && null xs then [] else x : xs) [] - - span :: (a -> Bool) -> [a] -> ([a],[a]) - span _ xs@[] = (xs, xs) - span p xs@(x:xs') - | p x = let (ys,zs) = span p xs' in (x:ys,zs) - | otherwise = ([],xs) - - break :: (a -> Bool) -> [a] -> ([a],[a]) - break _ xs@[] = (xs, xs) - break p xs@(x:xs') - | p x = ([],xs) - | otherwise = let (ys,zs) = break p xs' in (x:ys,zs) - -- Overlapping patterns don't singletonize stripPrefix :: Eq a => [a] -> [a] -> Maybe [a] stripPrefix [] ys = Just ys @@ -376,94 +239,6 @@ | x == y = stripPrefix xs ys stripPrefix _ _ = Nothing - -- Relies on groupBy, which relies on span, which does not singletonize - group :: Eq a => [a] -> [[a]] - group xs = groupBy (==) xs - - -- Requires Ord instance, which does not singletonize - maximum :: (Ord a) => [a] -> a - maximum [] = error "Data.Singletons.List.maximum: empty list" - maximum xs = foldl1 max xs - - -- Requires Ord instance, which does not singletonize - minimum :: (Ord a) => [a] -> a - minimum [] = error "Data.Singletons.List.minimum: empty list" - minimum xs = foldl1 min xs - - -- Requires Ord instance, which does not singletonize - insert :: Ord a => a -> [a] -> [a] - insert e ls = insertBy (compare) e ls - - -- Requires Ord instance, which does not singletonize - sort :: (Ord a) => [a] -> [a] - sort = sortBy compare - - -- Relies on span, which does not singletonize - groupBy :: (a -> a -> Bool) -> [a] -> [[a]] - groupBy _ [] = [] - groupBy eq (x:xs) = (x:ys) : groupBy eq zs - where (ys,zs) = span (eq x) xs - - lookup :: (Eq a) => a -> [(a,b)] -> Maybe b - lookup _key [] = Nothing - lookup key ((x,y):xys) - | key == x = Just y - | otherwise = lookup key xys - - -- Relies on filter, which does not singletonize - find :: (a -> Bool) -> [a] -> Maybe a - find p = listToMaybe . filter p - - filter :: (a -> Bool) -> [a] -> [a] - filter _p [] = [] - filter p (x:xs) - | p x = x : filter p xs - | otherwise = filter p xs - - -- Relies on select, which does not singletonize (#30, #33) - partition :: (a -> Bool) -> [a] -> ([a],[a]) - partition p xs = foldr (select p) ([],[]) xs - - -- Lazy pattern removed from select - select :: (a -> Bool) -> a -> ([a], [a]) -> ([a], [a]) - select p x (ts,fs) | p x = (x:ts,fs) - | otherwise = (ts, x:fs) - --- Can't be promoted because of limitations of Int promotion. --- Below is a re-implementation using Nat --- (!!) :: [a] -> Int -> a --- xs !! n | n < 0 = error "Data.Singletons.List.!!: negative index" --- [] !! _ = error "Data.Singletons.List.!!: index too large" --- (x:_) !! 0 = x --- (_:xs) !! n = xs !! (n-1) - - (!!) :: [a] -> Nat -> a - _ !! n | n < 0 = error "Data.Singletons.List.!!: negative index" - [] !! _ = error "Data.Singletons.List.!!: index too large" - (x:_) !! 0 = x - (_:xs) !! n = xs !! (n-1) - --- These three rely on findIndices, which does not promote. --- Since we have our own implementation of findIndices these are perfectly valid - elemIndex :: Eq a => a -> [a] -> Maybe Nat - elemIndex x = findIndex (x==) - - elemIndices :: Eq a => a -> [a] -> [Nat] - elemIndices x = findIndices (x==) - - findIndex :: (a -> Bool) -> [a] -> Maybe Nat - findIndex p = listToMaybe . findIndices p - --- Uses list comprehensions, infinite lists and and Ints --- findIndices :: (a -> Bool) -> [a] -> [Int] --- findIndices p xs = [ i | (x,i) <- zip xs [0..], p x] - - findIndices :: (a -> Bool) -> [a] -> [Nat] - findIndices p xs = map snd (filter (\(x,_) -> p x) - (zip xs (buildList 0 (length xs)))) - where buildList _ 0 = [] - buildList a n = a : buildList (a+1) (n-1) - -- To singletonize these we would need to rewrite all patterns -- as non-overlapping. This means 2^7 equations for zipWith7. @@ -504,63 +279,12 @@ = z a b c d e f g : zipWith7 z as bs cs ds es fs gs zipWith7 _ _ _ _ _ _ _ _ = [] - nub :: (Eq a) => [a] -> [a] - nub l = nub' l [] - where - nub' :: [a] -> [a] -> [a] - nub' [] _ = [] - nub' (x:xs) ls - | x `elem` ls = nub' xs ls - | otherwise = x : nub' xs (x:ls) - - nubBy :: (a -> a -> Bool) -> [a] -> [a] - nubBy eq l = nubBy' l [] - where - nubBy' :: [b] -> [b] -> [b] - nubBy' [] _ = [] - nubBy' (y:ys) xs - | elem_by eq y xs = nubBy' ys xs - | otherwise = y : nubBy' ys (y:xs) - - elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool - elem_by _ _ [] = False - elem_by eq y (x:xs) = y `eq` x || elem_by eq y xs - - -- Relies on nubBy, which does not singletonize - unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a] - unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs - - -- Relies on unionBy, which does not singletonize - union :: (Eq a) => [a] -> [a] -> [a] - union = unionBy (==) - - -- Relies on intersectBy, which does not singletonize - intersect :: (Eq a) => [a] -> [a] -> [a] - intersect = intersectBy (==) - --- Uses list comprehensions. Desugared version uses filter, which does --- not singletonize due to #30 --- intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a] --- intersectBy _ [] [] = [] --- intersectBy _ [] (_:_) = [] --- intersectBy _ (_:_) [] = [] --- intersectBy eq xs ys = [x | x <- xs, any_ (eq x) ys] - - intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a] - intersectBy _ [] [] = [] - intersectBy _ [] (_:_) = [] - intersectBy _ (_:_) [] = [] - intersectBy eq xs ys = filter (\x -> any_ (eq x) ys) xs - -- These functions use Integral or Num typeclass instead of Int. -- -- genericLength, genericTake, genericDrop, genericSplitAt, genericIndex -- genericReplicate -- -- We provide aliases below to improve compatibility - - genericLength :: (Num i) => [a] -> i - genericLength = length genericTake :: (Integral i) => i -> [a] -> [a] genericTake = take diff --git a/src/Data/Singletons/Prelude/List.hs b/src/Data/Singletons/Prelude/List.hs --- a/src/Data/Singletons/Prelude/List.hs +++ b/src/Data/Singletons/Prelude/List.hs @@ -36,12 +36,12 @@ -- * Basic functions (:++), (%:++), Head, sHead, Last, sLast, Tail, sTail, Init, sInit, - Null, sNull, + Null, sNull, Length, sLength, -- * List transformations Map, sMap, Reverse, sReverse, Intersperse, sIntersperse, - Intercalate, sIntercalate, Subsequences, sSubsequences, - Permutations, sPermutations, + Intercalate, sIntercalate, Transpose, sTranspose, + Subsequences, sSubsequences, Permutations, sPermutations, -- * Reducing lists (folds) Foldl, sFoldl, Foldl', sFoldl', Foldl1, sFoldl1, Foldl1', sFoldl1', @@ -50,6 +50,8 @@ -- ** Special folds Concat, sConcat, ConcatMap, sConcatMap, And, sAnd, Or, sOr, Any_, sAny_, All, sAll, + Sum, sSum, Product, sProduct, Maximum, sMaximum, + Minimum, sMinimum, any_, -- equivalent of Data.List `any`. Avoids name clash with Any type -- * Building lists @@ -60,12 +62,18 @@ -- ** Accumulating maps MapAccumL, sMapAccumL, MapAccumR, sMapAccumR, + -- ** Cyclical lists + Replicate, sReplicate, + -- ** Unfolding Unfoldr, sUnfoldr, -- * Sublists -- ** Extracting sublists + Take, sTake, Drop, sDrop, SplitAt, sSplitAt, + TakeWhile, sTakeWhile, DropWhile, sDropWhile, DropWhileEnd, sDropWhileEnd, + Span, sSpan, Break, sBreak, Group, sGroup, Inits, sInits, Tails, sTails, -- ** Predicates @@ -74,8 +82,16 @@ -- * Searching lists -- ** Searching by equality - Elem, sElem, NotElem, sNotElem, + Elem, sElem, NotElem, sNotElem, Lookup, sLookup, + -- ** Searching with a predicate + Find, sFind, Filter, sFilter, Partition, sPartition, + + -- * Indexing lists + (:!!), (%:!!), + ElemIndex, sElemIndex, ElemIndices, sElemIndices, + FindIndex, sFindIndex, FindIndices, sFindIndices, + -- * Zipping and unzipping lists Zip, sZip, Zip3, sZip3, ZipWith, sZipWith, ZipWith3, sZipWith3, Unzip, sUnzip, Unzip3, sUnzip3, Unzip4, sUnzip4, @@ -84,29 +100,45 @@ -- * Special lists -- ** \"Set\" operations - Delete, sDelete, (:\\), (%:\\), + Nub, sNub, Delete, sDelete, (:\\), (%:\\), + Union, sUnion, Intersect, sIntersect, -- ** Ordered lists - -- Insert, sInsert, Sort, sSort, + Insert, sInsert, Sort, sSort, -- * Generalized functions -- ** The \"@By@\" operations + + -- *** User-supplied equality (replacing an @Eq@ context) + -- | The predicate is assumed to define an equivalence. + NubBy, sNubBy, DeleteBy, sDeleteBy, DeleteFirstsBy, sDeleteFirstsBy, + UnionBy, sUnionBy, IntersectBy, sIntersectBy, + GroupBy, sGroupBy, + -- *** User-supplied comparison (replacing an @Ord@ context) + -- | The function is assumed to define a total ordering. SortBy, sSortBy, InsertBy, sInsertBy, MaximumBy, sMaximumBy, MinimumBy, sMinimumBy, + -- ** The \"@generic@\" operations + -- | The prefix \`@generic@\' indicates an overloaded function that + -- is a generalized version of a "Prelude" function. + GenericLength, sGenericLength, + -- * Defunctionalization symbols NilSym0, (:$), (:$$), (:$$$), (:++$$$), (:++$$), (:++$), HeadSym0, HeadSym1, LastSym0, LastSym1, TailSym0, TailSym1, InitSym0, InitSym1, NullSym0, NullSym1, + LengthSym0, LengthSym1, MapSym0, MapSym1, MapSym2, ReverseSym0, ReverseSym1, IntersperseSym0, IntersperseSym1, IntersperseSym2, IntercalateSym0, IntercalateSym1, IntercalateSym2, + TransposeSym0, TransposeSym1, SubsequencesSym0, SubsequencesSym1, PermutationsSym0, PermutationsSym1, @@ -122,6 +154,10 @@ AndSym0, AndSym1, OrSym0, OrSym1, Any_Sym0, Any_Sym1, Any_Sym2, AllSym0, AllSym1, AllSym2, + SumSym0, SumSym1, + ProductSym0, ProductSym1, + MaximumSym0, MaximumSym1, + MinimumSym0, MinimumSym1, ScanlSym0, ScanlSym1, ScanlSym2, ScanlSym3, Scanl1Sym0, Scanl1Sym1, Scanl1Sym2, @@ -131,8 +167,19 @@ MapAccumLSym0, MapAccumLSym1, MapAccumLSym2, MapAccumLSym3, MapAccumRSym0, MapAccumRSym1, MapAccumRSym2, MapAccumRSym3, + ReplicateSym0, ReplicateSym1, ReplicateSym2, + UnfoldrSym0, UnfoldrSym1, UnfoldrSym2, + TakeSym0, TakeSym1, TakeSym2, + DropSym0, DropSym1, DropSym2, + SplitAtSym0, SplitAtSym1, SplitAtSym2, + TakeWhileSym0, TakeWhileSym1, TakeWhileSym2, + DropWhileSym0, DropWhileSym1, DropWhileSym2, + DropWhileEndSym0, DropWhileEndSym1, DropWhileEndSym2, + SpanSym0, SpanSym1, SpanSym2, + BreakSym0, BreakSym1, BreakSym2, + GroupSym0, GroupSym1, InitsSym0, InitsSym1, TailsSym0, TailsSym1, IsPrefixOfSym0, IsPrefixOfSym1, IsPrefixOfSym2, @@ -141,7 +188,18 @@ ElemSym0, ElemSym1, ElemSym2, NotElemSym0, NotElemSym1, NotElemSym2, + LookupSym0, LookupSym1, LookupSym2, + FindSym0, FindSym1, FindSym2, + FilterSym0, FilterSym1, FilterSym2, + PartitionSym0, PartitionSym1, PartitionSym2, + + (:!!$), (:!!$$), (:!!$$$), + ElemIndexSym0, ElemIndexSym1, ElemIndexSym2, + ElemIndicesSym0, ElemIndicesSym1, ElemIndicesSym2, + FindIndexSym0, FindIndexSym1, FindIndexSym2, + FindIndicesSym0, FindIndicesSym1, FindIndicesSym2, + ZipSym0, ZipSym1, ZipSym2, Zip3Sym0, Zip3Sym1, Zip3Sym2, Zip3Sym3, ZipWithSym0, ZipWithSym1, ZipWithSym2, ZipWithSym3, @@ -153,19 +211,28 @@ Unzip6Sym0, Unzip6Sym1, Unzip7Sym0, Unzip7Sym1, + NubSym0, NubSym1, DeleteSym0, DeleteSym1, DeleteSym2, (:\\$), (:\\$$), (:\\$$$), + UnionSym0, UnionSym1, UnionSym2, + IntersectSym0, IntersectSym1, IntersectSym2, - -- InsertSym0, InsertSym1, InsertSym2, - -- SortSym0, SortSym1, + InsertSym0, InsertSym1, InsertSym2, + SortSym0, SortSym1, + NubBySym0, NubBySym1, NubBySym2, DeleteBySym0, DeleteBySym1, DeleteBySym2, DeleteBySym3, DeleteFirstsBySym0, DeleteFirstsBySym1, DeleteFirstsBySym2, DeleteFirstsBySym3, + UnionBySym0, UnionBySym1, UnionBySym2, UnionBySym3, + IntersectBySym0, IntersectBySym1, IntersectBySym2, IntersectBySym3, + GroupBySym0, GroupBySym1, GroupBySym2, SortBySym0, SortBySym1, SortBySym2, InsertBySym0, InsertBySym1, InsertBySym2, InsertBySym3, MaximumBySym0, MaximumBySym1, MaximumBySym2, MinimumBySym0, MinimumBySym1, MinimumBySym2, + + GenericLengthSym0, GenericLengthSym1 ) where import Data.Singletons @@ -175,6 +242,11 @@ import Data.Singletons.Prelude.Base import Data.Singletons.Prelude.Bool import Data.Singletons.Prelude.Eq +import Data.Singletons.Prelude.Maybe +import Data.Singletons.Prelude.Tuple +import Data.Singletons.Prelude.Num +import Data.Singletons.Prelude.Ord +import Data.Maybe $(singletons [d| any_ :: (a -> Bool) -> [a] -> Bool @@ -483,5 +555,244 @@ GT -> y EQ -> x LT -> x + + filter :: (a -> Bool) -> [a] -> [a] + filter _p [] = [] + filter p (x:xs) = if p x then x : filter p xs else filter p xs + + find :: (a -> Bool) -> [a] -> Maybe a + find p = listToMaybe . filter p + +-- These three rely on findIndices, which does not promote. +-- Since we have our own implementation of findIndices these are perfectly valid + elemIndex :: Eq a => a -> [a] -> Maybe Nat + elemIndex x = findIndex (x==) + + elemIndices :: Eq a => a -> [a] -> [Nat] + elemIndices x = findIndices (x==) + + findIndex :: (a -> Bool) -> [a] -> Maybe Nat + findIndex p = listToMaybe . findIndices p + +-- Uses list comprehensions, infinite lists and and Ints +-- findIndices :: (a -> Bool) -> [a] -> [Int] +-- findIndices p xs = [ i | (x,i) <- zip xs [0..], p x] + + findIndices :: (a -> Bool) -> [a] -> [Nat] + findIndices p xs = map snd (filter (\(x,_) -> p x) + (zip xs (buildList 0 xs))) + where buildList :: Nat -> [b] -> [Nat] + buildList _ [] = [] + buildList a (_:rest) = a : buildList (a+1) rest + + -- Relies on intersectBy, which does not singletonize + intersect :: (Eq a) => [a] -> [a] -> [a] + intersect = intersectBy (==) + +-- Uses list comprehensions. +-- intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a] +-- intersectBy _ [] [] = [] +-- intersectBy _ [] (_:_) = [] +-- intersectBy _ (_:_) [] = [] +-- intersectBy eq xs ys = [x | x <- xs, any_ (eq x) ys] + + intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a] + intersectBy _ [] [] = [] + intersectBy _ [] (_:_) = [] + intersectBy _ (_:_) [] = [] + intersectBy eq xs@(_:_) ys@(_:_) = filter (\x -> any_ (eq x) ys) xs + + takeWhile :: (a -> Bool) -> [a] -> [a] + takeWhile _ [] = [] + takeWhile p (x:xs) = if p x then x : takeWhile p xs else [] + + dropWhile :: (a -> Bool) -> [a] -> [a] + dropWhile _ [] = [] + dropWhile p xs@(x:xs') = if p x then dropWhile p xs' else xs + + dropWhileEnd :: (a -> Bool) -> [a] -> [a] + dropWhileEnd p = foldr (\x xs -> if p x && null xs then [] else x : xs) [] + + span :: (a -> Bool) -> [a] -> ([a],[a]) + span _ xs@[] = (xs, xs) + span p xs@(x:xs') = if p x then let (ys,zs) = span p xs' in (x:ys,zs) + else ([], xs) + + break :: (a -> Bool) -> [a] -> ([a],[a]) + break _ xs@[] = (xs, xs) + break p xs@(x:xs') = if p x then ([],xs) + else let (ys,zs) = break p xs' in (x:ys,zs) + +-- Can't be promoted because of limitations of Int promotion +-- Below is a re-implementation using Nat +-- take :: Int -> [a] -> [a] +-- take n _ | n <= 0 = [] +-- take _ [] = [] +-- take n (x:xs) = x : take (n-1) xs + +-- drop :: Int -> [a] -> [a] +-- drop n xs | n <= 0 = xs +-- drop _ [] = [] +-- drop n (_:xs) = drop (n-1) xs + +-- splitAt :: Int -> [a] -> ([a],[a]) +-- splitAt n xs = (take n xs, drop n xs) + + take :: Nat -> [a] -> [a] + take _ [] = [] + take n (x:xs) = if n == 0 then [] else x : take (n-1) xs + + drop :: Nat -> [a] -> [a] + drop _ [] = [] + drop n (x:xs) = if n == 0 then x:xs else drop (n-1) xs + + splitAt :: Nat -> [a] -> ([a],[a]) + splitAt n xs = (take n xs, drop n xs) + + group :: Eq a => [a] -> [[a]] + group xs = groupBy (==) xs + + maximum :: (Ord a) => [a] -> a + maximum [] = error "Data.Singletons.List.maximum: empty list" + maximum xs@(_:_) = foldl1 max xs + + minimum :: (Ord a) => [a] -> a + minimum [] = error "Data.Singletons.List.minimum: empty list" + minimum xs@(_:_) = foldl1 min xs + + insert :: Ord a => a -> [a] -> [a] + insert e ls = insertBy (compare) e ls + + sort :: (Ord a) => [a] -> [a] + sort = sortBy compare + + groupBy :: (a -> a -> Bool) -> [a] -> [[a]] + groupBy _ [] = [] + groupBy eq (x:xs) = (x:ys) : groupBy eq zs + where (ys,zs) = span (eq x) xs + + lookup :: (Eq a) => a -> [(a,b)] -> Maybe b + lookup _key [] = Nothing + lookup key ((x,y):xys) = if key == x then Just y else lookup key xys + + partition :: (a -> Bool) -> [a] -> ([a],[a]) + partition p xs = foldr (select p) ([],[]) xs + + -- Lazy pattern removed from select + select :: (a -> Bool) -> a -> ([a], [a]) -> ([a], [a]) + select p x (ts,fs) = if p x then (x:ts,fs) else (ts, x:fs) + +-- Can't be promoted because of limitations of Int promotion +-- Below is a re-implementation using Nat +-- sum :: (Num a) => [a] -> a +-- sum l = sum' l 0 +-- where +-- sum' [] a = a +-- sum' (x:xs) a = sum' xs (a+x) +-- +-- product :: (Num a) => [a] -> a +-- product l = prod l 1 +-- where +-- prod [] a = a +-- prod (x:xs) a = prod xs (a*x) + + sum :: forall a. Num a => [a] -> a + sum l = sum' l 0 + where + sum' :: [a] -> a -> a + sum' [] a = a + sum' (x:xs) a = sum' xs (a+x) + + product :: forall a. Num a => [a] -> a + product l = prod l 1 + where + prod :: [a] -> a -> a + prod [] a = a + prod (x:xs) a = prod xs (a*x) + + +-- Can't be promoted because of limitations of Int promotion +-- Below is a re-implementation using Nat +-- length :: [a] -> Int +-- length l = lenAcc l 0# +-- +-- lenAcc :: [a] -> Int# -> Int +-- lenAcc [] a# = I# a# +-- lenAcc (_:xs) a# = lenAcc xs (a# +# 1#) +-- +-- incLen :: a -> (Int# -> Int) -> Int# -> Int +-- incLen _ g x = g (x +# 1#) + + length :: [a] -> Nat + length [] = 0 + length (_:xs) = 1 + length xs + +-- Functions working on infinite lists don't promote because they create +-- infinite types. replicate also uses integers, but luckily it can be rewritten +-- iterate :: (a -> a) -> a -> [a] +-- iterate f x = x : iterate f (f x) +-- +-- repeat :: a -> [a] +-- repeat x = xs where xs = x : xs +-- +-- replicate :: Int -> a -> [a] +-- replicate n x = take n (repeat x) +-- +-- cycle :: [a] -> [a] +-- cycle [] = error "Data.Singletons.List.cycle: empty list" +-- cycle xs = xs' where xs' = xs ++ xs' + + replicate :: Nat -> a -> [a] + replicate n x = if n == 0 then [] else x : replicate (n-1) x + +-- Uses list comprehensions +-- transpose :: [[a]] -> [[a]] +-- transpose [] = [] +-- transpose ([] : xss) = transpose xss +-- transpose ((x:xs) : xss) = (x : [h | (h:_) <- xss]) : transpose (xs : [ t | (_:t) <- xss]) + + transpose :: [[a]] -> [[a]] + transpose [] = [] + transpose ([] : xss) = transpose xss + transpose ((x:xs) : xss) = (x : (map head xss)) : transpose (xs : (map tail xss)) + +-- Can't be promoted because of limitations of Int promotion. +-- Below is a re-implementation using Nat +-- (!!) :: [a] -> Int -> a +-- xs !! n | n < 0 = error "Data.Singletons.List.!!: negative index" +-- [] !! _ = error "Data.Singletons.List.!!: index too large" +-- (x:_) !! 0 = x +-- (_:xs) !! n = xs !! (n-1) + + (!!) :: [a] -> Nat -> a + [] !! _ = error "Data.Singletons.List.!!: index too large" + (x:xs) !! n = if n == 0 then x else xs !! (n-1) + + nub :: forall a. (Eq a) => [a] -> [a] + nub l = nub' l [] + where + nub' :: [a] -> [a] -> [a] + nub' [] _ = [] + nub' (x:xs) ls = if x `elem` ls then nub' xs ls else x : nub' xs (x:ls) + + nubBy :: (a -> a -> Bool) -> [a] -> [a] + nubBy eq l = nubBy' l [] + where + nubBy' [] _ = [] + nubBy' (y:ys) xs = if elem_by eq y xs then nubBy' ys xs else y : nubBy' ys (y:xs) + + elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool + elem_by _ _ [] = False + elem_by eq y (x:xs) = y `eq` x || elem_by eq y xs + + unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a] + unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs + + union :: (Eq a) => [a] -> [a] -> [a] + union = unionBy (==) + + genericLength :: (Num i) => [a] -> i + genericLength [] = 0 + genericLength (_:xs) = 1 + genericLength xs |])