Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Internal.Generic

Description

Tree traversal for internal syntax.

Synopsis

class TermLike a where
- traverseTermM :: Monad m => (Term -> m Term) -> a -> m a
- foldTerm :: Monoid m => (Term -> m) -> a -> m
copyTerm :: (TermLike a, Monad m) => a -> m a

Documentation

class TermLike a where Source #

Generic term traversal.

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

Minimal complete definition

Nothing

Methods

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

Generic traversal with post-traversal action. Ignores sorts.

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

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

Generic fold, ignoring sorts.

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

Instances

Instances details

TermLike Bool Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Bool -> m Bool Source # foldTerm :: Monoid m => (Term -> m) -> Bool -> m Source #
TermLike Char Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Char -> m Char Source # foldTerm :: Monoid m => (Term -> m) -> Char -> m Source #
TermLike Int Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Int -> m Int Source # foldTerm :: Monoid m => (Term -> m) -> Int -> m Source #
TermLike Integer Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Integer -> m Integer Source # foldTerm :: Monoid m => (Term -> m) -> Integer -> m Source #
TermLike QName Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> QName -> m QName Source # foldTerm :: Monoid m => (Term -> m) -> QName -> m Source #
TermLike EqualityView Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> EqualityView -> m EqualityView Source # foldTerm :: Monoid m => (Term -> m) -> EqualityView -> m Source #
TermLike PlusLevel Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> PlusLevel -> m PlusLevel Source # foldTerm :: Monoid m => (Term -> m) -> PlusLevel -> m Source #
TermLike Level Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Level -> m Level Source # foldTerm :: Monoid m => (Term -> m) -> Level -> m Source #
TermLike Sort Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Sort -> m Sort Source # foldTerm :: Monoid m => (Term -> m) -> Sort -> m Source #
TermLike Type Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Type -> m Type Source # foldTerm :: Monoid m => (Term -> m) -> Type -> m Source #
TermLike Term Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Term -> m Term Source # foldTerm :: Monoid m => (Term -> m) -> Term -> m Source #
TermLike CompareAs Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods traverseTermM :: Monad m => (Term -> m Term) -> CompareAs -> m CompareAs Source # foldTerm :: Monoid m => (Term -> m) -> CompareAs -> m Source #
TermLike Constraint Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods traverseTermM :: Monad m => (Term -> m Term) -> Constraint -> m Constraint Source # foldTerm :: Monoid m => (Term -> m) -> Constraint -> m Source #
TermLike Nat Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods traverseTermM :: Monad m => (Term -> m Term) -> Nat -> m Nat Source # foldTerm :: Monoid m => (Term -> m) -> Nat -> m Source #
TermLike a => TermLike [a] Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> [a] -> m [a] Source # foldTerm :: Monoid m => (Term -> m) -> [a] -> m Source #
TermLike a => TermLike (Maybe a) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Maybe a -> m (Maybe a) Source # foldTerm :: Monoid m => (Term -> m) -> Maybe a -> m Source #
TermLike a => TermLike (Arg a) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Arg a -> m (Arg a) Source # foldTerm :: Monoid m => (Term -> m) -> Arg a -> m Source #
TermLike a => TermLike (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> WithHiding a -> m (WithHiding a) Source # foldTerm :: Monoid m => (Term -> m) -> WithHiding a -> m Source #
TermLike a => TermLike (Elim' a) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Elim' a -> m (Elim' a) Source # foldTerm :: Monoid m => (Term -> m) -> Elim' a -> m Source #
TermLike a => TermLike (Blocked a) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Blocked a -> m (Blocked a) Source # foldTerm :: Monoid m => (Term -> m) -> Blocked a -> m Source #
TermLike a => TermLike (Tele a) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Tele a -> m (Tele a) Source # foldTerm :: Monoid m => (Term -> m) -> Tele a -> m Source #
TermLike a => TermLike (Abs a) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Abs a -> m (Abs a) Source # foldTerm :: Monoid m => (Term -> m) -> Abs a -> m Source #
TermLike a => TermLike (Dom a) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Dom a -> m (Dom a) Source # foldTerm :: Monoid m => (Term -> m) -> Dom a -> m Source #
TermLike a => TermLike (CompiledClauses' a) Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods traverseTermM :: Monad m => (Term -> m Term) -> CompiledClauses' a -> m (CompiledClauses' a) Source # foldTerm :: Monoid m => (Term -> m) -> CompiledClauses' a -> m Source #
TermLike a => TermLike (Case a) Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods traverseTermM :: Monad m => (Term -> m Term) -> Case a -> m (Case a) Source # foldTerm :: Monoid m => (Term -> m) -> Case a -> m Source #
TermLike a => TermLike (WithArity a) Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods traverseTermM :: Monad m => (Term -> m Term) -> WithArity a -> m (WithArity a) Source # foldTerm :: Monoid m => (Term -> m) -> WithArity a -> m Source #
(TermLike a, TermLike b) => TermLike (a, b) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> (a, b) -> m (a, b) Source # foldTerm :: Monoid m => (Term -> m) -> (a, b) -> m Source #
(TermLike a, TermLike b, TermLike c) => TermLike (a, b, c) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> (a, b, c) -> m (a, b, c) Source # foldTerm :: Monoid m => (Term -> m) -> (a, b, c) -> m Source #
(TermLike a, TermLike b, TermLike c, TermLike d) => TermLike (a, b, c, d) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> (a, b, c, d) -> m (a, b, c, d) Source # foldTerm :: Monoid m => (Term -> m) -> (a, b, c, d) -> m Source #

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

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