{-# LANGUAGE CPP, TypeOperators, DataKinds, PolyKinds, TypeFamilies, TemplateHaskell, GADTs, UndecidableInstances, RankNTypes, ScopedTypeVariables, FlexibleContexts #-} #if __GLASGOW_HASKELL__ < 707 {-# OPTIONS_GHC -fno-warn-name-shadowing #-} #endif ----------------------------------------------------------------------------- -- | -- Module : Data.Singletons.Prelude.List -- Copyright : (C) 2013-2014 Richard Eisenberg, Jan Stolarek -- License : BSD-style (see LICENSE) -- Maintainer : Richard Eisenberg (eir@cis.upenn.edu) -- Stability : experimental -- Portability : non-portable -- -- Defines functions and datatypes relating to the singleton for '[]', -- including a singletons version of a few of the definitions in @Data.List@. -- -- Because many of these definitions are produced by Template Haskell, -- it is not possible to create proper Haddock documentation. Please look -- up the corresponding operation in @Data.List@. Also, please excuse -- the apparent repeated variable names. This is due to an interaction -- between Template Haskell and Haddock. -- ---------------------------------------------------------------------------- module Data.Singletons.Prelude.List ( -- * The singleton for lists Sing(SNil, SCons), -- | Though Haddock doesn't show it, the 'Sing' instance above declares -- constructors -- -- > SNil :: Sing '[] -- > SCons :: Sing (h :: k) -> Sing (t :: [k]) -> Sing (h ': t) SList, -- | 'SList' is a kind-restricted synonym for 'Sing': @type SList (a :: [k]) = Sing a@ -- * Basic functions (:++), (%:++), Head, sHead, Last, sLast, Tail, sTail, Init, sInit, Null, sNull, -- * List transformations Map, sMap, Reverse, sReverse, Intersperse, sIntersperse, Intercalate, sIntercalate, Subsequences, sSubsequences, Permutations, sPermutations, -- * Reducing lists (folds) Foldl, sFoldl, Foldl', sFoldl', Foldl1, sFoldl1, Foldl1', sFoldl1', Foldr, sFoldr, Foldr1, sFoldr1, -- ** Special folds Concat, sConcat, ConcatMap, sConcatMap, And, sAnd, Or, sOr, Any_, sAny_, All, sAll, any_, -- equivalent of Data.List `any`. Avoids name clash with Any type -- * Building lists -- ** Scans Scanl, sScanl, Scanl1, sScanl1, Scanr, sScanr, Scanr1, sScanr1, -- ** Accumulating maps MapAccumL, sMapAccumL, MapAccumR, sMapAccumR, -- ** Unfolding Unfoldr, sUnfoldr, -- * Sublists -- ** Extracting sublists Inits, sInits, Tails, sTails, -- ** Predicates IsPrefixOf, sIsPrefixOf, IsSuffixOf, sIsSuffixOf, IsInfixOf, sIsInfixOf, -- * Searching lists -- ** Searching by equality Elem, sElem, NotElem, sNotElem, -- * Zipping and unzipping lists Zip, sZip, Zip3, sZip3, ZipWith, sZipWith, ZipWith3, sZipWith3, Unzip, sUnzip, Unzip3, sUnzip3, Unzip4, sUnzip4, Unzip5, sUnzip5, Unzip6, sUnzip6, Unzip7, sUnzip7, -- * Special lists -- ** \"Set\" operations Delete, sDelete, (:\\), (%:\\), -- ** Ordered lists -- Insert, sInsert, Sort, sSort, -- * Generalized functions -- ** The \"@By@\" operations DeleteBy, sDeleteBy, DeleteFirstsBy, sDeleteFirstsBy, SortBy, sSortBy, InsertBy, sInsertBy, MaximumBy, sMaximumBy, MinimumBy, sMinimumBy, -- * Defunctionalization symbols (:$), (:$$), (:$$$), NilSym0, ConsSym0, ConsSym1, ConsSym2, (:++$$), (:++$), HeadSym0, HeadSym1, LastSym0, LastSym1, TailSym0, TailSym1, InitSym0, InitSym1, NullSym0, NullSym1, MapSym0, MapSym1, MapSym2, ReverseSym0, ReverseSym1, IntersperseSym0, IntersperseSym1, IntersperseSym2, IntercalateSym0, IntercalateSym1, IntercalateSym2, SubsequencesSym0, SubsequencesSym1, PermutationsSym0, PermutationsSym1, FoldlSym0, FoldlSym1, FoldlSym2, FoldlSym3, Foldl'Sym0, Foldl'Sym1, Foldl'Sym2, Foldl'Sym3, Foldl1Sym0, Foldl1Sym1, Foldl1Sym2, Foldl1'Sym0, Foldl1'Sym1, Foldl1'Sym2, FoldrSym0, FoldrSym1, FoldrSym2, FoldrSym3, Foldr1Sym0, Foldr1Sym1, Foldr1Sym2, ConcatSym0, ConcatSym1, ConcatMapSym0, ConcatMapSym1, ConcatMapSym2, AndSym0, AndSym1, OrSym0, OrSym1, Any_Sym0, Any_Sym1, Any_Sym2, AllSym0, AllSym1, AllSym2, ScanlSym0, ScanlSym1, ScanlSym2, ScanlSym3, Scanl1Sym0, Scanl1Sym1, Scanl1Sym2, ScanrSym0, ScanrSym1, ScanrSym2, ScanrSym3, Scanr1Sym0, Scanr1Sym1, Scanr1Sym2, MapAccumLSym0, MapAccumLSym1, MapAccumLSym2, MapAccumLSym3, MapAccumRSym0, MapAccumRSym1, MapAccumRSym2, MapAccumRSym3, UnfoldrSym0, UnfoldrSym1, UnfoldrSym2, InitsSym0, InitsSym1, TailsSym0, TailsSym1, IsPrefixOfSym0, IsPrefixOfSym1, IsPrefixOfSym2, IsSuffixOfSym0, IsSuffixOfSym1, IsSuffixOfSym2, IsInfixOfSym0, IsInfixOfSym1, IsInfixOfSym2, ElemSym0, ElemSym1, ElemSym2, NotElemSym0, NotElemSym1, NotElemSym2, ZipSym0, ZipSym1, ZipSym2, Zip3Sym0, Zip3Sym1, Zip3Sym2, Zip3Sym3, ZipWithSym0, ZipWithSym1, ZipWithSym2, ZipWithSym3, ZipWith3Sym0, ZipWith3Sym1, ZipWith3Sym2, ZipWith3Sym3, UnzipSym0, UnzipSym1, Unzip3Sym0, Unzip3Sym1, Unzip4Sym0, Unzip4Sym1, Unzip5Sym0, Unzip5Sym1, Unzip6Sym0, Unzip6Sym1, Unzip7Sym0, Unzip7Sym1, DeleteSym0, DeleteSym1, DeleteSym2, (:\\$), (:\\$$), (:\\$$$), -- InsertSym0, InsertSym1, InsertSym2, -- SortSym0, SortSym1, DeleteBySym0, DeleteBySym1, DeleteBySym2, DeleteBySym3, DeleteFirstsBySym0, DeleteFirstsBySym1, DeleteFirstsBySym2, DeleteFirstsBySym3, SortBySym0, SortBySym1, SortBySym2, InsertBySym0, InsertBySym1, InsertBySym2, InsertBySym3, MaximumBySym0, MaximumBySym1, MaximumBySym2, MinimumBySym0, MinimumBySym1, MinimumBySym2, ) where import Data.Singletons import Data.Singletons.Prelude.Instances import Data.Singletons.Single import Data.Singletons.TypeLits import Data.Singletons.Prelude.Base import Data.Singletons.Prelude.Bool import Data.Singletons.Prelude.Eq $(singletons [d| any_ :: (a -> Bool) -> [a] -> Bool any_ _ [] = False any_ p (x:xs) = p x || any_ p xs |]) $(singletonsOnly [d| head :: [a] -> a head (a : _) = a head [] = error "Data.Singletons.List.head: empty list" last :: [a] -> a last [] = error "Data.Singletons.List.last: empty list" last (x:xs) = last' x xs where last' :: a -> [a] -> a last' y [] = y last' _ (y:ys) = last' y ys tail :: [a] -> [a] tail (_ : t) = t tail [] = error "Data.Singletons.List.tail: empty list" init :: [a] -> [a] init [] = error "Data.Singletons.List.init: empty list" init (x:xs) = init' x xs where init' :: a -> [a] -> [a] init' _ [] = [] init' y (z:zs) = y : init' z zs null :: [a] -> Bool null [] = True null (_:_) = False reverse :: [a] -> [a] reverse l = rev l [] where rev :: [a] -> [a] -> [a] rev [] a = a rev (x:xs) a = rev xs (x:a) intersperse :: a -> [a] -> [a] intersperse _ [] = [] intersperse sep (x:xs) = x : prependToAll sep xs intercalate :: [a] -> [[a]] -> [a] intercalate xs xss = concat (intersperse xs xss) subsequences :: [a] -> [[a]] subsequences xs = [] : nonEmptySubsequences xs nonEmptySubsequences :: [a] -> [[a]] nonEmptySubsequences [] = [] nonEmptySubsequences (x:xs) = [x] : foldr f [] (nonEmptySubsequences xs) where f ys r = ys : (x : ys) : r prependToAll :: a -> [a] -> [a] prependToAll _ [] = [] prependToAll sep (x:xs) = sep : x : prependToAll sep xs permutations :: [a] -> [[a]] permutations xs0 = xs0 : perms xs0 [] where perms [] _ = [] perms (t:ts) is = foldr interleave (perms ts (t:is)) (permutations is) where interleave xs r = let (_,zs) = interleave' id xs r in zs interleave' _ [] r = (ts, r) interleave' f (y:ys) r = let (us,zs) = interleave' (f . (y:)) ys r in (y:us, f (t:y:us) : zs) foldl :: (b -> a -> b) -> b -> [a] -> b foldl f z0 xs0 = lgo z0 xs0 where lgo :: b -> [a] -> b lgo z [] = z lgo z (x:xs) = lgo (f z x) xs foldl' :: forall a b. (b -> a -> b) -> b -> [a] -> b foldl' f z0 xs0 = lgo z0 xs0 where lgo :: b -> [a] -> b lgo z [] = z lgo z (x:xs) = let z' = f z x in z' `seq` lgo z' xs foldl1 :: (a -> a -> a) -> [a] -> a foldl1 f (x:xs) = foldl f x xs foldl1 _ [] = error "Data.Singletons.List.foldl1: empty list" foldl1' :: (a -> a -> a) -> [a] -> a foldl1' f (x:xs) = foldl' f x xs foldl1' _ [] = error "Data.Singletons.List.foldl1': empty list" foldr1 :: (a -> a -> a) -> [a] -> a foldr1 _ [x] = x foldr1 f (x:xs@(_:_)) = f x (foldr1 f xs) foldr1 _ [] = error "Data.Singletons.List.foldr1: empty list" concat :: [[a]] -> [a] concat = foldr (++) [] concatMap :: (a -> [b]) -> [a] -> [b] concatMap f = foldr ((++) . f) [] and :: [Bool] -> Bool and [] = True and (x:xs) = x && and xs or :: [Bool] -> Bool or [] = False or (x:xs) = x || or xs all :: (a -> Bool) -> [a] -> Bool all _ [] = True all p (x:xs) = p x && all p xs scanl :: (b -> a -> b) -> b -> [a] -> [b] scanl f q ls = q : (case ls of [] -> [] x:xs -> scanl f (f q x) xs) scanl1 :: (a -> a -> a) -> [a] -> [a] scanl1 f (x:xs) = scanl f x xs scanl1 _ [] = [] scanr :: (a -> b -> b) -> b -> [a] -> [b] scanr _ q0 [] = [q0] scanr f q0 (x:xs) = case scanr f q0 xs of [] -> error "Data.Singletons.List.scanr: empty list" (q:qs) -> f x q : (q:qs) scanr1 :: (a -> a -> a) -> [a] -> [a] scanr1 _ [] = [] scanr1 _ [x] = [x] scanr1 f (x:xs@(_:_)) = case scanr1 f xs of [] -> error "Data.Singletons.List.scanr1: empty list" (q:qs) -> f x q : (q:qs) mapAccumL :: (acc -> x -> (acc, y)) -> acc -> [x] -> (acc, [y]) mapAccumL _ s [] = (s, []) mapAccumL f s (x:xs) = (s'',y:ys) where (s', y ) = f s x (s'',ys) = mapAccumL f s' xs mapAccumR :: (acc -> x -> (acc, y)) -> acc -> [x] -> (acc, [y]) mapAccumR _ s [] = (s, []) mapAccumR f s (x:xs) = (s'', y:ys) where (s'',y ) = f s' x (s', ys) = mapAccumR f s xs unfoldr :: (b -> Maybe (a, b)) -> b -> [a] unfoldr f b = case f b of Just (a,new_b) -> a : unfoldr f new_b Nothing -> [] inits :: [a] -> [[a]] inits xs = [] : case xs of [] -> [] x : xs' -> map (x :) (inits xs') tails :: [a] -> [[a]] tails xs = xs : case xs of [] -> [] _ : xs' -> tails xs' isPrefixOf :: (Eq a) => [a] -> [a] -> Bool isPrefixOf [] [] = True isPrefixOf [] (_:_) = True isPrefixOf (_:_) [] = False isPrefixOf (x:xs) (y:ys)= x == y && isPrefixOf xs ys isSuffixOf :: (Eq a) => [a] -> [a] -> Bool isSuffixOf x y = reverse x `isPrefixOf` reverse y isInfixOf :: (Eq a) => [a] -> [a] -> Bool isInfixOf needle haystack = any_ (isPrefixOf needle) (tails haystack) elem :: (Eq a) => a -> [a] -> Bool elem _ [] = False elem x (y:ys) = x==y || elem x ys notElem :: (Eq a) => a -> [a] -> Bool notElem _ [] = True notElem x (y:ys) = x /= y && notElem x ys zip :: [a] -> [b] -> [(a,b)] zip (x:xs) (y:ys) = (x,y) : zip xs ys zip [] [] = [] zip (_:_) [] = [] zip [] (_:_) = [] zip3 :: [a] -> [b] -> [c] -> [(a,b,c)] zip3 (a:as) (b:bs) (c:cs) = (a,b,c) : zip3 as bs cs zip3 [] [] [] = [] zip3 [] [] (_:_) = [] zip3 [] (_:_) [] = [] zip3 [] (_:_) (_:_) = [] zip3 (_:_) [] [] = [] zip3 (_:_) [] (_:_) = [] zip3 (_:_) (_:_) [] = [] zipWith :: (a -> b -> c) -> [a] -> [b] -> [c] zipWith f (x:xs) (y:ys) = f x y : zipWith f xs ys zipWith _ [] [] = [] zipWith _ (_:_) [] = [] zipWith _ [] (_:_) = [] zipWith3 :: (a->b->c->d) -> [a]->[b]->[c]->[d] zipWith3 z (a:as) (b:bs) (c:cs) = z a b c : zipWith3 z as bs cs zipWith3 _ [] [] [] = [] zipWith3 _ [] [] (_:_) = [] zipWith3 _ [] (_:_) [] = [] zipWith3 _ [] (_:_) (_:_) = [] zipWith3 _ (_:_) [] [] = [] zipWith3 _ (_:_) [] (_:_) = [] zipWith3 _ (_:_) (_:_) [] = [] unzip :: [(a,b)] -> ([a],[b]) unzip xs = foldr (\(a,b) (as,bs) -> (a:as,b:bs)) ([],[]) xs -- Lazy patterns removed from unzip unzip3 :: [(a,b,c)] -> ([a],[b],[c]) unzip3 xs = foldr (\(a,b,c) (as,bs,cs) -> (a:as,b:bs,c:cs)) ([],[],[]) xs unzip4 :: [(a,b,c,d)] -> ([a],[b],[c],[d]) unzip4 xs = foldr (\(a,b,c,d) (as,bs,cs,ds) -> (a:as,b:bs,c:cs,d:ds)) ([],[],[],[]) xs unzip5 :: [(a,b,c,d,e)] -> ([a],[b],[c],[d],[e]) unzip5 xs = foldr (\(a,b,c,d,e) (as,bs,cs,ds,es) -> (a:as,b:bs,c:cs,d:ds,e:es)) ([],[],[],[],[]) xs unzip6 :: [(a,b,c,d,e,f)] -> ([a],[b],[c],[d],[e],[f]) unzip6 xs = foldr (\(a,b,c,d,e,f) (as,bs,cs,ds,es,fs) -> (a:as,b:bs,c:cs,d:ds,e:es,f:fs)) ([],[],[],[],[],[]) xs unzip7 :: [(a,b,c,d,e,f,g)] -> ([a],[b],[c],[d],[e],[f],[g]) unzip7 xs = foldr (\(a,b,c,d,e,f,g) (as,bs,cs,ds,es,fs,gs) -> (a:as,b:bs,c:cs,d:ds,e:es,f:fs,g:gs)) ([],[],[],[],[],[],[]) xs -- We can't promote any of these functions because at the type level -- String literals are no longer considered to be lists of Chars, so -- there is mismatch between term-level and type-level semantics -- lines :: String -> [String] -- lines "" = [] -- lines s = cons (case break (== '\n') s of -- (l, s') -> (l, case s' of -- [] -> [] -- _:s'' -> lines s'')) -- where -- cons ~(h, t) = h : t -- -- unlines :: [String] -> String -- unlines = concatMap (++ "\n") -- -- words :: String -> [String] -- words s = case dropWhile isSpace s of -- "" -> [] -- s' -> w : words s'' -- where (w, s'') = -- break isSpace s' -- -- unwords :: [String] -> String -- unwords [] = "" -- unwords ws = foldr1 (\w s -> w ++ ' ':s) ws delete :: (Eq a) => a -> [a] -> [a] delete = deleteBy (==) (\\) :: (Eq a) => [a] -> [a] -> [a] (\\) = foldl (flip delete) deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a] deleteBy _ _ [] = [] deleteBy eq x (y:ys) = if x `eq` y then ys else y : deleteBy eq x ys deleteFirstsBy :: (a -> a -> Bool) -> [a] -> [a] -> [a] deleteFirstsBy eq = foldl (flip (deleteBy eq)) sortBy :: (a -> a -> Ordering) -> [a] -> [a] sortBy cmp = foldr (insertBy cmp) [] insertBy :: (a -> a -> Ordering) -> a -> [a] -> [a] insertBy _ x [] = [x] insertBy cmp x ys@(y:ys') = case cmp x y of GT -> y : insertBy cmp x ys' LT -> x : ys EQ -> x : ys maximumBy :: (a -> a -> Ordering) -> [a] -> a maximumBy _ [] = error "Data.Singletons.List.maximumBy: empty list" maximumBy cmp xs@(_:_) = foldl1 maxBy xs where maxBy x y = case cmp x y of GT -> x EQ -> y LT -> y minimumBy :: (a -> a -> Ordering) -> [a] -> a minimumBy _ [] = error "Data.Singletons.List.minimumBy: empty list" minimumBy cmp xs@(_:_) = foldl1 minBy xs where minBy x y = case cmp x y of GT -> y EQ -> x LT -> x |]) -- The symbol []$ is clearly malformed, so we have to name this symbol -- NilSym0 type NilSym0 = '[] -- If Nil has an alphanumeric symbol, we wouldn't want to leave Cons out... type ConsSym0 = (:$) type ConsSym1 = (:$$) type ConsSym2 a b = (:$$$) a b