module Agda.TypeChecking.Monad.Constraints where

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 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.List
import Agda.Utils.Lens
import Agda.Utils.Monad
import Agda.Utils.Tuple ((&&&))

{-# INLINE solvingProblem #-}
solvingProblem :: MonadConstraint m => ProblemId -> m a -> m a
solvingProblem :: forall (m :: * -> *) a.
MonadConstraint m =>
ProblemId -> m a -> m a
solvingProblem ProblemId
pid 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 problem " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ProblemId -> [Char]
forall a. Show a => a -> [Char]
show ProblemId
pid) (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ do
  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 (ASetter TCEnv TCEnv (Set ProblemId) (Set ProblemId)
-> (Set ProblemId -> Set ProblemId) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv (Set ProblemId) (Set ProblemId)
Lens' TCEnv (Set ProblemId)
eActiveProblems (ProblemId -> Set ProblemId -> Set ProblemId
forall a. Ord a => a -> Set a -> Set a
Set.insert ProblemId
pid)) m a
m
  ifNotM (isProblemSolved pid)
      (reportSLn "tc.constr.solve" 50 $ "problem " ++ show pid ++ " was not solved.")
    $ {- else -} do
      reportSLn "tc.constr.solve" 50 $ "problem " ++ show pid ++ " was solved!"
      wakeConstraints (wakeIfBlockedOnProblem pid . constraintUnblocker)
  return x

{-# INLINE solvingProblems #-}
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
  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 (ASetter TCEnv TCEnv (Set ProblemId) (Set ProblemId)
-> (Set ProblemId -> Set ProblemId) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv (Set ProblemId) (Set ProblemId)
Lens' TCEnv (Set ProblemId)
eActiveProblems (Set ProblemId
pids Set ProblemId -> Set ProblemId -> Set ProblemId
forall a. Ord a => Set a -> Set a -> Set a
`Set.union`)) m a
m
  Fold.forM_ pids \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)
  return 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 = do
  active <- Lens' TCEnv (Set ProblemId) -> m (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Set ProblemId -> f (Set ProblemId)) -> TCEnv -> f TCEnv
Lens' TCEnv (Set ProblemId)
eActiveProblems
  tc     <- getTCState
  pure $!    not (Set.member pid active)
          && not (any belongsToUs (tc ^. stAwakeConstraints))
          && not (any belongsToUs (tc ^. stSleepingConstraints))
  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`

isProblemSolved'' :: ProblemId -> TCM Bool
isProblemSolved'' :: ProblemId -> TCM Bool
isProblemSolved'' ProblemId
pid = do
  active <- Lens' TCEnv (Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Set ProblemId -> f (Set ProblemId)) -> TCEnv -> f TCEnv
Lens' TCEnv (Set ProblemId)
eActiveProblems
  tc     <- getTCState
  pure $!    not (any belongsToUs (tc ^. stAwakeConstraints))
          && not (any belongsToUs (tc ^. stSleepingConstraints))
  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
False

{-# 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]
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]
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])
-> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint])
-> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifyConstraints [ProblemConstraint] -> [ProblemConstraint]
filt [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
  tc <- m TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  let (takeAwake , keepAwake ) = partition' f $ tc ^. stAwakeConstraints
  let (takeAsleep, keepAsleep) = partition' f $ tc ^. stSleepingConstraints
  modifyConstraints (const keepAwake) (const keepAsleep)
  return $! takeAwake ++! takeAsleep

putConstraintsToSleep :: MonadConstraint m => (ProblemConstraint -> Bool) -> m ()
putConstraintsToSleep :: forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> m ()
putConstraintsToSleep ProblemConstraint -> Bool
sleepy = do
  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 (!gotoSleep, !stayAwake) = partition' sleepy awakeOnes
  modifyConstraints (const stayAwake) (++! gotoSleep) -- TODO: quadratic append!

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
  tc <- TCMT IO TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  let (!holdAwake,  !stillAwake)  = partition' (p AwakeConstraint)    $ tc ^. stAwakeConstraints
  let (!holdAsleep, !stillAsleep) = partition' (p SleepingConstraint) $ tc ^. stSleepingConstraints
  modifyTC' $ set stAwakeConstraints stillAwake . set stSleepingConstraints stillAsleep
  let restore = (TCState -> TCState) -> TCMT IO ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC' ((TCState -> TCState) -> TCMT IO ())
-> (TCState -> TCState) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ ASetter TCState TCState [ProblemConstraint] [ProblemConstraint]
-> ([ProblemConstraint] -> [ProblemConstraint])
-> TCState
-> TCState
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCState TCState [ProblemConstraint] [ProblemConstraint]
Lens' TCState [ProblemConstraint]
stAwakeConstraints ([ProblemConstraint]
holdAwake [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
forall a. [a] -> [a] -> [a]
++!)
                          (TCState -> TCState) -> (TCState -> TCState) -> TCState -> TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter TCState TCState [ProblemConstraint] [ProblemConstraint]
-> ([ProblemConstraint] -> [ProblemConstraint])
-> TCState
-> TCState
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCState TCState [ProblemConstraint] [ProblemConstraint]
Lens' TCState [ProblemConstraint]
stSleepingConstraints ([ProblemConstraint]
holdAsleep [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
forall a. [a] -> [a] -> [a]
++!)
  catchError (m <* 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
  cs <- m [ProblemConstraint]
forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
getAwakeConstraints
  case break p 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
  s <- m TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  return $! s ^. stAwakeConstraints ++! s ^. 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
  pids'     <- Lens' TCEnv (Set ProblemId) -> m (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Set ProblemId -> f (Set ProblemId)) -> TCEnv -> f TCEnv
Lens' TCEnv (Set ProblemId)
eActiveProblems
  isSolving <- viewTC eSolvingConstraints
  enterClosure c \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 (ASetter TCEnv TCEnv (Set ProblemId) (Set ProblemId)
-> Set ProblemId -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv (Set ProblemId) (Set ProblemId)
Lens' TCEnv (Set ProblemId)
eActiveProblems Set ProblemId
pids' (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter TCEnv TCEnv Bool Bool -> Bool -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv Bool Bool
Lens' TCEnv Bool
eSolvingConstraints Bool
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
  pids <- Lens' TCEnv (Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Set ProblemId -> f (Set ProblemId)) -> TCEnv -> f TCEnv
Lens' TCEnv (Set ProblemId)
eActiveProblems
  buildProblemConstraint pids unblock 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 ()

  -- | Modify both awake (first argument) and sleeping (second argument) constraints.
  modifyConstraints :: (Constraints -> Constraints) -> (Constraints -> Constraints) -> m ()

  {-# INLINE modifyAwakeConstraints #-}
  modifyAwakeConstraints :: (Constraints -> Constraints) -> m ()
  modifyAwakeConstraints [ProblemConstraint] -> [ProblemConstraint]
f = ([ProblemConstraint] -> [ProblemConstraint])
-> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint])
-> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifyConstraints [ProblemConstraint] -> [ProblemConstraint]
f [ProblemConstraint] -> [ProblemConstraint]
forall a. a -> a
id

  {-# INLINE modifySleepingConstraints #-}
  modifySleepingConstraints  :: (Constraints -> Constraints) -> m ()
  modifySleepingConstraints [ProblemConstraint] -> [ProblemConstraint]
f = ([ProblemConstraint] -> [ProblemConstraint])
-> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint])
-> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifyConstraints [ProblemConstraint] -> [ProblemConstraint]
forall a. a -> a
id [ProblemConstraint] -> [ProblemConstraint]
f

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
  modifyConstraints :: ([ProblemConstraint] -> [ProblemConstraint])
-> ([ProblemConstraint] -> [ProblemConstraint]) -> ReaderT e m ()
modifyConstraints         = (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 ())
 -> ([ProblemConstraint] -> [ProblemConstraint]) -> ReaderT e m ())
-> (([ProblemConstraint] -> [ProblemConstraint])
    -> ([ProblemConstraint] -> [ProblemConstraint]) -> m ())
-> ([ProblemConstraint] -> [ProblemConstraint])
-> ([ProblemConstraint] -> [ProblemConstraint])
-> ReaderT e m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([ProblemConstraint] -> [ProblemConstraint])
-> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint])
-> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifyConstraints
  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

{-# INLINE addConstraintTo #-}
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
    pc <- Blocker -> Constraint -> TCM ProblemConstraint
buildConstraint Blocker
unblock Constraint
c
    tc <- getTCState
    putTC $! tc & stDirty .~ True & bucket %~ (pc :)

-- | 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
  RewConstraint{}       -> 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 (ASetter TCEnv TCEnv Bool Bool -> Bool -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv Bool Bool
Lens' TCEnv Bool
eSolvingConstraints Bool
True)

isSolvingConstraints :: MonadTCEnv m => m Bool
isSolvingConstraints :: forall (m :: * -> *). MonadTCEnv m => m Bool
isSolvingConstraints = Lens' TCEnv Bool -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eSolvingConstraints

{-# INLINE catchConstraint #-}
-- | 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
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 -> Getting Bool TCState Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool TCState Bool
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 -> Getting Bool TCState Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool TCState Bool
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
  skipInstance <- m Bool
forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
shouldPostponeInstanceSearch
  let 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)
  wakeConstraints $ wakeUpWhen (not . skip) p

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

mapAwakeConstraints :: (Constraints -> Constraints) -> TCState -> TCState
mapAwakeConstraints :: ([ProblemConstraint] -> [ProblemConstraint]) -> TCState -> TCState
mapAwakeConstraints = ASetter TCState TCState [ProblemConstraint] [ProblemConstraint]
-> ([ProblemConstraint] -> [ProblemConstraint])
-> TCState
-> TCState
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCState TCState [ProblemConstraint] [ProblemConstraint]
Lens' TCState [ProblemConstraint]
stAwakeConstraints

mapSleepingConstraints :: (Constraints -> Constraints) -> TCState -> TCState
mapSleepingConstraints :: ([ProblemConstraint] -> [ProblemConstraint]) -> TCState -> TCState
mapSleepingConstraints = ASetter TCState TCState [ProblemConstraint] [ProblemConstraint]
-> ([ProblemConstraint] -> [ProblemConstraint])
-> TCState
-> TCState
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCState TCState [ProblemConstraint] [ProblemConstraint]
Lens' TCState [ProblemConstraint]
stSleepingConstraints