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

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

- class ToConcrete a c | a -> c where
  - toConcrete :: a -> AbsToCon c
  - bindToConcrete :: a -> (c -> AbsToCon b) -> AbsToCon b
- toConcreteCtx :: ToConcrete a c => Precedence -> a -> AbsToCon c
- abstractToConcrete_ :: (MonadTCM tcm, ToConcrete a c) => a -> tcm c
- runAbsToCon :: MonadTCM tcm => AbsToCon a -> tcm a
- data RangeAndPragma = RangeAndPragma Range Pragma
- abstractToConcreteCtx :: (MonadTCM tcm, ToConcrete a c) => Precedence -> a -> tcm c
- withScope :: ScopeInfo -> AbsToCon a -> AbsToCon a
- makeEnv :: ScopeInfo -> Env
- abstractToConcrete :: ToConcrete a c => Env -> a -> c
- type AbsToCon = Reader Env
- data TypeAndDef
- data DontTouchMe a
- data Env

# Documentation

class ToConcrete a c | a -> c where

Methods

toConcrete :: a -> AbsToCon c

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

Instances

ToConcrete ModuleName QName |
ToConcrete QName QName |
ToConcrete Name Name |
ToConcrete MetaId Expr |
ToConcrete Pattern Pattern |
ToConcrete LHS LHS |
ToConcrete TypedBinding TypedBinding |
ToConcrete TypedBindings TypedBindings |
ToConcrete LamBinding LamBinding |
ToConcrete Expr Expr |
ToConcrete InteractionId Expr |
ToConcrete RangeAndPragma Pragma |
ToConcrete AsWhereDecls WhereClause |
ToConcrete Clause [Declaration] |
ToConcrete LetBinding [Declaration] |
ToConcrete Declaration [Declaration] |
ToConcrete TypeAndDef [Declaration] |
ToConcrete RHS (RHS, [Expr], [Expr], [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) |

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

Translate something in a context of the given precedence.

abstractToConcrete_ :: (MonadTCM tcm, ToConcrete a c) => a -> tcm c

runAbsToCon :: MonadTCM tcm => AbsToCon a -> tcm a

data RangeAndPragma

Constructors

RangeAndPragma Range Pragma |

Instances

ToConcrete RangeAndPragma Pragma |

abstractToConcreteCtx :: (MonadTCM tcm, ToConcrete a c) => Precedence -> a -> tcm c

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

makeEnv :: ScopeInfo -> Env

abstractToConcrete :: ToConcrete a c => Env -> a -> c

type AbsToCon = Reader Env

We make the translation monadic for modularity purposes.

data TypeAndDef

Instances

ToConcrete TypeAndDef [Declaration] |

data DontTouchMe a

Instances

ToConcrete (DontTouchMe a) a |

data Env