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

Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Compiler.Common

Synopsis

data IsMain
- = IsMain
- | NotMain
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
topLevelModuleName :: ReadTCState m => ModuleName -> m TopLevelModuleName

Documentation

data IsMain Source #

Constructors

IsMain
NotMain

Instances

Instances details

Monoid IsMain Source #
Instance details Defined in Agda.Compiler.Common Methods mempty :: IsMain mappend :: IsMain -> IsMain -> IsMain mconcat :: [IsMain] -> IsMain
Semigroup IsMain Source #	Conjunctive semigroup (`NotMain` is absorbing).
Instance details Defined in Agda.Compiler.Common Methods (<>) :: IsMain -> IsMain -> IsMain # sconcat :: NonEmpty IsMain -> IsMain stimes :: Integral b => b -> IsMain -> IsMain
Show IsMain Source #
Instance details Defined in Agda.Compiler.Common Methods showsPrec :: Int -> IsMain -> ShowS show :: IsMain -> String showList :: [IsMain] -> ShowS
Eq IsMain Source #
Instance details Defined in Agda.Compiler.Common Methods (==) :: IsMain -> IsMain -> Bool (/=) :: IsMain -> IsMain -> Bool

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

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

setInterface :: Interface -> TCM () Source #

curIF :: ReadTCState m => m Interface Source #

curMName :: ReadTCState m => m TopLevelModuleName Source #

curDefs :: ReadTCState m => m Definitions Source #

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

compileDir :: HasOptions m => m FilePath Source #

repl :: [String] -> String -> String Source #

inCompilerEnv :: CheckResult -> TCM a -> TCM a Source #

Sets up the compilation environment.

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