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

Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.Backend

Description

Interface for compiler backend writers.

Synopsis

Documentation

data Backend where Source #

Constructors

Backend :: Backend' opts env menv mod def -> Backend 

data Backend' opts env menv mod def Source #

Constructors

Backend' 

Fields

  • backendName :: String
     
  • backendVersion :: Maybe String

    Optional version information to be printed with --version.

  • options :: opts

    Default options

  • commandLineFlags :: [OptDescr (Flag opts)]

    Backend-specific command-line flags. Should at minimum contain a flag to enable the backend.

  • isEnabled :: opts -> Bool

    Unless the backend has been enabled, runAgda will fall back to vanilla Agda behaviour.

  • preCompile :: opts -> TCM env

    Called after type checking completes, but before compilation starts.

  • postCompile :: env -> IsMain -> Map ModuleName mod -> TCM ()

    Called after module compilation has completed. The IsMain argument is NotMain if the --no-main flag is present.

  • preModule :: env -> IsMain -> ModuleName -> FilePath -> TCM (Recompile menv mod)

    Called before compilation of each module. Gets the path to the .agdai file to allow up-to-date checking of previously written compilation results. Should return Skip m if compilation is not required.

  • postModule :: env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod

    Called after all definitions of a module have been compiled.

  • compileDef :: env -> menv -> IsMain -> Definition -> TCM def

    Compile a single definition.

  • scopeCheckingSuffices :: Bool

    True if the backend works if --only-scope-checking is used.

  • mayEraseType :: QName -> TCM Bool

    The treeless compiler may ask the Backend if elements of the given type maybe possibly erased. The answer should be False if the compilation of the type is used by a third party, e.g. in a FFI binding.

data Recompile menv mod Source #

Constructors

Recompile menv 
Skip mod 

data IsMain Source #

Constructors

IsMain 
NotMain 
Instances
Eq IsMain Source # 
Instance details

Defined in Agda.Compiler.Common

Methods

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

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

Show IsMain Source # 
Instance details

Defined in Agda.Compiler.Common

Semigroup IsMain Source #

Conjunctive semigroup (NotMain is absorbing).

Instance details

Defined in Agda.Compiler.Common

Monoid IsMain Source # 
Instance details

Defined in Agda.Compiler.Common

type Flag opts = opts -> OptM opts Source #

f :: Flag opts is an action on the option record that results from parsing an option. f opts produces either an error message or an updated options record

toTreeless :: EvaluationStrategy -> QName -> TCM (Maybe TTerm) Source #

Converts compiled clauses to treeless syntax.

Note: Do not use any of the concrete names in the returned term for identification purposes! If you wish to do so, first apply the Agda.Compiler.Treeless.NormalizeNames transformation.

builtinsNoDef :: [String] Source #

Builtins that come without a definition in Agda syntax. These are giving names to Agda internal concepts which cannot be assigned an Agda type.

An example would be a user-defined name for Set.

{--}

The type of Type would be Type : Level → Setω which is not valid Agda.

data Polarity Source #

Polarity for equality and subtype checking.

Constructors

Covariant

monotone

Contravariant

antitone

Invariant

no information (mixed variance)

Nonvariant

constant

Instances
Eq Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Polarity -> c Polarity #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Polarity #

toConstr :: Polarity -> Constr #

dataTypeOf :: Polarity -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Polarity) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Polarity) #

gmapT :: (forall b. Data b => b -> b) -> Polarity -> Polarity #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Polarity -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Polarity -> r #

gmapQ :: (forall d. Data d => d -> u) -> Polarity -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Polarity -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity #

Show Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Abstract [Polarity] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply [Polarity] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

newtype ProblemId Source #

Constructors

ProblemId Nat 
Instances
Enum ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Integral ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemId -> c ProblemId #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemId #

toConstr :: ProblemId -> Constr #

dataTypeOf :: ProblemId -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemId) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemId) #

gmapT :: (forall b. Data b => b -> b) -> ProblemId -> ProblemId #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r #

gmapQ :: (forall d. Data d => d -> u) -> ProblemId -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemId -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId #

Num ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Ord ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Real ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

ToJSON ProblemId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Pretty ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasFresh ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

EncodeTCM ProblemId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Monad m => MonadFresh ProblemId (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

data Comparison Source #

Constructors

CmpEq 
CmpLeq 
Instances
Eq Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Comparison -> c Comparison #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Comparison #

toConstr :: Comparison -> Constr #

dataTypeOf :: Comparison -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Comparison) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Comparison) #

gmapT :: (forall b. Data b => b -> b) -> Comparison -> Comparison #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Comparison -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Comparison -> r #

gmapQ :: (forall d. Data d => d -> u) -> Comparison -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Comparison -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison #

Show Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

type ModuleToSource = Map TopLevelModuleName AbsolutePath Source #

Maps top-level module names to the corresponding source file names.

type TCM = TCMT IO Source #

Type checking monad.

newtype TCMT m a Source #

The type checking monad transformer. Adds readonly TCEnv and mutable TCState.

Constructors

TCM 

Fields

Instances
MonadTrans TCMT Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

lift :: Monad m => m a -> TCMT m a #

CatchImpossible TCM Source #

Like catchError, but resets the state completely before running the handler. This means it also loses changes to the stPersistentState.

The intended use is to catch internal errors during debug printing. In debug printing, we are not expecting state changes.

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

catchImpossible :: TCM a -> (Impossible -> TCM a) -> TCM a Source #

catchImpossibleJust :: (Impossible -> Maybe b) -> TCM a -> (b -> TCM a) -> TCM a Source #

handleImpossible :: (Impossible -> TCM a) -> TCM a -> TCM a Source #

handleImpossibleJust :: (Impossible -> Maybe b) -> (b -> TCM a) -> TCM a -> TCM a Source #

MonadFixityError ScopeM Source # 
Instance details

Defined in Agda.Syntax.Scope.Monad

MonadStConcreteNames TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadInteractionPoints TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

MonadAddContext TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> TCM a -> TCM a Source #

addLetBinding' :: Name -> Term -> Dom Type -> TCM a -> TCM a Source #

updateContext :: Substitution -> (Context -> Context) -> TCM a -> TCM a Source #

withFreshName :: Range -> ArgName -> (Name -> TCM a) -> TCM a Source #

MonadDebug TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

MonadStatistics TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> TCM () Source #

MonadWarning TCM Source # 
Instance details

Defined in Agda.TypeChecking.Warnings

Methods

addWarning :: TCWarning -> TCM () Source #

MonadConstraint TCM Source # 
Instance details

Defined in Agda.TypeChecking.Constraints

MonadMetaSolver TCM Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars

MonadError TCErr TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

throwError :: TCErr -> TCM a #

catchError :: TCM a -> (TCErr -> TCM a) -> TCM a #

MonadError TCErr IM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

throwError :: TCErr -> IM a #

catchError :: IM a -> (TCErr -> IM a) -> IM a #

MonadBench Phase TCM Source #

We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking.

Instance details

Defined in Agda.TypeChecking.Monad.Base

HasFresh i => MonadFresh i TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fresh :: TCM i Source #

Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #

Conversion TOM Type (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O) Source #

Conversion TOM Term (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O) Source #

Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #

Conversion TOM [Clause] [([Pat O], MExp O)] Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #

Conversion TOM (Arg Pattern) (Pat O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Arg Pattern -> TOM (Pat O) Source #

Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Arg a -> TOM (Hiding, b) Source #

MonadIO m => Monad (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(>>=) :: TCMT m a -> (a -> TCMT m b) -> TCMT m b #

(>>) :: TCMT m a -> TCMT m b -> TCMT m b #

return :: a -> TCMT m a #

fail :: String -> TCMT m a #

MonadIO m => Functor (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> TCMT m a -> TCMT m b #

(<$) :: a -> TCMT m b -> TCMT m a #

MonadIO m => MonadFail (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fail :: String -> TCMT m a #

MonadIO m => Applicative (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pure :: a -> TCMT m a #

(<*>) :: TCMT m (a -> b) -> TCMT m a -> TCMT m b #

liftA2 :: (a -> b -> c) -> TCMT m a -> TCMT m b -> TCMT m c #

(*>) :: TCMT m a -> TCMT m b -> TCMT m b #

(<*) :: TCMT m a -> TCMT m b -> TCMT m a #

Semigroup (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Warnings

Methods

(<>) :: TCM Doc -> TCM Doc -> TCM Doc #

sconcat :: NonEmpty (TCM Doc) -> TCM Doc #

stimes :: Integral b => b -> TCM Doc -> TCM Doc #

MonadIO m => MonadIO (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftIO :: IO a -> TCMT m a #

Null (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadIO m => MonadTCM (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> TCMT m a Source #

MonadIO m => MonadTCState (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadIO m => MonadTCEnv (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: TCMT m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> TCMT m a -> TCMT m a Source #

MonadIO m => MonadReduce (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> TCMT m a Source #

MonadIO m => HasOptions (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadIO m => ReadTCState (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: TCMT m TCState Source #

locallyTCState :: Lens' a TCState -> (a -> a) -> TCMT m b -> TCMT m b Source #

withTCState :: (TCState -> TCState) -> TCMT m a -> TCMT m a Source #

MonadIO m => HasBuiltins (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

TraceS [TCM Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m c -> m c Source #

TraceS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c Source #

ReportS [TCM Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m () Source #

ReportS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m () Source #

HasConstInfo (TCMT IO) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Signature

(IsString a, MonadIO m) => IsString (TCMT m a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fromString :: String -> TCMT m a #

(MonadIO m, Semigroup a) => Semigroup (TCMT m a) Source #

Strict (non-shortcut) semigroup.

Note that there might be a lazy alternative, e.g., for TCM All we might want and2M as concatenation, to shortcut conjunction in case we already have False.

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(<>) :: TCMT m a -> TCMT m a -> TCMT m a #

sconcat :: NonEmpty (TCMT m a) -> TCMT m a #

stimes :: Integral b => b -> TCMT m a -> TCMT m a #

(MonadIO m, Semigroup a, Monoid a) => Monoid (TCMT m a) Source #

Strict (non-shortcut) monoid.

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

mempty :: TCMT m a #

mappend :: TCMT m a -> TCMT m a -> TCMT m a #

mconcat :: [TCMT m a] -> TCMT m a #

data TCState Source #

Constructors

TCSt 

Fields

Instances
Show TCState Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensPersistentVerbosity TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensIncludePaths TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensSafeMode TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensCommandLineOptions TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensVerbosity TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensPragmaOptions TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

data TCEnv Source #

Constructors

TCEnv 

Fields

Instances
Data TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TCEnv -> c TCEnv #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TCEnv #

toConstr :: TCEnv -> Constr #

dataTypeOf :: TCEnv -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TCEnv) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TCEnv) #

gmapT :: (forall b. Data b => b -> b) -> TCEnv -> TCEnv #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TCEnv -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TCEnv -> r #

gmapQ :: (forall d. Data d => d -> u) -> TCEnv -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TCEnv -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TCEnv -> m TCEnv #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TCEnv -> m TCEnv #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TCEnv -> m TCEnv #

LensIsAbstract TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensRelevance TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensQuantity TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensModality TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensTCEnv TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data HighlightingLevel Source #

How much highlighting should be sent to the user interface?

Constructors

None 
NonInteractive 
Interactive

This includes both non-interactive highlighting and interactive highlighting of the expression that is currently being type-checked.

Instances
Eq HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HighlightingLevel -> c HighlightingLevel #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HighlightingLevel #

toConstr :: HighlightingLevel -> Constr #

dataTypeOf :: HighlightingLevel -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HighlightingLevel) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HighlightingLevel) #

gmapT :: (forall b. Data b => b -> b) -> HighlightingLevel -> HighlightingLevel #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingLevel -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingLevel -> r #

gmapQ :: (forall d. Data d => d -> u) -> HighlightingLevel -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> HighlightingLevel -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HighlightingLevel -> m HighlightingLevel #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingLevel -> m HighlightingLevel #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingLevel -> m HighlightingLevel #

Ord HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Read HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data HighlightingMethod Source #

How should highlighting be sent to the user interface?

Constructors

Direct

Via stdout.

Indirect

Both via files and via stdout.

Instances
Eq HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HighlightingMethod -> c HighlightingMethod #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HighlightingMethod #

toConstr :: HighlightingMethod -> Constr #

dataTypeOf :: HighlightingMethod -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HighlightingMethod) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HighlightingMethod) #

gmapT :: (forall b. Data b => b -> b) -> HighlightingMethod -> HighlightingMethod #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingMethod -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingMethod -> r #

gmapQ :: (forall d. Data d => d -> u) -> HighlightingMethod -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> HighlightingMethod -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HighlightingMethod -> m HighlightingMethod #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingMethod -> m HighlightingMethod #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingMethod -> m HighlightingMethod #

Read HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data NamedMeta Source #

For printing, we couple a meta with its name suggestion.

data TCWarning Source #

Constructors

TCWarning 

Fields

data TCErr Source #

Type-checking errors.

Constructors

TypeError 

Fields

Exception Range Doc 
IOException TCState Range IOException

The first argument is the state in which the error was raised.

PatternErr

The exception which is usually caught. Raised for pattern violations during unification (assignV) but also in other situations where we want to backtrack.

Instances
Show TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> TCErr -> ShowS #

show :: TCErr -> String #

showList :: [TCErr] -> ShowS #

Exception TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Error TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: TCErr -> Range Source #

PrettyTCM TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: MonadPretty m => TCErr -> m Doc Source #

MonadError TCErr TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

throwError :: TCErr -> TCM a #

catchError :: TCM a -> (TCErr -> TCM a) -> TCM a #

MonadError TCErr IM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

throwError :: TCErr -> IM a #

catchError :: IM a -> (TCErr -> IM a) -> IM a #

MonadError TCErr TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

throwError :: TCErr -> TerM a #

catchError :: TerM a -> (TCErr -> TerM a) -> TerM a #

Monad m => MonadError TCErr (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

data Warning Source #

A non-fatal error is an error which does not prevent us from checking the document further and interacting with the user.

Constructors

NicifierIssue DeclarationWarning 
TerminationIssue [TerminationError] 
UnreachableClauses QName [Range]

`UnreachableClauses f rs` means that the clauses in f whose ranges are rs are unreachable

CoverageIssue QName [(Telescope, [NamedArg DeBruijnPattern])]

`CoverageIssue f pss` means that pss are not covered in f

CoverageNoExactSplit QName [Clause] 
NotStrictlyPositive QName (Seq OccursWhere) 
UnsolvedMetaVariables [Range]

Do not use directly with warning

UnsolvedInteractionMetas [Range]

Do not use directly with warning

UnsolvedConstraints Constraints

Do not use directly with warning

CantGeneralizeOverSorts [MetaId] 
AbsurdPatternRequiresNoRHS [NamedArg DeBruijnPattern] 
OldBuiltin String String

In `OldBuiltin old new`, the BUILTIN old has been replaced by new

EmptyRewritePragma

If the user wrote just {-# REWRITE #-}.

IllformedAsClause String

If the user wrote something other than an unqualified name in the as clause of an import statement. The String gives optionally extra explanation.

ClashesViaRenaming NameOrModule [Name]

If a renaming import directive introduces a name or module name clash in the exported names of a module. (See issue #4154.)

UselessPublic

If the user opens a module public before the module header. (See issue #2377.)

UselessInline QName 
WrongInstanceDeclaration 
InstanceWithExplicitArg QName

An instance was declared with an implicit argument, which means it will never actually be considered by instance search.

InstanceNoOutputTypeName Doc

The type of an instance argument doesn't end in a named or variable type, so it will never be considered by instance search.

InstanceArgWithExplicitArg Doc

As InstanceWithExplicitArg, but for local bindings rather than top-level instances.

InversionDepthReached QName

The --inversion-max-depth was reached. Generic warnings for one-off things

GenericWarning Doc

Harmless generic warning (not an error)

GenericNonFatalError Doc

Generic error which doesn't abort proceedings (not a warning) Safe flag errors

SafeFlagPostulate Name 
SafeFlagPragma [String]

Unsafe OPTIONS.

SafeFlagNonTerminating 
SafeFlagTerminating 
SafeFlagWithoutKFlagPrimEraseEquality 
WithoutKFlagPrimEraseEquality 
SafeFlagNoPositivityCheck 
SafeFlagPolarity 
SafeFlagNoUniverseCheck 
SafeFlagNoCoverageCheck 
SafeFlagInjective 
SafeFlagEta

ETA pragma is unsafe.

ParseWarning ParseWarning 
LibraryWarning LibWarning 
DeprecationWarning String String String

`DeprecationWarning old new version`: old is deprecated, use new instead. This will be an error in Agda version.

UserWarning String

User-defined warning (e.g. to mention that a name is deprecated)

FixityInRenamingModule (NonEmpty Range)

Fixity of modules cannot be changed via renaming (since modules have no fixity).

ModuleDoesntExport QName [ImportedName]

Some imported names are not actually exported by the source module

InfectiveImport String ModuleName

Importing a file using an infective option into one which doesn't

CoInfectiveImport String ModuleName

Importing a file not using a coinfective option from one which does

RewriteNonConfluent Term Term Term Doc

Confluence checker found critical pair and equality checking resulted in a type error

RewriteMaybeNonConfluent Term Term [Doc]

Confluence checker got stuck on computing overlap between two rewrite rules

PragmaCompileErased BackendName QName

COMPILE directive for an erased symbol

NotInScopeW [QName]

Out of scope error we can recover from

Instances
Data Warning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Warning -> c Warning #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Warning #

toConstr :: Warning -> Constr #

dataTypeOf :: Warning -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Warning) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Warning) #

gmapT :: (forall b. Data b => b -> b) -> Warning -> Warning #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Warning -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Warning -> r #

gmapQ :: (forall d. Data d => d -> u) -> Warning -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Warning -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Warning -> m Warning #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Warning -> m Warning #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Warning -> m Warning #

Show Warning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj Warning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

PrettyTCM Warning Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Warning

Methods

prettyTCM :: MonadPretty m => Warning -> m Doc Source #

class (Applicative tcm, MonadIO tcm, MonadTCEnv tcm, MonadTCState tcm, HasOptions tcm) => MonadTCM tcm where Source #

Embedding a TCM computation.

Minimal complete definition

Nothing

Methods

liftTCM :: TCM a -> tcm a Source #

liftTCM :: (MonadTCM m, MonadTrans t, tcm ~ t m) => TCM a -> tcm a Source #

Instances
MonadTCM TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

liftTCM :: TCM a -> TerM a Source #

MonadTCM tcm => MonadTCM (MaybeT tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> MaybeT tcm a Source #

MonadTCM tcm => MonadTCM (ListT tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ListT tcm a Source #

MonadIO m => MonadTCM (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> TCMT m a Source #

MonadTCM tcm => MonadTCM (ChangeT tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ChangeT tcm a Source #

MonadTCM m => MonadTCM (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

liftTCM :: TCM a -> NamesT m a Source #

MonadTCM tcm => MonadTCM (ExceptT err tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ExceptT err tcm a Source #

MonadTCM tcm => MonadTCM (IdentityT tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> IdentityT tcm a Source #

MonadTCM tcm => MonadTCM (StateT s tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> StateT s tcm a Source #

(Monoid w, MonadTCM tcm) => MonadTCM (WriterT w tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> WriterT w tcm a Source #

MonadTCM tcm => MonadTCM (ReaderT r tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ReaderT r tcm a Source #

type IM = TCMT (InputT IO) Source #

Interaction monad.

class Monad m => MonadTCState m where Source #

MonadTCState made into its own dedicated service class. This allows us to use MonadState for StateT extensions of TCM.

Minimal complete definition

getTC, (putTC | modifyTC)

Methods

getTC :: m TCState Source #

putTC :: TCState -> m () Source #

modifyTC :: (TCState -> TCState) -> m () Source #

Instances
MonadTCState TerM Source # 
Instance details

Defined in Agda.Termination.Monad

MonadTCState m => MonadTCState (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadTCState m => MonadTCState (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadIO m => MonadTCState (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadTCState m => MonadTCState (ChangeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadTCState m => MonadTCState (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

MonadTCState m => MonadTCState (ExceptT err m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTC :: ExceptT err m TCState Source #

putTC :: TCState -> ExceptT err m () Source #

modifyTC :: (TCState -> TCState) -> ExceptT err m () Source #

MonadTCState m => MonadTCState (IdentityT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadTCState m => MonadTCState (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTC :: StateT s m TCState Source #

putTC :: TCState -> StateT s m () Source #

modifyTC :: (TCState -> TCState) -> StateT s m () Source #

(Monoid w, MonadTCState m) => MonadTCState (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadTCState m => MonadTCState (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

class Monad m => MonadTCEnv m where Source #

MonadTCEnv made into its own dedicated service class. This allows u