Safe Haskell	None
Language	Haskell98

Agda.Compiler.MAlonzo.Compiler

Synopsis

Documentation

compilerMain :: IsMain -> Interface -> TCM () Source

compile :: Interface -> TCM () Source

imports :: TCM [ImportDecl] Source

definitions :: Definitions -> TCM [Decl] Source

definition :: Maybe CoinductionKit -> Definition -> TCM [Decl] Source

Note that the INFINITY, SHARP and FLAT builtins are translated as follows (if a CoinductionKit is given):

  type Infinity a b = b

  sharp :: a -> a
  sharp x = x

  flat :: a -> a
  flat x = x

data CCEnv Source

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

Constructors

CCEnv
Fields ccNameSupply :: NameSupply Supply of fresh names ccCxt :: CCContext Names currently in scope

type NameSupply = [Name] Source

type CCContext = [Name] Source

mapNameSupply :: (NameSupply -> NameSupply) -> CCEnv -> CCEnv Source

mapContext :: (CCContext -> CCContext) -> CCEnv -> CCEnv Source

initCCEnv :: CCEnv Source

Initial environment for expression generation.

lookupIndex :: Int -> CCContext -> Name Source

Term variables are de Bruijn indices.

type CC = ReaderT CCEnv TCM Source

freshNames :: Int -> ([Name] -> CC a) -> CC a Source

intros :: Int -> ([Name] -> CC a) -> CC a Source

Introduce n variables into the context.

checkConstructorType :: QName -> TCM [Decl] Source

checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [Decl] Source

closedTerm :: TTerm -> TCM Exp Source

term :: TTerm -> CC Exp Source

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

compilePrim :: TPrim -> Exp Source

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

literal :: Literal -> TCM Exp Source

hslit :: Literal -> Literal Source

litString :: String -> Exp Source

litqname :: QName -> Exp Source

litqnamepat :: QName -> Pat Source

condecl :: QName -> TCM (Nat, ConDecl) Source

cdecl :: QName -> Nat -> ConDecl Source

tvaldecl Source

Arguments

:: QName
-> Induction	Is the type inductive or coinductive?
-> Nat
-> Nat
-> [ConDecl]
-> Maybe Clause
-> [Decl]

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

hsCast :: Exp -> Exp Source

hsCast' :: Exp -> Exp Source

hsCastApp :: Exp -> Exp Source

hsCoerce :: Exp -> Exp Source

copyRTEModules :: TCM () Source

writeModule :: Module -> TCM () Source

outFile' :: (Pretty a, TransformBi ModuleName (Wrap a)) => a -> TCM (FilePath, FilePath) Source

outFile :: ModuleName -> TCM FilePath Source

outFile_ :: TCM FilePath Source

callGHC :: IsMain -> Interface -> TCM () Source