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

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 #

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

ToJSON ProblemId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Pretty ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasFresh ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

EncodeTCM ProblemId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

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

Defined in Agda.TypeChecking.Conversion.Pure

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 (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadStConcreteNames m => MonadStConcreteNames (ReaderT r 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

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

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

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