Agda-2.6.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Concrete.Generic

Contents

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

mapExpr

Methods

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

This corresponds to map.

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

This corresponds to mapM.

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

This is a reduce.

Instances
ExprLike Bool Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike () Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

ExprLike Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

ExprLike LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

ExprLike DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

ExprLike FieldAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

ExprLike a => ExprLike [a] Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (MaybePlaceholder a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

ExprLike a => ExprLike (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (WhereClause' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (RHS' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (TypedBinding' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike a => ExprLike (OpApp a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

foldExpr :: Monoid m => (Expr -> m) -> OpApp a -> m 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 #

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

foldExpr :: Monoid m => (Expr -> m) -> Either a b -> m 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 #

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

foldExpr :: Monoid m => (Expr -> m) -> (a, b) -> m 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 #

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

foldExpr :: Monoid m => (Expr -> m) -> Named name a -> m 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 #

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

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

(ExprLike qn, ExprLike e) => ExprLike (RewriteEqn' qn p e) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

foldExpr :: Monoid m => (Expr -> m) -> RewriteEqn' qn p e -> m 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 #

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

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

Instances for things that do not contain expressions.

Instances for functors.

Interesting instances