| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.Syntax.Abstract.Views
Contents
- data AppView = Application Expr [NamedArg Expr]
- appView :: Expr -> AppView
- unAppView :: AppView -> Expr
- asView :: Pattern -> ([Name], Pattern)
- isSet :: Expr -> Bool
- unScope :: Expr -> Expr
- deepUnScope :: Expr -> Expr
- class ExprLike a where
- traverseExpr :: (Monad m, Applicative m) => (Expr -> m Expr) -> a -> m a
- mapExpr :: (Expr -> Expr) -> a -> a
Documentation
appView :: Expr -> AppView Source
Gather applications to expose head and spine.
Note: everything is an application, possibly of itself to 0 arguments
asView :: Pattern -> ([Name], Pattern) Source
Gather top-level AsPatterns to expose underlying pattern.
unScope :: Expr -> Expr Source
Remove top ScopedExpr wrappers.
deepUnScope :: Expr -> Expr Source
Remove ScopedExpr wrappers everywhere.
Traversal
Apply an expression rewriting to every subexpression, inside-out.
See Generic
Minimal complete definition
Methods
traverseExpr :: (Monad m, Applicative m) => (Expr -> m Expr) -> a -> m a Source
Instances
| ExprLike TypedBinding | |
| ExprLike TypedBindings | |
| ExprLike LamBinding | |
| ExprLike LetBinding | |
| ExprLike Expr | |
| ExprLike a => ExprLike [a] | |
| ExprLike (Pattern' a) | TODO: currently does not go into patterns. |
| ExprLike (Clause' a) | TODO: currently does not go into clauses. |
| ExprLike a => ExprLike (x, a) | |
| ExprLike a => ExprLike (Named x a) | |
| ExprLike a => ExprLike (Arg c a) | TODO: currently does not go into colors. |