{-# LANGUAGE GeneralizedNewtypeDeriving, ParallelListComp, TemplateHaskell #-}
module Data.Singletons.Single.Monad (
SgM, bindLets, bindContext, askContext, lookupVarE, lookupConE,
wrapSingFun, wrapUnSingFun,
singM, singDecsM,
emitDecs, emitDecsM
) where
import Prelude hiding ( exp )
import Data.Map ( Map )
import qualified Data.Map as Map
import Data.Singletons.Promote.Monad ( emitDecs, emitDecsM )
import Data.Singletons.TH.Options
import Data.Singletons.Util
import Data.Singletons.Internal
import Language.Haskell.TH.Syntax hiding ( lift )
import Language.Haskell.TH.Desugar
import Control.Monad.Reader
import Control.Monad.Writer
import Control.Applicative
data SgEnv =
SgEnv { SgEnv -> Options
sg_options :: Options
, SgEnv -> Map Name DExp
sg_let_binds :: Map Name DExp
, SgEnv -> DCxt
sg_context :: DCxt
, SgEnv -> [Dec]
sg_local_decls :: [Dec]
}
emptySgEnv :: SgEnv
emptySgEnv :: SgEnv
emptySgEnv = SgEnv :: Options -> Map Name DExp -> DCxt -> [Dec] -> SgEnv
SgEnv { sg_options :: Options
sg_options = Options
defaultOptions
, sg_let_binds :: Map Name DExp
sg_let_binds = Map Name DExp
forall k a. Map k a
Map.empty
, sg_context :: DCxt
sg_context = []
, sg_local_decls :: [Dec]
sg_local_decls = []
}
newtype SgM a = SgM (ReaderT SgEnv (WriterT [DDec] Q) a)
deriving ( a -> SgM b -> SgM a
(a -> b) -> SgM a -> SgM b
(forall a b. (a -> b) -> SgM a -> SgM b)
-> (forall a b. a -> SgM b -> SgM a) -> Functor SgM
forall a b. a -> SgM b -> SgM a
forall a b. (a -> b) -> SgM a -> SgM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> SgM b -> SgM a
$c<$ :: forall a b. a -> SgM b -> SgM a
fmap :: (a -> b) -> SgM a -> SgM b
$cfmap :: forall a b. (a -> b) -> SgM a -> SgM b
Functor, Functor SgM
a -> SgM a
Functor SgM
-> (forall a. a -> SgM a)
-> (forall a b. SgM (a -> b) -> SgM a -> SgM b)
-> (forall a b c. (a -> b -> c) -> SgM a -> SgM b -> SgM c)
-> (forall a b. SgM a -> SgM b -> SgM b)
-> (forall a b. SgM a -> SgM b -> SgM a)
-> Applicative SgM
SgM a -> SgM b -> SgM b
SgM a -> SgM b -> SgM a
SgM (a -> b) -> SgM a -> SgM b
(a -> b -> c) -> SgM a -> SgM b -> SgM c
forall a. a -> SgM a
forall a b. SgM a -> SgM b -> SgM a
forall a b. SgM a -> SgM b -> SgM b
forall a b. SgM (a -> b) -> SgM a -> SgM b
forall a b c. (a -> b -> c) -> SgM a -> SgM b -> SgM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: SgM a -> SgM b -> SgM a
$c<* :: forall a b. SgM a -> SgM b -> SgM a
*> :: SgM a -> SgM b -> SgM b
$c*> :: forall a b. SgM a -> SgM b -> SgM b
liftA2 :: (a -> b -> c) -> SgM a -> SgM b -> SgM c
$cliftA2 :: forall a b c. (a -> b -> c) -> SgM a -> SgM b -> SgM c
<*> :: SgM (a -> b) -> SgM a -> SgM b
$c<*> :: forall a b. SgM (a -> b) -> SgM a -> SgM b
pure :: a -> SgM a
$cpure :: forall a. a -> SgM a
$cp1Applicative :: Functor SgM
Applicative, Applicative SgM
a -> SgM a
Applicative SgM
-> (forall a b. SgM a -> (a -> SgM b) -> SgM b)
-> (forall a b. SgM a -> SgM b -> SgM b)
-> (forall a. a -> SgM a)
-> Monad SgM
SgM a -> (a -> SgM b) -> SgM b
SgM a -> SgM b -> SgM b
forall a. a -> SgM a
forall a b. SgM a -> SgM b -> SgM b
forall a b. SgM a -> (a -> SgM b) -> SgM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> SgM a
$creturn :: forall a. a -> SgM a
>> :: SgM a -> SgM b -> SgM b
$c>> :: forall a b. SgM a -> SgM b -> SgM b
>>= :: SgM a -> (a -> SgM b) -> SgM b
$c>>= :: forall a b. SgM a -> (a -> SgM b) -> SgM b
$cp1Monad :: Applicative SgM
Monad
, MonadReader SgEnv, MonadWriter [DDec]
, Monad SgM
Monad SgM -> (forall a. String -> SgM a) -> MonadFail SgM
String -> SgM a
forall a. String -> SgM a
forall (m :: * -> *).
Monad m -> (forall a. String -> m a) -> MonadFail m
fail :: String -> SgM a
$cfail :: forall a. String -> SgM a
$cp1MonadFail :: Monad SgM
MonadFail, Monad SgM
Monad SgM -> (forall a. IO a -> SgM a) -> MonadIO SgM
IO a -> SgM a
forall a. IO a -> SgM a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: IO a -> SgM a
$cliftIO :: forall a. IO a -> SgM a
$cp1MonadIO :: Monad SgM
MonadIO, MonadFail SgM
MonadIO SgM
SgM [Extension]
SgM (Maybe a)
SgM Loc
a -> SgM ()
Bool -> String -> SgM (Maybe Name)
Bool -> String -> SgM ()
String -> SgM String
String -> SgM Name
String -> SgM ()
[Dec] -> SgM ()
IO a -> SgM a
Q () -> SgM ()
Name -> SgM [DecidedStrictness]
Name -> SgM [Role]
Name -> SgM (Maybe Fixity)
Name -> SgM Type
Name -> SgM Info
Name -> [Type] -> SgM [Dec]
MonadIO SgM
-> MonadFail SgM
-> (String -> SgM Name)
-> (Bool -> String -> SgM ())
-> (forall a. SgM a -> SgM a -> SgM a)
-> (Bool -> String -> SgM (Maybe Name))
-> (Name -> SgM Info)
-> (Name -> SgM (Maybe Fixity))
-> (Name -> SgM Type)
-> (Name -> [Type] -> SgM [Dec])
-> (Name -> SgM [Role])
-> (forall a. Data a => AnnLookup -> SgM [a])
-> (Module -> SgM ModuleInfo)
-> (Name -> SgM [DecidedStrictness])
-> SgM Loc
-> (forall a. IO a -> SgM a)
-> (String -> SgM ())
-> (String -> SgM String)
-> ([Dec] -> SgM ())
-> (ForeignSrcLang -> String -> SgM ())
-> (Q () -> SgM ())
-> (String -> SgM ())
-> (forall a. Typeable a => SgM (Maybe a))
-> (forall a. Typeable a => a -> SgM ())
-> (Extension -> SgM Bool)
-> SgM [Extension]
-> Quasi SgM
Extension -> SgM Bool
ForeignSrcLang -> String -> SgM ()
Module -> SgM ModuleInfo
AnnLookup -> SgM [a]
SgM a -> SgM a -> SgM a
forall a. Data a => AnnLookup -> SgM [a]
forall a. Typeable a => SgM (Maybe a)
forall a. Typeable a => a -> SgM ()
forall a. IO a -> SgM a
forall a. SgM a -> SgM a -> SgM a
forall (m :: * -> *).
MonadIO m
-> MonadFail m
-> (String -> m Name)
-> (Bool -> String -> m ())
-> (forall a. m a -> m a -> m a)
-> (Bool -> String -> m (Maybe Name))
-> (Name -> m Info)
-> (Name -> m (Maybe Fixity))
-> (Name -> m Type)
-> (Name -> [Type] -> m [Dec])
-> (Name -> m [Role])
-> (forall a. Data a => AnnLookup -> m [a])
-> (Module -> m ModuleInfo)
-> (Name -> m [DecidedStrictness])
-> m Loc
-> (forall a. IO a -> m a)
-> (String -> m ())
-> (String -> m String)
-> ([Dec] -> m ())
-> (ForeignSrcLang -> String -> m ())
-> (Q () -> m ())
-> (String -> m ())
-> (forall a. Typeable a => m (Maybe a))
-> (forall a. Typeable a => a -> m ())
-> (Extension -> m Bool)
-> m [Extension]
-> Quasi m
qExtsEnabled :: SgM [Extension]
$cqExtsEnabled :: SgM [Extension]
qIsExtEnabled :: Extension -> SgM Bool
$cqIsExtEnabled :: Extension -> SgM Bool
qPutQ :: a -> SgM ()
$cqPutQ :: forall a. Typeable a => a -> SgM ()
qGetQ :: SgM (Maybe a)
$cqGetQ :: forall a. Typeable a => SgM (Maybe a)
qAddCorePlugin :: String -> SgM ()
$cqAddCorePlugin :: String -> SgM ()
qAddModFinalizer :: Q () -> SgM ()
$cqAddModFinalizer :: Q () -> SgM ()
qAddForeignFilePath :: ForeignSrcLang -> String -> SgM ()
$cqAddForeignFilePath :: ForeignSrcLang -> String -> SgM ()
qAddTopDecls :: [Dec] -> SgM ()
$cqAddTopDecls :: [Dec] -> SgM ()
qAddTempFile :: String -> SgM String
$cqAddTempFile :: String -> SgM String
qAddDependentFile :: String -> SgM ()
$cqAddDependentFile :: String -> SgM ()
qRunIO :: IO a -> SgM a
$cqRunIO :: forall a. IO a -> SgM a
qLocation :: SgM Loc
$cqLocation :: SgM Loc
qReifyConStrictness :: Name -> SgM [DecidedStrictness]
$cqReifyConStrictness :: Name -> SgM [DecidedStrictness]
qReifyModule :: Module -> SgM ModuleInfo
$cqReifyModule :: Module -> SgM ModuleInfo
qReifyAnnotations :: AnnLookup -> SgM [a]
$cqReifyAnnotations :: forall a. Data a => AnnLookup -> SgM [a]
qReifyRoles :: Name -> SgM [Role]
$cqReifyRoles :: Name -> SgM [Role]
qReifyInstances :: Name -> [Type] -> SgM [Dec]
$cqReifyInstances :: Name -> [Type] -> SgM [Dec]
qReifyType :: Name -> SgM Type
$cqReifyType :: Name -> SgM Type
qReifyFixity :: Name -> SgM (Maybe Fixity)
$cqReifyFixity :: Name -> SgM (Maybe Fixity)
qReify :: Name -> SgM Info
$cqReify :: Name -> SgM Info
qLookupName :: Bool -> String -> SgM (Maybe Name)
$cqLookupName :: Bool -> String -> SgM (Maybe Name)
qRecover :: SgM a -> SgM a -> SgM a
$cqRecover :: forall a. SgM a -> SgM a -> SgM a
qReport :: Bool -> String -> SgM ()
$cqReport :: Bool -> String -> SgM ()
qNewName :: String -> SgM Name
$cqNewName :: String -> SgM Name
$cp2Quasi :: MonadFail SgM
$cp1Quasi :: MonadIO SgM
Quasi )
instance DsMonad SgM where
localDeclarations :: SgM [Dec]
localDeclarations = (SgEnv -> [Dec]) -> SgM [Dec]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SgEnv -> [Dec]
sg_local_decls
instance OptionsMonad SgM where
getOptions :: SgM Options
getOptions = (SgEnv -> Options) -> SgM Options
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SgEnv -> Options
sg_options
bindLets :: [(Name, DExp)] -> SgM a -> SgM a
bindLets :: [(Name, DExp)] -> SgM a -> SgM a
bindLets [(Name, DExp)]
lets1 =
(SgEnv -> SgEnv) -> SgM a -> SgM a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\env :: SgEnv
env@(SgEnv { sg_let_binds :: SgEnv -> Map Name DExp
sg_let_binds = Map Name DExp
lets2 }) ->
SgEnv
env { sg_let_binds :: Map Name DExp
sg_let_binds = ([(Name, DExp)] -> Map Name DExp
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Name, DExp)]
lets1) Map Name DExp -> Map Name DExp -> Map Name DExp
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map Name DExp
lets2 })
bindContext :: DCxt -> SgM a -> SgM a
bindContext :: DCxt -> SgM a -> SgM a
bindContext DCxt
ctxt1
= (SgEnv -> SgEnv) -> SgM a -> SgM a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\env :: SgEnv
env@(SgEnv { sg_context :: SgEnv -> DCxt
sg_context = DCxt
ctxt2 }) ->
SgEnv
env { sg_context :: DCxt
sg_context = DCxt
ctxt1 DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ DCxt
ctxt2 })
askContext :: SgM DCxt
askContext :: SgM DCxt
askContext = (SgEnv -> DCxt) -> SgM DCxt
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SgEnv -> DCxt
sg_context
lookupVarE :: Name -> SgM DExp
lookupVarE :: Name -> SgM DExp
lookupVarE Name
name = do
Options
opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
(Name -> Name) -> (Name -> DExp) -> Name -> SgM DExp
lookup_var_con (Options -> Name -> Name
singledValueName Options
opts)
(Name -> DExp
DVarE (Name -> DExp) -> (Name -> Name) -> Name -> DExp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Options -> Name -> Name
singledValueName Options
opts) Name
name
lookupConE :: Name -> SgM DExp
lookupConE :: Name -> SgM DExp
lookupConE Name
name = do
Options
opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
(Name -> Name) -> (Name -> DExp) -> Name -> SgM DExp
lookup_var_con (Options -> Name -> Name
singledDataConName Options
opts)
(Name -> DExp
DConE (Name -> DExp) -> (Name -> Name) -> Name -> DExp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Options -> Name -> Name
singledDataConName Options
opts) Name
name
lookup_var_con :: (Name -> Name) -> (Name -> DExp) -> Name -> SgM DExp
lookup_var_con :: (Name -> Name) -> (Name -> DExp) -> Name -> SgM DExp
lookup_var_con Name -> Name
mk_sing_name Name -> DExp
mk_exp Name
name = do
Options
opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
Map Name DExp
letExpansions <- (SgEnv -> Map Name DExp) -> SgM (Map Name DExp)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SgEnv -> Map Name DExp
sg_let_binds
Name
sName <- String -> SgM Name
forall (q :: * -> *). Quasi q => String -> q Name
mkDataName (Name -> String
nameBase (Name -> Name
mk_sing_name Name
name))
case Name -> Map Name DExp -> Maybe DExp
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
name Map Name DExp
letExpansions of
Maybe DExp
Nothing -> do
Maybe DInfo
m_dinfo <- (Maybe DInfo -> Maybe DInfo -> Maybe DInfo)
-> SgM (Maybe DInfo) -> SgM (Maybe DInfo) -> SgM (Maybe DInfo)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Maybe DInfo -> Maybe DInfo -> Maybe DInfo
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (Name -> SgM (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
sName) (Name -> SgM (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
name)
case Maybe DInfo
m_dinfo of
Just (DVarI Name
_ DType
ty Maybe Name
_) ->
let num_args :: Int
num_args = DType -> Int
countArgs DType
ty in
DExp -> SgM DExp
forall (m :: * -> *) a. Monad m => a -> m a
return (DExp -> SgM DExp) -> DExp -> SgM DExp
forall a b. (a -> b) -> a -> b
$ Int -> DType -> DExp -> DExp
wrapSingFun Int
num_args (Name -> DType
DConT (Name -> DType) -> Name -> DType
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
defunctionalizedName0 Options
opts Name
name)
(Name -> DExp
mk_exp Name
name)
Maybe DInfo
_ -> DExp -> SgM DExp
forall (m :: * -> *) a. Monad m => a -> m a
return (DExp -> SgM DExp) -> DExp -> SgM DExp
forall a b. (a -> b) -> a -> b
$ Name -> DExp
mk_exp Name
name
Just DExp
exp -> DExp -> SgM DExp
forall (m :: * -> *) a. Monad m => a -> m a
return DExp
exp
wrapSingFun :: Int -> DType -> DExp -> DExp
wrapSingFun :: Int -> DType -> DExp -> DExp
wrapSingFun Int
0 DType
_ = DExp -> DExp
forall a. a -> a
id
wrapSingFun Int
n DType
ty =
let wrap_fun :: DExp
wrap_fun = Name -> DExp
DVarE (Name -> DExp) -> Name -> DExp
forall a b. (a -> b) -> a -> b
$ case Int
n of
Int
1 -> 'singFun1
Int
2 -> 'singFun2
Int
3 -> 'singFun3
Int
4 -> 'singFun4
Int
5 -> 'singFun5
Int
6 -> 'singFun6
Int
7 -> 'singFun7
Int
_ -> String -> Name
forall a. HasCallStack => String -> a
error String
"No support for functions of arity > 7."
in
(DExp
wrap_fun DExp -> DType -> DExp
`DAppTypeE` DType
ty DExp -> DExp -> DExp
`DAppE`)
wrapUnSingFun :: Int -> DType -> DExp -> DExp
wrapUnSingFun :: Int -> DType -> DExp -> DExp
wrapUnSingFun Int
0 DType
_ = DExp -> DExp
forall a. a -> a
id
wrapUnSingFun Int
n DType
ty =
let unwrap_fun :: DExp
unwrap_fun = Name -> DExp
DVarE (Name -> DExp) -> Name -> DExp
forall a b. (a -> b) -> a -> b
$ case Int
n of
Int
1 -> 'unSingFun1
Int
2 -> 'unSingFun2
Int
3 -> 'unSingFun3
Int
4 -> 'unSingFun4
Int
5 -> 'unSingFun5
Int
6 -> 'unSingFun6
Int
7 -> 'unSingFun7
Int
_ -> String -> Name
forall a. HasCallStack => String -> a
error String
"No support for functions of arity > 7."
in
(DExp
unwrap_fun DExp -> DType -> DExp
`DAppTypeE` DType
ty DExp -> DExp -> DExp
`DAppE`)
singM :: OptionsMonad q => [Dec] -> SgM a -> q (a, [DDec])
singM :: [Dec] -> SgM a -> q (a, [DDec])
singM [Dec]
locals (SgM ReaderT SgEnv (WriterT [DDec] Q) a
rdr) = do
Options
opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
[Dec]
other_locals <- q [Dec]
forall (m :: * -> *). DsMonad m => m [Dec]
localDeclarations
let wr :: WriterT [DDec] Q a
wr = ReaderT SgEnv (WriterT [DDec] Q) a -> SgEnv -> WriterT [DDec] Q a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT SgEnv (WriterT [DDec] Q) a
rdr (SgEnv
emptySgEnv { sg_options :: Options
sg_options = Options
opts
, sg_local_decls :: [Dec]
sg_local_decls = [Dec]
other_locals [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec]
locals })
q :: Q (a, [DDec])
q = WriterT [DDec] Q a -> Q (a, [DDec])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT WriterT [DDec] Q a
wr
Q (a, [DDec]) -> q (a, [DDec])
forall (m :: * -> *) a. Quasi m => Q a -> m a
runQ Q (a, [DDec])
q
singDecsM :: OptionsMonad q => [Dec] -> SgM [DDec] -> q [DDec]
singDecsM :: [Dec] -> SgM [DDec] -> q [DDec]
singDecsM [Dec]
locals SgM [DDec]
thing = do
([DDec]
decs1, [DDec]
decs2) <- [Dec] -> SgM [DDec] -> q ([DDec], [DDec])
forall (q :: * -> *) a.
OptionsMonad q =>
[Dec] -> SgM a -> q (a, [DDec])
singM [Dec]
locals SgM [DDec]
thing
[DDec] -> q [DDec]
forall (m :: * -> *) a. Monad m => a -> m a
return ([DDec] -> q [DDec]) -> [DDec] -> q [DDec]
forall a b. (a -> b) -> a -> b
$ [DDec]
decs1 [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
decs2