Agda.Compiler.Alonzo.Main

Documentation

compilerMain :: TCM () -> TCM ()

The main function

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