Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Syntax.Internal.Elim

Synopsis

data Elim' a
- = Apply (Arg a)
- | Proj ProjOrigin QName
- | IApply a a a
isApplyElim :: Elim' a -> Maybe (Arg a)
isApplyElim' :: Empty -> Elim' a -> Arg a
allApplyElims :: [Elim' a] -> Maybe [Arg a]
splitApplyElims :: [Elim' a] -> ([Arg a], [Elim' a])
class IsProjElim e where
- isProjElim :: e -> Maybe (ProjOrigin, QName)
argsFromElims :: [Elim' t] -> [Arg t]
allProjElims :: [Elim' t] -> Maybe [(ProjOrigin, QName)]

Documentation

data Elim' a Source #

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

Instances details

IsPrefixOf Elims Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Elims -> Elims -> Maybe Elims Source #
MentionsMeta Elim Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Elim -> Bool Source #
PrettyTCM Elim Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Elim -> m Doc Source #
Reduce Elim Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Elim -> ReduceM Elim Source # reduceB' :: Elim -> ReduceM (Blocked Elim) Source #
Foldable Elim' Source #
Instance details 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' Source #
Instance details 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' Source #
Instance details Defined in Agda.Syntax.Internal.Elim Methods fmap :: (a -> b) -> Elim' a -> Elim' b # (<$) :: a -> Elim' b -> Elim' a #
LensOrigin (Elim' a) Source #	This instance cheats on `Proj`, use with care. `Proj`s are always assumed to be `UserWritten`, since they have no `ArgInfo`. Same for IApply
Instance details Defined in Agda.Syntax.Internal.Elim Methods getOrigin :: Elim' a -> Origin Source # setOrigin :: Origin -> Elim' a -> Elim' a Source # mapOrigin :: (Origin -> Origin) -> Elim' a -> Elim' a Source #
GetDefs a => GetDefs (Elim' a) Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Elim' a -> m () Source #
IsProjElim (Elim' a) Source #
Instance details Defined in Agda.Syntax.Internal.Elim Methods isProjElim :: Elim' a -> Maybe (ProjOrigin, QName) Source #
TermLike a => TermLike (Elim' a) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Elim' a -> m (Elim' a) Source # foldTerm :: Monoid m => (Term -> m) -> Elim' a -> m Source #
TermLike a => AllMetas (Elim' a) Source #
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Elim' a -> m Source #
NamesIn a => NamesIn (Elim' a) Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn' :: Monoid m => (QName -> m) -> Elim' a -> m Source #
KillRange a => KillRange (Elim' a) Source #
Instance details Defined in Agda.Syntax.Internal.Elim Methods killRange :: KillRangeT (Elim' a) Source #
Reify i => Reify (Elim' i) Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo (Elim' i) Source # Methods reify :: MonadReify m => Elim' i -> m (ReifiesTo (Elim' i)) Source # reifyWhen :: MonadReify m => Bool -> Elim' i -> m (ReifiesTo (Elim' i)) Source #
AbsTerm a => AbsTerm (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Elim' a -> Elim' a Source #
EqualSy a => EqualSy (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Elim' a -> Elim' a -> Bool Source #
Free t => Free (Elim' t) Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Elim' t -> FreeM a c Source #
PrecomputeFreeVars a => PrecomputeFreeVars (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Elim' a -> FV (Elim' a) Source #
(Reduce a, ForceNotFree a) => ForceNotFree (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Elim' a -> m (Elim' a)
UsableModality a => UsableModality (Elim' a) Source #
Instance details 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 Source #
UsableRelevance a => UsableRelevance (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Elim' a -> m Bool Source #
AnyRigid a => AnyRigid (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Elim' a -> tcm Bool Source #
Occurs a => Occurs (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Elim' a -> OccursM (Elim' a) Source # metaOccurs :: MetaId -> Elim' a -> TCM () Source #
ComputeOccurrences a => ComputeOccurrences (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Elim' a -> OccM OccurrencesBuilder Source #
PrettyTCM (Elim' DisplayTerm) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Elim' DisplayTerm -> m Doc Source #
PrettyTCM (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Elim' NLPat -> m Doc Source #
Instantiate t => Instantiate (Elim' t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Elim' t -> ReduceM (Elim' t) Source #
InstantiateFull t => InstantiateFull (Elim' t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Elim' t -> ReduceM (Elim' t) Source #
IsMeta a => IsMeta (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: Elim' a -> Maybe MetaId Source #
Normalise t => Normalise (Elim' t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Elim' t -> ReduceM (Elim' t) Source #
Simplify t => Simplify (Elim' t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Elim' t -> ReduceM (Elim' t) Source #
GetMatchables a => GetMatchables (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Elim' a -> [QName] Source #
EmbPrj a => EmbPrj (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Elim' a -> S Int32 Source # icod_ :: Elim' a -> S Int32 Source # value :: Int32 -> R (Elim' a) Source #
Subst a => Subst (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg (Elim' a) Source # Methods applySubst :: Substitution' (SubstArg (Elim' a)) -> Elim' a -> Elim' a Source #
SynEq a => SynEq (Elim' a) Source #
Instance details 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) Source #
Instance details Defined in Agda.Syntax.Internal.Elim Methods pretty :: Elim' tm -> Doc Source # prettyPrec :: Int -> Elim' tm -> Doc Source # prettyList :: [Elim' tm] -> Doc Source #
Data a => Data (Elim' a) Source #
Instance details 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) #
Show a => Show (Elim' a) Source #
Instance details 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) Source #
Instance details Defined in Agda.Syntax.Internal.Elim Methods rnf :: Elim' a -> () #
(Subst a, Eq a) => Eq (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Elim' a -> Elim' a -> Bool # (/=) :: Elim' a -> Elim' a -> Bool #
(Subst a, Ord a) => Ord (Elim' a) Source #
Instance details 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) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: Arg DeBruijnPattern -> Elim' NLPat Source #
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat Source #
ToNLPat a b => ToNLPat (Elim' a) (Elim' b) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: Elim' a -> Elim' b Source #
NLPatToTerm p a => NLPatToTerm (Elim' p) (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => Elim' p -> m (Elim' a) Source #
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, Elims -> Term) [Elim' NLPat] Elims Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> (Type, Elims -> Term) -> [Elim' NLPat] -> Elims -> NLM () Source #
type ReifiesTo (Elim' i) Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (Elim' i) = Elim' (ReifiesTo i)
type SubstArg (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Elim' a) = SubstArg a

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

Drop Apply constructor. (Safe)

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

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

Drop Apply constructors. (Safe)

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

Split at first non-Apply

class IsProjElim e where Source #

Methods

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

Instances

Instances details

IsProjElim (Elim' a) Source #
Instance details Defined in Agda.Syntax.Internal.Elim Methods isProjElim :: Elim' a -> Maybe (ProjOrigin, QName) Source #
IsProjElim e => IsProjElim (MaybeReduced e) Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods isProjElim :: MaybeReduced e -> Maybe (ProjOrigin, QName) Source #

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

Discards Proj f entries.

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

Drop Proj constructors. (Safe)