Agda.Syntax.Concrete.Generic

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

However, here we use the terminology of Traversable.

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike ()

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike QName

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike Name

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike ModuleApplication

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication

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

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

ExprLike Declaration

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike LamClause

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> LamClause -> LamClause

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

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

ExprLike LHS

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike LamBinding

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike DoStmt

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> DoStmt -> DoStmt

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

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

ExprLike Expr

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike ModuleAssignment

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> ModuleAssignment -> ModuleAssignment

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

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

ExprLike FieldAssignment

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> FieldAssignment -> FieldAssignment

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

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

ExprLike a => ExprLike [a]

Defined in Agda.Syntax.Concrete.Generic

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)

Defined in Agda.Syntax.Concrete.Generic

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)

Defined in Agda.Syntax.Concrete.Generic

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)

Defined in Agda.Syntax.Concrete.Generic

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 (WithHiding a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (WhereClause' a)

Defined in Agda.Syntax.Concrete.Generic

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)

Defined in Agda.Syntax.Concrete.Generic

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)

Defined in Agda.Syntax.Concrete.Generic

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)

Defined in Agda.Syntax.Concrete.Generic

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)

Defined in Agda.Syntax.Concrete.Generic

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)

Defined in Agda.Syntax.Concrete.Generic

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)

Defined in Agda.Syntax.Concrete.Generic

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)

Defined in Agda.Syntax.Concrete.Generic

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 qn, ExprLike e) => ExprLike (RewriteEqn' qn p e)

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> RewriteEqn' qn p e -> RewriteEqn' qn p e

traverseExpr :: Monad m => (Expr -> m Expr) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e)

foldExpr :: Monoid m => (Expr -> m) -> RewriteEqn' qn p e -> m

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

Defined in Agda.Syntax.Concrete.Generic

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