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

Functor Elim'

Defined in Agda.Syntax.Internal.Elim

Methods

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

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

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)

PrettyTCM Elim

Defined in Agda.TypeChecking.Pretty

Methods

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

MentionsMeta Elim

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Elim -> Bool

Reduce Elim

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Elim -> ReduceM Elim

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

IsPrefixOf Elims

Defined in Agda.TypeChecking.Abstract

Methods

isPrefixOf :: Elims -> Elims -> Maybe Elims

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data a => Data (Elim' a)

Defined in Agda.Syntax.Internal.Elim

Methods

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

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

toConstr :: Elim' a -> Constr

dataTypeOf :: Elim' a -> DataType

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

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

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

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

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

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

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

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

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

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

(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

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

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

KillRange a => KillRange (Elim' a)

Defined in Agda.Syntax.Internal.Elim

Methods

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

IsProjElim (Elim' a)

Defined in Agda.Syntax.Internal.Elim

Methods

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

PrecomputeFreeVars a => PrecomputeFreeVars (Elim' a)

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

Free t => Free (Elim' t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

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

GetDefs a => GetDefs (Elim' a)

Defined in Agda.Syntax.Internal.Defs

Methods

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

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)

PrettyTCM (Elim' NLPat)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Elim' DisplayTerm)

Defined in Agda.TypeChecking.Pretty

Methods

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

NamesIn a => NamesIn (Elim' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Elim' a -> m

InstantiateFull t => InstantiateFull (Elim' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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)

IsMeta a => IsMeta (Elim' a)

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Elim' a -> Maybe MetaId

Instantiate t => Instantiate (Elim' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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)

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

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Elim' a -> m (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))

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

GetMatchables a => GetMatchables (Elim' a)

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

getMatchables :: Elim' a -> [QName]

ComputeOccurrences a => ComputeOccurrences (Elim' a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Elim' a -> OccM OccurrencesBuilder

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

EqualSy a => EqualSy (Elim' a)

Defined in Agda.TypeChecking.Abstract

Methods

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

AbsTerm a => AbsTerm (Elim' a)

Defined in Agda.TypeChecking.Abstract

Methods

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

ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat)

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat

ToNLPat (Arg DeBruijnPattern) (Elim' NLPat)

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Arg 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 SubstArg (Elim' a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Elim' a) = SubstArg a

type ReifiesTo (Elim' i)

Defined in Agda.Syntax.Translation.InternalToAbstract

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

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

Drop Apply constructor. (Safe)

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

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)