| 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.
Synopsis
- class ToConcrete a c | a -> c where
- toConcrete :: a -> AbsToCon c
- bindToConcrete :: a -> (c -> AbsToCon b) -> AbsToCon b
- toConcreteCtx :: ToConcrete a c => Precedence -> a -> AbsToCon c
- abstractToConcrete_ :: (ToConcrete a c, MonadAbsToCon m) => a -> m c
- abstractToConcreteScope :: (ToConcrete a c, MonadAbsToCon m) => ScopeInfo -> a -> m c
- abstractToConcreteHiding :: (LensHiding i, ToConcrete a c, MonadAbsToCon m) => i -> a -> m c
- runAbsToCon :: MonadAbsToCon m => AbsToCon c -> m c
- data RangeAndPragma = RangeAndPragma Range Pragma
- abstractToConcreteCtx :: (ToConcrete a c, MonadAbsToCon m) => Precedence -> a -> m c
- withScope :: ScopeInfo -> AbsToCon a -> AbsToCon a
- preserveInteractionIds :: AbsToCon a -> AbsToCon a
- type MonadAbsToCon m = (MonadTCEnv m, ReadTCState m, MonadStConcreteNames m, HasOptions m, HasBuiltins m, MonadDebug m)
- data AbsToCon a
- data Env
- noTakenNames :: AbsToCon a -> AbsToCon a
Documentation
class ToConcrete a c | a -> c where Source #
Minimal complete definition
Nothing
Methods
toConcrete :: a -> AbsToCon c Source #
bindToConcrete :: a -> (c -> AbsToCon b) -> AbsToCon b Source #
Instances
toConcreteCtx :: ToConcrete a c => Precedence -> a -> AbsToCon c Source #
Translate something in a context of the given precedence.
abstractToConcrete_ :: (ToConcrete a c, MonadAbsToCon m) => a -> m c Source #
abstractToConcreteScope :: (ToConcrete a c, MonadAbsToCon m) => ScopeInfo -> a -> m c Source #
abstractToConcreteHiding :: (LensHiding i, ToConcrete a c, MonadAbsToCon m) => i -> a -> m c Source #
runAbsToCon :: MonadAbsToCon m => AbsToCon c -> m c Source #
data RangeAndPragma Source #
Constructors
| RangeAndPragma Range Pragma |
Instances
| ToConcrete RangeAndPragma Pragma Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: RangeAndPragma -> AbsToCon Pragma Source # bindToConcrete :: RangeAndPragma -> (Pragma -> AbsToCon b) -> AbsToCon b Source # | |
abstractToConcreteCtx :: (ToConcrete a c, MonadAbsToCon m) => Precedence -> a -> m c Source #
preserveInteractionIds :: AbsToCon a -> AbsToCon a Source #
type MonadAbsToCon m = (MonadTCEnv m, ReadTCState m, MonadStConcreteNames m, HasOptions m, HasBuiltins m, MonadDebug m) Source #
We need: - Read access to the AbsToCon environment - Read access to the TC environment - Read access to the TC state - Read and write access to the stConcreteNames part of the TC state - Read access to the options - Permission to print debug messages
Instances
noTakenNames :: AbsToCon a -> AbsToCon a Source #