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 MetaId Expr

Methods

reify :: MetaId -> TCM Expr

reifyWhen :: Bool -> MetaId -> TCM Expr

Reify Name Name

Methods

reify :: Name -> TCM Name

reifyWhen :: Bool -> Name -> TCM Name

Reify Literal Expr

Methods

reify :: Literal -> TCM Expr

reifyWhen :: Bool -> Literal -> TCM Expr

Reify Level Expr

Methods

reify :: Level -> TCM Expr

reifyWhen :: Bool -> Level -> TCM Expr

Reify Sort Expr

Methods

reify :: Sort -> TCM Expr

reifyWhen :: Bool -> Sort -> TCM Expr

Reify Telescope Telescope

Methods

reify :: Telescope -> TCM Telescope

reifyWhen :: Bool -> Telescope -> TCM Telescope

Reify Type Expr

Methods

reify :: Type -> TCM Expr

reifyWhen :: Bool -> Type -> TCM Expr

Reify Term Expr

Methods

reify :: Term -> TCM Expr

reifyWhen :: Bool -> Term -> TCM Expr

Reify Expr Expr

Methods

reify :: Expr -> TCM Expr

reifyWhen :: Bool -> Expr -> TCM Expr

Reify DisplayTerm Expr

Methods

reify :: DisplayTerm -> TCM Expr

reifyWhen :: Bool -> DisplayTerm -> TCM Expr

Reify NamedClause Clause

Methods

reify :: NamedClause -> TCM Clause

reifyWhen :: Bool -> NamedClause -> TCM Clause

Reify (QNamed Clause) Clause

Methods

reify :: QNamed Clause -> TCM Clause

reifyWhen :: Bool -> QNamed Clause -> TCM Clause

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

Methods

reify :: [i] -> TCM [a]

reifyWhen :: Bool -> [i] -> TCM [a]

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

Methods

reify :: Dom i -> TCM (Arg a)

reifyWhen :: Bool -> Dom i -> TCM (Arg a)

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

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

Methods

reify :: Arg i -> TCM (Arg a)

reifyWhen :: Bool -> Arg i -> TCM (Arg a)

Reify i a => Reify (Elim' i) (Elim' a)

Methods

reify :: Elim' i -> TCM (Elim' a)

reifyWhen :: Bool -> Elim' i -> TCM (Elim' a)

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

Methods

reify :: Abs i -> TCM (Name, a)

reifyWhen :: Bool -> Abs i -> TCM (Name, a)

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

Methods

reify :: (i1, i2) -> TCM (a1, a2)

reifyWhen :: Bool -> (i1, i2) -> TCM (a1, a2)

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

Methods

reify :: Named n i -> TCM (Named n a)

reifyWhen :: Bool -> Named n i -> TCM (Named n a)

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

Methods

reify :: (i1, i2, i3) -> TCM (a1, a2, a3)

reifyWhen :: Bool -> (i1, i2, i3) -> TCM (a1, a2, a3)

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

Methods

reify :: (i1, i2, i3, i4) -> TCM (a1, a2, a3, a4)

reifyWhen :: Bool -> (i1, i2, i3, i4) -> TCM (a1, a2, a3, a4)

data NamedClause

Constructors

NamedClause QName Bool Clause

Also tracks whether module parameters should be dropped from the patterns.

Instances

PrettyTCM NamedClause

Methods

prettyTCM :: NamedClause -> TCM Doc

Reify NamedClause Clause

Methods

reify :: NamedClause -> TCM Clause

reifyWhen :: Bool -> NamedClause -> TCM Clause

reifyPatterns :: MonadTCM tcm => [NamedArg DeBruijnPattern] -> tcm [NamedArg Pattern]

Assumes that pattern variables have been added to the context already. Picks pattern variable names from context.