ModuleAgda-2.8.0.2Haskell2010

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

2 types
1 class
4 values

PackageAgda-2.8.0.2
Exports7
LanguageHaskell2010
LicenceMIT
SourceInternalToAbstract.hs

classclass Reify i where

Associated types

type family ReifiesTo i

Methods

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

Instances29Reify, …

Reify ExprDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify NameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify MetaIdDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify LevelDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify SortDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify TelescopeDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify TermDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify TypeDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify LiteralDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify NamedClauseDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify ConstraintDefined in Agda-2.8.0.2 · Agda.Interaction.BasicOps · orphan
Reify DisplayTermDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify ProblemConstraintDefined in Agda-2.8.0.2 · Agda.Interaction.BasicOps · orphan
Reify ContextEntryDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify BoolDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify CharDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify (QNamed Clause)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify (QNamed System)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify a => Reify (IPBoundary' a)Defined in Agda-2.8.0.2 · Agda.Interaction.BasicOps · orphan
Reify i => Reify (Arg i)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Skip reification of implicit and irrelevant args if option is off.
Reify i => Reify (Dom i)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify i => Reify (Elim' i)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify i => Reify (List1 i)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify i => Reify [i]Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
(Free i, Reify i) => Reify (Abs i)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify i => Reify (Named n i)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
(Reify i1, Reify i2) => Reify (i1, i2)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
(Reify i1, Reify i2, Reify i3) => Reify (i1, i2, i3)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
(Reify i1, Reify i2, Reify i3, Reify i4) => Reify (i1, i2, i3, i4)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract

typetype MonadReify (m :: Type -> Type) = (PureTCM m, MonadInteractionPoints m, MonadFresh NameId m)

datadata NamedClause

Constructors

NamedClause QName Bool Clause
Also tracks whether module parameters should be dropped from the patterns.

Instances3PrettyTCM, Reify, ReifiesTo

PrettyTCM NamedClauseDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
Reify NamedClauseDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
type ReifiesTo NamedClause = ClauseDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract

valuereifyPatterns

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

valuereifyUnblocked :: Reify i => i -> TCM (ReifiesTo i)

Like reify but instantiates blocking metas, useful for reporting.

valueblankNotInScope :: (MonadTCEnv m, MonadDebug m, BlankVars a) => a -> m a

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

valuereifyDisplayFormP

:: 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!