Agda.Syntax.Internal.Elim

Documentation

data Elim' a

Eliminations, subsuming applications and projections.

Constructors

Apply (Arg a)

Application.

Proj ProjOrigin QName

Projection. QName is name of a record projection.

IApply a a a

IApply x y r, x and y are the endpoints

Instances

IsPrefixOf Elims

Defined in Agda.TypeChecking.Abstract

Methods

isPrefixOf :: Elims -> Elims -> Maybe Elims

MentionsMeta Elim

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Elim -> Bool

PrettyTCM Elim

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Elim -> m Doc

Reduce Elim

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Elim -> ReduceM Elim

reduceB' :: Elim -> ReduceM (Blocked Elim)

Foldable Elim'

Defined in Agda.Syntax.Internal.Elim

Methods

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

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

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

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

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

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

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

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

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

toList :: Elim' a -> [a]

null :: Elim' a -> Bool

length :: Elim' a -> Int

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

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

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

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

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

Traversable Elim'

Defined in Agda.Syntax.Internal.Elim

Methods

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

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

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

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

Functor Elim'

Defined in Agda.Syntax.Internal.Elim

Methods

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

(<$) :: a -> Elim' b -> Elim' a

LensOrigin (Elim' a)

This instance cheats on Proj, use with care. Projs are always assumed to be UserWritten, since they have no ArgInfo. Same for IApply

Defined in Agda.Syntax.Internal.Elim

Methods

getOrigin :: Elim' a -> Origin

setOrigin :: Origin -> Elim' a -> Elim' a

mapOrigin :: (Origin -> Origin) -> Elim' a -> Elim' a

GetDefs a => GetDefs (Elim' a)

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => Elim' a -> m ()

IsProjElim (Elim' a)

Defined in Agda.Syntax.Internal.Elim

Methods

isProjElim :: Elim' a -> Maybe (ProjOrigin, QName)

TermLike a => TermLike (Elim' a)

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Elim' a -> m (Elim' a)

foldTerm :: Monoid m => (Term -> m) -> Elim' a -> m

TermLike a => AllMetas (Elim' a)

Defined in Agda.Syntax.Internal.MetaVars

Methods

allMetas :: Monoid m => (MetaId -> m) -> Elim' a -> m

NamesIn a => NamesIn (Elim' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Elim' a -> m

KillRange a => KillRange (Elim' a)

Defined in Agda.Syntax.Internal.Elim

Methods

killRange :: KillRangeT (Elim' a)

Reify i => Reify (Elim' i)

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Elim' i)

Methods

reify :: MonadReify m => Elim' i -> m (ReifiesTo (Elim' i))

reifyWhen :: MonadReify m => Bool -> Elim' i -> m (ReifiesTo (Elim' i))

AbsTerm a => AbsTerm (Elim' a)

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Elim' a -> Elim' a

EqualSy a => EqualSy (Elim' a)

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Elim' a -> Elim' a -> Bool

Free t => Free (Elim' t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Elim' t -> FreeM a c

PrecomputeFreeVars a => PrecomputeFreeVars (Elim' a)

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Elim' a -> FV (Elim' a)

(Reduce a, ForceNotFree a) => ForceNotFree (Elim' a)

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Elim' a -> m (Elim' a)

UsableModality a => UsableModality (Elim' a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Elim' a -> m Bool

UsableRelevance a => UsableRelevance (Elim' a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Elim' a -> m Bool

AnyRigid a => AnyRigid (Elim' a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Elim' a -> tcm Bool

Occurs a => Occurs (Elim' a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Elim' a -> OccursM (Elim' a)

metaOccurs :: MetaId -> Elim' a -> TCM ()

ComputeOccurrences a => ComputeOccurrences (Elim' a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Elim' a -> OccM OccurrencesBuilder

PrettyTCM (Elim' DisplayTerm)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Elim' DisplayTerm -> m Doc

PrettyTCM (Elim' NLPat)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Elim' NLPat -> m Doc

Instantiate t => Instantiate (Elim' t)

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Elim' t -> ReduceM (Elim' t)

InstantiateFull t => InstantiateFull (Elim' t)

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Elim' t -> ReduceM (Elim' t)

IsMeta a => IsMeta (Elim' a)

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Elim' a -> Maybe MetaId

Normalise t => Normalise (Elim' t)

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Elim' t -> ReduceM (Elim' t)

Simplify t => Simplify (Elim' t)

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Elim' t -> ReduceM (Elim' t)

GetMatchables a => GetMatchables (Elim' a)

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

getMatchables :: Elim' a -> [QName]

EmbPrj a => EmbPrj (Elim' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Elim' a -> S Int32

icod_ :: Elim' a -> S Int32

value :: Int32 -> R (Elim' a)

Subst a => Subst (Elim' a)

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Elim' a)

Methods

applySubst :: Substitution' (SubstArg (Elim' a)) -> Elim' a -> Elim' a

SynEq a => SynEq (Elim' a)

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a)

synEq' :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a)

Pretty tm => Pretty (Elim' tm)

Defined in Agda.Syntax.Internal.Elim

Methods

pretty :: Elim' tm -> Doc

prettyPrec :: Int -> Elim' tm -> Doc

prettyList :: [Elim' tm] -> Doc

Show a => Show (Elim' a)

Defined in Agda.Syntax.Internal.Elim

Methods

showsPrec :: Int -> Elim' a -> ShowS

show :: Elim' a -> String

showList :: [Elim' a] -> ShowS

NFData a => NFData (Elim' a)

Defined in Agda.Syntax.Internal.Elim

Methods

rnf :: Elim' a -> ()

(Subst a, Eq a) => Eq (Elim' a)

Defined in Agda.TypeChecking.Substitute

Methods

(==) :: Elim' a -> Elim' a -> Bool

(/=) :: Elim' a -> Elim' a -> Bool

(Subst a, Ord a) => Ord (Elim' a)

Defined in Agda.TypeChecking.Substitute

Methods

compare :: Elim' a -> Elim' a -> Ordering

(<) :: Elim' a -> Elim' a -> Bool

(<=) :: Elim' a -> Elim' a -> Bool

(>) :: Elim' a -> Elim' a -> Bool

(>=) :: Elim' a -> Elim' a -> Bool

max :: Elim' a -> Elim' a -> Elim' a

min :: Elim' a -> Elim' a -> Elim' a

ToNLPat (Arg DeBruijnPattern) (Elim' NLPat)

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Arg DeBruijnPattern -> Elim' NLPat

ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat)

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat

ToNLPat a b => ToNLPat (Elim' a) (Elim' b)

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Elim' a -> Elim' b

NLPatToTerm p a => NLPatToTerm (Elim' p) (Elim' a)

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatToTerm :: PureTCM m => Elim' p -> m (Elim' a)

PatternFrom (Type, Term) Elims [Elim' NLPat]

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

Match (Type, Elims -> Term) [Elim' NLPat] Elims

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

type ReifiesTo (Elim' i)

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (Elim' i) = Elim' (ReifiesTo i)

type SubstArg (Elim' a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Elim' a) = SubstArg a

isApplyElim :: Elim' a -> Maybe (Arg a)

Drop Apply constructor. (Safe)

isApplyElim' :: Empty -> Elim' a -> Arg a

isProperApplyElim :: Elim' a -> Bool

Only Apply variant.

allApplyElims :: [Elim' a] -> Maybe [Arg a]

Drop Apply constructors. (Safe)

splitApplyElims :: [Elim' a] -> ([Arg a], [Elim' a])

Split at first non-Apply

class IsProjElim e where

Methods

isProjElim :: e -> Maybe (ProjOrigin, QName)

Instances

IsProjElim (Elim' a)

Defined in Agda.Syntax.Internal.Elim

Methods

isProjElim :: Elim' a -> Maybe (ProjOrigin, QName)

IsProjElim e => IsProjElim (MaybeReduced e)

Defined in Agda.TypeChecking.Monad.Base

Methods

isProjElim :: MaybeReduced e -> Maybe (ProjOrigin, QName)

argsFromElims :: [Elim' t] -> [Arg t]

Discards Proj f entries.

allProjElims :: [Elim' t] -> Maybe [(ProjOrigin, QName)]

Drop Proj constructors. (Safe)