module Agda.TypeChecking.Monad.Constraints where
import Control.Arrow ((&&&))
import Control.Monad.Except
import Control.Monad.Reader
import qualified Data.Foldable as Fold
import qualified Data.List as List
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Semigroup ((<>))
import Agda.Interaction.Options.Base
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Closure
import Agda.TypeChecking.Monad.Debug
import Agda.Utils.Lens
import Agda.Utils.Monad
solvingProblem :: MonadConstraint m => ProblemId -> m a -> m a
solvingProblem :: forall (m :: * -> *) a.
MonadConstraint m =>
ProblemId -> m a -> m a
solvingProblem ProblemId
pid = Set ProblemId -> m a -> m a
forall (m :: * -> *) a.
MonadConstraint m =>
Set ProblemId -> m a -> m a
solvingProblems (ProblemId -> Set ProblemId
forall a. a -> Set a
Set.singleton ProblemId
pid)
solvingProblems :: MonadConstraint m => Set ProblemId -> m a -> m a
solvingProblems :: forall (m :: * -> *) a.
MonadConstraint m =>
Set ProblemId -> m a -> m a
solvingProblems Set ProblemId
pids m a
m = [Char] -> VerboseLevel -> [Char] -> m a -> m a
forall a. [Char] -> VerboseLevel -> [Char] -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.constr.solve" VerboseLevel
50 ([Char]
"working on problems " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [ProblemId] -> [Char]
forall a. Show a => a -> [Char]
show (Set ProblemId -> [ProblemId]
forall a. Set a -> [a]
Set.toList Set ProblemId
pids)) (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ do
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
$ 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
{-# 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
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
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
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)
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
(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
class ( MonadTCEnv m
, ReadTCState m
, MonadError TCErr m
, MonadBlock m
, HasOptions m
, MonadDebug m
) => MonadConstraint m where
addConstraint :: Blocker -> Constraint -> m ()
addAwakeConstraint :: Blocker -> Constraint -> m ()
solveConstraint :: Constraint -> m ()
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
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 :)
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
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
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)
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
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