Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

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

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 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 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 BoundName Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: BindName -> AbsToCon BoundName Source # bindToConcrete :: BindName -> (BoundName -> 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 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 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 Env Source #

noTakenNames :: AbsToCon a -> AbsToCon a Source #