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 where

Minimal complete definition

reify

Associated Types

type ReifiesTo i

Methods

reify :: MonadReify m => i -> m (ReifiesTo i)

reifyWhen :: MonadReify m => Bool -> i -> m (ReifiesTo i)

Instances

Reify Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Expr

Methods

reify :: MonadReify m => Expr -> m (ReifiesTo Expr)

reifyWhen :: MonadReify m => Bool -> Expr -> m (ReifiesTo Expr)

Reify Name

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Name

Methods

reify :: MonadReify m => Name -> m (ReifiesTo Name)

reifyWhen :: MonadReify m => Bool -> Name -> m (ReifiesTo Name)

Reify MetaId

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo MetaId

Methods

reify :: MonadReify m => MetaId -> m (ReifiesTo MetaId)

reifyWhen :: MonadReify m => Bool -> MetaId -> m (ReifiesTo MetaId)

Reify Level

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Level

Methods

reify :: MonadReify m => Level -> m (ReifiesTo Level)

reifyWhen :: MonadReify m => Bool -> Level -> m (ReifiesTo Level)

Reify Sort

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Sort

Methods

reify :: MonadReify m => Sort -> m (ReifiesTo Sort)

reifyWhen :: MonadReify m => Bool -> Sort -> m (ReifiesTo Sort)

Reify Telescope

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope

Methods

reify :: MonadReify m => Telescope -> m (ReifiesTo Telescope)

reifyWhen :: MonadReify m => Bool -> Telescope -> m (ReifiesTo Telescope)

Reify Term

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Term

Methods

reify :: MonadReify m => Term -> m (ReifiesTo Term)

reifyWhen :: MonadReify m => Bool -> Term -> m (ReifiesTo Term)

Reify Type

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Type

Methods

reify :: MonadReify m => Type -> m (ReifiesTo Type)

reifyWhen :: MonadReify m => Bool -> Type -> m (ReifiesTo Type)

Reify Literal

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Literal

Methods

reify :: MonadReify m => Literal -> m (ReifiesTo Literal)

reifyWhen :: MonadReify m => Bool -> Literal -> m (ReifiesTo Literal)

Reify NamedClause

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo NamedClause

Methods

reify :: MonadReify m => NamedClause -> m (ReifiesTo NamedClause)

reifyWhen :: MonadReify m => Bool -> NamedClause -> m (ReifiesTo NamedClause)

Reify Constraint

Defined in Agda.Interaction.BasicOps

Associated Types

type ReifiesTo Constraint

Methods

reify :: MonadReify m => Constraint -> m (ReifiesTo Constraint)

reifyWhen :: MonadReify m => Bool -> Constraint -> m (ReifiesTo Constraint)

Reify DisplayTerm

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo DisplayTerm

Methods

reify :: MonadReify m => DisplayTerm -> m (ReifiesTo DisplayTerm)

reifyWhen :: MonadReify m => Bool -> DisplayTerm -> m (ReifiesTo DisplayTerm)

Reify ProblemConstraint

Defined in Agda.Interaction.BasicOps

Associated Types

type ReifiesTo ProblemConstraint

Methods

reify :: MonadReify m => ProblemConstraint -> m (ReifiesTo ProblemConstraint)

reifyWhen :: MonadReify m => Bool -> ProblemConstraint -> m (ReifiesTo ProblemConstraint)

Reify Bool

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Bool

Methods

reify :: MonadReify m => Bool -> m (ReifiesTo Bool)

reifyWhen :: MonadReify m => Bool -> Bool -> m (ReifiesTo Bool)

Reify (QNamed Clause)

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (QNamed Clause)

Methods

reify :: MonadReify m => QNamed Clause -> m (ReifiesTo (QNamed Clause))

reifyWhen :: MonadReify m => Bool -> QNamed Clause -> m (ReifiesTo (QNamed Clause))

Reify (QNamed System)

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (QNamed System)

Methods

reify :: MonadReify m => QNamed System -> m (ReifiesTo (QNamed System))

reifyWhen :: MonadReify m => Bool -> QNamed System -> m (ReifiesTo (QNamed System))

Reify i => Reify (Arg i)

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Arg i)

Methods

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

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

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Abs i)

Methods

reify :: MonadReify m => Abs i -> m (ReifiesTo (Abs i))

reifyWhen :: MonadReify m => Bool -> Abs i -> m (ReifiesTo (Abs i))

Reify i => Reify (Dom i)

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Dom i)

Methods

reify :: MonadReify m => Dom i -> m (ReifiesTo (Dom i))

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

Reify i => Reify (Elim' i)

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Elim' i)

Methods

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

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

Reify a => Reify (IPBoundary' a)

Defined in Agda.Interaction.BasicOps

Associated Types

type ReifiesTo (IPBoundary' a)

Methods

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

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

Reify i => Reify [i]

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo [i]

Methods

reify :: MonadReify m => [i] -> m (ReifiesTo [i])

reifyWhen :: MonadReify m => Bool -> [i] -> m (ReifiesTo [i])

Reify i => Reify (Named n i)

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Named n i)

Methods

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

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

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (i1, i2)

Methods

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

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

(Reify i1, Reify i2, Reify i3) => Reify (i1, i2, i3)

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (i1, i2, i3)

Methods

reify :: MonadReify m => (i1, i2, i3) -> m (ReifiesTo (i1, i2, i3))

reifyWhen :: MonadReify m => Bool -> (i1, i2, i3) -> m (ReifiesTo (i1, i2, i3))

(Reify i1, Reify i2, Reify i3, Reify i4) => Reify (i1, i2, i3, i4)

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (i1, i2, i3, i4)

Methods

reify :: MonadReify m => (i1, i2, i3, i4) -> m (ReifiesTo (i1, i2, i3, i4))

reifyWhen :: MonadReify m => Bool -> (i1, i2, i3, i4) -> m (ReifiesTo (i1, i2, i3, i4))

type MonadReify m = (PureTCM m, MonadInteractionPoints m, MonadFresh NameId m)

data NamedClause

Constructors

NamedClause QName Bool Clause

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

Instances

Reify NamedClause

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo NamedClause

Methods

reify :: MonadReify m => NamedClause -> m (ReifiesTo NamedClause)

reifyWhen :: MonadReify m => Bool -> NamedClause -> m (ReifiesTo NamedClause)

PrettyTCM NamedClause

Defined in Agda.TypeChecking.Pretty

Methods

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

type ReifiesTo NamedClause

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo NamedClause = 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 => i -> TCM (ReifiesTo i)

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!