Agda-2.6.2.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
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 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 () 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 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 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 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 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 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 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 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 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 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 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 (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 (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 (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 (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 (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 (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 (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 (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 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 (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 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 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 #

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

Instances for things that do not contain expressions.

Instances for collections and decorations.

Interesting instances