Agda-2.6.1.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Internal.Generic

Description

Tree traversal for internal syntax.

Synopsis

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 LevelAtom Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

foldTerm :: Monoid m => (Term -> m) -> LevelAtom -> 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 (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 (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 (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.