module Agda.Compiler.UHC.CompileState
( CompileT
, Compile
, runCompileT
, CoreMeta
, addExports
, addMetaCon
, addMetaData
, getExports
, getDeclMetas
, getCoreName
, getCoreName1
, getConstrCTag
, getConstrFun
, moduleNameToCoreName
, moduleNameToCoreNameParts
, freshLocalName
, conArityAndPars
, dataRecCons
)
where
import Control.Monad.State
import Control.Monad.Reader.Class
import Data.List
import qualified Data.Map as Map
import Data.Maybe
import Data.Char
#if __GLASGOW_HASKELL__ <= 708
import Control.Applicative
import Data.Monoid
#endif
import Agda.Compiler.UHC.MagicTypes
import Agda.Syntax.Internal
import Agda.Syntax.Common
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Monad.Builtin hiding (coinductionKit')
import qualified Agda.TypeChecking.Monad as TM
import Agda.Compiler.UHC.Bridge
import Agda.Compiler.UHC.Pragmas.Base
import Agda.Compiler.Common
import Agda.Utils.Lens
#include "undefined.h"
import Agda.Utils.Impossible
import Data.Time.Clock.POSIX
getTime :: IO Integer
getTime = round <$> getPOSIXTime
data CoreMeta = CoreMeta
{ coreMetaData :: Map.Map QName ( [CDataCon] -> CDeclMeta )
, coreMetaCon :: Map.Map QName [CDataCon]
, coreExports :: [CExport]
}
instance Monoid CoreMeta where
mempty = CoreMeta mempty mempty []
mappend (CoreMeta a b c) (CoreMeta r s t) =
CoreMeta (Map.union a r) (Map.unionWith (++) b s) (c ++ t)
data CompileState = CompileState
{ coreMeta :: CoreMeta
, nameSupply :: Integer
}
newtype CompileT m a = CompileT { unCompileT :: StateT CompileState m a }
deriving (Monad, MonadIO, MonadTrans, Applicative, Functor)
type Compile = CompileT TCM
runCompileT :: MonadIO m =>
ModuleName
-> CompileT m a
-> m a
runCompileT amod comp = do
(result, state') <- runStateT (unCompileT comp) initial
return result
where initial = CompileState
{ coreMeta = mempty
, nameSupply = 0
}
appendCoreMeta :: Monad m => CoreMeta -> CompileT m ()
appendCoreMeta cm =
CompileT $ modify (\s -> s { coreMeta = cm `mappend` coreMeta s })
addExports :: Monad m => [HsName] -> CompileT m ()
addExports = addExports' . map mkExport
addExports' :: Monad m => [CExport] -> CompileT m ()
addExports' nms = appendCoreMeta (mempty { coreExports = nms })
addMetaCon :: QName -> CDataCon -> Compile ()
addMetaCon q c = do
dtNm <- conData . theDef <$> lift (getConstInfo q)
appendCoreMeta (mempty { coreMetaCon = Map.singleton dtNm [c] })
addMetaData :: QName -> ([CDataCon] -> CDeclMeta) -> Compile ()
addMetaData q d =
appendCoreMeta (mempty { coreMetaData = Map.singleton q d })
getExports :: Compile [CExport]
getExports = CompileT $ gets (coreExports . coreMeta)
getDeclMetas :: Compile [CDeclMeta]
getDeclMetas = CompileT $ do
cons <- gets (coreMetaCon . coreMeta)
dts <- gets (coreMetaData . coreMeta)
return $ map (\(dtNm, f) -> f (Map.findWithDefault [] dtNm cons)) (Map.toList dts)
freshLocalName :: Monad m => CompileT m HsName
freshLocalName = CompileT $ do
i <- gets nameSupply
modify (\s -> s { nameSupply = i + 1 } )
return $ mkUniqueHsName "nl.uu.agda.fresh-local-name" [] ("x" ++ show i)
getConstrCTag :: QName -> Compile CTag
getConstrCTag q = do
def <- lift $ getConstInfo q
(arity, _) <- lift $ conArityAndPars q
case compiledCore $ defCompiledRep def of
Nothing -> do
let dtQ = conData $ theDef def
tag <- fromJust . elemIndex q . dataRecCons . theDef <$> lift (getConstInfo dtQ)
mkCTag <$> getCoreName dtQ <*> (getCoreName q) <*> pure tag <*> pure arity
Just (CrConstr crCon) -> do
return $ coreConstrToCTag crCon arity
_ -> __IMPOSSIBLE__
getConstrFun :: QName -> Compile HsName
getConstrFun q = do
def <- lift $ getConstInfo q
case compiledCore $ defCompiledRep def of
Nothing -> getCoreName q
Just (CrConstr crCon) ->
return $
destructCTag builtinUnitCtor (\_ con _ _ -> con)
(coreConstrToCTag crCon 0)
_ -> __IMPOSSIBLE__
dataRecCons :: Defn -> [QName]
dataRecCons r@(Record{}) = [recCon r]
dataRecCons d@(Datatype{}) = dataCons d
dataRecCons _ = __IMPOSSIBLE__
moduleNameToCoreNameParts :: ModuleName -> [String]
moduleNameToCoreNameParts modNm = "Agda" : (map show $ mnameToList modNm)
moduleNameToCoreName :: ModuleName -> HsName
moduleNameToCoreName modNm = mkHsName (init nmParts) (last nmParts)
where nmParts = moduleNameToCoreNameParts modNm
getCoreName :: QName -> Compile HsName
getCoreName qnm = CompileT $ do
lift $ getCoreName1 qnm
getCoreName1 :: QName -> TCM HsName
getCoreName1 qnm = do
modNm <- topLevelModuleName (qnameModule qnm)
def <- theDef <$> getConstInfo qnm
let locName = intercalate "_" $ map show $ either id id $ unqualifyQ modNm qnm
modParts = moduleNameToCoreNameParts modNm
identName = locName ++ "_" ++ show idnum
identName' = case def of
Datatype{} -> capitalize identName
Record{} -> capitalize identName
Constructor{} -> capitalize identName
_ -> identName
return $ mkUniqueHsName "nl.uu.agda.top-level-def" modParts identName
where
idnum = let (NameId x _) = nameId $ qnameName qnm in x
capitalize (x:xs) = (toUpper x):xs
capitalize _ = __IMPOSSIBLE__
unqualifyQ :: ModuleName -> QName -> Either [Name] [Name]
unqualifyQ modNm qnm =
case stripPrefix modNs qnms of
Nothing -> Left qnms
Just nm -> Right nm
where
modNs = mnameToList modNm
qnms = qnameToList qnm
instance MonadReader r m => MonadReader r (CompileT m) where
ask = lift ask
local f (CompileT x) = CompileT $ local f x
instance MonadState s m => MonadState s (CompileT m) where
get = lift get
put = lift . put
instance MonadTCM m => MonadTCM (CompileT m) where
liftTCM = lift . TM.liftTCM