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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Concrete.Generic

Contents

Description

Generic traversal and reduce for concrete syntax, in the style of Agda.Syntax.Internal.Generic.

However, here we use the terminology of Traversable.

Synopsis

Documentation

class ExprLike a where #

Generic traversals for concrete expressions.

Note: does not go into patterns!

Minimal complete definition

mapExpr

Methods

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

This corresponds to map.

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

This corresponds to mapM.

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

This is a reduce.

Instances

ExprLike Bool # 

Methods

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

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

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

ExprLike QName # 

Methods

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

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

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

ExprLike Name # 

Methods

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

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

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

ExprLike ModuleApplication # 
ExprLike Declaration # 

Methods

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

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

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

ExprLike LHS # 

Methods

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

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

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

ExprLike TypedBindings # 
ExprLike LamBinding # 

Methods

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

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

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

ExprLike Expr # 

Methods

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

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

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

ExprLike ModuleAssignment # 
ExprLike FieldAssignment # 
ExprLike a => ExprLike [a] # 

Methods

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

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

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

ExprLike a => ExprLike (Maybe a) # 

Methods

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

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

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

ExprLike a => ExprLike (MaybePlaceholder a) # 

Methods

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

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

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

ExprLike a => ExprLike (Arg a) # 

Methods

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

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

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

ExprLike a => ExprLike (WhereClause' a) # 

Methods

mapExpr :: (Expr -> Expr) -> WhereClause' a -> WhereClause' a #

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

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

ExprLike a => ExprLike (RHS' a) # 

Methods

mapExpr :: (Expr -> Expr) -> RHS' a -> RHS' a #

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

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

ExprLike a => ExprLike (TypedBinding' a) # 

Methods

mapExpr :: (Expr -> Expr) -> TypedBinding' a -> TypedBinding' a #

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

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

ExprLike a => ExprLike (OpApp a) # 

Methods

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

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

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

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

Methods

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

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

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

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

Methods

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

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

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

ExprLike a => ExprLike (Named name a) # 

Methods

mapExpr :: (Expr -> Expr) -> Named name a -> Named name a #

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

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

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

Methods

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

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

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

(ExprLike a, ExprLike b, ExprLike c, ExprLike d) => ExprLike (a, b, c, d) # 

Methods

mapExpr :: (Expr -> Expr) -> (a, b, c, d) -> (a, b, c, d) #

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

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

Instances for things that do not contain expressions.

Instances for functors.

Interesting instances