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_ :: (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
Translate something in a context of the given precedence.