Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Internal.Generic

Description

Tree traversal for internal syntax.

Synopsis

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

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 #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Bool -> m Bool # foldTerm :: Monoid m => (Term -> m) -> Bool -> m #
TermLike Char #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Char -> m Char # foldTerm :: Monoid m => (Term -> m) -> Char -> m #
TermLike Int #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Int -> m Int # foldTerm :: Monoid m => (Term -> m) -> Int -> m #
TermLike Integer #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Integer -> m Integer # foldTerm :: Monoid m => (Term -> m) -> Integer -> m #
TermLike QName #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> QName -> m QName # foldTerm :: Monoid m => (Term -> m) -> QName -> m #
TermLike EqualityView #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> EqualityView -> m EqualityView # foldTerm :: Monoid m => (Term -> m) -> EqualityView -> m #
TermLike LevelAtom #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> LevelAtom -> m LevelAtom # foldTerm :: Monoid m => (Term -> m) -> LevelAtom -> m #
TermLike PlusLevel #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> PlusLevel -> m PlusLevel # foldTerm :: Monoid m => (Term -> m) -> PlusLevel -> m #
TermLike Level #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Level -> m Level # foldTerm :: Monoid m => (Term -> m) -> Level -> m #
TermLike Type #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Type -> m Type # foldTerm :: Monoid m => (Term -> m) -> Type -> m #
TermLike Term #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Term -> m Term # foldTerm :: Monoid m => (Term -> m) -> Term -> m #
TermLike Constraint #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods traverseTermM :: Monad m => (Term -> m Term) -> Constraint -> m Constraint # foldTerm :: Monoid m => (Term -> m) -> Constraint -> m #
TermLike Nat #
Instance details Defined in Agda.TypeChecking.Primitive Methods traverseTermM :: Monad m => (Term -> m Term) -> Nat -> m Nat # foldTerm :: Monoid m => (Term -> m) -> Nat -> m #
TermLike a => TermLike [a] #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> [a] -> m [a] # foldTerm :: Monoid m => (Term -> m) -> [a] -> m #
TermLike a => TermLike (Maybe a) #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Maybe a -> m (Maybe a) # foldTerm :: Monoid m => (Term -> m) -> Maybe a -> m #
TermLike a => TermLike (Dom a) #
Instance details Defined in Agda.Syntax.Internal.Generic 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) #
Instance details Defined in Agda.Syntax.Internal.Generic 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) #
Instance details Defined in Agda.Syntax.Internal.Generic 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) #
Instance details Defined in Agda.Syntax.Internal.Generic 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) #
Instance details Defined in Agda.Syntax.Internal.Generic 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) #
Instance details Defined in Agda.TypeChecking.CompiledClause 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) #
Instance details Defined in Agda.TypeChecking.CompiledClause 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) #
Instance details Defined in Agda.TypeChecking.CompiledClause 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) #
Instance details Defined in Agda.Syntax.Internal.Generic 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) #
Instance details Defined in Agda.Syntax.Internal.Generic 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) #
Instance details Defined in Agda.Syntax.Internal.Generic 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.