{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Type-level non-empty lists
module Data.SOP.NonEmpty
  ( NonEmpty (..)

    -- * Proofs
  , IsNonEmpty (..)
  , ProofNonEmpty (..)
  , checkIsNonEmpty

    -- * Working with 'NonEmpty'
  , nonEmptyFromList
  , nonEmptyHead
  , nonEmptyInit
  , nonEmptyLast
  , nonEmptyMapOne
  , nonEmptyMapTwo
  , nonEmptyStrictPrefixes
  , nonEmptyToList
  ) where

import Control.Applicative
import qualified Data.Foldable as Foldable
import Data.Kind (Type)
import Data.Proxy
import Data.SOP.Sing

{-------------------------------------------------------------------------------
  NonEmpty
-------------------------------------------------------------------------------}

-- | Non-empty variation on 'AtMost'
type NonEmpty :: [Type] -> Type -> Type
data NonEmpty xs a where
  NonEmptyOne :: !a -> NonEmpty (x ': xs) a
  NonEmptyCons :: !a -> !(NonEmpty xs a) -> NonEmpty (x ': xs) a

deriving instance Eq a => Eq (NonEmpty xs a)
deriving instance Show a => Show (NonEmpty xs a)
deriving instance Functor (NonEmpty xs)
deriving instance Foldable (NonEmpty xs)
deriving instance Traversable (NonEmpty xs)

instance (IsNonEmpty xs, SListI xs) => Applicative (NonEmpty xs) where
  pure :: forall a. a -> NonEmpty xs a
  pure :: forall a. a -> NonEmpty xs a
pure a
a = case Proxy xs -> ProofNonEmpty xs
forall {a} (xs :: [a]) (proxy :: [a] -> *).
IsNonEmpty xs =>
proxy xs -> ProofNonEmpty xs
forall (proxy :: [*] -> *). proxy xs -> ProofNonEmpty xs
isNonEmpty (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) of
    ProofNonEmpty{} -> Shape xs -> NonEmpty (x : xs) a
forall x (xs' :: [*]). Shape xs' -> NonEmpty (x : xs') a
go Shape xs
forall k (xs :: [k]). SListI xs => Shape xs
shape
   where
    go :: forall x xs'. Shape xs' -> NonEmpty (x : xs') a
    go :: forall x (xs' :: [*]). Shape xs' -> NonEmpty (x : xs') a
go Shape xs'
ShapeNil = a -> NonEmpty (x : xs') a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne a
a
    go (ShapeCons Shape xs
xs') = a -> NonEmpty xs' a -> NonEmpty (x : xs') a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
a (Shape xs -> NonEmpty (x : xs) a
forall x (xs' :: [*]). Shape xs' -> NonEmpty (x : xs') a
go Shape xs
xs')
  <*> :: forall a b. NonEmpty xs (a -> b) -> NonEmpty xs a -> NonEmpty xs b
(<*>) = NonEmpty xs (a -> b) -> NonEmpty xs a -> NonEmpty xs b
forall (xs' :: [*]) a b.
NonEmpty xs' (a -> b) -> NonEmpty xs' a -> NonEmpty xs' b
go
   where
    go :: NonEmpty xs' (a -> b) -> NonEmpty xs' a -> NonEmpty xs' b
    go :: forall (xs' :: [*]) a b.
NonEmpty xs' (a -> b) -> NonEmpty xs' a -> NonEmpty xs' b
go (NonEmptyOne a -> b
f) (NonEmptyOne a
x) = b -> NonEmpty (x : xs) b
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne (a -> b
f a
x)
    go (NonEmptyCons a -> b
f NonEmpty xs (a -> b)
_) (NonEmptyOne a
x) = b -> NonEmpty (x : xs) b
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne (a -> b
f a
x)
    go (NonEmptyOne a -> b
f) (NonEmptyCons a
x NonEmpty xs a
_) = b -> NonEmpty (x : xs) b
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne (a -> b
f a
x)
    go (NonEmptyCons a -> b
f NonEmpty xs (a -> b)
fs) (NonEmptyCons a
x NonEmpty xs a
xs) = b -> NonEmpty xs b -> NonEmpty (x : xs) b
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons (a -> b
f a
x) (NonEmpty xs (a -> b) -> NonEmpty xs a -> NonEmpty xs b
forall (xs' :: [*]) a b.
NonEmpty xs' (a -> b) -> NonEmpty xs' a -> NonEmpty xs' b
go NonEmpty xs (a -> b)
fs NonEmpty xs a
NonEmpty xs a
xs)

{-------------------------------------------------------------------------------
  Working with 'NonEmpty'
-------------------------------------------------------------------------------}

-- | Analogue of 'head'
nonEmptyHead :: NonEmpty xs a -> a
nonEmptyHead :: forall (xs :: [*]) a. NonEmpty xs a -> a
nonEmptyHead (NonEmptyOne a
x) = a
x
nonEmptyHead (NonEmptyCons a
x NonEmpty xs a
_) = a
x

-- | Analogue of 'last'
nonEmptyLast :: NonEmpty xs a -> a
nonEmptyLast :: forall (xs :: [*]) a. NonEmpty xs a -> a
nonEmptyLast = (Maybe (NonEmpty xs a), a) -> a
forall a b. (a, b) -> b
snd ((Maybe (NonEmpty xs a), a) -> a)
-> (NonEmpty xs a -> (Maybe (NonEmpty xs a), a))
-> NonEmpty xs a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
forall (xs :: [*]) a. NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
nonEmptyInit

-- | Analogue of 'init'
nonEmptyInit :: NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
nonEmptyInit :: forall (xs :: [*]) a. NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
nonEmptyInit (NonEmptyOne a
x) = (Maybe (NonEmpty xs a)
forall a. Maybe a
Nothing, a
x)
nonEmptyInit (NonEmptyCons a
x NonEmpty xs a
xs) =
  case NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
forall (xs :: [*]) a. NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
nonEmptyInit NonEmpty xs a
xs of
    (Maybe (NonEmpty xs a)
Nothing, a
final) -> (NonEmpty xs a -> Maybe (NonEmpty xs a)
forall a. a -> Maybe a
Just (a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne a
x), a
final)
    (Just NonEmpty xs a
xs', a
final) -> (NonEmpty xs a -> Maybe (NonEmpty xs a)
forall a. a -> Maybe a
Just (a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
x NonEmpty xs a
xs'), a
final)

-- | Build a 'NonEmpty' from a list. Returns 'Nothing' when the list is empty
-- or when it's longer than @xs@.
nonEmptyFromList :: forall xs a. SListI xs => [a] -> Maybe (NonEmpty xs a)
nonEmptyFromList :: forall (xs :: [*]) a. SListI xs => [a] -> Maybe (NonEmpty xs a)
nonEmptyFromList = SList xs -> [a] -> Maybe (NonEmpty xs a)
forall (xs' :: [*]). SList xs' -> [a] -> Maybe (NonEmpty xs' a)
go (forall (xs :: [*]). SListI xs => SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList @xs)
 where
  go :: forall xs'. SList xs' -> [a] -> Maybe (NonEmpty xs' a)
  go :: forall (xs' :: [*]). SList xs' -> [a] -> Maybe (NonEmpty xs' a)
go SList xs'
s [a]
ys = case (SList xs'
s, [a]
ys) of
    (SList xs'
SCons, [a
y]) -> NonEmpty xs' a -> Maybe (NonEmpty xs' a)
forall a. a -> Maybe a
Just (NonEmpty xs' a -> Maybe (NonEmpty xs' a))
-> NonEmpty xs' a -> Maybe (NonEmpty xs' a)
forall a b. (a -> b) -> a -> b
$ a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne a
y
    (SList xs'
SCons, a
y : [a]
ys') -> a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
y (NonEmpty xs a -> NonEmpty xs' a)
-> Maybe (NonEmpty xs a) -> Maybe (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SList xs -> [a] -> Maybe (NonEmpty xs a)
forall (xs' :: [*]). SList xs' -> [a] -> Maybe (NonEmpty xs' a)
go SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList [a]
ys'
    (SList xs'
SCons, []) -> Maybe (NonEmpty xs' a)
forall a. Maybe a
Nothing
    (SList xs'
SNil, [a]
_) -> Maybe (NonEmpty xs' a)
forall a. Maybe a
Nothing

-- | Convert a 'NonEmpty' to a list.
nonEmptyToList :: forall xs a. NonEmpty xs a -> [a]
nonEmptyToList :: forall (xs :: [*]) a. NonEmpty xs a -> [a]
nonEmptyToList = NonEmpty xs a -> [a]
forall (xs' :: [*]). NonEmpty xs' a -> [a]
go
 where
  go :: forall xs'. NonEmpty xs' a -> [a]
  go :: forall (xs' :: [*]). NonEmpty xs' a -> [a]
go (NonEmptyOne a
x) = [a
x]
  go (NonEmptyCons a
x NonEmpty xs a
xs) = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: NonEmpty xs a -> [a]
forall (xs' :: [*]). NonEmpty xs' a -> [a]
go NonEmpty xs a
xs

-- | A strict prefixes
--
-- >    nonEmptyStrictPrefixes (fromJust (nonEmptyFromList [1..4]))
-- > == [ NonEmptyOne  1
-- >    , NonEmptyCons 1 $ NonEmptyOne  2
-- >    , NonEmptyCons 1 $ NonEmptyCons 2 $ NonEmptyOne 3
-- >    ]
nonEmptyStrictPrefixes :: NonEmpty xs a -> [NonEmpty xs a]
nonEmptyStrictPrefixes :: forall (xs :: [*]) a. NonEmpty xs a -> [NonEmpty xs a]
nonEmptyStrictPrefixes = NonEmpty xs a -> [NonEmpty xs a]
forall (xs :: [*]) a. NonEmpty xs a -> [NonEmpty xs a]
go
 where
  go :: NonEmpty xs a -> [NonEmpty xs a]
  go :: forall (xs :: [*]) a. NonEmpty xs a -> [NonEmpty xs a]
go (NonEmptyOne a
_) = []
  go (NonEmptyCons a
x NonEmpty xs a
xs) = a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne a
x NonEmpty xs a -> [NonEmpty xs a] -> [NonEmpty xs a]
forall a. a -> [a] -> [a]
: (NonEmpty xs a -> NonEmpty xs a)
-> [NonEmpty xs a] -> [NonEmpty xs a]
forall a b. (a -> b) -> [a] -> [b]
map (a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
x) (NonEmpty xs a -> [NonEmpty xs a]
forall (xs :: [*]) a. NonEmpty xs a -> [NonEmpty xs a]
go NonEmpty xs a
xs)

-- | Apply the specified function to exactly one element
nonEmptyMapOne ::
  forall m xs a.
  Alternative m =>
  (a -> m a) -> NonEmpty xs a -> m (NonEmpty xs a)
nonEmptyMapOne :: forall (m :: * -> *) (xs :: [*]) a.
Alternative m =>
(a -> m a) -> NonEmpty xs a -> m (NonEmpty xs a)
nonEmptyMapOne a -> m a
f = NonEmpty xs a -> m (NonEmpty xs a)
forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go
 where
  go :: NonEmpty xs' a -> m (NonEmpty xs' a)
  go :: forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go (NonEmptyOne a
x) = a -> NonEmpty xs' a
a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne (a -> NonEmpty xs' a) -> m a -> m (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
f a
x
  go (NonEmptyCons a
x NonEmpty xs a
xs) =
    [m (NonEmpty xs' a)] -> m (NonEmpty xs' a)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
Foldable.asum
      [ (a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
`NonEmptyCons` NonEmpty xs a
xs) (a -> NonEmpty xs' a) -> m a -> m (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
f a
x
      , a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
x (NonEmpty xs a -> NonEmpty xs' a)
-> m (NonEmpty xs a) -> m (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty xs a -> m (NonEmpty xs a)
forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go NonEmpty xs a
xs
      ]

-- | Variation on 'nonEmptyMapOne' where we try to apply the function to
-- /pairs/ of elements
nonEmptyMapTwo ::
  forall m xs a.
  Alternative m =>
  (a -> m a) -> -- Used when we reached the end of the list
  (a -> a -> m (a, a)) ->
  NonEmpty xs a ->
  m (NonEmpty xs a)
nonEmptyMapTwo :: forall (m :: * -> *) (xs :: [*]) a.
Alternative m =>
(a -> m a)
-> (a -> a -> m (a, a)) -> NonEmpty xs a -> m (NonEmpty xs a)
nonEmptyMapTwo a -> m a
f a -> a -> m (a, a)
g = NonEmpty xs a -> m (NonEmpty xs a)
forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go
 where
  go :: NonEmpty xs' a -> m (NonEmpty xs' a)
  go :: forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go (NonEmptyOne a
x) =
    a -> NonEmpty xs' a
a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne (a -> NonEmpty xs' a) -> m a -> m (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
f a
x
  go (NonEmptyCons a
x xs :: NonEmpty xs a
xs@(NonEmptyOne a
y)) =
    [m (NonEmpty xs' a)] -> m (NonEmpty xs' a)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
Foldable.asum
      [ (\(a
x', a
y') -> a -> NonEmpty (x : xs) a -> NonEmpty (x : x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
x' (a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne a
y')) ((a, a) -> NonEmpty xs' a) -> m (a, a) -> m (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> a -> m (a, a)
g a
x a
y
      , a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
x (NonEmpty xs a -> NonEmpty xs' a)
-> m (NonEmpty xs a) -> m (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty xs a -> m (NonEmpty xs a)
forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go NonEmpty xs a
xs
      ]
  go (NonEmptyCons a
x xs :: NonEmpty xs a
xs@(NonEmptyCons a
y NonEmpty xs a
zs)) =
    [m (NonEmpty xs' a)] -> m (NonEmpty xs' a)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
Foldable.asum
      [ (\(a
x', a
y') -> a -> NonEmpty (x : xs) a -> NonEmpty (x : x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
x' (a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
y' NonEmpty xs a
zs)) ((a, a) -> NonEmpty xs' a) -> m (a, a) -> m (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> a -> m (a, a)
g a
x a
y
      , a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
x (NonEmpty xs a -> NonEmpty xs' a)
-> m (NonEmpty xs a) -> m (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty xs a -> m (NonEmpty xs a)
forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go NonEmpty xs a
xs
      ]

{-------------------------------------------------------------------------------
  Proofs
-------------------------------------------------------------------------------}

type ProofNonEmpty :: [a] -> Type
data ProofNonEmpty xs where
  ProofNonEmpty :: Proxy x -> Proxy xs -> ProofNonEmpty (x ': xs)

class IsNonEmpty xs where
  isNonEmpty :: proxy xs -> ProofNonEmpty xs

instance IsNonEmpty (x ': xs) where
  isNonEmpty :: forall (proxy :: [a] -> *).
proxy (x : xs) -> ProofNonEmpty (x : xs)
isNonEmpty proxy (x : xs)
_ = Proxy x -> Proxy xs -> ProofNonEmpty (x : xs)
forall {k} (x :: k) (xs :: [k]).
Proxy x -> Proxy xs -> ProofNonEmpty (x : xs)
ProofNonEmpty (forall (t :: a). Proxy t
forall {k} (t :: k). Proxy t
Proxy @x) (forall (t :: [a]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs)

checkIsNonEmpty :: forall xs. SListI xs => Proxy xs -> Maybe (ProofNonEmpty xs)
checkIsNonEmpty :: forall {a} (xs :: [a]).
SListI xs =>
Proxy xs -> Maybe (ProofNonEmpty xs)
checkIsNonEmpty Proxy xs
_ = case forall (xs :: [a]). SListI xs => SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList @xs of
  SList xs
SNil -> Maybe (ProofNonEmpty xs)
forall a. Maybe a
Nothing
  SList xs
SCons -> ProofNonEmpty xs -> Maybe (ProofNonEmpty xs)
forall a. a -> Maybe a
Just (ProofNonEmpty xs -> Maybe (ProofNonEmpty xs))
-> ProofNonEmpty xs -> Maybe (ProofNonEmpty xs)
forall a b. (a -> b) -> a -> b
$ Proxy x -> Proxy xs -> ProofNonEmpty (x : xs)
forall {k} (x :: k) (xs :: [k]).
Proxy x -> Proxy xs -> ProofNonEmpty (x : xs)
ProofNonEmpty Proxy x
forall {k} (t :: k). Proxy t
Proxy Proxy xs
forall {k} (t :: k). Proxy t
Proxy