Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Monad.Constraints

Contents

Lenses

Synopsis

solvingProblem :: MonadConstraint m => ProblemId -> m a -> m a
solvingProblems :: MonadConstraint m => Set ProblemId -> m a -> m a
isProblemSolved :: (MonadTCEnv m, ReadTCState m) => ProblemId -> m Bool
isProblemCompletelySolved :: (MonadTCEnv m, ReadTCState m) => ProblemId -> m Bool
isProblemSolved' :: (MonadTCEnv m, ReadTCState m) => Bool -> ProblemId -> m Bool
getConstraintsForProblem :: ReadTCState m => ProblemId -> m Constraints
getAwakeConstraints :: ReadTCState m => m Constraints
dropConstraints :: MonadConstraint m => (ProblemConstraint -> Bool) -> m ()
takeConstraints :: MonadConstraint m => (ProblemConstraint -> Bool) -> m Constraints
putConstraintsToSleep :: MonadConstraint m => (ProblemConstraint -> Bool) -> m ()
putAllConstraintsToSleep :: MonadConstraint m => m ()
data ConstraintStatus
- = AwakeConstraint
- | SleepingConstraint
holdConstraints :: (ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a
takeAwakeConstraint :: MonadConstraint m => m (Maybe ProblemConstraint)
takeAwakeConstraint' :: MonadConstraint m => (ProblemConstraint -> Bool) -> m (Maybe ProblemConstraint)
getAllConstraints :: ReadTCState m => m Constraints
withConstraint :: MonadConstraint m => (Constraint -> m a) -> ProblemConstraint -> m a
buildProblemConstraint :: (MonadTCEnv m, ReadTCState m) => Set ProblemId -> Blocker -> Constraint -> m ProblemConstraint
buildProblemConstraint_ :: (MonadTCEnv m, ReadTCState m) => Blocker -> Constraint -> m ProblemConstraint
buildConstraint :: Blocker -> Constraint -> TCM ProblemConstraint
class (MonadTCEnv m, ReadTCState m, MonadError TCErr m, MonadBlock m, HasOptions m, MonadDebug m) => MonadConstraint (m :: Type -> Type) where
- addConstraint :: Blocker -> Constraint -> m ()
- addAwakeConstraint :: Blocker -> Constraint -> m ()
- solveConstraint :: Constraint -> m ()
- solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> m ()
- wakeConstraints :: (ProblemConstraint -> WakeUp) -> m ()
- stealConstraints :: ProblemId -> m ()
- modifyAwakeConstraints :: (Constraints -> Constraints) -> m ()
- modifySleepingConstraints :: (Constraints -> Constraints) -> m ()
addConstraint' :: Blocker -> Constraint -> TCM ()
addAwakeConstraint' :: Blocker -> Constraint -> TCM ()
addConstraintTo :: Lens' TCState Constraints -> Blocker -> Constraint -> TCM ()
isBlockingConstraint :: Constraint -> Bool
nowSolvingConstraints :: MonadTCEnv m => m a -> m a
isSolvingConstraints :: MonadTCEnv m => m Bool
catchConstraint :: MonadConstraint m => Constraint -> m () -> m ()
isInstanceConstraint :: Constraint -> Bool
canDropRecursiveInstance :: (ReadTCState m, HasOptions m) => m Bool
shouldPostponeInstanceSearch :: (ReadTCState m, HasOptions m) => m Bool
wakeConstraints' :: MonadConstraint m => (ProblemConstraint -> WakeUp) -> m ()
mapAwakeConstraints :: (Constraints -> Constraints) -> TCState -> TCState
mapSleepingConstraints :: (Constraints -> Constraints) -> TCState -> TCState

Documentation

solvingProblem :: MonadConstraint m => ProblemId -> m a -> m a Source #

solvingProblems :: MonadConstraint m => Set ProblemId -> m a -> m a Source #

isProblemSolved :: (MonadTCEnv m, ReadTCState m) => ProblemId -> m Bool Source #

isProblemCompletelySolved :: (MonadTCEnv m, ReadTCState m) => ProblemId -> m Bool Source #

isProblemSolved' :: (MonadTCEnv m, ReadTCState m) => Bool -> ProblemId -> m Bool Source #

getConstraintsForProblem :: ReadTCState m => ProblemId -> m Constraints Source #

getAwakeConstraints :: ReadTCState m => m Constraints Source #

Get the awake constraints

dropConstraints :: MonadConstraint m => (ProblemConstraint -> Bool) -> m () Source #

takeConstraints :: MonadConstraint m => (ProblemConstraint -> Bool) -> m Constraints Source #

Takes out all constraints matching given filter. Danger! The taken constraints need to be solved or put back at some point.

putConstraintsToSleep :: MonadConstraint m => (ProblemConstraint -> Bool) -> m () Source #

putAllConstraintsToSleep :: MonadConstraint m => m () Source #

data ConstraintStatus Source #

Constructors

AwakeConstraint
SleepingConstraint

Instances

Instances details

Show ConstraintStatus Source #
Instance details Defined in Agda.TypeChecking.Monad.Constraints Methods showsPrec :: Int -> ConstraintStatus -> ShowS show :: ConstraintStatus -> String showList :: [ConstraintStatus] -> ShowS
Eq ConstraintStatus Source #
Instance details Defined in Agda.TypeChecking.Monad.Constraints Methods (==) :: ConstraintStatus -> ConstraintStatus -> Bool (/=) :: ConstraintStatus -> ConstraintStatus -> Bool

holdConstraints :: (ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a Source #

Suspend constraints matching the predicate during the execution of the second argument. Caution: held sleeping constraints will not be woken up by events that would normally trigger a wakeup call.

takeAwakeConstraint :: MonadConstraint m => m (Maybe ProblemConstraint) Source #

takeAwakeConstraint' :: MonadConstraint m => (ProblemConstraint -> Bool) -> m (Maybe ProblemConstraint) Source #

getAllConstraints :: ReadTCState m => m Constraints Source #

withConstraint :: MonadConstraint m => (Constraint -> m a) -> ProblemConstraint -> m a Source #

buildProblemConstraint :: (MonadTCEnv m, ReadTCState m) => Set ProblemId -> Blocker -> Constraint -> m ProblemConstraint Source #

buildProblemConstraint_ :: (MonadTCEnv m, ReadTCState m) => Blocker -> Constraint -> m ProblemConstraint Source #

buildConstraint :: Blocker -> Constraint -> TCM ProblemConstraint Source #

class (MonadTCEnv m, ReadTCState m, MonadError TCErr m, MonadBlock m, HasOptions m, MonadDebug m) => MonadConstraint (m :: Type -> Type) where Source #

Monad service class containing methods for adding and solving constraints

Methods

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

Unconditionally add the constraint.

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

Add constraint as awake constraint.

solveConstraint :: Constraint -> m () Source #

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

Solve awake constraints matching the predicate. If the second argument is True solve constraints even if already isSolvingConstraints.

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

stealConstraints :: ProblemId -> m () Source #

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

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

Instances

Instances details

MonadConstraint TCM Source #
Instance details Defined in Agda.TypeChecking.Constraints Methods addConstraint :: Blocker -> Constraint -> TCM () Source # addAwakeConstraint :: Blocker -> Constraint -> TCM () Source # solveConstraint :: Constraint -> TCM () Source # solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> TCM () Source # wakeConstraints :: (ProblemConstraint -> WakeUp) -> TCM () Source # stealConstraints :: ProblemId -> TCM () Source # modifyAwakeConstraints :: (Constraints -> Constraints) -> TCM () Source # modifySleepingConstraints :: (Constraints -> Constraints) -> TCM () 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 #
MonadConstraint m => MonadConstraint (ReaderT e m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Constraints Methods addConstraint :: Blocker -> Constraint -> ReaderT e m () Source # addAwakeConstraint :: Blocker -> Constraint -> ReaderT e m () Source # solveConstraint :: Constraint -> ReaderT e m () Source # solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> ReaderT e m () Source # wakeConstraints :: (ProblemConstraint -> WakeUp) -> ReaderT e m () Source # stealConstraints :: ProblemId -> ReaderT e m () Source # modifyAwakeConstraints :: (Constraints -> Constraints) -> ReaderT e m () Source # modifySleepingConstraints :: (Constraints -> Constraints) -> ReaderT e m () Source #

addConstraint' :: Blocker -> Constraint -> TCM () Source #

Add new a constraint

addAwakeConstraint' :: Blocker -> Constraint -> TCM () Source #

addConstraintTo :: Lens' TCState Constraints -> Blocker -> Constraint -> TCM () Source #

isBlockingConstraint :: Constraint -> Bool Source #

A problem is considered solved if there are no unsolved blocking constraints belonging to it. There's no really good principle for what constraints are blocking and which are not, but the general idea is that nothing bad should happen if you assume a non-blocking constraint is solvable, but it turns out it isn't. For instance, assuming an equality constraint between two types that turns out to be false can lead to ill typed terms in places where we don't expect them.

nowSolvingConstraints :: MonadTCEnv m => m a -> m a Source #

Start solving constraints

isSolvingConstraints :: MonadTCEnv m => m Bool Source #

catchConstraint :: MonadConstraint m => Constraint -> m () -> m () Source #

Add constraint if the action raises a pattern violation

isInstanceConstraint :: Constraint -> Bool Source #

canDropRecursiveInstance :: (ReadTCState m, HasOptions m) => m Bool Source #

shouldPostponeInstanceSearch :: (ReadTCState m, HasOptions m) => m Bool Source #

wakeConstraints' :: MonadConstraint m => (ProblemConstraint -> WakeUp) -> m () Source #

Wake constraints matching the given predicate (and aren't instance constraints if shouldPostponeInstanceSearch).

Lenses

mapAwakeConstraints :: (Constraints -> Constraints) -> TCState -> TCState Source #

mapSleepingConstraints :: (Constraints -> Constraints) -> TCState -> TCState Source #