Agda.Syntax.Internal.Generic

Tree traversal for internal syntax.

Documentation

class TermLike a where

Generic term traversal.

Note: ignores sorts in terms! (Does not traverse into or collect from them.)

Methods

traverseTermM :: Monad m => (Term -> m Term) -> a -> m a

Generic traversal with post-traversal action. Ignores sorts.

traverseTermM :: (Monad m, Traversable f, TermLike b, f b ~ a) => (Term -> m Term) -> a -> m a

Generic traversal with post-traversal action. Ignores sorts.

foldTerm :: Monoid m => (Term -> m) -> a -> m

Generic fold, ignoring sorts.

foldTerm :: (Monoid m, Foldable f, TermLike b, f b ~ a) => (Term -> m) -> a -> m

Generic fold, ignoring sorts.

Instances

TermLike Bool

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Bool -> m Bool

foldTerm :: Monoid m => (Term -> m) -> Bool -> m

TermLike Char

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Char -> m Char

foldTerm :: Monoid m => (Term -> m) -> Char -> m

TermLike Int

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Int -> m Int

foldTerm :: Monoid m => (Term -> m) -> Int -> m

TermLike Integer

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Integer -> m Integer

foldTerm :: Monoid m => (Term -> m) -> Integer -> m

TermLike QName

Methods

traverseTermM :: Monad m => (Term -> m Term) -> QName -> m QName

foldTerm :: Monoid m => (Term -> m) -> QName -> m

TermLike EqualityView

Methods

traverseTermM :: Monad m => (Term -> m Term) -> EqualityView -> m EqualityView

foldTerm :: Monoid m => (Term -> m) -> EqualityView -> m

TermLike LevelAtom

Methods

traverseTermM :: Monad m => (Term -> m Term) -> LevelAtom -> m LevelAtom

foldTerm :: Monoid m => (Term -> m) -> LevelAtom -> m

TermLike PlusLevel

Methods

traverseTermM :: Monad m => (Term -> m Term) -> PlusLevel -> m PlusLevel

foldTerm :: Monoid m => (Term -> m) -> PlusLevel -> m

TermLike Level

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Level -> m Level

foldTerm :: Monoid m => (Term -> m) -> Level -> m

TermLike Type

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Type -> m Type

foldTerm :: Monoid m => (Term -> m) -> Type -> m

TermLike Term

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Term -> m Term

foldTerm :: Monoid m => (Term -> m) -> Term -> m

TermLike Constraint

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Constraint -> m Constraint

foldTerm :: Monoid m => (Term -> m) -> Constraint -> m

TermLike Nat

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Nat -> m Nat

foldTerm :: Monoid m => (Term -> m) -> Nat -> m

TermLike a => TermLike [a]

Methods

traverseTermM :: Monad m => (Term -> m Term) -> [a] -> m [a]

foldTerm :: Monoid m => (Term -> m) -> [a] -> m

TermLike a => TermLike (Maybe a)

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Maybe a -> m (Maybe a)

foldTerm :: Monoid m => (Term -> m) -> Maybe a -> m

TermLike a => TermLike (Ptr a)

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Ptr a -> m (Ptr a)

foldTerm :: Monoid m => (Term -> m) -> Ptr a -> m

TermLike a => TermLike (Dom a)

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Dom a -> m (Dom a)

foldTerm :: Monoid m => (Term -> m) -> Dom a -> m

TermLike a => TermLike (Arg a)

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Arg a -> m (Arg a)

foldTerm :: Monoid m => (Term -> m) -> Arg a -> m

TermLike a => TermLike (Blocked a)

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Blocked a -> m (Blocked a)

foldTerm :: Monoid m => (Term -> m) -> Blocked a -> m

TermLike a => TermLike (Abs a)

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Abs a -> m (Abs a)

foldTerm :: Monoid m => (Term -> m) -> Abs a -> m

TermLike a => TermLike (Elim' a)

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Elim' a -> m (Elim' a)

foldTerm :: Monoid m => (Term -> m) -> Elim' a -> m

TermLike a => TermLike (CompiledClauses' a)

Methods

traverseTermM :: Monad m => (Term -> m Term) -> CompiledClauses' a -> m (CompiledClauses' a)

foldTerm :: Monoid m => (Term -> m) -> CompiledClauses' a -> m

TermLike a => TermLike (Case a)

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Case a -> m (Case a)

foldTerm :: Monoid m => (Term -> m) -> Case a -> m

TermLike a => TermLike (WithArity a)

Methods

traverseTermM :: Monad m => (Term -> m Term) -> WithArity a -> m (WithArity a)

foldTerm :: Monoid m => (Term -> m) -> WithArity a -> m

(TermLike a, TermLike b) => TermLike (a, b)

Methods

traverseTermM :: Monad m => (Term -> m Term) -> (a, b) -> m (a, b)

foldTerm :: Monoid m => (Term -> m) -> (a, b) -> m

(TermLike a, TermLike b, TermLike c) => TermLike (a, b, c)

Methods

traverseTermM :: Monad m => (Term -> m Term) -> (a, b, c) -> m (a, b, c)

foldTerm :: Monoid m => (Term -> m) -> (a, b, c) -> m

(TermLike a, TermLike b, TermLike c, TermLike d) => TermLike (a, b, c, d)

Methods

traverseTermM :: Monad m => (Term -> m Term) -> (a, b, c, d) -> m (a, b, c, d)

foldTerm :: Monoid m => (Term -> m) -> (a, b, c, d) -> m

copyTerm :: (TermLike a, Monad m) => a -> m a

Put it in a monad to make it possible to do strictly.