Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
- abstractToConcreteScope :: ToConcrete a c => ScopeInfo -> a -> TCM c
- abstractToConcreteHiding :: (LensHiding i, ToConcrete a c) => i -> 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
- preserveInteractionIds :: AbsToCon a -> AbsToCon a
- type AbsToCon = ReaderT Env TCM
- data DontTouchMe a
- data Env
- noTakenNames :: AbsToCon a -> AbsToCon a
Documentation
class ToConcrete a c | a -> c where Source #
toConcrete :: a -> AbsToCon c Source #
bindToConcrete :: a -> (c -> AbsToCon b) -> AbsToCon b Source #
toConcreteCtx :: ToConcrete a c => Precedence -> a -> AbsToCon c Source #
Translate something in a context of the given precedence.
abstractToConcrete_ :: ToConcrete a c => a -> TCM c Source #
abstractToConcreteScope :: ToConcrete a c => ScopeInfo -> a -> TCM c Source #
abstractToConcreteHiding :: (LensHiding i, ToConcrete a c) => i -> a -> TCM c Source #
runAbsToCon :: AbsToCon c -> TCM c Source #
abstractToConcreteCtx :: ToConcrete a c => Precedence -> a -> TCM c Source #
preserveInteractionIds :: AbsToCon a -> AbsToCon a Source #
type AbsToCon = ReaderT Env TCM Source #
We put the translation into TCM in order to print debug messages.
data DontTouchMe a Source #
ToConcrete (DontTouchMe a) a Source # | |
noTakenNames :: AbsToCon a -> AbsToCon a Source #