ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Abstract.Views

11 types
2 classes
12 values

PackageAgda-2.7.0.1
Exports25
LanguageHaskell2010
LicenceMIT
SourceViews.hs

datadata AppView' arg

Constructors

Application Expr [NamedArg arg]

Instances1Functor

Functor AppView'Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views

typetype AppView = AppView' Expr

valueappView :: Expr -> AppView

Gather applications to expose head and spine.

Note: everything is an application, possibly of itself to 0 arguments

valueappView' :: Expr -> AppView' (AppInfo, Expr)

valuemaybeProjTurnPostfix :: Expr -> Maybe Expr

valueunAppView :: AppView -> Expr

datadata LamView

Collects plain lambdas.

Constructors

LamView [LamBinding] Expr

valuelamView :: Expr -> LamView

datadata PiView

Collect A.Pis.

Constructors

PiView [(ExprInfo, Telescope1)] Type

valuepiView :: Expr -> PiView

valueunPiView :: PiView -> Expr

valueasView :: Pattern -> ([Name], [Expr], Pattern)

Gather top-level AsPatterns and AnnPatterns to expose underlying pattern.

valueunScope :: Expr -> Expr

Remove top ScopedExpr wrappers.

valuedeepUnscope :: 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.

valuedeepUnscopeDecls :: [Declaration] -> [Declaration]

valuedeepUnscopeDecl :: Declaration -> [Declaration]

Traversal

7 declarations

typetype RecurseExprFn (m :: Type -> Type) a = Applicative m => (Expr -> m Expr -> m Expr) -> a -> m a

typetype RecurseExprRecFn (m :: Type -> Type) = forall a. ExprLike a => a -> m a

typetype FoldExprFn m a = Monoid m => (Expr -> m) -> a -> m

typetype FoldExprRecFn m = forall a. ExprLike a => a -> m

typetype TraverseExprFn (m :: Type -> Type) a = (Applicative m, Monad m) => (Expr -> m Expr) -> a -> m a

typetype TraverseExprRecFn (m :: Type -> Type) = forall a. ExprLike a => a -> m a

classclass ExprLike a where

Apply an expression rewriting to every subexpression, inside-out. See Agda.Syntax.Internal.Generic.

Methods

recurseExpr :: RecurseExprFn m a
The first expression is pre-traversal, the second one post-traversal.
foldExpr :: FoldExprFn m a
traverseExpr :: TraverseExprFn m a
mapExpr :: (Expr -> Expr) -> a -> a

Instances33ExprLike, …

ExprLike BindNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike DataDefParamsDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike DeclarationDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike ExprDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike GeneralizeTelescopeDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike LHSDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike LamBindingDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike LetBindingDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike ModuleApplicationDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike PragmaDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike RHSDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike SpineLHSDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike TypedBindingDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike TypedBindingInfoDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike WhereDeclarationsDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike VoidDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike a => ExprLike (Clause' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike a => ExprLike (LHSCore' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike a => ExprLike (Pattern' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike a => ExprLike (Arg a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike a => ExprLike (Ranged a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike a => ExprLike (WithHiding a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike a => ExprLike (FieldAssignment' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike a => ExprLike (TacticAttribute' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike a => ExprLike (List1 a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike a => ExprLike (Maybe a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike a => ExprLike [a]Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
ExprLike a => ExprLike (Named x a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
(ExprLike a, ExprLike b) => ExprLike (Either a b)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
(ExprLike a, ExprLike b) => ExprLike (a, b)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
(ExprLike qn, ExprLike nm, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn nm p e)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views

Getting all declared names

2 declarations

typetype KName = WithKind QName

classclass DeclaredNames a where

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.7.0.1 · Agda.Syntax.Abstract.Views
DeclaredNames DeclarationDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
DeclaredNames PragmaDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
DeclaredNames RHSDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
DeclaredNames RecordDirectivesDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
DeclaredNames WhereDeclarationsDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
DeclaredNames KNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
DeclaredNames a => DeclaredNames (Arg a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
DeclaredNames a => DeclaredNames (FieldAssignment' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
DeclaredNames a => DeclaredNames (List1 a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
DeclaredNames a => DeclaredNames (Maybe a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
DeclaredNames a => DeclaredNames [a]Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
DeclaredNames a => DeclaredNames (Named name a)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
(DeclaredNames a, DeclaredNames b) => DeclaredNames (Either a b)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
(DeclaredNames a, DeclaredNames b) => DeclaredNames (a, b)Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views