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

Agda.Compiler.MAlonzo.Compiler

Synopsis

Documentation

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.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)))))

class Monad m => ReadGHCOpts m where Source #

Monads that can read GHCOptions

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

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

Defined in Agda.Compiler.MAlonzo.Compiler

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

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 

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.

data CCEnv Source #

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

Constructors

CCEnv 

Fields

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.

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.

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

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

compiledcondecl Source #

Arguments

:: Maybe Nat

The constructor's arity (after erasure).

-> QName 
-> HsCompileM Decl 

tvaldecl Source #

Arguments

:: QName 
-> Induction

Is the type inductive or coinductive?

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

callGHC :: ReaderT GHCModule TCM () Source #