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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Conversion.Pure

# Documentation

data FreshThings Source #

Constructors

FreshThings |

Fields

- freshInt :: Int
- freshProblemId :: ProblemId
- freshNameId :: NameId

#### Instances

Instances details

Monad m => MonadState FreshThings (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods get :: PureConversionT m FreshThings Source # put :: FreshThings -> PureConversionT m () Source # state :: (FreshThings -> (a, FreshThings)) -> PureConversionT m a Source #

newtype PureConversionT m a Source #

Constructors

PureConversionT |

Fields

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

#### Instances

Instances details

MonadTrans PureConversionT Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods lift :: Monad m => m a -> PureConversionT m a Source #
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 Source # catchError :: PureConversionT m a -> (TCErr -> PureConversionT m a) -> PureConversionT m a Source #
Monad m => MonadState FreshThings (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods get :: PureConversionT m FreshThings Source # put :: FreshThings -> PureConversionT m () Source # state :: (FreshThings -> (a, FreshThings)) -> PureConversionT m a Source #
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' a TCState -> (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 :: String -> 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' :: 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 #

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 :: [MetaKind] -> 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 #
MonadFail m => MonadFail (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods fail :: String -> PureConversionT m a Source #
Monad m => Applicative (PureConversionT m) Source # |

Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

pure :: a -> PureConversionT m a Source #

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

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

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

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

Functor m => Functor (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods fmap :: (a -> b) -> PureConversionT m a -> PureConversionT m b Source # (<$) :: a -> PureConversionT m b -> PureConversionT m a Source #
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 Source # (>>) :: PureConversionT m a -> PureConversionT m b -> PureConversionT m b Source # return :: a -> PureConversionT m a Source #
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 #
(IsString a, Monad m) => IsString (PureConversionT m a) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods fromString :: String -> PureConversionT m a 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 Source # sconcat :: NonEmpty (PureConversionT m a) -> PureConversionT m a Source # stimes :: Integral b => b -> PureConversionT m a -> PureConversionT m a Source #

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, Show a) => PureConversionT m a -> m (Maybe a) Source #