ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Constraints

24 values

PackageAgda-2.7.0.1
Exports24
LanguageHaskell2010
LicenceMIT
SourceConstraints.hs

valueaddConstraintTCM :: Blocker -> Constraint -> TCM ()

valuewakeConstraintsTCM :: (ProblemConstraint -> WakeUp) -> TCM ()

valuestealConstraintsTCM :: ProblemId -> TCM ()

Add all constraints belonging to the given problem to the current problem(s).

valuenoConstraints

:: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
=> m a
-> m a

Don't allow the argument to produce any blocking constraints.

WARNING: this does not mean that the given computation cannot constrain the solution space further. It can well do so, by solving metas.

valuereallyNoConstraints

:: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
=> m a
-> m a

As noConstraints but also fail for non-blocking constraints.

valuenoConstraints'

:: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
=> Bool
-> m a
-> m a

valuenonConstraining

:: (HasOptions m, MonadConstraint m, MonadDebug m, MonadError TCErr m, MonadFresh ProblemId m, MonadTCEnv m, MonadWarning m)
=> m a
-> m a

Run a computation that should succeeds without constraining the solution space, i.e., not add any information about meta-variables.

valuenewProblem

:: (MonadFresh ProblemId m, MonadConstraint m)
=> m a
-> m (ProblemId, a)

Create a fresh problem for the given action.

valuenewProblem_

:: (MonadFresh ProblemId m, MonadConstraint m)
=> m a
-> m ProblemId

valueifNoConstraints

:: TCM a
-> a -> TCM b
-> ProblemId -> a -> TCM b
-> TCM b

valueifNoConstraints_ :: TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a

valueguardConstraint :: Constraint -> TCM () -> TCM ()

guardConstraint c blocker tries to solve blocker first. If successful without constraints, it moves on to solve c, otherwise it adds a c to the constraint pool, blocked by the problem generated by blocker.

valuewhenConstraints :: TCM () -> TCM () -> TCM ()

valuewakeupConstraints :: MonadMetaSolver m => MetaId -> m ()

Wake up the constraints depending on the given meta.

valuewakeupConstraints_ :: TCM ()

Wake up all constraints not blocked on a problem.

valuesolveSomeAwakeConstraintsTCM

:: ProblemConstraint -> Bool
-> Bool
-> TCM ()

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

valuesolveConstraintTCM :: Constraint -> TCM ()

valuesolveConstraint_ :: Constraint -> TCM ()

valuecheckTypeCheckingProblem :: TypeCheckingProblem -> TCM Term

valuedebugConstraints :: TCM ()

valueupdateBlocker :: PureTCM m => Blocker -> m Blocker

valueaddAndUnblocker :: (PureTCM m, MonadBlock m) => Blocker -> m a -> m a

valueaddOrUnblocker :: (PureTCM m, MonadBlock m) => Blocker -> m a -> m a

valuewithReduced

:: (Reduce a, IsMeta a, PureTCM m, MonadBlock m)
=> a
-> a -> m b
-> m b

Orphan instances

1 instance

MonadConstraint TCM