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

Safe HaskellNone
LanguageHaskell98

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

Generic traversals for concrete expressions.

Note: does not go into patterns!

Minimal complete definition

mapExpr

Methods

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

This corresponds to map.

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

This corresponds to mapM.

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

This is a reduce.

Instances

ExprLike Bool Source # 

Methods

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

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

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

ExprLike QName Source # 

Methods

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

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

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

ExprLike Name Source # 

Methods

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

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

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

ExprLike ModuleApplication Source # 
ExprLike Declaration Source # 
ExprLike LHS Source # 

Methods

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

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

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

ExprLike TypedBindings Source # 
ExprLike LamBinding Source # 
ExprLike Expr Source # 

Methods

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

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

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

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

Methods

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

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

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

ExprLike a => ExprLike (Maybe a) Source # 

Methods

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

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

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

ExprLike a => ExprLike (MaybePlaceholder a) Source # 
ExprLike a => ExprLike (Arg a) Source # 

Methods

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

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

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

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

Methods

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

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

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

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

Methods

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

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

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

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

Methods

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

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

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

ExprLike a => ExprLike (OpApp a) Source # 

Methods

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

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

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

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

Methods

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

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

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

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

Methods

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

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

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

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

Methods

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

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

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

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

Methods

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

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

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

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

Methods

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

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

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

Instances for things that do not contain expressions.

Instances for functors.

Interesting instances