Agda-2.6.4: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

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

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 (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Ranged a) Source #

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) 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 #