Agda.TypeChecking.Conversion.Pure

Documentation

data FreshThings

Constructors

FreshThings

Fields

• freshInt :: Int
• freshProblemId :: ProblemId
• freshNameId :: NameId

Instances

Monad m => MonadState FreshThings (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

get :: PureConversionT m FreshThings

put :: FreshThings -> PureConversionT m ()

state :: (FreshThings -> (a, FreshThings)) -> PureConversionT m a

newtype PureConversionT m a

Constructors

PureConversionT

Fields

• unPureConversionT :: ExceptT TCErr (StateT FreshThings m) a

Instances

MonadTrans PureConversionT

Defined in Agda.TypeChecking.Conversion.Pure

Methods

lift :: Monad m => m a -> PureConversionT m a

Monad m => MonadFresh NameId (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fresh :: PureConversionT m NameId

Monad m => MonadFresh ProblemId (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fresh :: PureConversionT m ProblemId

Monad m => MonadFresh Int (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fresh :: PureConversionT m Int

Monad m => MonadError TCErr (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

throwError :: TCErr -> PureConversionT m a

catchError :: PureConversionT m a -> (TCErr -> PureConversionT m a) -> PureConversionT m a

Monad m => MonadState FreshThings (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

get :: PureConversionT m FreshThings

put :: FreshThings -> PureConversionT m ()

state :: (FreshThings -> (a, FreshThings)) -> PureConversionT m a

HasOptions m => HasOptions (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

pragmaOptions :: PureConversionT m PragmaOptions

commandLineOptions :: PureConversionT m CommandLineOptions

Monad m => MonadBlock (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

patternViolation :: Blocker -> PureConversionT m a

catchPatternErr :: (Blocker -> PureConversionT m a) -> PureConversionT m a -> PureConversionT m a

MonadReduce m => MonadReduce (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

liftReduce :: ReduceM a -> PureConversionT m a

ReadTCState m => MonadStConcreteNames (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

runStConcreteNames :: StateT ConcreteNames (PureConversionT m) a -> PureConversionT m a

useConcreteNames :: PureConversionT m ConcreteNames

modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> PureConversionT m ()

MonadTCEnv m => MonadTCEnv (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

askTC :: PureConversionT m TCEnv

localTC :: (TCEnv -> TCEnv) -> PureConversionT m a -> PureConversionT m a

ReadTCState m => ReadTCState (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

getTCState :: PureConversionT m TCState

locallyTCState :: Lens' a TCState -> (a -> a) -> PureConversionT m b -> PureConversionT m b

withTCState :: (TCState -> TCState) -> PureConversionT m a -> PureConversionT m a

HasBuiltins m => HasBuiltins (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

getBuiltinThing :: String -> PureConversionT m (Maybe (Builtin PrimFun))

(PureTCM m, MonadBlock m) => MonadConstraint (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

addConstraint :: Blocker -> Constraint -> PureConversionT m ()

addAwakeConstraint :: Blocker -> Constraint -> PureConversionT m ()

solveConstraint :: Constraint -> PureConversionT m ()

solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> PureConversionT m ()

wakeConstraints :: (ProblemConstraint -> WakeUp) -> PureConversionT m ()

stealConstraints :: ProblemId -> PureConversionT m ()

modifyAwakeConstraints :: (Constraints -> Constraints) -> PureConversionT m ()

modifySleepingConstraints :: (Constraints -> Constraints) -> PureConversionT m ()

MonadAddContext m => MonadAddContext (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

addCtx :: Name -> Dom Type -> PureConversionT m a -> PureConversionT m a

addLetBinding' :: Name -> Term -> Dom Type -> PureConversionT m a -> PureConversionT m a

updateContext :: Substitution -> (Context -> Context) -> PureConversionT m a -> PureConversionT m a

withFreshName :: Range -> ArgName -> (Name -> PureConversionT m a) -> PureConversionT m a

MonadDebug m => MonadDebug (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> PureConversionT m String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> PureConversionT m a -> PureConversionT m a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> PureConversionT m a -> PureConversionT m a

getVerbosity :: PureConversionT m Verbosity

isDebugPrinting :: PureConversionT m Bool

nowDebugPrinting :: PureConversionT m a -> PureConversionT m a

(PureTCM m, MonadBlock m) => MonadInteractionPoints (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

freshInteractionId :: PureConversionT m InteractionId

modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> PureConversionT m ()

(PureTCM m, MonadBlock m) => MonadMetaSolver (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> PureConversionT m MetaId

assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> PureConversionT m ()

assignTerm' :: MetaId -> [Arg ArgName] -> Term -> PureConversionT m ()

etaExpandMeta :: [MetaKind] -> MetaId -> PureConversionT m ()

updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> PureConversionT m ()

speculateMetas :: PureConversionT m () -> PureConversionT m KeepMetas -> PureConversionT m ()

(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadReduce m) => PureTCM (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

HasConstInfo m => HasConstInfo (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

getConstInfo :: QName -> PureConversionT m Definition

getConstInfo' :: QName -> PureConversionT m (Either SigError Definition)

getRewriteRulesFor :: QName -> PureConversionT m RewriteRules

ReadTCState m => MonadStatistics (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

modifyCounter :: String -> (Integer -> Integer) -> PureConversionT m ()

(PureTCM m, MonadBlock m) => MonadWarning (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

addWarning :: TCWarning -> PureConversionT m ()

MonadFail m => MonadFail (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fail :: String -> PureConversionT m a

Monad m => Applicative (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

pure :: a -> PureConversionT m a

(<*>) :: PureConversionT m (a -> b) -> PureConversionT m a -> PureConversionT m b

liftA2 :: (a -> b -> c) -> PureConversionT m a -> PureConversionT m b -> PureConversionT m c

(*>) :: PureConversionT m a -> PureConversionT m b -> PureConversionT m b

(<*) :: PureConversionT m a -> PureConversionT m b -> PureConversionT m a

Functor m => Functor (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fmap :: (a -> b) -> PureConversionT m a -> PureConversionT m b

(<$) :: a -> PureConversionT m b -> PureConversionT m a

Monad m => Monad (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

(>>=) :: PureConversionT m a -> (a -> PureConversionT m b) -> PureConversionT m b

(>>) :: PureConversionT m a -> PureConversionT m b -> PureConversionT m b

return :: a -> PureConversionT m a

Monad m => Null (PureConversionT m Doc)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

empty :: PureConversionT m Doc

null :: PureConversionT m Doc -> Bool

(IsString a, Monad m) => IsString (PureConversionT m a)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fromString :: String -> PureConversionT m a

(Monad m, Semigroup a) => Semigroup (PureConversionT m a)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

(<>) :: PureConversionT m a -> PureConversionT m a -> PureConversionT m a

sconcat :: NonEmpty (PureConversionT m a) -> PureConversionT m a

stimes :: Integral b => b -> PureConversionT m a -> PureConversionT m a

pureEqualTerm :: (PureTCM m, MonadBlock m) => Type -> Term -> Term -> m Bool

pureEqualType :: (PureTCM m, MonadBlock m) => Type -> Type -> m Bool

pureCompareAs :: (PureTCM m, MonadBlock m) => Comparison -> CompareAs -> Term -> Term -> m Bool

runPureConversion :: (MonadBlock m, PureTCM m, Show a) => PureConversionT m a -> m (Maybe a)