Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Concrete.Generic

Contents

Instances for things that do not contain expressions.
Instances for functors.
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

Documentation

class ExprLike a where #

Generic traversals for concrete expressions.

Note: does not go into patterns!

Minimal complete definition

mapExpr

Methods

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

This corresponds to map.

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

This corresponds to mapM.

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

This is a reduce.

Instances

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

Instances for things that do not contain expressions.

Documentation

Instances for things that do not contain expressions.

Instances for functors.

Interesting instances