Safe Haskell | None |
---|---|
Language | Haskell2010 |
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.
- class ToConcrete a c | a -> c where
- toConcreteCtx :: ToConcrete a c => Precedence -> a -> AbsToCon c
- abstractToConcrete_ :: ToConcrete a c => a -> TCM c
- abstractToConcreteEnv :: ToConcrete a c => Env -> a -> TCM c
- runAbsToCon :: AbsToCon c -> TCM c
- data RangeAndPragma = RangeAndPragma Range Pragma
- abstractToConcreteCtx :: ToConcrete a c => Precedence -> a -> TCM c
- withScope :: ScopeInfo -> AbsToCon a -> AbsToCon a
- makeEnv :: ScopeInfo -> Env
- type AbsToCon = ReaderT Env TCM
- data DontTouchMe a
- data Env
- noTakenNames :: AbsToCon a -> AbsToCon a
Documentation
class ToConcrete a c | a -> c where #
Instances
toConcreteCtx :: ToConcrete a c => Precedence -> a -> AbsToCon c #
Translate something in a context of the given precedence.
abstractToConcrete_ :: ToConcrete a c => a -> TCM c #
abstractToConcreteEnv :: ToConcrete a c => Env -> a -> TCM c #
runAbsToCon :: AbsToCon c -> TCM c #
abstractToConcreteCtx :: ToConcrete a c => Precedence -> a -> TCM c #
data DontTouchMe a #
Instances
ToConcrete (DontTouchMe a) a # | |
noTakenNames :: AbsToCon a -> AbsToCon a #