module Agda.TypeChecking.Monad.Constraints where

import Control.Arrow ((&&&))



import qualified Data.Foldable as Fold
import qualified Data.List as List
import Data.Set (Set)
import qualified Data.Set as Set

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Closure
import Agda.TypeChecking.Monad.Debug

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


solvingProblem :: MonadConstraint m => ProblemId -> m a -> m a
solvingProblem :: 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 :: Set ProblemId -> m a -> m a
solvingProblems Set ProblemId
pids m a
m = VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
"tc.constr.solve" VerboseLevel
50 (VerboseKey
"working on problems " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [ProblemId] -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Set ProblemId -> [ProblemId]
forall a. Set a -> [a]
Set.toList Set ProblemId
pids)) (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ do
  a
x <- (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
e -> TCEnv
e { envActiveProblems :: Set ProblemId
envActiveProblems = Set ProblemId
pids Set ProblemId -> Set ProblemId -> Set ProblemId
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` TCEnv -> Set ProblemId
envActiveProblems TCEnv
e }) m a
m
  Set ProblemId -> (ProblemId -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
Fold.forM_ Set ProblemId
pids ((ProblemId -> m ()) -> m ()) -> (ProblemId -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ ProblemId
pid -> do
    m Bool -> m () -> m () -> m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (ProblemId -> m Bool
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
ProblemId -> m Bool
isProblemSolved ProblemId
pid)
        (VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.constr.solve" VerboseLevel
50 (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"problem " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ ProblemId -> VerboseKey
forall a. Show a => a -> VerboseKey
show ProblemId
pid VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" was not solved.")
      (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ {- else -} do
        VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.constr.solve" VerboseLevel
50 (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"problem " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ ProblemId -> VerboseKey
forall a. Show a => a -> VerboseKey
show ProblemId
pid VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" was solved!"
        (ProblemConstraint -> m Bool) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> m Bool) -> m ()
wakeConstraints (Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool)
-> (ProblemConstraint -> Bool) -> ProblemConstraint -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemId -> Constraint -> Bool
blockedOn ProblemId
pid (Constraint -> Bool)
-> (ProblemConstraint -> Constraint) -> ProblemConstraint -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (Closure Constraint -> Constraint)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint)
  a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
  where
    blockedOn :: ProblemId -> Constraint -> Bool
blockedOn ProblemId
pid (Guarded Constraint
_ ProblemId
pid') = ProblemId
pid ProblemId -> ProblemId -> Bool
forall a. Eq a => a -> a -> Bool
== ProblemId
pid'
    blockedOn ProblemId
_ Constraint
_ = Bool
False

isProblemSolved :: (MonadTCEnv m, ReadTCState m) => ProblemId -> m Bool
isProblemSolved :: ProblemId -> m Bool
isProblemSolved 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)
        ((ProblemConstraint -> Bool) -> [ProblemConstraint] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool)
-> (ProblemConstraint -> Bool) -> ProblemConstraint -> 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)
-> (ProblemConstraint -> Set ProblemId)
-> ProblemConstraint
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Set ProblemId
constraintProblems) ([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)

getConstraintsForProblem :: ReadTCState m => ProblemId -> m Constraints
getConstraintsForProblem :: 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 :: m [ProblemConstraint]
getAwakeConstraints = Lens' [ProblemConstraint] TCState -> m [ProblemConstraint]
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' [ProblemConstraint] TCState
stAwakeConstraints

-- danger...
dropConstraints :: MonadConstraint m => (ProblemConstraint -> Bool) -> m ()
dropConstraints :: (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 :: (ProblemConstraint -> Bool) -> m [ProblemConstraint]
takeConstraints ProblemConstraint -> Bool
f = do
  ([ProblemConstraint]
takeAwake , [ProblemConstraint]
keepAwake ) <- (ProblemConstraint -> Bool)
-> [ProblemConstraint]
-> ([ProblemConstraint], [ProblemConstraint])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition ProblemConstraint -> Bool
f ([ProblemConstraint] -> ([ProblemConstraint], [ProblemConstraint]))
-> m [ProblemConstraint]
-> m ([ProblemConstraint], [ProblemConstraint])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' [ProblemConstraint] TCState -> m [ProblemConstraint]
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [ProblemConstraint] TCState
stAwakeConstraints
  ([ProblemConstraint]
takeAsleep, [ProblemConstraint]
keepAsleep) <- (ProblemConstraint -> Bool)
-> [ProblemConstraint]
-> ([ProblemConstraint], [ProblemConstraint])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition ProblemConstraint -> Bool
f ([ProblemConstraint] -> ([ProblemConstraint], [ProblemConstraint]))
-> m [ProblemConstraint]
-> m ([ProblemConstraint], [ProblemConstraint])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' [ProblemConstraint] TCState -> m [ProblemConstraint]
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [ProblemConstraint] TCState
stSleepingConstraints
  ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifyAwakeConstraints    (([ProblemConstraint] -> [ProblemConstraint]) -> m ())
-> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall a b. (a -> b) -> a -> b
$ [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
forall a b. a -> b -> a
const [ProblemConstraint]
keepAwake
  ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
([ProblemConstraint] -> [ProblemConstraint]) -> m ()
modifySleepingConstraints (([ProblemConstraint] -> [ProblemConstraint]) -> m ())
-> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
forall a b. (a -> b) -> a -> b
$ [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
forall a b. a -> b -> a
const [ProblemConstraint]
keepAsleep
  [ProblemConstraint] -> m [ProblemConstraint]
forall (m :: * -> *) a. Monad m => a -> m a
return ([ProblemConstraint] -> m [ProblemConstraint])
-> [ProblemConstraint] -> m [ProblemConstraint]
forall a b. (a -> b) -> a -> b
$ [ProblemConstraint]
takeAwake [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
forall a. [a] -> [a] -> [a]
++ [ProblemConstraint]
takeAsleep

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

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

takeAwakeConstraint :: MonadConstraint m => m (Maybe ProblemConstraint)
takeAwakeConstraint :: 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' :: (ProblemConstraint -> Bool) -> m (Maybe ProblemConstraint)
takeAwakeConstraint' ProblemConstraint -> Bool
p = do
  [ProblemConstraint]
cs <- m [ProblemConstraint]
forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
getAwakeConstraints
  case (ProblemConstraint -> Bool)
-> [ProblemConstraint]
-> ([ProblemConstraint], [ProblemConstraint])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break ProblemConstraint -> Bool
p [ProblemConstraint]
cs of
    ([ProblemConstraint]
_, [])       -> Maybe ProblemConstraint -> m (Maybe ProblemConstraint)
forall (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 (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 :: m [ProblemConstraint]
getAllConstraints = do
  TCState
s <- m TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  [ProblemConstraint] -> m [ProblemConstraint]
forall (m :: * -> *) a. Monad m => a -> m a
return ([ProblemConstraint] -> m [ProblemConstraint])
-> [ProblemConstraint] -> m [ProblemConstraint]
forall a b. (a -> b) -> a -> b
$ TCState
sTCState -> Lens' [ProblemConstraint] TCState -> [ProblemConstraint]
forall o i. o -> Lens' i o -> i
^.Lens' [ProblemConstraint] TCState
stAwakeConstraints [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
forall a. [a] -> [a] -> [a]
++ TCState
sTCState -> Lens' [ProblemConstraint] TCState -> [ProblemConstraint]
forall o i. o -> Lens' i o -> i
^.Lens' [ProblemConstraint] TCState
stSleepingConstraints

withConstraint :: MonadConstraint m => (Constraint -> m a) -> ProblemConstraint -> m a
withConstraint :: (Constraint -> m a) -> ProblemConstraint -> m a
withConstraint Constraint -> m a
f (PConstr Set ProblemId
pids Closure Constraint
c) = do
  -- We should preserve the problem stack and the isSolvingConstraint flag
  (Set ProblemId
pids', Bool
isSolving) <- (TCEnv -> (Set ProblemId, Bool)) -> m (Set ProblemId, Bool)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC ((TCEnv -> (Set ProblemId, Bool)) -> m (Set ProblemId, Bool))
-> (TCEnv -> (Set ProblemId, Bool)) -> m (Set ProblemId, Bool)
forall a b. (a -> b) -> a -> b
$ TCEnv -> Set ProblemId
envActiveProblems (TCEnv -> Set ProblemId)
-> (TCEnv -> Bool) -> TCEnv -> (Set ProblemId, Bool)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& TCEnv -> Bool
envSolvingConstraints
  Closure Constraint -> (Constraint -> m a) -> m a
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Constraint
c ((Constraint -> m a) -> m a) -> (Constraint -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \Constraint
c ->
    (TCEnv -> TCEnv) -> m a -> m a
forall (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 }) (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 -> Constraint -> m ProblemConstraint
buildProblemConstraint :: Set ProblemId -> Constraint -> m ProblemConstraint
buildProblemConstraint Set ProblemId
pids Constraint
c = Set ProblemId -> Closure Constraint -> ProblemConstraint
PConstr Set ProblemId
pids (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)
  => Constraint -> m ProblemConstraint
buildProblemConstraint_ :: Constraint -> m ProblemConstraint
buildProblemConstraint_ = Set ProblemId -> Constraint -> m ProblemConstraint
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
Set ProblemId -> Constraint -> m ProblemConstraint
buildProblemConstraint Set ProblemId
forall a. Set a
Set.empty

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

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

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

  -- | `catchPatternErr handle m` runs m, handling pattern violations
  --    with `handle` (doesn't roll back the state)
  catchPatternErr :: m a -> m a -> m a

  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-> m Bool) -> m ()

  stealConstraints :: ProblemId -> m ()

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

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

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

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

addConstraintTo :: Lens' Constraints TCState -> Constraint -> TCM ()
addConstraintTo :: Lens' [ProblemConstraint] TCState -> Constraint -> TCMT IO ()
addConstraintTo Lens' [ProblemConstraint] TCState
bucket Constraint
c = do
    ProblemConstraint
pc <- TCM ProblemConstraint
build
    Lens' Bool TCState
stDirty Lens' Bool TCState -> Bool -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` Bool
True
    Lens' [ProblemConstraint] TCState
bucket Lens' [ProblemConstraint] TCState
-> ([ProblemConstraint] -> [ProblemConstraint]) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` (ProblemConstraint
pc ProblemConstraint -> [ProblemConstraint] -> [ProblemConstraint]
forall a. a -> [a] -> [a]
:)
  where
    build :: TCM ProblemConstraint
build | Constraint -> Bool
isBlocking Constraint
c = Constraint -> TCM ProblemConstraint
buildConstraint Constraint
c
          | Bool
otherwise    = Constraint -> TCM ProblemConstraint
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
Constraint -> m ProblemConstraint
buildProblemConstraint_ Constraint
c
    isBlocking :: Constraint -> Bool
isBlocking = \case
      SortCmp{}        -> Bool
False
      LevelCmp{}       -> Bool
False
      ValueCmp{}       -> Bool
True
      ValueCmpOnFace{} -> Bool
True
      ElimCmp{}        -> Bool
True
      TelCmp{}         -> Bool
True
      Guarded Constraint
c ProblemId
_      -> Constraint -> Bool
isBlocking Constraint
c
      UnBlock{}        -> Bool
True
      FindInstance{}   -> Bool
False
      IsEmpty{}        -> Bool
True
      CheckSizeLtSat{} -> Bool
True
      CheckFunDef{}    -> Bool
True
      HasBiggerSort{}  -> Bool
False
      HasPTSRule{}     -> Bool
False
      UnquoteTactic{}  -> Bool
True
      CheckMetaInst{}  -> Bool
True

-- | Start solving constraints
nowSolvingConstraints :: MonadTCEnv m => m a -> m a
nowSolvingConstraints :: m a -> m a
nowSolvingConstraints = (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 :: Bool
envSolvingConstraints = Bool
True }

isSolvingConstraints :: MonadTCEnv m => m Bool
isSolvingConstraints :: 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 :: Constraint -> m () -> m ()
catchConstraint Constraint
c = m () -> m () -> m ()
forall (m :: * -> *) a. MonadConstraint m => m a -> m a -> m a
catchPatternErr (m () -> m () -> m ()) -> m () -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Constraint -> m ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
addConstraint Constraint
c

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

mapAwakeConstraints :: (Constraints -> Constraints) -> TCState -> TCState
mapAwakeConstraints :: ([ProblemConstraint] -> [ProblemConstraint]) -> TCState -> TCState
mapAwakeConstraints = Lens' [ProblemConstraint] TCState
-> ([ProblemConstraint] -> [ProblemConstraint])
-> TCState
-> TCState
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 = Lens' [ProblemConstraint] TCState
-> ([ProblemConstraint] -> [ProblemConstraint])
-> TCState
-> TCState
forall i o. Lens' i o -> LensMap i o
over Lens' [ProblemConstraint] TCState
stSleepingConstraints