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

Agda.Syntax.Translation.InternalToAbstract

Description

Translating from internal syntax to abstract syntax. Enables nice pretty printing of internal syntax.

TODO

- numbers on metas - fake dependent functions to independent functions - meta parameters - shadowing

# Documentation

apps :: MonadTCM tcm => (Expr, [Arg Expr]) -> tcm Expr

exprInfo :: ExprInfo

reifyApp :: MonadTCM tcm => Expr -> [Arg Term] -> tcm Expr

class Reify i a | i -> a where

Methods

reify :: MonadTCM tcm => i -> tcm a

Instances

Reify Literal Expr |
Reify MetaId Expr |
Reify ClauseBody RHS |
Reify Telescope Telescope |
Reify Sort Expr |
Reify Type Expr |
Reify Term Expr |
Reify DisplayTerm Expr |
Reify NamedClause Clause |
Reify Constraint (OutputForm Expr Expr) |
Reify i a => Reify [i] [a] |
Reify i a => Reify (Arg i) (Arg a) |
Reify i a => Reify (Abs i) (Name, a) |
(Reify i1 a1, Reify i2 a2) => Reify (i1, i2) (a1, a2) |
(Reify t t', Reify a a') => Reify (Judgement t a) (Judgement t' a') |

reifyDisplayForm :: MonadTCM tcm => QName -> Args -> tcm Expr -> tcm Expr

reifyDisplayFormP :: LHS -> TCM LHS

data NamedClause

Constructors

NamedClause QName Clause |

Instances

PrettyTCM NamedClause |
Reify NamedClause Clause |

stripImplicits :: MonadTCM tcm => [NamedArg Pattern] -> [Pattern] -> tcm ([NamedArg Pattern], [Pattern])

class DotVars a where

Methods

dotVars :: a -> Set Name

Instances

DotVars Pattern |
DotVars TypedBinding |
DotVars TypedBindings |
DotVars Expr |
DotVars a => DotVars [a] |
DotVars a => DotVars (Arg a) |
(DotVars a, DotVars b) => DotVars (a, b) |
DotVars a => DotVars (Named s a) |

reifyPatterns :: MonadTCM tcm => Telescope -> Permutation -> [Arg Pattern] -> tcm [NamedArg Pattern]