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.

Documentation

class ToConcrete a c | a -> c where

Methods

toConcrete :: a -> AbsToCon c

bindToConcrete :: a -> (c -> AbsToCon b) -> AbsToCon b

Instances

ToConcrete InteractionId Expr

ToConcrete ModuleName QName

ToConcrete QName QName

ToConcrete Name Name

ToConcrete Pattern Pattern

ToConcrete LHSCore Pattern

ToConcrete LHS LHS

ToConcrete SpineLHS LHS

ToConcrete TypedBinding TypedBinding

ToConcrete ModuleApplication ModuleApplication

ToConcrete Expr Expr

ToConcrete NamedMeta Expr

ToConcrete RangeAndPragma Pragma

ToConcrete TypedBindings [TypedBindings]

ToConcrete LamBinding [LamBinding]

ToConcrete LetBinding [Declaration]

ToConcrete Declaration [Declaration]

ToConcrete RHS (RHS, [Expr], [Expr], [Declaration])

ToConcrete (Constr Constructor) Declaration

ToConcrete (ArgInfo ac) ArgInfo

ToConcrete (DontTouchMe a) a

ToConcrete a c => ToConcrete [a] [c]

ToConcrete (Maybe QName) (Maybe Name)

ToConcrete a LHS => ToConcrete (Clause' a) [Declaration]

ToConcrete a c => ToConcrete (Arg ac a) (Arg c)

(ToConcrete a1 c1, ToConcrete a2 c2) => ToConcrete (a1, a2) (c1, c2)

ToConcrete a c => ToConcrete (Named name a) (Named name c)

(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint' a b) (OutputConstraint' c d)

(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint a b) (OutputConstraint c d)

(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputForm a b) (OutputForm c d)

(ToConcrete a1 c1, ToConcrete a2 c2, ToConcrete a3 c3) => ToConcrete (a1, a2, a3) (c1, c2, c3)

toConcreteCtx :: ToConcrete a c => Precedence -> a -> AbsToCon c

Translate something in a context of the given precedence.

abstractToConcrete_ :: ToConcrete a c => a -> TCM c

abstractToConcreteEnv :: ToConcrete a c => Env -> a -> TCM c

runAbsToCon :: AbsToCon c -> TCM c

data RangeAndPragma

Constructors

RangeAndPragma Range Pragma

Instances

ToConcrete RangeAndPragma Pragma

abstractToConcreteCtx :: ToConcrete a c => Precedence -> a -> TCM c

withScope :: ScopeInfo -> AbsToCon a -> AbsToCon a

makeEnv :: ScopeInfo -> Env

type AbsToCon = ReaderT Env TCM

We put the translation into TCM in order to print debug messages.

data DontTouchMe a

Instances

ToConcrete (DontTouchMe a) a

data Env

noTakenNames :: AbsToCon a -> AbsToCon a