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 :: MonadReify m => i -> m a

reifyWhen :: MonadReify m => Bool -> i -> m a

Instances

Reify Bool Bool

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Bool -> m Bool

reifyWhen :: MonadReify m => Bool -> Bool -> m Bool

Reify MetaId Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => MetaId -> m Expr

reifyWhen :: MonadReify m => Bool -> MetaId -> m Expr

Reify Name Name

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Name -> m Name

reifyWhen :: MonadReify m => Bool -> Name -> m Name

Reify Literal Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Literal -> m Expr

reifyWhen :: MonadReify m => Bool -> Literal -> m Expr

Reify Level Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Level -> m Expr

reifyWhen :: MonadReify m => Bool -> Level -> m Expr

Reify Sort Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Sort -> m Expr

reifyWhen :: MonadReify m => Bool -> Sort -> m Expr

Reify Telescope Telescope

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Telescope0 -> m Telescope

reifyWhen :: MonadReify m => Bool -> Telescope0 -> m Telescope

Reify Type Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Type -> m Expr

reifyWhen :: MonadReify m => Bool -> Type -> m Expr

Reify Term Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Term -> m Expr

reifyWhen :: MonadReify m => Bool -> Term -> m Expr

Reify Expr Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Expr -> m Expr

reifyWhen :: MonadReify m => Bool -> Expr -> m Expr

Reify DisplayTerm Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => DisplayTerm -> m Expr

reifyWhen :: MonadReify m => Bool -> DisplayTerm -> m Expr

Reify NamedClause Clause

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => NamedClause -> m Clause

reifyWhen :: MonadReify m => Bool -> NamedClause -> m Clause

Reify ProblemConstraint (Closure (OutputForm Expr Expr))

Defined in Agda.Interaction.BasicOps

Methods

reify :: MonadReify m => ProblemConstraint -> m (Closure (OutputForm Expr Expr))

reifyWhen :: MonadReify m => Bool -> ProblemConstraint -> m (Closure (OutputForm Expr Expr))

Reify Constraint (OutputConstraint Expr Expr)

Defined in Agda.Interaction.BasicOps

Methods

reify :: MonadReify m => Constraint -> m (OutputConstraint Expr Expr)

reifyWhen :: MonadReify m => Bool -> Constraint -> m (OutputConstraint Expr Expr)

Reify (QNamed Clause) Clause

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => QNamed Clause0 -> m Clause

reifyWhen :: MonadReify m => Bool -> QNamed Clause0 -> m Clause

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => [i] -> m [a]

reifyWhen :: MonadReify m => Bool -> [i] -> m [a]

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

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Arg i -> m (Arg a)

reifyWhen :: MonadReify m => Bool -> Arg i -> m (Arg a)

Reify (QNamed System) [Clause]

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => QNamed System -> m [Clause]

reifyWhen :: MonadReify m => Bool -> QNamed System -> m [Clause]

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Elim' i -> m (Elim' a)

reifyWhen :: MonadReify m => Bool -> Elim' i -> m (Elim' a)

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Dom i -> m (Arg a)

reifyWhen :: MonadReify m => Bool -> Dom i -> m (Arg a)

Reify a e => Reify (IPBoundary' a) (IPBoundary' e)

Defined in Agda.Interaction.BasicOps

Methods

reify :: MonadReify m => IPBoundary' a -> m (IPBoundary' e)

reifyWhen :: MonadReify m => Bool -> IPBoundary' a -> m (IPBoundary' e)

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Abs i -> m (Name, a)

reifyWhen :: MonadReify m => Bool -> Abs i -> m (Name, a)

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => (i1, i2) -> m (a1, a2)

reifyWhen :: MonadReify m => Bool -> (i1, i2) -> m (a1, a2)

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Named n i -> m (Named n a)

reifyWhen :: MonadReify m => Bool -> Named n i -> m (Named n a)

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => (i1, i2, i3) -> m (a1, a2, a3)

reifyWhen :: MonadReify m => Bool -> (i1, i2, i3) -> m (a1, a2, a3)

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => (i1, i2, i3, i4) -> m (a1, a2, a3, a4)

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

type MonadReify m = (MonadReduce m, MonadAddContext m, MonadInteractionPoints m, MonadFresh NameId m, HasConstInfo m, HasOptions m, HasBuiltins m, MonadDebug m)

data NamedClause

Constructors

NamedClause QName Bool Clause

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

Instances

PrettyTCM NamedClause

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => NamedClause -> m Doc

Reify NamedClause Clause

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => NamedClause -> m Clause

reifyWhen :: MonadReify m => Bool -> NamedClause -> m Clause

reifyPatterns :: MonadReify m => [NamedArg DeBruijnPattern] -> m [NamedArg Pattern]

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

reifyUnblocked :: Reify i a => i -> TCM a

Like reify but instantiates blocking metas, useful for reporting.

blankNotInScope :: (MonadTCEnv m, BlankVars a) => a -> m a

blankNotInScope e replaces variables in expression e with _ if they are currently not in scope.

reifyDisplayFormP

Arguments

:: MonadReify m

=> QName

LHS head symbol

-> Patterns

Patterns to be taken into account to find display form.

-> Patterns

Remaining trailing patterns ("with patterns").

-> m (QName, Patterns)

New head symbol and new patterns.

reifyDisplayFormP tries to recursively rewrite a lhs with a display form.

Note: we are not necessarily in the empty context upon entry!