Agda-2.6.2.1: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Compiler.MAlonzo.Compiler

Synopsis

Documentation

ghcBackend :: Backend Source #

ghcBackend' :: Backend' GHCFlags GHCEnv GHCModuleEnv GHCModule GHCDefinition Source #

data GHCFlags Source #

Constructors

GHCFlags 

Fields

Instances

Instances details
Generic GHCFlags Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

rnf :: GHCFlags -> () #

type Rep GHCFlags Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Compiler

type Rep GHCFlags = D1 ('MetaData "GHCFlags" "Agda.Compiler.MAlonzo.Compiler" "Agda-2.6.2.1-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 Source #

ghcCommandLineFlags :: [OptDescr (Flag GHCFlags)] Source #

withCompilerFlag :: FilePath -> Flag GHCFlags Source #

class Monad m => ReadGHCOpts m where Source #

Monads that can read GHCOptions

Methods

askGhcOpts :: m GHCOptions Source #

Instances

Instances details
Monad m => ReadGHCOpts (ReaderT GHCModule m) Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

askGhcOpts :: ReaderT GHCModule m GHCOptions Source #

Monad m => ReadGHCOpts (ReaderT GHCEnv m) Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

askGhcOpts :: ReaderT GHCEnv m GHCOptions Source #

Monad m => ReadGHCOpts (ReaderT GHCModuleEnv m) Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

askGhcOpts :: ReaderT GHCModuleEnv m GHCOptions Source #

Monad m => ReadGHCOpts (ReaderT GHCOptions m) Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

askGhcOpts :: ReaderT GHCOptions m GHCOptions Source #

data GHCModule Source #

Constructors

GHCModule 

Fields

Instances

Instances details
Monad m => ReadGHCOpts (ReaderT GHCModule m) Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

askGhcOpts :: ReaderT GHCModule m GHCOptions Source #

Monad m => ReadGHCModuleEnv (ReaderT GHCModule m) Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

askGHCModuleEnv :: ReaderT GHCModule m GHCModuleEnv Source #

askHsModuleEnv :: ReaderT GHCModule m HsModuleEnv Source #

askGHCEnv :: ReaderT GHCModule m GHCEnv Source #

data GHCDefinition Source #

Constructors

GHCDefinition 

Fields

ghcPreCompile :: GHCFlags -> TCM GHCEnv Source #

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

ghcPreModule Source #

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 Source #

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 Source #

ghcMayEraseType :: QName -> TCM Bool Source #

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] Source #

newtype UsesFloat Source #

Constructors

UsesFloat Bool 

Instances

Instances details
Monoid UsesFloat Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

mempty :: UsesFloat #

mappend :: UsesFloat -> UsesFloat -> UsesFloat #

mconcat :: [UsesFloat] -> UsesFloat #

Semigroup UsesFloat Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

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

sconcat :: NonEmpty UsesFloat -> UsesFloat #

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

Show UsesFloat Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

showsPrec :: Int -> UsesFloat -> ShowS #

show :: UsesFloat -> String #

showList :: [UsesFloat] -> ShowS #

Eq UsesFloat Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

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

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

pattern YesFloat :: UsesFloat Source #

pattern NoFloat :: UsesFloat Source #

mazRTEFloatImport :: UsesFloat -> [ImportDecl] Source #

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

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

data CCEnv Source #

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

Constructors

CCEnv 

Fields

type NameSupply = [Name] Source #

type CCContext = [Name] Source #

ccNameSupply :: Lens' NameSupply CCEnv Source #

ccContext :: Lens' CCContext CCEnv Source #

initCCEnv :: CCEnv Source #

Initial environment for expression generation.

lookupIndex :: Int -> CCContext -> Name Source #

Term variables are de Bruijn indices.

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

Constructor coverage monad transformer

type CC = CCT TCM Source #

Constructor coverage monad

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

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

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

Introduce n variables into the context.

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

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

closedTerm_ :: TTerm -> HsCompileM Exp Source #

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

mkIf :: TTerm -> CC TTerm Source #

term :: TTerm -> CC Exp Source #

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

noApplication :: TTerm -> CC Exp Source #

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

hsCoerce :: Exp -> Exp Source #

compilePrim :: TPrim -> Exp Source #

alt :: Int -> TAlt -> CC Alt Source #

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

hslit :: Literal -> Literal Source #

litString :: Text -> Exp Source #

litqname :: QName -> Exp Source #

litqnamepat :: QName -> Pat Source #

condecl :: QName -> Induction -> HsCompileM ConDecl Source #

compiledcondecl Source #

Arguments

:: Maybe Nat

The constructor's arity (after erasure).

-> QName 
-> HsCompileM Decl 

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

tvaldecl Source #

Arguments

:: QName 
-> Induction

Is the type inductive or coinductive?

-> Nat 
-> [ConDecl] 
-> Maybe Clause 
-> [Decl] 

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

type MonadGHCIO m = (MonadIO m, ReadGHCOpts m) Source #

copyRTEModules :: MonadGHCIO m => m () Source #

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

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

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

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

callGHC :: ReaderT GHCModule TCM () Source #