{-# LANGUAGE DataKinds, TypeFamilies, KindSignatures, TemplateHaskell #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Singletons.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!
--
----------------------------------------------------------------------------

module Data.Singletons.CustomStar (
  singletonStar,

  module Data.Singletons.Prelude.Eq,
  module Data.Singletons.Prelude.Bool,
  module Data.Singletons.TH
  ) where

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

-- | 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 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 :: [Name] -> q [Dec]
singletonStar [Name]
names = do
  [[DKind]]
kinds <- (Name -> q [DKind]) -> [Name] -> q [[DKind]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> q [DKind]
forall (q :: * -> *). DsMonad q => Name -> q [DKind]
getKind [Name]
names
  [DCon]
ctors <- (Name -> [DKind] -> q DCon) -> [Name] -> [[DKind]] -> q [DCon]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Bool -> Name -> [DKind] -> q DCon
forall (q :: * -> *).
DsMonad q =>
Bool -> Name -> [DKind] -> q DCon
mkCtor Bool
True) [Name]
names [[DKind]]
kinds
  let repDecl :: DDec
repDecl = NewOrData
-> [DKind]
-> Name
-> [DTyVarBndr]
-> Maybe DKind
-> [DCon]
-> [DDerivClause]
-> DDec
DDataD NewOrData
Data [] Name
repName [] (DKind -> Maybe DKind
forall a. a -> Maybe a
Just (Name -> DKind
DConT Name
typeKindName)) [DCon]
ctors
                         [Maybe DDerivStrategy -> [DKind] -> DDerivClause
DDerivClause Maybe DDerivStrategy
forall a. Maybe a
Nothing ((Name -> DKind) -> [Name] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DKind
DConT [''Eq, ''Ord, ''Read, ''Show])]
  [DCon]
fakeCtors <- (Name -> [DKind] -> q DCon) -> [Name] -> [[DKind]] -> q [DCon]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Bool -> Name -> [DKind] -> q DCon
forall (q :: * -> *).
DsMonad q =>
Bool -> Name -> [DKind] -> q DCon
mkCtor Bool
False) [Name]
names [[DKind]]
kinds
  let dataDecl :: DataDecl
dataDecl = Name -> [DTyVarBndr] -> [DCon] -> DataDecl
DataDecl 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.
  [Dec] -> DsM q [Dec] -> q [Dec]
forall (q :: * -> *) a. DsMonad q => [Dec] -> DsM q a -> q a
withLocalDeclarations (DDec -> [Dec]
decToTH DDec
repDecl) (DsM q [Dec] -> q [Dec]) -> DsM q [Dec] -> q [Dec]
forall a b. (a -> b) -> a -> b
$ do
    -- We opt to infer the constraints for the Eq instance here so that when it's
    -- promoted, Rep will be promoted to Type.
    [DKind]
dataDeclEqCxt <- DKind -> DKind -> [DCon] -> DsM q [DKind]
forall (q :: * -> *).
DsMonad q =>
DKind -> DKind -> [DCon] -> q [DKind]
inferConstraints (Name -> DKind
DConT ''Eq) (Name -> DKind
DConT Name
repName) [DCon]
fakeCtors
    let dataDeclEqInst :: DerivedDecl Eq
dataDeclEqInst = Maybe [DKind] -> DKind -> Name -> DataDecl -> DerivedDecl Eq
forall (cls :: * -> Constraint).
Maybe [DKind] -> DKind -> Name -> DataDecl -> DerivedDecl cls
DerivedDecl ([DKind] -> Maybe [DKind]
forall a. a -> Maybe a
Just [DKind]
dataDeclEqCxt) (Name -> DKind
DConT Name
repName) Name
repName DataDecl
dataDecl
    UInstDecl
ordInst  <- DerivDesc (DsM q)
forall (q :: * -> *). DsMonad q => DerivDesc q
mkOrdInstance Maybe [DKind]
forall a. Maybe a
Nothing (Name -> DKind
DConT Name
repName) DataDecl
dataDecl
    UInstDecl
showInst <- ShowMode -> DerivDesc (DsM q)
forall (q :: * -> *). OptionsMonad q => ShowMode -> DerivDesc q
mkShowInstance ShowMode
ForPromotion Maybe [DKind]
forall a. Maybe a
Nothing (Name -> DKind
DConT Name
repName) DataDecl
dataDecl
    ([AInstDecl]
pInsts, [DDec]
promDecls) <- [Dec] -> PrM [AInstDecl] -> DsM q ([AInstDecl], [DDec])
forall (q :: * -> *) a.
OptionsMonad q =>
[Dec] -> PrM a -> q (a, [DDec])
promoteM [] (PrM [AInstDecl] -> DsM q ([AInstDecl], [DDec]))
-> PrM [AInstDecl] -> DsM q ([AInstDecl], [DDec])
forall a b. (a -> b) -> a -> b
$ do [DLetDec]
_ <- DataDecl -> PrM [DLetDec]
promoteDataDec DataDecl
dataDecl
                                            DerivedDecl Eq -> PrM ()
promoteDerivedEqDec DerivedDecl Eq
dataDeclEqInst
                                            (UInstDecl -> PrM AInstDecl) -> [UInstDecl] -> PrM [AInstDecl]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (OMap Name DKind
-> Map Name [DTyVarBndr] -> UInstDecl -> PrM AInstDecl
promoteInstanceDec OMap Name DKind
forall a. Monoid a => a
mempty Map Name [DTyVarBndr]
forall a. Monoid a => a
mempty)
                                              [UInstDecl
ordInst, UInstDecl
showInst]
    [DDec]
singletonDecls <- [Dec] -> SgM [DDec] -> DsM q [DDec]
forall (q :: * -> *).
OptionsMonad q =>
[Dec] -> SgM [DDec] -> q [DDec]
singDecsM [] (SgM [DDec] -> DsM q [DDec]) -> SgM [DDec] -> DsM q [DDec]
forall a b. (a -> b) -> a -> b
$ do [DDec]
decs1 <- DataDecl -> SgM [DDec]
singDataD DataDecl
dataDecl
                                        [DDec]
decs2 <- DerivedDecl Eq -> SgM [DDec]
singDerivedEqDecs DerivedDecl Eq
dataDeclEqInst
                                        [DDec]
decs3 <- (AInstDecl -> SgM DDec) -> [AInstDecl] -> SgM [DDec]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse AInstDecl -> SgM DDec
singInstD [AInstDecl]
pInsts
                                        [DDec] -> SgM [DDec]
forall (m :: * -> *) a. Monad m => a -> m a
return ([DDec]
decs1 [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
decs2 [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
decs3)
    [Dec] -> DsM q [Dec]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dec] -> DsM q [Dec]) -> [Dec] -> DsM q [Dec]
forall a b. (a -> b) -> a -> b
$ [DDec] -> [Dec]
decsToTH ([DDec] -> [Dec]) -> [DDec] -> [Dec]
forall a b. (a -> b) -> a -> b
$ DDec
repDecl DDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
:
                        [DDec]
promDecls [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++
                        [DDec]
singletonDecls
  where -- get the kinds of the arguments to the tycon with the given name
        getKind :: DsMonad q => Name -> q [DKind]
        getKind :: Name -> q [DKind]
getKind Name
name = do
          Info
info <- Name -> q Info
forall (q :: * -> *). DsMonad q => Name -> q Info
reifyWithLocals Name
name
          DInfo
dinfo <- Info -> q DInfo
forall (q :: * -> *). DsMonad q => Info -> q DInfo
dsInfo Info
info
          case DInfo
dinfo of
            DTyConI (DDataD NewOrData
_ (DKind
_:[DKind]
_) Name
_ [DTyVarBndr]
_ Maybe DKind
_ [DCon]
_ [DDerivClause]
_) Maybe [DDec]
_ ->
               String -> q [DKind]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Cannot make a representation of a constrained data type"
            DTyConI (DDataD NewOrData
_ [] Name
_ [DTyVarBndr]
tvbs Maybe DKind
mk [DCon]
_ [DDerivClause]
_) Maybe [DDec]
_ -> do
               [DTyVarBndr]
all_tvbs <- [DTyVarBndr] -> Maybe DKind -> q [DTyVarBndr]
forall (q :: * -> *).
DsMonad q =>
[DTyVarBndr] -> Maybe DKind -> q [DTyVarBndr]
buildDataDTvbs [DTyVarBndr]
tvbs Maybe DKind
mk
               [DKind] -> q [DKind]
forall (m :: * -> *) a. Monad m => a -> m a
return ([DKind] -> q [DKind]) -> [DKind] -> q [DKind]
forall a b. (a -> b) -> a -> b
$ (DTyVarBndr -> DKind) -> [DTyVarBndr] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map (DKind -> Maybe DKind -> DKind
forall a. a -> Maybe a -> a
fromMaybe (Name -> DKind
DConT Name
typeKindName) (Maybe DKind -> DKind)
-> (DTyVarBndr -> Maybe DKind) -> DTyVarBndr -> DKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTyVarBndr -> Maybe DKind
extractTvbKind) [DTyVarBndr]
all_tvbs
            DTyConI (DTySynD Name
_ [DTyVarBndr]
tvbs DKind
_) Maybe [DDec]
_ ->
               [DKind] -> q [DKind]
forall (m :: * -> *) a. Monad m => a -> m a
return ([DKind] -> q [DKind]) -> [DKind] -> q [DKind]
forall a b. (a -> b) -> a -> b
$ (DTyVarBndr -> DKind) -> [DTyVarBndr] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map (DKind -> Maybe DKind -> DKind
forall a. a -> Maybe a -> a
fromMaybe (Name -> DKind
DConT Name
typeKindName) (Maybe DKind -> DKind)
-> (DTyVarBndr -> Maybe DKind) -> DTyVarBndr -> DKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTyVarBndr -> Maybe DKind
extractTvbKind) [DTyVarBndr]
tvbs
            DPrimTyConI Name
_ Int
n Bool
_ ->
               [DKind] -> q [DKind]
forall (m :: * -> *) a. Monad m => a -> m a
return ([DKind] -> q [DKind]) -> [DKind] -> q [DKind]
forall a b. (a -> b) -> a -> b
$ Int -> DKind -> [DKind]
forall a. Int -> a -> [a]
replicate Int
n (DKind -> [DKind]) -> DKind -> [DKind]
forall a b. (a -> b) -> a -> b
$ Name -> DKind
DConT Name
typeKindName
            DInfo
_ -> String -> q [DKind]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> q [DKind]) -> String -> q [DKind]
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 :: Bool -> Name -> [DKind] -> q DCon
mkCtor Bool
real Name
name [DKind]
args = do
          ([DKind]
types, [Name]
vars) <- QWithAux [Name] q [DKind] -> q ([DKind], [Name])
forall m (q :: * -> *) a. QWithAux m q a -> q (a, m)
evalForPair (QWithAux [Name] q [DKind] -> q ([DKind], [Name]))
-> QWithAux [Name] q [DKind] -> q ([DKind], [Name])
forall a b. (a -> b) -> a -> b
$ (DKind -> QWithAux [Name] q DKind)
-> [DKind] -> QWithAux [Name] q [DKind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([DTypeArg] -> DKind -> QWithAux [Name] q DKind
forall (q :: * -> *).
DsMonad q =>
[DTypeArg] -> DKind -> QWithAux [Name] q DKind
kindToType []) [DKind]
args
          Name
dataName <- if Bool
real then String -> q Name
forall (q :: * -> *). Quasi q => String -> q Name
mkDataName (Name -> String
nameBase Name
name) else Name -> q Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
name
          DCon -> q DCon
forall (m :: * -> *) a. Monad m => a -> m a
return (DCon -> q DCon) -> DCon -> q DCon
forall a b. (a -> b) -> a -> b
$ [DTyVarBndr] -> [DKind] -> Name -> DConFields -> DKind -> DCon
DCon ((Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DTyVarBndr
DPlainTV [Name]
vars) [] Name
dataName
                        (Bool -> [DBangType] -> DConFields
DNormalC Bool
False ((DKind -> DBangType) -> [DKind] -> [DBangType]
forall a b. (a -> b) -> [a] -> [b]
map (\DKind
ty -> (Bang
noBang, DKind
ty)) [DKind]
types))
                        (Name -> DKind
DConT Name
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 :: [DTypeArg] -> DKind -> QWithAux [Name] q DKind
kindToType [DTypeArg]
_    (DForallT ForallVisFlag
_ [DTyVarBndr]
_ DKind
_)    = String -> QWithAux [Name] q DKind
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Explicit forall encountered in kind"
        kindToType [DTypeArg]
_    (DConstrainedT [DKind]
_ DKind
_) = String -> QWithAux [Name] q DKind
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Explicit constraint encountered in kind"
        kindToType [DTypeArg]
args (DAppT DKind
f DKind
a) = do
          DKind
a' <- [DTypeArg] -> DKind -> QWithAux [Name] q DKind
forall (q :: * -> *).
DsMonad q =>
[DTypeArg] -> DKind -> QWithAux [Name] q DKind
kindToType [] DKind
a
          [DTypeArg] -> DKind -> QWithAux [Name] q DKind
forall (q :: * -> *).
DsMonad q =>
[DTypeArg] -> DKind -> QWithAux [Name] q DKind
kindToType (DKind -> DTypeArg
DTANormal DKind
a' DTypeArg -> [DTypeArg] -> [DTypeArg]
forall a. a -> [a] -> [a]
: [DTypeArg]
args) DKind
f
        kindToType [DTypeArg]
args (DAppKindT DKind
f DKind
a) = do
          DKind
a' <- [DTypeArg] -> DKind -> QWithAux [Name] q DKind
forall (q :: * -> *).
DsMonad q =>
[DTypeArg] -> DKind -> QWithAux [Name] q DKind
kindToType [] DKind
a
          [DTypeArg] -> DKind -> QWithAux [Name] q DKind
forall (q :: * -> *).
DsMonad q =>
[DTypeArg] -> DKind -> QWithAux [Name] q DKind
kindToType (DKind -> DTypeArg
DTyArg DKind
a' DTypeArg -> [DTypeArg] -> [DTypeArg]
forall a. a -> [a] -> [a]
: [DTypeArg]
args) DKind
f
        kindToType [DTypeArg]
args (DSigT DKind
t DKind
k) = do
          DKind
t' <- [DTypeArg] -> DKind -> QWithAux [Name] q DKind
forall (q :: * -> *).
DsMonad q =>
[DTypeArg] -> DKind -> QWithAux [Name] q DKind
kindToType [] DKind
t
          DKind
k' <- [DTypeArg] -> DKind -> QWithAux [Name] q DKind
forall (q :: * -> *).
DsMonad q =>
[DTypeArg] -> DKind -> QWithAux [Name] q DKind
kindToType [] DKind
k
          DKind -> QWithAux [Name] q DKind
forall (m :: * -> *) a. Monad m => a -> m a
return (DKind -> QWithAux [Name] q DKind)
-> DKind -> QWithAux [Name] q DKind
forall a b. (a -> b) -> a -> b
$ DKind -> DKind -> DKind
DSigT DKind
t' DKind
k' DKind -> [DTypeArg] -> DKind
`applyDType` [DTypeArg]
args
        kindToType [DTypeArg]
args (DVarT Name
n) = do
          Name -> QWithAux [Name] q ()
forall (q :: * -> *) elt. Quasi q => elt -> QWithAux [elt] q ()
addElement Name
n
          DKind -> QWithAux [Name] q DKind
forall (m :: * -> *) a. Monad m => a -> m a
return (DKind -> QWithAux [Name] q DKind)
-> DKind -> QWithAux [Name] q DKind
forall a b. (a -> b) -> a -> b
$ Name -> DKind
DVarT Name
n DKind -> [DTypeArg] -> DKind
`applyDType` [DTypeArg]
args
        kindToType [DTypeArg]
args (DConT Name
n)    = DKind -> QWithAux [Name] q DKind
forall (m :: * -> *) a. Monad m => a -> m a
return (DKind -> QWithAux [Name] q DKind)
-> DKind -> QWithAux [Name] q DKind
forall a b. (a -> b) -> a -> b
$ Name -> DKind
DConT Name
name DKind -> [DTypeArg] -> DKind
`applyDType` [DTypeArg]
args
          where name :: Name
name | Name -> Bool
isTypeKindName Name
n = Name
repName
                     | Bool
otherwise        = Name
n
        kindToType [DTypeArg]
args DKind
DArrowT      = DKind -> QWithAux [Name] q DKind
forall (m :: * -> *) a. Monad m => a -> m a
return (DKind -> QWithAux [Name] q DKind)
-> DKind -> QWithAux [Name] q DKind
forall a b. (a -> b) -> a -> b
$ DKind
DArrowT    DKind -> [DTypeArg] -> DKind
`applyDType` [DTypeArg]
args
        kindToType [DTypeArg]
args k :: DKind
k@(DLitT {}) = DKind -> QWithAux [Name] q DKind
forall (m :: * -> *) a. Monad m => a -> m a
return (DKind -> QWithAux [Name] q DKind)
-> DKind -> QWithAux [Name] q DKind
forall a b. (a -> b) -> a -> b
$ DKind
k          DKind -> [DTypeArg] -> DKind
`applyDType` [DTypeArg]
args
        kindToType [DTypeArg]
args DKind
DWildCardT   = DKind -> QWithAux [Name] q DKind
forall (m :: * -> *) a. Monad m => a -> m a
return (DKind -> QWithAux [Name] q DKind)
-> DKind -> QWithAux [Name] q DKind
forall a b. (a -> b) -> a -> b
$ DKind
DWildCardT DKind -> [DTypeArg] -> DKind
`applyDType` [DTypeArg]
args