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

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

-- | Get the awake constraints
getAwakeConstraints :: ReadTCState m => m Constraints
getAwakeConstraints :: forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
getAwakeConstraints = forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' [ProblemConstraint] TCState
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 = forall a. (a -> Bool) -> [a] -> [a]
List.filter forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Bool
crit
  forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifySleepingConstraints [ProblemConstraint] -> [ProblemConstraint]
filt
  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 ) <- forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition ProblemConstraint -> Bool
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [ProblemConstraint] TCState
stAwakeConstraints
  ([ProblemConstraint]
takeAsleep, [ProblemConstraint]
keepAsleep) <- forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition ProblemConstraint -> Bool
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [ProblemConstraint] TCState
stSleepingConstraints
  forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifyAwakeConstraints    forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const [ProblemConstraint]
keepAwake
  forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifySleepingConstraints forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const [ProblemConstraint]
keepAsleep
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [ProblemConstraint]
takeAwake 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 <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' [ProblemConstraint] TCState
stAwakeConstraints
  let ([ProblemConstraint]
gotoSleep, [ProblemConstraint]
stayAwake) = forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition ProblemConstraint -> Bool
sleepy [ProblemConstraint]
awakeOnes
  forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifySleepingConstraints forall a b. (a -> b) -> a -> b
$ (forall a. [a] -> [a] -> [a]
++ [ProblemConstraint]
gotoSleep)
  forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifyAwakeConstraints    forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const [ProblemConstraint]
stayAwake

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

data ConstraintStatus = AwakeConstraint | SleepingConstraint
  deriving (ConstraintStatus -> ConstraintStatus -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConstraintStatus -> ConstraintStatus -> Bool
$c/= :: ConstraintStatus -> ConstraintStatus -> Bool
== :: ConstraintStatus -> ConstraintStatus -> Bool
$c== :: ConstraintStatus -> ConstraintStatus -> Bool
Eq, VerboseLevel -> ConstraintStatus -> ShowS
[ConstraintStatus] -> ShowS
ConstraintStatus -> [Char]
forall a.
(VerboseLevel -> a -> ShowS)
-> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ConstraintStatus] -> ShowS
$cshowList :: [ConstraintStatus] -> ShowS
show :: ConstraintStatus -> [Char]
$cshow :: ConstraintStatus -> [Char]
showsPrec :: VerboseLevel -> ConstraintStatus -> ShowS
$cshowsPrec :: VerboseLevel -> ConstraintStatus -> ShowS
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)   <- forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (ConstraintStatus -> ProblemConstraint -> Bool
p ConstraintStatus
AwakeConstraint)    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [ProblemConstraint] TCState
stAwakeConstraints
  ([ProblemConstraint]
holdAsleep, [ProblemConstraint]
stillAsleep) <- forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (ConstraintStatus -> ProblemConstraint -> Bool
p ConstraintStatus
SleepingConstraint) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [ProblemConstraint] TCState
stSleepingConstraints
  Lens' [ProblemConstraint] TCState
stAwakeConstraints    forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` [ProblemConstraint]
stillAwake
  Lens' [ProblemConstraint] TCState
stSleepingConstraints forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` [ProblemConstraint]
stillAsleep
  let restore :: TCMT IO ()
restore = do
        Lens' [ProblemConstraint] TCState
stAwakeConstraints    forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` ([ProblemConstraint]
holdAwake forall a. [a] -> [a] -> [a]
++)
        Lens' [ProblemConstraint] TCState
stSleepingConstraints forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` ([ProblemConstraint]
holdAsleep forall a. [a] -> [a] -> [a]
++)
  forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (TCM a
m forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* TCMT IO ()
restore) (\ TCErr
err -> TCMT IO ()
restore forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> 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 = forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> m (Maybe ProblemConstraint)
takeAwakeConstraint' (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 <- forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
getAwakeConstraints
  case forall a. (a -> Bool) -> [a] -> ([a], [a])
break ProblemConstraint -> Bool
p [ProblemConstraint]
cs of
    ([ProblemConstraint]
_, [])       -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    ([ProblemConstraint]
cs0, ProblemConstraint
c : [ProblemConstraint]
cs) -> do
      forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifyAwakeConstraints forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const ([ProblemConstraint]
cs0 forall a. [a] -> [a] -> [a]
++ [ProblemConstraint]
cs)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ProblemConstraint
c

getAllConstraints :: ReadTCState m => m Constraints
getAllConstraints :: forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
getAllConstraints = do
  TCState
s <- forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ TCState
sforall o i. o -> Lens' i o -> i
^.Lens' [ProblemConstraint] TCState
stAwakeConstraints forall a. [a] -> [a] -> [a]
++ TCState
sforall o i. o -> Lens' i o -> i
^.Lens' [ProblemConstraint] TCState
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) <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a b. (a -> b) -> a -> b
$ TCEnv -> Set ProblemId
envActiveProblems forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& TCEnv -> Bool
envSolvingConstraints
  forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Constraint
c forall a b. (a -> b) -> a -> b
$ \Constraint
c ->
    forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
e -> TCEnv
e { envActiveProblems :: Set ProblemId
envActiveProblems = Set ProblemId
pids', envSolvingConstraints :: Bool
envSolvingConstraints = Bool
isSolving }) forall a b. (a -> b) -> a -> b
$
    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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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_ = forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
Set ProblemId -> Blocker -> Constraint -> m ProblemConstraint
buildProblemConstraint 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 <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Set ProblemId
envActiveProblems
  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             = (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint
  addAwakeConstraint :: Blocker -> Constraint -> ReaderT e m ()
addAwakeConstraint        = (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addAwakeConstraint
  solveConstraint :: Constraint -> ReaderT e m ()
solveConstraint           = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
solveConstraint
  solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> ReaderT e m ()
solveSomeAwakeConstraints = (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> Bool -> m ()
solveSomeAwakeConstraints
  stealConstraints :: ProblemId -> ReaderT e m ()
stealConstraints          = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadConstraint m => ProblemId -> m ()
stealConstraints
  modifyAwakeConstraints :: ([ProblemConstraint] -> [ProblemConstraint]) -> ReaderT e m ()
modifyAwakeConstraints    = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifyAwakeConstraints
  modifySleepingConstraints :: ([ProblemConstraint] -> [ProblemConstraint]) -> ReaderT e m ()
modifySleepingConstraints = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifySleepingConstraints
  wakeConstraints :: (ProblemConstraint -> WakeUp) -> ReaderT e m ()
wakeConstraints = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> WakeUp) -> m ()
wakeConstraints

addAndUnblocker :: MonadBlock m => Blocker -> m a -> m a
addAndUnblocker :: forall (m :: * -> *) a. MonadBlock m => Blocker -> m a -> m a
addAndUnblocker Blocker
u
  | Blocker
u forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock = forall a. a -> a
id
  | Bool
otherwise          = forall (m :: * -> *) a.
MonadBlock m =>
(Blocker -> m a) -> m a -> m a
catchPatternErr forall a b. (a -> b) -> a -> b
$ \ Blocker
u' -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> Blocker -> Blocker
unblockOnBoth Blocker
u Blocker
u')

addOrUnblocker :: MonadBlock m => Blocker -> m a -> m a
addOrUnblocker :: forall (m :: * -> *) a. MonadBlock m => Blocker -> m a -> m a
addOrUnblocker Blocker
u
  | Blocker
u forall a. Eq a => a -> a -> Bool
== Blocker
neverUnblock = forall a. a -> a
id
  | Bool
otherwise         = forall (m :: * -> *) a.
MonadBlock m =>
(Blocker -> m a) -> m a -> m a
catchPatternErr forall a b. (a -> b) -> a -> b
$ \ Blocker
u' -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> Blocker -> Blocker
unblockOnEither Blocker
u Blocker
u')

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

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

addConstraintTo :: Lens' Constraints TCState -> Blocker -> Constraint -> TCM ()
addConstraintTo :: Lens' [ProblemConstraint] TCState
-> Blocker -> Constraint -> TCMT IO ()
addConstraintTo Lens' [ProblemConstraint] TCState
bucket Blocker
unblock Constraint
c = do
    ProblemConstraint
pc <- TCM ProblemConstraint
build
    Lens' Bool TCState
stDirty forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` Bool
True
    Lens' [ProblemConstraint] TCState
bucket forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` (ProblemConstraint
pc forall a. a -> [a] -> [a]
:)
  where
    build :: TCM ProblemConstraint
build | Constraint -> Bool
isBlocking Constraint
c = Blocker -> Constraint -> TCM ProblemConstraint
buildConstraint Blocker
unblock Constraint
c
          | Bool
otherwise    = forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
Blocker -> Constraint -> m ProblemConstraint
buildProblemConstraint_ Blocker
unblock Constraint
c
    isBlocking :: Constraint -> Bool
isBlocking = \case
      SortCmp{}        -> Bool
False
      LevelCmp{}       -> Bool
False
      FindInstance{}   -> 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 = forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envSolvingConstraints :: Bool
envSolvingConstraints = Bool
True }

isSolvingConstraints :: MonadTCEnv m => m Bool
isSolvingConstraints :: forall (m :: * -> *). MonadTCEnv m => m Bool
isSolvingConstraints = 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 = forall (m :: * -> *) a.
MonadBlock m =>
(Blocker -> m a) -> m a -> m a
catchPatternErr forall a b. (a -> b) -> a -> b
$ \ Blocker
unblock -> 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

shouldPostponeInstanceSearch :: (ReadTCState m, HasOptions m) => m Bool
shouldPostponeInstanceSearch :: forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
shouldPostponeInstanceSearch =
  forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
and2M ((forall o i. o -> Lens' i o -> i
^. Lens' Bool TCState
stConsideringInstance) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m TCState
getTCState)
        (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optOverlappingInstances forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
  forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` ((forall o i. o -> Lens' i o -> i
^. Lens' Bool TCState
stPostponeInstanceSearch) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
shouldPostponeInstanceSearch
  let skip :: ProblemConstraint -> Bool
skip ProblemConstraint
c = Bool
skipInstance Bool -> Bool -> Bool
&& Constraint -> Bool
isInstanceConstraint (forall a. Closure a -> a
clValue forall a b. (a -> b) -> a -> b
$ ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c)
  forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> WakeUp) -> m ()
wakeConstraints forall a b. (a -> b) -> a -> b
$ forall constr.
(constr -> Bool) -> (constr -> WakeUp) -> constr -> WakeUp
wakeUpWhen (Bool -> Bool
not 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 = forall i o. Lens' i o -> LensMap i o
over Lens' [ProblemConstraint] TCState
stAwakeConstraints

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