Agda-2.8.0: 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 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 #