Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 whereSource
Methods
toConcrete :: a -> AbsToCon cSource
bindToConcrete :: a -> (c -> AbsToCon b) -> AbsToCon bSource
abstractToConcrete_ :: (MonadTCM tcm, ToConcrete a c) => a -> tcm cSource
runAbsToCon :: MonadTCM tcm => AbsToCon a -> tcm aSource
data RangeAndPragma Source
Constructors
RangeAndPragma Range Pragma
abstractToConcreteCtx :: (MonadTCM tcm, ToConcrete a c) => Precedence -> a -> tcm cSource
withScope :: ScopeInfo -> AbsToCon a -> AbsToCon aSource
makeEnv :: ScopeInfo -> EnvSource
abstractToConcrete :: ToConcrete a c => Env -> a -> cSource
type AbsToCon = Reader EnvSource
We make the translation monadic for modularity purposes.
data TypeAndDef Source
data DontTouchMe a Source
data Env Source
Produced by Haddock version 2.6.0