module Data.Singletons.Single.Defun (singDefuns) where
import Control.Monad
import Data.Foldable
import Data.Singletons.Names
import Data.Singletons.Promote.Defun
import Data.Singletons.Single.Monad
import Data.Singletons.Single.Type
import Data.Singletons.TH.Options
import Data.Singletons.Util
import Language.Haskell.TH.Desugar
import Language.Haskell.TH.Syntax
singDefuns :: Name
-> NameSpace
-> DCxt
-> [Maybe DKind]
-> Maybe DKind
-> SgM [DDec]
singDefuns :: Name
-> NameSpace -> DCxt -> [Maybe DKind] -> Maybe DKind -> SgM [DDec]
singDefuns Name
n NameSpace
ns DCxt
ty_ctxt [Maybe DKind]
mb_ty_args Maybe DKind
mb_ty_res =
case [Maybe DKind]
mb_ty_args of
[] -> [DDec] -> SgM [DDec]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
[Maybe DKind]
_ -> do Options
opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
DCxt
sty_ctxt <- (DKind -> SgM DKind) -> DCxt -> SgM DCxt
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DKind -> SgM DKind
singPred DCxt
ty_ctxt
[Name]
names <- Int -> SgM Name -> SgM [Name]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM ([Maybe DKind] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Maybe DKind]
mb_ty_args) (SgM Name -> SgM [Name]) -> SgM Name -> SgM [Name]
forall a b. (a -> b) -> a -> b
$ String -> SgM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"d"
let tvbs :: [DTyVarBndr]
tvbs = (Name -> Maybe DKind -> DTyVarBndr)
-> [Name] -> [Maybe DKind] -> [DTyVarBndr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> Maybe DKind -> DTyVarBndr
inferMaybeKindTV [Name]
names [Maybe DKind]
mb_ty_args
(Maybe DKind
_, [DDec]
insts) = Options
-> Int
-> DCxt
-> [DTyVarBndr]
-> [DTyVarBndr]
-> (Maybe DKind, [DDec])
go Options
opts Int
0 DCxt
sty_ctxt [] [DTyVarBndr]
tvbs
[DDec] -> SgM [DDec]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [DDec]
insts
where
num_ty_args :: Int
num_ty_args :: Int
num_ty_args = [Maybe DKind] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Maybe DKind]
mb_ty_args
go :: Options -> Int -> DCxt -> [DTyVarBndr] -> [DTyVarBndr]
-> (Maybe DKind, [DDec])
go :: Options
-> Int
-> DCxt
-> [DTyVarBndr]
-> [DTyVarBndr]
-> (Maybe DKind, [DDec])
go Options
_ Int
_ DCxt
_ [DTyVarBndr]
_ [] = (Maybe DKind
mb_ty_res, [])
go Options
opts Int
sym_num DCxt
sty_ctxt [DTyVarBndr]
arg_tvbs (DTyVarBndr
res_tvb:[DTyVarBndr]
res_tvbs) =
(Maybe DKind
mb_new_res, DDec
new_instDDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
:[DDec]
insts)
where
mb_res :: Maybe DKind
insts :: [DDec]
(Maybe DKind
mb_res, [DDec]
insts) = Options
-> Int
-> DCxt
-> [DTyVarBndr]
-> [DTyVarBndr]
-> (Maybe DKind, [DDec])
go Options
opts (Int
sym_num Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) DCxt
sty_ctxt ([DTyVarBndr]
arg_tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndr
res_tvb]) [DTyVarBndr]
res_tvbs
mb_new_res :: Maybe DKind
mb_new_res :: Maybe DKind
mb_new_res = DTyVarBndr -> Maybe DKind -> Maybe DKind
mk_inst_kind DTyVarBndr
res_tvb Maybe DKind
mb_res
sing_fun_num :: Int
sing_fun_num :: Int
sing_fun_num = Int
num_ty_args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
sym_num
mk_sing_fun_expr :: DExp -> DExp
mk_sing_fun_expr :: DExp -> DExp
mk_sing_fun_expr DExp
sing_expr =
(DExp -> Name -> DExp) -> DExp -> [Name] -> DExp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\DExp
f Name
tvb_n -> DExp
f DExp -> DExp -> DExp
`DAppE` (Name -> DExp
DVarE Name
singMethName DExp -> DKind -> DExp
`DAppTypeE` Name -> DKind
DVarT Name
tvb_n))
DExp
sing_expr
((DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> Name
extractTvbName [DTyVarBndr]
arg_tvbs)
singI_ctxt :: DCxt
singI_ctxt :: DCxt
singI_ctxt = (DTyVarBndr -> DKind) -> [DTyVarBndr] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
singIName) (DKind -> DKind) -> (DTyVarBndr -> DKind) -> DTyVarBndr -> DKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTyVarBndr -> DKind
tvbToType) [DTyVarBndr]
arg_tvbs
mk_inst_ty :: DType -> DType
mk_inst_ty :: DKind -> DKind
mk_inst_ty DKind
inst_head
= case Maybe DKind
mb_new_res of
Just DKind
inst_kind -> DKind
inst_head DKind -> DKind -> DKind
`DSigT` DKind
inst_kind
Maybe DKind
Nothing -> DKind
inst_head
arg_tvb_tys :: [DType]
arg_tvb_tys :: DCxt
arg_tvb_tys = (DTyVarBndr -> DKind) -> [DTyVarBndr] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> DKind
dTyVarBndrToDType [DTyVarBndr]
arg_tvbs
mk_inst_kind :: DTyVarBndr -> Maybe DKind -> Maybe DKind
mk_inst_kind :: DTyVarBndr -> Maybe DKind -> Maybe DKind
mk_inst_kind DTyVarBndr
tvb' = Maybe DKind -> Maybe DKind -> Maybe DKind
buildTyFunArrow_maybe (DTyVarBndr -> Maybe DKind
extractTvbKind DTyVarBndr
tvb')
new_inst :: DDec
new_inst :: DDec
new_inst = Maybe Overlap
-> Maybe [DTyVarBndr] -> DCxt -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndr]
forall a. Maybe a
Nothing
(DCxt
sty_ctxt DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ DCxt
singI_ctxt)
(Name -> DKind
DConT Name
singIName DKind -> DKind -> DKind
`DAppT` DKind -> DKind
mk_inst_ty DKind
defun_inst_ty)
[DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ DPat -> DExp -> DLetDec
DValD (Name -> DPat
DVarP Name
singMethName)
(DExp -> DLetDec) -> DExp -> DLetDec
forall a b. (a -> b) -> a -> b
$ Int -> DKind -> DExp -> DExp
wrapSingFun Int
sing_fun_num DKind
defun_inst_ty
(DExp -> DExp) -> DExp -> DExp
forall a b. (a -> b) -> a -> b
$ DExp -> DExp
mk_sing_fun_expr DExp
sing_exp ]
where
defun_inst_ty :: DType
defun_inst_ty :: DKind
defun_inst_ty = DKind -> DCxt -> DKind
foldType (Name -> DKind
DConT (Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
n Int
sym_num))
DCxt
arg_tvb_tys
sing_exp :: DExp
sing_exp :: DExp
sing_exp = case NameSpace
ns of
NameSpace
DataName -> Name -> DExp
DConE (Name -> DExp) -> Name -> DExp
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
singledDataConName Options
opts Name
n
NameSpace
_ -> Name -> DExp
DVarE (Name -> DExp) -> Name -> DExp
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
singledValueName Options
opts Name
n