Agda.Syntax.Abstract.Views

Documentation

data AppView

Constructors

Application Expr [NamedArg Expr]

appView :: Expr -> AppView

Gather applications to expose head and spine.

Note: everything is an application, possibly of itself to 0 arguments

maybeProjTurnPostfix :: Expr -> Maybe Expr

unAppView :: AppView -> Expr

asView :: Pattern -> ([Name], Pattern)

Gather top-level AsPatterns to expose underlying pattern.

isSet :: Expr -> Bool

Check whether we are dealing with a universe.

unScope :: Expr -> Expr

Remove top ScopedExpr wrappers.

deepUnscope :: ExprLike a => a -> a

Remove ScopedExpr wrappers everywhere.

NB: Unless the implementation of ExprLike for clauses has been finished, this does not work for clauses yet.

deepUnscopeDecls :: [Declaration] -> [Declaration]

deepUnscopeDecl :: Declaration -> [Declaration]

Traversal

class ExprLike a where

Apply an expression rewriting to every subexpression, inside-out. See Agda.Syntax.Internal.Generic.

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> a -> m a

The first expression is pre-traversal, the second one post-traversal.

recurseExpr :: (Traversable f, ExprLike a', a ~ f a', Applicative m) => (Expr -> m Expr -> m Expr) -> a -> m a

The first expression is pre-traversal, the second one post-traversal.

foldExpr :: Monoid m => (Expr -> m) -> a -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> a -> m a

mapExpr :: (Expr -> Expr) -> a -> a

Instances

ExprLike Void

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Void -> m Void

foldExpr :: Monoid m => (Expr -> m) -> Void -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> Void -> m Void

mapExpr :: (Expr -> Expr) -> Void -> Void

ExprLike ModuleName

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> ModuleName -> m ModuleName

foldExpr :: Monoid m => (Expr -> m) -> ModuleName -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> ModuleName -> m ModuleName

mapExpr :: (Expr -> Expr) -> ModuleName -> ModuleName

ExprLike QName

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> QName -> m QName

foldExpr :: Monoid m => (Expr -> m) -> QName -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> QName -> m QName

mapExpr :: (Expr -> Expr) -> QName -> QName

ExprLike LHS

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LHS -> m LHS

foldExpr :: Monoid m => (Expr -> m) -> LHS -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> LHS -> m LHS

mapExpr :: (Expr -> Expr) -> LHS -> LHS

ExprLike SpineLHS

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> SpineLHS -> m SpineLHS

foldExpr :: Monoid m => (Expr -> m) -> SpineLHS -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> SpineLHS -> m SpineLHS

mapExpr :: (Expr -> Expr) -> SpineLHS -> SpineLHS

ExprLike RHS

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> RHS -> m RHS

foldExpr :: Monoid m => (Expr -> m) -> RHS -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> RHS -> m RHS

mapExpr :: (Expr -> Expr) -> RHS -> RHS

ExprLike TypedBinding

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> TypedBinding -> m TypedBinding

foldExpr :: Monoid m => (Expr -> m) -> TypedBinding -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> TypedBinding -> m TypedBinding

mapExpr :: (Expr -> Expr) -> TypedBinding -> TypedBinding

ExprLike TypedBindings

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> TypedBindings -> m TypedBindings

foldExpr :: Monoid m => (Expr -> m) -> TypedBindings -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> TypedBindings -> m TypedBindings

mapExpr :: (Expr -> Expr) -> TypedBindings -> TypedBindings

ExprLike LamBinding

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LamBinding -> m LamBinding

foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding

mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding

ExprLike LetBinding

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LetBinding -> m LetBinding

foldExpr :: Monoid m => (Expr -> m) -> LetBinding -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> LetBinding -> m LetBinding

mapExpr :: (Expr -> Expr) -> LetBinding -> LetBinding

ExprLike Pragma

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Pragma -> m Pragma

foldExpr :: Monoid m => (Expr -> m) -> Pragma -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> Pragma -> m Pragma

mapExpr :: (Expr -> Expr) -> Pragma -> Pragma

ExprLike ModuleApplication

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> ModuleApplication -> m ModuleApplication

foldExpr :: Monoid m => (Expr -> m) -> ModuleApplication -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> ModuleApplication -> m ModuleApplication

mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication

ExprLike Declaration

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Declaration -> m Declaration

foldExpr :: Monoid m => (Expr -> m) -> Declaration -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> Declaration -> m Declaration

mapExpr :: (Expr -> Expr) -> Declaration -> Declaration

ExprLike Expr

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Expr -> m Expr

foldExpr :: Monoid m => (Expr -> m) -> Expr -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> Expr -> m Expr

mapExpr :: (Expr -> Expr) -> Expr -> Expr

ExprLike a => ExprLike [a]

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> [a] -> m [a]

foldExpr :: Monoid m => (Expr -> m) -> [a] -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> [a] -> m [a]

mapExpr :: (Expr -> Expr) -> [a] -> [a]

ExprLike a => ExprLike (Arg a)

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Arg a -> m (Arg a)

foldExpr :: Monoid m => (Expr -> m) -> Arg a -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> Arg a -> m (Arg a)

mapExpr :: (Expr -> Expr) -> Arg a -> Arg a

ExprLike a => ExprLike (FieldAssignment' a)

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> FieldAssignment' a -> m (FieldAssignment' a)

foldExpr :: Monoid m => (Expr -> m) -> FieldAssignment' a -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> FieldAssignment' a -> m (FieldAssignment' a)

mapExpr :: (Expr -> Expr) -> FieldAssignment' a -> FieldAssignment' a

ExprLike a => ExprLike (Pattern' a)

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Pattern' a -> m (Pattern' a)

foldExpr :: Monoid m => (Expr -> m) -> Pattern' a -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> Pattern' a -> m (Pattern' a)

mapExpr :: (Expr -> Expr) -> Pattern' a -> Pattern' a

ExprLike a => ExprLike (LHSCore' a)

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LHSCore' a -> m (LHSCore' a)

foldExpr :: Monoid m => (Expr -> m) -> LHSCore' a -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> LHSCore' a -> m (LHSCore' a)

mapExpr :: (Expr -> Expr) -> LHSCore' a -> LHSCore' a

ExprLike a => ExprLike (Clause' a)

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Clause' a -> m (Clause' a)

foldExpr :: Monoid m => (Expr -> m) -> Clause' a -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> Clause' a -> m (Clause' a)

mapExpr :: (Expr -> Expr) -> Clause' a -> Clause' a

(ExprLike a, ExprLike b) => ExprLike (Either a b)

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Either a b -> m (Either a b)

foldExpr :: Monoid m => (Expr -> m) -> Either a b -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> Either a b -> m (Either a b)

mapExpr :: (Expr -> Expr) -> Either a b -> Either a b

(ExprLike a, ExprLike b) => ExprLike (a, b)

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> (a, b) -> m (a, b)

foldExpr :: Monoid m => (Expr -> m) -> (a, b) -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> (a, b) -> m (a, b)

mapExpr :: (Expr -> Expr) -> (a, b) -> (a, b)

ExprLike a => ExprLike (Named x a)

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Named x a -> m (Named x a)

foldExpr :: Monoid m => (Expr -> m) -> Named x a -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> Named x a -> m (Named x a)

mapExpr :: (Expr -> Expr) -> Named x a -> Named x a