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 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
  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
  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 =
  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
  (takeAwake , 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
  (takeAsleep, keepAsleep) <- List.partition f <$> useTC stSleepingConstraints
  modifyAwakeConstraints    $ const keepAwake
  modifySleepingConstraints $ 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) = List.partition sleepy awakeOnes
  modifySleepingConstraints $ (++ gotoSleep)
  modifyAwakeConstraints    $ const 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
  (holdAwake, 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
  (holdAsleep, stillAsleep) <- List.partition (p SleepingConstraint) <$> useTC stSleepingConstraints
  stAwakeConstraints    `setTCLens` stillAwake
  stSleepingConstraints `setTCLens` stillAsleep
  let 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]
++)
  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', 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
  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 (\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
  pids <- (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Set ProblemId
envActiveProblems
  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 ()

  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
    pc <- Blocker -> Constraint -> TCM ProblemConstraint
buildConstraint Blocker
unblock Constraint
c
    stDirty `setTCLens` True
    bucket `modifyTCLens` (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

-- | 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
  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 = 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