{-# LANGUAGE TypeOperators, DataKinds, PolyKinds, TypeFamilies,
             TemplateHaskell, GADTs, UndecidableInstances, RankNTypes,
             ScopedTypeVariables, FlexibleContexts, CPP #-}
{-# OPTIONS_GHC -O0 #-}
#if __GLASGOW_HASKELL__ >= 711
{-# LANGUAGE TypeInType #-}
#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, Length, sLength,

   -- * List transformations
  Map, sMap, Reverse, sReverse, Intersperse, sIntersperse,
  Intercalate, sIntercalate, Transpose, sTranspose,
  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,
  Sum, sSum, Product, sProduct, Maximum, sMaximum,
  Minimum, sMinimum,
  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,

  -- ** 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
  IsPrefixOf, sIsPrefixOf, IsSuffixOf, sIsSuffixOf, IsInfixOf, sIsInfixOf,

  -- * Searching lists

  -- ** Searching by equality
  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,
  Unzip5, sUnzip5, Unzip6, sUnzip6, Unzip7, sUnzip7,

  -- * Special lists

  -- ** \"Set\" operations
  Nub, sNub, Delete, sDelete, (:\\), (%:\\),
  Union, sUnion, Intersect, sIntersect,

  -- ** Ordered lists
  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,

  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,
  SumSym0, SumSym1,
  ProductSym0, ProductSym1,
  MaximumSym0, MaximumSym1,
  MinimumSym0, MinimumSym1,

  ScanlSym0, ScanlSym1, ScanlSym2, ScanlSym3,
  Scanl1Sym0, Scanl1Sym1, Scanl1Sym2,
  ScanrSym0, ScanrSym1, ScanrSym2, ScanrSym3,
  Scanr1Sym0, Scanr1Sym1, Scanr1Sym2,

  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,
  IsSuffixOfSym0, IsSuffixOfSym1, IsSuffixOfSym2,
  IsInfixOfSym0, IsInfixOfSym1, IsInfixOfSym2,

  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,
  ZipWith3Sym0, ZipWith3Sym1, ZipWith3Sym2, ZipWith3Sym3, ZipWith3Sym4,
  UnzipSym0, UnzipSym1,
  Unzip3Sym0, Unzip3Sym1,
  Unzip4Sym0, Unzip4Sym1,
  Unzip5Sym0, Unzip5Sym1,
  Unzip6Sym0, Unzip6Sym1,
  Unzip7Sym0, Unzip7Sym1,

  NubSym0, NubSym1,
  DeleteSym0, DeleteSym1, DeleteSym2,
  (:\\$), (:\\$$), (:\\$$$),
  UnionSym0, UnionSym1, UnionSym2,
  IntersectSym0, IntersectSym1, IntersectSym2,

  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
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
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
  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]      =  x
  last (_:x:xs) =  last (x:xs)

  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'           :: 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)
  infix 5 \\      -- This comment is necessary so CPP doesn't treat the
                  -- trailing backslash as a line splice. Urgh.

  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

  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

  |])