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

Instances details

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

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 AsPatterns 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.

default recurseExpr :: (Traversable f, ExprLike a', a ~ f a', 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 #

Instances

Instances details

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 (Maybe a) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Maybe a -> m (Maybe a) Source # foldExpr :: Monoid m => (Expr -> m) -> Maybe a -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Maybe a -> m (Maybe a) Source # mapExpr :: (Expr -> Expr) -> Maybe a -> Maybe 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 (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> WithHiding a -> m (WithHiding a) Source # foldExpr :: Monoid m => (Expr -> m) -> WithHiding a -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> WithHiding a -> m (WithHiding a) Source # mapExpr :: (Expr -> Expr) -> WithHiding a -> WithHiding 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 #
(ExprLike qn, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn p e) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) Source # foldExpr :: Monoid m => (Expr -> m) -> RewriteEqn' qn p e -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) Source # mapExpr :: (Expr -> Expr) -> RewriteEqn' qn p e -> RewriteEqn' qn p e Source #