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

class Reify i a | i -> a where

Minimal complete definition

reify

Methods

reify :: i -> TCM a

reifyWhen :: Bool -> i -> TCM a

Instances

Reify Name Name

Reify Literal Expr

Reify Expr Expr

Reify ClauseBody RHS

Reify MetaId Expr

Reify Level Expr

Reify Sort Expr

Reify Telescope Telescope

Reify Type Expr

Reify Elim Expr

Reify Term Expr

Reify ArgInfo ArgInfo

Reify DisplayTerm Expr

Reify NamedClause Clause

Reify ProblemConstraint (Closure (OutputForm Expr Expr))

Reify Constraint (OutputConstraint Expr Expr)

Reify i a => Reify [i] [a]

Reify i a => Reify (Dom i) (Arg a)

Reify i a => Reify (Arg i) (Arg a)

Skip reification of implicit and irrelevant args if option is off.

(Free i, Reify i a) => Reify (Abs i) (Name, a)

(Reify i1 a1, Reify i2 a2) => Reify (i1, i2) (a1, a2)

Reify i a => Reify (Named n i) (Named n a)

(Reify t t', Reify a a') => Reify (Judgement t a) (Judgement t' a')

(Reify i1 a1, Reify i2 a2, Reify i3 a3) => Reify (i1, i2, i3) (a1, a2, a3)

(Reify i1 a1, Reify i2 a2, Reify i3 a3, Reify i4 a4) => Reify (i1, i2, i3, i4) (a1, a2, a3, a4)

type NamedClause = QNamed Clause

reifyPatterns :: Telescope -> Permutation -> [NamedArg Pattern] -> TCM [NamedArg Pattern]