Safe Haskell	None
Language	Haskell2010

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

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
class FoldDecl a where
- foldDecl :: Monoid m => (Declaration -> m) -> a -> m
class TraverseDecl a where
- preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> 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 :: forall (t :: Type -> Type) b. (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 :: forall m (t :: Type -> Type) b. (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 :: forall m (t :: Type -> Type) b. (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 (Ranged a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Ranged a -> Ranged a Source # foldExpr :: Monoid m => (Expr -> m) -> Ranged a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Ranged a -> m (Ranged 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 (TacticAttribute' a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> TacticAttribute' a -> TacticAttribute' a Source # foldExpr :: Monoid m => (Expr -> m) -> TacticAttribute' a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> TacticAttribute' a -> m (TacticAttribute' 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 #

class FoldDecl a where Source #

Minimal complete definition

Nothing

Methods

foldDecl :: Monoid m => (Declaration -> m) -> a -> m Source #

Collect declarations and subdeclarations, transitively. Prefix-order tree traversal.

default foldDecl :: forall m (t :: Type -> Type) b. (Monoid m, Foldable t, FoldDecl b, t b ~ a) => (Declaration -> m) -> a -> m Source #

Instances

Instances details

FoldDecl Declaration Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods foldDecl :: Monoid m => (Declaration -> m) -> Declaration -> m Source #
FoldDecl a => FoldDecl (WhereClause' a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods foldDecl :: Monoid m => (Declaration -> m) -> WhereClause' a -> m Source #
FoldDecl a => FoldDecl (List1 a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods foldDecl :: Monoid m => (Declaration -> m) -> List1 a -> m Source #
FoldDecl a => FoldDecl (List2 a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods foldDecl :: Monoid m => (Declaration -> m) -> List2 a -> m Source #
FoldDecl a => FoldDecl [a] Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods foldDecl :: Monoid m => (Declaration -> m) -> [a] -> m Source #

class TraverseDecl a where Source #

Minimal complete definition

Nothing

Methods

preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> a -> m a Source #

Update declarations and their subdeclarations. Prefix-order traversal: traverses subdeclarations of updated declaration.

default preTraverseDecl :: forall m (t :: Type -> Type) b. (Monad m, Traversable t, TraverseDecl b, t b ~ a) => (Declaration -> m Declaration) -> a -> m a Source #

Instances

Instances details

TraverseDecl Declaration Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> Declaration -> m Declaration Source #
TraverseDecl a => TraverseDecl (WhereClause' a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> WhereClause' a -> m (WhereClause' a) Source #
TraverseDecl a => TraverseDecl (List1 a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> List1 a -> m (List1 a) Source #
TraverseDecl a => TraverseDecl (List2 a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> List2 a -> m (List2 a) Source #
TraverseDecl a => TraverseDecl [a] Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> [a] -> m [a] Source #