ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Monad.Constraints
Contents
Synopsis
- value solvingProblem
- value solvingProblems
- value isProblemSolved
- value isProblemCompletelySolved
- value isProblemSolved'
- value getConstraintsForProblem
- value getAwakeConstraints
- value dropConstraints
- value takeConstraints
- value putConstraintsToSleep
- value putAllConstraintsToSleep
- data ConstraintStatus
- value holdConstraints
- value takeAwakeConstraint
- value takeAwakeConstraint'
- value getAllConstraints
- value withConstraint
- value buildProblemConstraint
- value buildProblemConstraint_
- value buildConstraint
- class MonadConstraint
- value addConstraint'
- value addAwakeConstraint'
- value addConstraintTo
- value isBlockingConstraint
- value nowSolvingConstraints
- value isSolvingConstraints
- value catchConstraint
- value isInstanceConstraint
- value canDropRecursiveInstance
- value shouldPostponeInstanceSearch
- value wakeConstraints'
- value mapAwakeConstraints
- value mapSleepingConstraints
- PackageAgda-2.8.0.2
- Exports34
- LanguageHaskell2010
- LicenceMIT
- SourceConstraints.hs
Get the awake constraints
Takes out all constraints matching given filter. Danger! The taken constraints need to be solved or put back at some point.
Instances2Eq, Show
Eq ConstraintStatusDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ConstraintsShow ConstraintStatusDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Constraints
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.
class (MonadTCEnv m, ReadTCState m, MonadError TCErr m, MonadBlock m, HasOptions m, MonadDebug m) => MonadConstraint (m :: Type -> Type) whereMonad service class containing methods for adding and solving constraints
Methods
addConstraint :: Blocker -> Constraint -> m ()Unconditionally add the constraint.
addAwakeConstraint :: Blocker -> Constraint -> m ()Add constraint as awake constraint.
solveConstraint :: Constraint -> m ()solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> m ()Solve awake constraints matching the predicate. If the second argument is True solve constraints even if already isSolvingConstraints.
wakeConstraints :: (ProblemConstraint -> WakeUp) -> m ()stealConstraints :: ProblemId -> m ()modifyAwakeConstraints :: (Constraints -> Constraints) -> m ()modifySleepingConstraints :: (Constraints -> Constraints) -> m ()
Instances3MonadConstraint
MonadConstraint TCMDefined in Agda-2.8.0.2 · Agda.TypeChecking.Constraints · orphanPureTCM m => MonadConstraint (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureMonadConstraint m => MonadConstraint (ReaderT e m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Constraints
Add new a constraint
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.
Start solving constraints
Add constraint if the action raises a pattern violation
Wake constraints matching the given predicate (and aren't instance constraints if shouldPostponeInstanceSearch).