Agda-2.6.2.2.20230105: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Concrete.Generic

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

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.

Interesting instances