ModuleAgda-2.7.0.1Haskell2010

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.

4 types
1 class
10 values

PackageAgda-2.7.0.1
Exports15
LanguageHaskell2010
LicenceMIT
SourceAbstractToConcrete.hs

classclass ToConcrete a where

Associated types

type family ConOfAbs a

Methods

toConcrete :: a -> AbsToCon (ConOfAbs a)
bindToConcrete :: a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b

Instances51ToConcrete, …

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

valuetoConcreteCtx :: ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)

Translate something in a context of the given precedence.

valueabstractToConcrete_

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

valueabstractToConcreteScope

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

valueabstractToConcreteHiding

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

valuerunAbsToCon :: MonadAbsToCon m => AbsToCon c -> m c

datadata RangeAndPragma

Constructors

RangeAndPragma Range Pragma

Instances2ToConcrete, ConOfAbs

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

valueabstractToConcreteCtx

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

valuewithScope :: ScopeInfo -> AbsToCon a -> AbsToCon a

valuepreserveInteractionIds :: AbsToCon a -> AbsToCon a

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))

The function runAbsToCon can target any monad that satisfies the constraints of MonadAbsToCon.

newtypenewtype AbsToCon a

Instances20Monad, Functor, MonadFail, Applicative, HasOptions, MonadReduce, …

Monad AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
Functor AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
MonadFail AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
Applicative AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
HasOptions AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
MonadReduce AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
MonadStConcreteNames AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
MonadTCEnv AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
ReadTCState AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
HasBuiltins AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
MonadAddContext AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
MonadDebug AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
MonadInteractionPoints AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
PureTCM AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
HasConstInfo AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
MonadReader Env AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
MonadFresh NameId AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
IsString (AbsToCon Doc)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
Semigroup (AbsToCon Doc)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
Null (AbsToCon Doc)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete

datadata Env

Instances1MonadReader

MonadReader Env AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete

valuenoTakenNames :: AbsToCon a -> AbsToCon a

valuelookupQName :: AllowAmbiguousNames -> QName -> AbsToCon QName