{-# LANGUAGE CPP                      #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE RankNTypes               #-}
{-# LANGUAGE RoleAnnotations          #-}
{-# LANGUAGE Safe                     #-}
#if __GLASGOW_HASKELL__ >= 810
{-# LANGUAGE StandaloneKindSignatures #-}
#endif
module Data.Some.GADT (
    Some(Some),
    mkSome,
    withSome,
    withSomeM,
    mapSome,
    foldSome,
    traverseSome,
    ) where

import Control.Applicative (Applicative (..))
import Control.DeepSeq     (NFData (..))
import Data.Monoid         (Monoid (..))
import Data.Semigroup      (Semigroup (..))

#if __GLASGOW_HASKELL__ >= 810
import Data.Kind (Type)
#endif

import Data.GADT.Compare
import Data.GADT.DeepSeq
import Data.GADT.Show


-- $setup
-- >>> :set -XKindSignatures -XGADTs
-- >>> import Data.GADT.Show
-- >>> import Data.Kind (Type)

-- | Existential. This is type is useful to hide GADTs' parameters.
--
-- >>> data Tag :: Type -> Type where TagInt :: Tag Int; TagBool :: Tag Bool
-- >>> instance GShow Tag where gshowsPrec _ TagInt = showString "TagInt"; gshowsPrec _ TagBool = showString "TagBool"
-- >>> classify s = case s of "TagInt" -> [mkGReadResult TagInt]; "TagBool" -> [mkGReadResult TagBool]; _ -> []
-- >>> instance GRead Tag where greadsPrec _ s = [ (r, rest) | (con, rest) <-  lex s, r <- classify con ]
--
-- You can either use constructor:
--
-- >>> let x = Some TagInt
-- >>> x
-- Some TagInt
--
-- >>> case x of { Some TagInt -> "I"; Some TagBool -> "B" } :: String
-- "I"
--
-- or you can use functions
--
-- >>> let y = mkSome TagBool
-- >>> y
-- Some TagBool
--
-- >>> withSome y $ \y' -> case y' of { TagInt -> "I"; TagBool -> "B" } :: String
-- "B"
--
-- The implementation of 'mapSome' is /safe/.
--
-- >>> let f :: Tag a -> Tag a; f TagInt = TagInt; f TagBool = TagBool
-- >>> mapSome f y
-- Some TagBool
--
-- but you can also use:
--
-- >>> withSome y (mkSome . f)
-- Some TagBool
--
-- >>> read "Some TagBool" :: Some Tag
-- Some TagBool
--
-- >>> read "mkSome TagInt" :: Some Tag
-- Some TagInt
--
#if __GLASGOW_HASKELL__ >= 810
type Some :: (k -> Type) -> Type
#endif
data Some tag where
    Some :: tag a -> Some tag

type role Some representational

-- | Constructor.
mkSome :: tag a -> Some tag
mkSome :: forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
mkSome = forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some

-- | Eliminator.
withSome :: Some tag -> (forall a. tag a -> b) -> b
withSome :: forall {k} (tag :: k -> *) b.
Some tag -> (forall (a :: k). tag a -> b) -> b
withSome (Some tag a
thing) forall (a :: k). tag a -> b
some = forall (a :: k). tag a -> b
some tag a
thing

-- | Monadic 'withSome'.
--
-- @since 1.0.1
withSomeM :: Monad m => m (Some tag) -> (forall a. tag a -> m r) -> m r
withSomeM :: forall {k} (m :: * -> *) (tag :: k -> *) r.
Monad m =>
m (Some tag) -> (forall (a :: k). tag a -> m r) -> m r
withSomeM m (Some tag)
m forall (a :: k). tag a -> m r
k = m (Some tag)
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Some tag
s -> forall {k} (tag :: k -> *) b.
Some tag -> (forall (a :: k). tag a -> b) -> b
withSome Some tag
s forall (a :: k). tag a -> m r
k

-- | @'flip' 'withSome'@
foldSome :: (forall a. tag a -> b) -> Some tag -> b
foldSome :: forall {k} (tag :: k -> *) b.
(forall (a :: k). tag a -> b) -> Some tag -> b
foldSome forall (a :: k). tag a -> b
some (Some tag a
thing) = forall (a :: k). tag a -> b
some tag a
thing

-- | Map over argument.
mapSome :: (forall x. f x -> g x) ->  Some f -> Some g
mapSome :: forall {k} (f :: k -> *) (g :: k -> *).
(forall (x :: k). f x -> g x) -> Some f -> Some g
mapSome forall (x :: k). f x -> g x
nt (Some f a
fx) = forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some (forall (x :: k). f x -> g x
nt f a
fx)

-- | Traverse over argument.
traverseSome :: Functor m => (forall a. f a -> m (g a)) -> Some f -> m (Some g)
traverseSome :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *).
Functor m =>
(forall (a :: k). f a -> m (g a)) -> Some f -> m (Some g)
traverseSome forall (a :: k). f a -> m (g a)
f (Some f a
x) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some (forall (a :: k). f a -> m (g a)
f f a
x)

instance GShow tag => Show (Some tag) where
    showsPrec :: Int -> Some tag -> ShowS
showsPrec Int
p (Some tag a
thing) = Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
10)
        forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Some "
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
gshowsPrec Int
11 tag a
thing

-- |
instance GRead f => Read (Some f) where
    readsPrec :: Int -> ReadS (Some f)
readsPrec Int
p = forall a. Bool -> ReadS a -> ReadS a
readParen (Int
pforall a. Ord a => a -> a -> Bool
>Int
10) forall a b. (a -> b) -> a -> b
$ \String
s ->
        [ (forall {k} (tag :: k -> *) b.
Some tag -> (forall (a :: k). tag a -> b) -> b
getGReadResult Some f
withTag forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some, String
rest')
        | (String
con, String
rest) <- ReadS String
lex String
s
        , String
con forall a. Eq a => a -> a -> Bool
== String
"Some" Bool -> Bool -> Bool
|| String
con forall a. Eq a => a -> a -> Bool
== String
"mkSome"
        , (Some f
withTag, String
rest') <- forall k (t :: k -> *). GRead t => Int -> GReadS t
greadsPrec Int
11 String
rest
        ]

instance GEq tag => Eq (Some tag) where
    Some tag a
x == :: Some tag -> Some tag -> Bool
== Some tag a
y = forall {k} (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Bool
defaultEq tag a
x tag a
y

instance GCompare tag => Ord (Some tag) where
    compare :: Some tag -> Some tag -> Ordering
compare (Some tag a
x) (Some tag a
y) = forall {k} (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> Ordering
defaultCompare tag a
x tag a
y

instance GNFData tag => NFData (Some tag) where
    rnf :: Some tag -> ()
rnf (Some tag a
x) = forall k (f :: k -> *) (a :: k). GNFData f => f a -> ()
grnf tag a
x

instance Control.Applicative.Applicative m => Data.Semigroup.Semigroup (Some m) where
    Some m a
m <> :: Some m -> Some m -> Some m
<> Some m a
n = forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some (m a
m forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m a
n)

instance Applicative m => Data.Monoid.Monoid (Some m) where
    mempty :: Some m
mempty = forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
    mappend :: Some m -> Some m -> Some m
mappend = forall a. Semigroup a => a -> a -> a
(<>)