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

Safe Haskell | None
Language | Haskell2010

Agda.Compiler.Common

Synopsis

- data IsMain
  - = IsMain
  - | NotMain
- doCompile :: forall r. Monoid r => IsMain -> Interface -> (IsMain -> Interface -> TCM r) -> TCM r
- setInterface :: Interface -> TCM ()
- curIF :: TCM Interface
- curSig :: TCM Signature
- curMName :: TCM ModuleName
- curDefs :: TCM Definitions
- sortDefs :: Definitions -> [(QName, Definition)]
- sigMName :: Signature -> ModuleName
- compileDir :: TCM FilePath
- repl :: [String] -> String -> String
- conArityAndPars :: QName -> TCM (Nat, Nat)
- inCompilerEnv :: Interface -> TCM a -> TCM a
- topLevelModuleName :: ModuleName -> TCM ModuleName

# Documentation

data IsMain Source #

Constructors

IsMain |
NotMain |

Instances

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

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

setInterface :: Interface -> TCM () Source #

curIF :: TCM Interface Source #

curSig :: TCM Signature Source #

curMName :: TCM ModuleName Source #

curDefs :: TCM Definitions Source #

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

sigMName :: Signature -> ModuleName Source #

compileDir :: TCM FilePath Source #

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

conArityAndPars :: QName -> TCM (Nat, Nat) Source #

Copy pasted from MAlonzo.... Move somewhere else!

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

Sets up the compilation environment.

topLevelModuleName :: ModuleName -> TCM ModuleName Source #