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
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 #

Methods

toConcrete :: a -> AbsToCon c #

bindToConcrete :: a -> (c -> AbsToCon b) -> AbsToCon b #

Instances

ToConcrete InteractionId Expr #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: InteractionId -> AbsToCon Expr # bindToConcrete :: InteractionId -> (Expr -> AbsToCon b) -> AbsToCon b #
ToConcrete ModuleName QName #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: ModuleName -> AbsToCon QName # bindToConcrete :: ModuleName -> (QName -> AbsToCon b) -> AbsToCon b #
ToConcrete QName QName #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: QName -> AbsToCon QName0 # bindToConcrete :: QName -> (QName0 -> AbsToCon b) -> AbsToCon b #
ToConcrete Name Name #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Name -> AbsToCon Name0 # bindToConcrete :: Name -> (Name0 -> AbsToCon b) -> AbsToCon b #
ToConcrete ResolvedName QName #	Assumes name is not `UnknownName`.
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: ResolvedName -> AbsToCon QName # bindToConcrete :: ResolvedName -> (QName -> AbsToCon b) -> AbsToCon b #
ToConcrete AbstractName QName #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: AbstractName -> AbsToCon QName # bindToConcrete :: AbstractName -> (QName -> AbsToCon b) -> AbsToCon b #
ToConcrete Pattern Pattern #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Pattern -> AbsToCon Pattern0 # bindToConcrete :: Pattern -> (Pattern0 -> AbsToCon b) -> AbsToCon b #
ToConcrete LHSCore Pattern #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LHSCore -> AbsToCon Pattern # bindToConcrete :: LHSCore -> (Pattern -> AbsToCon b) -> AbsToCon b #
ToConcrete LHS LHS #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LHS -> AbsToCon LHS0 # bindToConcrete :: LHS -> (LHS0 -> AbsToCon b) -> AbsToCon b #
ToConcrete SpineLHS LHS #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: SpineLHS -> AbsToCon LHS # bindToConcrete :: SpineLHS -> (LHS -> AbsToCon b) -> AbsToCon b #
ToConcrete WhereDeclarations WhereClause #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: WhereDeclarations -> AbsToCon WhereClause # bindToConcrete :: WhereDeclarations -> (WhereClause -> AbsToCon b) -> AbsToCon b #
ToConcrete TypedBinding TypedBinding #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: TypedBinding -> AbsToCon TypedBinding0 # bindToConcrete :: TypedBinding -> (TypedBinding0 -> AbsToCon b) -> AbsToCon b #
ToConcrete ModuleApplication ModuleApplication #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: ModuleApplication -> AbsToCon ModuleApplication0 # bindToConcrete :: ModuleApplication -> (ModuleApplication0 -> AbsToCon b) -> AbsToCon b #
ToConcrete Expr Expr #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Expr -> AbsToCon Expr0 # bindToConcrete :: Expr -> (Expr0 -> AbsToCon b) -> AbsToCon b #
ToConcrete BindName Name #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: BindName -> AbsToCon Name # bindToConcrete :: BindName -> (Name -> AbsToCon b) -> AbsToCon b #
ToConcrete NamedMeta Expr #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: NamedMeta -> AbsToCon Expr # bindToConcrete :: NamedMeta -> (Expr -> AbsToCon b) -> AbsToCon b #
ToConcrete RangeAndPragma Pragma #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: RangeAndPragma -> AbsToCon Pragma # bindToConcrete :: RangeAndPragma -> (Pragma -> AbsToCon b) -> AbsToCon b #
ToConcrete TypedBindings [TypedBindings] #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: TypedBindings -> AbsToCon [TypedBindings0] # bindToConcrete :: TypedBindings -> ([TypedBindings0] -> AbsToCon b) -> AbsToCon b #
ToConcrete LamBinding [LamBinding] #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LamBinding -> AbsToCon [LamBinding0] # bindToConcrete :: LamBinding -> ([LamBinding0] -> AbsToCon b) -> AbsToCon b #
ToConcrete LetBinding [Declaration] #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LetBinding -> AbsToCon [Declaration] # bindToConcrete :: LetBinding -> ([Declaration] -> AbsToCon b) -> AbsToCon b #
ToConcrete Declaration [Declaration] #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Declaration -> AbsToCon [Declaration0] # bindToConcrete :: Declaration -> ([Declaration0] -> AbsToCon b) -> AbsToCon b #
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: RHS -> AbsToCon (RHS0, [Expr], [Expr], [Declaration]) # bindToConcrete :: RHS -> ((RHS0, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b #
ToConcrete (Constr Constructor) Declaration #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Constr Constructor -> AbsToCon Declaration # bindToConcrete :: Constr Constructor -> (Declaration -> AbsToCon b) -> AbsToCon b #
ToConcrete (DontTouchMe a) a #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: DontTouchMe a -> AbsToCon a # bindToConcrete :: DontTouchMe a -> (a -> AbsToCon b) -> AbsToCon b #
ToConcrete a c => ToConcrete [a] [c] #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: [a] -> AbsToCon [c] # bindToConcrete :: [a] -> ([c] -> AbsToCon b) -> AbsToCon b #
ToConcrete (Maybe QName) (Maybe Name) #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Maybe QName -> AbsToCon (Maybe Name) # bindToConcrete :: Maybe QName -> (Maybe Name -> AbsToCon b) -> AbsToCon b #
ToConcrete a c => ToConcrete (Arg a) (Arg c) #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Arg a -> AbsToCon (Arg c) # bindToConcrete :: Arg a -> (Arg c -> AbsToCon b) -> AbsToCon b #
ToConcrete a c => ToConcrete (WithHiding a) (WithHiding c) #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: WithHiding a -> AbsToCon (WithHiding c) # bindToConcrete :: WithHiding a -> (WithHiding c -> AbsToCon b) -> AbsToCon b #
ToConcrete a c => ToConcrete (FieldAssignment' a) (FieldAssignment' c) #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: FieldAssignment' a -> AbsToCon (FieldAssignment' c) # bindToConcrete :: FieldAssignment' a -> (FieldAssignment' c -> AbsToCon b) -> AbsToCon b #
ToConcrete a LHS => ToConcrete (Clause' a) [Declaration] #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Clause' a -> AbsToCon [Declaration] # bindToConcrete :: Clause' a -> ([Declaration] -> AbsToCon b) -> AbsToCon b #
(ToConcrete a1 c1, ToConcrete a2 c2) => ToConcrete (Either a1 a2) (Either c1 c2) #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Either a1 a2 -> AbsToCon (Either c1 c2) # bindToConcrete :: Either a1 a2 -> (Either c1 c2 -> AbsToCon b) -> AbsToCon b #
(ToConcrete a1 c1, ToConcrete a2 c2) => ToConcrete (a1, a2) (c1, c2) #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: (a1, a2) -> AbsToCon (c1, c2) # bindToConcrete :: (a1, a2) -> ((c1, c2) -> AbsToCon b) -> AbsToCon b #
ToConcrete a c => ToConcrete (Named name a) (Named name c) #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Named name a -> AbsToCon (Named name c) # bindToConcrete :: Named name a -> (Named name c -> AbsToCon b) -> AbsToCon b #
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint' a b) (OutputConstraint' c d) #
Instance details Defined in Agda.Interaction.BasicOps Methods toConcrete :: OutputConstraint' a b -> AbsToCon (OutputConstraint' c d) # bindToConcrete :: OutputConstraint' a b -> (OutputConstraint' c d -> AbsToCon b0) -> AbsToCon b0 #
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint a b) (OutputConstraint c d) #
Instance details Defined in Agda.Interaction.BasicOps Methods toConcrete :: OutputConstraint a b -> AbsToCon (OutputConstraint c d) # bindToConcrete :: OutputConstraint a b -> (OutputConstraint c d -> AbsToCon b0) -> AbsToCon b0 #
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputForm a b) (OutputForm c d) #
Instance details Defined in Agda.Interaction.BasicOps Methods toConcrete :: OutputForm a b -> AbsToCon (OutputForm c d) # bindToConcrete :: OutputForm a b -> (OutputForm c d -> AbsToCon b0) -> AbsToCon b0 #
(ToConcrete a1 c1, ToConcrete a2 c2, ToConcrete a3 c3) => ToConcrete (a1, a2, a3) (c1, c2, c3) #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: (a1, a2, a3) -> AbsToCon (c1, c2, c3) # bindToConcrete :: (a1, a2, a3) -> ((c1, c2, c3) -> AbsToCon b) -> AbsToCon b #

toConcreteCtx :: ToConcrete a c => Precedence -> a -> AbsToCon c #

Translate something in a context of the given precedence.

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 #

Constructors

RangeAndPragma Range Pragma

Instances

ToConcrete RangeAndPragma Pragma #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: RangeAndPragma -> AbsToCon Pragma # bindToConcrete :: RangeAndPragma -> (Pragma -> AbsToCon b) -> AbsToCon b #

abstractToConcreteCtx :: ToConcrete a c => Precedence -> a -> TCM c #

withScope :: ScopeInfo -> AbsToCon a -> AbsToCon a #

preserveInteractionIds :: AbsToCon a -> AbsToCon a #

type AbsToCon = ReaderT Env TCM #

We put the translation into TCM in order to print debug messages.

data DontTouchMe a #

Instances

ToConcrete (DontTouchMe a) a #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: DontTouchMe a -> AbsToCon a # bindToConcrete :: DontTouchMe a -> (a -> AbsToCon b) -> AbsToCon b #

data Env #

noTakenNames :: AbsToCon a -> AbsToCon a #