|
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 |
|
| Methods | | | Instances | ToConcrete ModuleName QName | ToConcrete ModuleName QName | ToConcrete QName QName | ToConcrete QName QName | ToConcrete Name Name | ToConcrete Name Name | ToConcrete MetaId Expr | ToConcrete MetaId Expr | ToConcrete Pattern Pattern | ToConcrete Pattern Pattern | ToConcrete LHS LHS | ToConcrete LHS LHS | ToConcrete TypedBinding TypedBinding | ToConcrete TypedBinding TypedBinding | ToConcrete TypedBindings TypedBindings | ToConcrete TypedBindings TypedBindings | ToConcrete LamBinding LamBinding | ToConcrete LamBinding LamBinding | ToConcrete Expr Expr | ToConcrete Expr Expr | ToConcrete InteractionId Expr | ToConcrete InteractionId Expr | ToConcrete RangeAndPragma Pragma | ToConcrete RangeAndPragma Pragma | ToConcrete Clause ([] Declaration) | ToConcrete Clause ([] Declaration) | ToConcrete LetBinding ([] Declaration) | ToConcrete LetBinding ([] Declaration) | ToConcrete Declaration ([] Declaration) | ToConcrete Declaration ([] Declaration) | ToConcrete TypeAndDef ([] Declaration) | ToConcrete TypeAndDef ([] Declaration) | ToConcrete RHS ((,,,) RHS ([] Expr) ([] Expr) ([] Declaration)) | ToConcrete RHS ((,,,) RHS ([] Expr) ([] Expr) ([] Declaration)) | ToConcrete (Constr Constructor) Declaration | ToConcrete (Constr Constructor) Declaration | ToConcrete (DontTouchMe a) a | ToConcrete a c => ToConcrete ([] a) ([] c) | ToConcrete ([] Declaration) ([] Declaration) | ToConcrete a c => ToConcrete (Arg 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 (OutputForm' a b) (OutputForm' 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) |
|
|
|
|
|
|
|
|
Constructors | | Instances | |
|
|
|
|
|
|
|
|
|
|
|
We make the translation monadic for modularity purposes.
|
|
|
Instances | |
|
|
|
Instances | |
|
|
|
|
Produced by Haddock version 2.4.2 |