{- Data/Singletons/Single/Monad.hs

(c) Richard Eisenberg 2014
rae@cs.brynmawr.edu

This file defines the SgM monad and its operations, for use during singling.

The SgM monad allows reading from a SgEnv environment and is wrapped around a Q.
-}

{-# 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.Names
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

-- environment during singling
data SgEnv =
  SgEnv { SgEnv -> Map Name DExp
sg_let_binds   :: Map Name DExp   -- from the *original* name
        , SgEnv -> DCxt
sg_context     :: DCxt -- See Note [Tracking the current type signature context]
        , SgEnv -> [Dec]
sg_local_decls :: [Dec]
        }

emptySgEnv :: SgEnv
emptySgEnv :: SgEnv
emptySgEnv = SgEnv :: Map Name DExp -> DCxt -> [Dec] -> SgEnv
SgEnv { 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 = []
                   }

-- the singling monad
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 )

liftSgM :: Q a -> SgM a
liftSgM :: Q a -> SgM a
liftSgM = ReaderT SgEnv (WriterT [DDec] Q) a -> SgM a
forall a. ReaderT SgEnv (WriterT [DDec] Q) a -> SgM a
SgM (ReaderT SgEnv (WriterT [DDec] Q) a -> SgM a)
-> (Q a -> ReaderT SgEnv (WriterT [DDec] Q) a) -> Q a -> SgM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT [DDec] Q a -> ReaderT SgEnv (WriterT [DDec] Q) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (WriterT [DDec] Q a -> ReaderT SgEnv (WriterT [DDec] Q) a)
-> (Q a -> WriterT [DDec] Q a)
-> Q a
-> ReaderT SgEnv (WriterT [DDec] Q) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q a -> WriterT [DDec] Q a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

instance Quasi SgM where
  qNewName :: String -> SgM Name
qNewName          = Q Name -> SgM Name
forall a. Q a -> SgM a
liftSgM (Q Name -> SgM Name) -> (String -> Q Name) -> String -> SgM Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
`comp1` String -> Q Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName
  qReport :: Bool -> String -> SgM ()
qReport           = Q () -> SgM ()
forall a. Q a -> SgM a
liftSgM (Q () -> SgM ())
-> (Bool -> String -> Q ()) -> Bool -> String -> SgM ()
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
`comp2` Bool -> String -> Q ()
forall (m :: * -> *). Quasi m => Bool -> String -> m ()
qReport
  qLookupName :: Bool -> String -> SgM (Maybe Name)
qLookupName       = Q (Maybe Name) -> SgM (Maybe Name)
forall a. Q a -> SgM a
liftSgM (Q (Maybe Name) -> SgM (Maybe Name))
-> (Bool -> String -> Q (Maybe Name))
-> Bool
-> String
-> SgM (Maybe Name)
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
`comp2` Bool -> String -> Q (Maybe Name)
forall (m :: * -> *). Quasi m => Bool -> String -> m (Maybe Name)
qLookupName
  qReify :: Name -> SgM Info
qReify            = Q Info -> SgM Info
forall a. Q a -> SgM a
liftSgM (Q Info -> SgM Info) -> (Name -> Q Info) -> Name -> SgM Info
forall b c a. (b -> c) -> (a -> b) -> a -> c
`comp1` Name -> Q Info
forall (m :: * -> *). Quasi m => Name -> m Info
qReify
  qReifyInstances :: Name -> [Type] -> SgM [Dec]
qReifyInstances   = Q [Dec] -> SgM [Dec]
forall a. Q a -> SgM a
liftSgM (Q [Dec] -> SgM [Dec])
-> (Name -> [Type] -> Q [Dec]) -> Name -> [Type] -> SgM [Dec]
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
`comp2` Name -> [Type] -> Q [Dec]
forall (m :: * -> *). Quasi m => Name -> [Type] -> m [Dec]
qReifyInstances
  qLocation :: SgM Loc
qLocation         = Q Loc -> SgM Loc
forall a. Q a -> SgM a
liftSgM Q Loc
forall (m :: * -> *). Quasi m => m Loc
qLocation
  qRunIO :: IO a -> SgM a
qRunIO            = Q a -> SgM a
forall a. Q a -> SgM a
liftSgM (Q a -> SgM a) -> (IO a -> Q a) -> IO a -> SgM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
`comp1` IO a -> Q a
forall (m :: * -> *) a. Quasi m => IO a -> m a
qRunIO
  qAddDependentFile :: String -> SgM ()
qAddDependentFile = Q () -> SgM ()
forall a. Q a -> SgM a
liftSgM (Q () -> SgM ()) -> (String -> Q ()) -> String -> SgM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
`comp1` String -> Q ()
forall (m :: * -> *). Quasi m => String -> m ()
qAddDependentFile
  qReifyRoles :: Name -> SgM [Role]
qReifyRoles       = Q [Role] -> SgM [Role]
forall a. Q a -> SgM a
liftSgM (Q [Role] -> SgM [Role])
-> (Name -> Q [Role]) -> Name -> SgM [Role]
forall b c a. (b -> c) -> (a -> b) -> a -> c
`comp1` Name -> Q [Role]
forall (m :: * -> *). Quasi m => Name -> m [Role]
qReifyRoles
  qReifyAnnotations :: AnnLookup -> SgM [a]
qReifyAnnotations = Q [a] -> SgM [a]
forall a. Q a -> SgM a
liftSgM (Q [a] -> SgM [a]) -> (AnnLookup -> Q [a]) -> AnnLookup -> SgM [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
`comp1` AnnLookup -> Q [a]
forall (m :: * -> *) a. (Quasi m, Data a) => AnnLookup -> m [a]
qReifyAnnotations
  qReifyModule :: Module -> SgM ModuleInfo
qReifyModule      = Q ModuleInfo -> SgM ModuleInfo
forall a. Q a -> SgM a
liftSgM (Q ModuleInfo -> SgM ModuleInfo)
-> (Module -> Q ModuleInfo) -> Module -> SgM ModuleInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
`comp1` Module -> Q ModuleInfo
forall (m :: * -> *). Quasi m => Module -> m ModuleInfo
qReifyModule
  qAddTopDecls :: [Dec] -> SgM ()
qAddTopDecls      = Q () -> SgM ()
forall a. Q a -> SgM a
liftSgM (Q () -> SgM ()) -> ([Dec] -> Q ()) -> [Dec] -> SgM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
`comp1` [Dec] -> Q ()
forall (m :: * -> *). Quasi m => [Dec] -> m ()
qAddTopDecls
  qAddModFinalizer :: Q () -> SgM ()
qAddModFinalizer  = Q () -> SgM ()
forall a. Q a -> SgM a
liftSgM (Q () -> SgM ()) -> (Q () -> Q ()) -> Q () -> SgM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
`comp1` Q () -> Q ()
forall (m :: * -> *). Quasi m => Q () -> m ()
qAddModFinalizer
  qGetQ :: SgM (Maybe a)
qGetQ             = Q (Maybe a) -> SgM (Maybe a)
forall a. Q a -> SgM a
liftSgM Q (Maybe a)
forall (m :: * -> *) a. (Quasi m, Typeable a) => m (Maybe a)
qGetQ
  qPutQ :: a -> SgM ()
qPutQ             = Q () -> SgM ()
forall a. Q a -> SgM a
liftSgM (Q () -> SgM ()) -> (a -> Q ()) -> a -> SgM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
`comp1` a -> Q ()
forall (m :: * -> *) a. (Quasi m, Typeable a) => a -> m ()
qPutQ

  qReifyFixity :: Name -> SgM (Maybe Fixity)
qReifyFixity        = Q (Maybe Fixity) -> SgM (Maybe Fixity)
forall a. Q a -> SgM a
liftSgM (Q (Maybe Fixity) -> SgM (Maybe Fixity))
-> (Name -> Q (Maybe Fixity)) -> Name -> SgM (Maybe Fixity)
forall b c a. (b -> c) -> (a -> b) -> a -> c
`comp1` Name -> Q (Maybe Fixity)
forall (m :: * -> *). Quasi m => Name -> m (Maybe Fixity)
qReifyFixity
  qReifyConStrictness :: Name -> SgM [DecidedStrictness]
qReifyConStrictness = Q [DecidedStrictness] -> SgM [DecidedStrictness]
forall a. Q a -> SgM a
liftSgM (Q [DecidedStrictness] -> SgM [DecidedStrictness])
-> (Name -> Q [DecidedStrictness])
-> Name
-> SgM [DecidedStrictness]
forall b c a. (b -> c) -> (a -> b) -> a -> c
`comp1` Name -> Q [DecidedStrictness]
forall (m :: * -> *). Quasi m => Name -> m [DecidedStrictness]
qReifyConStrictness
  qIsExtEnabled :: Extension -> SgM Bool
qIsExtEnabled       = Q Bool -> SgM Bool
forall a. Q a -> SgM a
liftSgM (Q Bool -> SgM Bool)
-> (Extension -> Q Bool) -> Extension -> SgM Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
`comp1` Extension -> Q Bool
forall (m :: * -> *). Quasi m => Extension -> m Bool
qIsExtEnabled
  qExtsEnabled :: SgM [Extension]
qExtsEnabled        = Q [Extension] -> SgM [Extension]
forall a. Q a -> SgM a
liftSgM Q [Extension]
forall (m :: * -> *). Quasi m => m [Extension]
qExtsEnabled
  qAddForeignFilePath :: ForeignSrcLang -> String -> SgM ()
qAddForeignFilePath = Q () -> SgM ()
forall a. Q a -> SgM a
liftSgM (Q () -> SgM ())
-> (ForeignSrcLang -> String -> Q ())
-> ForeignSrcLang
-> String
-> SgM ()
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
`comp2` ForeignSrcLang -> String -> Q ()
forall (m :: * -> *). Quasi m => ForeignSrcLang -> String -> m ()
qAddForeignFilePath
  qAddTempFile :: String -> SgM String
qAddTempFile        = Q String -> SgM String
forall a. Q a -> SgM a
liftSgM (Q String -> SgM String)
-> (String -> Q String) -> String -> SgM String
forall b c a. (b -> c) -> (a -> b) -> a -> c
`comp1` String -> Q String
forall (m :: * -> *). Quasi m => String -> m String
qAddTempFile
  qAddCorePlugin :: String -> SgM ()
qAddCorePlugin      = Q () -> SgM ()
forall a. Q a -> SgM a
liftSgM (Q () -> SgM ()) -> (String -> Q ()) -> String -> SgM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
`comp1` String -> Q ()
forall (m :: * -> *). Quasi m => String -> m ()
qAddCorePlugin

  qRecover :: SgM a -> SgM a -> SgM a
qRecover (SgM handler :: ReaderT SgEnv (WriterT [DDec] Q) a
handler) (SgM body :: ReaderT SgEnv (WriterT [DDec] Q) a
body) = do
    SgEnv
env <- SgM SgEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
    (result :: a
result, aux :: [DDec]
aux) <- Q (a, [DDec]) -> SgM (a, [DDec])
forall a. Q a -> SgM a
liftSgM (Q (a, [DDec]) -> SgM (a, [DDec]))
-> Q (a, [DDec]) -> SgM (a, [DDec])
forall a b. (a -> b) -> a -> b
$
                     Q (a, [DDec]) -> Q (a, [DDec]) -> Q (a, [DDec])
forall (m :: * -> *) a. Quasi m => m a -> m a -> m a
qRecover (WriterT [DDec] Q a -> Q (a, [DDec])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT [DDec] Q a -> Q (a, [DDec]))
-> WriterT [DDec] Q a -> Q (a, [DDec])
forall a b. (a -> b) -> a -> b
$ 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
handler SgEnv
env)
                              (WriterT [DDec] Q a -> Q (a, [DDec])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT [DDec] Q a -> Q (a, [DDec]))
-> WriterT [DDec] Q a -> Q (a, [DDec])
forall a b. (a -> b) -> a -> b
$ 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
body SgEnv
env)
    [DDec] -> SgM ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [DDec]
aux
    a -> SgM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
result

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

bindLets :: [(Name, DExp)] -> SgM a -> SgM a
bindLets :: [(Name, DExp)] -> SgM a -> SgM a
bindLets lets1 :: [(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 })

-- Add some constraints to the current type signature context.
-- See Note [Tracking the current type signature context]
bindContext :: DCxt -> SgM a -> SgM a
bindContext :: DCxt -> SgM a -> SgM a
bindContext ctxt1 :: 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 })

-- Retrieve the current type signature context.
-- See Note [Tracking the current type signature context]
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) -> (Name -> DExp) -> Name -> SgM DExp
lookup_var_con Name -> Name
singValName (Name -> DExp
DVarE (Name -> DExp) -> (Name -> Name) -> Name -> DExp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
singValName)

lookupConE :: Name -> SgM DExp
lookupConE :: Name -> SgM DExp
lookupConE = (Name -> Name) -> (Name -> DExp) -> Name -> SgM DExp
lookup_var_con Name -> Name
singDataConName (Name -> DExp
DConE (Name -> DExp) -> (Name -> Name) -> Name -> DExp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
singDataConName)

lookup_var_con :: (Name -> Name) -> (Name -> DExp) -> Name -> SgM DExp
lookup_var_con :: (Name -> Name) -> (Name -> DExp) -> Name -> SgM DExp
lookup_var_con mk_sing_name :: Name -> Name
mk_sing_name mk_exp :: Name -> DExp
mk_exp name :: Name
name = do
  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 (m :: * -> *). Quasi m => String -> m Name
mkDataName (Name -> String
nameBase (Name -> Name
mk_sing_name Name
name)) -- we want *term* names!
  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
    Nothing -> do
      -- try to get it from the global context
      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)
        -- try the unrefined name too -- it's needed to bootstrap Enum
      case Maybe DInfo
m_dinfo of
        Just (DVarI _ ty :: DType
ty _) ->
          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
promoteValRhs Name
name) (Name -> DExp
mk_exp Name
name)
        _ -> 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   -- lambda-bound
    Just exp :: 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 0 _  = DExp -> DExp
forall a. a -> a
id
wrapSingFun n :: Int
n ty :: 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
                           1 -> 'singFun1
                           2 -> 'singFun2
                           3 -> 'singFun3
                           4 -> 'singFun4
                           5 -> 'singFun5
                           6 -> 'singFun6
                           7 -> 'singFun7
                           _ -> String -> Name
forall a. HasCallStack => String -> a
error "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 0 _  = DExp -> DExp
forall a. a -> a
id
wrapUnSingFun n :: Int
n ty :: 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
                             1 -> 'unSingFun1
                             2 -> 'unSingFun2
                             3 -> 'unSingFun3
                             4 -> 'unSingFun4
                             5 -> 'unSingFun5
                             6 -> 'unSingFun6
                             7 -> 'unSingFun7
                             _ -> String -> Name
forall a. HasCallStack => String -> a
error "No support for functions of arity > 7."
  in
  (DExp
unwrap_fun DExp -> DType -> DExp
`DAppTypeE` DType
ty DExp -> DExp -> DExp
`DAppE`)

singM :: DsMonad q => [Dec] -> SgM a -> q (a, [DDec])
singM :: [Dec] -> SgM a -> q (a, [DDec])
singM locals :: [Dec]
locals (SgM rdr :: ReaderT SgEnv (WriterT [DDec] Q) a
rdr) = do
  [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_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 :: DsMonad q => [Dec] -> SgM [DDec] -> q [DDec]
singDecsM :: [Dec] -> SgM [DDec] -> q [DDec]
singDecsM locals :: [Dec]
locals thing :: SgM [DDec]
thing = do
  (decs1 :: [DDec]
decs1, decs2 :: [DDec]
decs2) <- [Dec] -> SgM [DDec] -> q ([DDec], [DDec])
forall (q :: * -> *) a.
DsMonad 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

{-
Note [Tracking the current type signature context]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Much like we track the let-bound names in scope, we also track the current
context. For instance, in the following program:

  -- (1)
  f :: forall a. Show a => a -> String -> Bool
  f x y = g (show x) y
    where
      -- (2)
      g :: forall b. Eq b => b -> b -> Bool
      g = h
        where
          -- (3)
          h :: b -> b -> Bool
          h = (==)

Here is the context at various points:

(1) ()
(2) (Show a)
(3) (Show a, Eq b)

We track this informating during singling instead of during promotion, as the
promoted versions of things are often type families, which do not have
contexts.

Why do we bother tracking this at all? Ultimately, because singDefuns (from
Data.Singletons.Single.Defun) needs to know the current context in order to
generate a correctly typed SingI instance. For instance, if you called
singDefuns on the class method bar:

  class Foo a where
    bar :: Eq a => a -> Bool

Then if you only grabbed the context of `bar` itself, then you'd end up
generating the following SingI instance for BarSym0:

  instance SEq a => SingI (FooSym0 :: a ~> Bool) where ...

Which is incorrect—there needs to be an (SFoo a) constraint as well! If we
track the current context when singling Foo, then we will correctly propagate
this information to singDefuns.
-}