Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Compiler.MAlonzo.Compiler

Synopsis

- ghcBackend :: Backend
- ghcBackend' :: Backend' GHCFlags GHCEnv GHCModuleEnv GHCModule GHCDefinition
- data GHCFlags = GHCFlags {
  - flagGhcCompile :: Bool
  - flagGhcCallGhc :: Bool
  - flagGhcBin :: Maybe FilePath
  - flagGhcFlags :: [String]
  - flagGhcStrictData :: Bool
  - flagGhcStrict :: Bool
  }
- defaultGHCFlags :: GHCFlags
- ghcCommandLineFlags :: [OptDescr (Flag GHCFlags)]
- withCompilerFlag :: FilePath -> Flag GHCFlags
- class Monad m => ReadGHCOpts m where
  - askGhcOpts :: m GHCOptions
- data GHCModule = GHCModule {
  - ghcModModuleEnv :: GHCModuleEnv
  - ghcModMainFuncs :: [MainFunctionDef]
  }
- data GHCDefinition = GHCDefinition {
  - ghcDefUsesFloat :: UsesFloat
  - ghcDefDecls :: [Decl]
  - ghcDefDefinition :: Definition
  - ghcDefMainDef :: Maybe MainFunctionDef
  - ghcDefImports :: Set ModuleName
  }
- ghcPreCompile :: GHCFlags -> TCM GHCEnv
- ghcPostCompile :: GHCEnv -> IsMain -> Map ModuleName GHCModule -> TCM ()
- ghcPreModule :: GHCEnv -> IsMain -> ModuleName -> Maybe FilePath -> TCM (Recompile GHCModuleEnv GHCModule)
- ghcPostModule :: GHCEnv -> GHCModuleEnv -> IsMain -> ModuleName -> [GHCDefinition] -> TCM GHCModule
- ghcCompileDef :: GHCEnv -> GHCModuleEnv -> IsMain -> Definition -> TCM GHCDefinition
- ghcMayEraseType :: QName -> TCM Bool
- imports :: BuiltinThings PrimFun -> Set ModuleName -> [Definition] -> [ImportDecl]
- newtype 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 = CCEnv {
  - _ccNameSupply :: NameSupply
  - _ccContext :: CCContext
  }
- type NameSupply = [Name]
- type CCContext = [Name]
- ccNameSupply :: Lens' NameSupply CCEnv
- ccContext :: Lens' CCContext CCEnv
- initCCEnv :: CCEnv
- lookupIndex :: Int -> CCContext -> Name
- type CCT m = ReaderT CCEnv (WriterT UsesFloat (HsCompileT m))
- type CC = CCT TCM
- 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
- 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
- noApplication :: TTerm -> CC Exp
- 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 :: Maybe Nat -> QName -> HsCompileM Decl
- compiledTypeSynonym :: QName -> String -> Nat -> Decl
- tvaldecl :: QName -> Induction -> 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 ()

# Documentation

ghcBackend :: Backend Source #

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

data GHCFlags Source #

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

Instances details

Generic GHCFlags Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Compiler Associated Types type Rep GHCFlags :: Type -> Type Source # Methods from :: GHCFlags -> Rep GHCFlags x Source # to :: Rep GHCFlags x -> GHCFlags Source #
NFData GHCFlags Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Compiler Methods rnf :: GHCFlags -> () Source #
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.2-7KnEKyKhaJHFPwDzdI3vIK" '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

- 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

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

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

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 Source # mappend :: UsesFloat -> UsesFloat -> UsesFloat Source # mconcat :: [UsesFloat] -> UsesFloat Source #
Semigroup UsesFloat Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Compiler Methods (<>) :: UsesFloat -> UsesFloat -> UsesFloat Source # sconcat :: NonEmpty UsesFloat -> UsesFloat Source # stimes :: Integral b => b -> UsesFloat -> UsesFloat Source #
Show UsesFloat Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Compiler Methods showsPrec :: Int -> UsesFloat -> ShowS Source # show :: UsesFloat -> String Source # showList :: [UsesFloat] -> ShowS Source #
Eq UsesFloat Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Compiler Methods (==) :: UsesFloat -> UsesFloat -> Bool Source # (/=) :: UsesFloat -> UsesFloat -> Bool Source #

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

- _ccNameSupply :: NameSupply

  Supply of fresh names

- _ccContext :: CCContext

  Names currently in scope

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 #