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

Methods

toConcrete :: a -> AbsToCon c Source #

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

Instances

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

data RangeAndPragma Source #

Constructors

RangeAndPragma Range Pragma

Instances

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

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

withScope :: ScopeInfo -> AbsToCon a -> AbsToCon a 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 #

Instances

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

data Env Source #

noTakenNames :: AbsToCon a -> AbsToCon a Source #