Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Syntax.Concrete.Generic

Contents

Instances for things that do not contain expressions.
Instances for collections and decorations.
Interesting instances

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

class ExprLike a where
- mapExpr :: (Expr -> Expr) -> a -> a
- foldExpr :: Monoid m => (Expr -> m) -> a -> m
- traverseExpr :: Monad m => (Expr -> m Expr) -> a -> m a

Documentation

class ExprLike a where Source #

Generic traversals for concrete expressions.

Note: does not go into patterns!

Minimal complete definition

Nothing

Methods

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

This corresponds to map.

default mapExpr :: (Functor t, ExprLike b, t b ~ a) => (Expr -> Expr) -> a -> a Source #

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

This corresponds to foldMap.

default foldExpr :: (Monoid m, Foldable t, ExprLike b, t b ~ a) => (Expr -> m) -> a -> m Source #

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

This corresponds to mapM.

default traverseExpr :: (Monad m, Traversable t, ExprLike b, t b ~ a) => (Expr -> m Expr) -> a -> m a Source #

Instances

Instances details

ExprLike Declaration Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Declaration -> Declaration Source # foldExpr :: Monoid m => (Expr -> m) -> Declaration -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Declaration -> m Declaration Source #
ExprLike DoStmt Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> DoStmt -> DoStmt Source # foldExpr :: Monoid m => (Expr -> m) -> DoStmt -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> DoStmt -> m DoStmt Source #
ExprLike Expr Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Expr -> Expr Source # foldExpr :: Monoid m => (Expr -> m) -> Expr -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Expr -> m Expr Source #
ExprLike FieldAssignment Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> FieldAssignment -> FieldAssignment Source # foldExpr :: Monoid m => (Expr -> m) -> FieldAssignment -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> FieldAssignment -> m FieldAssignment Source #
ExprLike LHS Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LHS -> LHS Source # foldExpr :: Monoid m => (Expr -> m) -> LHS -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> LHS -> m LHS Source #
ExprLike LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding Source # foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding Source #
ExprLike LamClause Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LamClause -> LamClause Source # foldExpr :: Monoid m => (Expr -> m) -> LamClause -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> LamClause -> m LamClause Source #
ExprLike ModuleApplication Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication Source # foldExpr :: Monoid m => (Expr -> m) -> ModuleApplication -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> ModuleApplication -> m ModuleApplication Source #
ExprLike ModuleAssignment Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> ModuleAssignment -> ModuleAssignment Source # foldExpr :: Monoid m => (Expr -> m) -> ModuleAssignment -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> ModuleAssignment -> m ModuleAssignment Source #
ExprLike Name Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Name -> Name Source # foldExpr :: Monoid m => (Expr -> m) -> Name -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Name -> m Name Source #
ExprLike QName Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> QName -> QName Source # foldExpr :: Monoid m => (Expr -> m) -> QName -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> QName -> m QName Source #
ExprLike () Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> () -> () Source # foldExpr :: Monoid m => (Expr -> m) -> () -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> () -> m () Source #
ExprLike Bool Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Bool -> Bool Source # foldExpr :: Monoid m => (Expr -> m) -> Bool -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Bool -> m Bool Source #
ExprLike a => ExprLike (Arg a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Arg a -> Arg a Source # foldExpr :: Monoid m => (Expr -> m) -> Arg a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Arg a -> m (Arg a) Source #
ExprLike a => ExprLike (MaybePlaceholder a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> MaybePlaceholder a -> MaybePlaceholder a Source # foldExpr :: Monoid m => (Expr -> m) -> MaybePlaceholder a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> MaybePlaceholder a -> m (MaybePlaceholder a) Source #
ExprLike a => ExprLike (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> WithHiding a -> WithHiding a Source # foldExpr :: Monoid m => (Expr -> m) -> WithHiding a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> WithHiding a -> m (WithHiding a) Source #
ExprLike a => ExprLike (OpApp a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> OpApp a -> OpApp a Source # foldExpr :: Monoid m => (Expr -> m) -> OpApp a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> OpApp a -> m (OpApp a) Source #
ExprLike a => ExprLike (RHS' a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> RHS' a -> RHS' a Source # foldExpr :: Monoid m => (Expr -> m) -> RHS' a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> RHS' a -> m (RHS' a) Source #
ExprLike a => ExprLike (TypedBinding' a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> TypedBinding' a -> TypedBinding' a Source # foldExpr :: Monoid m => (Expr -> m) -> TypedBinding' a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> TypedBinding' a -> m (TypedBinding' a) Source #
ExprLike a => ExprLike (WhereClause' a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> WhereClause' a -> WhereClause' a Source # foldExpr :: Monoid m => (Expr -> m) -> WhereClause' a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> WhereClause' a -> m (WhereClause' a) Source #
ExprLike a => ExprLike (List1 a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> List1 a -> List1 a Source # foldExpr :: Monoid m => (Expr -> m) -> List1 a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> List1 a -> m (List1 a) Source #
ExprLike a => ExprLike (List2 a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> List2 a -> List2 a Source # foldExpr :: Monoid m => (Expr -> m) -> List2 a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> List2 a -> m (List2 a) Source #
ExprLike a => ExprLike (Maybe a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Maybe a -> Maybe a Source # foldExpr :: Monoid m => (Expr -> m) -> Maybe a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Maybe a -> m (Maybe a) Source #
ExprLike a => ExprLike [a] Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> [a] -> [a] Source # foldExpr :: Monoid m => (Expr -> m) -> [a] -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> [a] -> m [a] Source #
ExprLike a => ExprLike (Named name a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Named name a -> Named name a Source # foldExpr :: Monoid m => (Expr -> m) -> Named name a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Named name a -> m (Named name a) Source #
(ExprLike a, ExprLike b) => ExprLike (Either a b) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Either a b -> Either a b Source # foldExpr :: Monoid m => (Expr -> m) -> Either a b -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Either a b -> m (Either a b) Source #
(ExprLike a, ExprLike b) => ExprLike (a, b) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> (a, b) -> (a, b) Source # foldExpr :: Monoid m => (Expr -> m) -> (a, b) -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> (a, b) -> m (a, b) Source #
(ExprLike a, ExprLike b, ExprLike c) => ExprLike (a, b, c) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> (a, b, c) -> (a, b, c) Source # foldExpr :: Monoid m => (Expr -> m) -> (a, b, c) -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> (a, b, c) -> m (a, b, c) Source #
(ExprLike qn, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e Source # foldExpr :: Monoid m => (Expr -> m) -> RewriteEqn' qn nm p e -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> RewriteEqn' qn nm p e -> m (RewriteEqn' qn nm p e) Source #
(ExprLike a, ExprLike b, ExprLike c, ExprLike d) => ExprLike (a, b, c, d) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> (a, b, c, d) -> (a, b, c, d) Source # foldExpr :: Monoid m => (Expr -> m) -> (a, b, c, d) -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> (a, b, c, d) -> m (a, b, c, d) Source #

Instances for things that do not contain expressions.

Instances for collections and decorations.

Documentation

Instances

Instances for things that do not contain expressions.

Instances for collections and decorations.

Interesting instances