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

Safe Haskell | None

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_ :: ToConcrete a c => a -> TCM c
- runAbsToCon :: AbsToCon a -> TCM a
- data RangeAndPragma = RangeAndPragma Range Pragma
- abstractToConcreteCtx :: 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 DontTouchMe a
- data Env
- noTakenNames :: AbsToCon a -> AbsToCon a

# 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 Pattern Pattern |
ToConcrete LHSCore Pattern |
ToConcrete LHS LHS |
ToConcrete TypedBinding TypedBinding |
ToConcrete TypedBindings TypedBindings |
ToConcrete LamBinding LamBinding |
ToConcrete ModuleApplication ModuleApplication |
ToConcrete Expr Expr |
ToConcrete InteractionId Expr |
ToConcrete NamedMeta Expr |
ToConcrete RangeAndPragma Pragma |
ToConcrete AsWhereDecls WhereClause |
ToConcrete Clause [Declaration] |
ToConcrete LetBinding [Declaration] |
ToConcrete Declaration [Declaration] |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) |
ToConcrete (Constr Constructor) Declaration |
ToConcrete (DontTouchMe a) a |
ToConcrete a c => ToConcrete [a] [c] |
ToConcrete (Maybe QName) (Maybe Name) |
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 (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) |

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

Translate something in a context of the given precedence.

abstractToConcrete_ :: ToConcrete a c => a -> TCM c

runAbsToCon :: AbsToCon a -> TCM a

data RangeAndPragma

Constructors

RangeAndPragma Range Pragma |

Instances

ToConcrete RangeAndPragma Pragma |

abstractToConcreteCtx :: 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 DontTouchMe a

Instances

ToConcrete (DontTouchMe a) a |

data Env

noTakenNames :: AbsToCon a -> AbsToCon a