Agda.Syntax.Abstract.Views

Documentation

data AppView' arg

Constructors

Application Expr [NamedArg arg]

Instances

Functor AppView'

Defined in Agda.Syntax.Abstract.Views

Methods

fmap :: (a -> b) -> AppView' a -> AppView' b

(<$) :: a -> AppView' b -> AppView' a

type AppView = AppView' Expr

appView :: Expr -> AppView

Gather applications to expose head and spine.

Note: everything is an application, possibly of itself to 0 arguments

appView' :: Expr -> AppView' (AppInfo, Expr)

maybeProjTurnPostfix :: Expr -> Maybe Expr

unAppView :: AppView -> Expr

data LamView

Collects plain lambdas.

Constructors

LamView [LamBinding] Expr

lamView :: Expr -> LamView

asView :: Pattern -> ([Name], Pattern)

Gather top-level AsPatterns to expose underlying pattern.

isSet :: Expr -> Bool

Check whether we are dealing with a universe.

unScope :: Expr -> Expr

Remove top ScopedExpr wrappers.

deepUnscope :: ExprLike a => a -> a

Remove ScopedExpr wrappers everywhere.

NB: Unless the implementation of ExprLike for clauses has been finished, this does not work for clauses yet.

deepUnscopeDecls :: [Declaration] -> [Declaration]

deepUnscopeDecl :: Declaration -> [Declaration]

Traversal

class ExprLike a where

Apply an expression rewriting to every subexpression, inside-out. See Agda.Syntax.Internal.Generic.

Minimal complete definition

Nothing

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> a -> m a

The first expression is pre-traversal, the second one post-traversal.

default recurseExpr :: (Traversable f, ExprLike a', a ~ f a', Applicative m) => (Expr -> m Expr -> m Expr) -> a -> m a

foldExpr :: Monoid m => (Expr -> m) -> a -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> a -> m a

mapExpr :: (Expr -> Expr) -> a -> a

Instances

ExprLike Void

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Void -> m Void

foldExpr :: Monoid m => (Expr -> m) -> Void -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Void -> m Void

mapExpr :: (Expr -> Expr) -> Void -> Void

ExprLike ModuleName

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> ModuleName -> m ModuleName

foldExpr :: Monoid m => (Expr -> m) -> ModuleName -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> ModuleName -> m ModuleName

mapExpr :: (Expr -> Expr) -> ModuleName -> ModuleName

ExprLike QName

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> QName -> m QName

foldExpr :: Monoid m => (Expr -> m) -> QName -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> QName -> m QName

mapExpr :: (Expr -> Expr) -> QName -> QName

ExprLike LHS

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LHS -> m LHS

foldExpr :: Monoid m => (Expr -> m) -> LHS -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LHS -> m LHS

mapExpr :: (Expr -> Expr) -> LHS -> LHS

ExprLike SpineLHS

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> SpineLHS -> m SpineLHS

foldExpr :: Monoid m => (Expr -> m) -> SpineLHS -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> SpineLHS -> m SpineLHS

mapExpr :: (Expr -> Expr) -> SpineLHS -> SpineLHS

ExprLike RHS

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> RHS -> m RHS

foldExpr :: Monoid m => (Expr -> m) -> RHS -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> RHS -> m RHS

mapExpr :: (Expr -> Expr) -> RHS -> RHS

ExprLike WhereDeclarations

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> WhereDeclarations -> m WhereDeclarations

foldExpr :: Monoid m => (Expr -> m) -> WhereDeclarations -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> WhereDeclarations -> m WhereDeclarations

mapExpr :: (Expr -> Expr) -> WhereDeclarations -> WhereDeclarations

ExprLike DataDefParams

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> DataDefParams -> m DataDefParams

foldExpr :: Monoid m => (Expr -> m) -> DataDefParams -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> DataDefParams -> m DataDefParams

mapExpr :: (Expr -> Expr) -> DataDefParams -> DataDefParams

ExprLike GeneralizeTelescope

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> GeneralizeTelescope -> m GeneralizeTelescope

foldExpr :: Monoid m => (Expr -> m) -> GeneralizeTelescope -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> GeneralizeTelescope -> m GeneralizeTelescope

mapExpr :: (Expr -> Expr) -> GeneralizeTelescope -> GeneralizeTelescope

ExprLike TypedBinding

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> TypedBinding -> m TypedBinding

foldExpr :: Monoid m => (Expr -> m) -> TypedBinding -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> TypedBinding -> m TypedBinding

mapExpr :: (Expr -> Expr) -> TypedBinding -> TypedBinding

ExprLike LamBinding

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LamBinding -> m LamBinding

foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LamBinding -> m LamBinding

mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding

ExprLike LetBinding

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LetBinding -> m LetBinding

foldExpr :: Monoid m => (Expr -> m) -> LetBinding -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LetBinding -> m LetBinding

mapExpr :: (Expr -> Expr) -> LetBinding -> LetBinding

ExprLike Pragma

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Pragma -> m Pragma

foldExpr :: Monoid m => (Expr -> m) -> Pragma -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Pragma -> m Pragma

mapExpr :: (Expr -> Expr) -> Pragma -> Pragma

ExprLike ModuleApplication

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> ModuleApplication -> m ModuleApplication

foldExpr :: Monoid m => (Expr -> m) -> ModuleApplication -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> ModuleApplication -> m ModuleApplication

mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication

ExprLike Declaration

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Declaration -> m Declaration

foldExpr :: Monoid m => (Expr -> m) -> Declaration -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Declaration -> m Declaration

mapExpr :: (Expr -> Expr) -> Declaration -> Declaration

ExprLike Expr

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Expr -> m Expr

foldExpr :: Monoid m => (Expr -> m) -> Expr -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Expr -> m Expr

mapExpr :: (Expr -> Expr) -> Expr -> Expr

ExprLike a => ExprLike [a]

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> [a] -> m [a]

foldExpr :: Monoid m => (Expr -> m) -> [a] -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> [a] -> m [a]

mapExpr :: (Expr -> Expr) -> [a] -> [a]

ExprLike a => ExprLike (Maybe a)

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Maybe a -> m (Maybe a)

foldExpr :: Monoid m => (Expr -> m) -> Maybe a -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Maybe a -> m (Maybe a)

mapExpr :: (Expr -> Expr) -> Maybe a -> Maybe a

ExprLike a => ExprLike (Arg a)

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Arg a -> m (Arg a)

foldExpr :: Monoid m => (Expr -> m) -> Arg a -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Arg a -> m (Arg a)

mapExpr :: (Expr -> Expr) -> Arg a -> Arg a

ExprLike a => ExprLike (WithHiding a)

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> WithHiding a -> m (WithHiding a)

foldExpr :: Monoid m => (Expr -> m) -> WithHiding a -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> WithHiding a -> m (WithHiding a)

mapExpr :: (Expr -> Expr) -> WithHiding a -> WithHiding a

ExprLike a => ExprLike (FieldAssignment' a)

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> FieldAssignment' a -> m (FieldAssignment' a)

foldExpr :: Monoid m => (Expr -> m) -> FieldAssignment' a -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> FieldAssignment' a -> m (FieldAssignment' a)

mapExpr :: (Expr -> Expr) -> FieldAssignment' a -> FieldAssignment' a

ExprLike a => ExprLike (Pattern' a)

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Pattern' a -> m (Pattern' a)

foldExpr :: Monoid m => (Expr -> m) -> Pattern' a -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Pattern' a -> m (Pattern' a)

mapExpr :: (Expr -> Expr) -> Pattern' a -> Pattern' a

ExprLike a => ExprLike (LHSCore' a)

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LHSCore' a -> m (LHSCore' a)

foldExpr :: Monoid m => (Expr -> m) -> LHSCore' a -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LHSCore' a -> m (LHSCore' a)

mapExpr :: (Expr -> Expr) -> LHSCore' a -> LHSCore' a

ExprLike a => ExprLike (Clause' a)

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Clause' a -> m (Clause' a)

foldExpr :: Monoid m => (Expr -> m) -> Clause' a -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Clause' a -> m (Clause' a)

mapExpr :: (Expr -> Expr) -> Clause' a -> Clause' a

(ExprLike a, ExprLike b) => ExprLike (Either a b)

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Either a b -> m (Either a b)

foldExpr :: Monoid m => (Expr -> m) -> Either a b -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Either a b -> m (Either a b)

mapExpr :: (Expr -> Expr) -> Either a b -> Either a b

(ExprLike a, ExprLike b) => ExprLike (a, b)

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> (a, b) -> m (a, b)

foldExpr :: Monoid m => (Expr -> m) -> (a, b) -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> (a, b) -> m (a, b)

mapExpr :: (Expr -> Expr) -> (a, b) -> (a, b)

ExprLike a => ExprLike (Named x a)

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Named x a -> m (Named x a)

foldExpr :: Monoid m => (Expr -> m) -> Named x a -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Named x a -> m (Named x a)

mapExpr :: (Expr -> Expr) -> Named x a -> Named x a

(ExprLike qn, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn p e)

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e)

foldExpr :: Monoid m => (Expr -> m) -> RewriteEqn' qn p e -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e)

mapExpr :: (Expr -> Expr) -> RewriteEqn' qn p e -> RewriteEqn' qn p e