Agda-2.5.3: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Abstract.Views

Contents

Synopsis

Documentation

appView :: Expr -> AppView Source #

Gather applications to expose head and spine.

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

data LamView Source #

Collects plain lambdas.

Constructors

LamView [(LamInfo, LamBinding)] Expr 

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

Gather top-level AsPatterns to expose underlying pattern.

isSet :: Expr -> Bool Source #

Check whether we are dealing with a universe.

unScope :: Expr -> Expr Source #

Remove top ScopedExpr wrappers.

deepUnscope :: ExprLike a => a -> a Source #

Remove ScopedExpr wrappers everywhere.

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

Traversal

class ExprLike a where Source #

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 Source #

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 Source #

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

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

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

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

Instances

ExprLike Void Source # 

Methods

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

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

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

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

ExprLike ModuleName Source # 
ExprLike QName Source # 

Methods

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

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

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

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

ExprLike LHS Source # 

Methods

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

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

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

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

ExprLike SpineLHS Source # 

Methods

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

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

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

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

ExprLike RHS Source # 

Methods

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

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

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

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

ExprLike TypedBinding Source # 
ExprLike TypedBindings Source # 
ExprLike LamBinding Source # 
ExprLike LetBinding Source # 
ExprLike Pragma Source # 

Methods

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

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

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

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

ExprLike ModuleApplication Source # 
ExprLike Declaration Source # 
ExprLike Expr Source # 

Methods

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

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

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

mapExpr :: (Expr -> Expr) -> Expr -> Expr Source #

ExprLike a => ExprLike [a] Source # 

Methods

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

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

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

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

ExprLike a => ExprLike (Arg a) Source # 

Methods

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

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

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

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

ExprLike a => ExprLike (FieldAssignment' a) Source # 
ExprLike a => ExprLike (Pattern' a) Source # 

Methods

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

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

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

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

ExprLike a => ExprLike (LHSCore' a) Source # 

Methods

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

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

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

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

ExprLike a => ExprLike (Clause' a) Source # 

Methods

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

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

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

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

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

Methods

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

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

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

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

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

Methods

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

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

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

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

ExprLike a => ExprLike (Named x a) Source # 

Methods

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

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

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

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