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

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 :: Expr -> Expr

Remove ScopedExpr wrappers everywhere.

Traversal

class ExprLike a where

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

Minimal complete definition

foldExpr, traverseExpr

Methods

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

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

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

Instances

ExprLike TypedBinding

ExprLike TypedBindings

ExprLike LamBinding

ExprLike LetBinding

ExprLike Expr

ExprLike a => ExprLike [a]

ExprLike (Pattern' a)

TODO: currently does not go into patterns.

ExprLike (Clause' a)

TODO: currently does not go into clauses.

ExprLike a => ExprLike (x, a)

ExprLike a => ExprLike (Named x a)

ExprLike a => ExprLike (Arg c a)

TODO: currently does not go into colors.