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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Monad.Base

Contents

Synopsis

Type checking state

data TCState Source #

Constructors

TCSt 

Fields

Instances
Show TCState Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensPersistentVerbosity TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensIncludePaths TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensSafeMode TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensCommandLineOptions TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensVerbosity TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensPragmaOptions TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

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
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 (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 (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 (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 #

data PreScopeState Source #

Constructors

PreScopeState 

Fields

data PostScopeState Source #

Constructors

PostScopeState 

Fields

data MutualBlock Source #

A mutual block of names in the signature.

Constructors

MutualBlock 

Fields

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

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.

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).

data TypeCheckAction Source #

A complete log for a module will look like this:

  • Pragmas
  • EnterSection, entering the main module.
  • 'Decl'/'EnterSection'/'LeaveSection', for declarations and nested modules
  • LeaveSection, leaving the main module.

initPersistentState :: PersistentTCState Source #

Empty persistent state.

initPreScopeState :: PreScopeState Source #

Empty state of type checker.

st-prefixed lenses

Fresh things

class Monad m => MonadFresh i m where Source #

Methods

fresh :: m i Source #

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

newtype ProblemId Source #

Constructors

ProblemId Nat 
Instances
Enum ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Integral ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: ProblemId -> Constr #

dataTypeOf :: ProblemId -> DataType #

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

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

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

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

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

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

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

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

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

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

Num ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Ord ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Real ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

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

newtype CheckpointId Source #

Constructors

CheckpointId Int 
Instances
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 :: (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 FreshName a where Source #

Create a fresh name from a.

Methods

freshName_ :: MonadFresh NameId m => a -> m Name Source #

Instances
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

Managing file names

type ModuleToSource = Map TopLevelModuleName AbsolutePath Source #

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

type SourceToModule = Map AbsolutePath TopLevelModuleName Source #

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

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.

Associating concrete names to an abstract name

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

Interface

data ModuleInfo Source #

Constructors

ModuleInfo 

Fields

data Interface Source #

Constructors

Interface 

Fields

iFullHash :: Interface -> Hash Source #

Combines the source hash and the (full) hashes of the imported modules.

Closure

data Closure a Source #

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

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 :: (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

Constraints

data ProblemConstraint Source #

Instances
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 :: (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

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
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 :: (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 Comparison Source #

Constructors

CmpEq 
CmpLeq 
Instances
Eq Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: Comparison -> Constr #

dataTypeOf :: Comparison -> DataType #

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

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

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

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

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

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

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

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

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

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

Show Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

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

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
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 :: (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

Open things

data Open a Source #

A thing tagged with the context it came from.

Constructors

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

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 :: (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

Judgements

data Judgement a Source #

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

Constructors

HasType 

Fields

IsSort 

Fields

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

Generalizable variables

data DoGeneralize Source #

Instances
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 :: (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 GeneralizedValue Source #

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

Instances
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 :: (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

Meta variables

data MetaVariable Source #

Constructors

MetaVar 

Fields

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
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 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) 

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

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 MetaInfo Source #

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

Constructors

MetaInfo 

Fields

type MetaNameSuggestion = String Source #

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

data NamedMeta Source #

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

Interaction meta variables

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

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 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
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 :: (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

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

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 :: (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 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
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 :: (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 #

Signature

data Signature Source #

Constructors

Sig 

Fields

Instances
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 :: (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

newtype Section Source #

Constructors

Section 
Instances
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 :: (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 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
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 :: (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

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
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 :: (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

defaultDisplayForm :: QName -> [LocalDisplayForm] Source #

By default, we have no display form.

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
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 :: (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 NLPType Source #

Constructors

NLPType 
Instances
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 :: (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 NLPSort Source #

Constructors

PType NLPat 
PProp NLPat 
PInf 
PSizeUniv 
Instances
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 :: (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 RewriteRule Source #

Rewrite rules can be added independently from function clauses.

Constructors

RewriteRule 

Fields

Instances
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 :: (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 Definition Source #

Constructors

Defn 

Fields

Instances
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 :: (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 NumGeneralizableArgs Source #

Constructors

NoGeneralizableArgs 
SomeGeneralizableArgs Int

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

Instances
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 :: (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

defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition Source #

Create a definition with sensible defaults.

data Polarity Source #

Polarity for equality and subtype checking.

Constructors

Covariant

monotone

Contravariant

antitone

Invariant

no information (mixed variance)

Nonvariant

constant

Instances
Eq Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: Polarity -> Constr #

dataTypeOf :: Polarity -> DataType #

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

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

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

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

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

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

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

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

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

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

Show Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Abstract [Polarity] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply [Polarity] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data IsForced Source #

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

Constructors

Forced 
NotForced 
Instances
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 :: (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 CompilerPragma Source #

The backends are responsible for parsing their own pragmas.

Instances
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 :: (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

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

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
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 :: (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

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
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 :: (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 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
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 :: (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

newtype ProjLams Source #

Abstractions to build projection function (dropping parameters).

Constructors

ProjLams 

Fields

Instances
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 :: (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

projDropPars :: Projection -> ProjOrigin -> Term Source #

Building the projection function (which drops the parameters).

projArgInfo :: Projection -> ArgInfo Source #

The info of the principal (record) argument.

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
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 :: (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

setEtaEquality :: EtaEquality -> HasEta -> EtaEquality Source #

Make sure we do not overwrite a user specification.

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
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 :: (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 CompKit Source #

Constructors

CompKit 
Instances
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 :: (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 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
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 :: (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

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.

newtype Fields Source #

Constructors

Fields [(Name, Type)] 
Instances
Null Fields Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

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
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 :: (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

data Reduced no yes Source #

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

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

data IsReduced Source #

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

Constructors

NotReduced 
Reduced (Blocked ()) 

data MaybeReduced a Source #

Constructors

MaybeRed 
Instances
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 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 Term 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
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 :: (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

allReductions :: AllowedReductions Source #

Not quite all reductions (skip non-terminating reductions)

data PrimitiveImpl Source #

Primitives

Constructors

PrimImpl Type PrimFun 

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?

Injectivity

data FunctionInverse' c Source #

Constructors

NotInjective 
Inverse (InversionMap c) 
Instances
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 :: (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 TermHead Source #

Instances
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 :: (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

Mutual blocks

newtype MutualId Source #

Constructors

MutId Int32 
Instances
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 :: (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

Statistics

Trace

data Call Source #

Instances
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 :: (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 #

Instance table

type InstanceTable = Map QName (Set QName) Source #

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

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.

Builtin things

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.

data Builtin pf Source #

Constructors

Builtin Term 
Prim pf 
Instances
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 #

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

Highlighting levels

data HighlightingLevel Source #

How much highlighting should be sent to the user interface?

Constructors

None 
NonInteractive 
Interactive

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

Instances
Eq HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: HighlightingLevel -> Constr #

dataTypeOf :: HighlightingLevel -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Read HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data HighlightingMethod Source #

How should highlighting be sent to the user interface?

Constructors

Direct

Via stdout.

Indirect

Both via files and via stdout.

Instances
Eq HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: HighlightingMethod -> Constr #

dataTypeOf :: HighlightingMethod -> DataType #

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

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

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

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

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

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

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

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

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

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

Read HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

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.

Type checking environment

data TCEnv Source #

Constructors

TCEnv 

Fields

Instances
Data TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: TCEnv -> Constr #

dataTypeOf :: TCEnv -> DataType #

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

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

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

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

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

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

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

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

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

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

LensIsAbstract TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensRelevance TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensQuantity TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensModality TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensTCEnv TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

class LensTCEnv a where Source #

Instances
LensTCEnv TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensTCEnv (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data UnquoteFlags Source #

Constructors

UnquoteFlags 
Instances
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 :: (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 #

e-prefixed lenses

Context

type Context = [ContextEntry] Source #

The Context is a stack of ContextEntrys.

Let bindings

Abstract mode

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
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 :: (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

Insertion of implicit arguments

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
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 :: (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 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
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 :: (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

Type checking warnings (aka non-fatal errors)

data Warning Source #

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

Constructors

NicifierIssue DeclarationWarning 
TerminationIssue [TerminationError] 
UnreachableClauses QName [Range]

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

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

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

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

Do not use directly with warning

UnsolvedInteractionMetas [Range]

Do not use directly with warning

UnsolvedConstraints Constraints

Do not use directly with warning

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

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

EmptyRewritePragma

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

IllformedAsClause String

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

ClashesViaRenaming NameOrModule [Name]

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

UselessPublic

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

UselessInline QName 
WrongInstanceDeclaration 
InstanceWithExplicitArg QName

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

InstanceNoOutputTypeName Doc

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

InstanceArgWithExplicitArg Doc

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

InversionDepthReached QName

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

GenericWarning Doc

Harmless generic warning (not an error)

GenericNonFatalError Doc

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

SafeFlagPostulate Name 
SafeFlagPragma [String]

Unsafe OPTIONS.

SafeFlagNonTerminating 
SafeFlagTerminating 
SafeFlagWithoutKFlagPrimEraseEquality 
WithoutKFlagPrimEraseEquality 
SafeFlagNoPositivityCheck 
SafeFlagPolarity 
SafeFlagNoUniverseCheck 
SafeFlagNoCoverageCheck 
SafeFlagInjective 
SafeFlagEta

ETA pragma is unsafe.

ParseWarning ParseWarning 
LibraryWarning LibWarning 
DeprecationWarning String String String

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

UserWarning String

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

FixityInRenamingModule (NonEmpty Range)

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

ModuleDoesntExport QName [ImportedName]

Some imported names are not actually exported by the source module

InfectiveImport String ModuleName

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

CoInfectiveImport String ModuleName

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

RewriteNonConfluent Term Term Term Doc

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

RewriteMaybeNonConfluent Term Term [Doc]

Confluence checker got stuck on computing overlap between two rewrite rules

PragmaCompileErased BackendName QName

COMPILE directive for an erased symbol

NotInScopeW [QName]

Out of scope error we can recover from

Instances
Data Warning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: Warning -> Constr #

dataTypeOf :: Warning -> DataType #

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

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

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

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

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

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

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

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

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

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

Show Warning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj Warning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

PrettyTCM Warning Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Warning

Methods

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

data TCWarning Source #

Constructors

TCWarning 

Fields

Type checking errors

data CallInfo Source #

Information about a call.

Constructors

CallInfo 

Fields

Instances
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 :: (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 TerminationError Source #

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

Constructors

TerminationError 

Fields

Instances
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 :: (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 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
Show SplitError Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM SplitError 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 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
Show TypeError Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM TypeError Source # 
Instance details

Defined in Agda.TypeChecking.Errors

data LHSOrPatSyn Source #

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

Constructors

IsLHS 
IsPatSyn 

data TCErr Source #

Type-checking errors.

Constructors

TypeError 

Fields

Exception Range Doc 
IOException TCState Range IOException

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

PatternErr

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

Instances
Show TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> TCErr -> ShowS #

show :: TCErr -> String #

showList :: [TCErr] -> ShowS #

Exception TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Error TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: TCErr -> Range Source #

PrettyTCM TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

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

MonadError TCErr TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

throwError :: TCErr -> TCM a #

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

MonadError TCErr IM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

throwError :: TCErr -> IM a #

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

MonadError TCErr TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

throwError :: TCErr -> TerM a #

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

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

Defined in Agda.TypeChecking.Conversion.Pure

Accessing options

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.

commandLineOptions :: m CommandLineOptions Source #

Returns the command line options which are currently in effect.

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

Returns the pragma options which are currently in effect.

commandLineOptions :: (HasOptions n, MonadTrans t, m ~ t n) => m CommandLineOptions Source #

Returns the command line options which are currently in effect.

Instances
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 (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 (ExceptT e 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

getIncludeDirs :: HasOptions m => m [AbsolutePath] Source #

Gets the include directories.

Precondition: optAbsoluteIncludePaths must be nonempty (i.e. setCommandLineOptions must have run).

The reduce monad

data ReduceEnv Source #

Environment of the reduce monad.

Constructors

ReduceEnv 

Fields

newtype ReduceM a Source #

Constructors

ReduceM 

Fields

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

fail :: String -> 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

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 #

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

Methods

liftReduce :: ReduceM a -> m a Source #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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 (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 #

Monad with read-only TCEnv

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
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 (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 (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 (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 #

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.

Monad with mutable TCState

class Monad m => MonadTCState m where Source #

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

Minimal complete definition

getTC, (putTC | modifyTC)

Methods

getTC :: m TCState Source #

putTC :: TCState -> m () Source #

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

Instances
MonadTCState TerM Source # 
Instance details

Defined in Agda.Termination.Monad

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Names

MonadTCState m => MonadTCState (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 (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 (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

TCState accessors (no lenses)

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.

TCState accessors via lenses

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.

Type checking monad transformer

newtype TCMT m a Source #

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

Constructors

TCM 

Fields

Instances
MonadTrans TCMT Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

CatchImpossible TCM Source #

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

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

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

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

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

MonadFixityError ScopeM Source # 
Instance details

Defined in Agda.Syntax.Scope.Monad

MonadStConcreteNames TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadInteractionPoints TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

MonadAddContext TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

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

MonadDebug TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

MonadStatistics TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Statistics

Methods

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

MonadWarning TCM Source # 
Instance details

Defined in Agda.TypeChecking.Warnings

Methods

addWarning :: TCWarning -> TCM () Source #

MonadConstraint TCM Source # 
Instance details

Defined in Agda.TypeChecking.Constraints

MonadMetaSolver TCM Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars

MonadError TCErr TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

throwError :: TCErr -> TCM a #

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

MonadError TCErr IM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

throwError :: TCErr -> IM a #

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

MonadBench Phase TCM Source #

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

Instance details

Defined in Agda.TypeChecking.Monad.Base

HasFresh i => MonadFresh i TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fresh :: TCM i Source #

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

Defined in Agda.Auto.Convert

Methods

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

Conversion TOM Type (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

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

Conversion TOM Term (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

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

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

Defined in Agda.Auto.Convert

Methods

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

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

Defined in Agda.Auto.Convert

Methods

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

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

Defined in Agda.Auto.Convert

Methods

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

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

Defined in Agda.Auto.Convert

Methods

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

return :: a -> TCMT m a #

fail :: String -> TCMT m a #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

fail :: String -> TCMT m a #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

pure :: a -> TCMT m a #

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

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

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

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

Semigroup (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Warnings

Methods

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

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

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

liftIO :: IO a -> TCMT m a #

Null (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: TCMT m TCEnv Source #

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: TCMT m TCState Source #

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

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

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

Defined in Agda.TypeChecking.Monad.Builtin

TraceS [TCM Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

TraceS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

ReportS [TCM Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

ReportS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

HasConstInfo (TCMT IO) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Signature

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

Defined in Agda.TypeChecking.Monad.Base

Methods

fromString :: String -> TCMT m a #

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

Strict (non-shortcut) semigroup.

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

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

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

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

Strict (non-shortcut) monoid.

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

mempty :: TCMT m a #

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

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

type TCM = TCMT IO Source #

Type checking monad.

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 #

type IM = TCMT (InputT IO) Source #

Interaction monad.

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.

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

Embedding a TCM computation.

Minimal complete definition

Nothing

Methods

liftTCM :: TCM a -> tcm a Source #

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

Instances
MonadTCM TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

liftTCM :: TCM a -> TerM a Source #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Defined in Agda.TypeChecking.Names

Methods

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

MonadTCM tcm => MonadTCM (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 (ExceptT err tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ExceptT err 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 #

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 TCMT action (a TCMT 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.

Names for generated definitions

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

KillRange instances