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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Abstract.Views

Contents

Synopsis

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

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.

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 # 
ExprLike 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 # 
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) # 
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 #