Constructors
Application Expr [NamedArg arg]
ModuleAgda-2.8.0.2Haskell2010
Agda.Syntax.Abstract.Views
Contents
Synopsis
- data AppView'
- type AppView
- value appView
- value appView'
- value maybeProjTurnPostfix
- value unAppView
- data LamView
- value lamView
- data PiView
- value piView
- value unPiView
- value asView
- value unScope
- value deepUnscope
- value deepUnscopeDecls
- value deepUnscopeDecl
- type RecurseExprFn
- type RecurseExprRecFn
- type FoldExprFn
- type FoldExprRecFn
- type TraverseExprFn
- type TraverseExprRecFn
- class ExprLike
- type KName
- class DeclaredNames
- PackageAgda-2.8.0.2
- Exports25
- LanguageHaskell2010
- LicenceMIT
- SourceViews.hs
Gather applications to expose head and spine.
Note: everything is an application, possibly of itself to 0 arguments
Collects plain lambdas.
Constructors
Collect A.Pis.
Constructors
PiView [(ExprInfo, Telescope1)] Type
Gather top-level AsPatterns to expose underlying pattern.
Remove top ScopedExpr wrappers.
Remove ScopedExpr wrappers everywhere.
NB: Unless the implementation of ExprLike for clauses has been finished, this does not work for clauses yet.
Traversal
type
type RecurseExprFn (m :: Type -> Type) a = Applicative m => (Expr -> m Expr -> m Expr) -> a -> m atype
type TraverseExprFn (m :: Type -> Type) a = (Applicative m, Monad m) => (Expr -> m Expr) -> a -> m aApply an expression rewriting to every subexpression, inside-out. See Agda.Syntax.Internal.Generic.
Methods
recurseExpr :: RecurseExprFn m aThe first expression is pre-traversal, the second one post-traversal.
foldExpr :: FoldExprFn m atraverseExpr :: TraverseExprFn m amapExpr :: (Expr -> Expr) -> a -> a
Instances33ExprLike, …
ExprLike BindNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike DataDefParamsDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike DeclarationDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike ExprDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike GeneralizeTelescopeDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike LHSDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike LamBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike LetBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike ModuleApplicationDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike PragmaDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike RHSDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike SpineLHSDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike TypedBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike TypedBindingInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike WhereDeclarationsDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike VoidDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike a => ExprLike (Clause' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike a => ExprLike (LHSCore' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike a => ExprLike (Pattern' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike a => ExprLike (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike a => ExprLike (Ranged a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike a => ExprLike (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike a => ExprLike (FieldAssignment' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike a => ExprLike (TacticAttribute' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike a => ExprLike (List1 a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike a => ExprLike (Maybe a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike a => ExprLike [a]Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsExprLike a => ExprLike (Named x a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views(ExprLike a, ExprLike b) => ExprLike (Either a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views(ExprLike a, ExprLike b) => ExprLike (a, b)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views(ExprLike qn, ExprLike nm, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn nm p e)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views
Getting all declared names
Extracts "all" names which are declared in a Declaration.
Includes: local modules and where clauses.
Excludes: open public, let, with function names, extended lambdas.
Methods
declaredNames :: Collection KName m => a -> m
Instances15DeclaredNames, …
DeclaredNames ClauseDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsDeclaredNames DeclarationDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsDeclaredNames PragmaDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsDeclaredNames RHSDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsDeclaredNames RecordDirectivesDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsDeclaredNames WhereDeclarationsDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsDeclaredNames KNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsDeclaredNames a => DeclaredNames (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsDeclaredNames a => DeclaredNames (FieldAssignment' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsDeclaredNames a => DeclaredNames (List1 a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsDeclaredNames a => DeclaredNames (Maybe a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsDeclaredNames a => DeclaredNames [a]Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.ViewsDeclaredNames a => DeclaredNames (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views(DeclaredNames a, DeclaredNames b) => DeclaredNames (Either a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views(DeclaredNames a, DeclaredNames b) => DeclaredNames (a, b)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views