Agda.Syntax.Translation.InternalToAbstract

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

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]