Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

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 = (MonadTCEnv m, ReadTCState m, MonadStConcreteNames m, HasOptions m, HasBuiltins m, MonadDebug m)
- 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 = (MonadTCEnv m, ReadTCState m, MonadStConcreteNames m, HasOptions m, HasBuiltins m, MonadDebug m) Source #

We need: - Read access to the AbsToCon environment - Read access to the TC environment - Read access to the TC state - Read and write access to the stConcreteNames part of the TC state - Read access to the options - Permission to print debug messages

data AbsToCon a Source #

#### Instances

Instances details

HasOptions AbsToCon Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods pragmaOptions :: AbsToCon PragmaOptions Source # commandLineOptions :: AbsToCon CommandLineOptions 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' a TCState -> (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 :: String -> AbsToCon (Maybe (Builtin PrimFun)) 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 #

isDebugPrinting :: AbsToCon Bool Source #

nowDebugPrinting :: AbsToCon a -> AbsToCon a Source #

MonadFail AbsToCon Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods fail :: String -> AbsToCon a Source #
Applicative AbsToCon Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods pure :: a -> AbsToCon a Source # (<*>) :: AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b Source # liftA2 :: (a -> b -> c) -> AbsToCon a -> AbsToCon b -> AbsToCon c Source # (*>) :: AbsToCon a -> AbsToCon b -> AbsToCon b Source # (<*) :: AbsToCon a -> AbsToCon b -> AbsToCon a Source #
Functor AbsToCon Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods fmap :: (a -> b) -> AbsToCon a -> AbsToCon b Source # (<$) :: a -> AbsToCon b -> AbsToCon a Source #
Monad AbsToCon Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods (>>=) :: AbsToCon a -> (a -> AbsToCon b) -> AbsToCon b Source # (>>) :: AbsToCon a -> AbsToCon b -> AbsToCon b Source # return :: a -> AbsToCon a Source #
MonadReader Env AbsToCon Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods ask :: AbsToCon Env Source # local :: (Env -> Env) -> AbsToCon a -> AbsToCon a Source # reader :: (Env -> a) -> AbsToCon a Source #

data Env Source #

#### Instances

Instances details

MonadReader Env AbsToCon Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods ask :: AbsToCon Env Source # local :: (Env -> Env) -> AbsToCon a -> AbsToCon a Source # reader :: (Env -> a) -> AbsToCon a Source #

noTakenNames :: AbsToCon a -> AbsToCon a Source #

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