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
- 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
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
abstractToConcreteCtx :: (MonadTCM tcm, ToConcrete a c) => Precedence -> a -> tcm cSource
abstractToConcrete :: ToConcrete a c => Env -> a -> cSource
data DontTouchMe a Source
ToConcrete (DontTouchMe a) a |