{-# LANGUAGE TemplateHaskellQuotes #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Singletons.TH.CustomStar
-- Copyright   :  (C) 2013 Richard Eisenberg
-- License     :  BSD-style (see LICENSE)
-- Maintainer  :  Ryan Scott
-- Stability   :  experimental
-- Portability :  non-portable
--
-- This file implements 'singletonStar', which generates a datatype @Rep@ and associated
-- singleton from a list of types. The promoted version of @Rep@ is kind @*@ and the
-- Haskell types themselves. This is still very experimental, so expect unusual
-- results!
--
-- See also @Data.Singletons.Base.CustomStar@ from @singletons-base@, a
-- variant of this module that also re-exports related definitions from
-- @Prelude.Singletons@.
--
----------------------------------------------------------------------------

module Data.Singletons.TH.CustomStar (
  singletonStar,

  module Data.Singletons.TH
  ) where

import Language.Haskell.TH
import Data.Singletons.TH
import Data.Singletons.TH.Deriving.Eq
import Data.Singletons.TH.Deriving.Infer
import Data.Singletons.TH.Deriving.Ord
import Data.Singletons.TH.Deriving.Show
import Data.Singletons.TH.Promote
import Data.Singletons.TH.Promote.Monad
import Data.Singletons.TH.Names
import Data.Singletons.TH.Options
import Data.Singletons.TH.Single
import Data.Singletons.TH.Single.Data
import Data.Singletons.TH.Single.Monad
import Data.Singletons.TH.Syntax
import Data.Singletons.TH.Util
import Control.Monad
import Data.Maybe
import Language.Haskell.TH.Desugar

-- | Produce a representation and singleton for the collection of types given.
--
-- A datatype @Rep@ is created, with one constructor per type in the declared
-- universe. When this type is promoted by the @singletons-th@ library, the
-- constructors become full types in @*@, not just promoted data constructors.
--
-- For example,
--
-- > $(singletonStar [''Nat, ''Bool, ''Maybe])
--
-- generates the following:
--
-- > data Rep = Nat | Bool | Maybe Rep deriving (Eq, Ord, Read, Show)
--
-- and its singleton. However, because @Rep@ is promoted to @*@, the singleton
-- is perhaps slightly unexpected:
--
-- > data SRep (a :: *) where
-- >   SNat :: Sing Nat
-- >   SBool :: Sing Bool
-- >   SMaybe :: Sing a -> Sing (Maybe a)
-- > type instance Sing = SRep
--
-- The unexpected part is that @Nat@, @Bool@, and @Maybe@ above are the real @Nat@,
-- @Bool@, and @Maybe@, not just promoted data constructors.
--
-- Please note that this function is /very/ experimental. Use at your own risk.
singletonStar :: OptionsMonad q
              => [Name]        -- ^ A list of Template Haskell @Name@s for types
              -> q [Dec]
singletonStar :: forall (q :: * -> *). OptionsMonad q => [Name] -> q [Dec]
singletonStar [Name]
names = do
  kinds <- (Name -> q [DType]) -> [Name] -> q [[DType]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Name -> q [DType]
forall (q :: * -> *). DsMonad q => Name -> q [DType]
getKind [Name]
names
  ctors <- zipWithM (mkCtor True) names kinds
  let repDecl = DataFlavor
-> [DType]
-> Name
-> [DTyVarBndrVis]
-> Maybe DType
-> [DCon]
-> [DDerivClause]
-> DDec
DDataD DataFlavor
Data [] Name
repName [] (DType -> Maybe DType
forall a. a -> Maybe a
Just (Name -> DType
DConT Name
typeKindName)) [DCon]
ctors
                         [Maybe DDerivStrategy -> [DType] -> DDerivClause
DDerivClause Maybe DDerivStrategy
forall a. Maybe a
Nothing ((Name -> DType) -> [Name] -> [DType]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DConT [''Eq, ''Ord, ''Read, ''Show])]
  fakeCtors <- zipWithM (mkCtor False) names kinds
  let dataDecl = DataFlavor -> Name -> [DTyVarBndrVis] -> [DCon] -> DataDecl
DataDecl DataFlavor
Data Name
repName [] [DCon]
fakeCtors
  -- Why do we need withLocalDeclarations here? It's because we end up
  -- expanding type synonyms when deriving instances for Rep, which requires
  -- reifying Rep itself. Since Rep hasn't been spliced in yet, we must put it
  -- into the local declarations.
  withLocalDeclarations [decToTH repDecl] $ do
    -- We opt to infer the constraints for the Eq instance here so that when it's
    -- promoted, Rep will be promoted to Type.
    dataDeclEqCxt <- inferConstraints (DConT ''Eq) (DConT repName) fakeCtors
    let dataDeclEqInst = Maybe [DType] -> DType -> Name -> DataDecl -> DerivedDecl cls
forall (cls :: * -> Constraint).
Maybe [DType] -> DType -> Name -> DataDecl -> DerivedDecl cls
DerivedDecl ([DType] -> Maybe [DType]
forall a. a -> Maybe a
Just [DType]
dataDeclEqCxt) (Name -> DType
DConT Name
repName) Name
repName DataDecl
dataDecl
    eqInst   <- mkEqInstance Nothing (DConT repName) dataDecl
    ordInst  <- mkOrdInstance Nothing (DConT repName) dataDecl
    showInst <- mkShowInstance Nothing (DConT repName) dataDecl
    (pInsts, promDecls) <- promoteM [] $ do _ <- promoteDataDec dataDecl
                                            traverse (promoteInstanceDec mempty mempty)
                                              [eqInst, ordInst, showInst]
    singletonDecls <- singDecsM [] $ do decs1 <- singDataD dataDecl
                                        decs2 <- singDerivedEqDecs dataDeclEqInst
                                        decs3 <- traverse singInstD pInsts
                                        return (decs1 ++ decs2 ++ decs3)
    return $ decsToTH $ repDecl :
                        promDecls ++
                        singletonDecls
  where -- get the kinds of the arguments to the tycon with the given name
        getKind :: DsMonad q => Name -> q [DKind]
        getKind :: forall (q :: * -> *). DsMonad q => Name -> q [DType]
getKind Name
name = do
          info <- Name -> q Info
forall (q :: * -> *). DsMonad q => Name -> q Info
reifyWithLocals Name
name
          dinfo <- dsInfo info
          case dinfo of
            DTyConI (DDataD DataFlavor
_ (DType
_:[DType]
_) Name
_ [DTyVarBndrVis]
_ Maybe DType
_ [DCon]
_ [DDerivClause]
_) Maybe [DDec]
_ ->
               String -> q [DType]
forall a. String -> q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Cannot make a representation of a constrained data type"
            DTyConI (DDataD DataFlavor
_ [] Name
_ [DTyVarBndrVis]
tvbs Maybe DType
mk [DCon]
_ [DDerivClause]
_) Maybe [DDec]
_ -> do
               all_tvbs <- [DTyVarBndrVis] -> Maybe DType -> q [DTyVarBndrVis]
forall (q :: * -> *).
DsMonad q =>
[DTyVarBndrVis] -> Maybe DType -> q [DTyVarBndrVis]
buildDataDTvbs [DTyVarBndrVis]
tvbs Maybe DType
mk
               return $ map (fromMaybe (DConT typeKindName) . extractTvbKind) all_tvbs
            DTyConI (DTySynD Name
_ [DTyVarBndrVis]
tvbs DType
_) Maybe [DDec]
_ ->
               [DType] -> q [DType]
forall a. a -> q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([DType] -> q [DType]) -> [DType] -> q [DType]
forall a b. (a -> b) -> a -> b
$ (DTyVarBndrVis -> DType) -> [DTyVarBndrVis] -> [DType]
forall a b. (a -> b) -> [a] -> [b]
map (DType -> Maybe DType -> DType
forall a. a -> Maybe a -> a
fromMaybe (Name -> DType
DConT Name
typeKindName) (Maybe DType -> DType)
-> (DTyVarBndrVis -> Maybe DType) -> DTyVarBndrVis -> DType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTyVarBndrVis -> Maybe DType
forall flag. DTyVarBndr flag -> Maybe DType
extractTvbKind) [DTyVarBndrVis]
tvbs
            DPrimTyConI Name
_ Int
n Bool
_ ->
               [DType] -> q [DType]
forall a. a -> q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([DType] -> q [DType]) -> [DType] -> q [DType]
forall a b. (a -> b) -> a -> b
$ Int -> DType -> [DType]
forall a. Int -> a -> [a]
replicate Int
n (DType -> [DType]) -> DType -> [DType]
forall a b. (a -> b) -> a -> b
$ Name -> DType
DConT Name
typeKindName
            DInfo
_ -> String -> q [DType]
forall a. String -> q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> q [DType]) -> String -> q [DType]
forall a b. (a -> b) -> a -> b
$ String
"Invalid thing for representation: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Name -> String
forall a. Show a => a -> String
show Name
name)

        -- first parameter is whether this is a real ctor (with a fresh name)
        -- or a fake ctor (when the name is actually a Haskell type)
        mkCtor :: DsMonad q => Bool -> Name -> [DKind] -> q DCon
        mkCtor :: forall (q :: * -> *).
DsMonad q =>
Bool -> Name -> [DType] -> q DCon
mkCtor Bool
real Name
name [DType]
args = do
          (types, vars) <- QWithAux [Name] q [DType] -> q ([DType], [Name])
forall m (q :: * -> *) a. QWithAux m q a -> q (a, m)
evalForPair (QWithAux [Name] q [DType] -> q ([DType], [Name]))
-> QWithAux [Name] q [DType] -> q ([DType], [Name])
forall a b. (a -> b) -> a -> b
$ (DType -> QWithAux [Name] q DType)
-> [DType] -> QWithAux [Name] q [DType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([DTypeArg] -> DType -> QWithAux [Name] q DType
forall (q :: * -> *).
DsMonad q =>
[DTypeArg] -> DType -> QWithAux [Name] q DType
kindToType []) [DType]
args
          dataName <- if real then mkDataName (nameBase name) else return name
          return $ DCon (map (`DPlainTV` SpecifiedSpec) vars) [] dataName
                        (DNormalC False (map (\DType
ty -> (Bang
noBang, DType
ty)) types))
                        (DConT repName)
            where
              noBang :: Bang
noBang = SourceUnpackedness -> SourceStrictness -> Bang
Bang SourceUnpackedness
NoSourceUnpackedness SourceStrictness
NoSourceStrictness

        -- demote a kind back to a type, accumulating any unbound parameters
        kindToType :: DsMonad q => [DTypeArg] -> DKind -> QWithAux [Name] q DType
        kindToType :: forall (q :: * -> *).
DsMonad q =>
[DTypeArg] -> DType -> QWithAux [Name] q DType
kindToType [DTypeArg]
_    (DForallT DForallTelescope
_ DType
_)      = String -> QWithAux [Name] q DType
forall a. String -> QWithAux [Name] q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Explicit forall encountered in kind"
        kindToType [DTypeArg]
_    (DConstrainedT [DType]
_ DType
_) = String -> QWithAux [Name] q DType
forall a. String -> QWithAux [Name] q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Explicit constraint encountered in kind"
        kindToType [DTypeArg]
args (DAppT DType
f DType
a) = do
          a' <- [DTypeArg] -> DType -> QWithAux [Name] q DType
forall (q :: * -> *).
DsMonad q =>
[DTypeArg] -> DType -> QWithAux [Name] q DType
kindToType [] DType
a
          kindToType (DTANormal a' : args) f
        kindToType [DTypeArg]
args (DAppKindT DType
f DType
a) = do
          a' <- [DTypeArg] -> DType -> QWithAux [Name] q DType
forall (q :: * -> *).
DsMonad q =>
[DTypeArg] -> DType -> QWithAux [Name] q DType
kindToType [] DType
a
          kindToType (DTyArg a' : args) f
        kindToType [DTypeArg]
args (DSigT DType
t DType
k) = do
          t' <- [DTypeArg] -> DType -> QWithAux [Name] q DType
forall (q :: * -> *).
DsMonad q =>
[DTypeArg] -> DType -> QWithAux [Name] q DType
kindToType [] DType
t
          k' <- kindToType [] k
          return $ DSigT t' k' `applyDType` args
        kindToType [DTypeArg]
args (DVarT Name
n) = do
          Name -> QWithAux [Name] q ()
forall (q :: * -> *) elt. Quasi q => elt -> QWithAux [elt] q ()
addElement Name
n
          DType -> QWithAux [Name] q DType
forall a. a -> QWithAux [Name] q a
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> QWithAux [Name] q DType)
-> DType -> QWithAux [Name] q DType
forall a b. (a -> b) -> a -> b
$ Name -> DType
DVarT Name
n DType -> [DTypeArg] -> DType
`applyDType` [DTypeArg]
args
        kindToType [DTypeArg]
args (DConT Name
n)    = DType -> QWithAux [Name] q DType
forall a. a -> QWithAux [Name] q a
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> QWithAux [Name] q DType)
-> DType -> QWithAux [Name] q DType
forall a b. (a -> b) -> a -> b
$ Name -> DType
DConT Name
name DType -> [DTypeArg] -> DType
`applyDType` [DTypeArg]
args
          where name :: Name
name | Name -> Bool
isTypeKindName Name
n = Name
repName
                     | Bool
otherwise        = Name
n
        kindToType [DTypeArg]
args DType
DArrowT      = DType -> QWithAux [Name] q DType
forall a. a -> QWithAux [Name] q a
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> QWithAux [Name] q DType)
-> DType -> QWithAux [Name] q DType
forall a b. (a -> b) -> a -> b
$ DType
DArrowT    DType -> [DTypeArg] -> DType
`applyDType` [DTypeArg]
args
        kindToType [DTypeArg]
args k :: DType
k@(DLitT {}) = DType -> QWithAux [Name] q DType
forall a. a -> QWithAux [Name] q a
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> QWithAux [Name] q DType)
-> DType -> QWithAux [Name] q DType
forall a b. (a -> b) -> a -> b
$ DType
k          DType -> [DTypeArg] -> DType
`applyDType` [DTypeArg]
args
        kindToType [DTypeArg]
args DType
DWildCardT   = DType -> QWithAux [Name] q DType
forall a. a -> QWithAux [Name] q a
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> QWithAux [Name] q DType)
-> DType -> QWithAux [Name] q DType
forall a b. (a -> b) -> a -> b
$ DType
DWildCardT DType -> [DTypeArg] -> DType
`applyDType` [DTypeArg]
args