Safe Haskell	None
Language	Haskell98

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

Instances

ToConcrete InteractionId Expr Source
ToConcrete ModuleName QName Source
ToConcrete QName QName Source
ToConcrete Name Name Source
ToConcrete Pattern Pattern Source
ToConcrete LHSCore Pattern Source
ToConcrete LHS LHS Source
ToConcrete SpineLHS LHS Source
ToConcrete TypedBinding TypedBinding Source
ToConcrete ModuleApplication ModuleApplication Source
ToConcrete Expr Expr Source
ToConcrete NamedMeta Expr Source
ToConcrete RangeAndPragma Pragma Source
ToConcrete TypedBindings [TypedBindings] Source
ToConcrete LamBinding [LamBinding] Source
ToConcrete LetBinding [Declaration] Source
ToConcrete Declaration [Declaration] Source
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) Source
ToConcrete (Constr Constructor) Declaration Source
ToConcrete (ArgInfo ac) ArgInfo Source
ToConcrete (DontTouchMe a) a Source
ToConcrete a c => ToConcrete [a] [c] Source
ToConcrete (Maybe QName) (Maybe Name) Source
ToConcrete a c => ToConcrete (WithHiding a) (WithHiding c) Source
ToConcrete a LHS => ToConcrete (Clause' a) [Declaration] Source
ToConcrete a c => ToConcrete (Arg ac a) (Arg c) Source
(ToConcrete a1 c1, ToConcrete a2 c2) => ToConcrete (a1, a2) (c1, c2) Source
ToConcrete a c => ToConcrete (Named name a) (Named name c) Source
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint' a b) (OutputConstraint' c d) Source
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint a b) (OutputConstraint c d) Source
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputForm a b) (OutputForm c d) Source
(ToConcrete a1 c1, ToConcrete a2 c2, ToConcrete a3 c3) => ToConcrete (a1, a2, a3) (c1, c2, c3) Source