| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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

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 | Source

Methods

toConcrete :: a -> AbsToCon c | Source

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

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)

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

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

data RangeAndPragma | Source

Constructors

RangeAndPragma Range Pragma |

Instances

ToConcrete RangeAndPragma Pragma

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

withScope :: ScopeInfo -> AbsToCon a -> AbsToCon a | Source

makeEnv :: ScopeInfo -> Env | Source

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

type AbsToCon = Reader Env | Source

We make the translation monadic for modularity purposes.

data TypeAndDef | Source

Instances

ToConcrete TypeAndDef ([] Declaration)

data DontTouchMe a | Source

Instances

ToConcrete (DontTouchMe a) a

data Env | Source

Produced by Haddock version 2.4.2