Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Abstract.Views

Synopsis

Documentation

data AppView' arg Source #

Constructors

Application Expr [NamedArg arg] 

Instances

Instances details
Functor AppView' Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

fmap :: (a -> b) -> AppView' a -> AppView' b

(<$) :: a -> AppView' b -> AppView' a #

appView :: Expr -> AppView Source #

Gather applications to expose head and spine.

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

data LamView Source #

Collects plain lambdas.

Constructors

LamView [LamBinding] Expr 

data PiView Source #

Collect A.Pis.

Constructors

PiView [(ExprInfo, Telescope1)] Type 

asView :: Pattern -> ([Name], [Expr], Pattern) Source #

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

unScope :: Expr -> Expr Source #

Remove top ScopedExpr wrappers.

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.

Traversal

type RecurseExprFn (m :: Type -> Type) a = Applicative m => (Expr -> m Expr -> m Expr) -> a -> m a Source #

type RecurseExprRecFn (m :: Type -> Type) = forall a. ExprLike a => 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 #

type TraverseExprRecFn (m :: Type -> Type) = forall a. ExprLike a => 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 #

mapExpr :: (Expr -> Expr) -> a -> a Source #

Instances

Instances details
ExprLike BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike TypedBindingInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike Void Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m Void Source #

foldExpr :: FoldExprFn m Void Source #

traverseExpr :: TraverseExprFn m Void Source #

mapExpr :: (Expr -> Expr) -> Void -> Void Source #

ExprLike a => ExprLike (Clause' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike a => ExprLike (LHSCore' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike a => ExprLike (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike a => ExprLike (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike a => ExprLike (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike a => ExprLike (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike a => ExprLike (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike a => ExprLike (TacticAttribute' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike a => ExprLike (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike a => ExprLike (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike a => ExprLike [a] Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike a => ExprLike (Named x a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

(ExprLike a, ExprLike b) => ExprLike (Either a b) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m (Either a b) Source #

foldExpr :: FoldExprFn m (Either a b) Source #

traverseExpr :: TraverseExprFn m (Either a b) Source #

mapExpr :: (Expr -> Expr) -> Either a b -> Either a b Source #

(ExprLike a, ExprLike b) => ExprLike (a, b) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m (a, b) Source #

foldExpr :: FoldExprFn m (a, b) Source #

traverseExpr :: TraverseExprFn m (a, b) Source #

mapExpr :: (Expr -> Expr) -> (a, b) -> (a, b) Source #

(ExprLike qn, ExprLike nm, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

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 #

Instances

Instances details
DeclaredNames Clause Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

DeclaredNames Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

DeclaredNames Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

DeclaredNames RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

DeclaredNames RecordDirectives Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

DeclaredNames WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

DeclaredNames KName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

DeclaredNames a => DeclaredNames (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => Arg a -> m Source #

DeclaredNames a => DeclaredNames (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

DeclaredNames a => DeclaredNames (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => List1 a -> m Source #

DeclaredNames a => DeclaredNames (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => Maybe a -> m Source #

DeclaredNames a => DeclaredNames [a] Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => [a] -> m Source #

DeclaredNames a => DeclaredNames (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => Named name a -> m Source #

(DeclaredNames a, DeclaredNames b) => DeclaredNames (Either a b) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => Either a b -> m Source #

(DeclaredNames a, DeclaredNames b) => DeclaredNames (a, b) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => (a, b) -> m Source #