module Agda.TypeChecking.Monad.Constraints where

import Control.Arrow ((&&&))
import Control.Monad.Except
import Control.Monad.Reader

import qualified Data.Foldable as Fold
import qualified Data.List as List
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Semigroup ((<>))

import Agda.Interaction.Options.Base
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Closure
import Agda.TypeChecking.Monad.Debug

import Agda.Utils.Lens
import Agda.Utils.Monad

solvingProblem :: MonadConstraint m => ProblemId -> m a -> m a
solvingProblem :: forall (m :: * -> *) a.
MonadConstraint m =>
ProblemId -> m a -> m a
solvingProblem ProblemId
pid = Set ProblemId -> m a -> m a
forall (m :: * -> *) a.
MonadConstraint m =>
Set ProblemId -> m a -> m a
solvingProblems (ProblemId -> Set ProblemId
forall a. a -> Set a
Set.singleton ProblemId
pid)

solvingProblems :: MonadConstraint m => Set ProblemId -> m a -> m a
solvingProblems :: forall (m :: * -> *) a.
MonadConstraint m =>
Set ProblemId -> m a -> m a
solvingProblems Set ProblemId
pids m a
m = [Char] -> VerboseLevel -> [Char] -> m a -> m a
forall a. [Char] -> VerboseLevel -> [Char] -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.constr.solve" VerboseLevel
50 ([Char]
"working on problems " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [ProblemId] -> [Char]
forall a. Show a => a -> [Char]
show (Set ProblemId -> [ProblemId]
forall a. Set a -> [a]
Set.toList Set ProblemId
pids)) (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ do
  a
x <- (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
e -> TCEnv
e { envActiveProblems = pids `Set.union` envActiveProblems e }) m a
m
  Set ProblemId -> (ProblemId -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
Fold.forM_ Set ProblemId
pids ((ProblemId -> m ()) -> m ()) -> (ProblemId -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ ProblemId
pid -> do
    m Bool -> m () -> m () -> m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (ProblemId -> m Bool
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
ProblemId -> m Bool
isProblemSolved ProblemId
pid)
        ([Char] -> VerboseLevel -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"tc.constr.solve" VerboseLevel
50 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"problem " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ProblemId -> [Char]
forall a. Show a => a -> [Char]
show ProblemId
pid [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" was not solved.")
      (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ {- else -} do
        [Char] -> VerboseLevel -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"tc.constr.solve" VerboseLevel
50 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"problem " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ProblemId -> [Char]
forall a. Show a => a -> [Char]
show ProblemId
pid [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" was solved!"
        (ProblemConstraint -> WakeUp) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> WakeUp) -> m ()
wakeConstraints (ProblemId -> Blocker -> WakeUp
wakeIfBlockedOnProblem ProblemId
pid (Blocker -> WakeUp)
-> (ProblemConstraint -> Blocker) -> ProblemConstraint -> WakeUp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Blocker
constraintUnblocker)
  a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x

isProblemSolved :: (MonadTCEnv m, ReadTCState m) => ProblemId -> m Bool
isProblemSolved :: forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
ProblemId -> m Bool
isProblemSolved = Bool -> ProblemId -> m Bool
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
Bool -> ProblemId -> m Bool
isProblemSolved' Bool
False

isProblemCompletelySolved :: (MonadTCEnv m, ReadTCState m) => ProblemId -> m Bool
isProblemCompletelySolved :: forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
ProblemId -> m Bool
isProblemCompletelySolved = Bool -> ProblemId -> m Bool
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
Bool -> ProblemId -> m Bool
isProblemSolved' Bool
True

isProblemSolved' :: (MonadTCEnv m, ReadTCState m) => Bool -> ProblemId -> m Bool
isProblemSolved' :: forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
Bool -> ProblemId -> m Bool
isProblemSolved' Bool
completely ProblemId
pid =
  m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
and2M (Bool -> Bool
not (Bool -> Bool) -> (Set ProblemId -> Bool) -> Set ProblemId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemId -> Set ProblemId -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member ProblemId
pid (Set ProblemId -> Bool) -> m (Set ProblemId) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Set ProblemId) -> m (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Set ProblemId
envActiveProblems)
        (Bool -> Bool
not (Bool -> Bool)
-> ([ProblemConstraint] -> Bool) -> [ProblemConstraint] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProblemConstraint -> Bool) -> [ProblemConstraint] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ProblemConstraint -> Bool
belongsToUs ([ProblemConstraint] -> Bool) -> m [ProblemConstraint] -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [ProblemConstraint]
forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
getAllConstraints)
  where
    belongsToUs :: ProblemConstraint -> Bool
belongsToUs ProblemConstraint
c
      | ProblemId -> Set ProblemId -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember ProblemId
pid (ProblemConstraint -> Set ProblemId
constraintProblems ProblemConstraint
c)         = Bool
False
      | Constraint -> Bool
isBlockingConstraint (Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (Closure Constraint -> Constraint)
-> Closure Constraint -> Constraint
forall a b. (a -> b) -> a -> b
$ ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c) = Bool
True
      | Bool
otherwise                                        = Bool
completely -- Ignore non-blocking unless `completely`

{-# SPECIALIZE getConstraintsForProblem :: ProblemId -> TCM Constraints #-}
getConstraintsForProblem :: ReadTCState m => ProblemId -> m Constraints
getConstraintsForProblem :: forall (m :: * -> *).
ReadTCState m =>
ProblemId -> m [ProblemConstraint]
getConstraintsForProblem ProblemId
pid = (ProblemConstraint -> Bool)
-> [ProblemConstraint] -> [ProblemConstraint]
forall a. (a -> Bool) -> [a] -> [a]
List.filter (ProblemId -> Set ProblemId -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member ProblemId
pid (Set ProblemId -> Bool)
-> (ProblemConstraint -> Set ProblemId)
-> ProblemConstraint
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Set ProblemId
constraintProblems) ([ProblemConstraint] -> [ProblemConstraint])
-> m [ProblemConstraint] -> m [ProblemConstraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [ProblemConstraint]
forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
getAllConstraints

-- | Get the awake constraints
getAwakeConstraints :: ReadTCState m => m Constraints
getAwakeConstraints :: forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
getAwakeConstraints = Lens' TCState [ProblemConstraint] -> m [ProblemConstraint]
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR ([ProblemConstraint] -> f [ProblemConstraint])
-> TCState -> f TCState
Lens' TCState [ProblemConstraint]
stAwakeConstraints

-- danger...
dropConstraints :: MonadConstraint m => (ProblemConstraint -> Bool) -> m ()
dropConstraints :: forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> m ()
dropConstraints ProblemConstraint -> Bool
crit = do
  let filt :: [ProblemConstraint] -> [ProblemConstraint]
filt = (ProblemConstraint -> Bool)
-> [ProblemConstraint] -> [ProblemConstraint]
forall a. (a -> Bool) -> [a] -> [a]
List.filter ((ProblemConstraint -> Bool)
 -> [ProblemConstraint] -> [ProblemConstraint])
-> (ProblemConstraint -> Bool)
-> [ProblemConstraint]
-> [ProblemConstraint]
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool)
-> (ProblemConstraint -> Bool) -> ProblemConstraint -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Bool
crit
  ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifySleepingConstraints [ProblemConstraint] -> [ProblemConstraint]
filt
  ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifyAwakeConstraints    [ProblemConstraint] -> [ProblemConstraint]
filt

-- | Takes out all constraints matching given filter.
--   Danger!  The taken constraints need to be solved or put back at some point.
takeConstraints :: MonadConstraint m => (ProblemConstraint -> Bool) -> m Constraints
takeConstraints :: forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> m [ProblemConstraint]
takeConstraints ProblemConstraint -> Bool
f = do
  ([ProblemConstraint]
takeAwake , [ProblemConstraint]
keepAwake ) <- (ProblemConstraint -> Bool)
-> [ProblemConstraint]
-> ([ProblemConstraint], [ProblemConstraint])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition ProblemConstraint -> Bool
f ([ProblemConstraint] -> ([ProblemConstraint], [ProblemConstraint]))
-> m [ProblemConstraint]
-> m ([ProblemConstraint], [ProblemConstraint])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState [ProblemConstraint] -> m [ProblemConstraint]
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC ([ProblemConstraint] -> f [ProblemConstraint])
-> TCState -> f TCState
Lens' TCState [ProblemConstraint]
stAwakeConstraints
  ([ProblemConstraint]
takeAsleep, [ProblemConstraint]
keepAsleep) <- (ProblemConstraint -> Bool)
-> [ProblemConstraint]
-> ([ProblemConstraint], [ProblemConstraint])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition ProblemConstraint -> Bool
f ([ProblemConstraint] -> ([ProblemConstraint], [ProblemConstraint]))
-> m [ProblemConstraint]
-> m ([ProblemConstraint], [ProblemConstraint])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState [ProblemConstraint] -> m [ProblemConstraint]
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC ([ProblemConstraint] -> f [ProblemConstraint])
-> TCState -> f TCState
Lens' TCState [ProblemConstraint]
stSleepingConstraints
  ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifyAwakeConstraints    (([ProblemConstraint] -> [ProblemConstraint]) -> m ())
-> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall a b. (a -> b) -> a -> b
$ [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
forall a b. a -> b -> a
const [ProblemConstraint]
keepAwake
  ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifySleepingConstraints (([ProblemConstraint] -> [ProblemConstraint]) -> m ())
-> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall a b. (a -> b) -> a -> b
$ [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
forall a b. a -> b -> a
const [ProblemConstraint]
keepAsleep
  [ProblemConstraint] -> m [ProblemConstraint]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([ProblemConstraint] -> m [ProblemConstraint])
-> [ProblemConstraint] -> m [ProblemConstraint]
forall a b. (a -> b) -> a -> b
$ [ProblemConstraint]
takeAwake [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
forall a. [a] -> [a] -> [a]
++ [ProblemConstraint]
takeAsleep

putConstraintsToSleep :: MonadConstraint m => (ProblemConstraint -> Bool) -> m ()
putConstraintsToSleep :: forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> m ()
putConstraintsToSleep ProblemConstraint -> Bool
sleepy = do
  [ProblemConstraint]
awakeOnes <- Lens' TCState [ProblemConstraint] -> m [ProblemConstraint]
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR ([ProblemConstraint] -> f [ProblemConstraint])
-> TCState -> f TCState
Lens' TCState [ProblemConstraint]
stAwakeConstraints
  let ([ProblemConstraint]
gotoSleep, [ProblemConstraint]
stayAwake) = (ProblemConstraint -> Bool)
-> [ProblemConstraint]
-> ([ProblemConstraint], [ProblemConstraint])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition ProblemConstraint -> Bool
sleepy [ProblemConstraint]
awakeOnes
  ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifySleepingConstraints (([ProblemConstraint] -> [ProblemConstraint]) -> m ())
-> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall a b. (a -> b) -> a -> b
$ ([ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
forall a. [a] -> [a] -> [a]
++ [ProblemConstraint]
gotoSleep)
  ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifyAwakeConstraints    (([ProblemConstraint] -> [ProblemConstraint]) -> m ())
-> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall a b. (a -> b) -> a -> b
$ [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
forall a b. a -> b -> a
const [ProblemConstraint]
stayAwake

putAllConstraintsToSleep :: MonadConstraint m => m ()
putAllConstraintsToSleep :: forall (m :: * -> *). MonadConstraint m => m ()
putAllConstraintsToSleep = (ProblemConstraint -> Bool) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> m ()
putConstraintsToSleep (Bool -> ProblemConstraint -> Bool
forall a b. a -> b -> a
const Bool
True)

data ConstraintStatus = AwakeConstraint | SleepingConstraint
  deriving (ConstraintStatus -> ConstraintStatus -> Bool
(ConstraintStatus -> ConstraintStatus -> Bool)
-> (ConstraintStatus -> ConstraintStatus -> Bool)
-> Eq ConstraintStatus
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ConstraintStatus -> ConstraintStatus -> Bool
== :: ConstraintStatus -> ConstraintStatus -> Bool
$c/= :: ConstraintStatus -> ConstraintStatus -> Bool
/= :: ConstraintStatus -> ConstraintStatus -> Bool
Eq, VerboseLevel -> ConstraintStatus -> [Char] -> [Char]
[ConstraintStatus] -> [Char] -> [Char]
ConstraintStatus -> [Char]
(VerboseLevel -> ConstraintStatus -> [Char] -> [Char])
-> (ConstraintStatus -> [Char])
-> ([ConstraintStatus] -> [Char] -> [Char])
-> Show ConstraintStatus
forall a.
(VerboseLevel -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: VerboseLevel -> ConstraintStatus -> [Char] -> [Char]
showsPrec :: VerboseLevel -> ConstraintStatus -> [Char] -> [Char]
$cshow :: ConstraintStatus -> [Char]
show :: ConstraintStatus -> [Char]
$cshowList :: [ConstraintStatus] -> [Char] -> [Char]
showList :: [ConstraintStatus] -> [Char] -> [Char]
Show)

-- | 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.
holdConstraints :: (ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a
holdConstraints :: forall a.
(ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a
holdConstraints ConstraintStatus -> ProblemConstraint -> Bool
p TCM a
m = do
  ([ProblemConstraint]
holdAwake, [ProblemConstraint]
stillAwake)   <- (ProblemConstraint -> Bool)
-> [ProblemConstraint]
-> ([ProblemConstraint], [ProblemConstraint])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (ConstraintStatus -> ProblemConstraint -> Bool
p ConstraintStatus
AwakeConstraint)    ([ProblemConstraint] -> ([ProblemConstraint], [ProblemConstraint]))
-> TCMT IO [ProblemConstraint]
-> TCMT IO ([ProblemConstraint], [ProblemConstraint])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState [ProblemConstraint] -> TCMT IO [ProblemConstraint]
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC ([ProblemConstraint] -> f [ProblemConstraint])
-> TCState -> f TCState
Lens' TCState [ProblemConstraint]
stAwakeConstraints
  ([ProblemConstraint]
holdAsleep, [ProblemConstraint]
stillAsleep) <- (ProblemConstraint -> Bool)
-> [ProblemConstraint]
-> ([ProblemConstraint], [ProblemConstraint])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (ConstraintStatus -> ProblemConstraint -> Bool
p ConstraintStatus
SleepingConstraint) ([ProblemConstraint] -> ([ProblemConstraint], [ProblemConstraint]))
-> TCMT IO [ProblemConstraint]
-> TCMT IO ([ProblemConstraint], [ProblemConstraint])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState [ProblemConstraint] -> TCMT IO [ProblemConstraint]
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC ([ProblemConstraint] -> f [ProblemConstraint])
-> TCState -> f TCState
Lens' TCState [ProblemConstraint]
stSleepingConstraints
  ([ProblemConstraint] -> f [ProblemConstraint])
-> TCState -> f TCState
Lens' TCState [ProblemConstraint]
stAwakeConstraints    Lens' TCState [ProblemConstraint]
-> [ProblemConstraint] -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` [ProblemConstraint]
stillAwake
  ([ProblemConstraint] -> f [ProblemConstraint])
-> TCState -> f TCState
Lens' TCState [ProblemConstraint]
stSleepingConstraints Lens' TCState [ProblemConstraint]
-> [ProblemConstraint] -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` [ProblemConstraint]
stillAsleep
  let restore :: TCMT IO ()
restore = do
        ([ProblemConstraint] -> f [ProblemConstraint])
-> TCState -> f TCState
Lens' TCState [ProblemConstraint]
stAwakeConstraints    Lens' TCState [ProblemConstraint]
-> ([ProblemConstraint] -> [ProblemConstraint]) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` ([ProblemConstraint]
holdAwake [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
forall a. [a] -> [a] -> [a]
++)
        ([ProblemConstraint] -> f [ProblemConstraint])
-> TCState -> f TCState
Lens' TCState [ProblemConstraint]
stSleepingConstraints Lens' TCState [ProblemConstraint]
-> ([ProblemConstraint] -> [ProblemConstraint]) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` ([ProblemConstraint]
holdAsleep [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
forall a. [a] -> [a] -> [a]
++)
  TCM a -> (TCErr -> TCM a) -> TCM a
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (TCM a
m TCM a -> TCMT IO () -> TCM a
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* TCMT IO ()
restore) (\ TCErr
err -> TCMT IO ()
restore TCMT IO () -> TCM a -> TCM a
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> TCErr -> TCM a
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err)

takeAwakeConstraint :: MonadConstraint m => m (Maybe ProblemConstraint)
takeAwakeConstraint :: forall (m :: * -> *).
MonadConstraint m =>
m (Maybe ProblemConstraint)
takeAwakeConstraint = (ProblemConstraint -> Bool) -> m (Maybe ProblemConstraint)
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> m (Maybe ProblemConstraint)
takeAwakeConstraint' (Bool -> ProblemConstraint -> Bool
forall a b. a -> b -> a
const Bool
True)

takeAwakeConstraint'
  :: MonadConstraint m
  => (ProblemConstraint -> Bool) -> m (Maybe ProblemConstraint)
takeAwakeConstraint' :: forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> m (Maybe ProblemConstraint)
takeAwakeConstraint' ProblemConstraint -> Bool
p = do
  [ProblemConstraint]
cs <- m [ProblemConstraint]
forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
getAwakeConstraints
  case (ProblemConstraint -> Bool)
-> [ProblemConstraint]
-> ([ProblemConstraint], [ProblemConstraint])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break ProblemConstraint -> Bool
p [ProblemConstraint]
cs of
    ([ProblemConstraint]
_, [])       -> Maybe ProblemConstraint -> m (Maybe ProblemConstraint)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ProblemConstraint
forall a. Maybe a
Nothing
    ([ProblemConstraint]
cs0, ProblemConstraint
c : [ProblemConstraint]
cs) -> do
      ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifyAwakeConstraints (([ProblemConstraint] -> [ProblemConstraint]) -> m ())
-> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall a b. (a -> b) -> a -> b
$ [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
forall a b. a -> b -> a
const ([ProblemConstraint]
cs0 [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
forall a. [a] -> [a] -> [a]
++ [ProblemConstraint]
cs)
      Maybe ProblemConstraint -> m (Maybe ProblemConstraint)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ProblemConstraint -> m (Maybe ProblemConstraint))
-> Maybe ProblemConstraint -> m (Maybe ProblemConstraint)
forall a b. (a -> b) -> a -> b
$ ProblemConstraint -> Maybe ProblemConstraint
forall a. a -> Maybe a
Just ProblemConstraint
c

getAllConstraints :: ReadTCState m => m Constraints
getAllConstraints :: forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
getAllConstraints = do
  TCState
s <- m TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  [ProblemConstraint] -> m [ProblemConstraint]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([ProblemConstraint] -> m [ProblemConstraint])
-> [ProblemConstraint] -> m [ProblemConstraint]
forall a b. (a -> b) -> a -> b
$ TCState
s TCState -> Lens' TCState [ProblemConstraint] -> [ProblemConstraint]
forall o i. o -> Lens' o i -> i
^. ([ProblemConstraint] -> f [ProblemConstraint])
-> TCState -> f TCState
Lens' TCState [ProblemConstraint]
stAwakeConstraints [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
forall a. [a] -> [a] -> [a]
++ TCState
s TCState -> Lens' TCState [ProblemConstraint] -> [ProblemConstraint]
forall o i. o -> Lens' o i -> i
^. ([ProblemConstraint] -> f [ProblemConstraint])
-> TCState -> f TCState
Lens' TCState [ProblemConstraint]
stSleepingConstraints

withConstraint :: MonadConstraint m => (Constraint -> m a) -> ProblemConstraint -> m a
withConstraint :: forall (m :: * -> *) a.
MonadConstraint m =>
(Constraint -> m a) -> ProblemConstraint -> m a
withConstraint Constraint -> m a
f (PConstr Set ProblemId
pids Blocker
_ Closure Constraint
c) = do
  -- We should preserve the problem stack and the isSolvingConstraint flag
  (Set ProblemId
pids', Bool
isSolving) <- (TCEnv -> (Set ProblemId, Bool)) -> m (Set ProblemId, Bool)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC ((TCEnv -> (Set ProblemId, Bool)) -> m (Set ProblemId, Bool))
-> (TCEnv -> (Set ProblemId, Bool)) -> m (Set ProblemId, Bool)
forall a b. (a -> b) -> a -> b
$ TCEnv -> Set ProblemId
envActiveProblems (TCEnv -> Set ProblemId)
-> (TCEnv -> Bool) -> TCEnv -> (Set ProblemId, Bool)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& TCEnv -> Bool
envSolvingConstraints
  Closure Constraint -> (Constraint -> m a) -> m a
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure Constraint
c ((Constraint -> m a) -> m a) -> (Constraint -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \Constraint
c ->
    (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
e -> TCEnv
e { envActiveProblems = pids', envSolvingConstraints = isSolving }) (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$
    Set ProblemId -> m a -> m a
forall (m :: * -> *) a.
MonadConstraint m =>
Set ProblemId -> m a -> m a
solvingProblems Set ProblemId
pids (Constraint -> m a
f Constraint
c)

buildProblemConstraint
  :: (MonadTCEnv m, ReadTCState m)
  => Set ProblemId -> Blocker -> Constraint -> m ProblemConstraint
buildProblemConstraint :: forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
Set ProblemId -> Blocker -> Constraint -> m ProblemConstraint
buildProblemConstraint Set ProblemId
pids Blocker
unblock Constraint
c = Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
PConstr Set ProblemId
pids Blocker
unblock (Closure Constraint -> ProblemConstraint)
-> m (Closure Constraint) -> m ProblemConstraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Constraint -> m (Closure Constraint)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Constraint
c

buildProblemConstraint_
  :: (MonadTCEnv m, ReadTCState m)
  => Blocker -> Constraint -> m ProblemConstraint
buildProblemConstraint_ :: forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
Blocker -> Constraint -> m ProblemConstraint
buildProblemConstraint_ = Set ProblemId -> Blocker -> Constraint -> m ProblemConstraint
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
Set ProblemId -> Blocker -> Constraint -> m ProblemConstraint
buildProblemConstraint Set ProblemId
forall a. Set a
Set.empty

buildConstraint :: Blocker -> Constraint -> TCM ProblemConstraint
buildConstraint :: Blocker -> Constraint -> TCM ProblemConstraint
buildConstraint Blocker
unblock Constraint
c = do
  Set ProblemId
pids <- (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Set ProblemId
envActiveProblems
  Set ProblemId -> Blocker -> Constraint -> TCM ProblemConstraint
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
Set ProblemId -> Blocker -> Constraint -> m ProblemConstraint
buildProblemConstraint Set ProblemId
pids Blocker
unblock Constraint
c

-- | Monad service class containing methods for adding and solving
--   constraints
class ( MonadTCEnv m
      , ReadTCState m
      , MonadError TCErr m
      , MonadBlock m
      , HasOptions m
      , MonadDebug m
      ) => MonadConstraint m where
  -- | Unconditionally add the constraint.
  addConstraint :: Blocker -> Constraint -> m ()

  -- | Add constraint as awake constraint.
  addAwakeConstraint :: Blocker -> Constraint -> m ()

  solveConstraint :: Constraint -> m ()

  -- | Solve awake constraints matching the predicate. If the second argument is
  --   True solve constraints even if already 'isSolvingConstraints'.
  solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> m ()

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

  stealConstraints :: ProblemId -> m ()

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

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

instance MonadConstraint m => MonadConstraint (ReaderT e m) where
  addConstraint :: Blocker -> Constraint -> ReaderT e m ()
addConstraint             = (m () -> ReaderT e m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT e m ())
-> (Constraint -> m ()) -> Constraint -> ReaderT e m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Constraint -> m ()) -> Constraint -> ReaderT e m ())
-> (Blocker -> Constraint -> m ())
-> Blocker
-> Constraint
-> ReaderT e m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> Constraint -> m ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint
  addAwakeConstraint :: Blocker -> Constraint -> ReaderT e m ()
addAwakeConstraint        = (m () -> ReaderT e m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT e m ())
-> (Constraint -> m ()) -> Constraint -> ReaderT e m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Constraint -> m ()) -> Constraint -> ReaderT e m ())
-> (Blocker -> Constraint -> m ())
-> Blocker
-> Constraint
-> ReaderT e m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> Constraint -> m ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addAwakeConstraint
  solveConstraint :: Constraint -> ReaderT e m ()
solveConstraint           = m () -> ReaderT e m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT e m ())
-> (Constraint -> m ()) -> Constraint -> ReaderT e m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> m ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
solveConstraint
  solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> ReaderT e m ()
solveSomeAwakeConstraints = (m () -> ReaderT e m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT e m ())
-> (Bool -> m ()) -> Bool -> ReaderT e m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Bool -> m ()) -> Bool -> ReaderT e m ())
-> ((ProblemConstraint -> Bool) -> Bool -> m ())
-> (ProblemConstraint -> Bool)
-> Bool
-> ReaderT e m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProblemConstraint -> Bool) -> Bool -> m ()
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> Bool -> m ()
solveSomeAwakeConstraints
  stealConstraints :: ProblemId -> ReaderT e m ()
stealConstraints          = m () -> ReaderT e m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT e m ())
-> (ProblemId -> m ()) -> ProblemId -> ReaderT e m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemId -> m ()
forall (m :: * -> *). MonadConstraint m => ProblemId -> m ()
stealConstraints
  modifyAwakeConstraints :: ([ProblemConstraint] -> [ProblemConstraint]) -> ReaderT e m ()
modifyAwakeConstraints    = m () -> ReaderT e m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT e m ())
-> (([ProblemConstraint] -> [ProblemConstraint]) -> m ())
-> ([ProblemConstraint] -> [ProblemConstraint])
-> ReaderT e m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifyAwakeConstraints
  modifySleepingConstraints :: ([ProblemConstraint] -> [ProblemConstraint]) -> ReaderT e m ()
modifySleepingConstraints = m () -> ReaderT e m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT e m ())
-> (([ProblemConstraint] -> [ProblemConstraint]) -> m ())
-> ([ProblemConstraint] -> [ProblemConstraint])
-> ReaderT e m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifySleepingConstraints
  wakeConstraints :: (ProblemConstraint -> WakeUp) -> ReaderT e m ()
wakeConstraints = m () -> ReaderT e m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT e m ())
-> ((ProblemConstraint -> WakeUp) -> m ())
-> (ProblemConstraint -> WakeUp)
-> ReaderT e m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProblemConstraint -> WakeUp) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> WakeUp) -> m ()
wakeConstraints

-- | Add new a constraint
addConstraint' :: Blocker -> Constraint -> TCM ()
addConstraint' :: Blocker -> Constraint -> TCMT IO ()
addConstraint' = Lens' TCState [ProblemConstraint]
-> Blocker -> Constraint -> TCMT IO ()
addConstraintTo ([ProblemConstraint] -> f [ProblemConstraint])
-> TCState -> f TCState
Lens' TCState [ProblemConstraint]
stSleepingConstraints

addAwakeConstraint' :: Blocker -> Constraint -> TCM ()
addAwakeConstraint' :: Blocker -> Constraint -> TCMT IO ()
addAwakeConstraint' = Lens' TCState [ProblemConstraint]
-> Blocker -> Constraint -> TCMT IO ()
addConstraintTo ([ProblemConstraint] -> f [ProblemConstraint])
-> TCState -> f TCState
Lens' TCState [ProblemConstraint]
stAwakeConstraints

addConstraintTo :: Lens' TCState Constraints -> Blocker -> Constraint -> TCM ()
addConstraintTo :: Lens' TCState [ProblemConstraint]
-> Blocker -> Constraint -> TCMT IO ()
addConstraintTo Lens' TCState [ProblemConstraint]
bucket Blocker
unblock Constraint
c = do
    ProblemConstraint
pc <- Blocker -> Constraint -> TCM ProblemConstraint
buildConstraint Blocker
unblock Constraint
c
    (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
stDirty Lens' TCState Bool -> Bool -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` Bool
True
    ([ProblemConstraint] -> f [ProblemConstraint])
-> TCState -> f TCState
Lens' TCState [ProblemConstraint]
bucket Lens' TCState [ProblemConstraint]
-> ([ProblemConstraint] -> [ProblemConstraint]) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` (ProblemConstraint
pc ProblemConstraint -> [ProblemConstraint] -> [ProblemConstraint]
forall a. a -> [a] -> [a]
:)

-- | 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.
isBlockingConstraint :: Constraint -> Bool
isBlockingConstraint :: Constraint -> Bool
isBlockingConstraint = \case
  SortCmp{}             -> Bool
False
  LevelCmp{}            -> Bool
False
  FindInstance{}        -> Bool
False
  ResolveInstanceHead{} -> Bool
False
  HasBiggerSort{}       -> Bool
False
  HasPTSRule{}          -> Bool
False
  CheckDataSort{}       -> Bool
False
  ValueCmp{}            -> Bool
True
  ValueCmpOnFace{}      -> Bool
True
  ElimCmp{}             -> Bool
True
  UnBlock{}             -> Bool
True
  IsEmpty{}             -> Bool
True
  CheckSizeLtSat{}      -> Bool
True
  CheckFunDef{}         -> Bool
True
  UnquoteTactic{}       -> Bool
True
  CheckMetaInst{}       -> Bool
True
  CheckType{}           -> Bool
True
  CheckLockedVars{}     -> Bool
True
  UsableAtModality{}    -> Bool
True

-- | Start solving constraints
nowSolvingConstraints :: MonadTCEnv m => m a -> m a
nowSolvingConstraints :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
nowSolvingConstraints = (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envSolvingConstraints = True }

isSolvingConstraints :: MonadTCEnv m => m Bool
isSolvingConstraints :: forall (m :: * -> *). MonadTCEnv m => m Bool
isSolvingConstraints = (TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envSolvingConstraints

-- | Add constraint if the action raises a pattern violation
catchConstraint :: MonadConstraint m => Constraint -> m () -> m ()
catchConstraint :: forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint Constraint
c = (Blocker -> m ()) -> m () -> m ()
forall a. (Blocker -> m a) -> m a -> m a
forall (m :: * -> *) a.
MonadBlock m =>
(Blocker -> m a) -> m a -> m a
catchPatternErr ((Blocker -> m ()) -> m () -> m ())
-> (Blocker -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ \ Blocker
unblock -> Blocker -> Constraint -> m ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
unblock Constraint
c

isInstanceConstraint :: Constraint -> Bool
isInstanceConstraint :: Constraint -> Bool
isInstanceConstraint FindInstance{} = Bool
True
isInstanceConstraint Constraint
_              = Bool
False

canDropRecursiveInstance :: (ReadTCState m, HasOptions m) => m Bool
canDropRecursiveInstance :: forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
canDropRecursiveInstance =
  m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
and2M ((TCState -> Lens' TCState Bool -> Bool
forall o i. o -> Lens' o i -> i
^. (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
stConsideringInstance) (TCState -> Bool) -> m TCState -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState)
        (Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optBacktrackingInstances (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)

shouldPostponeInstanceSearch :: (ReadTCState m, HasOptions m) => m Bool
shouldPostponeInstanceSearch :: forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
shouldPostponeInstanceSearch = m Bool
forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
canDropRecursiveInstance m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` ((TCState -> Lens' TCState Bool -> Bool
forall o i. o -> Lens' o i -> i
^. (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
stPostponeInstanceSearch) (TCState -> Bool) -> m TCState -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState)

-- | Wake constraints matching the given predicate (and aren't instance
--   constraints if 'shouldPostponeInstanceSearch').
wakeConstraints' :: MonadConstraint m => (ProblemConstraint -> WakeUp) -> m ()
wakeConstraints' :: forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> WakeUp) -> m ()
wakeConstraints' ProblemConstraint -> WakeUp
p = do
  Bool
skipInstance <- m Bool
forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
shouldPostponeInstanceSearch
  let skip :: ProblemConstraint -> Bool
skip ProblemConstraint
c = Bool
skipInstance Bool -> Bool -> Bool
&& Constraint -> Bool
isInstanceConstraint (Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (Closure Constraint -> Constraint)
-> Closure Constraint -> Constraint
forall a b. (a -> b) -> a -> b
$ ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c)
  (ProblemConstraint -> WakeUp) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> WakeUp) -> m ()
wakeConstraints ((ProblemConstraint -> WakeUp) -> m ())
-> (ProblemConstraint -> WakeUp) -> m ()
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint -> Bool)
-> (ProblemConstraint -> WakeUp) -> ProblemConstraint -> WakeUp
forall constr.
(constr -> Bool) -> (constr -> WakeUp) -> constr -> WakeUp
wakeUpWhen (Bool -> Bool
not (Bool -> Bool)
-> (ProblemConstraint -> Bool) -> ProblemConstraint -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Bool
skip) ProblemConstraint -> WakeUp
p

---------------------------------------------------------------------------
-- * Lenses
---------------------------------------------------------------------------

mapAwakeConstraints :: (Constraints -> Constraints) -> TCState -> TCState
mapAwakeConstraints :: ([ProblemConstraint] -> [ProblemConstraint]) -> TCState -> TCState
mapAwakeConstraints = Lens' TCState [ProblemConstraint]
-> ([ProblemConstraint] -> [ProblemConstraint])
-> TCState
-> TCState
forall o i. Lens' o i -> LensMap o i
over ([ProblemConstraint] -> f [ProblemConstraint])
-> TCState -> f TCState
Lens' TCState [ProblemConstraint]
stAwakeConstraints

mapSleepingConstraints :: (Constraints -> Constraints) -> TCState -> TCState
mapSleepingConstraints :: ([ProblemConstraint] -> [ProblemConstraint]) -> TCState -> TCState
mapSleepingConstraints = Lens' TCState [ProblemConstraint]
-> ([ProblemConstraint] -> [ProblemConstraint])
-> TCState
-> TCState
forall o i. Lens' o i -> LensMap o i
over ([ProblemConstraint] -> f [ProblemConstraint])
-> TCState -> f TCState
Lens' TCState [ProblemConstraint]
stSleepingConstraints