| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Monad.Constraints
Contents
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
- 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
- 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 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 ()
- nowSolvingConstraints :: MonadTCEnv m => m a -> m a
- isSolvingConstraints :: MonadTCEnv m => m Bool
- catchConstraint :: MonadConstraint m => Constraint -> m () -> m ()
- isInstanceConstraint :: Constraint -> 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 #
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
| Show ConstraintStatus Source # | |
Defined in Agda.TypeChecking.Monad.Constraints Methods showsPrec :: Int -> ConstraintStatus -> ShowS show :: ConstraintStatus -> String showList :: [ConstraintStatus] -> ShowS | |
| Eq ConstraintStatus Source # | |
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 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
addConstraint' :: Blocker -> Constraint -> TCM () Source #
Add new a constraint
addAwakeConstraint' :: Blocker -> Constraint -> TCM () Source #
addConstraintTo :: Lens' TCState Constraints -> Blocker -> Constraint -> TCM () Source #
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 #
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 #