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 where
- type ConOfAbs a
- toConcrete :: MonadToConcrete m => a -> m (ConOfAbs a)
- bindToConcrete :: MonadToConcrete m => a -> (ConOfAbs a -> m b) -> m b
toConcreteCtx :: (MonadToConcrete m, ToConcrete a) => Precedence -> a -> m (ConOfAbs a)
type MonadAbsToCon (m :: Type -> Type) = (MonadFresh NameId m, MonadInteractionPoints m, MonadStConcreteNames m, HasOptions m, PureTCM m, IsString (m Doc), Null (m Doc), Semigroup (m Doc))
abstractToConcrete_ :: (ToConcrete a, MonadAbsToCon m) => a -> m (ConOfAbs a)
abstractToConcreteCtx :: (ToConcrete a, MonadAbsToCon m) => Precedence -> a -> m (ConOfAbs a)
abstractToConcreteHiding :: (LensHiding i, ToConcrete a, MonadAbsToCon m) => i -> a -> m (ConOfAbs a)
abstractToConcreteQName :: MonadAbsToCon m => AllowAmbiguousNames -> QName -> m QName
abstractToConcreteScope :: (ToConcrete a, MonadAbsToCon m) => ScopeInfo -> a -> m (ConOfAbs a)
abstractToConcreteTelescope :: MonadAbsToCon m => Telescope -> m [Maybe TypedBinding]
abstractToConcreteUnqualify :: (ToConcrete a, MonadAbsToCon m) => a -> m (ConOfAbs a)
data RangeAndPragma = RangeAndPragma Range Pragma
noTakenNames :: MonadToConcrete m => m a -> m a

Documentation

class ToConcrete a where Source #

Minimal complete definition

toConcrete | bindToConcrete

Associated Types

type ConOfAbs a Source #

Methods

toConcrete :: MonadToConcrete m => a -> m (ConOfAbs a) Source #

bindToConcrete :: MonadToConcrete m => a -> (ConOfAbs a -> m b) -> m b Source #

Instances

Instances details

ToConcrete BindName Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs BindName
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs BindName = BoundName

Methods

toConcrete :: MonadToConcrete m => BindName -> m (ConOfAbs BindName) Source #

bindToConcrete :: MonadToConcrete m => BindName -> (ConOfAbs BindName -> m b) -> m b Source #

ToConcrete Declaration Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Declaration
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Declaration = [Declaration]

Methods

toConcrete :: MonadToConcrete m => Declaration -> m (ConOfAbs Declaration) Source #

bindToConcrete :: MonadToConcrete m => Declaration -> (ConOfAbs Declaration -> m b) -> m b Source #

ToConcrete Expr Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Expr
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Expr = Expr

Methods

toConcrete :: MonadToConcrete m => Expr -> m (ConOfAbs Expr) Source #

bindToConcrete :: MonadToConcrete m => Expr -> (ConOfAbs Expr -> m b) -> m b Source #

ToConcrete LHS Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHS
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LHS = LHS

Methods

toConcrete :: MonadToConcrete m => LHS -> m (ConOfAbs LHS) Source #

bindToConcrete :: MonadToConcrete m => LHS -> (ConOfAbs LHS -> m b) -> m b Source #

ToConcrete LHSCore Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LHSCore = Pattern

Methods

toConcrete :: MonadToConcrete m => LHSCore -> m (ConOfAbs LHSCore) Source #

bindToConcrete :: MonadToConcrete m => LHSCore -> (ConOfAbs LHSCore -> m b) -> m b Source #

ToConcrete LamBinding Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LamBinding
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LamBinding = Maybe LamBinding

Methods

toConcrete :: MonadToConcrete m => LamBinding -> m (ConOfAbs LamBinding) Source #

bindToConcrete :: MonadToConcrete m => LamBinding -> (ConOfAbs LamBinding -> m b) -> m b Source #

ToConcrete LetBinding Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LetBinding
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LetBinding = [Declaration]

Methods

toConcrete :: MonadToConcrete m => LetBinding -> m (ConOfAbs LetBinding) Source #

bindToConcrete :: MonadToConcrete m => LetBinding -> (ConOfAbs LetBinding -> m b) -> m b Source #

ToConcrete ModuleApplication Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleApplication
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs ModuleApplication = ModuleApplication

Methods

toConcrete :: MonadToConcrete m => ModuleApplication -> m (ConOfAbs ModuleApplication) Source #

bindToConcrete :: MonadToConcrete m => ModuleApplication -> (ConOfAbs ModuleApplication -> m b) -> m b Source #

ToConcrete Pattern Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Pattern
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Pattern = Pattern

Methods

toConcrete :: MonadToConcrete m => Pattern -> m (ConOfAbs Pattern) Source #

bindToConcrete :: MonadToConcrete m => Pattern -> (ConOfAbs Pattern -> m b) -> m b Source #

ToConcrete RHS Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RHS
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs RHS = (RHS, [RewriteEqn], [WithExpr], [Declaration])

Methods

toConcrete :: MonadToConcrete m => RHS -> m (ConOfAbs RHS) Source #

bindToConcrete :: MonadToConcrete m => RHS -> (ConOfAbs RHS -> m b) -> m b Source #

ToConcrete RecordDirectives Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RecordDirectives
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs RecordDirectives = [RecordDirective]

Methods

toConcrete :: MonadToConcrete m => RecordDirectives -> m (ConOfAbs RecordDirectives) Source #

bindToConcrete :: MonadToConcrete m => RecordDirectives -> (ConOfAbs RecordDirectives -> m b) -> m b Source #

ToConcrete SpineLHS Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs SpineLHS
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs SpineLHS = LHS

Methods

toConcrete :: MonadToConcrete m => SpineLHS -> m (ConOfAbs SpineLHS) Source #

bindToConcrete :: MonadToConcrete m => SpineLHS -> (ConOfAbs SpineLHS -> m b) -> m b Source #

ToConcrete TypedBinding Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs TypedBinding
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs TypedBinding = Maybe TypedBinding

Methods

toConcrete :: MonadToConcrete m => TypedBinding -> m (ConOfAbs TypedBinding) Source #

bindToConcrete :: MonadToConcrete m => TypedBinding -> (ConOfAbs TypedBinding -> m b) -> m b Source #

ToConcrete WhereDeclarations Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs WhereDeclarations
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs WhereDeclarations = WhereClause

Methods

toConcrete :: MonadToConcrete m => WhereDeclarations -> m (ConOfAbs WhereDeclarations) Source #

bindToConcrete :: MonadToConcrete m => WhereDeclarations -> (ConOfAbs WhereDeclarations -> m b) -> m b Source #

ToConcrete ModuleName Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleName
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs ModuleName = QName

Methods

toConcrete :: MonadToConcrete m => ModuleName -> m (ConOfAbs ModuleName) Source #

bindToConcrete :: MonadToConcrete m => ModuleName -> (ConOfAbs ModuleName -> m b) -> m b Source #

ToConcrete Name Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Name
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Name = Name

Methods

toConcrete :: MonadToConcrete m => Name -> m (ConOfAbs Name) Source #

bindToConcrete :: MonadToConcrete m => Name -> (ConOfAbs Name -> m b) -> m b Source #

ToConcrete QName Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs QName
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs QName = QName

Methods

toConcrete :: MonadToConcrete m => QName -> m (ConOfAbs QName) Source #

bindToConcrete :: MonadToConcrete m => QName -> (ConOfAbs QName -> m b) -> m b Source #

ToConcrete InteractionId Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs InteractionId
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs InteractionId = Expr

Methods

toConcrete :: MonadToConcrete m => InteractionId -> m (ConOfAbs InteractionId) Source #

bindToConcrete :: MonadToConcrete m => InteractionId -> (ConOfAbs InteractionId -> m b) -> m b Source #

ToConcrete AbstractName Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs AbstractName
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs AbstractName = QName

Methods

toConcrete :: MonadToConcrete m => AbstractName -> m (ConOfAbs AbstractName) Source #

bindToConcrete :: MonadToConcrete m => AbstractName -> (ConOfAbs AbstractName -> m b) -> m b Source #

ToConcrete ResolvedName Source #

Assumes name is not UnknownName.

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ResolvedName
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs ResolvedName = QName

Methods

toConcrete :: MonadToConcrete m => ResolvedName -> m (ConOfAbs ResolvedName) Source #

bindToConcrete :: MonadToConcrete m => ResolvedName -> (ConOfAbs ResolvedName -> m b) -> m b Source #

ToConcrete RangeAndPragma Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RangeAndPragma
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs RangeAndPragma = Pragma

Methods

toConcrete :: MonadToConcrete m => RangeAndPragma -> m (ConOfAbs RangeAndPragma) Source #

bindToConcrete :: MonadToConcrete m => RangeAndPragma -> (ConOfAbs RangeAndPragma -> m b) -> m b Source #

ToConcrete NamedMeta Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs NamedMeta
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs NamedMeta = Expr

Methods

toConcrete :: MonadToConcrete m => NamedMeta -> m (ConOfAbs NamedMeta) Source #

bindToConcrete :: MonadToConcrete m => NamedMeta -> (ConOfAbs NamedMeta -> m b) -> m b Source #

ToConcrete () Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ()
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs () = ()

Methods

toConcrete :: MonadToConcrete m => () -> m (ConOfAbs ()) Source #

bindToConcrete :: MonadToConcrete m => () -> (ConOfAbs () -> m b) -> m b Source #

ToConcrete Bool Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Bool
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Bool = Bool

Methods

toConcrete :: MonadToConcrete m => Bool -> m (ConOfAbs Bool) Source #

bindToConcrete :: MonadToConcrete m => Bool -> (ConOfAbs Bool -> m b) -> m b Source #

ToConcrete Char Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Char
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Char = Char

Methods

toConcrete :: MonadToConcrete m => Char -> m (ConOfAbs Char) Source #

bindToConcrete :: MonadToConcrete m => Char -> (ConOfAbs Char -> m b) -> m b Source #

ToConcrete a => ToConcrete (Binder' a) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Binder' a)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Binder' a) = Binder' (ConOfAbs a)

Methods

toConcrete :: MonadToConcrete m => Binder' a -> m (ConOfAbs (Binder' a)) Source #

bindToConcrete :: MonadToConcrete m => Binder' a -> (ConOfAbs (Binder' a) -> m b) -> m b Source #

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

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Clause' a)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Clause' a) = List1 Declaration

Methods

toConcrete :: MonadToConcrete m => Clause' a -> m (ConOfAbs (Clause' a)) Source #

bindToConcrete :: MonadToConcrete m => Clause' a -> (ConOfAbs (Clause' a) -> m b) -> m b Source #

ToConcrete a => ToConcrete (Arg a) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Arg a)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Arg a) = Arg (ConOfAbs a)

Methods

toConcrete :: MonadToConcrete m => Arg a -> m (ConOfAbs (Arg a)) Source #

bindToConcrete :: MonadToConcrete m => Arg a -> (ConOfAbs (Arg a) -> m b) -> m b Source #

ToConcrete (Constr Constructor) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Constr Constructor)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Constr Constructor) = Declaration

Methods

toConcrete :: MonadToConcrete m => Constr Constructor -> m (ConOfAbs (Constr Constructor)) Source #

bindToConcrete :: MonadToConcrete m => Constr Constructor -> (ConOfAbs (Constr Constructor) -> m b) -> m b Source #

ToConcrete a => ToConcrete (Ranged a) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Ranged a)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Ranged a) = Ranged (ConOfAbs a)

Methods

toConcrete :: MonadToConcrete m => Ranged a -> m (ConOfAbs (Ranged a)) Source #

bindToConcrete :: MonadToConcrete m => Ranged a -> (ConOfAbs (Ranged a) -> m b) -> m b Source #

ToConcrete a => ToConcrete (WithHiding a) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (WithHiding a)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (WithHiding a) = WithHiding (ConOfAbs a)

Methods

toConcrete :: MonadToConcrete m => WithHiding a -> m (ConOfAbs (WithHiding a)) Source #

bindToConcrete :: MonadToConcrete m => WithHiding a -> (ConOfAbs (WithHiding a) -> m b) -> m b Source #

ToConcrete a => ToConcrete (FieldAssignment' a) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (FieldAssignment' a)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (FieldAssignment' a) = FieldAssignment' (ConOfAbs a)

Methods

toConcrete :: MonadToConcrete m => FieldAssignment' a -> m (ConOfAbs (FieldAssignment' a)) Source #

bindToConcrete :: MonadToConcrete m => FieldAssignment' a -> (ConOfAbs (FieldAssignment' a) -> m b) -> m b Source #

ToConcrete a => ToConcrete (TacticAttribute' a) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (TacticAttribute' a)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (TacticAttribute' a) = TacticAttribute' (ConOfAbs a)

Methods

toConcrete :: MonadToConcrete m => TacticAttribute' a -> m (ConOfAbs (TacticAttribute' a)) Source #

bindToConcrete :: MonadToConcrete m => TacticAttribute' a -> (ConOfAbs (TacticAttribute' a) -> m b) -> m b Source #

ToConcrete a => ToConcrete (IPBoundary' a) Source #

Instance details

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (IPBoundary' a)
Instance details Defined in Agda.Interaction.BasicOps type ConOfAbs (IPBoundary' a) = IPBoundary' (ConOfAbs a)

Methods

toConcrete :: MonadToConcrete m => IPBoundary' a -> m (ConOfAbs (IPBoundary' a)) Source #

bindToConcrete :: MonadToConcrete m => IPBoundary' a -> (ConOfAbs (IPBoundary' a) -> m b) -> m b Source #

ToConcrete a => ToConcrete (List1 a) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (List1 a)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (List1 a) = List1 (ConOfAbs a)

Methods

toConcrete :: MonadToConcrete m => List1 a -> m (ConOfAbs (List1 a)) Source #

bindToConcrete :: MonadToConcrete m => List1 a -> (ConOfAbs (List1 a) -> m b) -> m b Source #

ToConcrete a => ToConcrete (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe a)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Maybe a) = Maybe (ConOfAbs a)

Methods

toConcrete :: MonadToConcrete m => Maybe a -> m (ConOfAbs (Maybe a)) Source #

bindToConcrete :: MonadToConcrete m => Maybe a -> (ConOfAbs (Maybe a) -> m b) -> m b Source #

ToConcrete a => ToConcrete [a] Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs [a]
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs [a] = [ConOfAbs a]

Methods

toConcrete :: MonadToConcrete m => [a] -> m (ConOfAbs [a]) Source #

bindToConcrete :: MonadToConcrete m => [a] -> (ConOfAbs [a] -> m b) -> m b Source #

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

Instance details

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputConstraint' a b)
Instance details Defined in Agda.Interaction.BasicOps type ConOfAbs (OutputConstraint' a b) = OutputConstraint' (ConOfAbs a) (ConOfAbs b)

Methods

toConcrete :: MonadToConcrete m => OutputConstraint' a b -> m (ConOfAbs (OutputConstraint' a b)) Source #

bindToConcrete :: MonadToConcrete m => OutputConstraint' a b -> (ConOfAbs (OutputConstraint' a b) -> m b0) -> m b0 Source #

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

Instance details

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputConstraint a b)
Instance details Defined in Agda.Interaction.BasicOps type ConOfAbs (OutputConstraint a b) = OutputConstraint (ConOfAbs a) (ConOfAbs b)

Methods

toConcrete :: MonadToConcrete m => OutputConstraint a b -> m (ConOfAbs (OutputConstraint a b)) Source #

bindToConcrete :: MonadToConcrete m => OutputConstraint a b -> (ConOfAbs (OutputConstraint a b) -> m b0) -> m b0 Source #

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

Instance details

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputForm a b)
Instance details Defined in Agda.Interaction.BasicOps type ConOfAbs (OutputForm a b) = OutputForm (ConOfAbs a) (ConOfAbs b)

Methods

toConcrete :: MonadToConcrete m => OutputForm a b -> m (ConOfAbs (OutputForm a b)) Source #

bindToConcrete :: MonadToConcrete m => OutputForm a b -> (ConOfAbs (OutputForm a b) -> m b0) -> m b0 Source #

ToConcrete a => ToConcrete (Named name a) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Named name a)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Named name a) = Named name (ConOfAbs a)

Methods

toConcrete :: MonadToConcrete m => Named name a -> m (ConOfAbs (Named name a)) Source #

bindToConcrete :: MonadToConcrete m => Named name a -> (ConOfAbs (Named name a) -> m b) -> m b Source #

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

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Either a1 a2)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Either a1 a2) = Either (ConOfAbs a1) (ConOfAbs a2)

Methods

toConcrete :: MonadToConcrete m => Either a1 a2 -> m (ConOfAbs (Either a1 a2)) Source #

bindToConcrete :: MonadToConcrete m => Either a1 a2 -> (ConOfAbs (Either a1 a2) -> m b) -> m b Source #

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

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (a1, a2)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (a1, a2) = (ConOfAbs a1, ConOfAbs a2)

Methods

toConcrete :: MonadToConcrete m => (a1, a2) -> m (ConOfAbs (a1, a2)) Source #

bindToConcrete :: MonadToConcrete m => (a1, a2) -> (ConOfAbs (a1, a2) -> m b) -> m b Source #

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

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (a1, a2, a3)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (a1, a2, a3) = (ConOfAbs a1, ConOfAbs a2, ConOfAbs a3)

Methods

toConcrete :: MonadToConcrete m => (a1, a2, a3) -> m (ConOfAbs (a1, a2, a3)) Source #

bindToConcrete :: MonadToConcrete m => (a1, a2, a3) -> (ConOfAbs (a1, a2, a3) -> m b) -> m b Source #

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

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (RewriteEqn' qn BindName p a)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (RewriteEqn' qn BindName p a) = RewriteEqn' () Name (ConOfAbs p) (ConOfAbs a)

Methods

toConcrete :: MonadToConcrete m => RewriteEqn' qn BindName p a -> m (ConOfAbs (RewriteEqn' qn BindName p a)) Source #

bindToConcrete :: MonadToConcrete m => RewriteEqn' qn BindName p a -> (ConOfAbs (RewriteEqn' qn BindName p a) -> m b) -> m b Source #

toConcreteCtx :: (MonadToConcrete m, ToConcrete a) => Precedence -> a -> m (ConOfAbs a) Source #

Translate something in a context of the given precedence.

type MonadAbsToCon (m :: Type -> Type) = (MonadFresh NameId m, MonadInteractionPoints m, MonadStConcreteNames m, HasOptions m, PureTCM m, IsString (m Doc), Null (m Doc), Semigroup (m Doc)) Source #

Preconditions to run the AbstractToConcrete translation.

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

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

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

abstractToConcreteQName :: MonadAbsToCon m => AllowAmbiguousNames -> QName -> m QName Source #

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

abstractToConcreteTelescope :: MonadAbsToCon m => Telescope -> m [Maybe TypedBinding] Source #

abstractToConcreteUnqualify :: (ToConcrete a, MonadAbsToCon m) => a -> m (ConOfAbs a) Source #

data RangeAndPragma Source #

Constructors

RangeAndPragma Range Pragma

Instances

Instances details

ToConcrete RangeAndPragma Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RangeAndPragma
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs RangeAndPragma = Pragma

Methods

toConcrete :: MonadToConcrete m => RangeAndPragma -> m (ConOfAbs RangeAndPragma) Source #

bindToConcrete :: MonadToConcrete m => RangeAndPragma -> (ConOfAbs RangeAndPragma -> m b) -> m b Source #

type ConOfAbs RangeAndPragma Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs RangeAndPragma = Pragma

noTakenNames :: MonadToConcrete m => m a -> m a Source #