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

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Expr = 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

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Name = 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

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo MetaId = Expr

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

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Level = Expr

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

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Sort = Expr

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

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Telescope = 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

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Term = Expr

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

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Type = 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

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Literal = Expr

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

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo NamedClause = Clause

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

Defined in Agda.Interaction.BasicOps

type ReifiesTo Constraint = OutputConstraint Expr Expr

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

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo DisplayTerm = Expr

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

Defined in Agda.Interaction.BasicOps

type ReifiesTo ProblemConstraint = Closure (OutputForm Expr Expr)

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

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Bool = 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)

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (QNamed Clause) = 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)

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (QNamed System) = [Clause]

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)

Defined in Agda.Syntax.Translation.InternalToAbstract

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

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (Abs i) = (Name, ReifiesTo 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)

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (Dom i) = Arg (ReifiesTo 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)

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (Elim' i) = Elim' (ReifiesTo 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)

Defined in Agda.Interaction.BasicOps

type ReifiesTo (IPBoundary' a) = IPBoundary' (ReifiesTo 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]

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo [i] = [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)

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (Named n i) = Named n (ReifiesTo 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)

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (i1, i2) = (ReifiesTo i1, ReifiesTo 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)

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (i1, i2, i3) = (ReifiesTo i1, ReifiesTo i2, ReifiesTo 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)

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (i1, i2, i3, i4) = (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo 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 :: Type -> Type) = (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

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo NamedClause = Clause

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, MonadDebug 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!