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

Safe HaskellNone
LanguageHaskell2010

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 #

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

Methods

toConcrete :: RHS -> AbsToCon (RHS, [Expr], [Expr], [Declaration]) #

bindToConcrete :: RHS -> ((RHS, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b #

ToConcrete (Constr Constructor) Declaration # 
ToConcrete (DontTouchMe a) a # 
ToConcrete a c => ToConcrete [a] [c] # 

Methods

toConcrete :: [a] -> AbsToCon [c] #

bindToConcrete :: [a] -> ([c] -> AbsToCon b) -> AbsToCon b #

ToConcrete (Maybe QName) (Maybe Name) # 
ToConcrete a c => ToConcrete (Arg a) (Arg c) # 

Methods

toConcrete :: Arg a -> AbsToCon (Arg c) #

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

ToConcrete a c => ToConcrete (WithHiding a) (WithHiding c) # 
ToConcrete a c => ToConcrete (FieldAssignment' a) (FieldAssignment' c) # 
ToConcrete a LHS => ToConcrete (Clause' a) [Declaration] # 
(ToConcrete a1 c1, ToConcrete a2 c2) => ToConcrete (Either a1 a2) (Either c1 c2) # 

Methods

toConcrete :: Either a1 a2 -> AbsToCon (Either c1 c2) #

bindToConcrete :: Either a1 a2 -> (Either c1 c2 -> AbsToCon b) -> AbsToCon b #

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

Methods

toConcrete :: (a1, a2) -> AbsToCon (c1, c2) #

bindToConcrete :: (a1, a2) -> ((c1, c2) -> AbsToCon b) -> AbsToCon b #

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

Methods

toConcrete :: Named name a -> AbsToCon (Named name c) #

bindToConcrete :: Named name a -> (Named name c -> AbsToCon b) -> AbsToCon b #

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

Methods

toConcrete :: (a1, a2, a3) -> AbsToCon (c1, c2, c3) #

bindToConcrete :: (a1, a2, a3) -> ((c1, c2, c3) -> AbsToCon b) -> AbsToCon b #

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

Translate something in a context of the given precedence.

type AbsToCon = ReaderT Env TCM #

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

data DontTouchMe a #

Instances

data Env #