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 :: a -> AbsToCon (ConOfAbs a)
- bindToConcrete :: a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
toConcreteCtx :: ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
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 = RangeAndPragma Range 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 :: Type -> Type) = (MonadFresh NameId m, MonadInteractionPoints m, MonadStConcreteNames m, HasOptions m, PureTCM m, IsString (m Doc), Null (m Doc), Semigroup (m Doc))
data AbsToCon a
data Env
noTakenNames :: AbsToCon a -> AbsToCon a
lookupQName :: AllowAmbiguousNames -> QName -> AbsToCon QName

Documentation

class ToConcrete a where Source #

Minimal complete definition

Nothing

Associated Types

type ConOfAbs a Source #

Methods

toConcrete :: a -> AbsToCon (ConOfAbs a) Source #

bindToConcrete :: a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon 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 :: BindName -> AbsToCon (ConOfAbs BindName) Source #

bindToConcrete :: BindName -> (ConOfAbs BindName -> AbsToCon b) -> AbsToCon 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 :: Declaration -> AbsToCon (ConOfAbs Declaration) Source #

bindToConcrete :: Declaration -> (ConOfAbs Declaration -> AbsToCon b) -> AbsToCon 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 :: Expr -> AbsToCon (ConOfAbs Expr) Source #

bindToConcrete :: Expr -> (ConOfAbs Expr -> AbsToCon b) -> AbsToCon 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 :: LHS -> AbsToCon (ConOfAbs LHS) Source #

bindToConcrete :: LHS -> (ConOfAbs LHS -> AbsToCon b) -> AbsToCon 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 :: LHSCore -> AbsToCon (ConOfAbs LHSCore) Source #

bindToConcrete :: LHSCore -> (ConOfAbs LHSCore -> AbsToCon b) -> AbsToCon 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 :: LamBinding -> AbsToCon (ConOfAbs LamBinding) Source #

bindToConcrete :: LamBinding -> (ConOfAbs LamBinding -> AbsToCon b) -> AbsToCon 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 :: LetBinding -> AbsToCon (ConOfAbs LetBinding) Source #

bindToConcrete :: LetBinding -> (ConOfAbs LetBinding -> AbsToCon b) -> AbsToCon 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 :: ModuleApplication -> AbsToCon (ConOfAbs ModuleApplication) Source #

bindToConcrete :: ModuleApplication -> (ConOfAbs ModuleApplication -> AbsToCon b) -> AbsToCon 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 :: Pattern -> AbsToCon (ConOfAbs Pattern) Source #

bindToConcrete :: Pattern -> (ConOfAbs Pattern -> AbsToCon b) -> AbsToCon 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 :: RHS -> AbsToCon (ConOfAbs RHS) Source #

bindToConcrete :: RHS -> (ConOfAbs RHS -> AbsToCon b) -> AbsToCon 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 :: RecordDirectives -> AbsToCon (ConOfAbs RecordDirectives) Source #

bindToConcrete :: RecordDirectives -> (ConOfAbs RecordDirectives -> AbsToCon b) -> AbsToCon 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 :: SpineLHS -> AbsToCon (ConOfAbs SpineLHS) Source #

bindToConcrete :: SpineLHS -> (ConOfAbs SpineLHS -> AbsToCon b) -> AbsToCon 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 :: TypedBinding -> AbsToCon (ConOfAbs TypedBinding) Source #

bindToConcrete :: TypedBinding -> (ConOfAbs TypedBinding -> AbsToCon b) -> AbsToCon 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 :: WhereDeclarations -> AbsToCon (ConOfAbs WhereDeclarations) Source #

bindToConcrete :: WhereDeclarations -> (ConOfAbs WhereDeclarations -> AbsToCon b) -> AbsToCon 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 :: ModuleName -> AbsToCon (ConOfAbs ModuleName) Source #

bindToConcrete :: ModuleName -> (ConOfAbs ModuleName -> AbsToCon b) -> AbsToCon 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 :: Name -> AbsToCon (ConOfAbs Name) Source #

bindToConcrete :: Name -> (ConOfAbs Name -> AbsToCon b) -> AbsToCon 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 :: QName -> AbsToCon (ConOfAbs QName) Source #

bindToConcrete :: QName -> (ConOfAbs QName -> AbsToCon b) -> AbsToCon 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 :: InteractionId -> AbsToCon (ConOfAbs InteractionId) Source #

bindToConcrete :: InteractionId -> (ConOfAbs InteractionId -> AbsToCon b) -> AbsToCon 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 :: AbstractName -> AbsToCon (ConOfAbs AbstractName) Source #

bindToConcrete :: AbstractName -> (ConOfAbs AbstractName -> AbsToCon b) -> AbsToCon 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 :: ResolvedName -> AbsToCon (ConOfAbs ResolvedName) Source #

bindToConcrete :: ResolvedName -> (ConOfAbs ResolvedName -> AbsToCon b) -> AbsToCon 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 :: RangeAndPragma -> AbsToCon (ConOfAbs RangeAndPragma) Source #

bindToConcrete :: RangeAndPragma -> (ConOfAbs RangeAndPragma -> AbsToCon b) -> AbsToCon 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 :: NamedMeta -> AbsToCon (ConOfAbs NamedMeta) Source #

bindToConcrete :: NamedMeta -> (ConOfAbs NamedMeta -> AbsToCon b) -> AbsToCon 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 :: () -> AbsToCon (ConOfAbs ()) Source #

bindToConcrete :: () -> (ConOfAbs () -> AbsToCon b) -> AbsToCon 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 :: Bool -> AbsToCon (ConOfAbs Bool) Source #

bindToConcrete :: Bool -> (ConOfAbs Bool -> AbsToCon b) -> AbsToCon 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 :: Char -> AbsToCon (ConOfAbs Char) Source #

bindToConcrete :: Char -> (ConOfAbs Char -> AbsToCon b) -> AbsToCon 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 :: Binder' a -> AbsToCon (ConOfAbs (Binder' a)) Source #

bindToConcrete :: Binder' a -> (ConOfAbs (Binder' a) -> AbsToCon b) -> AbsToCon 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 :: Clause' a -> AbsToCon (ConOfAbs (Clause' a)) Source #

bindToConcrete :: Clause' a -> (ConOfAbs (Clause' a) -> AbsToCon b) -> AbsToCon 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 :: Arg a -> AbsToCon (ConOfAbs (Arg a)) Source #

bindToConcrete :: Arg a -> (ConOfAbs (Arg a) -> AbsToCon b) -> AbsToCon 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 :: Constr Constructor -> AbsToCon (ConOfAbs (Constr Constructor)) Source #

bindToConcrete :: Constr Constructor -> (ConOfAbs (Constr Constructor) -> AbsToCon b) -> AbsToCon 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 :: Ranged a -> AbsToCon (ConOfAbs (Ranged a)) Source #

bindToConcrete :: Ranged a -> (ConOfAbs (Ranged a) -> AbsToCon b) -> AbsToCon 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 :: WithHiding a -> AbsToCon (ConOfAbs (WithHiding a)) Source #

bindToConcrete :: WithHiding a -> (ConOfAbs (WithHiding a) -> AbsToCon b) -> AbsToCon 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 :: FieldAssignment' a -> AbsToCon (ConOfAbs (FieldAssignment' a)) Source #

bindToConcrete :: FieldAssignment' a -> (ConOfAbs (FieldAssignment' a) -> AbsToCon b) -> AbsToCon 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 :: TacticAttribute' a -> AbsToCon (ConOfAbs (TacticAttribute' a)) Source #

bindToConcrete :: TacticAttribute' a -> (ConOfAbs (TacticAttribute' a) -> AbsToCon b) -> AbsToCon 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 :: IPBoundary' a -> AbsToCon (ConOfAbs (IPBoundary' a)) Source #

bindToConcrete :: IPBoundary' a -> (ConOfAbs (IPBoundary' a) -> AbsToCon b) -> AbsToCon 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 :: List1 a -> AbsToCon (ConOfAbs (List1 a)) Source #

bindToConcrete :: List1 a -> (ConOfAbs (List1 a) -> AbsToCon b) -> AbsToCon 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 :: Maybe a -> AbsToCon (ConOfAbs (Maybe a)) Source #

bindToConcrete :: Maybe a -> (ConOfAbs (Maybe a) -> AbsToCon b) -> AbsToCon 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 :: [a] -> AbsToCon (ConOfAbs [a]) Source #

bindToConcrete :: [a] -> (ConOfAbs [a] -> AbsToCon b) -> AbsToCon 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 :: OutputConstraint' a b -> AbsToCon (ConOfAbs (OutputConstraint' a b)) Source #

bindToConcrete :: OutputConstraint' a b -> (ConOfAbs (OutputConstraint' a b) -> AbsToCon b0) -> AbsToCon 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 :: OutputConstraint a b -> AbsToCon (ConOfAbs (OutputConstraint a b)) Source #

bindToConcrete :: OutputConstraint a b -> (ConOfAbs (OutputConstraint a b) -> AbsToCon b0) -> AbsToCon 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 :: OutputForm a b -> AbsToCon (ConOfAbs (OutputForm a b)) Source #

bindToConcrete :: OutputForm a b -> (ConOfAbs (OutputForm a b) -> AbsToCon b0) -> AbsToCon 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 :: Named name a -> AbsToCon (ConOfAbs (Named name a)) Source #

bindToConcrete :: Named name a -> (ConOfAbs (Named name a) -> AbsToCon b) -> AbsToCon 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 :: Either a1 a2 -> AbsToCon (ConOfAbs (Either a1 a2)) Source #

bindToConcrete :: Either a1 a2 -> (ConOfAbs (Either a1 a2) -> AbsToCon b) -> AbsToCon 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 :: (a1, a2) -> AbsToCon (ConOfAbs (a1, a2)) Source #

bindToConcrete :: (a1, a2) -> (ConOfAbs (a1, a2) -> AbsToCon b) -> AbsToCon 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 :: (a1, a2, a3) -> AbsToCon (ConOfAbs (a1, a2, a3)) Source #

bindToConcrete :: (a1, a2, a3) -> (ConOfAbs (a1, a2, a3) -> AbsToCon b) -> AbsToCon 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 :: RewriteEqn' qn BindName p a -> AbsToCon (ConOfAbs (RewriteEqn' qn BindName p a)) Source #

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

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

Translate something in a context of the given precedence.

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

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

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

runAbsToCon :: MonadAbsToCon m => AbsToCon c -> m c 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 :: RangeAndPragma -> AbsToCon (ConOfAbs RangeAndPragma) Source #

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

type ConOfAbs RangeAndPragma Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs RangeAndPragma = Pragma

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

withScope :: ScopeInfo -> AbsToCon a -> AbsToCon a Source #

preserveInteractionIds :: AbsToCon a -> AbsToCon a Source #

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 #

The function runAbsToCon can target any monad that satisfies the constraints of MonadAbsToCon.

data AbsToCon a Source #

Instances

Instances details

HasOptions AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods pragmaOptions :: AbsToCon PragmaOptions Source # commandLineOptions :: AbsToCon CommandLineOptions Source #
MonadReduce AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods liftReduce :: ReduceM a -> AbsToCon a Source #
MonadStConcreteNames AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods runStConcreteNames :: StateT ConcreteNames AbsToCon a -> AbsToCon a Source # useConcreteNames :: AbsToCon ConcreteNames Source # modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> AbsToCon () Source #
MonadTCEnv AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods askTC :: AbsToCon TCEnv Source # localTC :: (TCEnv -> TCEnv) -> AbsToCon a -> AbsToCon a Source #
ReadTCState AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods getTCState :: AbsToCon TCState Source # locallyTCState :: Lens' TCState a -> (a -> a) -> AbsToCon b -> AbsToCon b Source # withTCState :: (TCState -> TCState) -> AbsToCon a -> AbsToCon a Source #
HasBuiltins AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods getBuiltinThing :: SomeBuiltin -> AbsToCon (Maybe (Builtin PrimFun)) Source #
MonadAddContext AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods addCtx :: Name -> Dom Type -> AbsToCon a -> AbsToCon a Source # addLetBinding' :: Origin -> Name -> Term -> Dom Type -> AbsToCon a -> AbsToCon a Source # updateContext :: Substitution -> (Context -> Context) -> AbsToCon a -> AbsToCon a Source # withFreshName :: Range -> ArgName -> (Name -> AbsToCon a) -> AbsToCon a Source #
MonadDebug AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> AbsToCon String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> AbsToCon a -> AbsToCon a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> AbsToCon a -> AbsToCon a Source # getVerbosity :: AbsToCon Verbosity Source # getProfileOptions :: AbsToCon ProfileOptions Source # isDebugPrinting :: AbsToCon Bool Source # nowDebugPrinting :: AbsToCon a -> AbsToCon a Source #
MonadInteractionPoints AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods freshInteractionId :: AbsToCon InteractionId Source # modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> AbsToCon () Source #
PureTCM AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete
HasConstInfo AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods getConstInfo :: QName -> AbsToCon Definition Source # getConstInfo' :: QName -> AbsToCon (Either SigError Definition) Source # getRewriteRulesFor :: QName -> AbsToCon RewriteRules Source #
Applicative AbsToCon Source #
Instance details 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
Functor AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods fmap :: (a -> b) -> AbsToCon a -> AbsToCon b (<$) :: a -> AbsToCon b -> AbsToCon a #
Monad AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods (>>=) :: AbsToCon a -> (a -> AbsToCon b) -> AbsToCon b (>>) :: AbsToCon a -> AbsToCon b -> AbsToCon b return :: a -> AbsToCon a
MonadFail AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods fail :: String -> AbsToCon a
MonadFresh NameId AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods fresh :: AbsToCon NameId Source #
MonadReader Env AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods ask :: AbsToCon Env local :: (Env -> Env) -> AbsToCon a -> AbsToCon a reader :: (Env -> a) -> AbsToCon a
Null (AbsToCon Doc) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods empty :: AbsToCon Doc Source # null :: AbsToCon Doc -> Bool Source #
Semigroup (AbsToCon Doc) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods (<>) :: AbsToCon Doc -> AbsToCon Doc -> AbsToCon Doc # sconcat :: NonEmpty (AbsToCon Doc) -> AbsToCon Doc stimes :: Integral b => b -> AbsToCon Doc -> AbsToCon Doc
IsString (AbsToCon Doc) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods fromString :: String -> AbsToCon Doc

data Env Source #

Instances

Instances details

MonadReader Env AbsToCon Source #
Instance details 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 Source #

lookupQName :: AllowAmbiguousNames -> QName -> AbsToCon QName Source #