Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Abstract.Views

Contents

- Traversal
- Getting all declared names

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], 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

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 Source # (<$) :: a -> AppView' b -> AppView' a Source #

type AppView = AppView' Expr Source #

appView :: Expr -> AppView Source #

Gather applications to expose head and spine.

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

appView' :: Expr -> AppView' (AppInfo, Expr) Source #

maybeProjTurnPostfix :: Expr -> Maybe Expr Source #

unAppView :: AppView -> Expr Source #

data LamView Source #

Collects plain lambdas.

Constructors

LamView [LamBinding] Expr |

lamView :: Expr -> LamView Source #

data PiView Source #

Collect `A.Pi`s.

Constructors

PiView [(ExprInfo, Telescope1)] Type |

piView :: Expr -> PiView Source #

unPiView :: PiView -> Expr Source #

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

Gather top-level `AsP`atterns 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.

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 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 Methods recurseExpr :: RecurseExprFn m BindName Source # foldExpr :: FoldExprFn m BindName Source # traverseExpr :: TraverseExprFn m BindName Source # mapExpr :: (Expr -> Expr) -> BindName -> BindName Source #
ExprLike DataDefParams Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m DataDefParams Source # foldExpr :: FoldExprFn m DataDefParams Source # traverseExpr :: TraverseExprFn m DataDefParams Source # mapExpr :: (Expr -> Expr) -> DataDefParams -> DataDefParams Source #
ExprLike Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m Declaration Source # foldExpr :: FoldExprFn m Declaration Source # traverseExpr :: TraverseExprFn m Declaration Source # mapExpr :: (Expr -> Expr) -> Declaration -> Declaration Source #
ExprLike Expr Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m Expr Source # foldExpr :: FoldExprFn m Expr Source # traverseExpr :: TraverseExprFn m Expr Source # mapExpr :: (Expr -> Expr) -> Expr -> Expr Source #
ExprLike GeneralizeTelescope Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m GeneralizeTelescope Source # foldExpr :: FoldExprFn m GeneralizeTelescope Source # traverseExpr :: TraverseExprFn m GeneralizeTelescope Source # mapExpr :: (Expr -> Expr) -> GeneralizeTelescope -> GeneralizeTelescope Source #
ExprLike LHS Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m LHS Source # foldExpr :: FoldExprFn m LHS Source # traverseExpr :: TraverseExprFn m LHS Source # mapExpr :: (Expr -> Expr) -> LHS -> LHS Source #
ExprLike LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m LamBinding Source # foldExpr :: FoldExprFn m LamBinding Source # traverseExpr :: TraverseExprFn m LamBinding Source # mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding Source #
ExprLike LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m LetBinding Source # foldExpr :: FoldExprFn m LetBinding Source # traverseExpr :: TraverseExprFn m LetBinding Source # mapExpr :: (Expr -> Expr) -> LetBinding -> LetBinding Source #
ExprLike ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m ModuleApplication Source # foldExpr :: FoldExprFn m ModuleApplication Source # traverseExpr :: TraverseExprFn m ModuleApplication Source # mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication Source #
ExprLike Pragma Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m Pragma Source # foldExpr :: FoldExprFn m Pragma Source # traverseExpr :: TraverseExprFn m Pragma Source # mapExpr :: (Expr -> Expr) -> Pragma -> Pragma Source #
ExprLike RHS Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m RHS Source # foldExpr :: FoldExprFn m RHS Source # traverseExpr :: TraverseExprFn m RHS Source # mapExpr :: (Expr -> Expr) -> RHS -> RHS Source #
ExprLike SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m SpineLHS Source # foldExpr :: FoldExprFn m SpineLHS Source # traverseExpr :: TraverseExprFn m SpineLHS Source # mapExpr :: (Expr -> Expr) -> SpineLHS -> SpineLHS Source #
ExprLike TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m TypedBinding Source # foldExpr :: FoldExprFn m TypedBinding Source # traverseExpr :: TraverseExprFn m TypedBinding Source # mapExpr :: (Expr -> Expr) -> TypedBinding -> TypedBinding Source #
ExprLike TypedBindingInfo Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m TypedBindingInfo Source # foldExpr :: FoldExprFn m TypedBindingInfo Source # traverseExpr :: TraverseExprFn m TypedBindingInfo Source # mapExpr :: (Expr -> Expr) -> TypedBindingInfo -> TypedBindingInfo Source #
ExprLike WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m WhereDeclarations Source # foldExpr :: FoldExprFn m WhereDeclarations Source # traverseExpr :: TraverseExprFn m WhereDeclarations Source # mapExpr :: (Expr -> Expr) -> WhereDeclarations -> WhereDeclarations Source #
ExprLike ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m ModuleName Source # foldExpr :: FoldExprFn m ModuleName Source # traverseExpr :: TraverseExprFn m ModuleName Source # mapExpr :: (Expr -> Expr) -> ModuleName -> ModuleName Source #
ExprLike QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m QName Source # foldExpr :: FoldExprFn m QName Source # traverseExpr :: TraverseExprFn m QName Source # mapExpr :: (Expr -> Expr) -> QName -> QName Source #
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 Methods recurseExpr :: RecurseExprFn m (Clause' a) Source # foldExpr :: FoldExprFn m (Clause' a) Source # traverseExpr :: TraverseExprFn m (Clause' a) Source # mapExpr :: (Expr -> Expr) -> Clause' a -> Clause' a Source #
ExprLike a => ExprLike (LHSCore' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (LHSCore' a) Source # foldExpr :: FoldExprFn m (LHSCore' a) Source # traverseExpr :: TraverseExprFn m (LHSCore' a) Source # mapExpr :: (Expr -> Expr) -> LHSCore' a -> LHSCore' a Source #
ExprLike a => ExprLike (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (Pattern' a) Source # foldExpr :: FoldExprFn m (Pattern' a) Source # traverseExpr :: TraverseExprFn m (Pattern' a) Source # mapExpr :: (Expr -> Expr) -> Pattern' a -> Pattern' a Source #
ExprLike a => ExprLike (Arg a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (Arg a) Source # foldExpr :: FoldExprFn m (Arg a) Source # traverseExpr :: TraverseExprFn m (Arg a) Source # mapExpr :: (Expr -> Expr) -> Arg a -> Arg a Source #
ExprLike a => ExprLike (Ranged a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (Ranged a) Source # foldExpr :: FoldExprFn m (Ranged a) Source # traverseExpr :: TraverseExprFn m (Ranged a) Source # mapExpr :: (Expr -> Expr) -> Ranged a -> Ranged a Source #
ExprLike a => ExprLike (WithHiding a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (WithHiding a) Source # foldExpr :: FoldExprFn m (WithHiding a) Source # traverseExpr :: TraverseExprFn m (WithHiding a) Source # mapExpr :: (Expr -> Expr) -> WithHiding a -> WithHiding a Source #
ExprLike a => ExprLike (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (FieldAssignment' a) Source # foldExpr :: FoldExprFn m (FieldAssignment' a) Source # traverseExpr :: TraverseExprFn m (FieldAssignment' a) Source # mapExpr :: (Expr -> Expr) -> FieldAssignment' a -> FieldAssignment' a Source #
ExprLike a => ExprLike (TacticAttribute' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (TacticAttribute' a) Source # foldExpr :: FoldExprFn m (TacticAttribute' a) Source # traverseExpr :: TraverseExprFn m (TacticAttribute' a) Source # mapExpr :: (Expr -> Expr) -> TacticAttribute' a -> TacticAttribute' a Source #
ExprLike a => ExprLike (List1 a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (List1 a) Source # foldExpr :: FoldExprFn m (List1 a) Source # traverseExpr :: TraverseExprFn m (List1 a) Source # mapExpr :: (Expr -> Expr) -> List1 a -> List1 a Source #
ExprLike a => ExprLike (Maybe a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (Maybe a) Source # foldExpr :: FoldExprFn m (Maybe a) Source # traverseExpr :: TraverseExprFn m (Maybe a) Source # mapExpr :: (Expr -> Expr) -> Maybe a -> Maybe a Source #
ExprLike a => ExprLike [a] Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m [a] Source # foldExpr :: FoldExprFn m [a] Source # traverseExpr :: TraverseExprFn m [a] Source # mapExpr :: (Expr -> Expr) -> [a] -> [a] Source #
ExprLike a => ExprLike (Named x a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (Named x a) Source # foldExpr :: FoldExprFn m (Named x a) Source # traverseExpr :: TraverseExprFn m (Named x a) Source # mapExpr :: (Expr -> Expr) -> Named x a -> Named x a Source #
(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 Methods recurseExpr :: RecurseExprFn m (RewriteEqn' qn nm p e) Source # foldExpr :: FoldExprFn m (RewriteEqn' qn nm p e) Source # traverseExpr :: TraverseExprFn m (RewriteEqn' qn nm p e) Source # mapExpr :: (Expr -> Expr) -> RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e Source #

# Getting all declared names

type KName = WithKind QName Source #

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 Methods declaredNames :: Collection KName m => Clause -> m Source #
DeclaredNames Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Declaration -> m Source #
DeclaredNames Pragma Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Pragma -> m Source #
DeclaredNames RHS Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => RHS -> m Source #
DeclaredNames RecordDirectives Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => RecordDirectives -> m Source #
DeclaredNames WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => WhereDeclarations -> m Source #
DeclaredNames KName Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => KName -> m Source #
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 Methods declaredNames :: Collection KName m => FieldAssignment' a -> m Source #
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 #