Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Abstract.Views

Contents

- Traversal

Synopsis

- data AppView' arg = Application Expr [NamedArg arg]
- type AppView = AppView' Expr
- appView :: Expr -> AppView
- appView' :: Expr -> AppView' (AppInfo, Expr)
- maybeProjTurnPostfix :: Expr -> Maybe Expr
- unAppView :: AppView -> Expr
- data LamView = LamView [LamBinding] Expr
- lamView :: Expr -> LamView
- asView :: Pattern -> ([Name], Pattern)
- isSet :: Expr -> Bool
- unScope :: Expr -> Expr
- deepUnscope :: ExprLike a => a -> a
- deepUnscopeDecls :: [Declaration] -> [Declaration]
- deepUnscopeDecl :: Declaration -> [Declaration]
- class ExprLike a where
  - 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

# Documentation

data AppView' arg Source #

Constructors

Application Expr [NamedArg arg] |

Instances

Functor AppView' Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods fmap :: (a -> b) -> AppView' a -> AppView' b Source # (<$) :: a -> AppView' b -> AppView' a Source #

type AppView = AppView' Expr Source #

appView :: Expr -> AppView Source #

Gather applications to expose head and spine.

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

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

maybeProjTurnPostfix :: Expr -> Maybe Expr Source #

unAppView :: AppView -> Expr Source #

data LamView Source #

Collects plain lambdas.

Constructors

LamView [LamBinding] Expr |

lamView :: Expr -> LamView Source #

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

Gather top-level `AsP`atterns to expose underlying pattern.

isSet :: Expr -> Bool Source #

Check whether we are dealing with a universe.

unScope :: Expr -> Expr Source #

Remove top `ScopedExpr` wrappers.

deepUnscope :: ExprLike a => a -> a Source #

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] Source #

deepUnscopeDecl :: Declaration -> [Declaration] Source #

# Traversal

class ExprLike a where Source #

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 Source #

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

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

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

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

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

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

Instances

ExprLike Void Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Void -> m Void Source # foldExpr :: Monoid m => (Expr -> m) -> Void -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Void -> m Void Source # mapExpr :: (Expr -> Expr) -> Void -> Void Source #
ExprLike ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> ModuleName -> m ModuleName Source # foldExpr :: Monoid m => (Expr -> m) -> ModuleName -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> ModuleName -> m ModuleName Source # mapExpr :: (Expr -> Expr) -> ModuleName -> ModuleName Source #
ExprLike QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> QName -> m QName Source # foldExpr :: Monoid m => (Expr -> m) -> QName -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> QName -> m QName Source # mapExpr :: (Expr -> Expr) -> QName -> QName Source #
ExprLike LHS Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LHS -> m LHS Source # foldExpr :: Monoid m => (Expr -> m) -> LHS -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LHS -> m LHS Source # mapExpr :: (Expr -> Expr) -> LHS -> LHS Source #
ExprLike SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> SpineLHS -> m SpineLHS Source # foldExpr :: Monoid m => (Expr -> m) -> SpineLHS -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> SpineLHS -> m SpineLHS Source # mapExpr :: (Expr -> Expr) -> SpineLHS -> SpineLHS Source #
ExprLike RHS Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> RHS -> m RHS Source # foldExpr :: Monoid m => (Expr -> m) -> RHS -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> RHS -> m RHS Source # mapExpr :: (Expr -> Expr) -> RHS -> RHS Source #
ExprLike WhereDeclarations Source # |

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

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

ExprLike DataDefParams Source # |

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

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

ExprLike GeneralizeTelescope Source # |

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

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

ExprLike TypedBinding Source # |

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

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

ExprLike LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LamBinding -> m LamBinding Source # foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LamBinding -> m LamBinding Source # mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding Source #
ExprLike LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LetBinding -> m LetBinding Source # foldExpr :: Monoid m => (Expr -> m) -> LetBinding -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LetBinding -> m LetBinding Source # mapExpr :: (Expr -> Expr) -> LetBinding -> LetBinding Source #
ExprLike Pragma Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Pragma -> m Pragma Source # foldExpr :: Monoid m => (Expr -> m) -> Pragma -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Pragma -> m Pragma Source # mapExpr :: (Expr -> Expr) -> Pragma -> Pragma Source #
ExprLike ModuleApplication Source # |

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

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

ExprLike Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Declaration -> m Declaration Source # foldExpr :: Monoid m => (Expr -> m) -> Declaration -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Declaration -> m Declaration Source # mapExpr :: (Expr -> Expr) -> Declaration -> Declaration Source #
ExprLike Expr Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Expr -> m Expr Source # foldExpr :: Monoid m => (Expr -> m) -> Expr -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Expr -> m Expr Source # mapExpr :: (Expr -> Expr) -> Expr -> Expr Source #
ExprLike a => ExprLike [a] Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> [a] -> m [a] Source # foldExpr :: Monoid m => (Expr -> m) -> [a] -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> [a] -> m [a] Source # mapExpr :: (Expr -> Expr) -> [a] -> [a] Source #
ExprLike a => ExprLike (Arg a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Arg a -> m (Arg a) Source # foldExpr :: Monoid m => (Expr -> m) -> Arg a -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Arg a -> m (Arg a) Source # mapExpr :: (Expr -> Expr) -> Arg a -> Arg a Source #
ExprLike a => ExprLike (FieldAssignment' a) Source # |

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

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

ExprLike a => ExprLike (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Pattern' a -> m (Pattern' a) Source # foldExpr :: Monoid m => (Expr -> m) -> Pattern' a -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Pattern' a -> m (Pattern' a) Source # mapExpr :: (Expr -> Expr) -> Pattern' a -> Pattern' a Source #
ExprLike a => ExprLike (LHSCore' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LHSCore' a -> m (LHSCore' a) Source # foldExpr :: Monoid m => (Expr -> m) -> LHSCore' a -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LHSCore' a -> m (LHSCore' a) Source # mapExpr :: (Expr -> Expr) -> LHSCore' a -> LHSCore' a Source #
ExprLike a => ExprLike (Clause' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Clause' a -> m (Clause' a) Source # foldExpr :: Monoid m => (Expr -> m) -> Clause' a -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Clause' a -> m (Clause' a) Source # mapExpr :: (Expr -> Expr) -> Clause' a -> Clause' a Source #
(ExprLike a, ExprLike b) => ExprLike (Either a b) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Either a b -> m (Either a b) Source # foldExpr :: Monoid m => (Expr -> m) -> Either a b -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Either a b -> m (Either a b) Source # mapExpr :: (Expr -> Expr) -> Either a b -> Either a b Source #
(ExprLike a, ExprLike b) => ExprLike (a, b) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> (a, b) -> m (a, b) Source # foldExpr :: Monoid m => (Expr -> m) -> (a, b) -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> (a, b) -> m (a, b) Source # mapExpr :: (Expr -> Expr) -> (a, b) -> (a, b) Source #
ExprLike a => ExprLike (Named x a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Named x a -> m (Named x a) Source # foldExpr :: Monoid m => (Expr -> m) -> Named x a -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Named x a -> m (Named x a) Source # mapExpr :: (Expr -> Expr) -> Named x a -> Named x a Source #