| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Abstract.Views
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
- data PiView = PiView [(ExprInfo, Telescope1)] Type
- piView :: Expr -> PiView
- unPiView :: PiView -> Expr
- asView :: Pattern -> ([Name], [Expr], Pattern)
- unScope :: Expr -> Expr
- deepUnscope :: ExprLike a => a -> a
- deepUnscopeDecls :: [Declaration] -> [Declaration]
- deepUnscopeDecl :: Declaration -> [Declaration]
- type RecurseExprFn (m :: Type -> Type) a = Applicative m => (Expr -> m Expr -> m Expr) -> a -> m a
- type RecurseExprRecFn (m :: Type -> Type) = forall a. ExprLike a => a -> m a
- type FoldExprFn m a = Monoid m => (Expr -> m) -> a -> m
- type FoldExprRecFn m = forall a. ExprLike a => a -> m
- type TraverseExprFn (m :: Type -> Type) a = (Applicative m, Monad m) => (Expr -> m Expr) -> a -> m a
- type TraverseExprRecFn (m :: Type -> Type) = forall a. ExprLike a => a -> m a
- class ExprLike a where
- recurseExpr :: RecurseExprFn m a
- foldExpr :: FoldExprFn m a
- traverseExpr :: TraverseExprFn m a
- mapExpr :: (Expr -> Expr) -> a -> a
- type KName = WithKind QName
- class DeclaredNames a where
- declaredNames :: Collection KName m => a -> m
Documentation
Constructors
| Application Expr [NamedArg arg] |
appView :: Expr -> AppView Source #
Gather applications to expose head and spine.
Note: everything is an application, possibly of itself to 0 arguments
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
type RecurseExprFn (m :: Type -> Type) a = Applicative m => (Expr -> m Expr -> m Expr) -> a -> m a Source #
type FoldExprFn m a = Monoid m => (Expr -> m) -> a -> m Source #
type FoldExprRecFn m = forall a. ExprLike a => a -> m Source #
type TraverseExprFn (m :: Type -> Type) a = (Applicative m, Monad m) => (Expr -> m Expr) -> a -> m a Source #
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 :: RecurseExprFn m a Source #
The first expression is pre-traversal, the second one post-traversal.
default recurseExpr :: forall (f :: Type -> Type) a' m. (Traversable f, ExprLike a', a ~ f a', Applicative m) => (Expr -> m Expr -> m Expr) -> a -> m a Source #
foldExpr :: FoldExprFn m a Source #
traverseExpr :: TraverseExprFn m a Source #
Instances
Getting all declared names
class DeclaredNames a where Source #
Extracts "all" names which are declared in a Declaration.
Includes: local modules and where clauses.
Excludes: open public, let, with function names, extended lambdas.
Minimal complete definition
Nothing
Methods
declaredNames :: Collection KName m => a -> m Source #
default declaredNames :: forall (t :: Type -> Type) b m. (Foldable t, DeclaredNames b, t b ~ a, Collection KName m) => a -> m Source #