Safe Haskell	Safe-Inferred
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 = (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 Source # 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 Source # 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 Source # 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 Source # 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 Source # 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 Source # 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 Source # 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 Source # 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 Source # 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 Source # Methods toConcrete :: RHS -> AbsToCon (ConOfAbs RHS) Source # bindToConcrete :: RHS -> (ConOfAbs RHS -> AbsToCon b) -> AbsToCon b Source #
ToConcrete SpineLHS Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs SpineLHS Source # 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 Source # 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 Source # 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 Source # 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 Source # 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 Source # 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 Source # 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 Source # 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 Source # 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 Source # 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 Source # 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 () Source # 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 Source # Methods toConcrete :: Bool -> AbsToCon (ConOfAbs Bool) Source # bindToConcrete :: Bool -> (ConOfAbs Bool -> 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) Source # 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) Source # 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) Source # 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) Source # Methods toConcrete :: Constr Constructor -> AbsToCon (ConOfAbs (Constr Constructor)) Source # bindToConcrete :: Constr Constructor -> (ConOfAbs (Constr Constructor) -> 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) Source # 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) Source # Methods toConcrete :: FieldAssignment' a -> AbsToCon (ConOfAbs (FieldAssignment' a)) Source # bindToConcrete :: FieldAssignment' a -> (ConOfAbs (FieldAssignment' 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) Source # 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) Source # Methods toConcrete :: List1 a -> AbsToCon (ConOfAbs (List1 a)) Source # bindToConcrete :: List1 a -> (ConOfAbs (List1 a) -> AbsToCon b) -> AbsToCon b Source #
ToConcrete (Maybe BindName) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Maybe BindName) Source # Methods toConcrete :: Maybe BindName -> AbsToCon (ConOfAbs (Maybe BindName)) Source # bindToConcrete :: Maybe BindName -> (ConOfAbs (Maybe BindName) -> AbsToCon b) -> AbsToCon b Source #
ToConcrete (Maybe Pattern) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Maybe Pattern) Source # Methods toConcrete :: Maybe Pattern -> AbsToCon (ConOfAbs (Maybe Pattern)) Source # bindToConcrete :: Maybe Pattern -> (ConOfAbs (Maybe Pattern) -> AbsToCon b) -> AbsToCon b Source #
ToConcrete (Maybe QName) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Maybe QName) Source # Methods toConcrete :: Maybe QName -> AbsToCon (ConOfAbs (Maybe QName)) Source # bindToConcrete :: Maybe QName -> (ConOfAbs (Maybe QName) -> AbsToCon b) -> AbsToCon b Source #
ToConcrete a => ToConcrete [a] Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs [a] Source # 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) Source # 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) Source # 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) Source # 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) Source # 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) Source # 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) Source # 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) Source # 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) Source # 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 Source # 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 = (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 #
MonadFail AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods fail :: String -> AbsToCon a #
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 #
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 #
IsString (AbsToCon Doc) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods fromString :: String -> AbsToCon Doc #
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 #

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 #