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

Nothing

Methods

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

This corresponds to map.

default mapExpr :: forall (t :: Type -> Type) b. (Functor t, ExprLike b, t b ~ a) => (Expr -> Expr) -> a -> a

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

This corresponds to foldMap.

default foldExpr :: forall m (t :: Type -> Type) b. (Monoid m, Foldable t, ExprLike b, t b ~ a) => (Expr -> m) -> a -> m

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

This corresponds to mapM.

default traverseExpr :: forall m (t :: Type -> Type) b. (Monad m, Traversable t, ExprLike b, t b ~ a) => (Expr -> m Expr) -> a -> m a

Instances

ExprLike Declaration

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike DoStmt

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike Expr

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike FieldAssignment

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike LHS

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike LamBinding

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike LamClause

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike ModuleApplication

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike ModuleAssignment

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike Name

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike QName

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike ()

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike Bool

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (Arg a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (MaybePlaceholder a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (Ranged a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (WithHiding a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (OpApp a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (RHS' a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (TypedBinding' a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (WhereClause' a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (List1 a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (List2 a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (Maybe a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike [a]

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (Named name a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

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

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> Either a b -> 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)

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

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

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

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

(ExprLike qn, ExprLike e) => ExprLike (RewriteEqn' qn nm p e)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

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

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

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

class FoldDecl a where

Minimal complete definition

Nothing

Methods

foldDecl :: Monoid m => (Declaration -> m) -> a -> m

Collect declarations and subdeclarations, transitively. Prefix-order tree traversal.

default foldDecl :: forall m (t :: Type -> Type) b. (Monoid m, Foldable t, FoldDecl b, t b ~ a) => (Declaration -> m) -> a -> m

Instances

FoldDecl Declaration

Defined in Agda.Syntax.Concrete.Generic

Methods

foldDecl :: Monoid m => (Declaration -> m) -> Declaration -> m

FoldDecl a => FoldDecl (WhereClause' a)

Defined in Agda.Syntax.Concrete.Generic

Methods

foldDecl :: Monoid m => (Declaration -> m) -> WhereClause' a -> m

FoldDecl a => FoldDecl (List1 a)

Defined in Agda.Syntax.Concrete.Generic

Methods

foldDecl :: Monoid m => (Declaration -> m) -> List1 a -> m

FoldDecl a => FoldDecl (List2 a)

Defined in Agda.Syntax.Concrete.Generic

Methods

foldDecl :: Monoid m => (Declaration -> m) -> List2 a -> m

FoldDecl a => FoldDecl [a]

Defined in Agda.Syntax.Concrete.Generic

Methods

foldDecl :: Monoid m => (Declaration -> m) -> [a] -> m

class TraverseDecl a where

Minimal complete definition

Nothing

Methods

preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> a -> m a

Update declarations and their subdeclarations. Prefix-order traversal: traverses subdeclarations of updated declaration.

default preTraverseDecl :: forall m (t :: Type -> Type) b. (Monad m, Traversable t, TraverseDecl b, t b ~ a) => (Declaration -> m Declaration) -> a -> m a

Instances

TraverseDecl Declaration

Defined in Agda.Syntax.Concrete.Generic

Methods

preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> Declaration -> m Declaration

TraverseDecl a => TraverseDecl (WhereClause' a)

Defined in Agda.Syntax.Concrete.Generic

Methods

preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> WhereClause' a -> m (WhereClause' a)

TraverseDecl a => TraverseDecl (List1 a)

Defined in Agda.Syntax.Concrete.Generic

Methods

preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> List1 a -> m (List1 a)

TraverseDecl a => TraverseDecl (List2 a)

Defined in Agda.Syntax.Concrete.Generic

Methods

preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> List2 a -> m (List2 a)

TraverseDecl a => TraverseDecl [a]

Defined in Agda.Syntax.Concrete.Generic

Methods

preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> [a] -> m [a]