{-# LANGUAGE ParallelListComp, TupleSections, LambdaCase #-}
module Data.Singletons.Single.Data where
import Language.Haskell.TH.Desugar
import Language.Haskell.TH.Syntax
import Data.Singletons.Single.Defun
import Data.Singletons.Single.Monad
import Data.Singletons.Single.Type
import Data.Singletons.Single.Fixity
import Data.Singletons.Promote.Type
import Data.Singletons.Util
import Data.Singletons.Names
import Data.Singletons.Syntax
import Data.Singletons.TH.Options
import Control.Monad
singDataD :: DataDecl -> SgM [DDec]
singDataD :: DataDecl -> SgM [DDec]
singDataD (DataDecl Name
name [DTyVarBndr]
tvbs [DCon]
ctors) = do
Options
opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
let tvbNames :: [Name]
tvbNames = (DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> Name
extractTvbName [DTyVarBndr]
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 :: * -> *). MonadFail 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)
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)
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)
mapM DCon -> SgM DClause
mkToSingClause [DCon]
ctors
DClause
emptyToSingClause <- SgM DClause
mkEmptyToSingClause
let singKindInst :: DDec
singKindInst =
Maybe Overlap
-> Maybe [DTyVarBndr] -> [DKind] -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndr]
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 [DTyVarBndr] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr]
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 [DTyVarBndr] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr]
forall a. Maybe a
Nothing
(Name -> DKind
DConT Name
singFamilyName DKind -> DKind -> DKind
`DAppKindT` DKind
k)
(Name -> DKind
DConT Name
singDataName)
mk_data_dec :: [DTyVarBndr] -> Maybe DKind -> DDec
mk_data_dec [DTyVarBndr]
tvbs' Maybe DKind
mb_kind =
NewOrData
-> [DKind]
-> Name
-> [DTyVarBndr]
-> Maybe DKind
-> [DCon]
-> [DDerivClause]
-> DDec
DDataD NewOrData
Data [] Name
singDataName [DTyVarBndr]
tvbs' Maybe DKind
mb_kind [DCon]
ctors' []
[DDec]
data_decs <-
case Maybe DKind
mb_data_sak of
Maybe DKind
Nothing -> do
DKind
ki <- DKind -> SgM DKind
forall (m :: * -> *). MonadFail m => DKind -> m DKind
promoteType (DKind -> SgM DKind) -> DKind -> SgM DKind
forall a b. (a -> b) -> a -> b
$ DKind -> [DKind] -> DKind
foldType (Name -> DKind
DConT Name
name) ((DTyVarBndr -> DKind) -> [DTyVarBndr] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> DKind
dTyVarBndrToDType [DTyVarBndr]
tvbs)
let sing_tvbs :: [DTyVarBndr]
sing_tvbs = [DKind] -> [DTyVarBndr]
toposortTyVarsOf [DKind
k]
kinded_sing_ty :: DKind
kinded_sing_ty = ForallVisFlag -> [DTyVarBndr] -> DKind -> DKind
DForallT ForallVisFlag
ForallInvis [DTyVarBndr]
sing_tvbs (DKind -> DKind) -> DKind -> DKind
forall a b. (a -> b) -> a -> b
$
DKind
DArrowT DKind -> DKind -> DKind
`DAppT` DKind
ki DKind -> DKind -> DKind
`DAppT` Name -> DKind
DConT Name
typeKindName
[DDec] -> SgM [DDec]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [[DTyVarBndr] -> Maybe DKind -> DDec
mk_data_dec [] (DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
kinded_sing_ty)]
Just DKind
data_sak -> do
let (DFunArgs
args, DKind
_) = DKind -> (DFunArgs, DKind)
unravelDType DKind
data_sak
vis_args :: [DVisFunArg]
vis_args = DFunArgs -> [DVisFunArg]
filterDVisFunArgs DFunArgs
args
invis_tvbs :: [DTyVarBndr]
invis_tvbs = DFunArgs -> [DTyVarBndr]
filterInvisTvbArgs DFunArgs
args
vis_tvbs :: [DTyVarBndr]
vis_tvbs = (DVisFunArg -> DTyVarBndr -> DTyVarBndr)
-> [DVisFunArg] -> [DTyVarBndr] -> [DTyVarBndr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith DVisFunArg -> DTyVarBndr -> DTyVarBndr
replaceTvbKind [DVisFunArg]
vis_args [DTyVarBndr]
tvbs
DKind
ki <- DKind -> SgM DKind
forall (m :: * -> *). MonadFail m => DKind -> m DKind
promoteType (DKind -> SgM DKind) -> DKind -> SgM DKind
forall a b. (a -> b) -> a -> b
$ DKind -> [DKind] -> DKind
foldType (Name -> DKind
DConT Name
name) ((DTyVarBndr -> DKind) -> [DTyVarBndr] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> DKind
dTyVarBndrToDType [DTyVarBndr]
vis_tvbs)
Name
z <- String -> SgM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"z"
let sing_data_sak :: DKind
sing_data_sak = ForallVisFlag -> [DTyVarBndr] -> DKind -> DKind
DForallT ForallVisFlag
ForallInvis ([DTyVarBndr]
invis_tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndr]
vis_tvbs) (DKind -> DKind) -> DKind -> DKind
forall a b. (a -> b) -> a -> b
$
DKind
DArrowT DKind -> DKind -> DKind
`DAppT` DKind
ki DKind -> DKind -> DKind
`DAppT` Name -> DKind
DConT Name
typeKindName
[DDec] -> SgM [DDec]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ Name -> DKind -> DDec
DKiSigD Name
singDataName DKind
sing_data_sak
, [DTyVarBndr] -> Maybe DKind -> DDec
mk_data_dec [Name -> DTyVarBndr
DPlainTV Name
z] Maybe DKind
forall a. Maybe a
Nothing
]
[DDec] -> SgM [DDec]
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] [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 (m :: * -> *). Quasi m => String -> m 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 (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 (m :: * -> *). Quasi m => String -> m Name
qNewName String
"b")
DClause -> SgM DClause
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 -> [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]
_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)
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 (m :: * -> *). Quasi m => String -> m 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)
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 (m :: * -> *). Quasi m => String -> m 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)
mapM DKind -> SgM DKind
forall (m :: * -> *). MonadFail 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 (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 -> [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 -> [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 (m :: * -> *). Quasi m => String -> m Name
qNewName String
"x"
DClause -> SgM DClause
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 (m :: * -> *). Quasi m => String -> m Name
qNewName String
"x"
DClause -> SgM DClause
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]
con_tvbs [DKind]
cxt Name
name DConFields
fields DKind
rty)
| Bool -> Bool
not ([DKind] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DKind]
cxt)
= String -> SgM DCon
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
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
name
DKind -> SgM ()
forall (m :: * -> *). MonadFail m => DKind -> m ()
checkVanillaDType (DKind -> SgM ()) -> DKind -> SgM ()
forall a b. (a -> b) -> a -> b
$ [DTyVarBndr] -> [DKind] -> [DKind] -> DKind -> DKind
ravelVanillaDType [DTyVarBndr]
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)
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 (m :: * -> *). Quasi m => String -> m 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)
mapM DKind -> SgM DKind
forall (m :: * -> *). MonadFail m => DKind -> m DKind
promoteType_NC [DKind]
types
DKind
rty' <- DKind -> SgM DKind
forall (m :: * -> *). MonadFail 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]
kvbs = [DTyVarBndr]
-> [DKind] -> [DKind] -> DKind -> OSet Name -> [DTyVarBndr]
singTypeKVBs [DTyVarBndr]
con_tvbs [DKind]
kinds [] DKind
rty' OSet Name
forall a. Monoid a => a
mempty
all_tvbs :: [DTyVarBndr]
all_tvbs = [DTyVarBndr]
kvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ (Name -> DKind -> DTyVarBndr) -> [Name] -> [DKind] -> [DTyVarBndr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> DKind -> DTyVarBndr
DKindedTV [Name]
indexNames [DKind]
kinds
[DDec] -> SgM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs
[Maybe Overlap
-> Maybe [DTyVarBndr] -> [DKind] -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndr]
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]
indices)
(DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
singIName)
(DKind -> [DKind] -> DKind
foldType DKind
pCon [DKind]
kindedIndices))
[DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ DPat -> DExp -> DLetDec
DValD (Name -> DPat
DVarP Name
singMethName)
(DExp -> [DExp] -> DExp
foldExp DExp
sCon ((DKind -> DExp) -> [DKind] -> [DExp]
forall a b. (a -> b) -> [a] -> [b]
map (DExp -> DKind -> DExp
forall a b. a -> b -> a
const (DExp -> DKind -> DExp) -> DExp -> DKind -> DExp
forall a b. (a -> b) -> a -> b
$ Name -> DExp
DVarE Name
singMethName) [DKind]
types))]]
[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')
let noBang :: Bang
noBang = SourceUnpackedness -> SourceStrictness -> Bang
Bang SourceUnpackedness
NoSourceUnpackedness SourceStrictness
NoSourceStrictness
args :: [(Bang, DKind)]
args = (DKind -> (Bang, DKind)) -> [DKind] -> [(Bang, DKind)]
forall a b. (a -> b) -> [a] -> [b]
map ((Bang
noBang,) (DKind -> (Bang, DKind))
-> (DKind -> DKind) -> DKind -> (Bang, DKind)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DKind -> DKind -> DKind
DAppT DKind
singFamily) [DKind]
indices
conFields :: DConFields
conFields = case DConFields
fields of
DNormalC Bool
dInfix [(Bang, DKind)]
_ -> Bool -> [(Bang, DKind)] -> DConFields
DNormalC Bool
dInfix [(Bang, DKind)]
args
DRecC [DVarBangType]
_ -> Bool -> [(Bang, DKind)] -> DConFields
DNormalC Bool
False [(Bang, DKind)]
args
DCon -> SgM DCon
forall (m :: * -> *) a. Monad m => a -> m a
return (DCon -> SgM DCon) -> DCon -> SgM DCon
forall a b. (a -> b) -> a -> b
$ [DTyVarBndr] -> [DKind] -> Name -> DConFields -> DKind -> DCon
DCon [DTyVarBndr]
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'))