{-# LANGUAGE TemplateHaskellQuotes #-}
module Data.Singletons.TH.Promote.Defun where
import Language.Haskell.TH.Desugar
import Language.Haskell.TH.Syntax
import Data.Singletons.TH.Names
import Data.Singletons.TH.Options
import Data.Singletons.TH.Promote.Monad
import Data.Singletons.TH.Promote.Type
import Data.Singletons.TH.Syntax
import Data.Singletons.TH.Util
import Control.Monad
import qualified Data.Map.Strict as Map
import Data.Map.Strict (Map)
import Data.Maybe
defunInfo :: DInfo -> PrM [DDec]
defunInfo :: DInfo -> PrM [DDec]
defunInfo (DTyConI DDec
dec Maybe [DDec]
_instances) = DDec -> PrM [DDec]
buildDefunSyms DDec
dec
defunInfo (DPrimTyConI Name
_name Int
_numArgs Bool
_unlifted) =
String -> PrM [DDec]
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> PrM [DDec]) -> String -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ String
"Building defunctionalization symbols of primitive " String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"type constructors not supported"
defunInfo (DVarI Name
_name DKind
_ty Maybe Name
_mdec) =
String -> PrM [DDec]
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Building defunctionalization symbols of values not supported"
defunInfo (DTyVarI Name
_name DKind
_ty) =
String -> PrM [DDec]
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Building defunctionalization symbols of type variables not supported"
defunInfo (DPatSynI {}) =
String -> PrM [DDec]
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Building defunctionalization symbols of pattern synonyms not supported"
defunTopLevelTypeDecls ::
[TySynDecl]
-> [ClosedTypeFamilyDecl]
-> [OpenTypeFamilyDecl]
-> PrM ()
defunTopLevelTypeDecls :: [TySynDecl]
-> [ClosedTypeFamilyDecl] -> [OpenTypeFamilyDecl] -> PrM ()
defunTopLevelTypeDecls [TySynDecl]
ty_syns [ClosedTypeFamilyDecl]
c_tyfams [OpenTypeFamilyDecl]
o_tyfams = do
[DDec]
defun_ty_syns <-
(TySynDecl -> PrM [DDec]) -> [TySynDecl] -> PrM [DDec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM (\(TySynDecl Name
name [DTyVarBndrUnit]
tvbs DKind
rhs) -> Name -> [DTyVarBndrUnit] -> DKind -> PrM [DDec]
buildDefunSymsTySynD Name
name [DTyVarBndrUnit]
tvbs DKind
rhs) [TySynDecl]
ty_syns
[DDec]
defun_c_tyfams <-
(ClosedTypeFamilyDecl -> PrM [DDec])
-> [ClosedTypeFamilyDecl] -> PrM [DDec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM (DTypeFamilyHead -> PrM [DDec]
buildDefunSymsClosedTypeFamilyD (DTypeFamilyHead -> PrM [DDec])
-> (ClosedTypeFamilyDecl -> DTypeFamilyHead)
-> ClosedTypeFamilyDecl
-> PrM [DDec]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClosedTypeFamilyDecl -> DTypeFamilyHead
forall (info :: FamilyInfo). TypeFamilyDecl info -> DTypeFamilyHead
getTypeFamilyDecl) [ClosedTypeFamilyDecl]
c_tyfams
[DDec]
defun_o_tyfams <-
(OpenTypeFamilyDecl -> PrM [DDec])
-> [OpenTypeFamilyDecl] -> PrM [DDec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM (DTypeFamilyHead -> PrM [DDec]
buildDefunSymsOpenTypeFamilyD (DTypeFamilyHead -> PrM [DDec])
-> (OpenTypeFamilyDecl -> DTypeFamilyHead)
-> OpenTypeFamilyDecl
-> PrM [DDec]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpenTypeFamilyDecl -> DTypeFamilyHead
forall (info :: FamilyInfo). TypeFamilyDecl info -> DTypeFamilyHead
getTypeFamilyDecl) [OpenTypeFamilyDecl]
o_tyfams
[DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs ([DDec] -> PrM ()) -> [DDec] -> PrM ()
forall a b. (a -> b) -> a -> b
$ [DDec]
defun_ty_syns [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
defun_c_tyfams [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
defun_o_tyfams
defunAssociatedTypeFamilies ::
[DTyVarBndrUnit]
-> [OpenTypeFamilyDecl]
-> PrM ()
defunAssociatedTypeFamilies :: [DTyVarBndrUnit] -> [OpenTypeFamilyDecl] -> PrM ()
defunAssociatedTypeFamilies [DTyVarBndrUnit]
cls_tvbs [OpenTypeFamilyDecl]
atfs = do
[DDec]
defun_atfs <- (OpenTypeFamilyDecl -> PrM [DDec])
-> [OpenTypeFamilyDecl] -> PrM [DDec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM OpenTypeFamilyDecl -> PrM [DDec]
defun [OpenTypeFamilyDecl]
atfs
[DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs [DDec]
defun_atfs
where
defun :: OpenTypeFamilyDecl -> PrM [DDec]
defun :: OpenTypeFamilyDecl -> PrM [DDec]
defun (TypeFamilyDecl DTypeFamilyHead
tf_head) =
(DTyVarBndrUnit -> DTyVarBndrUnit)
-> (Maybe DKind -> Maybe DKind) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndrUnit -> DTyVarBndrUnit
ascribe_tf_tvb_kind Maybe DKind -> Maybe DKind
forall a. a -> a
id DTypeFamilyHead
tf_head
cls_tvb_kind_map :: Map Name DKind
cls_tvb_kind_map :: Map Name DKind
cls_tvb_kind_map = [(Name, DKind)] -> Map Name DKind
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (DTyVarBndrUnit -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName DTyVarBndrUnit
tvb, DKind
tvb_kind)
| DTyVarBndrUnit
tvb <- [DTyVarBndrUnit]
cls_tvbs
, Just DKind
tvb_kind <- [DTyVarBndrUnit -> Maybe DKind
forall flag. DTyVarBndr flag -> Maybe DKind
extractTvbKind DTyVarBndrUnit
tvb]
]
ascribe_tf_tvb_kind :: DTyVarBndrUnit -> DTyVarBndrUnit
ascribe_tf_tvb_kind :: DTyVarBndrUnit -> DTyVarBndrUnit
ascribe_tf_tvb_kind DTyVarBndrUnit
tvb =
case DTyVarBndrUnit
tvb of
DKindedTV{} -> DTyVarBndrUnit
tvb
DPlainTV Name
n ()
_ -> DTyVarBndrUnit
-> (DKind -> DTyVarBndrUnit) -> Maybe DKind -> DTyVarBndrUnit
forall b a. b -> (a -> b) -> Maybe a -> b
maybe DTyVarBndrUnit
tvb (Name -> () -> DKind -> DTyVarBndrUnit
forall flag. Name -> flag -> DKind -> DTyVarBndr flag
DKindedTV Name
n ()) (Maybe DKind -> DTyVarBndrUnit) -> Maybe DKind -> DTyVarBndrUnit
forall a b. (a -> b) -> a -> b
$ Name -> Map Name DKind -> Maybe DKind
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n Map Name DKind
cls_tvb_kind_map
buildDefunSyms :: DDec -> PrM [DDec]
buildDefunSyms :: DDec -> PrM [DDec]
buildDefunSyms DDec
dec =
case DDec
dec of
DDataD DataFlavor
_new_or_data DCxt
_cxt Name
_tyName [DTyVarBndrUnit]
_tvbs Maybe DKind
_k [DCon]
ctors [DDerivClause]
_derivings ->
[DCon] -> PrM [DDec]
buildDefunSymsDataD [DCon]
ctors
DClosedTypeFamilyD DTypeFamilyHead
tf_head [DTySynEqn]
_ ->
DTypeFamilyHead -> PrM [DDec]
buildDefunSymsClosedTypeFamilyD DTypeFamilyHead
tf_head
DOpenTypeFamilyD DTypeFamilyHead
tf_head ->
DTypeFamilyHead -> PrM [DDec]
buildDefunSymsOpenTypeFamilyD DTypeFamilyHead
tf_head
DTySynD Name
name [DTyVarBndrUnit]
tvbs DKind
rhs ->
Name -> [DTyVarBndrUnit] -> DKind -> PrM [DDec]
buildDefunSymsTySynD Name
name [DTyVarBndrUnit]
tvbs DKind
rhs
DClassD DCxt
_cxt Name
name [DTyVarBndrUnit]
tvbs [FunDep]
_fundeps [DDec]
_members ->
Name -> [DTyVarBndrUnit] -> Maybe DKind -> PrM [DDec]
defunReify Name
name [DTyVarBndrUnit]
tvbs (DKind -> Maybe DKind
forall a. a -> Maybe a
Just (Name -> DKind
DConT Name
constraintName))
DDec
_ -> String -> PrM [DDec]
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> PrM [DDec]) -> String -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ String
"Defunctionalization symbols can only be built for " String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"type families and data declarations"
buildDefunSymsClosedTypeFamilyD :: DTypeFamilyHead -> PrM [DDec]
buildDefunSymsClosedTypeFamilyD :: DTypeFamilyHead -> PrM [DDec]
buildDefunSymsClosedTypeFamilyD = (DTyVarBndrUnit -> DTyVarBndrUnit)
-> (Maybe DKind -> Maybe DKind) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndrUnit -> DTyVarBndrUnit
forall a. a -> a
id Maybe DKind -> Maybe DKind
forall a. a -> a
id
buildDefunSymsOpenTypeFamilyD :: DTypeFamilyHead -> PrM [DDec]
buildDefunSymsOpenTypeFamilyD :: DTypeFamilyHead -> PrM [DDec]
buildDefunSymsOpenTypeFamilyD =
(DTyVarBndrUnit -> DTyVarBndrUnit)
-> (Maybe DKind -> Maybe DKind) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndrUnit -> DTyVarBndrUnit
forall flag. DTyVarBndr flag -> DTyVarBndr flag
defaultTvbToTypeKind (DKind -> Maybe DKind
forall a. a -> Maybe a
Just (DKind -> Maybe DKind)
-> (Maybe DKind -> DKind) -> Maybe DKind -> Maybe DKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe DKind -> DKind
defaultMaybeToTypeKind)
buildDefunSymsTypeFamilyHead
:: (DTyVarBndrUnit -> DTyVarBndrUnit)
-> (Maybe DKind -> Maybe DKind)
-> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead :: (DTyVarBndrUnit -> DTyVarBndrUnit)
-> (Maybe DKind -> Maybe DKind) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndrUnit -> DTyVarBndrUnit
default_tvb Maybe DKind -> Maybe DKind
default_kind
(DTypeFamilyHead Name
name [DTyVarBndrUnit]
tvbs DFamilyResultSig
result_sig Maybe InjectivityAnn
_) = do
let arg_tvbs :: [DTyVarBndrUnit]
arg_tvbs = (DTyVarBndrUnit -> DTyVarBndrUnit)
-> [DTyVarBndrUnit] -> [DTyVarBndrUnit]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrUnit -> DTyVarBndrUnit
default_tvb [DTyVarBndrUnit]
tvbs
res_kind :: Maybe DKind
res_kind = Maybe DKind -> Maybe DKind
default_kind (DFamilyResultSig -> Maybe DKind
resultSigToMaybeKind DFamilyResultSig
result_sig)
Name -> [DTyVarBndrUnit] -> Maybe DKind -> PrM [DDec]
defunReify Name
name [DTyVarBndrUnit]
arg_tvbs Maybe DKind
res_kind
buildDefunSymsTySynD :: Name -> [DTyVarBndrUnit] -> DType -> PrM [DDec]
buildDefunSymsTySynD :: Name -> [DTyVarBndrUnit] -> DKind -> PrM [DDec]
buildDefunSymsTySynD Name
name [DTyVarBndrUnit]
tvbs DKind
rhs = Name -> [DTyVarBndrUnit] -> Maybe DKind -> PrM [DDec]
defunReify Name
name [DTyVarBndrUnit]
tvbs Maybe DKind
mb_res_kind
where
mb_res_kind :: Maybe DKind
mb_res_kind :: Maybe DKind
mb_res_kind = case DKind
rhs of
DSigT DKind
_ DKind
k -> DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
k
DKind
_ -> Maybe DKind
forall a. Maybe a
Nothing
buildDefunSymsDataD :: [DCon] -> PrM [DDec]
buildDefunSymsDataD :: [DCon] -> PrM [DDec]
buildDefunSymsDataD [DCon]
ctors =
(DCon -> PrM [DDec]) -> [DCon] -> PrM [DDec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM DCon -> PrM [DDec]
promoteCtor [DCon]
ctors
where
promoteCtor :: DCon -> PrM [DDec]
promoteCtor :: DCon -> PrM [DDec]
promoteCtor (DCon [DTyVarBndrSpec]
tvbs DCxt
_ Name
name DConFields
fields DKind
res_ty) = do
Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
let name' :: Name
name' = Options -> Name -> Name
promotedDataTypeOrConName Options
opts Name
name
arg_tys :: DCxt
arg_tys = DConFields -> DCxt
tysOfConFields DConFields
fields
DCxt
arg_kis <- (DKind -> PrM DKind) -> DCxt -> PrM DCxt
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse DKind -> PrM DKind
forall (m :: * -> *). OptionsMonad m => DKind -> m DKind
promoteType_NC DCxt
arg_tys
DKind
res_ki <- DKind -> PrM DKind
forall (m :: * -> *). OptionsMonad m => DKind -> m DKind
promoteType_NC DKind
res_ty
let con_ki :: DKind
con_ki = [DTyVarBndrSpec] -> DCxt -> DCxt -> DKind -> DKind
ravelVanillaDType [DTyVarBndrSpec]
tvbs [] DCxt
arg_kis DKind
res_ki
Maybe Fixity
m_fixity <- Name -> PrM (Maybe Fixity)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe Fixity)
reifyFixityWithLocals Name
name'
Name -> Maybe Fixity -> DefunKindInfo -> PrM [DDec]
defunctionalize Name
name' Maybe Fixity
m_fixity (DefunKindInfo -> PrM [DDec]) -> DefunKindInfo -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ DKind -> DefunKindInfo
DefunSAK DKind
con_ki
defunReify :: Name
-> [DTyVarBndrUnit]
-> Maybe DKind
-> PrM [DDec]
defunReify :: Name -> [DTyVarBndrUnit] -> Maybe DKind -> PrM [DDec]
defunReify Name
name [DTyVarBndrUnit]
tvbs Maybe DKind
m_res_kind = do
Maybe Fixity
m_fixity <- Name -> PrM (Maybe Fixity)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe Fixity)
reifyFixityWithLocals Name
name
Maybe DKind
m_sak <- Name -> PrM (Maybe DKind)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DKind)
dsReifyType Name
name
let defun :: DefunKindInfo -> PrM [DDec]
defun = Name -> Maybe Fixity -> DefunKindInfo -> PrM [DDec]
defunctionalize Name
name Maybe Fixity
m_fixity
case Maybe DKind
m_sak of
Just DKind
sak -> DefunKindInfo -> PrM [DDec]
defun (DefunKindInfo -> PrM [DDec]) -> DefunKindInfo -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ DKind -> DefunKindInfo
DefunSAK DKind
sak
Maybe DKind
Nothing -> DefunKindInfo -> PrM [DDec]
defun (DefunKindInfo -> PrM [DDec]) -> DefunKindInfo -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ [DTyVarBndrUnit] -> Maybe DKind -> DefunKindInfo
DefunNoSAK [DTyVarBndrUnit]
tvbs Maybe DKind
m_res_kind
defunctionalize :: Name
-> Maybe Fixity
-> DefunKindInfo
-> PrM [DDec]
defunctionalize :: Name -> Maybe Fixity -> DefunKindInfo -> PrM [DDec]
defunctionalize Name
name Maybe Fixity
m_fixity DefunKindInfo
defun_ki = do
case DefunKindInfo
defun_ki of
DefunSAK DKind
sak ->
case DKind -> Either String ([DTyVarBndrSpec], DCxt, DCxt, DKind)
unravelVanillaDType_either DKind
sak of
Left String
_ -> [DTyVarBndrUnit] -> Maybe DKind -> PrM [DDec]
defun_fallback [] (DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
sak)
Right ([DTyVarBndrSpec]
sak_tvbs, DCxt
_sak_cxt, DCxt
sak_arg_kis, DKind
sak_res_ki)
-> [DTyVarBndrSpec] -> DCxt -> DKind -> PrM [DDec]
defun_vanilla_sak [DTyVarBndrSpec]
sak_tvbs DCxt
sak_arg_kis DKind
sak_res_ki
DefunNoSAK [DTyVarBndrUnit]
tvbs Maybe DKind
m_res -> [DTyVarBndrUnit] -> Maybe DKind -> PrM [DDec]
defun_fallback [DTyVarBndrUnit]
tvbs Maybe DKind
m_res
where
defun_vanilla_sak :: [DTyVarBndrSpec] -> [DKind] -> DKind -> PrM [DDec]
defun_vanilla_sak :: [DTyVarBndrSpec] -> DCxt -> DKind -> PrM [DDec]
defun_vanilla_sak [DTyVarBndrSpec]
sak_tvbs DCxt
sak_arg_kis DKind
sak_res_ki = do
Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
Name
extra_name <- String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"arg"
let sak_arg_n :: Int
sak_arg_n = DCxt -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length DCxt
sak_arg_kis
[Name]
arg_names <- Int -> PrM Name -> PrM [Name]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
sak_arg_n (Name -> Name
noExactName (Name -> Name) -> PrM Name -> PrM Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"a")
let
go :: Int -> [(Name, DKind)] -> [(Name, DKind)] -> (DKind, [DDec])
go :: Int -> [(Name, DKind)] -> [(Name, DKind)] -> (DKind, [DDec])
go Int
n [(Name, DKind)]
arg_nks [(Name, DKind)]
res_nkss =
let arg_tvbs :: [DTyVarBndrUnit]
arg_tvbs :: [DTyVarBndrUnit]
arg_tvbs = ((Name, DKind) -> DTyVarBndrUnit)
-> [(Name, DKind)] -> [DTyVarBndrUnit]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
na, DKind
ki) -> Name -> () -> DKind -> DTyVarBndrUnit
forall flag. Name -> flag -> DKind -> DTyVarBndr flag
DKindedTV Name
na () DKind
ki) [(Name, DKind)]
arg_nks
mk_sak_dec :: DKind -> DDec
mk_sak_dec :: DKind -> DDec
mk_sak_dec DKind
res_ki =
Name -> DKind -> DDec
DKiSigD (Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
name Int
n) (DKind -> DDec) -> DKind -> DDec
forall a b. (a -> b) -> a -> b
$
[DTyVarBndrSpec] -> DCxt -> DCxt -> DKind -> DKind
ravelVanillaDType [DTyVarBndrSpec]
sak_tvbs [] (((Name, DKind) -> DKind) -> [(Name, DKind)] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (Name, DKind) -> DKind
forall a b. (a, b) -> b
snd [(Name, DKind)]
arg_nks) DKind
res_ki in
case [(Name, DKind)]
res_nkss of
[] ->
let sat_sak_dec :: DDec
sat_sak_dec = DKind -> DDec
mk_sak_dec DKind
sak_res_ki
sat_decs :: [DDec]
sat_decs = Options -> Int -> [DTyVarBndrUnit] -> Maybe DKind -> [DDec]
mk_sat_decs Options
opts Int
n [DTyVarBndrUnit]
arg_tvbs (DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
sak_res_ki)
in (DKind
sak_res_ki, DDec
sat_sak_decDDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
:[DDec]
sat_decs)
(Name, DKind)
res_nk:[(Name, DKind)]
res_nks ->
let (DKind
res_ki, [DDec]
decs) = Int -> [(Name, DKind)] -> [(Name, DKind)] -> (DKind, [DDec])
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ([(Name, DKind)]
arg_nks [(Name, DKind)] -> [(Name, DKind)] -> [(Name, DKind)]
forall a. [a] -> [a] -> [a]
++ [(Name, DKind)
res_nk]) [(Name, DKind)]
res_nks
tyfun :: DKind
tyfun = DKind -> DKind -> DKind
buildTyFunArrow ((Name, DKind) -> DKind
forall a b. (a, b) -> b
snd (Name, DKind)
res_nk) DKind
res_ki
defun_sak_dec :: DDec
defun_sak_dec = DKind -> DDec
mk_sak_dec DKind
tyfun
defun_other_decs :: [DDec]
defun_other_decs = Options
-> Int
-> Int
-> [DTyVarBndrUnit]
-> Name
-> Name
-> Maybe DKind
-> [DDec]
mk_defun_decs Options
opts Int
n Int
sak_arg_n
[DTyVarBndrUnit]
arg_tvbs ((Name, DKind) -> Name
forall a b. (a, b) -> a
fst (Name, DKind)
res_nk)
Name
extra_name (DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
tyfun)
in (DKind
tyfun, DDec
defun_sak_decDDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
:[DDec]
defun_other_decs [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
decs)
[DDec] -> PrM [DDec]
forall a. a -> PrM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DDec] -> PrM [DDec]) -> [DDec] -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ (DKind, [DDec]) -> [DDec]
forall a b. (a, b) -> b
snd ((DKind, [DDec]) -> [DDec]) -> (DKind, [DDec]) -> [DDec]
forall a b. (a -> b) -> a -> b
$ Int -> [(Name, DKind)] -> [(Name, DKind)] -> (DKind, [DDec])
go Int
0 [] ([(Name, DKind)] -> (DKind, [DDec]))
-> [(Name, DKind)] -> (DKind, [DDec])
forall a b. (a -> b) -> a -> b
$ [Name] -> DCxt -> [(Name, DKind)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
arg_names DCxt
sak_arg_kis
defun_fallback :: [DTyVarBndrUnit] -> Maybe DKind -> PrM [DDec]
defun_fallback :: [DTyVarBndrUnit] -> Maybe DKind -> PrM [DDec]
defun_fallback [DTyVarBndrUnit]
tvbs' Maybe DKind
m_res' = do
Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
Name
extra_name <- String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"arg"
([DTyVarBndrUnit]
tvbs, Maybe DKind
m_res) <- [DTyVarBndrUnit]
-> Maybe DKind -> PrM ([DTyVarBndrUnit], Maybe DKind)
eta_expand ([DTyVarBndrUnit] -> [DTyVarBndrUnit]
forall a. Data a => a -> a
noExactTyVars [DTyVarBndrUnit]
tvbs') (Maybe DKind -> Maybe DKind
forall a. Data a => a -> a
noExactTyVars Maybe DKind
m_res')
let tvbs_n :: Int
tvbs_n = [DTyVarBndrUnit] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DTyVarBndrUnit]
tvbs
go :: Int -> [DTyVarBndrUnit] -> [DTyVarBndrUnit] -> (Maybe DKind, [DDec])
go :: Int
-> [DTyVarBndrUnit] -> [DTyVarBndrUnit] -> (Maybe DKind, [DDec])
go Int
n [DTyVarBndrUnit]
arg_tvbs [DTyVarBndrUnit]
res_tvbss =
case [DTyVarBndrUnit]
res_tvbss of
[] ->
let sat_decs :: [DDec]
sat_decs = Options -> Int -> [DTyVarBndrUnit] -> Maybe DKind -> [DDec]
mk_sat_decs Options
opts Int
n [DTyVarBndrUnit]
arg_tvbs Maybe DKind
m_res
in (Maybe DKind
m_res, [DDec]
sat_decs)
DTyVarBndrUnit
res_tvb:[DTyVarBndrUnit]
res_tvbs ->
let (Maybe DKind
m_res_ki, [DDec]
decs) = Int
-> [DTyVarBndrUnit] -> [DTyVarBndrUnit] -> (Maybe DKind, [DDec])
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ([DTyVarBndrUnit]
arg_tvbs [DTyVarBndrUnit] -> [DTyVarBndrUnit] -> [DTyVarBndrUnit]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndrUnit
res_tvb]) [DTyVarBndrUnit]
res_tvbs
m_tyfun :: Maybe DKind
m_tyfun = Maybe DKind -> Maybe DKind -> Maybe DKind
buildTyFunArrow_maybe (DTyVarBndrUnit -> Maybe DKind
forall flag. DTyVarBndr flag -> Maybe DKind
extractTvbKind DTyVarBndrUnit
res_tvb)
Maybe DKind
m_res_ki
defun_decs' :: [DDec]
defun_decs' = Options
-> Int
-> Int
-> [DTyVarBndrUnit]
-> Name
-> Name
-> Maybe DKind
-> [DDec]
mk_defun_decs Options
opts Int
n Int
tvbs_n [DTyVarBndrUnit]
arg_tvbs
(DTyVarBndrUnit -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName DTyVarBndrUnit
res_tvb)
Name
extra_name Maybe DKind
m_tyfun
in (Maybe DKind
m_tyfun, [DDec]
defun_decs' [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
decs)
[DDec] -> PrM [DDec]
forall a. a -> PrM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DDec] -> PrM [DDec]) -> [DDec] -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ (Maybe DKind, [DDec]) -> [DDec]
forall a b. (a, b) -> b
snd ((Maybe DKind, [DDec]) -> [DDec])
-> (Maybe DKind, [DDec]) -> [DDec]
forall a b. (a -> b) -> a -> b
$ Int
-> [DTyVarBndrUnit] -> [DTyVarBndrUnit] -> (Maybe DKind, [DDec])
go Int
0 [] [DTyVarBndrUnit]
tvbs
mk_defun_decs :: Options
-> Int
-> Int
-> [DTyVarBndrUnit]
-> Name
-> Name
-> Maybe DKind
-> [DDec]
mk_defun_decs :: Options
-> Int
-> Int
-> [DTyVarBndrUnit]
-> Name
-> Name
-> Maybe DKind
-> [DDec]
mk_defun_decs Options
opts Int
n Int
fully_sat_n [DTyVarBndrUnit]
arg_tvbs Name
tyfun_name Name
extra_name Maybe DKind
m_tyfun =
let data_name :: Name
data_name = Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
name Int
n
next_name :: Name
next_name = Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
name (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
con_name :: Name
con_name = String -> String -> Name -> Name
prefixName String
"" String
":" (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ String -> String -> Name -> Name
suffixName String
"KindInference" String
"###" Name
data_name
arg_names :: [Name]
arg_names = (DTyVarBndrUnit -> Name) -> [DTyVarBndrUnit] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrUnit -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName [DTyVarBndrUnit]
arg_tvbs
params :: [DTyVarBndrUnit]
params = [DTyVarBndrUnit]
arg_tvbs [DTyVarBndrUnit] -> [DTyVarBndrUnit] -> [DTyVarBndrUnit]
forall a. [a] -> [a] -> [a]
++ [Name -> () -> DTyVarBndrUnit
forall flag. Name -> flag -> DTyVarBndr flag
DPlainTV Name
tyfun_name ()]
con_eq_ct :: DKind
con_eq_ct = Name -> DKind
DConT Name
sameKindName DKind -> DKind -> DKind
`DAppT` DKind
lhs DKind -> DKind -> DKind
`DAppT` DKind
rhs
where
lhs :: DKind
lhs = DKind -> DCxt -> DKind
foldType (Name -> DKind
DConT Name
data_name) ((Name -> DKind) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DKind
DVarT [Name]
arg_names) DKind -> DKind -> DKind
`apply` (Name -> DKind
DVarT Name
extra_name)
rhs :: DKind
rhs = DKind -> DCxt -> DKind
foldType (Name -> DKind
DConT Name
next_name) ((Name -> DKind) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DKind
DVarT ([Name]
arg_names [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
extra_name]))
con_decl :: DCon
con_decl = [DTyVarBndrSpec] -> DCxt -> Name -> DConFields -> DKind -> DCon
DCon [] [DKind
con_eq_ct] Name
con_name (Bool -> [DBangType] -> DConFields
DNormalC Bool
False [])
(DKind -> [DTyVarBndrUnit] -> DKind
forall flag. DKind -> [DTyVarBndr flag] -> DKind
foldTypeTvbs (Name -> DKind
DConT Name
data_name) [DTyVarBndrUnit]
params)
data_decl :: DDec
data_decl = DataFlavor
-> DCxt
-> Name
-> [DTyVarBndrUnit]
-> Maybe DKind
-> [DCon]
-> [DDerivClause]
-> DDec
DDataD DataFlavor
Data [] Name
data_name [DTyVarBndrUnit]
args Maybe DKind
m_tyfun [DCon
con_decl] []
where
args :: [DTyVarBndrUnit]
args | Maybe DKind -> Bool
forall a. Maybe a -> Bool
isJust Maybe DKind
m_tyfun = [DTyVarBndrUnit]
arg_tvbs
| Bool
otherwise = [DTyVarBndrUnit]
params
app_data_ty :: DKind
app_data_ty = DKind -> [DTyVarBndrUnit] -> DKind
forall flag. DKind -> [DTyVarBndr flag] -> DKind
foldTypeTvbs (Name -> DKind
DConT Name
data_name) [DTyVarBndrUnit]
arg_tvbs
app_eqn :: DTySynEqn
app_eqn = Maybe [DTyVarBndrUnit] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
(Name -> DKind
DConT Name
applyName DKind -> DKind -> DKind
`DAppT` DKind
app_data_ty
DKind -> DKind -> DKind
`DAppT` Name -> DKind
DVarT Name
tyfun_name)
(DKind -> [DTyVarBndrUnit] -> DKind
forall flag. DKind -> [DTyVarBndr flag] -> DKind
foldTypeTvbs (Name -> DKind
DConT Name
app_eqn_rhs_name)
([DTyVarBndrUnit]
arg_tvbs [DTyVarBndrUnit] -> [DTyVarBndrUnit] -> [DTyVarBndrUnit]
forall a. [a] -> [a] -> [a]
++ [Name -> () -> DTyVarBndrUnit
forall flag. Name -> flag -> DTyVarBndr flag
DPlainTV Name
tyfun_name ()]))
app_eqn_rhs_name :: Name
app_eqn_rhs_name | Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
fully_sat_n = Name
name
| Bool
otherwise = Name
next_name
app_decl :: DDec
app_decl = DTySynEqn -> DDec
DTySynInstD DTySynEqn
app_eqn
suppress :: DDec
suppress = Maybe Overlap
-> Maybe [DTyVarBndrUnit] -> DCxt -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing []
(Name -> DKind
DConT Name
suppressClassName DKind -> DKind -> DKind
`DAppT` DKind
app_data_ty)
[DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD Name
suppressMethodName
[[DPat] -> DExp -> DClause
DClause []
((Name -> DExp
DVarE 'snd) DExp -> DExp -> DExp
`DAppE`
[DExp] -> DExp
mkTupleDExp [Name -> DExp
DConE Name
con_name,
[DExp] -> DExp
mkTupleDExp []])]]
fixity_decl :: [DDec]
fixity_decl = Maybe DDec -> [DDec]
forall a. Maybe a -> [a]
maybeToList (Maybe DDec -> [DDec]) -> Maybe DDec -> [DDec]
forall a b. (a -> b) -> a -> b
$ (Fixity -> DDec) -> Maybe Fixity -> Maybe DDec
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> Fixity -> DDec
mk_fix_decl Name
data_name) Maybe Fixity
m_fixity
in DDec
data_decl DDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
: DDec
app_decl DDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
: DDec
suppress DDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
: [DDec]
fixity_decl
mk_sat_decs :: Options -> Int -> [DTyVarBndrUnit] -> Maybe DKind -> [DDec]
mk_sat_decs :: Options -> Int -> [DTyVarBndrUnit] -> Maybe DKind -> [DDec]
mk_sat_decs Options
opts Int
n [DTyVarBndrUnit]
sat_tvbs Maybe DKind
m_sat_res =
let sat_name :: Name
sat_name = Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
name Int
n
sat_dec :: DDec
sat_dec = DTypeFamilyHead -> [DTySynEqn] -> DDec
DClosedTypeFamilyD
(Name
-> [DTyVarBndrUnit]
-> DFamilyResultSig
-> Maybe InjectivityAnn
-> DTypeFamilyHead
DTypeFamilyHead Name
sat_name [DTyVarBndrUnit]
sat_tvbs
(Maybe DKind -> DFamilyResultSig
maybeKindToResultSig Maybe DKind
m_sat_res) Maybe InjectivityAnn
forall a. Maybe a
Nothing)
[Maybe [DTyVarBndrUnit] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
(DKind -> [DTyVarBndrUnit] -> DKind
forall flag. DKind -> [DTyVarBndr flag] -> DKind
foldTypeTvbs (Name -> DKind
DConT Name
sat_name) [DTyVarBndrUnit]
sat_tvbs)
(DKind -> [DTyVarBndrUnit] -> DKind
forall flag. DKind -> [DTyVarBndr flag] -> DKind
foldTypeTvbs (Name -> DKind
DConT Name
name) [DTyVarBndrUnit]
sat_tvbs)]
sat_fixity_dec :: [DDec]
sat_fixity_dec = Maybe DDec -> [DDec]
forall a. Maybe a -> [a]
maybeToList (Maybe DDec -> [DDec]) -> Maybe DDec -> [DDec]
forall a b. (a -> b) -> a -> b
$ (Fixity -> DDec) -> Maybe Fixity -> Maybe DDec
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> Fixity -> DDec
mk_fix_decl Name
sat_name) Maybe Fixity
m_fixity
in DDec
sat_dec DDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
: [DDec]
sat_fixity_dec
eta_expand :: [DTyVarBndrUnit] -> Maybe DKind -> PrM ([DTyVarBndrUnit], Maybe DKind)
eta_expand :: [DTyVarBndrUnit]
-> Maybe DKind -> PrM ([DTyVarBndrUnit], Maybe DKind)
eta_expand [DTyVarBndrUnit]
m_arg_tvbs Maybe DKind
Nothing = ([DTyVarBndrUnit], Maybe DKind)
-> PrM ([DTyVarBndrUnit], Maybe DKind)
forall a. a -> PrM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndrUnit]
m_arg_tvbs, Maybe DKind
forall a. Maybe a
Nothing)
eta_expand [DTyVarBndrUnit]
m_arg_tvbs (Just DKind
res_kind) = do
let (DFunArgs
arg_ks, DKind
result_k) = DKind -> (DFunArgs, DKind)
unravelDType DKind
res_kind
vis_arg_ks :: [DVisFunArg]
vis_arg_ks = DFunArgs -> [DVisFunArg]
filterDVisFunArgs DFunArgs
arg_ks
[DTyVarBndrUnit]
extra_arg_tvbs <- (DVisFunArg -> PrM DTyVarBndrUnit)
-> [DVisFunArg] -> PrM [DTyVarBndrUnit]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse DVisFunArg -> PrM DTyVarBndrUnit
mk_extra_tvb [DVisFunArg]
vis_arg_ks
([DTyVarBndrUnit], Maybe DKind)
-> PrM ([DTyVarBndrUnit], Maybe DKind)
forall a. a -> PrM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndrUnit]
m_arg_tvbs [DTyVarBndrUnit] -> [DTyVarBndrUnit] -> [DTyVarBndrUnit]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndrUnit]
extra_arg_tvbs, DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
result_k)
mk_extra_tvb :: DVisFunArg -> PrM DTyVarBndrUnit
mk_extra_tvb :: DVisFunArg -> PrM DTyVarBndrUnit
mk_extra_tvb DVisFunArg
vfa =
case DVisFunArg
vfa of
DVisFADep DTyVarBndrUnit
tvb -> DTyVarBndrUnit -> PrM DTyVarBndrUnit
forall a. a -> PrM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DTyVarBndrUnit
tvb
DVisFAAnon DKind
k -> (\Name
n -> Name -> () -> DKind -> DTyVarBndrUnit
forall flag. Name -> flag -> DKind -> DTyVarBndr flag
DKindedTV Name
n () DKind
k) (Name -> DTyVarBndrUnit) -> PrM Name -> PrM DTyVarBndrUnit
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(Name -> Name
noExactName (Name -> Name) -> PrM Name -> PrM Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"e")
mk_fix_decl :: Name -> Fixity -> DDec
mk_fix_decl :: Name -> Fixity -> DDec
mk_fix_decl Name
n Fixity
f = DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Fixity -> Name -> DLetDec
DInfixD Fixity
f Name
n
data DefunKindInfo
= DefunSAK DKind
| DefunNoSAK [DTyVarBndrUnit] (Maybe DKind)
buildTyFunArrow :: DKind -> DKind -> DKind
buildTyFunArrow :: DKind -> DKind -> DKind
buildTyFunArrow DKind
k1 DKind
k2 = Name -> DKind
DConT Name
tyFunArrowName DKind -> DKind -> DKind
`DAppT` DKind
k1 DKind -> DKind -> DKind
`DAppT` DKind
k2
buildTyFunArrow_maybe :: Maybe DKind -> Maybe DKind -> Maybe DKind
buildTyFunArrow_maybe :: Maybe DKind -> Maybe DKind -> Maybe DKind
buildTyFunArrow_maybe Maybe DKind
m_k1 Maybe DKind
m_k2 = DKind -> DKind -> DKind
buildTyFunArrow (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