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

Safe Haskell | None
Language | Haskell2010

Agda.Compiler.Common

Synopsis

- doCompile :: Monoid r => (IsMain -> Interface -> TCM r) -> IsMain -> Interface -> TCM r
- repl :: [String] -> String -> String
- topLevelModuleName :: ReadTCState m => ModuleName -> m TopLevelModuleName
- curIF :: ReadTCState m => m Interface
- doCompile' :: Monoid r => (IsMain -> Interface -> TCM r) -> IsMain -> Interface -> StateT (Set ModuleName) TCM r
- setInterface :: Interface -> TCM ()
- curMName :: ReadTCState m => m TopLevelModuleName
- curDefs :: ReadTCState m => m Definitions
- sortDefs :: Definitions -> [(QName, Definition)]
- compileDir :: HasOptions m => m FilePath
- inCompilerEnv :: CheckResult -> TCM a -> TCM a
- data IsMain
  - = IsMain
  - | NotMain

# Documentation

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

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

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

curIF :: ReadTCState m => m Interface Source #

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

setInterface :: Interface -> TCM () Source #

curMName :: ReadTCState m => m TopLevelModuleName Source #

curDefs :: ReadTCState m => m Definitions Source #

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

compileDir :: HasOptions m => m FilePath Source #

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

Sets up the compilation environment.

data IsMain Source #

Constructors

IsMain |
NotMain |

#### Instances

Instances details

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