| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Compiler.Alonzo.Main

Synopsis

compilerMain :: TCM () -> TCM ()
fromCurrentModule :: QName -> TCM Bool
flattenSubmodules :: QName -> TCM QName
maybeQualName :: (QName -> HsQName) -> (Name -> HsName) -> QName -> PM HsQName
numOfMainS :: [QName] -> Maybe Nat
processDefWithDebug :: (QName, Definition) -> TCM [HsDecl]
infoDecl :: String -> String -> HsDecl
processDef :: (QName, Definition) -> TCM [HsDecl]
times :: Nat -> a -> [a]
consDefs :: [QName] -> TCM [Definition]
processClause :: Name -> Nat -> Clause -> TCM HsDecl
contClause :: Name -> Nat -> Clause -> TCM HsDecl
foldClauses :: Name -> Nat -> [Clause] -> TCM [HsDecl]
processArgPats :: [Arg Pattern] -> PM [HsPat]
processArgPat :: Arg Pattern -> PM HsPat
processPat :: Pattern -> PM HsPat
processBody :: ClauseBody -> PM HsExp
processTerm :: Term -> PM HsExp
processLit :: Literal -> HsExp
processVap :: HsExp -> [Arg Term] -> PM HsExp
unfoldVap :: PState -> HsExp -> [Arg Term] -> TCM HsExp
getDefinitions :: TCM Definitions
getConArity :: QName -> TCM Nat
typeArity :: Type -> Nat
clauseBod :: Clause -> Term
vecApp :: HsExp -> [HsExp] -> HsExp

Documentation

compilerMain :: TCM () -> TCM () | Source

The main function

fromCurrentModule :: QName -> TCM Bool | Source

flattenSubmodules :: QName -> TCM QName | Source

maybeQualName :: (QName -> HsQName) -> (Name -> HsName) -> QName -> PM HsQName | Source

numOfMainS :: [QName] -> Maybe Nat | Source

processDefWithDebug :: (QName, Definition) -> TCM [HsDecl] | Source

infoDecl :: String -> String -> HsDecl | Source

processDef :: (QName, Definition) -> TCM [HsDecl] | Source

times :: Nat -> a -> [a] | Source

consDefs :: [QName] -> TCM [Definition] | Source

processClause :: Name -> Nat -> Clause -> TCM HsDecl | Source

contClause :: Name -> Nat -> Clause -> TCM HsDecl | Source

foldClauses :: Name -> Nat -> [Clause] -> TCM [HsDecl] | Source

processArgPats :: [Arg Pattern] -> PM [HsPat] | Source

processArgPat :: Arg Pattern -> PM HsPat | Source

processPat :: Pattern -> PM HsPat | Source

processBody :: ClauseBody -> PM HsExp | Source

processTerm :: Term -> PM HsExp | Source

processLit :: Literal -> HsExp | Source

processVap :: HsExp -> [Arg Term] -> PM HsExp | Source

unfoldVap :: PState -> HsExp -> [Arg Term] -> TCM HsExp | Source

getDefinitions :: TCM Definitions | Source

getConArity :: QName -> TCM Nat | Source

typeArity :: Type -> Nat | Source

clauseBod :: Clause -> Term | Source

vecApp :: HsExp -> [HsExp] -> HsExp | Source

Produced by Haddock version 2.4.2