Agda.Compiler.MAlonzo.Compiler

Documentation

ghcBackend :: Backend

ghcBackend' :: Backend' GHCFlags GHCEnv GHCModuleEnv GHCModule GHCDefinition

data GHCFlags

Constructors

GHCFlags

Fields

• flagGhcCompile :: Bool
• flagGhcCallGhc :: Bool
• flagGhcBin :: Maybe FilePath

  Use the compiler at PATH instead of "ghc"

• flagGhcFlags :: [String]
• flagGhcStrictData :: Bool

  Make inductive constructors strict?

• flagGhcStrict :: Bool

  Make functions strict?

Instances

Generic GHCFlags

Defined in Agda.Compiler.MAlonzo.Compiler

Associated Types

type Rep GHCFlags :: Type -> Type

Methods

from :: GHCFlags -> Rep GHCFlags x

to :: Rep GHCFlags x -> GHCFlags

NFData GHCFlags

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

rnf :: GHCFlags -> ()

type Rep GHCFlags

Defined in Agda.Compiler.MAlonzo.Compiler

type Rep GHCFlags = D1 ('MetaData "GHCFlags" "Agda.Compiler.MAlonzo.Compiler" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "GHCFlags" 'PrefixI 'True) ((S1 ('MetaSel ('Just "flagGhcCompile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "flagGhcCallGhc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "flagGhcBin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe FilePath)))) :*: (S1 ('MetaSel ('Just "flagGhcFlags") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]) :*: (S1 ('MetaSel ('Just "flagGhcStrictData") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "flagGhcStrict") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

defaultGHCFlags :: GHCFlags

ghcCommandLineFlags :: [OptDescr (Flag GHCFlags)]

withCompilerFlag :: FilePath -> Flag GHCFlags

class Monad m => ReadGHCOpts m where

Monads that can read GHCOptions

Methods

askGhcOpts :: m GHCOptions

Instances

Monad m => ReadGHCOpts (ReaderT GHCModule m)

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

askGhcOpts :: ReaderT GHCModule m GHCOptions

Monad m => ReadGHCOpts (ReaderT GHCEnv m)

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

askGhcOpts :: ReaderT GHCEnv m GHCOptions

Monad m => ReadGHCOpts (ReaderT GHCModuleEnv m)

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

askGhcOpts :: ReaderT GHCModuleEnv m GHCOptions

Monad m => ReadGHCOpts (ReaderT GHCOptions m)

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

askGhcOpts :: ReaderT GHCOptions m GHCOptions

data GHCModule

Constructors

GHCModule

Fields

• ghcModModuleEnv :: GHCModuleEnv
• ghcModMainFuncs :: [MainFunctionDef]

  The main function definition(s), if both the module is the IsMain module (root/focused) and a suitable main function was defined.

Instances

Monad m => ReadGHCOpts (ReaderT GHCModule m)

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

askGhcOpts :: ReaderT GHCModule m GHCOptions

Monad m => ReadGHCModuleEnv (ReaderT GHCModule m)

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

askGHCModuleEnv :: ReaderT GHCModule m GHCModuleEnv

askHsModuleEnv :: ReaderT GHCModule m HsModuleEnv

askGHCEnv :: ReaderT GHCModule m GHCEnv

data GHCDefinition

Constructors

GHCDefinition

Fields

• ghcDefUsesFloat :: UsesFloat
• ghcDefDecls :: [Decl]
• ghcDefDefinition :: Definition
• ghcDefMainDef :: Maybe MainFunctionDef
• ghcDefImports :: Set ModuleName

ghcPreCompile :: GHCFlags -> TCM GHCEnv

ghcPostCompile :: GHCEnv -> IsMain -> Map ModuleName GHCModule -> TCM ()

ghcPreModule

Arguments

:: GHCEnv

-> IsMain

Are we looking at the main module?

-> ModuleName

-> Maybe FilePath

Path to the .agdai file.

-> TCM (Recompile GHCModuleEnv GHCModule)

Could we confirm the existence of a main function?

ghcPostModule

Arguments

:: GHCEnv

-> GHCModuleEnv

-> IsMain

Are we looking at the main module?

-> ModuleName

-> [GHCDefinition]

Compiled module content.

-> TCM GHCModule

ghcCompileDef :: GHCEnv -> GHCModuleEnv -> IsMain -> Definition -> TCM GHCDefinition

ghcMayEraseType :: QName -> TCM Bool

We do not erase types that have a HsData pragma. This is to ensure a stable interface to third-party code.

imports :: BuiltinThings PrimFun -> Set ModuleName -> [Definition] -> [ImportDecl]

newtype UsesFloat

Constructors

UsesFloat Bool

Instances

Monoid UsesFloat

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

mempty :: UsesFloat

mappend :: UsesFloat -> UsesFloat -> UsesFloat

mconcat :: [UsesFloat] -> UsesFloat

Semigroup UsesFloat

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

(<>) :: UsesFloat -> UsesFloat -> UsesFloat

sconcat :: NonEmpty UsesFloat -> UsesFloat

stimes :: Integral b => b -> UsesFloat -> UsesFloat

Show UsesFloat

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

showsPrec :: Int -> UsesFloat -> ShowS

show :: UsesFloat -> String

showList :: [UsesFloat] -> ShowS

Eq UsesFloat

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

(==) :: UsesFloat -> UsesFloat -> Bool

(/=) :: UsesFloat -> UsesFloat -> Bool

pattern YesFloat :: UsesFloat

pattern NoFloat :: UsesFloat

mazRTEFloatImport :: UsesFloat -> [ImportDecl]

definition :: Definition -> HsCompileM (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)

constructorCoverageCode :: QName -> Int -> [QName] -> HaskellType -> [HaskellCode] -> HsCompileM [Decl]

data CCEnv

Environment for naming of local variables. Invariant: reverse ccCxt ++ ccNameSupply

Constructors

CCEnv

Fields

• _ccNameSupply :: NameSupply

  Supply of fresh names

• _ccContext :: CCContext

  Names currently in scope

type NameSupply = [Name]

type CCContext = [Name]

ccNameSupply :: Lens' NameSupply CCEnv

ccContext :: Lens' CCContext CCEnv

initCCEnv :: CCEnv

Initial environment for expression generation.

lookupIndex :: Int -> CCContext -> Name

Term variables are de Bruijn indices.

type CCT m = ReaderT CCEnv (WriterT UsesFloat (HsCompileT m))

Constructor coverage monad transformer

type CC = CCT TCM

Constructor coverage monad

liftCC :: Monad m => HsCompileT m a -> CCT m a

freshNames :: Monad m => Int -> ([Name] -> CCT m a) -> CCT m a

intros :: Monad m => Int -> ([Name] -> CCT m a) -> CCT m a

Introduce n variables into the context.

checkConstructorType :: QName -> HaskellCode -> HsCompileM [Decl]

checkCover :: HasConstInfo m => QName -> HaskellType -> Nat -> [QName] -> [HaskellCode] -> m [Decl]

closedTerm_ :: TTerm -> HsCompileM Exp

closedTerm :: TTerm -> HsCompileM (Exp, UsesFloat)

mkIf :: TTerm -> CC TTerm

term :: TTerm -> CC Exp

Extract Agda term to Haskell expression. Erased arguments are extracted as (). Types are extracted as ().

noApplication :: TTerm -> CC Exp

Translate a non-application, non-coercion, non-constructor, non-definition term.

hsCoerce :: Exp -> Exp

compilePrim :: TPrim -> Exp

alt :: Int -> TAlt -> CC Alt

literal :: forall m. Monad m => Literal -> CCT m Exp

hslit :: Literal -> Literal

litString :: Text -> Exp

litqname :: QName -> Exp

litqnamepat :: QName -> Pat

condecl :: QName -> Induction -> HsCompileM ConDecl

compiledcondecl

Arguments

:: Maybe Nat

The constructor's arity (after erasure).

-> QName

-> HsCompileM Decl

compiledTypeSynonym :: QName -> String -> Nat -> Decl

tvaldecl

Arguments

:: QName

-> Induction

Is the type inductive or coinductive?

-> Nat

-> [ConDecl]

-> Maybe Clause

-> [Decl]

infodecl :: QName -> [Decl] -> [Decl]

type MonadGHCIO m = (MonadIO m, ReadGHCOpts m)

copyRTEModules :: MonadGHCIO m => m ()

writeModule :: MonadGHCIO m => Module -> m ()

outFileAndDir :: MonadGHCIO m => ModuleName -> m (FilePath, FilePath)

curOutFileAndDir :: (MonadGHCIO m, ReadGHCModuleEnv m) => m (FilePath, FilePath)

curOutFile :: (MonadGHCIO m, ReadGHCModuleEnv m) => m FilePath

callGHC :: ReaderT GHCModule TCM ()