Agda.Compiler.UHC.CompileState

Contains the state monad that the compiler works in and some functions for tampering with the state.

Documentation

data CompileT m a

Compiler monad

Instances

MonadTrans CompileT

Methods

lift :: Monad m => m a -> CompileT m a

MonadReader r m => MonadReader r (CompileT m)

Methods

ask :: CompileT m r

local :: (r -> r) -> CompileT m a -> CompileT m a

reader :: (r -> a) -> CompileT m a

MonadState s m => MonadState s (CompileT m)

Methods

get :: CompileT m s

put :: s -> CompileT m ()

state :: (s -> (a, s)) -> CompileT m a

Monad m => Monad (CompileT m)

Methods

(>>=) :: CompileT m a -> (a -> CompileT m b) -> CompileT m b

(>>) :: CompileT m a -> CompileT m b -> CompileT m b

return :: a -> CompileT m a

fail :: String -> CompileT m a

Functor m => Functor (CompileT m)

Methods

fmap :: (a -> b) -> CompileT m a -> CompileT m b

(<$) :: a -> CompileT m b -> CompileT m a

Monad m => Applicative (CompileT m)

Methods

pure :: a -> CompileT m a

(<*>) :: CompileT m (a -> b) -> CompileT m a -> CompileT m b

(*>) :: CompileT m a -> CompileT m b -> CompileT m b

(<*) :: CompileT m a -> CompileT m b -> CompileT m a

MonadIO m => MonadIO (CompileT m)

Methods

liftIO :: IO a -> CompileT m a

MonadTCM m => MonadTCM (CompileT m)

Methods

liftTCM :: TCM a -> CompileT m a

type Compile = CompileT TCM

runCompileT

Arguments

:: MonadIO m

=> ModuleName

The module to compile.

-> CompileT m a

-> m a

Used to run the Agda-to-UHC Core transformation. During this transformation,

data CoreMeta

Instances

Semigroup CoreMeta

Methods

(<>) :: CoreMeta -> CoreMeta -> CoreMeta

sconcat :: NonEmpty CoreMeta -> CoreMeta

stimes :: Integral b => b -> CoreMeta -> CoreMeta

Monoid CoreMeta

Methods

mempty :: CoreMeta

mappend :: CoreMeta -> CoreMeta -> CoreMeta

mconcat :: [CoreMeta] -> CoreMeta

addExports :: Monad m => [HsName] -> CompileT m ()

addMetaCon :: QName -> CDataCon -> Compile ()

addMetaData :: QName -> ([CDataCon] -> CDeclMeta) -> Compile ()

getExports :: Compile [CExport]

getDeclMetas :: Compile [CDeclMeta]

getCoreName :: QName -> Compile HsName

getCoreName1 :: QName -> TCM HsName

getConstrCTag :: QName -> Compile CTag

Returns the CTag for a constructor. Not defined for Sharp and magic UNIT constructor.

getConstrFun :: QName -> Compile HsName

Returns the expression to use to build a value of the given datatype/constructor.

moduleNameToCoreName :: ModuleName -> HsName

moduleNameToCoreNameParts :: ModuleName -> [String]

freshLocalName :: Monad m => CompileT m HsName

conArityAndPars :: QName -> TCM (Nat, Nat)

Copy pasted from MAlonzo.... Move somewhere else!

dataRecCons :: Defn -> [QName]