Agda-2.6.20240714: 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 :: 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

ExprLike ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

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

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 #