Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Syntax.Abstract.Views
Contents
- data AppView = Application Expr [NamedArg Expr]
- appView :: Expr -> AppView
- maybeProjTurnPostfix :: Expr -> Maybe Expr
- unAppView :: AppView -> Expr
- 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
Documentation
Gather applications to expose head and spine.
Note: everything is an application, possibly of itself to 0 arguments
maybeProjTurnPostfix :: Expr -> Maybe 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
Apply an expression rewriting to every subexpression, inside-out. See Agda.Syntax.Internal.Generic.
Methods
recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> a -> m a #
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 #
The first expression is pre-traversal, the second one post-traversal.
foldExpr :: Monoid m => (Expr -> m) -> a -> m #
traverseExpr :: Monad m => (Expr -> m Expr) -> a -> m a #
Instances
ExprLike Void # | |
ExprLike ModuleName # | |
ExprLike QName # | |
ExprLike LHS # | |
ExprLike SpineLHS # | |
ExprLike RHS # | |
ExprLike TypedBinding # | |
ExprLike TypedBindings # | |
ExprLike LamBinding # | |
ExprLike LetBinding # | |
ExprLike Pragma # | |
ExprLike ModuleApplication # | |
ExprLike Declaration # | |
ExprLike Expr # | |
ExprLike a => ExprLike [a] # | |
ExprLike a => ExprLike (Arg a) # | |
ExprLike a => ExprLike (FieldAssignment' a) # | |
ExprLike a => ExprLike (Pattern' a) # | |
ExprLike a => ExprLike (LHSCore' a) # | |
ExprLike a => ExprLike (Clause' a) # | |
(ExprLike a, ExprLike b) => ExprLike (Either a b) # | |
(ExprLike a, ExprLike b) => ExprLike (a, b) # | |
ExprLike a => ExprLike (Named x a) # | |