Agda-2.2.4: 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) ([] Declaration)) ToConcrete RHS ((,,) RHS ([] 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