module Data.Singletons.TH.Single.Defun (singDefuns) where
import Control.Monad
import Data.Foldable
import Data.Singletons.TH.Names
import Data.Singletons.TH.Options
import Data.Singletons.TH.Promote.Defun
import Data.Singletons.TH.Single.Monad
import Data.Singletons.TH.Single.Type
import Data.Singletons.TH.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 a. a -> SgM a
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. [a] -> 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 :: [DTyVarBndrUnit]
tvbs = (Name -> Maybe DKind -> DTyVarBndrUnit)
-> [Name] -> [Maybe DKind] -> [DTyVarBndrUnit]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> Maybe DKind -> DTyVarBndrUnit
inferMaybeKindTV [Name]
names [Maybe DKind]
mb_ty_args
(Maybe DKind
_, [DDec]
insts) <- Options
-> Int
-> DCxt
-> [DTyVarBndrUnit]
-> [DTyVarBndrUnit]
-> SgM (Maybe DKind, [DDec])
go Options
opts Int
0 DCxt
sty_ctxt [] [DTyVarBndrUnit]
tvbs
[DDec] -> SgM [DDec]
forall a. a -> SgM a
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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Maybe DKind]
mb_ty_args
go :: Options -> Int -> DCxt -> [DTyVarBndrUnit] -> [DTyVarBndrUnit]
-> SgM (Maybe DKind, [DDec])
go :: Options
-> Int
-> DCxt
-> [DTyVarBndrUnit]
-> [DTyVarBndrUnit]
-> SgM (Maybe DKind, [DDec])
go Options
_ Int
_ DCxt
_ [DTyVarBndrUnit]
_ [] = (Maybe DKind, [DDec]) -> SgM (Maybe DKind, [DDec])
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe DKind
mb_ty_res, [])
go Options
opts Int
sym_num DCxt
sty_ctxt [DTyVarBndrUnit]
arg_tvbs (DTyVarBndrUnit
res_tvb:[DTyVarBndrUnit]
res_tvbs) = do
(Maybe DKind
mb_res, [DDec]
insts) <- Options
-> Int
-> DCxt
-> [DTyVarBndrUnit]
-> [DTyVarBndrUnit]
-> SgM (Maybe DKind, [DDec])
go Options
opts (Int
sym_num Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) DCxt
sty_ctxt ([DTyVarBndrUnit]
arg_tvbs [DTyVarBndrUnit] -> [DTyVarBndrUnit] -> [DTyVarBndrUnit]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndrUnit
res_tvb]) [DTyVarBndrUnit]
res_tvbs
[DDec]
new_insts <- (Int -> SgM (Maybe DDec)) -> [Int] -> SgM [DDec]
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM (Maybe DKind -> Int -> SgM (Maybe DDec)
mb_new_inst Maybe DKind
mb_res) [Int
0, Int
1, Int
2]
(Maybe DKind, [DDec]) -> SgM (Maybe DKind, [DDec])
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndrUnit] -> DTyVarBndrUnit -> Maybe DKind -> Maybe DKind
mk_inst_kind [] DTyVarBndrUnit
res_tvb Maybe DKind
mb_res, [DDec]
new_insts [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
insts)
where
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_inst_kind :: [DTyVarBndrUnit] -> DTyVarBndrUnit -> Maybe DKind -> Maybe DKind
mk_inst_kind :: [DTyVarBndrUnit] -> DTyVarBndrUnit -> Maybe DKind -> Maybe DKind
mk_inst_kind [DTyVarBndrUnit]
funTvbs DTyVarBndrUnit
defunTvb Maybe DKind
mbKind =
(Maybe DKind -> Maybe DKind -> Maybe DKind)
-> Maybe DKind -> [Maybe DKind] -> Maybe DKind
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Maybe DKind -> Maybe DKind -> Maybe DKind
buildFunArrow_maybe
(Maybe DKind -> Maybe DKind -> Maybe DKind
buildTyFunArrow_maybe (DTyVarBndrUnit -> Maybe DKind
forall flag. DTyVarBndr flag -> Maybe DKind
extractTvbKind DTyVarBndrUnit
defunTvb) Maybe DKind
mbKind)
((DTyVarBndrUnit -> Maybe DKind)
-> [DTyVarBndrUnit] -> [Maybe DKind]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrUnit -> Maybe DKind
forall flag. DTyVarBndr flag -> Maybe DKind
extractTvbKind [DTyVarBndrUnit]
funTvbs)
mb_new_inst :: Maybe DKind -> Int -> SgM (Maybe DDec)
mb_new_inst :: Maybe DKind -> Int -> SgM (Maybe DDec)
mb_new_inst Maybe DKind
mb_res Int
k
| Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
sym_num
= do [Name]
vs <- Int -> SgM Name -> SgM [Name]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
k (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
"s"
let sing_vs :: [DPat]
sing_vs = (Name -> DTyVarBndrUnit -> DPat)
-> [Name] -> [DTyVarBndrUnit] -> [DPat]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Name
v DTyVarBndrUnit
arg_tvb ->
DPat -> DKind -> DPat
DSigP (Name -> DPat
DVarP Name
v)
(DKind
singFamily DKind -> DKind -> DKind
`DAppT` DTyVarBndrUnit -> DKind
forall flag. DTyVarBndr flag -> DKind
dTyVarBndrToDType DTyVarBndrUnit
arg_tvb))
[Name]
vs [DTyVarBndrUnit]
last_arg_tvbs
Maybe DDec -> SgM (Maybe DDec)
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe DDec -> SgM (Maybe DDec)) -> Maybe DDec -> SgM (Maybe DDec)
forall a b. (a -> b) -> a -> b
$ 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] -> DCxt -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
(DCxt
sty_ctxt DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ DCxt
singI_ctxt)
(Name -> DKind
DConT (Int -> Name
mkSingIName Int
k) DKind -> DKind -> DKind
`DAppT` DKind -> DKind
mk_inst_ty ([DTyVarBndrUnit] -> DKind
mk_defun_inst_ty [DTyVarBndrUnit]
init_arg_tvbs))
[ DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD (Int -> Name
mkSingMethName Int
k)
[ [DPat] -> DExp -> DClause
DClause [DPat]
sing_vs
(DExp -> DClause) -> DExp -> DClause
forall a b. (a -> b) -> a -> b
$ Int -> DKind -> DExp -> DExp
wrapSingFun Int
sing_fun_num ([DTyVarBndrUnit] -> DKind
mk_defun_inst_ty [DTyVarBndrUnit]
arg_tvbs)
(DExp -> DExp) -> DExp -> DExp
forall a b. (a -> b) -> a -> b
$ DExp -> [Name] -> DExp
mk_sing_fun_expr DExp
sing_exp [Name]
vs
]
]
| Bool
otherwise
= Maybe DDec -> SgM (Maybe DDec)
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe DDec
forall a. Maybe a
Nothing
where
init_arg_tvbs, last_arg_tvbs :: [DTyVarBndrUnit]
([DTyVarBndrUnit]
init_arg_tvbs, [DTyVarBndrUnit]
last_arg_tvbs) = Int -> [DTyVarBndrUnit] -> ([DTyVarBndrUnit], [DTyVarBndrUnit])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
sym_num Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k) [DTyVarBndrUnit]
arg_tvbs
mk_defun_inst_ty :: [DTyVarBndrUnit] -> DType
mk_defun_inst_ty :: [DTyVarBndrUnit] -> DKind
mk_defun_inst_ty [DTyVarBndrUnit]
tvbs =
DKind -> DCxt -> DKind
foldType (Name -> DKind
DConT (Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
n Int
sym_num))
((DTyVarBndrUnit -> DKind) -> [DTyVarBndrUnit] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrUnit -> DKind
forall flag. DTyVarBndr flag -> DKind
dTyVarBndrToDType [DTyVarBndrUnit]
tvbs)
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
mk_sing_fun_expr :: DExp -> [Name] -> DExp
mk_sing_fun_expr :: DExp -> [Name] -> DExp
mk_sing_fun_expr DExp
sing_expr [Name]
vs =
(DExp -> DExp -> DExp) -> DExp -> [DExp] -> DExp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' DExp -> DExp -> DExp
DAppE DExp
sing_expr
((DTyVarBndrUnit -> DExp) -> [DTyVarBndrUnit] -> [DExp]
forall a b. (a -> b) -> [a] -> [b]
map (\DTyVarBndrUnit
arg_tvb -> Name -> DExp
DVarE Name
singMethName DExp -> DKind -> DExp
`DAppTypeE`
Name -> DKind
DVarT (DTyVarBndrUnit -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName DTyVarBndrUnit
arg_tvb))
[DTyVarBndrUnit]
init_arg_tvbs [DExp] -> [DExp] -> [DExp]
forall a. [a] -> [a] -> [a]
++
(Name -> DExp) -> [Name] -> [DExp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DExp
DVarE [Name]
vs)
singI_ctxt :: DCxt
singI_ctxt :: DCxt
singI_ctxt = (DTyVarBndrUnit -> DKind) -> [DTyVarBndrUnit] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
singIName) (DKind -> DKind)
-> (DTyVarBndrUnit -> DKind) -> DTyVarBndrUnit -> DKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTyVarBndrUnit -> DKind
forall flag. DTyVarBndr flag -> DKind
tvbToType) [DTyVarBndrUnit]
init_arg_tvbs
mk_inst_ty :: DType -> DType
mk_inst_ty :: DKind -> DKind
mk_inst_ty DKind
inst_head
= case [DTyVarBndrUnit] -> DTyVarBndrUnit -> Maybe DKind -> Maybe DKind
mk_inst_kind [DTyVarBndrUnit]
last_arg_tvbs DTyVarBndrUnit
res_tvb Maybe DKind
mb_res of
Just DKind
inst_kind -> DKind
inst_head DKind -> DKind -> DKind
`DSigT` DKind
inst_kind
Maybe DKind
Nothing -> DKind
inst_head
buildFunArrow :: DKind -> DKind -> DKind
buildFunArrow :: DKind -> DKind -> DKind
buildFunArrow DKind
k1 DKind
k2 = DKind
DArrowT DKind -> DKind -> DKind
`DAppT` DKind
k1 DKind -> DKind -> DKind
`DAppT` DKind
k2
buildFunArrow_maybe :: Maybe DKind -> Maybe DKind -> Maybe DKind
buildFunArrow_maybe :: Maybe DKind -> Maybe DKind -> Maybe DKind
buildFunArrow_maybe Maybe DKind
m_k1 Maybe DKind
m_k2 = DKind -> DKind -> DKind
buildFunArrow (DKind -> DKind -> DKind) -> Maybe DKind -> Maybe (DKind -> DKind)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe DKind
m_k1 Maybe (DKind -> DKind) -> Maybe DKind -> Maybe DKind
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe DKind
m_k2