Agda.Syntax.Translation.AbstractToConcrete

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.

Documentation

class ToConcrete a c | a -> c where

Methods

toConcrete :: a -> AbsToCon c

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

Instances

ToConcrete InteractionId Expr

Methods

toConcrete :: InteractionId -> AbsToCon Expr

bindToConcrete :: InteractionId -> (Expr -> AbsToCon b) -> AbsToCon b

ToConcrete ModuleName QName

Methods

toConcrete :: ModuleName -> AbsToCon QName

bindToConcrete :: ModuleName -> (QName -> AbsToCon b) -> AbsToCon b

ToConcrete QName QName

Methods

toConcrete :: QName -> AbsToCon QName

bindToConcrete :: QName -> (QName -> AbsToCon b) -> AbsToCon b

ToConcrete Name Name

Methods

toConcrete :: Name -> AbsToCon Name

bindToConcrete :: Name -> (Name -> AbsToCon b) -> AbsToCon b

ToConcrete Pattern Pattern

Methods

toConcrete :: Pattern -> AbsToCon Pattern

bindToConcrete :: Pattern -> (Pattern -> AbsToCon b) -> AbsToCon b

ToConcrete LHSCore Pattern

Methods

toConcrete :: LHSCore -> AbsToCon Pattern

bindToConcrete :: LHSCore -> (Pattern -> AbsToCon b) -> AbsToCon b

ToConcrete LHS LHS

Methods

toConcrete :: LHS -> AbsToCon LHS

bindToConcrete :: LHS -> (LHS -> AbsToCon b) -> AbsToCon b

ToConcrete SpineLHS LHS

Methods

toConcrete :: SpineLHS -> AbsToCon LHS

bindToConcrete :: SpineLHS -> (LHS -> AbsToCon b) -> AbsToCon b

ToConcrete TypedBinding TypedBinding

Methods

toConcrete :: TypedBinding -> AbsToCon TypedBinding

bindToConcrete :: TypedBinding -> (TypedBinding -> AbsToCon b) -> AbsToCon b

ToConcrete ModuleApplication ModuleApplication

Methods

toConcrete :: ModuleApplication -> AbsToCon ModuleApplication

bindToConcrete :: ModuleApplication -> (ModuleApplication -> AbsToCon b) -> AbsToCon b

ToConcrete Expr Expr

Methods

toConcrete :: Expr -> AbsToCon Expr

bindToConcrete :: Expr -> (Expr -> AbsToCon b) -> AbsToCon b

ToConcrete NamedMeta Expr

Methods

toConcrete :: NamedMeta -> AbsToCon Expr

bindToConcrete :: NamedMeta -> (Expr -> AbsToCon b) -> AbsToCon b

ToConcrete RangeAndPragma Pragma

Methods

toConcrete :: RangeAndPragma -> AbsToCon Pragma

bindToConcrete :: RangeAndPragma -> (Pragma -> AbsToCon b) -> AbsToCon b

ToConcrete TypedBindings [TypedBindings]

Methods

toConcrete :: TypedBindings -> AbsToCon [TypedBindings]

bindToConcrete :: TypedBindings -> ([TypedBindings] -> AbsToCon b) -> AbsToCon b

ToConcrete LamBinding [LamBinding]

Methods

toConcrete :: LamBinding -> AbsToCon [LamBinding]

bindToConcrete :: LamBinding -> ([LamBinding] -> AbsToCon b) -> AbsToCon b

ToConcrete LetBinding [Declaration]

Methods

toConcrete :: LetBinding -> AbsToCon [Declaration]

bindToConcrete :: LetBinding -> ([Declaration] -> AbsToCon b) -> AbsToCon b

ToConcrete Declaration [Declaration]

Methods

toConcrete :: Declaration -> AbsToCon [Declaration]

bindToConcrete :: Declaration -> ([Declaration] -> AbsToCon b) -> AbsToCon b

ToConcrete RHS (RHS, [Expr], [Expr], [Declaration])

Methods

toConcrete :: RHS -> AbsToCon (RHS, [Expr], [Expr], [Declaration])

bindToConcrete :: RHS -> ((RHS, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b

ToConcrete (Constr Constructor) Declaration

Methods

toConcrete :: Constr Constructor -> AbsToCon Declaration

bindToConcrete :: Constr Constructor -> (Declaration -> AbsToCon b) -> AbsToCon b

ToConcrete (DontTouchMe a) a

Methods

toConcrete :: DontTouchMe a -> AbsToCon a

bindToConcrete :: DontTouchMe a -> (a -> AbsToCon b) -> AbsToCon b

ToConcrete a c => ToConcrete [a] [c]

Methods

toConcrete :: [a] -> AbsToCon [c]

bindToConcrete :: [a] -> ([c] -> AbsToCon b) -> AbsToCon b

ToConcrete (Maybe QName) (Maybe Name)

Methods

toConcrete :: Maybe QName -> AbsToCon (Maybe Name)

bindToConcrete :: Maybe QName -> (Maybe Name -> AbsToCon b) -> AbsToCon b

ToConcrete a c => ToConcrete (Arg a) (Arg c)

Methods

toConcrete :: Arg a -> AbsToCon (Arg c)

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

ToConcrete a c => ToConcrete (WithHiding a) (WithHiding c)

Methods

toConcrete :: WithHiding a -> AbsToCon (WithHiding c)

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

ToConcrete a c => ToConcrete (FieldAssignment' a) (FieldAssignment' c)

Methods

toConcrete :: FieldAssignment' a -> AbsToCon (FieldAssignment' c)

bindToConcrete :: FieldAssignment' a -> (FieldAssignment' c -> AbsToCon b) -> AbsToCon b

ToConcrete a LHS => ToConcrete (Clause' a) [Declaration]

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)

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)

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)

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)

Methods

toConcrete :: OutputConstraint' a b -> AbsToCon (OutputConstraint' c d)

bindToConcrete :: OutputConstraint' a b -> (OutputConstraint' c d -> AbsToCon b) -> AbsToCon b

(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint a b) (OutputConstraint c d)

Methods

toConcrete :: OutputConstraint a b -> AbsToCon (OutputConstraint c d)

bindToConcrete :: OutputConstraint a b -> (OutputConstraint c d -> AbsToCon b) -> AbsToCon b

(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputForm a b) (OutputForm c d)

Methods

toConcrete :: OutputForm a b -> AbsToCon (OutputForm c d)

bindToConcrete :: OutputForm a b -> (OutputForm c d -> AbsToCon b) -> AbsToCon b

(ToConcrete a1 c1, ToConcrete a2 c2, ToConcrete a3 c3) => ToConcrete (a1, a2, a3) (c1, c2, c3)

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

abstractToConcreteEnv :: ToConcrete a c => Env -> a -> TCM c

runAbsToCon :: AbsToCon c -> TCM c

data RangeAndPragma

Constructors

RangeAndPragma Range Pragma

Instances

ToConcrete RangeAndPragma Pragma

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

makeEnv :: ScopeInfo -> Env

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

Methods

toConcrete :: DontTouchMe a -> AbsToCon a

bindToConcrete :: DontTouchMe a -> (a -> AbsToCon b) -> AbsToCon b

data Env

noTakenNames :: AbsToCon a -> AbsToCon a