{-# LANGUAGE TemplateHaskell #-}
module Data.Singletons.Promote.Defun where
import Language.Haskell.TH.Desugar
import Data.Singletons.Promote.Monad
import Data.Singletons.Promote.Type
import Data.Singletons.Names
import Language.Haskell.TH.Syntax
import Data.Singletons.Syntax
import Data.Singletons.TH.Options
import Data.Singletons.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 (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 DType
_ty Maybe Name
_mdec) =
String -> PrM [DDec]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Building defunctionalization symbols of values not supported"
defunInfo (DTyVarI Name
_name DType
_ty) =
String -> PrM [DDec]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Building defunctionalization symbols of type variables not supported"
defunInfo (DPatSynI {}) =
String -> PrM [DDec]
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 [DTyVarBndr]
tvbs DType
rhs) -> Name -> [DTyVarBndr] -> DType -> PrM [DDec]
buildDefunSymsTySynD Name
name [DTyVarBndr]
tvbs DType
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 ::
[DTyVarBndr]
-> [OpenTypeFamilyDecl]
-> PrM ()
defunAssociatedTypeFamilies :: [DTyVarBndr] -> [OpenTypeFamilyDecl] -> PrM ()
defunAssociatedTypeFamilies [DTyVarBndr]
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) =
(DTyVarBndr -> DTyVarBndr)
-> (Maybe DType -> Maybe DType) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndr -> DTyVarBndr
ascribe_tf_tvb_kind Maybe DType -> Maybe DType
forall a. a -> a
id DTypeFamilyHead
tf_head
cls_tvb_kind_map :: Map Name DKind
cls_tvb_kind_map :: Map Name DType
cls_tvb_kind_map = [(Name, DType)] -> Map Name DType
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (DTyVarBndr -> Name
extractTvbName DTyVarBndr
tvb, DType
tvb_kind)
| DTyVarBndr
tvb <- [DTyVarBndr]
cls_tvbs
, Just DType
tvb_kind <- [DTyVarBndr -> Maybe DType
extractTvbKind DTyVarBndr
tvb]
]
ascribe_tf_tvb_kind :: DTyVarBndr -> DTyVarBndr
ascribe_tf_tvb_kind :: DTyVarBndr -> DTyVarBndr
ascribe_tf_tvb_kind DTyVarBndr
tvb =
case DTyVarBndr
tvb of
DKindedTV{} -> DTyVarBndr
tvb
DPlainTV Name
n -> DTyVarBndr -> (DType -> DTyVarBndr) -> Maybe DType -> DTyVarBndr
forall b a. b -> (a -> b) -> Maybe a -> b
maybe DTyVarBndr
tvb (Name -> DType -> DTyVarBndr
DKindedTV Name
n) (Maybe DType -> DTyVarBndr) -> Maybe DType -> DTyVarBndr
forall a b. (a -> b) -> a -> b
$ Name -> Map Name DType -> Maybe DType
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n Map Name DType
cls_tvb_kind_map
buildDefunSyms :: DDec -> PrM [DDec]
buildDefunSyms :: DDec -> PrM [DDec]
buildDefunSyms DDec
dec =
case DDec
dec of
DDataD NewOrData
_new_or_data DCxt
_cxt Name
_tyName [DTyVarBndr]
_tvbs Maybe DType
_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 [DTyVarBndr]
tvbs DType
rhs ->
Name -> [DTyVarBndr] -> DType -> PrM [DDec]
buildDefunSymsTySynD Name
name [DTyVarBndr]
tvbs DType
rhs
DClassD DCxt
_cxt Name
name [DTyVarBndr]
tvbs [FunDep]
_fundeps [DDec]
_members ->
Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defunReify Name
name [DTyVarBndr]
tvbs (DType -> Maybe DType
forall a. a -> Maybe a
Just (Name -> DType
DConT Name
constraintName))
DDec
_ -> String -> PrM [DDec]
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 = (DTyVarBndr -> DTyVarBndr)
-> (Maybe DType -> Maybe DType) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndr -> DTyVarBndr
forall a. a -> a
id Maybe DType -> Maybe DType
forall a. a -> a
id
buildDefunSymsOpenTypeFamilyD :: DTypeFamilyHead -> PrM [DDec]
buildDefunSymsOpenTypeFamilyD :: DTypeFamilyHead -> PrM [DDec]
buildDefunSymsOpenTypeFamilyD =
(DTyVarBndr -> DTyVarBndr)
-> (Maybe DType -> Maybe DType) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndr -> DTyVarBndr
defaultTvbToTypeKind (DType -> Maybe DType
forall a. a -> Maybe a
Just (DType -> Maybe DType)
-> (Maybe DType -> DType) -> Maybe DType -> Maybe DType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe DType -> DType
defaultMaybeToTypeKind)
buildDefunSymsTypeFamilyHead
:: (DTyVarBndr -> DTyVarBndr)
-> (Maybe DKind -> Maybe DKind)
-> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead :: (DTyVarBndr -> DTyVarBndr)
-> (Maybe DType -> Maybe DType) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndr -> DTyVarBndr
default_tvb Maybe DType -> Maybe DType
default_kind
(DTypeFamilyHead Name
name [DTyVarBndr]
tvbs DFamilyResultSig
result_sig Maybe InjectivityAnn
_) = do
let arg_tvbs :: [DTyVarBndr]
arg_tvbs = (DTyVarBndr -> DTyVarBndr) -> [DTyVarBndr] -> [DTyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> DTyVarBndr
default_tvb [DTyVarBndr]
tvbs
res_kind :: Maybe DType
res_kind = Maybe DType -> Maybe DType
default_kind (DFamilyResultSig -> Maybe DType
resultSigToMaybeKind DFamilyResultSig
result_sig)
Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defunReify Name
name [DTyVarBndr]
arg_tvbs Maybe DType
res_kind
buildDefunSymsTySynD :: Name -> [DTyVarBndr] -> DType -> PrM [DDec]
buildDefunSymsTySynD :: Name -> [DTyVarBndr] -> DType -> PrM [DDec]
buildDefunSymsTySynD Name
name [DTyVarBndr]
tvbs DType
rhs = Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defunReify Name
name [DTyVarBndr]
tvbs Maybe DType
mb_res_kind
where
mb_res_kind :: Maybe DKind
mb_res_kind :: Maybe DType
mb_res_kind = case DType
rhs of
DSigT DType
_ DType
k -> DType -> Maybe DType
forall a. a -> Maybe a
Just DType
k
DType
_ -> Maybe DType
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 [DTyVarBndr]
tvbs DCxt
_ Name
name DConFields
fields DType
res_ty) = do
let arg_tys :: DCxt
arg_tys = DConFields -> DCxt
tysOfConFields DConFields
fields
DCxt
arg_kis <- (DType -> PrM DType) -> DCxt -> PrM DCxt
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse DType -> PrM DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType_NC DCxt
arg_tys
DType
res_ki <- DType -> PrM DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType_NC DType
res_ty
let con_ki :: DType
con_ki = [DTyVarBndr] -> DCxt -> DCxt -> DType -> DType
ravelVanillaDType [DTyVarBndr]
tvbs [] DCxt
arg_kis DType
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
$ DType -> DefunKindInfo
DefunSAK DType
con_ki
defunReify :: Name
-> [DTyVarBndr]
-> Maybe DKind
-> PrM [DDec]
defunReify :: Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defunReify Name
name [DTyVarBndr]
tvbs Maybe DType
m_res_kind = do
Maybe Fixity
m_fixity <- Name -> PrM (Maybe Fixity)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe Fixity)
reifyFixityWithLocals Name
name
Maybe DType
m_sak <- Name -> PrM (Maybe DType)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DType)
dsReifyType Name
name
let defun :: DefunKindInfo -> PrM [DDec]
defun = Name -> Maybe Fixity -> DefunKindInfo -> PrM [DDec]
defunctionalize Name
name Maybe Fixity
m_fixity
case Maybe DType
m_sak of
Just DType
sak -> DefunKindInfo -> PrM [DDec]
defun (DefunKindInfo -> PrM [DDec]) -> DefunKindInfo -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ DType -> DefunKindInfo
DefunSAK DType
sak
Maybe DType
Nothing -> DefunKindInfo -> PrM [DDec]
defun (DefunKindInfo -> PrM [DDec]) -> DefunKindInfo -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ [DTyVarBndr] -> Maybe DType -> DefunKindInfo
DefunNoSAK [DTyVarBndr]
tvbs Maybe DType
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 DType
sak ->
case DType -> Either String ([DTyVarBndr], DCxt, DCxt, DType)
unravelVanillaDType_either DType
sak of
Left String
_ -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defun_fallback [] (DType -> Maybe DType
forall a. a -> Maybe a
Just DType
sak)
Right ([DTyVarBndr]
sak_tvbs, DCxt
_sak_cxt, DCxt
sak_arg_kis, DType
sak_res_ki)
-> [DTyVarBndr] -> DCxt -> DType -> PrM [DDec]
defun_vanilla_sak [DTyVarBndr]
sak_tvbs DCxt
sak_arg_kis DType
sak_res_ki
DefunNoSAK [DTyVarBndr]
tvbs Maybe DType
m_res -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defun_fallback [DTyVarBndr]
tvbs Maybe DType
m_res
where
defun_vanilla_sak :: [DTyVarBndr] -> [DKind] -> DKind -> PrM [DDec]
defun_vanilla_sak :: [DTyVarBndr] -> DCxt -> DType -> PrM [DDec]
defun_vanilla_sak [DTyVarBndr]
sak_tvbs DCxt
sak_arg_kis DType
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"
[Name]
arg_names <- Int -> PrM Name -> PrM [Name]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM (DCxt -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length DCxt
sak_arg_kis) (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, DType)] -> [(Name, DType)] -> (DType, [DDec])
go Int
n [(Name, DType)]
arg_nks [(Name, DType)]
res_nkss =
case [(Name, DType)]
res_nkss of
[] ->
let
sat_decs :: [DDec]
sat_decs = Options -> Int -> [DTyVarBndr] -> Maybe DType -> [DDec]
mk_sat_decs Options
opts Int
n (((Name, DType) -> DTyVarBndr) -> [(Name, DType)] -> [DTyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map ((Name -> DType -> DTyVarBndr) -> (Name, DType) -> DTyVarBndr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> DType -> DTyVarBndr
DKindedTV) [(Name, DType)]
arg_nks)
(DType -> Maybe DType
forall a. a -> Maybe a
Just DType
sak_res_ki)
in (DType
sak_res_ki, [DDec]
sat_decs)
(Name, DType)
res_nk:[(Name, DType)]
res_nks ->
let (DType
res_ki, [DDec]
decs) = Int -> [(Name, DType)] -> [(Name, DType)] -> (DType, [DDec])
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ([(Name, DType)]
arg_nks [(Name, DType)] -> [(Name, DType)] -> [(Name, DType)]
forall a. [a] -> [a] -> [a]
++ [(Name, DType)
res_nk]) [(Name, DType)]
res_nks
tyfun :: DType
tyfun = DType -> DType -> DType
buildTyFunArrow ((Name, DType) -> DType
forall a b. (a, b) -> b
snd (Name, DType)
res_nk) DType
res_ki
defun_sak_dec :: DDec
defun_sak_dec = Name -> DType -> DDec
DKiSigD (Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
name Int
n) (DType -> DDec) -> DType -> DDec
forall a b. (a -> b) -> a -> b
$
[DTyVarBndr] -> DCxt -> DCxt -> DType -> DType
ravelVanillaDType [DTyVarBndr]
sak_tvbs [] (((Name, DType) -> DType) -> [(Name, DType)] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (Name, DType) -> DType
forall a b. (a, b) -> b
snd [(Name, DType)]
arg_nks) DType
tyfun
defun_other_decs :: [DDec]
defun_other_decs = Options
-> Int -> [DTyVarBndr] -> Name -> Name -> Maybe DType -> [DDec]
mk_defun_decs Options
opts Int
n (((Name, DType) -> DTyVarBndr) -> [(Name, DType)] -> [DTyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> DTyVarBndr
DPlainTV (Name -> DTyVarBndr)
-> ((Name, DType) -> Name) -> (Name, DType) -> DTyVarBndr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, DType) -> Name
forall a b. (a, b) -> a
fst) [(Name, DType)]
arg_nks)
((Name, DType) -> Name
forall a b. (a, b) -> a
fst (Name, DType)
res_nk) Name
extra_name Maybe DType
forall a. Maybe a
Nothing
in (DType
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 (f :: * -> *) a. Applicative f => a -> f a
pure ([DDec] -> PrM [DDec]) -> [DDec] -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ (DType, [DDec]) -> [DDec]
forall a b. (a, b) -> b
snd ((DType, [DDec]) -> [DDec]) -> (DType, [DDec]) -> [DDec]
forall a b. (a -> b) -> a -> b
$ Int -> [(Name, DType)] -> [(Name, DType)] -> (DType, [DDec])
go Int
0 [] ([(Name, DType)] -> (DType, [DDec]))
-> [(Name, DType)] -> (DType, [DDec])
forall a b. (a -> b) -> a -> b
$ [Name] -> DCxt -> [(Name, DType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
arg_names DCxt
sak_arg_kis
defun_fallback :: [DTyVarBndr] -> Maybe DKind -> PrM [DDec]
defun_fallback :: [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defun_fallback [DTyVarBndr]
tvbs' Maybe DType
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"
([DTyVarBndr]
tvbs, Maybe DType
m_res) <- [DTyVarBndr] -> Maybe DType -> PrM ([DTyVarBndr], Maybe DType)
eta_expand ([DTyVarBndr] -> [DTyVarBndr]
forall a. Data a => a -> a
noExactTyVars [DTyVarBndr]
tvbs') (Maybe DType -> Maybe DType
forall a. Data a => a -> a
noExactTyVars Maybe DType
m_res')
let
go :: Int -> [DTyVarBndr] -> [DTyVarBndr] -> (Maybe DKind, [DDec])
go :: Int -> [DTyVarBndr] -> [DTyVarBndr] -> (Maybe DType, [DDec])
go Int
n [DTyVarBndr]
arg_tvbs [DTyVarBndr]
res_tvbss =
case [DTyVarBndr]
res_tvbss of
[] ->
let sat_decs :: [DDec]
sat_decs = Options -> Int -> [DTyVarBndr] -> Maybe DType -> [DDec]
mk_sat_decs Options
opts Int
n [DTyVarBndr]
arg_tvbs Maybe DType
m_res
in (Maybe DType
m_res, [DDec]
sat_decs)
DTyVarBndr
res_tvb:[DTyVarBndr]
res_tvbs ->
let (Maybe DType
m_res_ki, [DDec]
decs) = Int -> [DTyVarBndr] -> [DTyVarBndr] -> (Maybe DType, [DDec])
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ([DTyVarBndr]
arg_tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndr
res_tvb]) [DTyVarBndr]
res_tvbs
m_tyfun :: Maybe DType
m_tyfun = Maybe DType -> Maybe DType -> Maybe DType
buildTyFunArrow_maybe (DTyVarBndr -> Maybe DType
extractTvbKind DTyVarBndr
res_tvb)
Maybe DType
m_res_ki
defun_decs' :: [DDec]
defun_decs' = Options
-> Int -> [DTyVarBndr] -> Name -> Name -> Maybe DType -> [DDec]
mk_defun_decs Options
opts Int
n [DTyVarBndr]
arg_tvbs
(DTyVarBndr -> Name
extractTvbName DTyVarBndr
res_tvb)
Name
extra_name Maybe DType
m_tyfun
in (Maybe DType
m_tyfun, [DDec]
defun_decs' [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
decs)
[DDec] -> PrM [DDec]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DDec] -> PrM [DDec]) -> [DDec] -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ (Maybe DType, [DDec]) -> [DDec]
forall a b. (a, b) -> b
snd ((Maybe DType, [DDec]) -> [DDec])
-> (Maybe DType, [DDec]) -> [DDec]
forall a b. (a -> b) -> a -> b
$ Int -> [DTyVarBndr] -> [DTyVarBndr] -> (Maybe DType, [DDec])
go Int
0 [] [DTyVarBndr]
tvbs
mk_defun_decs :: Options
-> Int
-> [DTyVarBndr]
-> Name
-> Name
-> Maybe DKind
-> [DDec]
mk_defun_decs :: Options
-> Int -> [DTyVarBndr] -> Name -> Name -> Maybe DType -> [DDec]
mk_defun_decs Options
opts Int
n [DTyVarBndr]
arg_tvbs Name
tyfun_name Name
extra_name Maybe DType
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 = (DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> Name
extractTvbName [DTyVarBndr]
arg_tvbs
params :: [DTyVarBndr]
params = [DTyVarBndr]
arg_tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ [Name -> DTyVarBndr
DPlainTV Name
tyfun_name]
con_eq_ct :: DType
con_eq_ct = Name -> DType
DConT Name
sameKindName DType -> DType -> DType
`DAppT` DType
lhs DType -> DType -> DType
`DAppT` DType
rhs
where
lhs :: DType
lhs = DType -> DCxt -> DType
foldType (Name -> DType
DConT Name
data_name) ((Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DVarT [Name]
arg_names) DType -> DType -> DType
`apply` (Name -> DType
DVarT Name
extra_name)
rhs :: DType
rhs = DType -> DCxt -> DType
foldType (Name -> DType
DConT Name
next_name) ((Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DVarT ([Name]
arg_names [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
extra_name]))
con_decl :: DCon
con_decl = [DTyVarBndr] -> DCxt -> Name -> DConFields -> DType -> DCon
DCon [] [DType
con_eq_ct] Name
con_name (Bool -> [DBangType] -> DConFields
DNormalC Bool
False [])
(DType -> [DTyVarBndr] -> DType
foldTypeTvbs (Name -> DType
DConT Name
data_name) [DTyVarBndr]
params)
data_decl :: DDec
data_decl = NewOrData
-> DCxt
-> Name
-> [DTyVarBndr]
-> Maybe DType
-> [DCon]
-> [DDerivClause]
-> DDec
DDataD NewOrData
Data [] Name
data_name [DTyVarBndr]
args Maybe DType
m_tyfun [DCon
con_decl] []
where
args :: [DTyVarBndr]
args | Maybe DType -> Bool
forall a. Maybe a -> Bool
isJust Maybe DType
m_tyfun = [DTyVarBndr]
arg_tvbs
| Bool
otherwise = [DTyVarBndr]
params
app_data_ty :: DType
app_data_ty = DType -> [DTyVarBndr] -> DType
foldTypeTvbs (Name -> DType
DConT Name
data_name) [DTyVarBndr]
arg_tvbs
app_eqn :: DTySynEqn
app_eqn = Maybe [DTyVarBndr] -> DType -> DType -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr]
forall a. Maybe a
Nothing
(Name -> DType
DConT Name
applyName DType -> DType -> DType
`DAppT` DType
app_data_ty
DType -> DType -> DType
`DAppT` Name -> DType
DVarT Name
tyfun_name)
(DType -> [DTyVarBndr] -> DType
foldTypeTvbs (Name -> DType
DConT Name
next_name)
([DTyVarBndr]
arg_tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ [Name -> DTyVarBndr
DPlainTV Name
tyfun_name]))
app_decl :: DDec
app_decl = DTySynEqn -> DDec
DTySynInstD DTySynEqn
app_eqn
suppress :: DDec
suppress = Maybe Overlap
-> Maybe [DTyVarBndr] -> DCxt -> DType -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndr]
forall a. Maybe a
Nothing []
(Name -> DType
DConT Name
suppressClassName DType -> DType -> DType
`DAppT` DType
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 (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 -> [DTyVarBndr] -> Maybe DKind -> [DDec]
mk_sat_decs :: Options -> Int -> [DTyVarBndr] -> Maybe DType -> [DDec]
mk_sat_decs Options
opts Int
n [DTyVarBndr]
sat_tvbs Maybe DType
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 = Name -> [DTyVarBndr] -> DType -> DDec
DTySynD Name
sat_name [DTyVarBndr]
sat_tvbs (DType -> DDec) -> DType -> DDec
forall a b. (a -> b) -> a -> b
$
DType -> [DTyVarBndr] -> DType
foldTypeTvbs (Name -> DType
DConT Name
name) [DTyVarBndr]
sat_tvbs DType -> Maybe DType -> DType
`maybeSigT` Maybe DType
m_sat_res
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 (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 :: [DTyVarBndr] -> Maybe DKind -> PrM ([DTyVarBndr], Maybe DKind)
eta_expand :: [DTyVarBndr] -> Maybe DType -> PrM ([DTyVarBndr], Maybe DType)
eta_expand [DTyVarBndr]
m_arg_tvbs Maybe DType
Nothing = ([DTyVarBndr], Maybe DType) -> PrM ([DTyVarBndr], Maybe DType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndr]
m_arg_tvbs, Maybe DType
forall a. Maybe a
Nothing)
eta_expand [DTyVarBndr]
m_arg_tvbs (Just DType
res_kind) = do
let (DFunArgs
arg_ks, DType
result_k) = DType -> (DFunArgs, DType)
unravelDType DType
res_kind
vis_arg_ks :: [DVisFunArg]
vis_arg_ks = DFunArgs -> [DVisFunArg]
filterDVisFunArgs DFunArgs
arg_ks
[DTyVarBndr]
extra_arg_tvbs <- (DVisFunArg -> PrM DTyVarBndr) -> [DVisFunArg] -> PrM [DTyVarBndr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse DVisFunArg -> PrM DTyVarBndr
mk_extra_tvb [DVisFunArg]
vis_arg_ks
([DTyVarBndr], Maybe DType) -> PrM ([DTyVarBndr], Maybe DType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndr]
m_arg_tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndr]
extra_arg_tvbs, DType -> Maybe DType
forall a. a -> Maybe a
Just DType
result_k)
mk_extra_tvb :: DVisFunArg -> PrM DTyVarBndr
mk_extra_tvb :: DVisFunArg -> PrM DTyVarBndr
mk_extra_tvb DVisFunArg
vfa =
case DVisFunArg
vfa of
DVisFADep DTyVarBndr
tvb -> DTyVarBndr -> PrM DTyVarBndr
forall (f :: * -> *) a. Applicative f => a -> f a
pure DTyVarBndr
tvb
DVisFAAnon DType
k -> Name -> DType -> DTyVarBndr
DKindedTV (Name -> DType -> DTyVarBndr)
-> PrM Name -> PrM (DType -> DTyVarBndr)
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" PrM (DType -> DTyVarBndr) -> PrM DType -> PrM DTyVarBndr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DType -> PrM DType
forall (f :: * -> *) a. Applicative f => a -> f a
pure DType
k
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 [DTyVarBndr] (Maybe DKind)
buildTyFunArrow :: DKind -> DKind -> DKind
buildTyFunArrow :: DType -> DType -> DType
buildTyFunArrow DType
k1 DType
k2 = Name -> DType
DConT Name
tyFunArrowName DType -> DType -> DType
`DAppT` DType
k1 DType -> DType -> DType
`DAppT` DType
k2
buildTyFunArrow_maybe :: Maybe DKind -> Maybe DKind -> Maybe DKind
buildTyFunArrow_maybe :: Maybe DType -> Maybe DType -> Maybe DType
buildTyFunArrow_maybe Maybe DType
m_k1 Maybe DType
m_k2 = DType -> DType -> DType
buildTyFunArrow (DType -> DType -> DType) -> Maybe DType -> Maybe (DType -> DType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe DType
m_k1 Maybe (DType -> DType) -> Maybe DType -> Maybe DType
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe DType
m_k2