Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Conversion.Pure

Synopsis

data FreshThings = FreshThings {
- freshInt :: Int
- freshProblemId :: ProblemId
- freshNameId :: NameId
}
newtype PureConversionT (m :: Type -> Type) a = PureConversionT {
- unPureConversionT :: ExceptT TCErr (StateT FreshThings m) a
}
pureEqualTerm :: (PureTCM m, MonadBlock m) => Type -> Term -> Term -> m Bool
pureEqualTermB :: PureTCM m => Type -> Term -> Term -> m (Either Blocker Bool)
pureEqualType :: (PureTCM m, MonadBlock m) => Type -> Type -> m Bool
pureEqualTypeB :: PureTCM m => Type -> Type -> m (Either Blocker Bool)
pureCompareAs :: (PureTCM m, MonadBlock m) => Comparison -> CompareAs -> Term -> Term -> m Bool
runPureConversion :: (MonadBlock m, PureTCM m) => PureConversionT m a -> m (Maybe a)
runPureConversionB :: PureTCM m => PureConversionT m a -> m (Either Blocker (Maybe a))

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 # put :: FreshThings -> PureConversionT m () # state :: (FreshThings -> (a, FreshThings)) -> PureConversionT m a #

newtype PureConversionT (m :: Type -> Type) 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 #
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 => 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 => 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 => 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 => MonadWarning (PureConversionT m) Source #
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods addWarning :: Bool -> 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 #

pureEqualTermB :: PureTCM m => Type -> Term -> Term -> m (Either Blocker Bool) Source #

Return the blocker instead of throwing a patternViolation.

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

pureEqualTypeB :: PureTCM m => Type -> Type -> m (Either Blocker Bool) Source #

Return the blocker instead of throwing a patternViolation.

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

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

runPureConversionB :: PureTCM m => PureConversionT m a -> m (Either Blocker (Maybe a)) Source #