Agda-2.4.2.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.Syntax.Translation.AbstractToConcrete

Description

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.

Synopsis

Documentation

class ToConcrete a c | a -> c where Source

Minimal complete definition

Nothing

Methods

toConcrete :: a -> AbsToCon c Source

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

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

Translate something in a context of the given precedence.

type AbsToCon = ReaderT Env TCM Source

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

data DontTouchMe a Source

Instances

data Env Source