singletons-1.0: src/Data/Singletons/Promote.hs
{- Data/Singletons/Promote.hs
(c) Richard Eisenberg 2013
eir@cis.upenn.edu
This file contains functions to promote term-level constructs to the
type level. It is an internal module to the singletons package.
-}
{-# LANGUAGE TemplateHaskell, CPP, MultiWayIf, LambdaCase, TupleSections #-}
module Data.Singletons.Promote where
import Language.Haskell.TH hiding ( Q, cxt )
import Language.Haskell.TH.Syntax ( Quasi(..) )
import Language.Haskell.TH.Desugar
import Language.Haskell.TH.Desugar.Sweeten
import Data.Singletons.Names
import Data.Singletons.Promote.Monad
import Data.Singletons.Promote.Eq
import Data.Singletons.Promote.Ord
import Data.Singletons.Promote.Bounded
import Data.Singletons.Promote.Defun
import Data.Singletons.Promote.Type
import Data.Singletons.Util
import Data.Singletons.Syntax
import Prelude hiding (exp)
import Control.Monad
import Control.Applicative
import Data.Maybe
import qualified Data.Map.Strict as Map
import Data.Map.Strict ( Map )
-- | Generate promoted definitions from a type that is already defined.
-- This is generally only useful with classes.
genPromotions :: Quasi q => [Name] -> q [Dec]
genPromotions names = do
checkForRep names
infos <- mapM reifyWithWarning names
dinfos <- mapM dsInfo infos
ddecs <- promoteM_ $ mapM_ promoteInfo dinfos
return $ decsToTH ddecs
-- | Promote every declaration given to the type level, retaining the originals.
promote :: Quasi q => q [Dec] -> q [Dec]
promote qdec = do
decls <- qdec
ddecls <- dsDecs decls
promDecls <- promoteM_ $ promoteDecs ddecls
return $ decls ++ decsToTH promDecls
-- | Promote each declaration, discarding the originals.
promoteOnly :: Quasi q => q [Dec] -> q [Dec]
promoteOnly qdec = do
decls <- qdec
ddecls <- dsDecs decls
promDecls <- promoteM_ $ promoteDecs ddecls
return $ decsToTH promDecls
-- | Generate defunctionalization symbols for existing type family
genDefunSymbols :: Quasi q => [Name] -> q [Dec]
genDefunSymbols names = do
checkForRep names
infos <- mapM (dsInfo <=< reifyWithWarning) names
decs <- promoteMDecs $ concatMapM defunInfo infos
return $ decsToTH decs
-- | Produce instances for '(:==)' (type-level equality) from the given types
promoteEqInstances :: Quasi q => [Name] -> q [Dec]
promoteEqInstances = concatMapM promoteEqInstance
-- | Produce instances for 'Compare' from the given types
promoteOrdInstances :: Quasi q => [Name] -> q [Dec]
promoteOrdInstances = concatMapM promoteOrdInstance
-- | Produce instances for 'MinBound' and 'MaxBound' from the given types
promoteBoundedInstances :: Quasi q => [Name] -> q [Dec]
promoteBoundedInstances = concatMapM promoteBoundedInstance
-- | Produce an instance for '(:==)' (type-level equality) from the given type
promoteEqInstance :: Quasi q => Name -> q [Dec]
promoteEqInstance name = do
(_tvbs, cons) <- getDataD "I cannot make an instance of (:==) for it." name
cons' <- mapM dsCon cons
#if __GLASGOW_HASKELL__ >= 707
vars <- replicateM (length _tvbs) (qNewName "k")
kind <- promoteType (foldType (DConT name) (map DVarT vars))
inst_decs <- mkEqTypeInstance kind cons'
return $ decsToTH inst_decs
#else
let pairs = [(c1, c2) | c1 <- cons, c2 <- cons]
mapM (fmap decsToTH . mkEqTypeInstance) pairs
#endif
-- | Produce an instance for 'Compare' from the given type
promoteOrdInstance :: Quasi q => Name -> q [Dec]
promoteOrdInstance name = do
(_tvbs, cons) <- getDataD "I cannot make an instance of Ord for it." name
cons' <- mapM dsCon cons
#if __GLASGOW_HASKELL__ >= 707
vars <- replicateM (length _tvbs) (qNewName "k")
kind <- promoteType (foldType (DConT name) (map DVarT vars))
inst_decs <- mkOrdTypeInstance kind cons'
return $ decsToTH inst_decs
#else
fail "promoteOrdInstance not implemented for GHC 7.6"
#endif
-- | Produce an instance for 'MinBound' and 'MaxBound' from the given type
promoteBoundedInstance :: Quasi q => Name -> q [Dec]
promoteBoundedInstance name = do
(_tvbs, cons) <- getDataD "I cannot make an instance of Bounded for it." name
cons' <- mapM dsCon cons
#if __GLASGOW_HASKELL__ >= 707
vars <- replicateM (length _tvbs) (qNewName "k")
kind <- promoteType (foldType (DConT name) (map DVarT vars))
inst_decs <- mkBoundedTypeInstance kind cons'
return $ decsToTH inst_decs
#else
fail "promoteBoundedInstance not implemented for GHC 7.6"
#endif
promoteInfo :: DInfo -> PrM ()
promoteInfo (DTyConI dec _instances) = promoteDecs [dec]
promoteInfo (DPrimTyConI _name _numArgs _unlifted) =
fail "Promotion of primitive type constructors not supported"
promoteInfo (DVarI _name _ty _mdec _fixity) =
fail "Promotion of individual values not supported"
promoteInfo (DTyVarI _name _ty) =
fail "Promotion of individual type variables not supported"
-- Note [Promoting declarations in two stages]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- It is necessary to know the types of things when promoting. So,
-- we promote in two stages: first, we build a LetDecEnv, which allows
-- for easy lookup. Then, we go through the actual elements of the LetDecEnv,
-- performing the promotion.
--
-- Why do we need the types? For kind annotations on the type family. We also
-- need to have both the types and the actual function definition at the same
-- time, because the function definition tells us how many patterns are
-- matched. Note that an eta-contracted function needs to return a TyFun,
-- not a proper type-level function.
--
-- Consider this example:
--
-- foo :: Nat -> Bool -> Bool
-- foo Zero = id
-- foo _ = not
--
-- Here the first parameter to foo is non-uniform, because it is
-- inspected in a pattern and can be different in each defining
-- equation of foo. The second parameter to foo, specified in the type
-- signature as Bool, is a uniform parameter - it is not inspected and
-- each defining equation of foo uses it the same way. The foo
-- function will be promoted to a type familty Foo like this:
--
-- type family Foo (n :: Nat) :: TyFun Bool Bool -> * where
-- Foo Zero = Id
-- Foo a = Not
--
-- To generate type signature for Foo type family we must first learn
-- what is the actual number of patterns used in defining cequations
-- of foo. In this case there is only one so we declare Foo to take
-- one argument and have return type of Bool -> Bool.
-- Promote a list of top-level declarations.
promoteDecs :: [DDec] -> PrM ()
promoteDecs decls = do
checkForRepInDecls decls
-- See Note [Promoting declarations in two stages]
PDecs { pd_let_decs = let_decs
, pd_class_decs = classes
, pd_instance_decs = insts
, pd_data_decs = datas } <- partitionDecs decls
-- promoteLetDecs returns LetBinds, which we don't need at top level
_ <- promoteLetDecs noPrefix let_decs
(cls_tvb_env, meth_sigs) <- concatMapM promoteClassDec classes
mapM_ (promoteInstanceDec cls_tvb_env meth_sigs) insts
promoteDataDecs datas
promoteDataDecs :: [DataDecl] -> PrM ()
promoteDataDecs data_decs = do
rec_selectors <- concatMapM extract_rec_selectors data_decs
_ <- promoteLetDecs noPrefix rec_selectors
mapM_ promoteDataDec data_decs
where
extract_rec_selectors :: DataDecl -> PrM [DLetDec]
extract_rec_selectors (DataDecl _nd data_name tvbs cons _derivings) =
let arg_ty = foldType (DConT data_name)
(map (DVarT . extractTvbName) tvbs)
in
concatMapM (getRecordSelectors arg_ty) cons
-- curious about ALetDecEnv? See the LetDecEnv module for an explanation.
promoteLetDecs :: String -- prefix to use on all new definitions
-> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
promoteLetDecs prefix decls = do
let_dec_env <- buildLetDecEnv decls
all_locals <- allLocals
let binds = [ (name, foldType (DConT sym) (map DVarT all_locals))
| name <- Map.keys $ lde_defns let_dec_env
, let proName = promoteValNameLhsPrefix prefix name
sym = promoteTySym proName (length all_locals) ]
(decs, let_dec_env') <- letBind binds $ promoteLetDecEnv prefix let_dec_env
emitDecs decs
return (binds, let_dec_env' { lde_proms = Map.fromList binds })
noPrefix :: String
noPrefix = ""
-- Promotion of data types to kinds is automatic (see "Ginving Haskell a
-- Promotion" paper for more details). Here we "plug into" the promotion
-- mechanism to add some extra stuff to the promotion:
--
-- * if data type derives Eq we generate a type family that implements the
-- equality test for the data type.
--
-- * for each data constructor with arity greater than 0 we generate type level
-- symbols for use with Apply type family. In this way promoted data
-- constructors and promoted functions can be used in a uniform way at the
-- type level in the same way they can be used uniformly at the type level.
--
-- * for each nullary data constructor we generate a type synonym
promoteDataDec :: DataDecl -> PrM ()
promoteDataDec (DataDecl _nd name tvbs ctors derivings) = do
#if __GLASGOW_HASKELL__ < 707
when (_nd == Newtype) $
fail $ "Newtypes don't promote under GHC 7.6. " ++
"Use <<data>> instead or upgrade GHC."
#endif
-- deriving Eq instance
_kvs <- replicateM (length tvbs) (qNewName "k")
_kind <- promoteType (foldType (DConT name) (map DVarT _kvs))
when (elem eqName derivings) $ do
#if __GLASGOW_HASKELL__ >= 707
eq_decs <- mkEqTypeInstance _kind ctors
#else
let pairs = [ (c1, c2) | c1 <- ctors, c2 <- ctors ]
eq_decs <- mapM mkEqTypeInstance pairs
#endif
emitDecs eq_decs
-- deriving Ord instance
when (elem ordName derivings) $ do
#if __GLASGOW_HASKELL__ >= 707
ord_decs <- mkOrdTypeInstance _kind ctors
#else
fail "Ord deriving not yet implemented in GHC 7.6"
#endif
emitDecs ord_decs
-- deriving Bounded instance
when (elem boundedName derivings) $ do
#if __GLASGOW_HASKELL__ >= 707
bounded_decs <- mkBoundedTypeInstance _kind ctors
#else
fail "Bounded deriving not yet implemented in GHC 7.6"
#endif
emitDecs bounded_decs
ctorSyms <- buildDefunSymsDataD name tvbs ctors
emitDecs ctorSyms
promoteClassDec :: ClassDecl
-> PrM ( Map Name [Name] -- from class names to tyvar lists
, Map Name DType ) -- returns method signatures
promoteClassDec (ClassDecl cxt cls_name tvbs
(LetDecEnv { lde_defns = defaults
, lde_types = meth_sigs
, lde_infix = infix_decls })) = do
let tvbNames = map extractTvbName tvbs
pClsName = promoteClassName cls_name
kproxies <- mapM (const $ qNewName "kproxy") tvbs
pCxt <- mapM promote_superclass_pred cxt
let proxyCxt = map (\kp -> foldl DAppPr (DConPr equalityName)
[DVarT kp, DConT kProxyDataName]) kproxies
cxt' = pCxt ++ proxyCxt
ptvbs = zipWith (\proxy tvbName -> DKindedTV proxy
(DConK kProxyTypeName [DVarK tvbName]))
kproxies tvbNames
sig_decs <- mapM (uncurry promote_sig) (Map.toList meth_sigs)
-- the first arg to promoteMethod is a kind subst. We actually don't
-- want to subst for default instances, so we pass Map.empty
default_decs <- concatMapM (promoteMethod Map.empty meth_sigs)
(Map.toList defaults)
let infix_decls' = catMaybes $ map (uncurry promoteInfixDecl) infix_decls
emitDecs [ DClassD cxt' pClsName ptvbs [] (sig_decs ++
default_decs ++
infix_decls') ]
return ( Map.singleton cls_name tvbNames
, meth_sigs )
where
promote_sig :: Name -> DType -> PrM DDec
promote_sig name ty = do
let proName = promoteValNameLhs name
(argKs, resK) <- snocView `liftM` (mapM promoteType (snd $ unravel ty))
args <- mapM (const $ qNewName "arg") argKs
emitDecsM $ defunctionalize proName (map Just argKs) (Just resK)
return $ DFamilyD TypeFam proName
(zipWith DKindedTV args argKs)
(Just resK)
promote_superclass_pred :: DPred -> PrM DPred
promote_superclass_pred = go
where
go (DAppPr pr ty) = DAppPr <$> go pr <*> fmap kindParam (promoteType ty)
go (DSigPr pr _k) = go pr -- just ignore the kind; it can't matter
go (DVarPr name) = fail $ "Cannot promote ConstraintKinds variables like "
++ show name
go (DConPr name) = return $ DConPr (promoteClassName name)
promoteInstanceDec :: Map Name [Name] -> Map Name DType -> InstDecl -> PrM ()
promoteInstanceDec cls_tvb_env meth_sigs
(InstDecl cls_name inst_tys meths) = do
cls_tvb_names <- lookup_cls_tvb_names
inst_kis <- mapM promoteType inst_tys
let subst = Map.fromList $ zip cls_tvb_names inst_kis
meths' <- concatMapM (promoteMethod subst meth_sigs) meths
emitDecs [DInstanceD [] (foldType (DConT pClsName)
(map kindParam inst_kis)) meths']
where
pClsName = promoteClassName cls_name
lookup_cls_tvb_names :: PrM [String]
lookup_cls_tvb_names = case Map.lookup cls_name cls_tvb_env of
Nothing -> do
m_dinfo <- qReifyMaybe pClsName
case m_dinfo of
Just (DTyConI (DClassD _cxt _name cls_tvbs _fds _decs) _insts) -> do
mapM extract_kv_name cls_tvbs
_ -> fail $ "Cannot find class declaration for " ++ show cls_name
-- See Note [Bad Names in reification]
Just tvb_names -> return $ map nameBase tvb_names
extract_kv_name :: DTyVarBndr -> PrM String
extract_kv_name (DKindedTV _kpVar (DConK _kpType [DVarK kv])) =
-- See Note [Bad Names in reification]
return $ nameBase kv
extract_kv_name tvb =
fail $ "Unexpected parameter to promoted class: " ++ show tvb
-- Note [Bad Names in reification]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- For reasons I (RAE) don't understand, reifying a class and reifying an
-- associated type family sometimes produce *different* Names for the
-- associated type/kind variables. This wreaks havoc with the type subst
-- algorithm in promoteMethod. The solution? Ickily compare nameBases
-- instead of proper Names. See also GHC#9081.
-- See Note [Bad Names in reification]
promoteMethod :: Map String DKind -- instantiations for class tyvars
-> Map Name DType -- method types
-> (Name, ULetDecRHS) -> PrM [DDec]
promoteMethod subst sigs_map (meth_name, meth_rhs) = do
(payload, _defuns, _ann_rhs)
<- promoteLetDecRHS sigs_map noPrefix meth_name meth_rhs
let eqns = payload_to_eqns payload
(arg_kis, res_ki) <- lookup_meth_ty
let meth_arg_kis' = map subst_ki arg_kis
meth_res_ki' = subst_ki res_ki
eqns' = map (apply_kis meth_arg_kis' meth_res_ki') eqns
return $ map (DTySynInstD proName) eqns'
where
proName = promoteValNameLhs meth_name
payload_to_eqns (Left (_name, tvbs, rhs)) =
[DTySynEqn (map tvb_to_ty tvbs) rhs]
payload_to_eqns (Right (_name, _tvbs, _res_ki, eqns)) = eqns
tvb_to_ty (DPlainTV n) = DVarT n
tvb_to_ty (DKindedTV n ki) = DVarT n `DSigT` ki
lookup_meth_ty :: PrM ([DKind], DKind)
lookup_meth_ty = case Map.lookup meth_name sigs_map of
Nothing -> do
-- lookup the promoted name, just in case the term-level one
-- isn't defined
m_dinfo <- qReifyMaybe proName
case m_dinfo of
Just (DTyConI (DFamilyD _flav _name tvbs (Just res)) _insts) -> do
arg_kis <- mapM (expect_just . extractTvbKind) tvbs
return (arg_kis, res)
_ -> fail $ "Cannot find type of " ++ show proName
Just ty -> do
let (_, tys) = unravel ty
kis <- mapM promoteType tys
return $ snocView kis
expect_just :: Maybe a -> PrM a
expect_just (Just x) = return x
expect_just Nothing =
fail "Internal error: unknown kind of a promoted class method."
subst_ki :: DKind -> DKind
subst_ki (DForallK {}) =
error "Higher-rank kind encountered in instance method promotion."
subst_ki (DVarK n) =
-- See Note [Bad Names in reification]
case Map.lookup (nameBase n) subst of
Just ki -> ki
Nothing -> DVarK n
subst_ki (DConK con kis) = DConK con (map subst_ki kis)
subst_ki (DArrowK k1 k2) = DArrowK (subst_ki k1) (subst_ki k2)
subst_ki DStarK = DStarK
apply_kis :: [DKind] -> DKind -> DTySynEqn -> DTySynEqn
apply_kis arg_kis res_ki (DTySynEqn lhs rhs) =
DTySynEqn (zipWith apply_ki lhs arg_kis) (apply_ki rhs res_ki)
apply_ki :: DType -> DKind -> DType
apply_ki = DSigT
promoteLetDecEnv :: String -> ULetDecEnv -> PrM ([DDec], ALetDecEnv)
promoteLetDecEnv prefix (LetDecEnv { lde_defns = value_env
, lde_types = type_env
, lde_infix = infix_decls }) = do
-- deal with the infix_decls, to get them out of the way
let infix_decls' = catMaybes $ map (uncurry promoteInfixDecl) infix_decls
-- promote all the declarations, producing annotated declarations
(names, rhss) = unzip $ Map.toList value_env
(payloads, defun_decss, ann_rhss)
<- fmap unzip3 $ zipWithM (promoteLetDecRHS type_env prefix) names rhss
emitDecs $ concat defun_decss
let decs = map payload_to_dec payloads
-- build the ALetDecEnv
let let_dec_env' = LetDecEnv { lde_defns = Map.fromList $ zip names ann_rhss
, lde_types = type_env
, lde_infix = infix_decls
, lde_proms = Map.empty } -- filled in promoteLetDecs
return (infix_decls' ++ decs, let_dec_env')
where
payload_to_dec (Left (name, tvbs, ty)) = DTySynD name tvbs ty
payload_to_dec (Right (name, tvbs, m_ki, eqns)) =
DClosedTypeFamilyD name tvbs m_ki eqns
promoteInfixDecl :: Fixity -> Name -> Maybe DDec
promoteInfixDecl fixity name
| isUpcase name = Nothing -- no need to promote the decl
| otherwise = Just $ DLetDec $ DInfixD fixity (promoteValNameLhs name)
-- This function is used both to promote class method defaults and normal
-- let bindings. Thus, it can't quite do all the work locally and returns
-- an unwiedly intermediate structure. Perhaps a better design is available.
promoteLetDecRHS :: Map Name DType -- local type env't
-> String -- let-binding prefix
-> Name -- name of the thing being promoted
-> ULetDecRHS -- body of the thing
-> PrM ( Either
(Name, [DTyVarBndr], DType) -- "type synonym"
(Name, [DTyVarBndr], Maybe DKind, [DTySynEqn])
-- "type family"
, [DDec] -- defunctionalization
, ALetDecRHS ) -- annotated RHS
promoteLetDecRHS type_env prefix name (UValue exp) = do
(res_kind, mk_rhs, num_arrows)
<- case Map.lookup name type_env of
Nothing -> return (Nothing, id, 0)
Just ty -> do
ki <- promoteType ty
return (Just ki, (`DSigT` ki), countArgs ty)
case num_arrows of
0 -> do
all_locals <- allLocals
(exp', ann_exp) <- promoteExp exp
let proName = promoteValNameLhsPrefix prefix name
defuns <- defunctionalize proName (map (const Nothing) all_locals) res_kind
return ( Left (proName, map DPlainTV all_locals, mk_rhs exp')
, defuns
, AValue (foldType (DConT proName) (map DVarT all_locals))
num_arrows ann_exp )
_ -> do
names <- replicateM num_arrows (newUniqueName "a")
let pats = map DVarPa names
newArgs = map DVarE names
promoteLetDecRHS type_env prefix name
(UFunction [DClause pats (foldExp exp newArgs)])
promoteLetDecRHS type_env prefix name (UFunction clauses) = do
numArgs <- count_args clauses
(m_argKs, m_resK, ty_num_args) <- case Map.lookup name type_env of
#if __GLASGOW_HASKELL__ < 707
-- we require a type signature here because GHC 7.6.3 doesn't support
-- kind inference for type families
Nothing -> fail ("No type signature for function \"" ++
(nameBase name) ++ "\". Cannot promote in GHC 7.6.3.\n" ++
"Either add a type signature or upgrade GHC.")
#else
Nothing -> return (replicate numArgs Nothing, Nothing, numArgs)
#endif
Just ty -> do
-- promoteType turns arrows into TyFun. So, we unravel first to
-- avoid this behavior. Note the use of ravelTyFun in resultK
-- to make the return kind work out
kis <- mapM promoteType (snd $ unravel ty)
let (argKs, resultK) = snocView kis
-- invariant: countArgs ty == length argKs
return (map Just argKs, Just resultK, length argKs)
let proName = promoteValNameLhsPrefix prefix name
all_locals <- allLocals
defun_decs <- defunctionalize proName
(map (const Nothing) all_locals ++ m_argKs) m_resK
local_tvbs <- mapM inferKindTV all_locals
tyvarNames <- mapM (const $ qNewName "a") m_argKs
expClauses <- mapM (etaExpand (ty_num_args - numArgs)) clauses
(eqns, ann_clauses) <- mapAndUnzipM promoteClause expClauses
prom_fun <- lookupVarE name
args <- zipWithM inferMaybeKindTV tyvarNames m_argKs
let all_args = local_tvbs ++ args
resultK <- inferKind m_resK
return ( Right (proName, all_args, resultK, eqns)
, defun_decs
, AFunction prom_fun ty_num_args ann_clauses )
where
etaExpand :: Int -> DClause -> PrM DClause
etaExpand n (DClause pats exp) = do
names <- replicateM n (newUniqueName "a")
let newPats = map DVarPa names
newArgs = map DVarE names
return $ DClause (pats ++ newPats) (foldExp exp newArgs)
count_args (DClause pats _ : _) = return $ length pats
count_args _ = fail $ "Impossible! A function without clauses."
promoteClause :: DClause -> PrM (DTySynEqn, ADClause)
promoteClause (DClause pats exp) = do
-- promoting the patterns creates variable bindings. These are passed
-- to the function promoted the RHS
(types, new_vars) <- evalForPair $ mapM promotePat pats
(ty, ann_exp) <- lambdaBind new_vars $ promoteExp exp
all_locals <- allLocals -- these are bound *outside* of this clause
return ( DTySynEqn (map DVarT all_locals ++ types) ty
, ADClause new_vars pats ann_exp )
promoteMatch :: DType -> DMatch -> PrM (DTySynEqn, ADMatch)
promoteMatch prom_case (DMatch pat exp) = do
-- promoting the patterns creates variable bindings. These are passed
-- to the function promoted the RHS
(ty, new_vars) <- evalForPair $ promotePat pat
(rhs, ann_exp) <- lambdaBind new_vars $ promoteExp exp
all_locals <- allLocals
return $ ( DTySynEqn (map DVarT all_locals ++ [ty]) rhs
, ADMatch new_vars prom_case pat ann_exp)
-- promotes a term pattern into a type pattern, accumulating bound variable names
promotePat :: DPat -> QWithAux VarPromotions PrM DType
promotePat (DLitPa lit) = promoteLit lit
promotePat (DVarPa name) = do
-- term vars can be symbols... type vars can't!
tyName <- mkTyName name
addElement (name, tyName)
return $ DVarT tyName
promotePat (DConPa name pats) = do
types <- mapM promotePat pats
let name' = unboxed_tuple_to_tuple name
return $ foldType (DConT name') types
where
unboxed_tuple_to_tuple n
| Just deg <- unboxedTupleNameDegree_maybe n = tupleDataName deg
| otherwise = n
promotePat (DTildePa pat) = do
qReportWarning "Lazy pattern converted into regular pattern in promotion"
promotePat pat
promotePat (DBangPa pat) = do
qReportWarning "Strict pattern converted into regular pattern in promotion"
promotePat pat
promotePat DWildPa = do
name <- qNewName "z"
return $ DVarT name
promoteExp :: DExp -> PrM (DType, ADExp)
promoteExp (DVarE name) = fmap (, ADVarE name) $ lookupVarE name
promoteExp (DConE name) = return $ (promoteValRhs name, ADConE name)
promoteExp (DLitE lit) = fmap (, ADLitE lit) $ promoteLit lit
promoteExp (DAppE exp1 exp2) = do
(exp1', ann_exp1) <- promoteExp exp1
(exp2', ann_exp2) <- promoteExp exp2
return (apply exp1' exp2', ADAppE ann_exp1 ann_exp2)
promoteExp (DLamE names exp) = do
lambdaName <- newUniqueName "Lambda"
resultKVarName <- qNewName "r"
tyNames <- mapM mkTyName names
let var_proms = zip names tyNames
(rhs, ann_exp) <- lambdaBind var_proms $ promoteExp exp
tyFamLamTypes <- mapM (const $ qNewName "t") names
all_locals <- allLocals
let all_args = all_locals ++ tyFamLamTypes
tvbs <- mapM inferKindTV all_args
let resultK = DVarK resultKVarName
m_resultK = unknownResult resultK
emitDecs [DClosedTypeFamilyD lambdaName
tvbs
m_resultK
[DTySynEqn (map DVarT (all_locals ++ tyNames))
rhs]]
emitDecsM $ defunctionalize lambdaName (map (const Nothing) all_args) Nothing
let promLambda = foldl apply (DConT (promoteTySym lambdaName 0))
(map DVarT all_locals)
return (promLambda, ADLamE var_proms promLambda names ann_exp)
promoteExp (DCaseE exp matches) = do
caseTFName <- newUniqueName "Case"
all_locals <- allLocals
let prom_case = foldType (DConT caseTFName) (map DVarT all_locals)
(exp', ann_exp) <- promoteExp exp
(eqns, ann_matches) <- mapAndUnzipM (promoteMatch prom_case) matches
tyvarName <- qNewName "t"
let all_args = all_locals ++ [tyvarName]
tvbs <- mapM inferKindTV all_args
resultK <- fmap DVarK $ qNewName "r"
emitDecs [DClosedTypeFamilyD caseTFName tvbs (unknownResult resultK) eqns]
return ( prom_case `DAppT` exp'
, ADCaseE ann_exp ann_matches )
promoteExp (DLetE decs exp) = do
letPrefix <- fmap nameBase $ newUniqueName "Let"
(binds, ann_env) <- promoteLetDecs letPrefix decs
(exp', ann_exp) <- letBind binds $ promoteExp exp
return (exp', ADLetE ann_env ann_exp)
promoteExp (DSigE exp ty) = do
(exp', ann_exp) <- promoteExp exp
ty' <- promoteType ty
return (DSigT exp' ty', ADSigE ann_exp ty)
promoteLit :: Monad m => Lit -> m DType
promoteLit (IntegerL n)
| n >= 0 = return $ DLitT (NumTyLit n)
| otherwise = fail ("Promoting negative integers not supported: " ++ (show n))
promoteLit (StringL str) = return $ DLitT (StrTyLit str)
promoteLit lit =
fail ("Only string and natural number literals can be promoted: " ++ show lit)