Safe Haskell | None |
---|---|

Language | Haskell98 |

- data AppView = Application Expr [NamedArg Expr]
- appView :: Expr -> AppView
- unAppView :: AppView -> Expr
- asView :: Pattern -> ([Name], Pattern)
- isSet :: Expr -> Bool
- unScope :: Expr -> Expr
- deepUnScope :: Expr -> Expr
- class ExprLike a where
- recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> a -> m a
- foldExpr :: Monoid m => (Expr -> m) -> a -> m
- traverseExpr :: (Monad m, Applicative m) => (Expr -> m Expr) -> a -> m a
- mapExpr :: (Expr -> Expr) -> a -> a

# Documentation

appView :: Expr -> AppView Source

Gather applications to expose head and spine.

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

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

Gather top-level `AsP`

atterns to expose underlying pattern.

unScope :: Expr -> Expr Source

Remove top `ScopedExpr`

wrappers.

deepUnScope :: Expr -> Expr Source

Remove `ScopedExpr`

wrappers everywhere.

# Traversal

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

Nothing

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> a -> m a Source

The first expression is pre-traversal, the second one post-traversal.

foldExpr :: Monoid m => (Expr -> m) -> a -> m Source

traverseExpr :: (Monad m, Applicative m) => (Expr -> m Expr) -> a -> m a Source

ExprLike TypedBinding Source | |

ExprLike TypedBindings Source | |

ExprLike LamBinding Source | |

ExprLike LetBinding Source | |

ExprLike Expr Source | |

ExprLike a => ExprLike [a] Source | |

ExprLike a => ExprLike (Pattern' a) Source | |

ExprLike (Clause' a) Source | TODO: currently does not go into clauses. |

ExprLike a => ExprLike (x, a) Source | |

ExprLike a => ExprLike (Named x a) Source | |

ExprLike a => ExprLike (Arg c a) Source | TODO: currently does not go into colors. |