Agda-2.6.20240731: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Conversion.Pure

Documentation

data FreshThings Source #

Constructors

FreshThings 

Fields

Instances

Instances details
Monad m => MonadState FreshThings (PureConversionT m) Source # 
Instance details

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 :: Type -> Type) a Source #

Constructors

PureConversionT 

Fields

Instances

Instances details
MonadTrans PureConversionT Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

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

Monad m => MonadFresh NameId (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fresh :: PureConversionT m NameId Source #

Monad m => MonadFresh ProblemId (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fresh :: PureConversionT m ProblemId Source #

Monad m => MonadFresh Int (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fresh :: PureConversionT m Int Source #

Monad m => MonadError TCErr (PureConversionT m) Source # 
Instance details

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

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

Defined in Agda.TypeChecking.Conversion.Pure

Methods

pragmaOptions :: PureConversionT m PragmaOptions Source #

commandLineOptions :: PureConversionT m CommandLineOptions Source #

Monad m => MonadBlock (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

patternViolation :: Blocker -> PureConversionT m a Source #

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

MonadReduce m => MonadReduce (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

liftReduce :: ReduceM a -> PureConversionT m a Source #

ReadTCState m => MonadStConcreteNames (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

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

useConcreteNames :: PureConversionT m ConcreteNames Source #

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

MonadTCEnv m => MonadTCEnv (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

askTC :: PureConversionT m TCEnv Source #

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

ReadTCState m => ReadTCState (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

getTCState :: PureConversionT m TCState Source #

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

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

HasBuiltins m => HasBuiltins (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

getBuiltinThing :: SomeBuiltin -> PureConversionT m (Maybe (Builtin PrimFun)) Source #

(PureTCM m, MonadBlock m) => MonadConstraint (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

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

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

solveConstraint :: Constraint -> PureConversionT m () Source #

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

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

stealConstraints :: ProblemId -> PureConversionT m () Source #

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

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

MonadAddContext m => MonadAddContext (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

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

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

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

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

MonadDebug m => MonadDebug (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

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

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

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

getVerbosity :: PureConversionT m Verbosity Source #

getProfileOptions :: PureConversionT m ProfileOptions Source #

isDebugPrinting :: PureConversionT m Bool Source #

nowDebugPrinting :: PureConversionT m a -> PureConversionT m a Source #

(PureTCM m, MonadBlock m) => MonadInteractionPoints (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

freshInteractionId :: PureConversionT m InteractionId Source #

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

(PureTCM m, MonadBlock m) => MonadMetaSolver (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

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

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

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

etaExpandMeta :: [MetaClass] -> MetaId -> PureConversionT m () Source #

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

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

(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadReduce m) => PureTCM (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

HasConstInfo m => HasConstInfo (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

getConstInfo :: QName -> PureConversionT m Definition Source #

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

getRewriteRulesFor :: QName -> PureConversionT m RewriteRules Source #

ReadTCState m => MonadStatistics (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

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

(PureTCM m, MonadBlock m) => MonadWarning (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

addWarning :: TCWarning -> PureConversionT m () Source #

Monad m => Applicative (PureConversionT m) Source # 
Instance details

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

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

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

MonadFail m => MonadFail (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fail :: String -> PureConversionT m a

Monad m => Null (PureConversionT m Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

empty :: PureConversionT m Doc Source #

null :: PureConversionT m Doc -> Bool Source #

(Monad m, Semigroup a) => Semigroup (PureConversionT m a) Source # 
Instance details

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

(IsString a, Monad m) => IsString (PureConversionT m a) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fromString :: String -> PureConversionT m a

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

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

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

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