Agda.Compiler.Common

Documentation

data IsMain

Constructors

IsMain

NotMain

Instances

Monoid IsMain

Defined in Agda.Compiler.Common

Methods

mempty :: IsMain

mappend :: IsMain -> IsMain -> IsMain

mconcat :: [IsMain] -> IsMain

Semigroup IsMain

Conjunctive semigroup (NotMain is absorbing).

Defined in Agda.Compiler.Common

Methods

(<>) :: IsMain -> IsMain -> IsMain

sconcat :: NonEmpty IsMain -> IsMain

stimes :: Integral b => b -> IsMain -> IsMain

Show IsMain

Defined in Agda.Compiler.Common

Methods

showsPrec :: Int -> IsMain -> ShowS

show :: IsMain -> String

showList :: [IsMain] -> ShowS

Eq IsMain

Defined in Agda.Compiler.Common

Methods

(==) :: IsMain -> IsMain -> Bool

(/=) :: IsMain -> IsMain -> Bool

doCompile :: Monoid r => (IsMain -> Interface -> TCM r) -> IsMain -> Interface -> TCM r

doCompile' :: Monoid r => (IsMain -> Interface -> TCM r) -> IsMain -> Interface -> StateT (Set ModuleName) TCM r

setInterface :: Interface -> TCM ()

curIF :: ReadTCState m => m Interface

curMName :: ReadTCState m => m TopLevelModuleName

curDefs :: ReadTCState m => m Definitions

sortDefs :: Definitions -> [(QName, Definition)]

compileDir :: HasOptions m => m FilePath

repl :: [String] -> String -> String

inCompilerEnv :: CheckResult -> TCM a -> TCM a

Sets up the compilation environment.

topLevelModuleName :: ReadTCState m => ModuleName -> m TopLevelModuleName