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

Agda.TypeChecking.Monad.Base

Synopsis

Type checking state

data TCState Source #

Constructors

TCSt 

Fields

Instances

Instances details
Show TCState Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> TCState -> ShowS

show :: TCState -> String

showList :: [TCState] -> ShowS

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

Instances details
ReadTCState ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

ReadTCState AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ReadTCState TerM Source # 
Instance details

Defined in Agda.Termination.Monad

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

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: MaybeT m TCState Source #

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

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: ListT m TCState Source #

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

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: TCMT m TCState Source #

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

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

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

Defined in Agda.TypeChecking.Names

Methods

getTCState :: NamesT m TCState Source #

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

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

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

Defined in Agda.TypeChecking.Conversion.Pure

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

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: ExceptT err m TCState Source #

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

withTCState :: (TCState -> TCState) -> ExceptT err m a -> ExceptT err m a Source #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: ReaderT r m TCState Source #

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

withTCState :: (TCState -> TCState) -> ReaderT r m a -> ReaderT r m a Source #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: StateT s m TCState Source #

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

withTCState :: (TCState -> TCState) -> StateT s m a -> StateT s m a Source #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: WriterT w m TCState Source #

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

withTCState :: (TCState -> TCState) -> WriterT w m a -> WriterT w m a Source #

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

Instances

Instances details
Eq MutualBlock Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: MutualBlock -> MutualBlock -> Bool

(/=) :: MutualBlock -> MutualBlock -> Bool

Show MutualBlock Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> MutualBlock -> ShowS

show :: MutualBlock -> String

showList :: [MutualBlock] -> ShowS

Null MutualBlock Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data PersistentTCState Source #

A part of the state which is not reverted when an error is thrown or the state is reset.

Constructors

PersistentTCSt 

Fields

Instances

Instances details
LensPersistentVerbosity PersistentTCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensIncludePaths PersistentTCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensSafeMode PersistentTCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensCommandLineOptions PersistentTCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

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:

initPersistentState :: PersistentTCState Source #

Empty persistent state.

initPreScopeState :: PreScopeState Source #

Empty state of type checker.

st-prefixed lenses

getUserWarnings :: ReadTCState m => m (Map QName String) Source #

Fresh things

class Monad m => MonadFresh i m where Source #

Methods

fresh :: m i Source #

Instances

Instances details
HasFresh i => MonadFresh i TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fresh :: TCM i Source #

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

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fresh :: PureConversionT m Int Source #

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

Instances details
Enum ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: ProblemId -> ProblemId -> Bool

(/=) :: ProblemId -> ProblemId -> Bool

Integral ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: ProblemId -> Constr

dataTypeOf :: ProblemId -> DataType

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

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

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

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

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

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

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

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

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

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

Num ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Ord ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: ProblemId -> ProblemId -> Ordering

(<) :: ProblemId -> ProblemId -> Bool

(<=) :: ProblemId -> ProblemId -> Bool

(>) :: ProblemId -> ProblemId -> Bool

(>=) :: ProblemId -> ProblemId -> Bool

max :: ProblemId -> ProblemId -> ProblemId

min :: ProblemId -> ProblemId -> ProblemId

Real ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

toRational :: ProblemId -> Rational

Show ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> ProblemId -> ShowS

show :: ProblemId -> String

showList :: [ProblemId] -> ShowS

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

Instances details
Enum CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: CheckpointId -> CheckpointId -> Bool

(/=) :: CheckpointId -> CheckpointId -> Bool

Integral CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: CheckpointId -> Constr

dataTypeOf :: CheckpointId -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> CheckpointId -> CheckpointId

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

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

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

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

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

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

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

Num CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Ord CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Real CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

toRational :: CheckpointId -> Rational

Show CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> CheckpointId -> ShowS

show :: CheckpointId -> String

showList :: [CheckpointId] -> ShowS

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

Methods

icode :: CheckpointId -> S Int32 Source #

icod_ :: CheckpointId -> S Int32 Source #

value :: Int32 -> R CheckpointId Source #

PrettyTCM CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

freshName :: MonadFresh NameId m => Range -> String -> m Name Source #

class FreshName a where Source #

Create a fresh name from a.

Methods

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

Instances

Instances details
FreshName () Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freshName_ :: MonadFresh NameId m => () -> m Name Source #

FreshName String Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

FreshName Range Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

FreshName (Range, String) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freshName_ :: MonadFresh NameId m => (Range, String) -> m Name Source #

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

Instances details
MonadStConcreteNames TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadStConcreteNames AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ReadTCState m => MonadStConcreteNames (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

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

Defined in Agda.TypeChecking.Monad.Base

Methods

runStConcreteNames :: StateT ConcreteNames (ReaderT r m) a -> ReaderT r m a Source #

useConcreteNames :: ReaderT r m ConcreteNames Source #

modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> ReaderT r m () Source #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

runStConcreteNames :: StateT ConcreteNames (StateT s m) a -> StateT s m a Source #

useConcreteNames :: StateT s m ConcreteNames Source #

modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> StateT s m () Source #

Interface

data ModuleInfo Source #

Constructors

ModuleInfo 

Fields

  • miInterface :: Interface
     
  • miWarnings :: Bool

    True if warnings were encountered when the module was type checked.

  • miPrimitive :: Bool

    True if the module is a primitive module, which should always be importable.

data ForeignCode Source #

Constructors

ForeignCode Range String 

Instances

Instances details
Show ForeignCode Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> ForeignCode -> ShowS

show :: ForeignCode -> String

showList :: [ForeignCode] -> ShowS

EmbPrj ForeignCode Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

Methods

icode :: ForeignCode -> S Int32 Source #

icod_ :: ForeignCode -> S Int32 Source #

value :: Int32 -> R ForeignCode Source #

data Interface Source #

Constructors

Interface 

Fields

Instances

Instances details
Show Interface Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Interface -> ShowS

show :: Interface -> String

showList :: [Interface] -> ShowS

Pretty Interface Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj Interface Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances

Methods

icode :: Interface -> S Int32 Source #

icod_ :: Interface -> S Int32 Source #

value :: Int32 -> R Interface Source #

InstantiateFull Interface Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

iFullHash :: Interface -> Hash Source #

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

Closure

data Closure a Source #

Instances

Instances details
Functor Closure Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Foldable Closure Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

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

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

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

foldl :: (b -> a -> b) -> b -> Closure a -> b

foldl' :: (b -> a -> b) -> b -> Closure a -> b

foldr1 :: (a -> a -> a) -> Closure a -> a

foldl1 :: (a -> a -> a) -> Closure a -> a

toList :: Closure a -> [a]

null :: Closure a -> Bool

length :: Closure a -> Int

elem :: Eq a => a -> Closure a -> Bool

maximum :: Ord a => Closure a -> a

minimum :: Ord a => Closure a -> a

sum :: Num a => Closure a -> a

product :: Num a => Closure a -> a

LensClosure a (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.Interaction.BasicOps

Data a => Data (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Closure a -> c (Closure a)

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

toConstr :: Closure a -> Constr

dataTypeOf :: Closure a -> DataType

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

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

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

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

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

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

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

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

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

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Closure a -> ShowS

show :: Closure a -> String

showList :: [Closure a] -> ShowS

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

Defined in Agda.TypeChecking.Monad.Base

HasRange a => HasRange (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: Closure a -> Range Source #

LensIsAbstract (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensTCEnv (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Pretty

Methods

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

MentionsMeta a => MentionsMeta (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Closure a -> Bool Source #

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

Defined in Agda.TypeChecking.Reduce

Normalise a => Normalise (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify a => Simplify (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce a => Reduce (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate a => Instantiate (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

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

Methods

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

Constraints

data ProblemConstraint Source #

Instances

Instances details
Data ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: ProblemConstraint -> Constr

dataTypeOf :: ProblemConstraint -> DataType

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

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

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

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

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

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

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

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

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

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

Show ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> ProblemConstraint -> ShowS

show :: ProblemConstraint -> String

showList :: [ProblemConstraint] -> ShowS

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

Methods

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

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

Instances details
Data Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: Constraint -> Constr

dataTypeOf :: Constraint -> DataType

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

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

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

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

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

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

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

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

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

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

Show Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Constraint -> ShowS

show :: Constraint -> String

showList :: [Constraint] -> ShowS

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

Instances details
Eq Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: Comparison -> Comparison -> Bool

(/=) :: Comparison -> Comparison -> Bool

Data Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: Comparison -> Constr

dataTypeOf :: Comparison -> DataType

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

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

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

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

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

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

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

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

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

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

Show Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Comparison -> ShowS

show :: Comparison -> String

showList :: [Comparison] -> ShowS

Pretty Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

data CompareDirection Source #

An extension of Comparison to >=.

Constructors

DirEq 
DirLeq 
DirGeq 

Instances

Instances details
Eq CompareDirection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show CompareDirection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> CompareDirection -> ShowS

show :: CompareDirection -> String

showList :: [CompareDirection] -> ShowS

Pretty CompareDirection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

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

Instances details
Eq CompareAs 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

(==) :: CompareAs -> CompareAs -> Bool

(/=) :: CompareAs -> CompareAs -> Bool

Data CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: CompareAs -> Constr

dataTypeOf :: CompareAs -> DataType

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

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

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

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

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

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

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

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

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

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

Show CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> CompareAs -> ShowS

show :: CompareAs -> String

showList :: [CompareAs] -> ShowS

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

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => CompareAs -> m (Maybe BoundedSize) Source #

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

Methods

isMeta :: HasBuiltins m => CompareAs -> m (Maybe MetaId) Source #

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

Instances details
Functor Open Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Foldable Open Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

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

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

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

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

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

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

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

toList :: Open a -> [a]

null :: Open a -> Bool

length :: Open a -> Int

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

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

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

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

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

Traversable Open Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

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

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

Decoration Open Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Open a -> c (Open a)

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

toConstr :: Open a -> Constr

dataTypeOf :: Open a -> DataType

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

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

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

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

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

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

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

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

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

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Open a -> ShowS

show :: Open a -> String

showList :: [Open a] -> ShowS

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Open a -> S Int32 Source #

icod_ :: Open a -> S Int32 Source #

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

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

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Open a -> Set QName Source #

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

Defined in Agda.TypeChecking.Reduce

Judgements

data Judgement a Source #

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

Constructors

HasType 

Fields

IsSort 

Fields

Instances

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

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Judgement a -> ShowS

show :: Judgement a -> String

showList :: [Judgement a] -> ShowS

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

Instances details
Eq DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: DoGeneralize -> DoGeneralize -> Bool

(/=) :: DoGeneralize -> DoGeneralize -> Bool

Data DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: DoGeneralize -> Constr

dataTypeOf :: DoGeneralize -> DataType

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

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

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

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

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

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

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

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

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

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

Ord DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> DoGeneralize -> ShowS

show :: DoGeneralize -> String

showList :: [DoGeneralize] -> ShowS

KillRange DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DoGeneralize -> S Int32 Source #

icod_ :: DoGeneralize -> S Int32 Source #

value :: Int32 -> R DoGeneralize Source #

data GeneralizedValue Source #

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

Instances

Instances details
Data GeneralizedValue Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: GeneralizedValue -> Constr

dataTypeOf :: GeneralizedValue -> DataType

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

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

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

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

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

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

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

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

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

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

Show GeneralizedValue Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> GeneralizedValue -> ShowS

show :: GeneralizedValue -> String

showList :: [GeneralizedValue] -> ShowS

Meta variables

data MetaVariable Source #

Constructors

MetaVar 

Fields

data Listener Source #

Instances

Instances details
Eq Listener Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: Listener -> Listener -> Bool

(/=) :: Listener -> Listener -> Bool

Ord Listener Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: Listener -> Listener -> Ordering

(<) :: Listener -> Listener -> Bool

(<=) :: Listener -> Listener -> Bool

(>) :: Listener -> Listener -> Bool

(>=) :: Listener -> Listener -> Bool

max :: Listener -> Listener -> Listener

min :: Listener -> Listener -> Listener

data Frozen Source #

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

Constructors

Frozen

Do not instantiate.

Instantiable 

Instances

Instances details
Eq Frozen Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Show Frozen Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Frozen -> ShowS

show :: Frozen -> String

showList :: [Frozen] -> ShowS

data MetaInstantiation Source #

Constructors

InstV [Arg String] Term

solved by term (abstracted over some free variables)

Open

unsolved

OpenInstance

open, to be instantiated by instance search

BlockedConst Term

solution blocked by unsolved constraints

PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool) 

Instances

Instances details
Show MetaInstantiation Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> MetaInstantiation -> ShowS

show :: MetaInstantiation -> String

showList :: [MetaInstantiation] -> ShowS

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

Instances

Instances details
PrettyTCM TypeCheckingProblem Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

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 

Instances

Instances details
Eq MetaPriority Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: MetaPriority -> MetaPriority -> Bool

(/=) :: MetaPriority -> MetaPriority -> Bool

Ord MetaPriority Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show MetaPriority Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> MetaPriority -> ShowS

show :: MetaPriority -> String

showList :: [MetaPriority] -> ShowS

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

  • ipRange :: Range

    The position of the interaction point.

  • ipMeta :: Maybe MetaId

    The meta variable, if any, holding the type etc.

  • ipSolved :: Bool

    Has this interaction point already been solved?

  • ipClause :: IPClause

    The clause of the interaction point (if any). Used for case splitting.

Instances

Instances details
Eq InteractionPoint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

type InteractionPoints = Map InteractionId InteractionPoint Source #

Data structure managing the interaction points.

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

data Overapplied Source #

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

Instances

Instances details
Eq Overapplied Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: Overapplied -> Overapplied -> Bool

(/=) :: Overapplied -> Overapplied -> Bool

Data Overapplied Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: Overapplied -> Constr

dataTypeOf :: Overapplied -> DataType

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

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

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

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

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

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

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

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

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

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

Show Overapplied Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Overapplied -> ShowS

show :: Overapplied -> String

showList :: [Overapplied] -> ShowS

data IPBoundary' t Source #

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

Constructors

IPBoundary 

Fields

Instances

Instances details
Functor IPBoundary' Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Foldable IPBoundary' Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

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

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

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

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

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

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

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

toList :: IPBoundary' a -> [a]

null :: IPBoundary' a -> Bool

length :: IPBoundary' a -> Int

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

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

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

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

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

Traversable IPBoundary' Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

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

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IPBoundary' t -> c (IPBoundary' t)

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

toConstr :: IPBoundary' t -> Constr

dataTypeOf :: IPBoundary' t -> DataType

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

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

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

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

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

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

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

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

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

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> IPBoundary' t -> ShowS

show :: IPBoundary' t -> String

showList :: [IPBoundary' t] -> ShowS

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

Methods

reify :: MonadReify m => IPBoundary' a -> m (IPBoundary' e) Source #

reifyWhen :: MonadReify m => Bool -> IPBoundary' a -> m (IPBoundary' e) Source #

data IPClause Source #

Which clause is an interaction point located in?

Constructors

IPClause 

Fields

IPNoClause

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

Instances

Instances details
Eq IPClause Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: IPClause -> IPClause -> Bool

(/=) :: IPClause -> IPClause -> Bool

Data IPClause Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: IPClause -> Constr

dataTypeOf :: IPClause -> DataType

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

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

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

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

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

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

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

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

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

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

Signature

data Signature Source #

Constructors

Sig 

Fields

Instances

Instances details
Data Signature Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: Signature -> Constr

dataTypeOf :: Signature -> DataType

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

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

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

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

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

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

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

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

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

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

Show Signature Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Signature -> ShowS

show :: Signature -> String

showList :: [Signature] -> ShowS

KillRange Signature Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj Signature Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Signature -> S Int32 Source #

icod_ :: Signature -> S Int32 Source #

value :: Int32 -> R Signature Source #

InstantiateFull Signature Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

newtype Section Source #

Constructors

Section 

Instances

Instances details
Eq Section 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: Section -> Constr

dataTypeOf :: Section -> DataType

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

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

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

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

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

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

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

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

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

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

Show Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Section -> ShowS

show :: Section -> String

showList :: [Section] -> ShowS

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

Methods

icode :: Section -> S Int32 Source #

icod_ :: Section -> S Int32 Source #

value :: Int32 -> R Section Source #

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

Instances details
Data DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: DisplayForm -> Constr

dataTypeOf :: DisplayForm -> DataType

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

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

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

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

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

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

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

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

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

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

Show DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> DisplayForm -> ShowS

show :: DisplayForm -> String

showList :: [DisplayForm] -> ShowS

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

Methods

icode :: DisplayForm -> S Int32 Source #

icod_ :: DisplayForm -> S Int32 Source #

value :: Int32 -> R DisplayForm Source #

NamesIn DisplayForm Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: DisplayForm -> Set QName Source #

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

Instances details
Data DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: DisplayTerm -> Constr

dataTypeOf :: DisplayTerm -> DataType

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

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

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

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

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

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

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

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

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

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

Show DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> DisplayTerm -> ShowS

show :: DisplayTerm -> String

showList :: [DisplayTerm] -> ShowS

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

Methods

icode :: DisplayTerm -> S Int32 Source #

icod_ :: DisplayTerm -> S Int32 Source #

value :: Int32 -> R DisplayTerm Source #

PrettyTCM DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

NamesIn DisplayTerm Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: DisplayTerm -> Set QName Source #

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

Instances details
Data NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: NLPat -> Constr

dataTypeOf :: NLPat -> DataType

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

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

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

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

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

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

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

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

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

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

Show NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> NLPat -> ShowS

show :: NLPat -> String

showList :: [NLPat] -> ShowS

KillRange NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

DeBruijn NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

deBruijnVar :: Int -> NLPat Source #

debruijnNamedVar :: String -> Int -> NLPat Source #

deBruijnView :: NLPat -> Maybe Int Source #

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

Methods

icode :: NLPat -> S Int32 Source #

icod_ :: NLPat -> S Int32 Source #

value :: Int32 -> R NLPat Source #

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

Methods

nlPatVarsUnder :: Int -> NLPat -> IntSet Source #

nlPatVars :: NLPat -> IntSet Source #

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

Methods

patternFrom :: Relevance -> Int -> Type -> Term -> TCM NLPat Source #

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

Methods

patternFrom :: Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat] Source #

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

Instances details
Data NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: NLPType -> Constr

dataTypeOf :: NLPType -> DataType

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

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

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

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

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

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

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

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

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

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

Show NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> NLPType -> ShowS

show :: NLPType -> String

showList :: [NLPType] -> ShowS

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

Methods

icode :: NLPType -> S Int32 Source #

icod_ :: NLPType -> S Int32 Source #

value :: Int32 -> R NLPType Source #

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

Methods

nlPatVarsUnder :: Int -> NLPType -> IntSet Source #

nlPatVars :: NLPType -> IntSet Source #

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

Instances details
Data NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: NLPSort -> Constr

dataTypeOf :: NLPSort -> DataType

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

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

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

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

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

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

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

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

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

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

Show NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> NLPSort -> ShowS

show :: NLPSort -> String

showList :: [NLPSort] -> ShowS

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

Methods

icode :: NLPSort -> S Int32 Source #

icod_ :: NLPSort -> S Int32 Source #

value :: Int32 -> R NLPSort Source #

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

Methods

nlPatVarsUnder :: Int -> NLPSort -> IntSet Source #

nlPatVars :: NLPSort -> IntSet Source #

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

Instances details
Data RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: RewriteRule -> Constr

dataTypeOf :: RewriteRule -> DataType

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

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

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

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

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

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

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

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

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

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

Show RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> RewriteRule -> ShowS

show :: RewriteRule -> String

showList :: [RewriteRule] -> ShowS

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

Methods

icode :: RewriteRule -> S Int32 Source #

icod_ :: RewriteRule -> S Int32 Source #

value :: Int32 -> R RewriteRule Source #

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

Instances details
Data Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: Definition -> Constr

dataTypeOf :: Definition -> DataType

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

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

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

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

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

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

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

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

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

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

Show Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Definition -> ShowS

show :: Definition -> String

showList :: [Definition] -> ShowS

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

Methods

icode :: Definition -> S Int32 Source #

icod_ :: Definition -> S Int32 Source #

value :: Int32 -> R Definition Source #

NamesIn Definition Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Definition -> Set QName Source #

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

Instances details
Data NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: NumGeneralizableArgs -> Constr

dataTypeOf :: NumGeneralizableArgs -> DataType

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

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

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

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

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

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

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

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

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

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

Show NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> NumGeneralizableArgs -> ShowS

show :: NumGeneralizableArgs -> String

showList :: [NumGeneralizableArgs] -> ShowS

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

Instances details
Eq Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: Polarity -> Polarity -> Bool

(/=) :: Polarity -> Polarity -> Bool

Data Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: Polarity -> Constr

dataTypeOf :: Polarity -> DataType

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

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

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

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

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

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

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

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

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

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

Show Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Polarity -> ShowS

show :: Polarity -> String

showList :: [Polarity] -> ShowS

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

Methods

icode :: Polarity -> S Int32 Source #

icod_ :: Polarity -> S Int32 Source #

value :: Int32 -> R Polarity Source #

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

Instances details
Eq IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: IsForced -> IsForced -> Bool

(/=) :: IsForced -> IsForced -> Bool

Data IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: IsForced -> Constr

dataTypeOf :: IsForced -> DataType

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

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

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

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

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

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

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

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

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

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

Show IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> IsForced -> ShowS

show :: IsForced -> String

showList :: [IsForced] -> ShowS

KillRange IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: IsForced -> S Int32 Source #

icod_ :: IsForced -> S Int32 Source #

value :: Int32 -> R IsForced Source #

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.

Constructors

CompilerPragma Range String 

Instances

Instances details
Eq CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: CompilerPragma -> Constr

dataTypeOf :: CompilerPragma -> DataType

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

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

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

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

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

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

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

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

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

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

Show CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> CompilerPragma -> ShowS

show :: CompilerPragma -> String

showList :: [CompilerPragma] -> ShowS

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

Methods

icode :: CompilerPragma -> S Int32 Source #

icod_ :: CompilerPragma -> S Int32 Source #

value :: Int32 -> R CompilerPragma Source #

type BackendName = String Source #

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

Instances details
Data System Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: System -> Constr

dataTypeOf :: System -> DataType

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

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

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

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

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

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

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

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

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

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

Show System Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> System -> ShowS

show :: System -> String

showList :: [System] -> ShowS

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

Methods

icode :: System -> S Int32 Source #

icod_ :: System -> S Int32 Source #

value :: Int32 -> R System Source #

InstantiateFull System Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => QNamed System -> m [Clause] Source #

reifyWhen :: MonadReify m => Bool -> QNamed System -> m [Clause] Source #

data ExtLamInfo Source #

Additional information for extended lambdas.

Constructors

ExtLamInfo 

Fields

  • extLamModule :: ModuleName

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

  • extLamSys :: !(Maybe System)
     

Instances

Instances details
Data ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: ExtLamInfo -> Constr

dataTypeOf :: ExtLamInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> ExtLamInfo -> ShowS

show :: ExtLamInfo -> String

showList :: [ExtLamInfo] -> ShowS

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

Methods

icode :: ExtLamInfo -> S Int32 Source #

icod_ :: ExtLamInfo -> S Int32 Source #

value :: Int32 -> R ExtLamInfo Source #

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

Instances details
Data Projection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: Projection -> Constr

dataTypeOf :: Projection -> DataType

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

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

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

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

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

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

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

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

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

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

Show Projection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Projection -> ShowS

show :: Projection -> String

showList :: [Projection] -> ShowS

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

Methods

icode :: Projection -> S Int32 Source #

icod_ :: Projection -> S Int32 Source #

value :: Int32 -> R Projection Source #

newtype ProjLams Source #

Abstractions to build projection function (dropping parameters).

Constructors

ProjLams 

Fields

Instances

Instances details
Data ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: ProjLams -> Constr

dataTypeOf :: ProjLams -> DataType

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

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

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

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

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

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

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

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

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

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

Show ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> ProjLams -> ShowS

show :: ProjLams -> String

showList :: [ProjLams] -> ShowS

Null ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: ProjLams Source #

null :: ProjLams -> Bool Source #

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

Methods

icode :: ProjLams -> S Int32 Source #

icod_ :: ProjLams -> S Int32 Source #

value :: Int32 -> R ProjLams Source #

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

Instances details
Eq EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: EtaEquality -> EtaEquality -> Bool

(/=) :: EtaEquality -> EtaEquality -> Bool

Data EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: EtaEquality -> Constr

dataTypeOf :: EtaEquality -> DataType

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

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

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

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

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

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

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

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

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

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

Show EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> EtaEquality -> ShowS

show :: EtaEquality -> String

showList :: [EtaEquality] -> ShowS

KillRange EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: EtaEquality -> S Int32 Source #

icod_ :: EtaEquality -> S Int32 Source #

value :: Int32 -> R EtaEquality Source #

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

Instances details
Enum FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: FunctionFlag -> FunctionFlag -> Bool

(/=) :: FunctionFlag -> FunctionFlag -> Bool

Data FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: FunctionFlag -> Constr

dataTypeOf :: FunctionFlag -> DataType

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

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

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

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

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

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

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

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

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

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

Ord FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> FunctionFlag -> ShowS

show :: FunctionFlag -> String

showList :: [FunctionFlag] -> ShowS

KillRange FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: FunctionFlag -> S Int32 Source #

icod_ :: FunctionFlag -> S Int32 Source #

value :: Int32 -> R FunctionFlag Source #

data CompKit Source #

Constructors

CompKit 

Fields

Instances

Instances details
Eq CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Data CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: CompKit -> Constr

dataTypeOf :: CompKit -> DataType

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

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

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

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

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

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

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

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

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

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

Ord CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: CompKit -> CompKit -> Ordering

(<) :: CompKit -> CompKit -> Bool

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

(>) :: CompKit -> CompKit -> Bool

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

max :: CompKit -> CompKit -> CompKit

min :: CompKit -> CompKit -> CompKit

Show CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> CompKit -> ShowS

show :: CompKit -> String

showList :: [CompKit] -> ShowS

KillRange CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompKit -> S Int32 Source #

icod_ :: CompKit -> S Int32 Source #

value :: Int32 -> R CompKit Source #

NamesIn CompKit Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: CompKit -> Set QName Source #

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

  • funClauses :: [Clause]
     
  • funCompiled :: Maybe CompiledClauses

    Nothing while function is still type-checked. Just cc after type and coverage checking and translation to case trees.

  • funSplitTree :: Maybe SplitTree

    The split tree constructed by the coverage checker. Needed to re-compile the clauses after forcing translation.

  • funTreeless :: Maybe Compiled

    Intermediate representation for compiler backends.

  • funCovering :: [Clause]

    Covering clauses computed by coverage checking. Erased by (IApply) confluence checking(?)

  • funInv :: FunctionInverse
     
  • funMutual :: Maybe [QName]

    Mutually recursive functions, datas and records. Does include this function. Empty list if not recursive. Nothing if not yet computed (by positivity checker).

  • funAbstr :: IsAbstract
     
  • funDelayed :: Delayed

    Are the clauses of this definition delayed?

  • funProjection :: Maybe Projection

    Is it a record projection? If yes, then return the name of the record type and index of the record argument. Start counting with 1, because 0 means that it is already applied to the record. (Can happen in module instantiation.) This information is used in the termination checker.

  • funFlags :: Set FunctionFlag
     
  • funTerminates :: Maybe Bool

    Has this function been termination checked? Did it pass?

  • funExtLam :: Maybe ExtLamInfo

    Is this function generated from an extended lambda? If yes, then return the number of hidden and non-hidden lambda-lifted arguments

  • funWith :: Maybe QName

    Is this a generated with-function? If yes, then what's the name of the parent function.

Datatype 

Fields

Record 

Fields

  • recPars :: Nat

    Number of parameters.

  • recClause :: Maybe Clause

    Was this record type created by a module application? If yes, the clause is its definition (linking back to the original record type).

  • recConHead :: ConHead

    Constructor name and fields.

  • recNamedCon :: Bool

    Does this record have a constructor?

  • recFields :: [Dom QName]

    The record field names.

  • recTel :: Telescope

    The record field telescope. (Includes record parameters.) Note: TelV recTel _ == telView' recConType. Thus, recTel is redundant.

  • recMutual :: Maybe [QName]

    Mutually recursive functions, datas and records. Does include this record. Empty if not recursive. Nothing if not yet computed (by positivity checker).

  • recEtaEquality' :: EtaEquality

    Eta-expand at this record type? False for unguarded recursive records and coinductive records unless the user specifies otherwise.

  • recInduction :: Maybe Induction

    Inductive or CoInductive? Matters only for recursive records. Nothing means that the user did not specify it, which is an error for recursive records.

  • recAbstr :: IsAbstract
     
  • recComp :: CompKit
     
Constructor 

Fields

  • conPars :: Int

    Number of parameters.

  • conArity :: Int

    Number of arguments (excluding parameters).

  • conSrcCon :: ConHead

    Name of (original) constructor and fields. (This might be in a module instance.)

  • conData :: QName

    Name of datatype or record type.

  • conAbstr :: IsAbstract
     
  • conInd :: Induction

    Inductive or coinductive?

  • conComp :: CompKit

    Cubical composition.

  • conProj :: Maybe [QName]

    Projections. Nothing if not yet computed.

  • conForced :: [IsForced]

    Which arguments are forced (i.e. determined by the type of the constructor)? Either this list is empty (if the forcing analysis isn't run), or its length is conArity.

  • conErased :: Maybe [Bool]

    Which arguments are erased at runtime (computed during compilation to treeless)? True means erased, False means retained. Nothing if no erasure analysis has been performed yet. The length of the list is conArity.

Primitive

Primitive or builtin functions.

Fields

Instances

Instances details
Data Defn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: Defn -> Constr

dataTypeOf :: Defn -> DataType

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

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

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

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

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

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

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

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

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

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

Show Defn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Defn -> ShowS

show :: Defn -> String

showList :: [Defn] -> ShowS

Pretty Defn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Defn -> Doc Source #

prettyPrec :: Int -> Defn -> Doc Source #

prettyList :: [Defn] -> Doc Source #

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

Methods

icode :: Defn -> S Int32 Source #

icod_ :: Defn -> S Int32 Source #

value :: Int32 -> R Defn Source #

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.

isMacro :: Defn -> Bool Source #

isEmptyFunction :: Defn -> Bool Source #

Checking whether we are dealing with a function yet to be defined.

newtype Fields Source #

Constructors

Fields [(Name, Type)] 

Instances

Instances details
Null Fields Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: Fields Source #

null :: Fields -> Bool Source #

data Simplification Source #

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

Instances

Instances details
Eq Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: Simplification -> Constr

dataTypeOf :: Simplification -> DataType

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

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

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

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

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

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

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

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

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

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

Show Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Simplification -> ShowS

show :: Simplification -> String

showList :: [Simplification] -> ShowS

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

Instances details
Functor (Reduced no) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

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

Instances details
Functor MaybeReduced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Pretty

data AllowedReduction Source #

Controlling reduce.

Constructors

ProjectionReductions

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

InlineReductions

Functions marked INLINE may be reduced.

CopatternReductions

Copattern definitions may be reduced.

FunctionReductions

Non-recursive functions and primitives may be reduced.

RecursiveReductions

Even recursive functions may be reduced.

LevelReductions

Reduce Level terms.

TypeLevelReductions

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

UnconfirmedReductions

Functions whose termination has not (yet) been confirmed.

NonTerminatingReductions

Functions that have failed termination checking.

Instances

Instances details
Bounded AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Enum AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: AllowedReduction -> Constr

dataTypeOf :: AllowedReduction -> DataType

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

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

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

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

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

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

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

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

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

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

Ord AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> AllowedReduction -> ShowS

show :: AllowedReduction -> String

showList :: [AllowedReduction] -> ShowS

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 

data PrimFun Source #

Instances

Instances details
Abstract PrimFun Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply PrimFun Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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

type InversionMap c = Map TermHead [c] Source #

data FunctionInverse' c Source #

Constructors

NotInjective 
Inverse (InversionMap c) 

Instances

Instances details
Functor FunctionInverse' Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Abstract FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

DropArgs FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.DropArgs

InstantiateFull FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: FunctionInverse' c -> Constr

dataTypeOf :: FunctionInverse' c -> DataType

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

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

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

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

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

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

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

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

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

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> FunctionInverse' c -> ShowS

show :: FunctionInverse' c -> String

showList :: [FunctionInverse' c] -> ShowS

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

Methods

icode :: FunctionInverse' a -> S Int32 Source #

icod_ :: FunctionInverse' a -> S Int32 Source #

value :: Int32 -> R (FunctionInverse' a) Source #

data TermHead Source #

Instances

Instances details
Eq TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: TermHead -> TermHead -> Bool

(/=) :: TermHead -> TermHead -> Bool

Data TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: TermHead -> Constr

dataTypeOf :: TermHead -> DataType

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

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

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

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

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

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

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

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

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

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

Ord TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: TermHead -> TermHead -> Ordering

(<) :: TermHead -> TermHead -> Bool

(<=) :: TermHead -> TermHead -> Bool

(>) :: TermHead -> TermHead -> Bool

(>=) :: TermHead -> TermHead -> Bool

max :: TermHead -> TermHead -> TermHead

min :: TermHead -> TermHead -> TermHead

Show TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> TermHead -> ShowS

show :: TermHead -> String

showList :: [TermHead] -> ShowS

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

Methods

icode :: TermHead -> S Int32 Source #

icod_ :: TermHead -> S Int32 Source #

value :: Int32 -> R TermHead Source #

Mutual blocks

newtype MutualId Source #

Constructors

MutId Int32 

Instances

Instances details
Enum MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: MutualId -> MutualId -> Bool

(/=) :: MutualId -> MutualId -> Bool

Data MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: MutualId -> Constr

dataTypeOf :: MutualId -> DataType

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

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

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

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

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

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

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

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

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

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

Num MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Ord MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: MutualId -> MutualId -> Ordering

(<) :: MutualId -> MutualId -> Bool

(<=) :: MutualId -> MutualId -> Bool

(>) :: MutualId -> MutualId -> Bool

(>=) :: MutualId -> MutualId -> Bool

max :: MutualId -> MutualId -> MutualId

min :: MutualId -> MutualId -> MutualId

Show MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> MutualId -> ShowS

show :: MutualId -> String

showList :: [MutualId] -> ShowS

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

Methods

icode :: MutualId -> S Int32 Source #

icod_ :: MutualId -> S Int32 Source #

value :: Int32 -> R MutualId Source #

Statistics

type Statistics = Map String Integer Source #

Trace

data Call Source #

Instances

Instances details
Data Call Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: Call -> Constr

dataTypeOf :: Call -> DataType

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

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

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

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

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

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

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

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

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

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

Pretty Call Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Call -> Doc Source #

prettyPrec :: Int -> Call -> Doc Source #

prettyList :: [Call] -> Doc Source #

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.

type BuiltinThings pf = Map String (Builtin pf) Source #

data Builtin pf Source #

Constructors

Builtin Term 
Prim pf 

Instances

Instances details
Functor Builtin Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Foldable Builtin Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

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

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

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

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

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

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

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

toList :: Builtin a -> [a]

null :: Builtin a -> Bool

length :: Builtin a -> Int

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

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

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

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

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

Traversable Builtin Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

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

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Builtin pf -> ShowS

show :: Builtin pf -> String

showList :: [Builtin pf] -> ShowS

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Builtin a -> S Int32 Source #

icod_ :: Builtin a -> S Int32 Source #

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

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

Instances details
Eq HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: HighlightingLevel -> Constr

dataTypeOf :: HighlightingLevel -> DataType

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

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

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

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

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

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

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

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

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

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

Ord HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Read HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> HighlightingLevel -> ShowS

show :: HighlightingLevel -> String

showList :: [HighlightingLevel] -> ShowS

data HighlightingMethod Source #

How should highlighting be sent to the user interface?

Constructors

Direct

Via stdout.

Indirect

Both via files and via stdout.

Instances

Instances details
Eq HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: HighlightingMethod -> Constr

dataTypeOf :: HighlightingMethod -> DataType

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

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

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

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

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

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

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

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

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

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

Read HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> HighlightingMethod -> ShowS

show :: HighlightingMethod -> String

showList :: [HighlightingMethod] -> ShowS

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

Instances details
Data TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: TCEnv -> Constr

dataTypeOf :: TCEnv -> DataType

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

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

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

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

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

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

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

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

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

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

LensIsAbstract TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensRelevance TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensQuantity TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensModality TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensTCEnv TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

class LensTCEnv a where Source #

Instances

Instances details
LensTCEnv TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensTCEnv (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data UnquoteFlags Source #

Constructors

UnquoteFlags 

Fields

Instances

Instances details
Data UnquoteFlags Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: UnquoteFlags -> Constr

dataTypeOf :: UnquoteFlags -> DataType

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

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

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

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

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

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

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

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

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

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

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

Instances details
Eq AbstractMode Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: AbstractMode -> AbstractMode -> Bool

(/=) :: AbstractMode -> AbstractMode -> Bool

Data AbstractMode Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: AbstractMode -> Constr

dataTypeOf :: AbstractMode -> DataType

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

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

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

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

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

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

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

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

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

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

Show AbstractMode Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> AbstractMode -> ShowS

show :: AbstractMode -> String

showList :: [AbstractMode] -> ShowS

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

Instances details
Eq ExpandHidden Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: ExpandHidden -> ExpandHidden -> Bool

(/=) :: ExpandHidden -> ExpandHidden -> Bool

Data ExpandHidden Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: ExpandHidden -> Constr

dataTypeOf :: ExpandHidden -> DataType

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

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

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

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

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

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

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

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

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

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

data Candidate Source #

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

Instances

Instances details
Eq Candidate 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

(==) :: Candidate -> Candidate -> Bool

(/=) :: Candidate -> Candidate -> Bool

Data Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: Candidate -> Constr

dataTypeOf :: Candidate -> DataType

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

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

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

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

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

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

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

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

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

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

Show Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Candidate -> ShowS

show :: Candidate -> String

showList :: [Candidate] -> ShowS

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

Instances details
Data Warning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: Warning -> Constr

dataTypeOf :: Warning -> DataType

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

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

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

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

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

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

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

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

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

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

Show Warning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Warning -> ShowS

show :: Warning -> String

showList :: [Warning] -> ShowS

EmbPrj Warning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Warning -> S Int32 Source #

icod_ :: Warning -> S Int32 Source #

value :: Int32 -> R Warning Source #

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

Instances

Instances details
Eq TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: TCWarning -> TCWarning -> Bool

(/=) :: TCWarning -> TCWarning -> Bool

Show TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> TCWarning -> ShowS

show :: TCWarning -> String

showList :: [TCWarning] -> ShowS

HasRange TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: TCWarning -> S Int32 Source #

icod_ :: TCWarning -> S Int32 Source #

value :: Int32 -> R TCWarning Source #

PrettyTCM TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Warning

Type checking errors

data CallInfo Source #

Information about a call.

Constructors

CallInfo 

Fields

Instances

Instances details
Data CallInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: CallInfo -> Constr

dataTypeOf :: CallInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show CallInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> CallInfo -> ShowS

show :: CallInfo -> String

showList :: [CallInfo] -> ShowS

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

Methods

allNames :: CallInfo -> Seq QName Source #

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

Instances details
Data TerminationError Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

toConstr :: TerminationError -> Constr

dataTypeOf :: TerminationError -> DataType

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

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

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

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

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

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

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

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

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

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

Show TerminationError Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> TerminationError -> ShowS

show :: TerminationError -> String

showList :: [TerminationError] -> ShowS

data SplitError Source #

Error when splitting a pattern variable into possible constructor patterns.

Constructors

NotADatatype (Closure Type)

Neither data type nor record.

IrrelevantDatatype (Closure Type)

Data type, but in irrelevant position.

ErasedDatatype Bool (Closure Type)

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

CoinductiveDatatype (Closure Type)

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

UnificationStuck 

Fields

CosplitCatchall

Copattern split with a catchall

CosplitNoTarget

We do not know the target type of the clause.

CosplitNoRecordType (Closure Type)

Target type is not a record type.

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

Instances

Instances details
Show SplitError Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> SplitError -> ShowS

show :: SplitError -> String

showList :: [SplitError] -> ShowS

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"

Instances

Instances details
Show UnificationFailure Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> UnificationFailure -> ShowS

show :: UnificationFailure -> String

showList :: [UnificationFailure] -> ShowS

PrettyTCM UnificationFailure Source # 
Instance details

Defined in Agda.TypeChecking.Errors

data UnquoteError Source #

Constructors

BadVisibility String (Arg Term) 
ConInsteadOfDef QName String String 
DefInsteadOfCon QName String String 
NonCanonical String Term 
BlockedOnMeta TCState MetaId 
UnquotePanic String 

Instances

Instances details
Show UnquoteError Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> UnquoteError -> ShowS

show :: UnquoteError -> String

showList :: [UnquoteError] -> ShowS

data TypeError Source #

Constructors

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

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

ShouldBeAppliedToTheDatatypeParameters Term Term

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

ShouldBeApplicationOf Type QName

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

ConstructorPatternInWrongDatatype QName QName

constructor, datatype

CantResolveOverloadedConstructorsTargetingSameDatatype QName [QName]

Datatype, constructors.

DoesNotConstructAnElementOf QName Type

constructor, type

WrongHidingInLHS

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

WrongHidingInLambda Type

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

WrongHidingInApplication Type

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

WrongNamedArgument (NamedArg Expr) [NamedName]

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

WrongIrrelevanceInLambda

Wrong user-given relevance annotation in lambda.

WrongQuantityInLambda

Wrong user-given quantity annotation in lambda.

WrongCohesionInLambda

Wrong user-given cohesion annotation in lambda.

QuantityMismatch Quantity Quantity

The given quantity does not correspond to the expected quantity.

HidingMismatch Hiding Hiding

The given hiding does not correspond to the expected hiding.

RelevanceMismatch Relevance Relevance

The given relevance does not correspond to the expected relevane.

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

The given type should have been a sort.

ShouldBePi Type

The given type should have been a pi.

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

This sort is not a type expression.

InvalidType Term

This term is not a type expression.

FunctionTypeInSizeUniv Term

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

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

The two function types have different relevance.

UnequalQuantity Comparison Term Term

The two function types have different relevance.

UnequalCohesion Comparison Term Term

The two function types have different cohesion.

UnequalHiding Term Term

The two function types have different hiding.

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

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

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

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

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

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

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

Found module name, expected module name.

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

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

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

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

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

Instances

Instances details
Show TypeError Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> TypeError -> ShowS

show :: TypeError -> String

showList :: [TypeError] -> ShowS

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 

Instances

Instances details
Eq LHSOrPatSyn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: LHSOrPatSyn -> LHSOrPatSyn -> Bool

(/=) :: LHSOrPatSyn -> LHSOrPatSyn -> Bool

Show LHSOrPatSyn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> LHSOrPatSyn -> ShowS

show :: LHSOrPatSyn -> String

showList :: [LHSOrPatSyn] -> ShowS

data TCErr Source #

Type-checking errors.

Constructors

TypeError 

Fields

Exception Range Doc 
IOException TCState Range IOException

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

PatternErr

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

Instances

Instances details
Show TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> TCErr -> ShowS

show :: TCErr -> String

showList :: [TCErr] -> ShowS

Exception TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

toException :: TCErr -> SomeException

fromException :: SomeException -> Maybe TCErr

displayException :: TCErr -> String

Error TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

noMsg :: TCErr Source #

strMsg :: String -> TCErr Source #

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.

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

commandLineOptions :: m CommandLineOptions Source #

Returns the command line options which are currently in effect.

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

Instances

Instances details
HasOptions ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasOptions AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

HasOptions TerM Source # 
Instance details

Defined in Agda.Termination.Monad

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Names

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

Defined in Agda.TypeChecking.Conversion.Pure

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

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

Instances details
Monad ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

return :: a -> ReduceM a

Functor ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

MonadFail ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fail :: String -> ReduceM a

Applicative ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pure :: a -> ReduceM a

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

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

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

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

MonadTCEnv ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadReduce ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ReduceM a Source #

HasOptions ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

ReadTCState ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadAddContext ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

HasBuiltins ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

Methods

getBuiltinThing :: String -> ReduceM (Maybe (Builtin PrimFun)) Source #

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

Instances details
MonadReduce ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ReduceM a Source #

MonadReduce TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

liftReduce :: ReduceM a -> TerM a Source #

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

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> TCMT m a Source #

MonadReduce m => MonadReduce (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

liftReduce :: ReduceM a -> NamesT m a Source #

MonadReduce m => MonadReduce (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadReduce m => MonadReduce (ExceptT err m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ExceptT err m a Source #

MonadReduce m => MonadReduce (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ReaderT r m a Source #

MonadReduce m => MonadReduce (StateT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> StateT w m a Source #

(Monoid w, MonadReduce m) => MonadReduce (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> WriterT w m a Source #

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

Instances details
MonadTCEnv ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadTCEnv AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

MonadTCEnv TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

askTC :: TerM TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> TerM a -> TerM a Source #

MonadTCEnv m => MonadTCEnv (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: MaybeT m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> MaybeT m a -> MaybeT m a Source #

MonadTCEnv m => MonadTCEnv (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: ListT m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> ListT m a -> ListT m a Source #

MonadIO m => MonadTCEnv (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: TCMT m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> TCMT m a -> TCMT m a Source #

MonadTCEnv m => MonadTCEnv (ChangeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: ChangeT m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> ChangeT m a -> ChangeT m a Source #

MonadTCEnv m => MonadTCEnv (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

askTC :: NamesT m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a Source #

MonadTCEnv m => MonadTCEnv (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadTCEnv m => MonadTCEnv (ExceptT err m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: ExceptT err m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> ExceptT err m a -> ExceptT err m a Source #

MonadTCEnv m => MonadTCEnv (IdentityT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: IdentityT m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> IdentityT m a -> IdentityT m a Source #

MonadTCEnv m => MonadTCEnv (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: ReaderT r m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> ReaderT r m a -> ReaderT r m a Source #

MonadTCEnv m => MonadTCEnv (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

Instances details
MonadTCState TerM Source # 
Instance details

Defined in Agda.Termination.Monad

MonadTCState m => MonadTCState (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTC :: MaybeT m TCState Source #

putTC :: TCState -> MaybeT m () Source #

modifyTC :: (TCState -> TCState) -> MaybeT m () Source #

MonadTCState m => MonadTCState (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadIO m => MonadTCState (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadTCState m => MonadTCState (ChangeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadTCState m => MonadTCState (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

MonadTCState m => MonadTCState (ExceptT err m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTC :: ExceptT err m TCState Source #

putTC :: TCState -> ExceptT err m () Source #

modifyTC :: (TCState -> TCState) -> ExceptT err m () Source #

MonadTCState m => MonadTCState (IdentityT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTC :: IdentityT m TCState Source #

putTC :: TCState -> IdentityT m () Source #

modifyTC :: (TCState -> TCState) -> IdentityT m () Source #

MonadTCState m => MonadTCState (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTC :: ReaderT r m TCState Source #

putTC :: TCState -> ReaderT r m () Source #

modifyTC :: (TCState -> TCState) -> ReaderT r 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

Methods

getTC :: WriterT w m TCState Source #

putTC :: TCState -> WriterT w m () Source #

modifyTC :: (TCState -> TCState) -> WriterT w m () Source #

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

Instances details
MonadTrans TCMT Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

lift :: Monad m => m a -> TCMT m a

CatchImpossible TCM Source #

Like catchError, but resets the state completely before running the handler. This means it also loses changes to the stPersistentState.

The intended use is to catch internal errors during debug printing. In debug printing, we are not expecting state changes.

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

catchImpossible :: TCM a -> (Impossible -> TCM a) -> TCM a Source #

catchImpossibleJust :: (Impossible -> Maybe b) -> TCM a -> (b -> TCM a) -> TCM a Source #

handleImpossible :: (Impossible -> TCM a) -> TCM a -> TCM a Source #

handleImpossibleJust :: (Impossible -> Maybe b) -> (b -> TCM a) -> TCM a -> TCM a Source #

MonadFixityError ScopeM Source # 
Instance details

Defined in Agda.Syntax.Scope.Monad

MonadStConcreteNames TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadInteractionPoints TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

MonadAddContext TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> TCM a -> TCM a Source #

addLetBinding' :: Name -> Term -> Dom Type -> TCM a -> TCM a Source #

updateContext :: Substitution -> (Context -> Context) -> TCM a -> TCM a Source #

withFreshName :: Range -> ArgName -> (Name -> TCM a) -> TCM a Source #

MonadDebug TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

MonadStatistics TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> TCM () Source #

MonadWarning TCM Source # 
Instance details

Defined in Agda.TypeChecking.Warnings

Methods

addWarning :: TCWarning -> TCM () Source #

MonadConstraint TCM Source # 
Instance details

Defined in Agda.TypeChecking.Constraints

MonadMetaSolver TCM Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars

MonadError TCErr TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

throwError :: TCErr -> TCM a #

catchError :: TCM a -> (TCErr -> TCM a) -> TCM a #

MonadError TCErr IM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

throwError :: TCErr -> IM a #

catchError :: IM a -> (TCErr -> IM a) -> IM a #

MonadBench Phase TCM Source #

We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking.

Instance details

Defined in Agda.TypeChecking.Monad.Base

HasFresh i => MonadFresh i TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fresh :: TCM i Source #

Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #

Conversion TOM Type (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O) Source #

Conversion TOM Term (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O) Source #

Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #

Conversion TOM [Clause] [([Pat O], MExp O)] Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #

Conversion TOM (Arg Pattern) (Pat O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Arg Pattern -> TOM (Pat O) Source #

Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Arg a -> TOM (Hiding, b) Source #

MonadIO m => Monad (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(>>=) :: TCMT m a -> (a -> TCMT m b) -> TCMT m b

(>>) :: TCMT m a -> TCMT m b -> TCMT m b

return :: a -> TCMT m a

MonadIO m => Functor (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> TCMT m a -> TCMT m b

(<$) :: a -> TCMT m b -> TCMT m a #

MonadIO m => MonadFail (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fail :: String -> TCMT m a

MonadIO m => Applicative (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pure :: a -> TCMT m a

(<*>) :: TCMT m (a -> b) -> TCMT m a -> TCMT m b #

liftA2 :: (a -> b -> c) -> TCMT m a -> TCMT m b -> TCMT m c

(*>) :: TCMT m a -> TCMT m b -> TCMT m b

(<*) :: TCMT m a -> TCMT m b -> TCMT m a

Semigroup (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Warnings

Methods

(<>) :: TCM Doc -> TCM Doc -> TCM Doc #

sconcat :: NonEmpty (TCM Doc) -> TCM Doc

stimes :: Integral b => b -> TCM Doc -> TCM Doc

MonadIO m => MonadIO (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftIO :: IO a -> TCMT m a

Null (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: TCM Doc Source #

null :: TCM Doc -> Bool Source #

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

Methods

getBuiltinThing :: String -> TCMT m (Maybe (Builtin PrimFun)) Source #

TraceS [TCM Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m c -> m c Source #

TraceS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c Source #

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 #

default liftTCM :: (MonadTCM m, MonadTrans t, tcm ~ t m) => TCM a -> tcm a Source #

Instances

Instances details
MonadTCM TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

liftTCM :: TCM a -> TerM a Source #

MonadTCM tcm => MonadTCM (MaybeT tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> MaybeT tcm a Source #

MonadTCM tcm => MonadTCM (ListT tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ListT tcm a Source #

MonadIO m => MonadTCM (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> TCMT m a Source #

MonadTCM tcm => MonadTCM (ChangeT tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ChangeT tcm a Source #

MonadTCM m => MonadTCM (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

liftTCM :: TCM a -> NamesT m a Source #

MonadTCM tcm => MonadTCM (ExceptT err tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ExceptT err tcm a Source #

MonadTCM tcm => MonadTCM (IdentityT tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> IdentityT tcm a Source #

MonadTCM tcm => MonadTCM (ReaderT r tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ReaderT r tcm a Source #

MonadTCM tcm => MonadTCM (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 TCM action (a TCM action which cannot fail) in the initial environment.

forkTCM :: TCM a -> TCM () Source #

Runs the given computation in a separate thread, with a copy of the current state and environment.

Note that Agda sometimes uses actual, mutable state. If the computation given to forkTCM tries to modify this state, then bad things can happen, because accesses are not mutually exclusive. The forkTCM function has been added mainly to allow the thread to read (a snapshot of) the current state in a convenient way.

Note also that exceptions which are raised in the thread are not propagated to the parent, so the thread should not do anything important.

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