ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Translation.AbstractToConcrete

The translation of abstract syntax to concrete syntax has two purposes. First it allows us to pretty print abstract syntax values without having to write a dedicated pretty printer, and second it serves as a sanity check for the concrete to abstract translation: translating from concrete to abstract and then back again should be (more or less) the identity.

2 types
1 class
9 values

PackageAgda-2.8.0.2
Exports12
LanguageHaskell2010
LicenceMIT
SourceAbstractToConcrete.hs

classclass ToConcrete a where

Associated types

type family ConOfAbs a

Methods

toConcrete :: MonadToConcrete m => a -> m (ConOfAbs a)
bindToConcrete :: MonadToConcrete m => a -> (ConOfAbs a -> m b) -> m b

Instances51ToConcrete, …

ToConcrete BindNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete DeclarationDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete ExprDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete LHSDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete LHSCoreDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete LamBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete LetBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete ModuleApplicationDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete PatternDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete RHSDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete RecordDirectivesDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete SpineLHSDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete TypedBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete WhereDeclarationsDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete NameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete InteractionIdDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete AbstractNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete ResolvedNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
Assumes name is not UnknownName.
ToConcrete BindingPatternDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete FreshenNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete RangeAndPragmaDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete NamedMetaDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete BoolDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete CharDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete ()Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete (Constr Constructor)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete (SplitPattern Pattern)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete (SplitPattern (NamedArg Pattern))Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete (UserPattern Pattern)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete (UserPattern (NamedArg Pattern))Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete a => ToConcrete (Binder' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete a => ToConcrete (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete a => ToConcrete (Ranged a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete a => ToConcrete (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete a => ToConcrete (FieldAssignment' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete a => ToConcrete (TacticAttribute' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete a => ToConcrete (IPBoundary' a)Defined in Agda-2.8.0.2 · Agda.Interaction.BasicOps · orphan
ToConcrete a => ToConcrete (List1 a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete a => ToConcrete (Maybe a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete a => ToConcrete [a]Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
(ToConcrete a, ConOfAbs a ~ LHS) => ToConcrete (Clause' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete a => ToConcrete (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint' a b)Defined in Agda-2.8.0.2 · Agda.Interaction.BasicOps · orphan
(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint a b)Defined in Agda-2.8.0.2 · Agda.Interaction.BasicOps · orphan
(ToConcrete a, ToConcrete b) => ToConcrete (OutputForm a b)Defined in Agda-2.8.0.2 · Agda.Interaction.BasicOps · orphan
(ToConcrete a1, ToConcrete a2) => ToConcrete (Either a1 a2)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
(ToConcrete a1, ToConcrete a2) => ToConcrete (a1, a2)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
(ToConcrete a1, ToConcrete a2, ToConcrete a3) => ToConcrete (a1, a2, a3)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
(ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete

valuetoConcreteCtx

:: (MonadToConcrete m, ToConcrete a)
=> Precedence
-> a
-> m (ConOfAbs a)

Translate something in a context of the given precedence.

type

type MonadAbsToCon (m :: Type -> Type) = (MonadFresh NameId m, MonadInteractionPoints m, MonadStConcreteNames m, HasOptions m, PureTCM m, IsString (m Doc), Null (m Doc), Semigroup (m Doc))

Preconditions to run the AbstractToConcrete translation.

valueabstractToConcrete_

:: (ToConcrete a, MonadAbsToCon m)
=> a
-> m (ConOfAbs a)

valueabstractToConcreteCtx

:: (ToConcrete a, MonadAbsToCon m)
=> Precedence
-> a
-> m (ConOfAbs a)

valueabstractToConcreteHiding

:: (LensHiding i, ToConcrete a, MonadAbsToCon m)
=> i
-> a
-> m (ConOfAbs a)

valueabstractToConcreteQName

valueabstractToConcreteScope

:: (ToConcrete a, MonadAbsToCon m)
=> ScopeInfo
-> a
-> m (ConOfAbs a)

valueabstractToConcreteTelescope

valueabstractToConcreteUnqualify

:: (ToConcrete a, MonadAbsToCon m)
=> a
-> m (ConOfAbs a)

datadata RangeAndPragma

Constructors

RangeAndPragma Range Pragma

Instances2ToConcrete, ConOfAbs

ToConcrete RangeAndPragmaDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
type ConOfAbs RangeAndPragma = PragmaDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete

valuenoTakenNames :: MonadToConcrete m => m a -> m a