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 where

Minimal complete definition

Nothing

Associated Types

type ConOfAbs a

Methods

toConcrete :: a -> AbsToCon (ConOfAbs a)

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

Instances

ToConcrete Bool

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Bool

Methods

toConcrete :: Bool -> AbsToCon (ConOfAbs Bool)

bindToConcrete :: Bool -> (ConOfAbs Bool -> AbsToCon b) -> AbsToCon b

ToConcrete ()

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ()

Methods

toConcrete :: () -> AbsToCon (ConOfAbs ())

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

ToConcrete InteractionId

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs InteractionId

Methods

toConcrete :: InteractionId -> AbsToCon (ConOfAbs InteractionId)

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

ToConcrete NamedMeta

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs NamedMeta

Methods

toConcrete :: NamedMeta -> AbsToCon (ConOfAbs NamedMeta)

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

ToConcrete ModuleName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleName

Methods

toConcrete :: ModuleName -> AbsToCon (ConOfAbs ModuleName)

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

ToConcrete QName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs QName

Methods

toConcrete :: QName -> AbsToCon (ConOfAbs QName)

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

ToConcrete Name

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Name

Methods

toConcrete :: Name -> AbsToCon (ConOfAbs Name)

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

ToConcrete ResolvedName

Assumes name is not UnknownName.

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ResolvedName

Methods

toConcrete :: ResolvedName -> AbsToCon (ConOfAbs ResolvedName)

bindToConcrete :: ResolvedName -> (ConOfAbs ResolvedName -> AbsToCon b) -> AbsToCon b

ToConcrete AbstractName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs AbstractName

Methods

toConcrete :: AbstractName -> AbsToCon (ConOfAbs AbstractName)

bindToConcrete :: AbstractName -> (ConOfAbs AbstractName -> AbsToCon b) -> AbsToCon b

ToConcrete Pattern

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Pattern

Methods

toConcrete :: Pattern -> AbsToCon (ConOfAbs Pattern)

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

ToConcrete LHSCore

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore

Methods

toConcrete :: LHSCore -> AbsToCon (ConOfAbs LHSCore)

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

ToConcrete LHS

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHS

Methods

toConcrete :: LHS -> AbsToCon (ConOfAbs LHS)

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

ToConcrete SpineLHS

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs SpineLHS

Methods

toConcrete :: SpineLHS -> AbsToCon (ConOfAbs SpineLHS)

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

ToConcrete RHS

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RHS

Methods

toConcrete :: RHS -> AbsToCon (ConOfAbs RHS)

bindToConcrete :: RHS -> (ConOfAbs RHS -> AbsToCon b) -> AbsToCon b

ToConcrete WhereDeclarations

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs WhereDeclarations

Methods

toConcrete :: WhereDeclarations -> AbsToCon (ConOfAbs WhereDeclarations)

bindToConcrete :: WhereDeclarations -> (ConOfAbs WhereDeclarations -> AbsToCon b) -> AbsToCon b

ToConcrete TypedBinding

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs TypedBinding

Methods

toConcrete :: TypedBinding -> AbsToCon (ConOfAbs TypedBinding)

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

ToConcrete LamBinding

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LamBinding

Methods

toConcrete :: LamBinding -> AbsToCon (ConOfAbs LamBinding)

bindToConcrete :: LamBinding -> (ConOfAbs LamBinding -> AbsToCon b) -> AbsToCon b

ToConcrete LetBinding

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LetBinding

Methods

toConcrete :: LetBinding -> AbsToCon (ConOfAbs LetBinding)

bindToConcrete :: LetBinding -> (ConOfAbs LetBinding -> AbsToCon b) -> AbsToCon b

ToConcrete ModuleApplication

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleApplication

Methods

toConcrete :: ModuleApplication -> AbsToCon (ConOfAbs ModuleApplication)

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

ToConcrete Declaration

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Declaration

Methods

toConcrete :: Declaration -> AbsToCon (ConOfAbs Declaration)

bindToConcrete :: Declaration -> (ConOfAbs Declaration -> AbsToCon b) -> AbsToCon b

ToConcrete Expr

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Expr

Methods

toConcrete :: Expr -> AbsToCon (ConOfAbs Expr)

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

ToConcrete BindName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs BindName

Methods

toConcrete :: BindName -> AbsToCon (ConOfAbs BindName)

bindToConcrete :: BindName -> (ConOfAbs BindName -> AbsToCon b) -> AbsToCon b

ToConcrete RangeAndPragma

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RangeAndPragma

Methods

toConcrete :: RangeAndPragma -> AbsToCon (ConOfAbs RangeAndPragma)

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

ToConcrete a => ToConcrete [a]

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs [a]

Methods

toConcrete :: [a] -> AbsToCon (ConOfAbs [a])

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

ToConcrete (Maybe QName)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe QName)

Methods

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

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

ToConcrete (Maybe Pattern)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe Pattern)

Methods

toConcrete :: Maybe Pattern -> AbsToCon (ConOfAbs (Maybe Pattern))

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

ToConcrete (Maybe BindName)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe BindName)

Methods

toConcrete :: Maybe BindName -> AbsToCon (ConOfAbs (Maybe BindName))

bindToConcrete :: Maybe BindName -> (ConOfAbs (Maybe BindName) -> AbsToCon b) -> AbsToCon b

ToConcrete a => ToConcrete (List1 a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (List1 a)

Methods

toConcrete :: List1 a -> AbsToCon (ConOfAbs (List1 a))

bindToConcrete :: List1 a -> (ConOfAbs (List1 a) -> AbsToCon b) -> AbsToCon b

ToConcrete (Constr Constructor)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Constr Constructor)

Methods

toConcrete :: Constr Constructor -> AbsToCon (ConOfAbs (Constr Constructor))

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

ToConcrete a => ToConcrete (Arg a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Arg a)

Methods

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

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

ToConcrete a => ToConcrete (WithHiding a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (WithHiding a)

Methods

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

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

ToConcrete a => ToConcrete (FieldAssignment' a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (FieldAssignment' a)

Methods

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

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

(ToConcrete a, ConOfAbs a ~ LHS) => ToConcrete (Clause' a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Clause' a)

Methods

toConcrete :: Clause' a -> AbsToCon (ConOfAbs (Clause' a))

bindToConcrete :: Clause' a -> (ConOfAbs (Clause' a) -> AbsToCon b) -> AbsToCon b

ToConcrete a => ToConcrete (Binder' a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Binder' a)

Methods

toConcrete :: Binder' a -> AbsToCon (ConOfAbs (Binder' a))

bindToConcrete :: Binder' a -> (ConOfAbs (Binder' a) -> AbsToCon b) -> AbsToCon b

ToConcrete a => ToConcrete (IPBoundary' a)

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (IPBoundary' a)

Methods

toConcrete :: IPBoundary' a -> AbsToCon (ConOfAbs (IPBoundary' a))

bindToConcrete :: IPBoundary' a -> (ConOfAbs (IPBoundary' a) -> AbsToCon b) -> AbsToCon b

(ToConcrete a1, ToConcrete a2) => ToConcrete (Either a1 a2)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Either a1 a2)

Methods

toConcrete :: Either a1 a2 -> AbsToCon (ConOfAbs (Either a1 a2))

bindToConcrete :: Either a1 a2 -> (ConOfAbs (Either a1 a2) -> AbsToCon b) -> AbsToCon b

(ToConcrete a1, ToConcrete a2) => ToConcrete (a1, a2)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (a1, a2)

Methods

toConcrete :: (a1, a2) -> AbsToCon (ConOfAbs (a1, a2))

bindToConcrete :: (a1, a2) -> (ConOfAbs (a1, a2) -> AbsToCon b) -> AbsToCon b

ToConcrete a => ToConcrete (Named name a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Named name a)

Methods

toConcrete :: Named name a -> AbsToCon (ConOfAbs (Named name a))

bindToConcrete :: Named name a -> (ConOfAbs (Named name a) -> AbsToCon b) -> AbsToCon b

(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint' a b)

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputConstraint' a b)

Methods

toConcrete :: OutputConstraint' a b -> AbsToCon (ConOfAbs (OutputConstraint' a b))

bindToConcrete :: OutputConstraint' a b -> (ConOfAbs (OutputConstraint' a b) -> AbsToCon b0) -> AbsToCon b0

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

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputConstraint a b)

Methods

toConcrete :: OutputConstraint a b -> AbsToCon (ConOfAbs (OutputConstraint a b))

bindToConcrete :: OutputConstraint a b -> (ConOfAbs (OutputConstraint a b) -> AbsToCon b0) -> AbsToCon b0

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

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputForm a b)

Methods

toConcrete :: OutputForm a b -> AbsToCon (ConOfAbs (OutputForm a b))

bindToConcrete :: OutputForm a b -> (ConOfAbs (OutputForm a b) -> AbsToCon b0) -> AbsToCon b0

(ToConcrete a1, ToConcrete a2, ToConcrete a3) => ToConcrete (a1, a2, a3)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (a1, a2, a3)

Methods

toConcrete :: (a1, a2, a3) -> AbsToCon (ConOfAbs (a1, a2, a3))

bindToConcrete :: (a1, a2, a3) -> (ConOfAbs (a1, a2, a3) -> AbsToCon b) -> AbsToCon b

(ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (RewriteEqn' qn BindName p a)

Methods

toConcrete :: RewriteEqn' qn BindName p a -> AbsToCon (ConOfAbs (RewriteEqn' qn BindName p a))

bindToConcrete :: RewriteEqn' qn BindName p a -> (ConOfAbs (RewriteEqn' qn BindName p a) -> AbsToCon b) -> AbsToCon b

toConcreteCtx :: ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)

Translate something in a context of the given precedence.

abstractToConcrete_ :: (ToConcrete a, MonadAbsToCon m) => a -> m (ConOfAbs a)

abstractToConcreteScope :: (ToConcrete a, MonadAbsToCon m) => ScopeInfo -> a -> m (ConOfAbs a)

abstractToConcreteHiding :: (LensHiding i, ToConcrete a, MonadAbsToCon m) => i -> a -> m (ConOfAbs a)

runAbsToCon :: MonadAbsToCon m => AbsToCon c -> m c

data RangeAndPragma

Constructors

RangeAndPragma Range Pragma

Instances

ToConcrete RangeAndPragma

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RangeAndPragma

Methods

toConcrete :: RangeAndPragma -> AbsToCon (ConOfAbs RangeAndPragma)

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

type ConOfAbs RangeAndPragma

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs RangeAndPragma = Pragma

abstractToConcreteCtx :: (ToConcrete a, MonadAbsToCon m) => Precedence -> a -> m (ConOfAbs a)

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)

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

data AbsToCon a

Instances

Monad AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

(>>=) :: AbsToCon a -> (a -> AbsToCon b) -> AbsToCon b

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

return :: a -> AbsToCon a

Functor AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

fmap :: (a -> b) -> AbsToCon a -> AbsToCon b

(<$) :: a -> AbsToCon b -> AbsToCon a

MonadFail AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

fail :: String -> AbsToCon a

Applicative AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

pure :: a -> AbsToCon a

(<*>) :: AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b

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

(*>) :: AbsToCon a -> AbsToCon b -> AbsToCon b

(<*) :: AbsToCon a -> AbsToCon b -> AbsToCon a

HasOptions AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

pragmaOptions :: AbsToCon PragmaOptions

commandLineOptions :: AbsToCon CommandLineOptions

MonadTCEnv AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

askTC :: AbsToCon TCEnv

localTC :: (TCEnv -> TCEnv) -> AbsToCon a -> AbsToCon a

MonadStConcreteNames AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

runStConcreteNames :: StateT ConcreteNames AbsToCon a -> AbsToCon a

useConcreteNames :: AbsToCon ConcreteNames

modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> AbsToCon ()

ReadTCState AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

getTCState :: AbsToCon TCState

locallyTCState :: Lens' a TCState -> (a -> a) -> AbsToCon b -> AbsToCon b

withTCState :: (TCState -> TCState) -> AbsToCon a -> AbsToCon a

HasBuiltins AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

getBuiltinThing :: String -> AbsToCon (Maybe (Builtin PrimFun))

MonadDebug AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> AbsToCon String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> AbsToCon a -> AbsToCon a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> AbsToCon a -> AbsToCon a

getVerbosity :: AbsToCon Verbosity

isDebugPrinting :: AbsToCon Bool

nowDebugPrinting :: AbsToCon a -> AbsToCon a

MonadReader Env AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

ask :: AbsToCon Env

local :: (Env -> Env) -> AbsToCon a -> AbsToCon a

reader :: (Env -> a) -> AbsToCon a

data Env

Instances

MonadReader Env AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

ask :: AbsToCon Env

local :: (Env -> Env) -> AbsToCon a -> AbsToCon a

reader :: (Env -> a) -> AbsToCon a

noTakenNames :: AbsToCon a -> AbsToCon a

lookupQName :: AllowAmbiguousNames -> QName -> AbsToCon QName