Agda-2.6.1.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

Instances details
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

Instances details
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 :: forall r r'. (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

Instances details
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 :: forall r r'. (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

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

ToJSON ProblemId 
Instance details

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: ProblemId -> Value

toEncoding :: ProblemId -> Encoding

toJSONList :: [ProblemId] -> Value

toEncodingList :: [ProblemId] -> Encoding

EncodeTCM ProblemId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: ProblemId -> TCM Value Source #

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

Defined in Agda.TypeChecking.Conversion.Pure

data Comparison Source #

Constructors

CmpEq 
CmpLeq 

Instances

Instances details
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 :: forall r r'. (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

Instances details
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 #

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

Instances details
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

Instances details
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 :: forall r r'. (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

Instances details
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 :: forall r r'. (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

Instances details
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 :: forall r r'. (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

Instances details
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

Instances details
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 :: forall r r'. (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 #

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

Instances

Instances details
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 (ReaderT r tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ReaderT r 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 #

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

Instances details
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 (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

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

class Monad m => MonadTCEnv m where Source #

MonadTCEnv made into its own dedicated service class. This allows us to use MonadReader for ReaderT extensions of TCM.

Methods

askTC :: m TCEnv Source #

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

Instances

Instances details
MonadTCEnv ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadTCEnv AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

MonadTCEnv TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

askTC :: TerM TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> TerM a -> TerM a Source #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: MaybeT m TCEnv Source #

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: ListT m TCEnv Source #

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

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 #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: ChangeT m TCEnv Source #

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

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

Defined in Agda.TypeChecking.Names

Methods

askTC :: NamesT m TCEnv Source #

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

MonadTCEnv m => MonadTCEnv (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

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

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: ExceptT err m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> ExceptT err m a -> ExceptT err m a Source #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: ReaderT r m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> ReaderT r m a -> ReaderT r m a Source #

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: StateT s m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> StateT s m a -> StateT s m a Source #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: WriterT w m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> WriterT w m a -> WriterT w m a Source #

class (Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) => MonadReduce m where Source #

Methods

liftReduce :: ReduceM a -> m a Source #

Instances

Instances details
MonadReduce ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ReduceM a Source #

MonadReduce TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

liftReduce :: ReduceM a -> TerM a Source #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ListT 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 #

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

Defined in Agda.TypeChecking.Names

Methods

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

MonadReduce m => MonadReduce (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

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

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ExceptT err m a Source #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ReaderT r m a Source #

MonadReduce m => MonadReduce (StateT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> StateT w m a Source #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> WriterT w m a Source #

newtype ReduceM a Source #

Constructors

ReduceM 

Fields

Instances

Instances details
Monad ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(>>=) :: ReduceM a -> (a -> ReduceM b) -> ReduceM b #

(>>) :: ReduceM a -> ReduceM b -> ReduceM b #

return :: a -> ReduceM a #

Functor ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> ReduceM a -> ReduceM b #

(<$) :: a -> ReduceM b -> ReduceM a #

MonadFail ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fail :: String -> ReduceM a #

Applicative ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pure :: a -> ReduceM a #

(<*>) :: ReduceM (a -> b) -> ReduceM a -> ReduceM b #

liftA2 :: (a -> b -> c) -> ReduceM a -> ReduceM b -> ReduceM c #

(*>) :: ReduceM a -> ReduceM b -> ReduceM b #

(<*) :: ReduceM a -> ReduceM b -> ReduceM a #

MonadTCEnv ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadReduce ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ReduceM a Source #

HasOptions ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

ReadTCState ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadAddContext ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

HasBuiltins ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

MonadDebug ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

HasConstInfo ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

data ReduceEnv Source #

Environment of the reduce monad.

Constructors

ReduceEnv 

Fields

class (Functor m, Applicative m, Monad m) => HasOptions m where Source #

Minimal complete definition

Nothing

Methods

pragmaOptions :: m PragmaOptions Source #

Returns the pragma options which are currently in effect.

default pragmaOptions :: (HasOptions n, MonadTrans t, m ~ t n) => m PragmaOptions Source #

commandLineOptions :: m CommandLineOptions Source #

Returns the command line options which are currently in effect.

Instances

Instances details
HasOptions ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasOptions AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

HasOptions TerM Source # 
Instance details

Defined in Agda.Termination.Monad

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Names

HasOptions m => HasOptions (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

HasOptions m => HasOptions (ExceptT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

data LHSOrPatSyn Source #

Distinguish error message when parsing lhs or pattern synonym, resp.

Constructors

IsLHS 
IsPatSyn 

Instances

Instances details
Eq LHSOrPatSyn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show LHSOrPatSyn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data TypeError Source #

Constructors

InternalError String 
NotImplemented String 
NotSupported String 
CompilationError String 
PropMustBeSingleton 
DataMustEndInSort Term 
ShouldEndInApplicationOfTheDatatype Type

The target of a constructor isn't an application of its datatype. The Type records what it does target.

ShouldBeAppliedToTheDatatypeParameters Term Term

The target of a constructor isn't its datatype applied to something that isn't the parameters. First term is the correct target and the second term is the actual target.

ShouldBeApplicationOf Type QName

Expected a type to be an application of a particular datatype.

ConstructorPatternInWrongDatatype QName QName

constructor, datatype

CantResolveOverloadedConstructorsTargetingSameDatatype QName [QName]

Datatype, constructors.

DoesNotConstructAnElementOf QName Type

constructor, type

WrongHidingInLHS

The left hand side of a function definition has a hidden argument where a non-hidden was expected.

WrongHidingInLambda Type

Expected a non-hidden function and found a hidden lambda.

WrongHidingInApplication Type

A function is applied to a hidden argument where a non-hidden was expected.

WrongNamedArgument (NamedArg Expr) [NamedName]

A function is applied to a hidden named argument it does not have. The list contains names of possible hidden arguments at this point.

WrongIrrelevanceInLambda

Wrong user-given relevance annotation in lambda.

WrongQuantityInLambda

Wrong user-given quantity annotation in lambda.

WrongCohesionInLambda

Wrong user-given cohesion annotation in lambda.

QuantityMismatch Quantity Quantity

The given quantity does not correspond to the expected quantity.

HidingMismatch Hiding Hiding

The given hiding does not correspond to the expected hiding.

RelevanceMismatch Relevance Relevance

The given relevance does not correspond to the expected relevane.

UninstantiatedDotPattern Expr 
ForcedConstructorNotInstantiated Pattern 
IlltypedPattern Pattern Type 
IllformedProjectionPattern Pattern 
CannotEliminateWithPattern (NamedArg Pattern) Type 
WrongNumberOfConstructorArguments QName Nat Nat 
ShouldBeEmpty Type [DeBruijnPattern] 
ShouldBeASort Type

The given type should have been a sort.

ShouldBePi Type

The given type should have been a pi.

ShouldBePath Type 
ShouldBeRecordType Type 
ShouldBeRecordPattern DeBruijnPattern 
NotAProjectionPattern (NamedArg Pattern) 
NotAProperTerm 
InvalidTypeSort Sort

This sort is not a type expression.

InvalidType Term

This term is not a type expression.

FunctionTypeInSizeUniv Term

This term, a function type constructor, lives in SizeUniv, which is not allowed.

SplitOnIrrelevant (Dom Type) 
SplitOnUnusableCohesion (Dom Type) 
SplitOnNonVariable Term Type 
DefinitionIsIrrelevant QName 
DefinitionIsErased QName 
VariableIsIrrelevant Name 
VariableIsErased Name 
VariableIsOfUnusableCohesion Name Cohesion 
UnequalLevel Comparison Level Level 
UnequalTerms Comparison Term Term CompareAs 
UnequalTypes Comparison Type Type 
UnequalRelevance Comparison Term Term

The two function types have different relevance.

UnequalQuantity Comparison Term Term

The two function types have different relevance.

UnequalCohesion Comparison Term Term

The two function types have different cohesion.

UnequalHiding Term Term

The two function types have different hiding.

UnequalSorts Sort Sort 
UnequalBecauseOfUniverseConflict Comparison Term Term 
NotLeqSort Sort Sort 
MetaCannotDependOn MetaId Nat

The arguments are the meta variable and the parameter that it wants to depend on.

MetaOccursInItself MetaId 
MetaIrrelevantSolution MetaId Term 
MetaErasedSolution MetaId Term 
GenericError String 
GenericDocError Doc 
BuiltinMustBeConstructor String Expr 
NoSuchBuiltinName String 
DuplicateBuiltinBinding String Term Term 
NoBindingForBuiltin String 
NoSuchPrimitiveFunction String 
DuplicatePrimitiveBinding String QName QName 
ShadowedModule Name [ModuleName] 
BuiltinInParameterisedModule String 
IllegalLetInTelescope TypedBinding 
IllegalPatternInTelescope Binder 
NoRHSRequiresAbsurdPattern [NamedArg Pattern] 
TooManyFields QName [Name] [Name]

Record type, fields not supplied by user, non-fields not supplied.

DuplicateFields [Name] 
DuplicateConstructors [Name] 
WithOnFreeVariable Expr Term 
UnexpectedWithPatterns [Pattern] 
WithClausePatternMismatch Pattern (NamedArg DeBruijnPattern) 
FieldOutsideRecord 
ModuleArityMismatch ModuleName Telescope [NamedArg Expr] 
GeneralizeCyclicDependency 
GeneralizeUnsolvedMeta 
SplitError SplitError 
ImpossibleConstructor QName NegativeUnification 
TooManyPolarities QName Int 
LocalVsImportedModuleClash ModuleName 
SolvedButOpenHoles

Some interaction points (holes) have not been filled by user. There are not UnsolvedMetas since unification solved them. This is an error, since interaction points are never filled without user interaction.

CyclicModuleDependency [TopLevelModuleName] 
FileNotFound TopLevelModuleName [AbsolutePath] 
OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName 
AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath] 
ModuleNameUnexpected TopLevelModuleName TopLevelModuleName

Found module name, expected module name.

ModuleNameDoesntMatchFileName TopLevelModuleName [AbsolutePath] 
ClashingFileNamesFor ModuleName [AbsolutePath] 
ModuleDefinedInOtherFile TopLevelModuleName AbsolutePath AbsolutePath

Module name, file from which it was loaded, file which the include path says contains the module. Scope errors

BothWithAndRHS 
AbstractConstructorNotInScope QName 
NotInScope [QName] 
NoSuchModule QName 
AmbiguousName QName (NonEmpty QName) 
AmbiguousModule QName (NonEmpty ModuleName) 
ClashingDefinition QName QName 
ClashingModule ModuleName ModuleName 
ClashingImport Name QName 
ClashingModuleImport Name ModuleName 
PatternShadowsConstructor Name QName 
DuplicateImports QName [ImportedName] 
InvalidPattern Pattern 
RepeatedVariablesInPattern [Name] 
GeneralizeNotSupportedHere QName 
MultipleFixityDecls [(Name, [Fixity'])] 
MultiplePolarityPragmas [Name] 
NotAModuleExpr Expr

The expr was used in the right hand side of an implicit module definition, but it wasn't of the form m Delta.

NotAnExpression Expr 
NotAValidLetBinding NiceDeclaration 
NotValidBeforeField NiceDeclaration 
NothingAppliedToHiddenArg Expr 
NothingAppliedToInstanceArg Expr 
BadArgumentsToPatternSynonym AmbiguousQName 
TooFewArgumentsToPatternSynonym AmbiguousQName 
CannotResolveAmbiguousPatternSynonym (NonEmpty (QName, PatternSynDefn)) 
UnusedVariableInPatternSynonym 
NoParseForApplication [Expr] 
AmbiguousParseForApplication [Expr] [Expr] 
NoParseForLHS LHSOrPatSyn Pattern 
AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern] 
OperatorInformation [NotationSection] TypeError 
InstanceNoCandidate Type [(Term, TCErr)] 
UnquoteFailed UnquoteError 
DeBruijnIndexOutOfScope Nat Telescope [Name] 
NeedOptionCopatterns 
NeedOptionRewriting 
NeedOptionProp 
NonFatalErrors [TCWarning] 
InstanceSearchDepthExhausted Term Type Int 
TriedToCopyConstrainedPrim QName 

Instances

Instances details
Show TypeError Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM TypeError Source # 
Instance details

Defined in Agda.TypeChecking.Errors

data UnificationFailure Source #

Constructors

UnifyIndicesNotVars Telescope Type Term Term Args

Failed to apply injectivity to constructor of indexed datatype

UnifyRecursiveEq Telescope Type Int Term

Can't solve equation because variable occurs in (type of) lhs

UnifyReflexiveEq Telescope Type Term

Can't solve reflexive equation because --without-K is enabled

UnifyUnusableModality Telescope Type Int Term Modality

Can't solve equation because solution modality is less "usable"

data SplitError Source #

Error when splitting a pattern variable into possible constructor patterns.

Constructors

NotADatatype (Closure Type)

Neither data type nor record.

IrrelevantDatatype (Closure Type)

Data type, but in irrelevant position.

ErasedDatatype Bool (Closure Type)

Data type, but in erased position. If the boolean is True, then the reason for the error is that the K rule is turned off.

CoinductiveDatatype (Closure Type)

Split on codata not allowed. UNUSED, but keep! -- | NoRecordConstructor Type -- ^ record type, but no constructor

UnificationStuck 

Fields

CosplitCatchall

Copattern split with a catchall

CosplitNoTarget

We do not know the target type of the clause.

CosplitNoRecordType (Closure Type)

Target type is not a record type.

CannotCreateMissingClause QName (Telescope, [NamedArg DeBruijnPattern]) Doc (Closure (Abs Type)) 
GenericSplitError String 

Instances

Instances details
Show SplitError Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM SplitError Source # 
Instance details

Defined in Agda.TypeChecking.Errors

data TerminationError Source #

Information about a mutual block which did not pass the termination checker.

Constructors

TerminationError 

Fields

Instances

Instances details
Data TerminationError 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) -> TerminationError -> c TerminationError #

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

toConstr :: TerminationError -> Constr #

dataTypeOf :: TerminationError -> DataType #

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

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

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

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

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

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

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

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

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

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

Show TerminationError Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data CallInfo Source #

Information about a call.

Constructors

CallInfo 

Fields

Instances

Instances details
Data CallInfo 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) -> CallInfo -> c CallInfo #

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

toConstr :: CallInfo -> Constr #

dataTypeOf :: CallInfo -> DataType #

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

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

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

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

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

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

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

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

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

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

Show CallInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty CallInfo Source #

We only show the name of the callee.

Instance details

Defined in Agda.TypeChecking.Monad.Base

AllNames CallInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM CallInfo Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Call

data Candidate Source #

A candidate solution for an instance meta is a term with its type. It may be the case that the candidate is not fully applied yet or of the wrong type, hence the need for the type.

Instances

Instances details
Eq Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Data Candidate 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) -> Candidate -> c Candidate #

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

toConstr :: Candidate -> Constr #

dataTypeOf :: Candidate -> DataType #

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

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

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

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

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

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

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

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

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

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

Show Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freeVars' :: IsVarSet a c => Candidate -> FreeM a c Source #

InstantiateFull Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Subst Term Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data ExpandHidden Source #

Constructors

ExpandLast

Add implicit arguments in the end until type is no longer hidden Pi.

DontExpandLast

Do not append implicit arguments.

ReallyDontExpandLast

Makes doExpandLast have no effect. Used to avoid implicit insertion of arguments to metavariables.

Instances

Instances details
Eq ExpandHidden Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data ExpandHidden 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) -> ExpandHidden -> c ExpandHidden #

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

toConstr :: ExpandHidden -> Constr #

dataTypeOf :: ExpandHidden -> DataType #

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

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

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

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

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

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

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

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

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

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

data AbstractMode Source #

Constructors

AbstractMode

Abstract things in the current module can be accessed.

ConcreteMode

No abstract things can be accessed.

IgnoreAbstractMode

All abstract things can be accessed.

Instances

Instances details
Eq AbstractMode Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data AbstractMode 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) -> AbstractMode -> c AbstractMode #

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

toConstr :: AbstractMode -> Constr #

dataTypeOf :: AbstractMode -> DataType #

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

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

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

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

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

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

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

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

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

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

Show AbstractMode Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

type Context = [ContextEntry] Source #

The Context is a stack of ContextEntrys.

data UnquoteFlags Source #

Constructors

UnquoteFlags 

Instances

Instances details
Data UnquoteFlags 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) -> UnquoteFlags -> c UnquoteFlags #

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

toConstr :: UnquoteFlags -> Constr #

dataTypeOf :: UnquoteFlags -> DataType #

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

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

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

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

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

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

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

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

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

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

class LensTCEnv a where Source #

Instances

Instances details
LensTCEnv TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensTCEnv (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data Builtin pf Source #

Constructors

Builtin Term 
Prim pf 

Instances

Instances details
Functor Builtin Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> Builtin a -> Builtin b #

(<$) :: a -> Builtin b -> Builtin a #

Foldable Builtin Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fold :: Monoid m => Builtin m -> m #

foldMap :: Monoid m => (a -> m) -> Builtin a -> m #

foldMap' :: Monoid m => (a -> m) -> Builtin a -> m #

foldr :: (a -> b -> b) -> b -> Builtin a -> b #

foldr' :: (a -> b -> b) -> b -> Builtin a -> b #

foldl :: (b -> a -> b) -> b -> Builtin a -> b #

foldl' :: (b -> a -> b) -> b -> Builtin a -> b #

foldr1 :: (a -> a -> a) -> Builtin a -> a #

foldl1 :: (a -> a -> a) -> Builtin a -> a #

toList :: Builtin a -> [a] #

null :: Builtin a -> Bool #

length :: Builtin a -> Int #

elem :: Eq a => a -> Builtin a -> Bool #

maximum :: Ord a => Builtin a -> a #

minimum :: Ord a => Builtin a -> a #

sum :: Num a => Builtin a -> a #

product :: Num a => Builtin a -> a #

Traversable Builtin Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

traverse :: Applicative f => (a -> f b) -> Builtin a -> f (Builtin b) #

sequenceA :: Applicative f => Builtin (f a) -> f (Builtin a) #

mapM :: Monad m => (a -> m b) -> Builtin a -> m (Builtin b) #

sequence :: Monad m => Builtin (m a) -> m (Builtin a) #

Show pf => Show (Builtin pf) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Builtin pf -> ShowS #

show :: Builtin pf -> String #

showList :: [Builtin pf] -> ShowS #

EmbPrj a => EmbPrj (Builtin a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

InstantiateFull a => InstantiateFull (Builtin a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data BuiltinDescriptor Source #

Constructors

BuiltinData (TCM Type) [String] 
BuiltinDataCons (TCM Type) 
BuiltinPrim String (Term -> TCM ()) 
BuiltinPostulate Relevance (TCM Type) 
BuiltinUnknown (Maybe (TCM Type)) (Term -> Type -> TCM ())

Builtin of any kind. Type can be checked (Just t) or inferred (Nothing). The second argument is the hook for the verification function.

type TempInstanceTable = (InstanceTable, Set QName) Source #

When typechecking something of the following form:

instance x : _ x = y

it's not yet known where to add x, so we add it to a list of unresolved instances and we'll deal with it later.

type InstanceTable = Map QName (Set QName) Source #

The instance table is a Map associating to every name of recorddata typepostulate its list of instances

data Call Source #

Instances

Instances details
Data Call 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) -> Call -> c Call #

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

toConstr :: Call -> Constr #

dataTypeOf :: Call -> DataType #

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

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

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

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

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

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

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

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

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

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

Pretty Call Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange Call Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: Call -> Range Source #

PrettyTCM Call Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Call

Methods

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

newtype MutualId Source #

Constructors

MutId Int32 

Instances

Instances details
Enum MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data MutualId 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) -> MutualId -> c MutualId #

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

toConstr :: MutualId -> Constr #

dataTypeOf :: MutualId -> DataType #

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

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

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

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

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

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

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

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

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

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

Num MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Ord MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasFresh MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

data TermHead Source #

Instances

Instances details
Eq TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data TermHead 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) -> TermHead -> c TermHead #

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

toConstr :: TermHead -> Constr #

dataTypeOf :: TermHead -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

data FunctionInverse' c Source #

Constructors

NotInjective 
Inverse (InversionMap c) 

Instances

Instances details
Functor FunctionInverse' Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> FunctionInverse' a -> FunctionInverse' b #

(<$) :: a -> FunctionInverse' b -> FunctionInverse' a #

Abstract FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

DropArgs FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.DropArgs

InstantiateFull FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Data c => Data (FunctionInverse' c) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c0 (d -> b) -> d -> c0 b) -> (forall g. g -> c0 g) -> FunctionInverse' c -> c0 (FunctionInverse' c) #

gunfold :: (forall b r. Data b => c0 (b -> r) -> c0 r) -> (forall r. r -> c0 r) -> Constr -> c0 (FunctionInverse' c) #

toConstr :: FunctionInverse' c -> Constr #

dataTypeOf :: FunctionInverse' c -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> FunctionInverse' c -> FunctionInverse' c #

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

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

gmapQ :: (forall d. Data d => d -> u) -> FunctionInverse' c -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> FunctionInverse' c -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FunctionInverse' c -> m (FunctionInverse' c) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionInverse' c -> m (FunctionInverse' c) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionInverse' c -> m (FunctionInverse' c) #

Show c => Show (FunctionInverse' c) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange c => KillRange (FunctionInverse' c) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj a => EmbPrj (FunctionInverse' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

data PrimFun Source #

Instances

Instances details
Abstract PrimFun Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply PrimFun Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data PrimitiveImpl Source #

Primitives

Constructors

PrimImpl Type PrimFun 

data AllowedReduction Source #

Controlling reduce.

Constructors

ProjectionReductions

(Projection and) projection-like functions may be reduced.

InlineReductions

Functions marked INLINE may be reduced.

CopatternReductions

Copattern definitions may be reduced.

FunctionReductions

Non-recursive functions and primitives may be reduced.

RecursiveReductions

Even recursive functions may be reduced.

LevelReductions

Reduce Level terms.

TypeLevelReductions

Allow allReductions in types, even if not allowed at term level (used by confluence checker)

UnconfirmedReductions

Functions whose termination has not (yet) been confirmed.

NonTerminatingReductions

Functions that have failed termination checking.

Instances

Instances details
Bounded AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Enum AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data AllowedReduction 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) -> AllowedReduction -> c AllowedReduction #

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

toConstr :: AllowedReduction -> Constr #

dataTypeOf :: AllowedReduction -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Ix AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data MaybeReduced a Source #

Constructors

MaybeRed 

Instances

Instances details
Functor MaybeReduced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> MaybeReduced a -> MaybeReduced b #

(<$) :: a -> MaybeReduced b -> MaybeReduced a #

IsProjElim e => IsProjElim (MaybeReduced e) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM a => PrettyTCM (MaybeReduced a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

data IsReduced Source #

Three cases: 1. not reduced, 2. reduced, but blocked, 3. reduced, not blocked.

Constructors

NotReduced 
Reduced (Blocked ()) 

data Reduced no yes Source #

Instances

Instances details
Functor (Reduced no) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> Reduced no a -> Reduced no b #

(<$) :: a -> Reduced no b -> Reduced no a #

data Simplification Source #

Did we encounter a simplifying reduction? In terms of CIC, that would be a iota-reduction. In terms of Agda, this is a constructor or literal pattern that matched. Just beta-reduction (substitution) or delta-reduction (unfolding of definitions) does not count as simplifying?

Instances

Instances details
Eq Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data Simplification 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) -> Simplification -> c Simplification #

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

toConstr :: Simplification -> Constr #

dataTypeOf :: Simplification -> DataType #

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

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

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

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

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

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

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

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

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

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

Show Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Semigroup Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Monoid Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Null Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

newtype Fields Source #

Constructors

Fields [(Name, Type)] 

Instances

Instances details
Null Fields Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data Defn Source #

Constructors

Axiom

Postulate

DataOrRecSig

Data or record type signature that doesn't yet have a definition

Fields

GeneralizableVar

Generalizable variable (introduced in generalize block)

AbstractDefn Defn

Returned by getConstInfo if definition is abstract.

Function 

Fields

Datatype 

Fields

Record 

Fields

Constructor 

Fields

Primitive

Primitive or builtin functions.

Fields

Instances

Instances details
Data Defn 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) -> Defn -> c Defn #

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

toConstr :: Defn -> Constr #

dataTypeOf :: Defn -> DataType #

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

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

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

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

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

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

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

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

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

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

Show Defn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Defn -> ShowS #

show :: Defn -> String #

showList :: [Defn] -> ShowS #

Pretty Defn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Defn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract Defn Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Defn Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Defn -> Args -> Defn Source #

applyE :: Defn -> Elims -> Defn Source #

EmbPrj Defn Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

NamesIn Defn Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Defn -> Set QName Source #

InstantiateFull Defn Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Occurs Defn Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

data CompKit Source #

Constructors

CompKit 

Instances

Instances details
Eq CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Data CompKit 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) -> CompKit -> c CompKit #

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

toConstr :: CompKit -> Constr #

dataTypeOf :: CompKit -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

NamesIn CompKit Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

data FunctionFlag Source #

Constructors

FunStatic

Should calls to this function be normalised at compile-time?

FunInline

Should calls to this function be inlined by the compiler?

FunMacro

Is this function a macro?

Instances

Instances details
Enum FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data FunctionFlag 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) -> FunctionFlag -> c FunctionFlag #

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

toConstr :: FunctionFlag -> Constr #

dataTypeOf :: FunctionFlag -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

data EtaEquality Source #

Should a record type admit eta-equality?

Constructors

Specified

User specifed 'eta-equality' or 'no-eta-equality'.

Inferred

Positivity checker inferred whether eta is safe.

Instances

Instances details
Eq EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data EtaEquality 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) -> EtaEquality -> c EtaEquality #

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

toConstr :: EtaEquality -> Constr #

dataTypeOf :: EtaEquality -> DataType #

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

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

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

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

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

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

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

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

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

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

Show EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

newtype ProjLams Source #

Abstractions to build projection function (dropping parameters).

Constructors

ProjLams 

Fields

Instances

Instances details
Data ProjLams 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) -> ProjLams -> c ProjLams #

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

toConstr :: ProjLams -> Constr #

dataTypeOf :: ProjLams -> DataType #

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

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

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

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

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

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

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

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

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

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

Show ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Null ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

data Projection Source #

Additional information for projection Functions.

Constructors

Projection 

Fields

  • projProper :: Maybe QName

    Nothing if only projection-like, Just r if record projection. The r is the name of the record type projected from. This field is updated by module application.

  • projOrig :: QName

    The original projection name (current name could be from module application).

  • projFromType :: Arg QName

    Type projected from. Original record type if projProper = Just{}. Also stores ArgInfo of the principal argument. This field is unchanged by module application.

  • projIndex :: Int

    Index of the record argument. Start counting with 1, because 0 means that it is already applied to the record value. This can happen in module instantiation, but then either the record value is var 0, or funProjection == Nothing.

  • projLams :: ProjLams

    Term t to be be applied to record parameters and record value. The parameters will be dropped. In case of a proper projection, a postfix projection application will be created: t = pars r -> r .p (Invariant: the number of abstractions equals projIndex.) In case of a projection-like function, just the function symbol is returned as Def: t = pars -> f.

Instances

Instances details
Data Projection 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) -> Projection -> c Projection #

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

toConstr :: Projection -> Constr #

dataTypeOf :: Projection -> DataType #

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

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

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

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

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

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

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

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

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

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

Show Projection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Projection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract Projection Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Projection Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj Projection Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

data ExtLamInfo Source #

Additional information for extended lambdas.

Constructors

ExtLamInfo 

Fields

  • extLamModule :: ModuleName

    For complicated reasons the scope checker decides the QName of a pattern lambda, and thus its module. We really need to decide the module during type checking though, since if the lambda appears in a refined context the module picked by the scope checker has very much the wrong parameters.

  • extLamSys :: !(Maybe System)
     

Instances

Instances details
Data ExtLamInfo 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) -> ExtLamInfo -> c ExtLamInfo #

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

toConstr :: ExtLamInfo -> Constr #

dataTypeOf :: ExtLamInfo -> DataType #

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

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

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

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

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

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

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

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

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

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

Show ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Apply ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

InstantiateFull ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data System Source #

An alternative representation of partial elements in a telescope: Γ ⊢ λ Δ. [φ₁ u₁, ... , φₙ uₙ] : Δ → PartialP (∨_ᵢ φᵢ) T see cubicaltt paper (however we do not store the type T).

Constructors

System 

Fields

  • systemTel :: Telescope

    the telescope Δ, binding vars for the clauses, Γ ⊢ Δ

  • systemClauses :: [(Face, Term)]

    a system [φ₁ u₁, ... , φₙ uₙ] where Γ, Δ ⊢ φᵢ and Γ, Δ, φᵢ ⊢ uᵢ

Instances

Instances details
Data System 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) -> System -> c System #

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

toConstr :: System -> Constr #

dataTypeOf :: System -> DataType #

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

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

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

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

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

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

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

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

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

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

Show System Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange System Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract System Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply System Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj System Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

InstantiateFull System Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reify (QNamed System) [Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type Face = [(Term, Bool)] Source #

data CompilerPragma Source #

The backends are responsible for parsing their own pragmas.

Instances

Instances details
Eq CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data CompilerPragma 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) -> CompilerPragma -> c CompilerPragma #

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

toConstr :: CompilerPragma -> Constr #

dataTypeOf :: CompilerPragma -> DataType #

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

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

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

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

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

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

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

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

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

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

Show CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange CompiledRepresentation Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

data IsForced Source #

Information about whether an argument is forced by the type of a function.

Constructors

Forced 
NotForced 

Instances

Instances details
Eq IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data IsForced 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) -> IsForced -> c IsForced #

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

toConstr :: IsForced -> Constr #

dataTypeOf :: IsForced -> DataType #

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

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

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

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

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

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

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

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

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

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

Show IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

ChooseFlex IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

data NumGeneralizableArgs Source #

Constructors

NoGeneralizableArgs 
SomeGeneralizableArgs Int

When lambda-lifting new args are generalizable if SomeGeneralizableArgs, also when the number is zero.

Instances

Instances details
Data NumGeneralizableArgs 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) -> NumGeneralizableArgs -> c NumGeneralizableArgs #

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

toConstr :: NumGeneralizableArgs -> Constr #

dataTypeOf :: NumGeneralizableArgs -> DataType #

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

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

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

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

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

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

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

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

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

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

Show NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

data Definition Source #

Constructors

Defn 

Fields

Instances

Instances details
Data Definition 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) -> Definition -> c Definition #

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

toConstr :: Definition -> Constr #

dataTypeOf :: Definition -> DataType #

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

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

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

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

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

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

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

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

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

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

Show Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Definitions Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensArgInfo Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensRelevance Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensQuantity Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensModality Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract Definition Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Definition Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj Definition Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

NamesIn Definition Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

InstantiateFull Definition Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data RewriteRule Source #

Rewrite rules can be added independently from function clauses.

Constructors

RewriteRule 

Fields

Instances

Instances details
Data RewriteRule 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) -> RewriteRule -> c RewriteRule #

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

toConstr :: RewriteRule -> Constr #

dataTypeOf :: RewriteRule -> DataType #

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

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

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

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

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

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

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

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

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

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

Show RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange RewriteRuleMap Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract RewriteRule Source #

tel ⊢ (Γ ⊢ lhs ↦ rhs : t) becomes tel, Γ ⊢ lhs ↦ rhs : t) we do not need to change lhs, rhs, and t since they live in Γ. See 'Abstract Clause'.

Instance details

Defined in Agda.TypeChecking.Substitute

Apply RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

InstantiateFull RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

GetMatchables RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Subst NLPat RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data NLPSort Source #

Constructors

PType NLPat 
PProp NLPat 
PInf 
PSizeUniv 

Instances

Instances details
Data NLPSort 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) -> NLPSort -> c NLPSort #

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

toConstr :: NLPSort -> Constr #

dataTypeOf :: NLPSort -> DataType #

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

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

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

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

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

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

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

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

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

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

Show NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

freeVars' :: IsVarSet a c => NLPSort -> FreeM a c Source #

EmbPrj NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

InstantiateFull NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

GetMatchables NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

NLPatVars NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Subst NLPat NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

NLPatToTerm NLPSort Sort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

PatternFrom () Sort NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> () -> Sort -> TCM NLPSort Source #

Match () NLPSort Sort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPSort -> Sort -> NLM () Source #

data NLPType Source #

Constructors

NLPType 

Instances

Instances details
Data NLPType 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) -> NLPType -> c NLPType #

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

toConstr :: NLPType -> Constr #

dataTypeOf :: NLPType -> DataType #

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

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

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

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

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

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

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

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

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

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

Show NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

freeVars' :: IsVarSet a c => NLPType -> FreeM a c Source #

EmbPrj NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

InstantiateFull NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

GetMatchables NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

NLPatVars NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Subst NLPat NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

NLPatToTerm NLPType Type Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

PatternFrom () Type NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> () -> Type -> TCM NLPType Source #

Match () NLPType Type Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPType -> Type -> NLM () Source #

data NLPat Source #

Non-linear (non-constructor) first-order pattern.

Constructors

PVar !Int [Arg Int]

Matches anything (modulo non-linearity) that only contains bound variables that occur in the given arguments.

PDef QName PElims

Matches f es

PLam ArgInfo (Abs NLPat)

Matches λ x → t

PPi (Dom NLPType) (Abs NLPType)

Matches (x : A) → B

PSort NLPSort

Matches a sort of the given shape.

PBoundVar !Int PElims

Matches x es where x is a lambda-bound variable

PTerm Term

Matches the term modulo β (ideally βη).

Instances

Instances details
Data NLPat 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) -> NLPat -> c NLPat #

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

toConstr :: NLPat -> Constr #

dataTypeOf :: NLPat -> DataType #

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

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

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

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

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

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

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

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

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

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

Show NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> NLPat -> ShowS #

show :: NLPat -> String #

showList :: [NLPat] -> ShowS #

KillRange NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

DeBruijn NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Free NLPat Source #

Only computes free variables that are not bound (see nlPatVars), i.e., those in a PTerm.

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

freeVars' :: IsVarSet a c => NLPat -> FreeM a c Source #

EmbPrj NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

InstantiateFull NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

GetMatchables NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

NLPatVars NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Subst NLPat RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst NLPat NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst NLPat NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst NLPat NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

NLPatToTerm NLPat Level Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

NLPatToTerm NLPat Term Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

PatternFrom () Level NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> () -> Level -> TCM NLPat Source #

PatternFrom Type Term NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Match () NLPat Level Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPat -> Level -> NLM () Source #

Match Type NLPat Term Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM () Source #

PrettyTCM (Type' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

PatternFrom (Type, Term) Elims [Elim' NLPat] Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Match (Type, Term) [Elim' NLPat] Elims Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> (Type, Term) -> [Elim' NLPat] -> Elims -> NLM () Source #

data DisplayTerm Source #

A structured presentation of a Term for reification into Syntax.

Constructors

DWithApp DisplayTerm [DisplayTerm] Elims

(f vs | ws) es. The first DisplayTerm is the parent function f with its args vs. The list of DisplayTerms are the with expressions ws. The Elims are additional arguments es (possible in case the with-application is of function type) or projections (if it is of record type).

DCon ConHead ConInfo [Arg DisplayTerm]

c vs.

DDef QName [Elim' DisplayTerm]

d vs.

DDot Term

.v.

DTerm Term

v.

Instances

Instances details
Data DisplayTerm 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) -> DisplayTerm -> c DisplayTerm #

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

toConstr :: DisplayTerm -> Constr #

dataTypeOf :: DisplayTerm -> DataType #

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

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

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

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

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

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

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

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

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

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

Show DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freeVars' :: IsVarSet a c => DisplayTerm -> FreeM a c Source #

Apply DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

NamesIn DisplayTerm Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

InstantiateFull DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

SubstWithOrigin DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

Subst Term DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Reify DisplayTerm Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

PrettyTCM (Elim' DisplayTerm) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

SubstWithOrigin (Arg DisplayTerm) Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

data DisplayForm Source #

A DisplayForm is in essence a rewrite rule q ts --> dt for a defined symbol (could be a constructor as well) q. The right hand side is a DisplayTerm which is used to reify to a more readable Syntax.

The patterns ts are just terms, but var 0 is interpreted as a hole. Each occurrence of var 0 is a new hole (pattern var). For each *occurrence* of var0 the rhs dt has a free variable. These are instantiated when matching a display form against a term q vs succeeds.

Constructors

Display 

Fields

Instances

Instances details
Data DisplayForm 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) -> DisplayForm -> c DisplayForm #

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

toConstr :: DisplayForm -> Constr #

dataTypeOf :: DisplayForm -> DataType #

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

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

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

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

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

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

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

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

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

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

Show DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freeVars' :: IsVarSet a c => DisplayForm -> FreeM a c Source #

EmbPrj DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

NamesIn DisplayForm Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

InstantiateFull DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Subst Term DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

newtype Section Source #

Constructors

Section 

Instances

Instances details
Eq Section Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data Section 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) -> Section -> c Section #

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

toConstr :: Section -> Constr #

dataTypeOf :: Section -> DataType #

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

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

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

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

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

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

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

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

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

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

Show Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Sections Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj Section Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

InstantiateFull Section Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data Signature Source #

Constructors

Sig 

Fields

Instances

Instances details
Data Signature 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) -> Signature -> c Signature #

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

toConstr :: Signature -> Constr #

dataTypeOf :: Signature -> DataType #

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

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

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

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

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

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

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

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

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

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

Show Signature Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Signature Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj Signature Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

InstantiateFull Signature Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data IPClause Source #

Which clause is an interaction point located in?

Constructors

IPClause 

Fields

IPNoClause

The interaction point is not in the rhs of a clause.

Instances

Instances details
Eq IPClause Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data IPClause 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) -> IPClause -> c IPClause #

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

toConstr :: IPClause -> Constr #

dataTypeOf :: IPClause -> DataType #

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

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

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

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

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

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

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

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

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

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

data IPBoundary' t Source #

Datatype representing a single boundary condition: x_0 = u_0, ... ,x_n = u_n ⊢ t = ?n es

Constructors

IPBoundary 

Fields

Instances

Instances details
Functor IPBoundary' Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> IPBoundary' a -> IPBoundary' b #

(<$) :: a -> IPBoundary' b -> IPBoundary' a #

Foldable IPBoundary' Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fold :: Monoid m => IPBoundary' m -> m #

foldMap :: Monoid m => (a -> m) -> IPBoundary' a -> m #

foldMap' :: Monoid m => (a -> m) -> IPBoundary' a -> m #

foldr :: (a -> b -> b) -> b -> IPBoundary' a -> b #

foldr' :: (a -> b -> b) -> b -> IPBoundary' a -> b #

foldl :: (b -> a -> b) -> b -> IPBoundary' a -> b #

foldl' :: (b -> a -> b) -> b -> IPBoundary' a -> b #

foldr1 :: (a -> a -> a) -> IPBoundary' a -> a #

foldl1 :: (a -> a -> a) -> IPBoundary' a -> a #

toList :: IPBoundary' a -> [a] #

null :: IPBoundary' a -> Bool #

length :: IPBoundary' a -> Int #

elem :: Eq a => a -> IPBoundary' a -> Bool #

maximum :: Ord a => IPBoundary' a -> a #

minimum :: Ord a => IPBoundary' a -> a #

sum :: Num a => IPBoundary' a -> a #

product :: Num a => IPBoundary' a -> a #

Traversable IPBoundary' Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

traverse :: Applicative f => (a -> f b) -> IPBoundary' a -> f (IPBoundary' b) #

sequenceA :: Applicative f => IPBoundary' (f a) -> f (IPBoundary' a) #

mapM :: Monad m => (a -> m b) -> IPBoundary' a -> m (IPBoundary' b) #

sequence :: Monad m => IPBoundary' (m a) -> m (IPBoundary' a) #

Data t => Data (IPBoundary' t) 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) -> IPBoundary' t -> c (IPBoundary' t) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (IPBoundary' t) #

toConstr :: IPBoundary' t -> Constr #

dataTypeOf :: IPBoundary' t -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> IPBoundary' t -> IPBoundary' t #

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

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

gmapQ :: (forall d. Data d => d -> u) -> IPBoundary' t -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> IPBoundary' t -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IPBoundary' t -> m (IPBoundary' t) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IPBoundary' t -> m (IPBoundary' t) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IPBoundary' t -> m (IPBoundary' t) #

Show t => Show (IPBoundary' t) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty c => Pretty (IPBoundary' c) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Normalise t => Normalise (IPBoundary' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify t => Simplify (IPBoundary' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce t => Reduce (IPBoundary' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

ToConcrete a c => ToConcrete (IPBoundary' a) (IPBoundary' c) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Reify a e => Reify (IPBoundary' a) (IPBoundary' e) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

data Overapplied Source #

Flag to indicate whether the meta is overapplied in the constraint. A meta is overapplied if it has more arguments than the size of the telescope in its creation environment (as stored in MetaInfo).

Instances

Instances details
Eq Overapplied Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data Overapplied 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) -> Overapplied -> c Overapplied #

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

toConstr :: Overapplied -> Constr #

dataTypeOf :: Overapplied -> DataType #

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

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

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

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

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

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

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

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

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

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

Show Overapplied Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

type InteractionPoints = Map InteractionId InteractionPoint Source #

Data structure managing the interaction points.

We never remove interaction points from this map, only set their ipSolved to True. (Issue #2368)

data InteractionPoint Source #

Interaction points are created by the scope checker who sets the range. The meta variable is created by the type checker and then hooked up to the interaction point.

Constructors

InteractionPoint 

Fields

Instances

Instances details
Eq InteractionPoint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

type MetaNameSuggestion = String Source #

Name suggestion for meta variable. Empty string means no suggestion.

data MetaInfo Source #

MetaInfo is cloned from one meta to the next during pruning.

Constructors

MetaInfo 

Fields

newtype MetaPriority Source #

Meta variable priority: When we have an equation between meta-variables, which one should be instantiated?

Higher value means higher priority to be instantiated.

Constructors

MetaPriority Int 

data TypeCheckingProblem Source #

Constructors

CheckExpr Comparison Expr Type 
CheckArgs ExpandHidden Range [NamedArg Expr] Type Type ([Maybe Range] -> Elims -> Type -> CheckedTarget -> TCM Term) 
CheckProjAppToKnownPrincipalArg Comparison Expr ProjOrigin (NonEmpty QName) Args Type Int Term Type 
CheckLambda Comparison (Arg ([WithHiding Name], Maybe Type)) Expr Type

(λ (xs : t₀) → e) : t This is not an instance of CheckExpr as the domain type has already been checked. For example, when checking (λ (x y : Fin _) → e) : (x : Fin n) → ? we want to postpone (λ (y : Fin n) → e) : ? where Fin n is a Type rather than an Expr.

DoQuoteTerm Comparison Term Type

Quote the given term and check type against Term

Instances

Instances details
PrettyTCM TypeCheckingProblem Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

data CheckedTarget Source #

Solving a CheckArgs constraint may or may not check the target type. If it did, it returns a handle to any unsolved constraints.

data MetaInstantiation Source #

Constructors

InstV [Arg String] Term

solved by term (abstracted over some free variables)

Open

unsolved

OpenInstance

open, to be instantiated by instance search

BlockedConst Term

solution blocked by unsolved constraints

PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool) 

Instances

Instances details
Show MetaInstantiation Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data Frozen Source #

Frozen meta variable cannot be instantiated by unification. This serves to prevent the completion of a definition by its use outside of the current block. (See issues 118, 288, 399).

Constructors

Frozen

Do not instantiate.

Instantiable 

Instances

Instances details
Eq Frozen Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Show Frozen Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data MetaVariable Source #

Constructors

MetaVar 

Fields

data GeneralizedValue Source #

The value of a generalizable variable. This is created to be a generalizable meta before checking the type to be generalized.

Instances

Instances details
Data GeneralizedValue 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) -> GeneralizedValue -> c GeneralizedValue #

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

toConstr :: GeneralizedValue -> Constr #

dataTypeOf :: GeneralizedValue -> DataType #

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

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

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

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

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

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

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

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

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

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

Show GeneralizedValue Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data DoGeneralize Source #

Instances

Instances details
Eq DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data DoGeneralize 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) -> DoGeneralize -> c DoGeneralize #

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

toConstr :: DoGeneralize -> Constr #

dataTypeOf :: DoGeneralize -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

data Judgement a Source #

Parametrized since it is used without MetaId when creating a new meta.

Constructors

HasType 

Fields

IsSort 

Fields

Instances

Instances details
Show a => Show (Judgement a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM a => PrettyTCM (Judgement a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Judgement a -> m Doc Source #

data Open a Source #

A thing tagged with the context it came from.

Constructors

OpenThing 

Instances

Instances details
Functor Open Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> Open a -> Open b #

(<$) :: a -> Open b -> Open a #

Foldable Open Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fold :: Monoid m => Open m -> m #

foldMap :: Monoid m => (a -> m) -> Open a -> m #

foldMap' :: Monoid m => (a -> m) -> Open a -> m #

foldr :: (a -> b -> b) -> b -> Open a -> b #

foldr' :: (a -> b -> b) -> b -> Open a -> b #

foldl :: (b -> a -> b) -> b -> Open a -> b #

foldl' :: (b -> a -> b) -> b -> Open a -> b #

foldr1 :: (a -> a -> a) -> Open a -> a #

foldl1 :: (a -> a -> a) -> Open a -> a #

toList :: Open a -> [a] #

null :: Open a -> Bool #

length :: Open a -> Int #

elem :: Eq a => a -> Open a -> Bool #

maximum :: Ord a => Open a -> a #

minimum :: Ord a => Open a -> a #

sum :: Num a => Open a -> a #

product :: Num a => Open a -> a #

Traversable Open Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

traverse :: Applicative f => (a -> f b) -> Open a -> f (Open b) #

sequenceA :: Applicative f => Open (f a) -> f (Open a) #

mapM :: Monad m => (a -> m b) -> Open a -> m (Open b) #

sequence :: Monad m => Open (m a) -> m (Open a) #

Decoration Open Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

traverseF :: Functor m => (a -> m b) -> Open a -> m (Open b) Source #

distributeF :: Functor m => Open (m a) -> m (Open a) Source #

Data a => Data (Open a) 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) -> Open a -> c (Open a) #

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

toConstr :: Open a -> Constr #

dataTypeOf :: Open a -> DataType #

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

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

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

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

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

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

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

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

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

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

Show a => Show (Open a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Open a -> ShowS #

show :: Open a -> String #

showList :: [Open a] -> ShowS #

KillRange a => KillRange (Open a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj a => EmbPrj (Open a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Open a -> S Int32 Source #

icod_ :: Open a -> S Int32 Source #

value :: Int32 -> R (Open a) Source #

NamesIn a => NamesIn (Open a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Open a -> Set QName Source #

InstantiateFull t => InstantiateFull (Open t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data CompareAs Source #

We can either compare two terms at a given type, or compare two types without knowing (or caring about) their sorts.

Constructors

AsTermsOf Type

Type should not be Size. But currently, we do not rely on this invariant.

AsSizes

Replaces AsTermsOf Size.

AsTypes 

Instances

Instances details
Eq CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Data CompareAs 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) -> CompareAs -> c CompareAs #

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

toConstr :: CompareAs -> Constr #

dataTypeOf :: CompareAs -> DataType #

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

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

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

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

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

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

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

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

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

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

Show CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freeVars' :: IsVarSet a c => CompareAs -> FreeM a c Source #

TermLike CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

traverseTermM :: Monad m => (Term -> m Term) -> CompareAs -> m CompareAs Source #

foldTerm :: Monoid m => (Term -> m) -> CompareAs -> m Source #

PrettyTCM CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

IsSizeType CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

MentionsMeta CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> CompareAs -> Bool Source #

InstantiateFull CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

IsMeta CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Subst Term CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data Constraint Source #

Constructors

ValueCmp Comparison CompareAs Term Term 
ValueCmpOnFace Comparison Term Type Term Term 
ElimCmp [Polarity] [IsForced] Type Term [Elim] [Elim] 
TelCmp Type Type Comparison Telescope Telescope

the two types are for the error message only

SortCmp Comparison Sort Sort 
LevelCmp Comparison Level Level 
HasBiggerSort Sort 
HasPTSRule (Dom Type) (Abs Sort) 
CheckMetaInst MetaId 
UnBlock MetaId 
Guarded Constraint ProblemId 
IsEmpty Range Type

The range is the one of the absurd pattern.

CheckSizeLtSat Term

Check that the Term is either not a SIZELT or a non-empty SIZELT.

FindInstance MetaId (Maybe MetaId) (Maybe [Candidate])

the first argument is the instance argument, the second one is the meta on which the constraint may be blocked on and the third one is the list of candidates (or Nothing if we haven’t determined the list of candidates yet)

CheckFunDef Delayed DefInfo QName [Clause] 
UnquoteTactic (Maybe MetaId) Term Term Type

First argument is computation and the others are hole and goal type

Instances

Instances details
Data Constraint 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) -> Constraint -> c Constraint #

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

toConstr :: Constraint -> Constr #

dataTypeOf :: Constraint -> DataType #

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

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

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

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

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

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

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

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

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

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

Show Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freeVars' :: IsVarSet a c => Constraint -> FreeM a c Source #

TermLike Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Constraint -> m Constraint Source #

foldTerm :: Monoid m => (Term -> m) -> Constraint -> m Source #

PrettyTCM Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

MentionsMeta Constraint Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Constraint -> Bool Source #

InstantiateFull Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Subst Term Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Reify Constraint (OutputConstraint Expr Expr) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

data ProblemConstraint Source #

Instances

Instances details
Data ProblemConstraint 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) -> ProblemConstraint -> c ProblemConstraint #

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

toConstr :: ProblemConstraint -> Constr #

dataTypeOf :: ProblemConstraint -> DataType #

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

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

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

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

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

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

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

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

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

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

Show ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

MentionsMeta ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

InstantiateFull ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

class LensClosure a b | b -> a where Source #

Methods

lensClosure :: Lens' (Closure a) b Source #

data Closure a Source #

Instances

Instances details
Functor Closure Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> Closure a -> Closure b #

(<$) :: a -> Closure b -> Closure a #

Foldable Closure Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fold :: Monoid m => Closure m -> m #

foldMap :: Monoid m => (a -> m) -> Closure a -> m #

foldMap' :: Monoid m => (a -> m) -> Closure a -> m #

foldr :: (a -> b -> b) -> b -> Closure a -> b #

foldr' :: (a -> b -> b) -> b -> Closure a -> b #

foldl :: (b -> a -> b) -> b -> Closure a -> b #

foldl' :: (b -> a -> b) -> b -> Closure a -> b #

foldr1 :: (a -> a -> a) -> Closure a -> a #

foldl1 :: (a -> a -> a) -> Closure a -> a #

toList :: Closure a -> [a] #

null :: Closure a -> Bool #

length :: Closure a -> Int #

elem :: Eq a => a -> Closure a -> Bool #

maximum :: Ord a => Closure a -> a #

minimum :: Ord a => Closure a -> a #

sum :: Num a => Closure a -> a #

product :: Num a => Closure a -> a #

LensClosure a (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Data a => Data (Closure a) 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) -> Closure a -> c (Closure a) #

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

toConstr :: Closure a -> Constr #

dataTypeOf :: Closure a -> DataType #

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

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

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

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

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

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

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

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

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

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

Show a => Show (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Closure a -> ShowS #

show :: Closure a -> String #

showList :: [Closure a] -> ShowS #

KillRange a => KillRange (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange a => HasRange (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: Closure a -> Range Source #

LensIsAbstract (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensTCEnv (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM a => PrettyTCM (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Closure a -> m Doc Source #

MentionsMeta a => MentionsMeta (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Closure a -> Bool Source #

InstantiateFull a => InstantiateFull (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise a => Normalise (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify a => Simplify (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce a => Reduce (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate a => Instantiate (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data Interface Source #

Constructors

Interface 

Fields

data ModuleInfo Source #

Constructors

ModuleInfo 

Fields

class Monad m => MonadStConcreteNames m where Source #

A monad that has read and write access to the stConcreteNames part of the TCState. Basically, this is a synonym for `MonadState ConcreteNames m` (which cannot be used directly because of the limitations of Haskell's typeclass system).

Minimal complete definition

runStConcreteNames

Instances

Instances details
MonadStConcreteNames TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadStConcreteNames AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ReadTCState m => MonadStConcreteNames (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

type SourceToModule = Map AbsolutePath TopLevelModuleName Source #

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

class FreshName a where Source #

Create a fresh name from a.

Methods

freshName_ :: MonadFresh NameId m => a -> m Name Source #

Instances

Instances details
FreshName () Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freshName_ :: MonadFresh NameId m => () -> m Name Source #

FreshName String Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

FreshName Range Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

FreshName (Range, String) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

newtype CheckpointId Source #

Constructors

CheckpointId Int 

Instances

Instances details
Enum CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Integral CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data CheckpointId 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) -> CheckpointId -> c CheckpointId #

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

toConstr :: CheckpointId -> Constr #

dataTypeOf :: CheckpointId -> DataType #

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

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

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

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

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

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

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

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

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

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

Num CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Ord CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Real CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasFresh CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

class Monad m => MonadFresh i m where Source #

Methods

fresh :: m i Source #

Instances

Instances details
HasFresh i => MonadFresh i TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fresh :: TCM i Source #

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

Defined in Agda.TypeChecking.Conversion.Pure

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

Defined in Agda.TypeChecking.Conversion.Pure

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

Defined in Agda.TypeChecking.Conversion.Pure

MonadFresh i m => MonadFresh i (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fresh :: StateT s m i Source #

MonadFresh i m => MonadFresh i (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fresh :: ReaderT r m i Source #

data TypeCheckAction Source #

A complete log for a module will look like this:

type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)] Source #

Like CachedTypeCheckLog, but storing the log for an ongoing type checking of a module. Stored in reverse order (last performed action first).

type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)] Source #

A log of what the type checker does and states after the action is completed. The cached version is stored first executed action first.

data PersistentTCState Source #

A part of the state which is not reverted when an error is thrown or the state is reset.

Constructors

PersistentTCSt 

Fields

Instances

Instances details
LensPersistentVerbosity PersistentTCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensIncludePaths PersistentTCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensSafeMode PersistentTCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensCommandLineOptions PersistentTCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

data MutualBlock Source #

A mutual block of names in the signature.

Constructors

MutualBlock 

Fields

Instances

Instances details
Eq MutualBlock Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show MutualBlock Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Null MutualBlock Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data PostScopeState Source #

Constructors

PostScopeState 

Fields

data PreScopeState Source #

Constructors

PreScopeState 

Fields

class Monad m => ReadTCState m where Source #

Minimal complete definition

getTCState, locallyTCState

Methods

getTCState :: m TCState Source #

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

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

Instances

Instances details
ReadTCState ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

ReadTCState AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ReadTCState TerM Source # 
Instance details

Defined in Agda.Termination.Monad

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

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: MaybeT m TCState Source #

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

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: ListT m TCState Source #

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

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

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 #

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

Defined in Agda.TypeChecking.Names

Methods

getTCState :: NamesT m TCState Source #

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

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

ReadTCState m => ReadTCState (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

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

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: ExceptT err m TCState Source #

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

withTCState :: (TCState -> TCState) -> ExceptT err m a -> ExceptT err m a Source #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: ReaderT r m TCState Source #

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

withTCState :: (TCState -> TCState) -> ReaderT r m a -> ReaderT r m a Source #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: StateT s m TCState Source #

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

withTCState :: (TCState -> TCState) -> StateT s m a -> StateT s m a Source #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: WriterT w m TCState Source #

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

withTCState :: (TCState -> TCState) -> WriterT w m a -> WriterT w m a Source #

initPersistentState :: PersistentTCState Source #

Empty persistent state.

initPreScopeState :: PreScopeState Source #

Empty state of type checker.

sourceToModule :: TCM SourceToModule Source #

Creates a SourceToModule map based on stModuleToSource.

O(n log n).

For a single reverse lookup in stModuleToSource, rather use lookupModuleFromSourse.

iFullHash :: Interface -> Hash Source #

Combines the source hash and the (full) hashes of the imported modules.

flipCmp :: CompareDirection -> CompareDirection Source #

Flip the direction of comparison.

dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c Source #

Turn a Comparison function into a CompareDirection function.

Property: dirToCmp f (fromCmp cmp) = f cmp

defaultDisplayForm :: QName -> [LocalDisplayForm] Source #

By default, we have no display form.

defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition Source #

Create a definition with sensible defaults.

projDropPars :: Projection -> ProjOrigin -> Term Source #

Building the projection function (which drops the parameters).

projArgInfo :: Projection -> ArgInfo Source #

The info of the principal (record) argument.

setEtaEquality :: EtaEquality -> HasEta -> EtaEquality Source #

Make sure we do not overwrite a user specification.

recRecursive :: Defn -> Bool Source #

Is the record type recursive?

emptyFunction :: Defn Source #

A template for creating Function definitions, with sensible defaults.

isEmptyFunction :: Defn -> Bool Source #

Checking whether we are dealing with a function yet to be defined.

redBind :: ReduceM (Reduced a a') -> (a -> b) -> (a' -> ReduceM (Reduced b b')) -> ReduceM (Reduced b b') Source #

Conceptually: redBind m f k = either (return . Left . f) k =<< m

allReductions :: AllowedReductions Source #

Not quite all reductions (skip non-terminating reductions)

defDelayed :: Definition -> Delayed Source #

Are the clauses of this definition delayed?

defNonterminating :: Definition -> Bool Source #

Has the definition failed the termination checker?

defTerminationUnconfirmed :: Definition -> Bool Source #

Has the definition not termination checked or did the check fail?

ifTopLevelAndHighlightingLevelIsOr :: MonadTCM tcm => HighlightingLevel -> Bool -> tcm () -> tcm () Source #

ifTopLevelAndHighlightingLevelIs l b m runs m when we're type-checking the top-level module and either the highlighting level is at least l or b is True.

ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm () Source #

ifTopLevelAndHighlightingLevelIs l m runs m when we're type-checking the top-level module and the highlighting level is at least l.

getIncludeDirs :: HasOptions m => m [AbsolutePath] Source #

Gets the include directories.

Precondition: optAbsoluteIncludePaths must be nonempty (i.e. setCommandLineOptions must have run).

fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b Source #

apReduce :: ReduceM (a -> b) -> ReduceM a -> ReduceM b Source #

bindReduce :: ReduceM a -> (a -> ReduceM b) -> ReduceM b Source #

runReduceF :: (a -> ReduceM b) -> TCM (a -> b) Source #

asksTC :: MonadTCEnv m => (TCEnv -> a) -> m a Source #

viewTC :: MonadTCEnv m => Lens' a TCEnv -> m a Source #

locallyTC :: MonadTCEnv m => Lens' a TCEnv -> (a -> a) -> m b -> m b Source #

Modify the lens-indicated part of the TCEnv in a subcomputation.

getsTC :: ReadTCState m => (TCState -> a) -> m a Source #

modifyTC' :: MonadTCState m => (TCState -> TCState) -> m () Source #

A variant of modifyTC in which the computation is strict in the new state.

setTCLens :: MonadTCState m => Lens' a TCState -> a -> m () infix 4 Source #

Overwrite the part of the TCState focused on by the lens.

modifyTCLens :: MonadTCState m => Lens' a TCState -> (a -> a) -> m () Source #

Modify the part of the TCState focused on by the lens.

modifyTCLensM :: MonadTCState m => Lens' a TCState -> (a -> m a) -> m () Source #

Modify a part of the state monadically.

stateTCLens :: MonadTCState m => Lens' a TCState -> (a -> (r, a)) -> m r Source #

Modify the part of the TCState focused on by the lens, and return some result.

stateTCLensM :: MonadTCState m => Lens' a TCState -> (a -> m (r, a)) -> m r Source #

Modify a part of the state monadically, and return some result.

mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a Source #

pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a Source #

returnTCMT :: MonadIO m => a -> TCMT m a Source #

bindTCMT :: MonadIO m => TCMT m a -> (a -> TCMT m b) -> TCMT m b Source #

thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m b Source #

fmapTCMT :: MonadIO m => (a -> b) -> TCMT m a -> TCMT m b Source #

apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m b Source #

runIM :: IM a -> TCM a Source #

catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a Source #

Preserve the state of the failing computation.

finally_ :: TCM a -> TCM b -> TCM a Source #

Execute a finalizer even when an exception is thrown. Does not catch any errors. In case both the regular computation and the finalizer throw an exception, the one of the finalizer is propagated.

internalError :: MonadTCM tcm => String -> tcm a Source #

runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState) Source #

Running the type checking monad (most general form).

runTCMTop :: TCM a -> IO (Either TCErr a) Source #

Running the type checking monad on toplevel (with initial state).

runTCMTop' :: MonadIO m => TCMT m a -> m a Source #

runSafeTCM :: TCM a -> TCState -> IO (a, TCState) Source #

runSafeTCM runs a safe TCM action (a TCM action which cannot fail) in the initial environment.

forkTCM :: TCM a -> TCM () Source #

Runs the given computation in a separate thread, with a copy of the current state and environment.

Note that Agda sometimes uses actual, mutable state. If the computation given to forkTCM tries to modify this state, then bad things can happen, because accesses are not mutually exclusive. The forkTCM function has been added mainly to allow the thread to read (a snapshot of) the current state in a convenient way.

Note also that exceptions which are raised in the thread are not propagated to the parent, so the thread should not do anything important.

patternInTeleName :: String Source #

Base name for patterns in telescopes

extendedLambdaName :: String Source #

Base name for extended lambda patterns

isExtendedLambdaName :: QName -> Bool Source #

Check whether we have an definition from an extended lambda.

absurdLambdaName :: String Source #

Name of absurdLambda definitions.

isAbsurdLambdaName :: QName -> Bool Source #

Check whether we have an definition from an absurd lambda.

generalizedFieldName :: String Source #

Base name for generalized variable projections

getGeneralizedFieldName :: QName -> Maybe String Source #

Check whether we have a generalized variable field

checkForImportCycle :: TCM () Source #

Assumes that the first module in the import path is the module we are worried about.

currentModule :: MonadTCEnv m => m ModuleName Source #

Get the name of the current module, if any.

withCurrentModule :: MonadTCEnv m => ModuleName -> m a -> m a Source #

Set the name of the current module.

getCurrentPath :: MonadTCEnv m => m AbsolutePath Source #

Get the path of the currently checked file

getAnonymousVariables :: MonadTCEnv m => ModuleName -> m Nat Source #

Get the number of variables bound by anonymous modules.

withAnonymousModule :: ModuleName -> Nat -> TCM a -> TCM a Source #

Add variables bound by an anonymous module.

withEnv :: MonadTCEnv m => TCEnv -> m a -> m a Source #

Set the current environment to the given

getEnv :: TCM TCEnv Source #

Get the current environment

withIncreasedModuleNestingLevel :: TCM a -> TCM a Source #

Increases the module nesting level by one in the given computation.

withHighlightingLevel :: HighlightingLevel -> TCM a -> TCM a Source #

Set highlighting level

doExpandLast :: TCM a -> TCM a Source #

Restore setting for ExpandLast to default.

performedSimplification :: MonadTCEnv m => m a -> m a Source #

If the reduced did a proper match (constructor or literal pattern), then record this as simplification step.

onlyReduceProjections :: MonadTCEnv m => m a -> m a Source #

Reduce Def f vs only if f is a projection.

allowAllReductions :: MonadTCEnv m => m a -> m a Source #

Allow all reductions except for non-terminating functions (default).

allowNonTerminatingReductions :: MonadTCEnv m => m a -> m a Source #

Allow all reductions including non-terminating functions.

onlyReduceTypes :: MonadTCEnv m => m a -> m a Source #

Allow all reductions when reducing types

typeLevelReductions :: MonadTCEnv m => m a -> m a Source #

Update allowed reductions when working on types

callByName :: TCM a -> TCM a Source #

Don't use call-by-need evaluation for the given computation.

class MonadTCEnv m => MonadAddContext m where Source #

Methods

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

addCtx x arg cont add a variable to the context.

Chooses an unused Name.

Warning: Does not update module parameter substitution!

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

Add a let bound variable to the context

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

Update the context. Requires a substitution that transports things living in the old context to the new.

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

Instances

Instances details
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 #

MonadAddContext ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

MonadAddContext TerM Source # 
Instance details

Defined in Agda.Termination.Monad

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> MaybeT m a -> MaybeT m a Source #

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

updateContext :: Substitution -> (Context -> Context) -> MaybeT m a -> MaybeT m a Source #

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

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> ListT m a -> ListT m a Source #

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

updateContext :: Substitution -> (Context -> Context) -> ListT m a -> ListT m a Source #

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

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

Defined in Agda.TypeChecking.Names

Methods

addCtx :: Name -> Dom Type -> NamesT m a -> NamesT m a Source #

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

updateContext :: Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a Source #

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

MonadAddContext m => MonadAddContext (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadAddContext m => MonadAddContext (ExceptT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> ExceptT e m a -> ExceptT e m a Source #

addLetBinding' :: Name -> Term -> Dom Type -> ExceptT e m a -> ExceptT e m a Source #

updateContext :: Substitution -> (Context -> Context) -> ExceptT e m a -> ExceptT e m a Source #

withFreshName :: Range -> ArgName -> (Name -> ExceptT e m a) -> ExceptT e m a Source #

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> ReaderT r m a -> ReaderT r m a Source #

addLetBinding' :: Name -> Term -> Dom Type -> ReaderT r m a -> ReaderT r m a Source #

updateContext :: Substitution -> (Context -> Context) -> ReaderT r m a -> ReaderT r m a Source #

withFreshName :: Range -> ArgName -> (Name -> ReaderT r m a) -> ReaderT r m a Source #

MonadAddContext m => MonadAddContext (StateT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> StateT r m a -> StateT r m a Source #

addLetBinding' :: Name -> Term -> Dom Type -> StateT r m a -> StateT r m a Source #

updateContext :: Substitution -> (Context -> Context) -> StateT r m a -> StateT r m a Source #

withFreshName :: Range -> ArgName -> (Name -> StateT r m a) -> StateT r m a Source #

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> WriterT w m a -> WriterT w m a Source #

addLetBinding' :: Name -> Term -> Dom Type -> WriterT w m a -> WriterT w m a Source #

updateContext :: Substitution -> (Context -> Context) -> WriterT w m a -> WriterT w m a Source #

withFreshName :: Range -> ArgName -> (Name -> WriterT w m a) -> WriterT w m a Source #

checkpointSubstitution :: MonadTCEnv tcm => CheckpointId -> tcm Substitution Source #

Get the substitution from the context at a given checkpoint to the current context.

class (Functor m, Applicative m, MonadFail m) => HasBuiltins m where Source #

Instances

Instances details
HasBuiltins ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

HasBuiltins TerM Source # 
Instance details

Defined in Agda.Termination.Monad

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

Defined in Agda.TypeChecking.Monad.Builtin

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

Defined in Agda.TypeChecking.Monad.Builtin

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

Defined in Agda.TypeChecking.Monad.Builtin

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

Defined in Agda.TypeChecking.Names

HasBuiltins m => HasBuiltins (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

HasBuiltins m => HasBuiltins (ExceptT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

HasBuiltins m => HasBuiltins (ReaderT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

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

Defined in Agda.TypeChecking.Monad.Builtin

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

Defined in Agda.TypeChecking.Monad.Builtin

class TraceS a where Source #

Debug print some lines if the verbosity level for the given VerboseKey is at least VerboseLevel.

Note: In the presence of OverloadedStrings, just @ traceS key level "Literate string" gives an Ambiguous type variable error in GHC@. Use the legacy functions traceSLn and traceSDoc instead then.

Methods

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

Instances

Instances details
TraceS String Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

TraceS Doc Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

TraceS [String] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

TraceS [Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [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 #

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 #

class ReportS a where Source #

Debug print some lines if the verbosity level for the given VerboseKey is at least VerboseLevel.

Note: In the presence of OverloadedStrings, just @ reportS key level "Literate string" gives an Ambiguous type variable error in GHC@. Use the legacy functions reportSLn and reportSDoc instead then.

Methods

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

Instances

Instances details
ReportS String Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

ReportS Doc Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

ReportS [String] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

ReportS [Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [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 #

ReportS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

class (Functor m, Applicative m, Monad m) => MonadDebug m where Source #

Minimal complete definition

formatDebugMessage, verboseBracket

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> m () Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> m a -> m a Source #

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> m String Source #

getVerbosity :: m Verbosity Source #

isDebugPrinting :: m Bool Source #

nowDebugPrinting :: m a -> m a Source #

default nowDebugPrinting :: MonadTCEnv m => m a -> m a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> m a -> m a Source #

Print brackets around debug messages issued by a computation.

Instances

Instances details
MonadDebug TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

MonadDebug ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

MonadDebug AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

MonadDebug TerM Source # 
Instance details

Defined in Agda.Termination.Monad

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

Defined in Agda.TypeChecking.Monad.Debug

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

Defined in Agda.TypeChecking.Monad.Debug

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

Defined in Agda.TypeChecking.Monad.Debug

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

Defined in Agda.TypeChecking.Names

MonadDebug m => MonadDebug (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadDebug m => MonadDebug (ExceptT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

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

Defined in Agda.TypeChecking.Monad.Debug

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

Defined in Agda.TypeChecking.Monad.Debug

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

Defined in Agda.TypeChecking.Monad.Debug

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

Defined in Agda.TypeChecking.Monad.Debug

catchAndPrintImpossible :: (CatchImpossible m, Monad m) => VerboseKey -> VerboseLevel -> m String -> m String Source #

During printing, catch internal errors of kind Impossible and print them.

reportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m () Source #

Conditionally println debug string.

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

Conditionally render debug Doc and print it.

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

Debug print the result of a computation.

unlessDebugPrinting :: MonadDebug m => m () -> m () Source #

traceSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a Source #

Conditionally render debug Doc, print it, and then continue.

hasVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool Source #

Check whether a certain verbosity level is activated.

Precondition: The level must be non-negative.

hasExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool Source #

Check whether a certain verbosity level is activated (exact match).

whenExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m () Source #

Run a computation if a certain verbosity level is activated (exact match).

verboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m () Source #

Run a computation if a certain verbosity level is activated.

Precondition: The level must be non-negative.

applyWhenVerboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a Source #

Apply a function if a certain verbosity level is activated.

Precondition: The level must be non-negative.

class ReadTCState m => MonadStatistics m where Source #

Minimal complete definition

Nothing

Methods

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

default modifyCounter :: (MonadStatistics n, MonadTrans t, t n ~ m) => String -> (Integer -> Integer) -> m () Source #

Instances

Instances details
MonadStatistics TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Statistics

Methods

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

MonadStatistics TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

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

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

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> MaybeT m () Source #

ReadTCState m => MonadStatistics (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadStatistics m => MonadStatistics (ExceptT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> ExceptT e m () Source #

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

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> ReaderT r m () Source #

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

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> StateT s m () Source #

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

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> WriterT w m () Source #

getStatistics :: ReadTCState m => m Statistics Source #

Get the statistics.

modifyStatistics :: (Statistics -> Statistics) -> TCM () Source #

Modify the statistics via given function.

tick :: MonadStatistics m => String -> m () Source #

Increase specified counter by 1.

tickN :: MonadStatistics m => String -> Integer -> m () Source #

Increase specified counter by n.

tickMax :: MonadStatistics m => String -> Integer -> m () Source #

Set the specified counter to the maximum of its current value and n.

printStatistics :: (MonadDebug m, MonadTCEnv m, HasOptions m) => Int -> Maybe TopLevelModuleName -> Statistics -> m () Source #

Print the given statistics if verbosity "profile.ticks" is given.

class (Functor m, Applicative m, MonadFail m, HasOptions m, MonadDebug m, MonadTCEnv m) => HasConstInfo m where Source #

Minimal complete definition

Nothing

Methods

getConstInfo :: QName -> m Definition Source #

Lookup the definition of a name. The result is a closed thing, all free variables have been abstracted over.

getConstInfo' :: QName -> m (Either SigError Definition) Source #

Version that reports exceptions:

getRewriteRulesFor :: QName -> m RewriteRules Source #

Lookup the rewrite rules with the given head symbol.

Instances

Instances details
HasConstInfo ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

HasConstInfo TerM Source # 
Instance details

Defined in Agda.Termination.Monad

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

Defined in Agda.TypeChecking.Monad.Signature

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

Defined in Agda.TypeChecking.Monad.Signature

HasConstInfo (TCMT IO) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Signature

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

Defined in Agda.TypeChecking.Monad.Signature

HasConstInfo m => HasConstInfo (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

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

Defined in Agda.TypeChecking.Monad.Signature

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

Defined in Agda.TypeChecking.Monad.Signature

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

Defined in Agda.TypeChecking.Monad.Signature

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

Defined in Agda.TypeChecking.Monad.Signature

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

Defined in Agda.TypeChecking.Monad.Signature

data SigError Source #

Signature lookup errors.

Constructors

SigUnknown String

The name is not in the signature; default error message.

SigAbstract

The name is not available, since it is abstract.

lookupSection :: (Functor m, ReadTCState m) => ModuleName -> m Telescope Source #

Lookup a section telescope.

If it doesn't exist, like in hierarchical top-level modules, the section telescope is empty.

inFreshModuleIfFreeParams :: TCM a -> TCM a Source #

Unless all variables in the context are module parameters, create a fresh module to capture the non-module parameters. Used when unquoting to make sure generated definitions work properly.

cachingStarts :: (MonadTCState m, ReadTCState m) => m () Source #

To be called before any write or restore calls.

writeToCurrentLog :: (MonadDebug m, MonadTCState m, ReadTCState m) => TypeCheckAction -> m () Source #

Writes a TypeCheckAction to the current log, using the current PostScopeState

localCache :: (MonadTCState m, ReadTCState m) => m a -> m a Source #

Runs the action and restores the current cache at the end of it.

withoutCache :: (MonadTCState m, ReadTCState m) => m a -> m a Source #

Runs the action without cache and restores the current cache at the end of it.

readFromCachedLog :: (MonadDebug m, MonadTCState m, ReadTCState m) => m (Maybe (TypeCheckAction, PostScopeState)) Source #

Reads the next entry in the cached type check log, if present.

cleanCachedLog :: (MonadDebug m, MonadTCState m) => m () Source #

Empties the "to read" CachedState. To be used when it gets invalid.

activateLoadedFileCache :: (HasOptions m, MonadDebug m, MonadTCState m) => m () Source #

Makes sure that the stLoadedFileCache is Just, with a clean current log. Crashes is stLoadedFileCache is already active with a dirty log. Should be called when we start typechecking the current file.

cacheCurrentLog :: (MonadDebug m, MonadTCState m) => m () Source #

Caches the current type check log. Discardes the old cache. Does nothing if caching is inactive.

resetState :: TCM () Source #

Resets the non-persistent part of the type checking state.

resetAllState :: TCM () Source #

Resets all of the type checking state.

Keep only Benchmark and backend information.

localTCState :: TCM a -> TCM a Source #

Restore TCState after performing subcomputation.

In contrast to localState, the Benchmark info from the subcomputation is saved.

localTCStateSaving :: TCM a -> TCM (a, TCState) Source #

Same as localTCState but also returns the state in which we were just before reverting it.

localTCStateSavingWarnings :: TCM a -> TCM a Source #

Same as localTCState but keep all warnings.

speculateTCState :: TCM (a, SpeculateResult) -> TCM a Source #

Allow rolling back the state changes of a TCM computation.

freshTCM :: TCM a -> TCM (Either TCErr a) Source #

A fresh TCM instance.

The computation is run in a fresh state, with the exception that the persistent state is preserved. If the computation changes the state, then these changes are ignored, except for changes to the persistent state. (Changes to the persistent state are also ignored if errors other than type errors or IO exceptions are encountered.)

getScope :: ReadTCState m => m ScopeInfo Source #

Get the current scope.

setScope :: ScopeInfo -> TCM () Source #

Set the current scope.

modifyScope_ :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m () Source #

Modify the current scope without updating the inverse maps.

modifyScope :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m () Source #

Modify the current scope.

useScope :: ReadTCState m => Lens' a ScopeInfo -> m a Source #

Get a part of the current scope.

locallyScope :: ReadTCState m => Lens' a ScopeInfo -> (a -> a) -> m b -> m b Source #

Run a computation in a modified scope.

withScope :: ReadTCState m => ScopeInfo -> m a -> m (a, ScopeInfo) Source #

Run a computation in a local scope.

withScope_ :: ReadTCState m => ScopeInfo -> m a -> m a Source #

Same as withScope, but discard the scope from the computation.

localScope :: TCM a -> TCM a Source #

Discard any changes to the scope by a computation.

notInScopeError :: QName -> TCM a Source #

Scope error.

printScope :: String -> Int -> String -> TCM () Source #

Debug print the scope.

modifyGlobalDefinition :: QName -> (Definition -> Definition) -> TCM () Source #

Update a possibly imported definition. Warning: changes made to imported definitions (during type checking) will not persist outside the current module. This function is currently used to update the compiled representation of a function during compilation.

withSignature :: Signature -> TCM a -> TCM a Source #

Run some computation in a different signature, restore original signature.

setTopLevelModule :: QName -> TCM () Source #

Set the top-level module. This affects the global module id of freshly generated names.

withTopLevelModule :: QName -> TCM a -> TCM a Source #

Use a different top-level module for a computation. Used when generating names for imported modules.

getAllPatternSyns :: ReadTCState m => m PatternSynDefns Source #

Get both local and imported pattern synonyms

modifyBenchmark :: (Benchmark -> Benchmark) -> TCM () Source #

Lens modify for Benchmark.

addImportedInstances :: Signature -> TCM () Source #

Look through the signature and reconstruct the instance table.

clearAnonInstanceDefs :: TCM () Source #

Remove all instances whose type is still unresolved.

addUnknownInstance :: QName -> TCM () Source #

Add an instance whose type is still unresolved.

addNamedInstance Source #

Arguments

:: QName

Name of the instance.

-> QName

Name of the class.

-> TCM () 

Add instance to some `class'.

traceCallM :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => tcm Call -> tcm a -> tcm a Source #

traceCallCPS :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Call -> ((a -> tcm b) -> tcm b) -> (a -> tcm b) -> tcm b Source #

Reset envCall to previous value in the continuation.

Caveat: if the last traceCall did not set an interestingCall, for example, only set the Range with SetRange, we will revert to the last interesting call.

traceCall :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Call -> tcm a -> tcm a Source #

Record a function call in the trace.

traceClosureCall :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Closure Call -> tcm a -> tcm a Source #

setCurrentRange :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) => x -> tcm a -> tcm a Source #

Sets the current range (for error messages etc.) to the range of the given object, if it has a range (i.e., its range is not noRange).

highlightAsTypeChecked Source #

Arguments

:: (MonadTCM tcm, ReadTCState tcm) 
=> Range
rPre
-> Range
r
-> tcm a 
-> tcm a 

highlightAsTypeChecked rPre r m runs m and returns its result. Additionally, some code may be highlighted:

  • If r is non-empty and not a sub-range of rPre (after continuousPerLine has been applied to both): r is highlighted as being type-checked while m is running (this highlighting is removed if m completes successfully).
  • Otherwise: Highlighting is removed for rPre - r before m runs, and if m completes successfully, then rPre - r is highlighted as being type-checked.

printHighlightingInfo :: (MonadTCM tcm, ReadTCState tcm) => RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm () Source #

Lispify and print the given highlighting information.

inMutualBlock :: (MutualId -> TCM a) -> TCM a Source #

Pass the current mutual block id or create a new mutual block if we are not already inside on.

setMutualBlockInfo :: MutualId -> MutualInfo -> TCM () Source #

Set the mutual block info for a block, possibly overwriting the existing one.

insertMutualBlockInfo :: MutualId -> MutualInfo -> TCM () Source #

Set the mutual block info for a block if non-existing.

setMutualBlock :: MutualId -> QName -> TCM () Source #

Set the mutual block for a definition.

currentOrFreshMutualBlock :: TCM MutualId Source #

Get the current mutual block, if any, otherwise a fresh mutual block is returned.

mutualBlockOf :: QName -> TCM MutualId Source #

Reverse lookup of a mutual block id for a names.

enterClosure :: (MonadTCEnv m, ReadTCState m, LensClosure a c) => c -> (a -> m b) -> m b Source #

withClosure :: (MonadTCEnv m, ReadTCState m) => Closure a -> (a -> m b) -> m (Closure b) Source #

mapClosure :: (MonadTCEnv m, ReadTCState m) => (a -> m b) -> Closure a -> m (Closure b) Source #

class (MonadTCEnv m, ReadTCState m, MonadError TCErr m, HasOptions m, MonadDebug m) => MonadConstraint m where Source #

Monad service class containing methods for adding and solving constraints

Methods

addConstraint :: Constraint -> m () Source #

Unconditionally add the constraint.

addAwakeConstraint :: Constraint -> m () Source #

Add constraint as awake constraint.

catchPatternErr :: m a -> m a -> m a Source #

`catchPatternErr handle m` runs m, handling pattern violations with handle (doesn't roll back the state)

solveConstraint :: Constraint -> m () Source #

solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> m () Source #

Solve awake constraints matching the predicate. If the second argument is True solve constraints even if already isSolvingConstraints.

wakeConstraints :: (ProblemConstraint -> m Bool) -> m () Source #

stealConstraints :: ProblemId -> m () Source #

modifyAwakeConstraints :: (Constraints -> Constraints) -> m () Source #

modifySleepingConstraints :: (Constraints -> Constraints) -> m () Source #

Instances

Instances details
MonadConstraint TCM Source # 
Instance details

Defined in Agda.TypeChecking.Constraints

(MonadTCEnv m, ReadTCState m, HasOptions m, MonadDebug m) => MonadConstraint (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

getAwakeConstraints :: ReadTCState m => m Constraints Source #

Get the awake constraints

takeConstraints :: MonadConstraint m => (ProblemConstraint -> Bool) -> m Constraints Source #

Takes out all constraints matching given filter. Danger! The taken constraints need to be solved or put back at some point.

holdConstraints :: (ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a Source #

Suspend constraints matching the predicate during the execution of the second argument. Caution: held sleeping constraints will not be woken up by events that would normally trigger a wakeup call.

addConstraint' :: Constraint -> TCM () Source #

Add new a constraint

nowSolvingConstraints :: MonadTCEnv m => m a -> m a Source #

Start solving constraints

catchConstraint :: MonadConstraint m => Constraint -> m () -> m () Source #

Add constraint if the action raises a pattern violation

setPragmaOptions :: PragmaOptions -> TCM () Source #

Sets the pragma options.

setCommandLineOptions :: CommandLineOptions -> TCM () Source #

Sets the command line options (both persistent and pragma options are updated).

Relative include directories are made absolute with respect to the current working directory. If the include directories have changed (thus, they are Left now, and were previously Right something), then the state is reset (completely, see setIncludeDirs) .

An empty list of relative include directories (Left []) is interpreted as ["."].

setCommandLineOptions' Source #

Arguments

:: AbsolutePath

The base directory of relative paths.

-> CommandLineOptions 
-> TCM () 

setLibraryPaths Source #

Arguments

:: AbsolutePath

The base directory of relative paths.

-> CommandLineOptions 
-> TCM CommandLineOptions 

addDefaultLibraries Source #

Arguments

:: AbsolutePath

The base directory of relative paths.

-> CommandLineOptions 
-> TCM CommandLineOptions 

enableDisplayForms :: MonadTCEnv m => m a -> m a Source #

Disable display forms.

disableDisplayForms :: MonadTCEnv m => m a -> m a Source #

Disable display forms.

displayFormsEnabled :: MonadTCEnv m => m Bool Source #

Check if display forms are enabled.

setIncludeDirs Source #

Arguments

:: [FilePath]

New include directories.

-> AbsolutePath

The base directory of relative paths.

-> TCM () 

Makes the given directories absolute and stores them as include directories.

If the include directories change, then the state is reset (completely, except for the include directories and stInteractionOutputCallback).

An empty list is interpreted as ["."].

withShowAllArguments :: ReadTCState m => m a -> m a Source #

Switch on printing of implicit and irrelevant arguments. E.g. for reification in with-function generation.

Restores all PragmaOptions after completion. Thus, do not attempt to make persistent PragmaOptions changes in a withShowAllArguments bracket.

withPragmaOptions :: ReadTCState m => (PragmaOptions -> PragmaOptions) -> m a -> m a Source #

Change PragmaOptions for a computation and restore afterwards.

makeOpen :: MonadTCEnv m => a -> m (Open a) Source #

Create an open term in the current context.

getOpen :: (Subst Term a, MonadTCEnv m) => Open a -> m a Source #

Extract the value from an open term. The checkpoint at which it was created must be in scope.

tryGetOpen :: (Subst Term a, MonadTCEnv m) => Open a -> m (Maybe a) Source #

Extract the value from an open term. Returns Nothing if the checkpoint at which it was created is not in scope.

isClosed :: Open a -> Bool Source #

An Open is closed if it has checkpoint 0.

newtype KeepNames a Source #

Wrapper to tell addContext not to mark names as NotInScope. Used when adding a user-provided, but already type checked, telescope to the context.

Constructors

KeepNames a 

class AddContext b where Source #

Various specializations of addCtx.

Methods

addContext :: MonadAddContext m => b -> m a -> m a Source #

contextSize :: b -> Nat Source #

Instances

Instances details
AddContext String Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext Name Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Name -> m a -> m a Source #

contextSize :: Name -> Nat Source #

AddContext Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext a => AddContext [a] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => [a] -> m a0 -> m a0 Source #

contextSize :: [a] -> Nat Source #

AddContext (Dom (String, Type)) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Dom (String, Type) -> m a -> m a Source #

contextSize :: Dom (String, Type) -> Nat Source #

AddContext (Dom (Name, Type)) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Dom (Name, Type) -> m a -> m a Source #

contextSize :: Dom (Name, Type) -> Nat Source #

AddContext (Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Dom Type -> m a -> m a Source #

contextSize :: Dom Type -> Nat Source #

AddContext (KeepNames Telescope) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext ([NamedArg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source #

contextSize :: ([NamedArg Name], Type) -> Nat Source #

AddContext ([Arg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a Source #

contextSize :: ([Arg Name], Type) -> Nat Source #

AddContext ([WithHiding Name], Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext ([Name], Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([Name], Dom Type) -> m a -> m a Source #

contextSize :: ([Name], Dom Type) -> Nat Source #

AddContext (String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (String, Dom Type) -> m a -> m a Source #

contextSize :: (String, Dom Type) -> Nat Source #

AddContext (Name, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (Name, Dom Type) -> m a -> m a Source #

contextSize :: (Name, Dom Type) -> Nat Source #

AddContext (KeepNames String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

unsafeModifyContext :: MonadTCEnv tcm => (Context -> Context) -> tcm a -> tcm a Source #

Modify a Context in a computation. Warning: does not update the checkpoints. Use updateContext instead.

modifyContextInfo :: MonadTCEnv tcm => (forall e. Dom e -> Dom e) -> tcm a -> tcm a Source #

Modify the Dom part of context entries.

inTopContext :: (MonadTCEnv tcm, ReadTCState tcm) => tcm a -> tcm a Source #

Change to top (=empty) context. Resets the checkpoints.

unsafeInTopContext :: (MonadTCEnv m, ReadTCState m) => m a -> m a Source #

Change to top (=empty) context, but don't update the checkpoints. Totally not safe!

unsafeEscapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a Source #

Delete the last n bindings from the context.

Doesn't update checkpoints! Use escapeContext or `updateContext rho (drop n)` instead, for an appropriate substitution rho.

escapeContext :: MonadAddContext m => Empty -> Int -> m a -> m a Source #

Delete the last n bindings from the context. Any occurrences of these variables are replaced with the given err.

checkpoint :: (MonadDebug tcm, MonadTCM tcm, MonadFresh CheckpointId tcm, ReadTCState tcm) => Substitution -> tcm a -> tcm a Source #

Add a new checkpoint. Do not use directly!

checkpointSubstitution' :: MonadTCEnv tcm => CheckpointId -> tcm (Maybe Substitution) Source #

Get the substitution from the context at a given checkpoint to the current context.

getModuleParameterSub :: (MonadTCEnv m, ReadTCState m) => ModuleName -> m (Maybe Substitution) Source #

Get substitution Γ ⊢ ρ : Γm where Γ is the current context and Γm is the module parameter telescope of module m.

Returns Nothing in case the we don't have a checkpoint for m.

defaultAddCtx :: MonadAddContext m => Name -> Dom Type -> m a -> m a Source #

Default implementation of addCtx in terms of updateContext

withFreshName_ :: MonadAddContext m => ArgName -> (Name -> m a) -> m a Source #

withShadowingNameTCM :: Name -> TCM b -> TCM b Source #

Run the given TCM action, and register the given variable as being shadowed by all the names with the same root that are added to the context during this TCM action.

underAbstraction :: (Subst t a, MonadAddContext m) => Dom Type -> Abs a -> (a -> m b) -> m b Source #

Go under an abstraction. Do not extend context in case of NoAbs.

underAbstraction' :: (Subst t a, MonadAddContext m, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b Source #

underAbstractionAbs :: (Subst t a, MonadAddContext m) => Dom Type -> Abs a -> (a -> m b) -> m b Source #

Go under an abstraction, treating NoAbs as Abs.

underAbstractionAbs' :: (Subst t a, MonadAddContext m, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b Source #

underAbstraction_ :: (Subst t a, MonadAddContext m) => Abs a -> (a -> m b) -> m b Source #

Go under an abstract without worrying about the type to add to the context.

mapAbstraction :: (Subst t a, Subst t' b, Free b, MonadAddContext m) => Dom Type -> (a -> m b) -> Abs a -> m (Abs b) Source #

Map a monadic function on the thing under the abstraction, adding the abstracted variable to the context.

defaultAddLetBinding' :: MonadTCEnv m => Name -> Term -> Dom Type -> m a -> m a Source #

Add a let bound variable

addLetBinding :: MonadAddContext m => ArgInfo -> Name -> Term -> Type -> m a -> m a Source #

Add a let bound variable

getContext :: MonadTCEnv m => m [Dom (Name, Type)] Source #

Get the current context.

getContextSize :: (Applicative m, MonadTCEnv m) => m Nat Source #

Get the size of the current context.

getContextArgs :: (Applicative m, MonadTCEnv m) => m Args Source #

Generate [var (n - 1), ..., var 0] for all declarations in the context.

getContextTerms :: (Applicative m, MonadTCEnv m) => m [Term] Source #

Generate [var (n - 1), ..., var 0] for all declarations in the context.

getContextTelescope :: (Applicative m, MonadTCEnv m) => m Telescope Source #

Get the current context as a Telescope.

getContextNames :: (Applicative m, MonadTCEnv m) => m [Name] Source #

Get the names of all declarations in the context.

lookupBV' :: MonadTCEnv m => Nat -> m (Maybe (Dom (Name, Type))) Source #

get type of bound variable (i.e. deBruijn index)

getVarInfo :: (MonadFail m, MonadTCEnv m) => Name -> m (Term, Dom Type) Source #

Get the term corresponding to a named variable. If it is a lambda bound variable the deBruijn index is returned and if it is a let bound variable its definition is returned.

data CoinductionKit Source #

The coinductive primitives.

getTerm :: HasBuiltins m => String -> String -> m Term Source #

getTerm use name looks up name as a primitive or builtin, and throws an error otherwise. The use argument describes how the name is used for the sake of the error message.

constructorForm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => Term -> m Term Source #

Rewrite a literal to constructor form if possible.

pathView :: HasBuiltins m => Type -> m PathView Source #

Check whether the type is actually an path (lhs ≡ rhs) and extract lhs, rhs, and their type.

Precondition: type is reduced.

idViewAsPath :: HasBuiltins m => Type -> m PathView Source #

Non dependent Path

pathUnview :: PathView -> Type Source #

Revert the PathView.

Postcondition: type is reduced.

primEqualityName :: TCM QName Source #

Get the name of the equality type.

equalityView :: Type -> TCM EqualityView Source #

Check whether the type is actually an equality (lhs ≡ rhs) and extract lhs, rhs, and their type.

Precondition: type is reduced.

equalityUnview :: EqualityView -> Type Source #

Revert the EqualityView.

Postcondition: type is reduced.

constrainedPrims :: [String] Source #

Primitives with typechecking constrants.

data SizeView Source #

A useful view on sizes.

class IsSizeType a where Source #

Check if a type is the primSize type. The argument should be reduced.

Instances

Instances details
IsSizeType Term Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

IsSizeType CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

IsSizeType a => IsSizeType (Type' a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

IsSizeType a => IsSizeType (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

IsSizeType a => IsSizeType (b, a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => (b, a) -> m (Maybe BoundedSize) Source #

data BoundedSize Source #

Result of querying whether size variable i is bounded by another size.

Constructors

BoundedLt Term

yes i : Size< t

BoundedNo 

Instances

Instances details
Eq BoundedSize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Show BoundedSize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

haveSizedTypes :: TCM Bool Source #

Test whether OPTIONS --sized-types and whether the size built-ins are defined.

haveSizeLt :: TCM Bool Source #

Test whether the SIZELT builtin is defined.

builtinSizeHook :: String -> QName -> Type -> TCM () Source #

Add polarity info to a SIZE builtin.

sizeSort :: Sort Source #

The sort of built-in types SIZE and SIZELT.

sizeUniv :: Type Source #

The type of built-in types SIZE and SIZELT.

sizeType_ :: QName -> Type Source #

The built-in type SIZE with user-given name.

sizeType :: (HasBuiltins m, MonadTCEnv m, ReadTCState m) => m Type Source #

The built-in type SIZE.

sizeSucName :: (HasBuiltins m, HasOptions m) => m (Maybe QName) Source #

The name of SIZESUC.

sizeMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => NonEmpty Term -> m Term Source #

Transform list of terms into a term build from binary maximum.

sizeView :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => Term -> m SizeView Source #

Expects argument to be reduced.

sizeViewComparable :: DeepSizeView -> DeepSizeView -> SizeViewComparable () Source #

sizeViewComparable v w checks whether v >= w (then Left) or v <= w (then Right). If uncomparable, it returns NotComparable.

sizeViewPred :: Nat -> DeepSizeView -> DeepSizeView Source #

sizeViewPred k v decrements v by k (must be possible!).

sizeViewOffset :: DeepSizeView -> Maybe Offset Source #

sizeViewOffset v returns the number of successors or Nothing when infty.

removeSucs :: (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView) Source #

Remove successors common to both sides.

unSizeView :: SizeView -> TCM Term Source #

Turn a size view into a term.

maxViewCons :: DeepSizeView -> SizeMaxView -> SizeMaxView Source #

maxViewCons v ws = max v ws. It only adds v to ws if it is not subsumed by an element of ws.

sizeViewComparableWithMax :: DeepSizeView -> SizeMaxView -> SizeViewComparable SizeMaxView' Source #

sizeViewComparableWithMax v ws tries to find w in ws that compares with v and singles this out. Precondition: v /= DSizeInv.

addConstant :: QName -> Definition -> TCM () Source #

Add a constant to the signature. Lifts the definition to top level.

setTerminates :: QName -> Bool -> TCM () Source #

Set termination info of a defined function symbol.

setCompiledClauses :: QName -> CompiledClauses -> TCM () Source #

Set CompiledClauses of a defined function symbol.

setSplitTree :: QName -> SplitTree -> TCM () Source #

Set SplitTree of a defined function symbol.

modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM () Source #

Modify the clauses of a function.

addClauses :: QName -> [Clause] -> TCM () Source #

Lifts clauses to the top-level and adds them to definition. Also adjusts the funCopatternLHS field if necessary.

addPragma :: BackendName -> QName -> String -> TCM () Source #

Add a compiler pragma `{-# COMPILE backend name text #-}`

addSection :: ModuleName -> TCM () Source #

Add a section to the signature.

The current context will be stored as the cumulative module parameters for this section.

setModuleCheckpoint :: ModuleName -> TCM () Source #

Sets the checkpoint for the given module to the current checkpoint.

getSection :: (Functor m, ReadTCState m) => ModuleName -> m (Maybe Section) Source #

Get a section.

Why Maybe? The reason is that we look up all prefixes of a module to compute number of parameters, and for hierarchical top-level modules, A.B.C say, A and A.B do not exist.

applySection Source #

Arguments

:: ModuleName

Name of new module defined by the module macro.

-> Telescope

Parameters of new module.

-> ModuleName

Name of old module applied to arguments.

-> Args

Arguments of module application.

-> ScopeCopyInfo

Imported names and modules

-> TCM () 

Module application (followed by module parameter abstraction).

addDisplayForm :: QName -> DisplayForm -> TCM () Source #

Add a display form to a definition (could be in this or imported signature).

chaseDisplayForms :: QName -> TCM (Set QName) Source #

Find all names used (recursively) by display forms of a given name.

hasLoopingDisplayForm :: QName -> TCM Bool Source #

Check if a display form is looping.

whatInduction :: MonadTCM tcm => QName -> tcm Induction Source #

Can be called on either a (co)datatype, a record type or a (co)constructor.

singleConstructorType :: QName -> TCM Bool Source #

Does the given constructor come from a single-constructor type?

Precondition: The name has to refer to a constructor.

sigError :: (String -> a) -> a -> SigError -> a Source #

Standard eliminator for SigError.

getOriginalProjection :: HasConstInfo m => QName -> m QName Source #

Get the original name of the projection (the current one could be from a module application).

getPolarity :: HasConstInfo m => QName -> m [Polarity] Source #

Look up the polarity of a definition.

getPolarity' :: HasConstInfo m => Comparison -> QName -> m [Polarity] Source #

Look up polarity of a definition and compose with polarity represented by Comparison.

setPolarity :: QName -> [Polarity] -> TCM () Source #

Set the polarity of a definition.

getForcedArgs :: HasConstInfo m => QName -> m [IsForced] Source #

Look up the forced arguments of a definition.

getArgOccurrence :: QName -> Nat -> TCM Occurrence Source #

Get argument occurrence info for argument i of definition d (never fails).

setArgOccurrences :: QName -> [Occurrence] -> TCM () Source #

Sets the defArgOccurrences for the given identifier (which should already exist in the signature).

getErasedConArgs :: QName -> TCM [Bool] Source #

Returns a list of length conArity. If no erasure analysis has been performed yet, this will be a list of Falses.

addDataCons :: QName -> [QName] -> TCM () Source #

add data constructors to a datatype

getMutual :: QName -> TCM (Maybe [QName]) Source #

Get the mutually recursive identifiers of a symbol from the signature.

getMutual_ :: Defn -> Maybe [QName] Source #

Get the mutually recursive identifiers from a Definition.

setMutual :: QName -> [QName] -> TCM () Source #

Set the mutually recursive identifiers.

mutuallyRecursive :: QName -> QName -> TCM Bool Source #

Check whether two definitions are mutually recursive.

definitelyNonRecursive_ :: Defn -> Bool Source #

A functiondatarecord definition is nonRecursive if it is not even mutually recursive with itself.

getCurrentModuleFreeVars :: TCM Nat Source #

Get the number of parameters to the current module.

getDefFreeVars :: (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) => QName -> m Nat Source #

Compute the number of free variables of a defined name. This is the sum of number of parameters shared with the current module and the number of anonymous variables (if the name comes from a let-bound module).

moduleParamsToApply :: (Functor m, Applicative m, HasOptions m, MonadTCEnv m, ReadTCState m, MonadDebug m) => ModuleName -> m Args Source #

Compute the context variables to apply a definition to.

We have to insert the module telescope of the common prefix of the current module and the module where the definition comes from. (Properly raised to the current context.)

Example: module M₁ Γ where module M₁ Δ where f = ... module M₃ Θ where ... M₁.M₂.f [insert Γ raised by Θ]

instantiateDef :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => Definition -> m Definition Source #

Instantiate a closed definition with the correct part of the current context.

makeAbstract :: Definition -> Maybe Definition Source #

Give the abstract view of a definition.

inAbstractMode :: MonadTCEnv m => m a -> m a Source #

Enter abstract mode. Abstract definition in the current module are transparent.

inConcreteMode :: MonadTCEnv m => m a -> m a Source #

Not in abstract mode. All abstract definitions are opaque.

ignoreAbstractMode :: MonadTCEnv m => m a -> m a Source #

Ignore abstract mode. All abstract definitions are transparent.

inConcreteOrAbstractMode :: (MonadTCEnv m, HasConstInfo m) => QName -> (Definition -> m a) -> m a Source #

Enter concrete or abstract mode depending on whether the given identifier is concrete or abstract.

treatAbstractly :: MonadTCEnv m => QName -> m Bool Source #

Check whether a name might have to be treated abstractly (either if we're inAbstractMode or it's not a local name). Returns true for things not declared abstract as well, but for those makeAbstract will have no effect.

treatAbstractly' :: QName -> TCEnv -> Bool Source #

Andreas, 2015-07-01: If the current module is a weak suffix of the identifier module, we can see through its abstract definition if we are abstract. (Then treatAbstractly' returns False).

If I am not mistaken, then we cannot see definitions in the where block of an abstract function from the perspective of the function, because then the current module is a strict prefix of the module of the local identifier. This problem is fixed by removing trailing anonymous module name parts (underscores) from both names.

typeOfConst :: (HasConstInfo m, ReadTCState m) => QName -> m Type Source #

Get type of a constant, instantiated to the current context.

relOfConst :: HasConstInfo m => QName -> m Relevance Source #

Get relevance of a constant.

modalityOfConst :: HasConstInfo m => QName -> m Modality Source #

Get modality of a constant.

droppedPars :: Definition -> Int Source #

The number of dropped parameters for a definition. 0 except for projection(-like) functions and constructors.

isProjection :: HasConstInfo m => QName -> m (Maybe Projection) Source #

Is it the name of a record projection?

isStaticFun :: Defn -> Bool Source #

Is it a function marked STATIC?

isInlineFun :: Defn -> Bool Source #

Is it a function marked INLINE?

isProperProjection :: Defn -> Bool Source #

Returns True if we are dealing with a proper projection, i.e., not a projection-like function nor a record field value (projection applied to argument).

projectionArgs :: Defn -> Int Source #

Number of dropped initial arguments of a projection(-like) function.

usesCopatterns :: HasConstInfo m => QName -> m Bool Source #

Check whether a definition uses copatterns.

applyDef :: HasConstInfo m => ProjOrigin -> QName -> Arg Term -> m Term Source #

Apply a function f to its first argument, producing the proper postfix projection if f is a projection.

class UnFreezeMeta a where Source #

Unfreeze meta and its type if this is a meta again. Does not unfreeze deep occurrences of metas.

Methods

unfreezeMeta :: MonadMetaSolver m => a -> m () Source #

Instances

Instances details
UnFreezeMeta MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => MetaId -> m () Source #

UnFreezeMeta LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

UnFreezeMeta PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

UnFreezeMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Level -> m () Source #

UnFreezeMeta Sort Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Sort -> m () Source #

UnFreezeMeta Type Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Type -> m () Source #

UnFreezeMeta Term Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Term -> m () Source #

UnFreezeMeta a => UnFreezeMeta [a] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => [a] -> m () Source #

UnFreezeMeta a => UnFreezeMeta (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Abs a -> m () Source #

class IsInstantiatedMeta a where Source #

Check whether all metas are instantiated. Precondition: argument is a meta (in some form) or a list of metas.

Instances

Instances details
IsInstantiatedMeta MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

IsInstantiatedMeta LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

IsInstantiatedMeta PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

IsInstantiatedMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

IsInstantiatedMeta Term Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

IsInstantiatedMeta a => IsInstantiatedMeta [a] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => [a] -> m Bool Source #

IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

IsInstantiatedMeta a => IsInstantiatedMeta (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) Source #

Does not worry about raising.

Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

class (MonadConstraint m, MonadReduce m, MonadAddContext m, MonadTCEnv m, ReadTCState m, HasBuiltins m, HasConstInfo m, MonadDebug m) => MonadMetaSolver m where Source #

Monad service class for creating, solving and eta-expanding of metavariables.

Methods

newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> m MetaId Source #

Generate a new meta variable with some instantiation given. For instance, the instantiation could be a PostponedTypeCheckingProblem.

assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m () Source #

Assign to an open metavar which may not be frozen. First check that metavar args are in pattern fragment. Then do extended occurs check on given thing.

Assignment is aborted by throwing a PatternErr via a call to patternViolation. This error is caught by catchConstraint during equality checking (compareAtom) and leads to restoration of the original constraints.

assignTerm' :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m () Source #

Directly instantiate the metavariable. Skip pattern check, occurs check and frozen check. Used for eta expanding frozen metas.

etaExpandMeta :: [MetaKind] -> MetaId -> m () Source #

Eta expand a metavariable, if it is of the specified kind. Don't do anything if the metavariable is a blocked term.

updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> m () Source #

Update the status of the metavariable

speculateMetas :: m () -> m KeepMetas -> m () Source #

'speculateMetas fallback m' speculatively runs m, but if the result is RollBackMetas any changes to metavariables are rolled back and fallback is run instead.

data MetaKind Source #

Various kinds of metavariables.

Constructors

Records

Meta variables of record type.

SingletonRecords

Meta variables of "hereditarily singleton" record type.

Levels

Meta variables of level type, if type-in-type is activated.

allMetaKinds :: [MetaKind] Source #

All possible metavariable kinds.

dontAssignMetas :: (MonadTCEnv m, HasOptions m, MonadDebug m) => m a -> m a Source #

Switch off assignment of metas.

getMetaStore :: ReadTCState m => m MetaStore Source #

Get the meta store.

metasCreatedBy :: ReadTCState m => m a -> m (a, IntSet) Source #

Run a computation and record which new metas it created.

lookupMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable) Source #

Lookup a meta variable.

metaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type Source #

Type of a term or sort meta.

updateMetaVarTCM :: MetaId -> (MetaVariable -> MetaVariable) -> TCM () Source #

Update the information associated with a meta variable.

insertMetaVar :: MetaId -> MetaVariable -> TCM () Source #

Insert a new meta variable with associated information into the meta store.

getMetaContextArgs :: MonadTCEnv m => MetaVariable -> m Args Source #

Compute the context variables that a meta should be applied to, accounting for pruning.

getMetaTypeInContext :: (MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m) => MetaId -> m Type Source #

Given a meta, return the type applied to the current context.

isGeneralizableMeta :: (ReadTCState m, MonadFail m) => MetaId -> m DoGeneralize Source #

Is it a meta that might be generalized?

constraintMetas :: Constraint -> TCM (Set MetaId) Source #

Returns all metavariables in a constraint. Slightly complicated by the fact that blocked terms are represented by two meta variables. To find the second one we need to look up the meta listeners for the one in the UnBlock constraint.

createMetaInfo :: (MonadTCEnv m, ReadTCState m) => m MetaInfo Source #

Create MetaInfo in the current environment.

registerInteractionPoint :: forall m. MonadInteractionPoints m => Bool -> Range -> Maybe Nat -> m InteractionId Source #

Register an interaction point during scope checking. If there is no interaction id yet, create one.

findInteractionPoint_ :: Range -> InteractionPoints -> Maybe InteractionId Source #

Find an interaction point by Range by searching the whole map.

O(n): linear in the number of registered interaction points.

connectInteractionPoint :: MonadInteractionPoints m => InteractionId -> MetaId -> m () Source #

Hook up meta variable to interaction point.

removeInteractionPoint :: MonadInteractionPoints m => InteractionId -> m () Source #

Mark an interaction point as solved.

getInteractionPoints :: ReadTCState m => m [InteractionId] Source #

Get a list of interaction ids.

getInteractionMetas :: ReadTCState m => m [MetaId] Source #

Get all metas that correspond to unsolved interaction ids.

getInteractionIdsAndMetas :: ReadTCState m => m [(InteractionId, MetaId)] Source #

Get all metas that correspond to unsolved interaction ids.

isInteractionMeta :: ReadTCState m => MetaId -> m (Maybe InteractionId) Source #

Does the meta variable correspond to an interaction point?

Time: O(n) where n is the number of interaction metas.

lookupInteractionPoint :: (MonadFail m, ReadTCState m, MonadError TCErr m) => InteractionId -> m InteractionPoint Source #

Get the information associated to an interaction point.

lookupInteractionId :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) => InteractionId -> m MetaId Source #

Get MetaId for an interaction point. Precondition: interaction point is connected.

lookupInteractionMeta :: ReadTCState m => InteractionId -> m (Maybe MetaId) Source #

Check whether an interaction id is already associated with a meta variable.

newMeta :: MonadMetaSolver m => Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> m MetaId Source #

Generate new meta variable.

newMetaTCM' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId Source #

Generate a new meta variable with some instantiation given. For instance, the instantiation could be a PostponedTypeCheckingProblem.

getMetaRange :: (MonadFail m, ReadTCState m) => MetaId -> m Range Source #

Get the Range for a meta variable.

listenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m () Source #

listenToMeta l m: register l as a listener to m. This is done when the type of l is blocked by m.

unlistenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m () Source #

Unregister a listener.

getMetaListeners :: (MonadFail m, ReadTCState m) => MetaId -> m [Listener] Source #

Get the listeners to a meta.

withFreezeMetas :: TCM a -> TCM a Source #

Freeze all so far unfrozen metas for the duration of the given computation.

freezeMetas :: TCM [MetaId] Source #

Freeze all meta variables and return the list of metas that got frozen.

freezeMetas' :: (MetaId -> Bool) -> TCM [MetaId] Source #

Freeze some meta variables and return the list of metas that got frozen.

unfreezeMetas :: TCM () Source #

Thaw all meta variables.

unfreezeMetas' :: (MetaId -> Bool) -> TCM () Source #

Thaw some metas, as indicated by the passed condition.

activeBackendMayEraseType :: QName -> TCM Bool Source #

Ask the active backend whether a type may be erased. See issue #3732.

callBackend :: String -> IsMain -> Interface -> TCM () Source #

Call the compilerMain function of the given backend.

lookupBackend :: BackendName -> TCM (Maybe Backend) Source #

Look for a backend of the given name.

activeBackend :: TCM (Maybe Backend) Source #

Get the currently active backend (if any).