module Data.Singletons.TH.Single.Data where
import Language.Haskell.TH.Desugar as Desugar
import Language.Haskell.TH.Syntax
import Data.Maybe
import Data.Singletons.TH.Names
import Data.Singletons.TH.Options
import Data.Singletons.TH.Promote.Type
import Data.Singletons.TH.Single.Defun
import Data.Singletons.TH.Single.Fixity
import Data.Singletons.TH.Single.Monad
import Data.Singletons.TH.Syntax
import Data.Singletons.TH.Util
import Control.Monad
singDataD :: DataDecl -> SgM [DDec]
singDataD :: DataDecl -> SgM [DDec]
singDataD (DataDecl DataFlavor
df Name
name [DTyVarBndrUnit]
tvbs [DCon]
ctors) = do
Options
opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
let tvbNames :: [Name]
tvbNames = (DTyVarBndrUnit -> Name) -> [DTyVarBndrUnit] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrUnit -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName [DTyVarBndrUnit]
tvbs
ctor_names :: [Name]
ctor_names = (DCon -> Name) -> [DCon] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DCon -> Name
extractName [DCon]
ctors
rec_sel_names :: [Name]
rec_sel_names = (DCon -> [Name]) -> [DCon] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DCon -> [Name]
extractRecSelNames [DCon]
ctors
DKind
k <- DKind -> SgM DKind
forall (m :: * -> *). OptionsMonad m => DKind -> m DKind
promoteType (DKind -> [DKind] -> DKind
foldType (Name -> DKind
DConT Name
name) ((Name -> DKind) -> [Name] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DKind
DVarT [Name]
tvbNames))
Maybe DKind
mb_data_sak <- Name -> SgM (Maybe DKind)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DKind)
dsReifyType Name
name
[DCon]
ctors' <- (DCon -> SgM DCon) -> [DCon] -> SgM [DCon]
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 -> DCon -> SgM DCon
singCtor Name
name) [DCon]
ctors
[DDec]
fixityDecs <- [Name] -> SgM [DDec]
forall (q :: * -> *). OptionsMonad q => [Name] -> q [DDec]
singReifiedInfixDecls ([Name] -> SgM [DDec]) -> [Name] -> SgM [DDec]
forall a b. (a -> b) -> a -> b
$ [Name]
ctor_names [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
rec_sel_names
[DClause]
fromSingClauses <- (DCon -> SgM DClause) -> [DCon] -> SgM [DClause]
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 DCon -> SgM DClause
mkFromSingClause [DCon]
ctors
DClause
emptyFromSingClause <- SgM DClause
mkEmptyFromSingClause
[DClause]
toSingClauses <- (DCon -> SgM DClause) -> [DCon] -> SgM [DClause]
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 DCon -> SgM DClause
mkToSingClause [DCon]
ctors
DClause
emptyToSingClause <- SgM DClause
mkEmptyToSingClause
let singKindInst :: DDec
singKindInst =
Maybe Overlap
-> Maybe [DTyVarBndrUnit] -> [DKind] -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
((Name -> DKind) -> [Name] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map (DKind -> DKind
singKindConstraint (DKind -> DKind) -> (Name -> DKind) -> Name -> DKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> DKind
DVarT) [Name]
tvbNames)
(DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
singKindClassName) DKind
k)
[ DTySynEqn -> DDec
DTySynInstD (DTySynEqn -> DDec) -> DTySynEqn -> DDec
forall a b. (a -> b) -> a -> b
$ Maybe [DTyVarBndrUnit] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
(Name -> DKind
DConT Name
demoteName DKind -> DKind -> DKind
`DAppT` DKind
k)
(DKind -> [DKind] -> DKind
foldType (Name -> DKind
DConT Name
name)
((Name -> DKind) -> [Name] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map (DKind -> DKind -> DKind
DAppT DKind
demote (DKind -> DKind) -> (Name -> DKind) -> Name -> DKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> DKind
DVarT) [Name]
tvbNames))
, DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD Name
fromSingName
([DClause]
fromSingClauses [DClause] -> [DClause] -> [DClause]
forall a. [a] -> [a] -> [a]
`orIfEmpty` [DClause
emptyFromSingClause])
, DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD Name
toSingName
([DClause]
toSingClauses [DClause] -> [DClause] -> [DClause]
forall a. [a] -> [a] -> [a]
`orIfEmpty` [DClause
emptyToSingClause]) ]
let singDataName :: Name
singDataName = Options -> Name -> Name
singledDataTypeName Options
opts Name
name
singSynInst :: DDec
singSynInst =
DTySynEqn -> DDec
DTySynInstD (DTySynEqn -> DDec) -> DTySynEqn -> DDec
forall a b. (a -> b) -> a -> b
$ Maybe [DTyVarBndrUnit] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
(Name -> DKind
DConT Name
singFamilyName DKind -> DKind -> DKind
`DAppKindT` DKind
k)
(Name -> DKind
DConT Name
singDataName)
mk_data_dec :: DKind -> DDec
mk_data_dec DKind
kind =
DataFlavor
-> [DKind]
-> Name
-> [DTyVarBndrUnit]
-> Maybe DKind
-> [DCon]
-> [DDerivClause]
-> DDec
DDataD DataFlavor
Data [] Name
singDataName [] (DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
kind) [DCon]
ctors' []
data_decs :: [DDec]
data_decs = case Maybe DKind
mb_data_sak of
Maybe DKind
Nothing ->
let sing_tvbs :: [DTyVarBndr Specificity]
sing_tvbs = Specificity -> [DTyVarBndrUnit] -> [DTyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [DTyVarBndr oldFlag] -> [DTyVarBndr newFlag]
changeDTVFlags Specificity
SpecifiedSpec ([DTyVarBndrUnit] -> [DTyVarBndr Specificity])
-> [DTyVarBndrUnit] -> [DTyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$
[DKind] -> [DTyVarBndrUnit]
toposortTyVarsOf ([DKind] -> [DTyVarBndrUnit]) -> [DKind] -> [DTyVarBndrUnit]
forall a b. (a -> b) -> a -> b
$ (DTyVarBndrUnit -> DKind) -> [DTyVarBndrUnit] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrUnit -> DKind
forall flag. DTyVarBndr flag -> DKind
dTyVarBndrToDType [DTyVarBndrUnit]
tvbs
kinded_sing_ty :: DKind
kinded_sing_ty = DForallTelescope -> DKind -> DKind
DForallT ([DTyVarBndr Specificity] -> DForallTelescope
DForallInvis [DTyVarBndr Specificity]
sing_tvbs) (DKind -> DKind) -> DKind -> DKind
forall a b. (a -> b) -> a -> b
$
DKind
DArrowT DKind -> DKind -> DKind
`DAppT` DKind
k DKind -> DKind -> DKind
`DAppT` Name -> DKind
DConT Name
typeKindName in
[DKind -> DDec
mk_data_dec DKind
kinded_sing_ty]
Just DKind
data_sak ->
let (DFunArgs
args, DKind
_) = DKind -> (DFunArgs, DKind)
unravelDType DKind
data_sak
vis_args :: [DVisFunArg]
vis_args = DFunArgs -> [DVisFunArg]
filterDVisFunArgs DFunArgs
args
vis_tvbs :: [DTyVarBndr Specificity]
vis_tvbs = Specificity -> [DTyVarBndrUnit] -> [DTyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [DTyVarBndr oldFlag] -> [DTyVarBndr newFlag]
changeDTVFlags Specificity
SpecifiedSpec ([DTyVarBndrUnit] -> [DTyVarBndr Specificity])
-> [DTyVarBndrUnit] -> [DTyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$
(DVisFunArg -> DTyVarBndrUnit -> DTyVarBndrUnit)
-> [DVisFunArg] -> [DTyVarBndrUnit] -> [DTyVarBndrUnit]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith DVisFunArg -> DTyVarBndrUnit -> DTyVarBndrUnit
replaceTvbKind [DVisFunArg]
vis_args [DTyVarBndrUnit]
tvbs
invis_args :: [DTyVarBndr Specificity]
invis_args = DFunArgs -> [DTyVarBndr Specificity]
filterInvisTvbArgs DFunArgs
args
invis_tvbs :: [DTyVarBndr Specificity]
invis_tvbs | [DTyVarBndr Specificity] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DTyVarBndr Specificity]
invis_args
= Specificity -> [DTyVarBndrUnit] -> [DTyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [DTyVarBndr oldFlag] -> [DTyVarBndr newFlag]
changeDTVFlags Specificity
SpecifiedSpec ([DTyVarBndrUnit] -> [DTyVarBndr Specificity])
-> [DTyVarBndrUnit] -> [DTyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$
[DKind] -> [DTyVarBndrUnit]
toposortTyVarsOf [DKind
data_sak]
| Bool
otherwise
= [DTyVarBndr Specificity]
invis_args
sing_data_sak :: DKind
sing_data_sak = DForallTelescope -> DKind -> DKind
DForallT ([DTyVarBndr Specificity] -> DForallTelescope
DForallInvis ([DTyVarBndr Specificity]
invis_tvbs [DTyVarBndr Specificity]
-> [DTyVarBndr Specificity] -> [DTyVarBndr Specificity]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndr Specificity]
vis_tvbs)) (DKind -> DKind) -> DKind -> DKind
forall a b. (a -> b) -> a -> b
$
DKind
DArrowT DKind -> DKind -> DKind
`DAppT` DKind
k DKind -> DKind -> DKind
`DAppT` Name -> DKind
DConT Name
typeKindName in
[ Name -> DKind -> DDec
DKiSigD Name
singDataName DKind
sing_data_sak
, DKind -> DDec
mk_data_dec DKind
sing_data_sak
]
[DDec] -> SgM [DDec]
forall a. a -> SgM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([DDec] -> SgM [DDec]) -> [DDec] -> SgM [DDec]
forall a b. (a -> b) -> a -> b
$ [DDec]
data_decs [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++
DDec
singSynInst DDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
:
[ DDec
singKindInst | Options -> Bool
genSingKindInsts Options
opts
,
DataFlavor
df DataFlavor -> DataFlavor -> Bool
forall a. Eq a => a -> a -> Bool
/= DataFlavor
Desugar.TypeData
] [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++
[DDec]
fixityDecs
where
mkConName :: Name -> SgM Name
mkConName :: Name -> SgM Name
mkConName
| Name -> String
nameBase Name
name String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> String
nameBase Name
repName = String -> SgM Name
forall (q :: * -> *). Quasi q => String -> q Name
mkDataName (String -> SgM Name) -> (Name -> String) -> Name -> SgM Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
nameBase
| Bool
otherwise = Name -> SgM Name
forall a. a -> SgM a
forall (m :: * -> *) a. Monad m => a -> m a
return
mkFromSingClause :: DCon -> SgM DClause
mkFromSingClause :: DCon -> SgM DClause
mkFromSingClause DCon
c = do
Options
opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
let (Name
cname, Int
numArgs) = DCon -> (Name, Int)
extractNameArgs DCon
c
Name
cname' <- Name -> SgM Name
mkConName Name
cname
[Name]
varNames <- Int -> SgM Name -> SgM [Name]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
numArgs (String -> SgM Name
forall (q :: * -> *). Quasi q => String -> q Name
qNewName String
"b")
DClause -> SgM DClause
forall a. a -> SgM a
forall (m :: * -> *) a. Monad m => a -> m a
return (DClause -> SgM DClause) -> DClause -> SgM DClause
forall a b. (a -> b) -> a -> b
$ [DPat] -> DExp -> DClause
DClause [Name -> [DKind] -> [DPat] -> DPat
DConP (Options -> Name -> Name
singledDataConName Options
opts Name
cname) [] ((Name -> DPat) -> [Name] -> [DPat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DPat
DVarP [Name]
varNames)]
(DExp -> [DExp] -> DExp
foldExp
(Name -> DExp
DConE Name
cname')
((Name -> DExp) -> [Name] -> [DExp]
forall a b. (a -> b) -> [a] -> [b]
map (DExp -> DExp -> DExp
DAppE (Name -> DExp
DVarE Name
fromSingName) (DExp -> DExp) -> (Name -> DExp) -> Name -> DExp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> DExp
DVarE) [Name]
varNames))
mkToSingClause :: DCon -> SgM DClause
mkToSingClause :: DCon -> SgM DClause
mkToSingClause (DCon [DTyVarBndr Specificity]
_tvbs [DKind]
_cxt Name
cname DConFields
fields DKind
_rty) = do
Options
opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
let types :: [DKind]
types = DConFields -> [DKind]
tysOfConFields DConFields
fields
[Name]
varNames <- (DKind -> SgM Name) -> [DKind] -> SgM [Name]
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 (SgM Name -> DKind -> SgM Name
forall a b. a -> b -> a
const (SgM Name -> DKind -> SgM Name) -> SgM Name -> DKind -> SgM Name
forall a b. (a -> b) -> a -> b
$ String -> SgM Name
forall (q :: * -> *). Quasi q => String -> q Name
qNewName String
"b") [DKind]
types
[Name]
svarNames <- (DKind -> SgM Name) -> [DKind] -> SgM [Name]
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 (SgM Name -> DKind -> SgM Name
forall a b. a -> b -> a
const (SgM Name -> DKind -> SgM Name) -> SgM Name -> DKind -> SgM Name
forall a b. (a -> b) -> a -> b
$ String -> SgM Name
forall (q :: * -> *). Quasi q => String -> q Name
qNewName String
"c") [DKind]
types
[DKind]
promoted <- (DKind -> SgM DKind) -> [DKind] -> SgM [DKind]
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 DKind -> SgM DKind
forall (m :: * -> *). OptionsMonad m => DKind -> m DKind
promoteType [DKind]
types
Name
cname' <- Name -> SgM Name
mkConName Name
cname
let varPats :: [DPat]
varPats = (Name -> DKind -> DPat) -> [Name] -> [DKind] -> [DPat]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> DKind -> DPat
mkToSingVarPat [Name]
varNames [DKind]
promoted
recursiveCalls :: [DExp]
recursiveCalls = (Name -> DKind -> DExp) -> [Name] -> [DKind] -> [DExp]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> DKind -> DExp
mkRecursiveCall [Name]
varNames [DKind]
promoted
DClause -> SgM DClause
forall a. a -> SgM a
forall (m :: * -> *) a. Monad m => a -> m a
return (DClause -> SgM DClause) -> DClause -> SgM DClause
forall a b. (a -> b) -> a -> b
$
[DPat] -> DExp -> DClause
DClause [Name -> [DKind] -> [DPat] -> DPat
DConP Name
cname' [] [DPat]
varPats]
([DExp] -> [DPat] -> DExp -> DExp
multiCase [DExp]
recursiveCalls
((Name -> DPat) -> [Name] -> [DPat]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> [DKind] -> [DPat] -> DPat
DConP Name
someSingDataName [] ([DPat] -> DPat) -> (Name -> [DPat]) -> Name -> DPat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DPat -> [DPat]
forall a. a -> [a]
listify (DPat -> [DPat]) -> (Name -> DPat) -> Name -> [DPat]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> DPat
DVarP)
[Name]
svarNames)
(DExp -> DExp -> DExp
DAppE (Name -> DExp
DConE Name
someSingDataName)
(DExp -> [DExp] -> DExp
foldExp (Name -> DExp
DConE (Options -> Name -> Name
singledDataConName Options
opts Name
cname))
((Name -> DExp) -> [Name] -> [DExp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DExp
DVarE [Name]
svarNames))))
mkToSingVarPat :: Name -> DKind -> DPat
mkToSingVarPat :: Name -> DKind -> DPat
mkToSingVarPat Name
varName DKind
ki =
DPat -> DKind -> DPat
DSigP (Name -> DPat
DVarP Name
varName) (DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
demoteName) DKind
ki)
mkRecursiveCall :: Name -> DKind -> DExp
mkRecursiveCall :: Name -> DKind -> DExp
mkRecursiveCall Name
var_name DKind
ki =
DExp -> DKind -> DExp
DSigE (DExp -> DExp -> DExp
DAppE (Name -> DExp
DVarE Name
toSingName) (Name -> DExp
DVarE Name
var_name))
(DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
someSingTypeName) DKind
ki)
mkEmptyFromSingClause :: SgM DClause
mkEmptyFromSingClause :: SgM DClause
mkEmptyFromSingClause = do
Name
x <- String -> SgM Name
forall (q :: * -> *). Quasi q => String -> q Name
qNewName String
"x"
DClause -> SgM DClause
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DClause -> SgM DClause) -> DClause -> SgM DClause
forall a b. (a -> b) -> a -> b
$ [DPat] -> DExp -> DClause
DClause [Name -> DPat
DVarP Name
x]
(DExp -> DClause) -> DExp -> DClause
forall a b. (a -> b) -> a -> b
$ DExp -> [DMatch] -> DExp
DCaseE (Name -> DExp
DVarE Name
x) []
mkEmptyToSingClause :: SgM DClause
mkEmptyToSingClause :: SgM DClause
mkEmptyToSingClause = do
Name
x <- String -> SgM Name
forall (q :: * -> *). Quasi q => String -> q Name
qNewName String
"x"
DClause -> SgM DClause
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DClause -> SgM DClause) -> DClause -> SgM DClause
forall a b. (a -> b) -> a -> b
$ [DPat] -> DExp -> DClause
DClause [Name -> DPat
DVarP Name
x]
(DExp -> DClause) -> DExp -> DClause
forall a b. (a -> b) -> a -> b
$ Name -> DExp
DConE Name
someSingDataName DExp -> DExp -> DExp
`DAppE` DExp -> [DMatch] -> DExp
DCaseE (Name -> DExp
DVarE Name
x) []
singCtor :: Name -> DCon -> SgM DCon
singCtor :: Name -> DCon -> SgM DCon
singCtor Name
dataName (DCon [DTyVarBndr Specificity]
con_tvbs [DKind]
cxt Name
name DConFields
fields DKind
rty)
| Bool -> Bool
not ([DKind] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DKind]
cxt)
= String -> SgM DCon
forall a. String -> SgM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Singling of constrained constructors not yet supported"
| Bool
otherwise
= do
Options
opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
let types :: [DKind]
types = DConFields -> [DKind]
tysOfConFields DConFields
fields
numTypes :: Int
numTypes = [DKind] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DKind]
types
sName :: Name
sName = Options -> Name -> Name
singledDataConName Options
opts Name
name
sCon :: DExp
sCon = Name -> DExp
DConE Name
sName
pCon :: DKind
pCon = Name -> DKind
DConT (Name -> DKind) -> Name -> DKind
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
promotedDataTypeOrConName Options
opts Name
name
DKind -> SgM ()
forall (m :: * -> *). MonadFail m => DKind -> m ()
checkVanillaDType (DKind -> SgM ()) -> DKind -> SgM ()
forall a b. (a -> b) -> a -> b
$ [DTyVarBndr Specificity] -> [DKind] -> [DKind] -> DKind -> DKind
ravelVanillaDType [DTyVarBndr Specificity]
con_tvbs [] [DKind]
types DKind
rty
[Name]
indexNames <- (DKind -> SgM Name) -> [DKind] -> SgM [Name]
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 (SgM Name -> DKind -> SgM Name
forall a b. a -> b -> a
const (SgM Name -> DKind -> SgM Name) -> SgM Name -> DKind -> SgM Name
forall a b. (a -> b) -> a -> b
$ String -> SgM Name
forall (q :: * -> *). Quasi q => String -> q Name
qNewName String
"n") [DKind]
types
[DKind]
kinds <- (DKind -> SgM DKind) -> [DKind] -> SgM [DKind]
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 DKind -> SgM DKind
forall (m :: * -> *). OptionsMonad m => DKind -> m DKind
promoteType_NC [DKind]
types
DKind
rty' <- DKind -> SgM DKind
forall (m :: * -> *). OptionsMonad m => DKind -> m DKind
promoteType_NC DKind
rty
let indices :: [DKind]
indices = (Name -> DKind) -> [Name] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DKind
DVarT [Name]
indexNames
kindedIndices :: [DKind]
kindedIndices = (DKind -> DKind -> DKind) -> [DKind] -> [DKind] -> [DKind]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith DKind -> DKind -> DKind
DSigT [DKind]
indices [DKind]
kinds
kvbs :: [DTyVarBndr Specificity]
kvbs | [DTyVarBndr Specificity] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DTyVarBndr Specificity]
con_tvbs
= Specificity -> [DTyVarBndrUnit] -> [DTyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [DTyVarBndr oldFlag] -> [DTyVarBndr newFlag]
changeDTVFlags Specificity
SpecifiedSpec ([DKind] -> [DTyVarBndrUnit]
toposortTyVarsOf ([DKind]
kinds [DKind] -> [DKind] -> [DKind]
forall a. [a] -> [a] -> [a]
++ [DKind
rty'])) [DTyVarBndr Specificity]
-> [DTyVarBndr Specificity] -> [DTyVarBndr Specificity]
forall a. [a] -> [a] -> [a]
++
[DTyVarBndr Specificity]
con_tvbs
| Bool
otherwise
= [DTyVarBndr Specificity]
con_tvbs
all_tvbs :: [DTyVarBndr Specificity]
all_tvbs = [DTyVarBndr Specificity]
kvbs [DTyVarBndr Specificity]
-> [DTyVarBndr Specificity] -> [DTyVarBndr Specificity]
forall a. [a] -> [a] -> [a]
++ (Name -> DKind -> DTyVarBndr Specificity)
-> [Name] -> [DKind] -> [DTyVarBndr Specificity]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Name -> Specificity -> DKind -> DTyVarBndr Specificity
forall flag. Name -> flag -> DKind -> DTyVarBndr flag
`DKindedTV` Specificity
SpecifiedSpec) [Name]
indexNames [DKind]
kinds
let mb_SingI_dec :: Int -> Maybe DDec
mb_SingI_dec :: Int -> Maybe DDec
mb_SingI_dec Int
k
| Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
numTypes
= let take_until_k :: [a] -> [a]
take_until_k = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take (Int
numTypes Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k) in
DDec -> Maybe DDec
forall a. a -> Maybe a
Just (DDec -> Maybe DDec) -> DDec -> Maybe DDec
forall a b. (a -> b) -> a -> b
$ Maybe Overlap
-> Maybe [DTyVarBndrUnit] -> [DKind] -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
((DKind -> DKind) -> [DKind] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map (DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
singIName)) ([DKind] -> [DKind]
forall {a}. [a] -> [a]
take_until_k [DKind]
indices))
(DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT (Int -> Name
mkSingIName Int
k))
(DKind -> [DKind] -> DKind
foldType DKind
pCon ([DKind] -> [DKind]
forall {a}. [a] -> [a]
take_until_k [DKind]
kindedIndices)))
[DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ DPat -> DExp -> DLetDec
DValD (Name -> DPat
DVarP (Int -> Name
mkSingMethName Int
k))
(DExp -> [DExp] -> DExp
foldExp DExp
sCon (Int -> DExp -> [DExp]
forall a. Int -> a -> [a]
replicate (Int
numTypes Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k) (Name -> DExp
DVarE Name
singMethName)))]
| Bool
otherwise
= Maybe DDec
forall a. Maybe a
Nothing
[DDec] -> SgM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs ([DDec] -> SgM ()) -> [DDec] -> SgM ()
forall a b. (a -> b) -> a -> b
$ (Int -> Maybe DDec) -> [Int] -> [DDec]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Int -> Maybe DDec
mb_SingI_dec [Int
0, Int
1, Int
2]
[DDec] -> SgM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs ([DDec] -> SgM ()) -> SgM [DDec] -> SgM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name
-> NameSpace
-> [DKind]
-> [Maybe DKind]
-> Maybe DKind
-> SgM [DDec]
singDefuns Name
name NameSpace
DataName [] ((DKind -> Maybe DKind) -> [DKind] -> [Maybe DKind]
forall a b. (a -> b) -> [a] -> [b]
map DKind -> Maybe DKind
forall a. a -> Maybe a
Just [DKind]
kinds) (DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
rty')
DConFields
conFields <- case DConFields
fields of
DNormalC Bool
dInfix [DBangType]
bts -> Bool -> [DBangType] -> DConFields
DNormalC Bool
dInfix ([DBangType] -> DConFields) -> SgM [DBangType] -> SgM DConFields
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(DBangType -> DKind -> SgM DBangType)
-> [DBangType] -> [DKind] -> SgM [DBangType]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\(Bang
b, DKind
_) DKind
index -> Bang -> DKind -> SgM DBangType
mk_bang_type Bang
b DKind
index)
[DBangType]
bts [DKind]
indices
DRecC [DVarBangType]
vbts -> Bool -> [DBangType] -> DConFields
DNormalC Bool
False ([DBangType] -> DConFields) -> SgM [DBangType] -> SgM DConFields
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(DVarBangType -> DKind -> SgM DBangType)
-> [DVarBangType] -> [DKind] -> SgM [DBangType]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\(Name
_, Bang
b, DKind
_) DKind
index -> Bang -> DKind -> SgM DBangType
mk_bang_type Bang
b DKind
index)
[DVarBangType]
vbts [DKind]
indices
DCon -> SgM DCon
forall a. a -> SgM a
forall (m :: * -> *) a. Monad m => a -> m a
return (DCon -> SgM DCon) -> DCon -> SgM DCon
forall a b. (a -> b) -> a -> b
$ [DTyVarBndr Specificity]
-> [DKind] -> Name -> DConFields -> DKind -> DCon
DCon [DTyVarBndr Specificity]
all_tvbs [] Name
sName DConFields
conFields
(Name -> DKind
DConT (Options -> Name -> Name
singledDataTypeName Options
opts Name
dataName) DKind -> DKind -> DKind
`DAppT`
(DKind -> [DKind] -> DKind
foldType DKind
pCon [DKind]
indices DKind -> DKind -> DKind
`DSigT` DKind
rty'))
where
mk_source_unpackedness :: SourceUnpackedness -> SgM SourceUnpackedness
mk_source_unpackedness :: SourceUnpackedness -> SgM SourceUnpackedness
mk_source_unpackedness SourceUnpackedness
su = case SourceUnpackedness
su of
SourceUnpackedness
NoSourceUnpackedness -> SourceUnpackedness -> SgM SourceUnpackedness
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceUnpackedness
su
SourceUnpackedness
SourceNoUnpack -> SourceUnpackedness -> SgM SourceUnpackedness
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceUnpackedness
su
SourceUnpackedness
SourceUnpack -> do
String -> SgM ()
forall (q :: * -> *). Quasi q => String -> q ()
qReportWarning String
"{-# UNPACK #-} pragmas are ignored by `singletons-th`."
SourceUnpackedness -> SgM SourceUnpackedness
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceUnpackedness
NoSourceUnpackedness
mk_bang :: Bang -> SgM Bang
mk_bang :: Bang -> SgM Bang
mk_bang (Bang SourceUnpackedness
su SourceStrictness
ss) = do SourceUnpackedness
su' <- SourceUnpackedness -> SgM SourceUnpackedness
mk_source_unpackedness SourceUnpackedness
su
Bang -> SgM Bang
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bang -> SgM Bang) -> Bang -> SgM Bang
forall a b. (a -> b) -> a -> b
$ SourceUnpackedness -> SourceStrictness -> Bang
Bang SourceUnpackedness
su' SourceStrictness
ss
mk_bang_type :: Bang -> DType -> SgM DBangType
mk_bang_type :: Bang -> DKind -> SgM DBangType
mk_bang_type Bang
b DKind
index = do Bang
b' <- Bang -> SgM Bang
mk_bang Bang
b
DBangType -> SgM DBangType
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bang
b', DKind -> DKind -> DKind
DAppT DKind
singFamily DKind
index)