module Agda.Syntax.Internal.Blockers where

import Control.DeepSeq

import Data.Data (Data)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Semigroup

import GHC.Generics (Generic)

import Agda.Syntax.Common
import Agda.Syntax.Internal.Elim

import Agda.Utils.Pretty hiding ((<>))
import Agda.Utils.Functor

---------------------------------------------------------------------------
-- * Blocked Terms
---------------------------------------------------------------------------

-- | Even if we are not stuck on a meta during reduction
--   we can fail to reduce a definition by pattern matching
--   for another reason.
data NotBlocked' t
  = StuckOn (Elim' t)
    -- ^ The 'Elim' is neutral and blocks a pattern match.
  | Underapplied
    -- ^ Not enough arguments were supplied to complete the matching.
  | AbsurdMatch
    -- ^ We matched an absurd clause, results in a neutral 'Def'.
  | MissingClauses
    -- ^ We ran out of clauses, all considered clauses
    --   produced an actual mismatch.
    --   This can happen when try to reduce a function application
    --   but we are still missing some function clauses.
    --   See "Agda.TypeChecking.Patterns.Match".
  | ReallyNotBlocked
    -- ^ Reduction was not blocked, we reached a whnf
    --   which can be anything but a stuck @'Def'@.
  deriving (Int -> NotBlocked' t -> ShowS
[NotBlocked' t] -> ShowS
NotBlocked' t -> String
(Int -> NotBlocked' t -> ShowS)
-> (NotBlocked' t -> String)
-> ([NotBlocked' t] -> ShowS)
-> Show (NotBlocked' t)
forall t. Show t => Int -> NotBlocked' t -> ShowS
forall t. Show t => [NotBlocked' t] -> ShowS
forall t. Show t => NotBlocked' t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NotBlocked' t] -> ShowS
$cshowList :: forall t. Show t => [NotBlocked' t] -> ShowS
show :: NotBlocked' t -> String
$cshow :: forall t. Show t => NotBlocked' t -> String
showsPrec :: Int -> NotBlocked' t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> NotBlocked' t -> ShowS
Show, Typeable (NotBlocked' t)
DataType
Constr
Typeable (NotBlocked' t)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> NotBlocked' t -> c (NotBlocked' t))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (NotBlocked' t))
-> (NotBlocked' t -> Constr)
-> (NotBlocked' t -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (NotBlocked' t)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (NotBlocked' t)))
-> ((forall b. Data b => b -> b) -> NotBlocked' t -> NotBlocked' t)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r)
-> (forall u. (forall d. Data d => d -> u) -> NotBlocked' t -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> NotBlocked' t -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> NotBlocked' t -> m (NotBlocked' t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> NotBlocked' t -> m (NotBlocked' t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> NotBlocked' t -> m (NotBlocked' t))
-> Data (NotBlocked' t)
NotBlocked' t -> DataType
NotBlocked' t -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (NotBlocked' t))
(forall b. Data b => b -> b) -> NotBlocked' t -> NotBlocked' t
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NotBlocked' t -> c (NotBlocked' t)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (NotBlocked' t)
forall t. Data t => Typeable (NotBlocked' t)
forall t. Data t => NotBlocked' t -> DataType
forall t. Data t => NotBlocked' t -> Constr
forall t.
Data t =>
(forall b. Data b => b -> b) -> NotBlocked' t -> NotBlocked' t
forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> NotBlocked' t -> u
forall t u.
Data t =>
(forall d. Data d => d -> u) -> NotBlocked' t -> [u]
forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r
forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r
forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d)
-> NotBlocked' t -> m (NotBlocked' t)
forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> NotBlocked' t -> m (NotBlocked' t)
forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (NotBlocked' t)
forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NotBlocked' t -> c (NotBlocked' t)
forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (NotBlocked' t))
forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (NotBlocked' t))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> NotBlocked' t -> u
forall u. (forall d. Data d => d -> u) -> NotBlocked' t -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> NotBlocked' t -> m (NotBlocked' t)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> NotBlocked' t -> m (NotBlocked' t)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (NotBlocked' t)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NotBlocked' t -> c (NotBlocked' t)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (NotBlocked' t))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (NotBlocked' t))
$cReallyNotBlocked :: Constr
$cMissingClauses :: Constr
$cAbsurdMatch :: Constr
$cUnderapplied :: Constr
$cStuckOn :: Constr
$tNotBlocked' :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> NotBlocked' t -> m (NotBlocked' t)
$cgmapMo :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> NotBlocked' t -> m (NotBlocked' t)
gmapMp :: (forall d. Data d => d -> m d)
-> NotBlocked' t -> m (NotBlocked' t)
$cgmapMp :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> NotBlocked' t -> m (NotBlocked' t)
gmapM :: (forall d. Data d => d -> m d)
-> NotBlocked' t -> m (NotBlocked' t)
$cgmapM :: forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d)
-> NotBlocked' t -> m (NotBlocked' t)
gmapQi :: Int -> (forall d. Data d => d -> u) -> NotBlocked' t -> u
$cgmapQi :: forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> NotBlocked' t -> u
gmapQ :: (forall d. Data d => d -> u) -> NotBlocked' t -> [u]
$cgmapQ :: forall t u.
Data t =>
(forall d. Data d => d -> u) -> NotBlocked' t -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r
$cgmapQr :: forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r
$cgmapQl :: forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r
gmapT :: (forall b. Data b => b -> b) -> NotBlocked' t -> NotBlocked' t
$cgmapT :: forall t.
Data t =>
(forall b. Data b => b -> b) -> NotBlocked' t -> NotBlocked' t
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (NotBlocked' t))
$cdataCast2 :: forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (NotBlocked' t))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (NotBlocked' t))
$cdataCast1 :: forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (NotBlocked' t))
dataTypeOf :: NotBlocked' t -> DataType
$cdataTypeOf :: forall t. Data t => NotBlocked' t -> DataType
toConstr :: NotBlocked' t -> Constr
$ctoConstr :: forall t. Data t => NotBlocked' t -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (NotBlocked' t)
$cgunfold :: forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (NotBlocked' t)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NotBlocked' t -> c (NotBlocked' t)
$cgfoldl :: forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NotBlocked' t -> c (NotBlocked' t)
$cp1Data :: forall t. Data t => Typeable (NotBlocked' t)
Data, (forall x. NotBlocked' t -> Rep (NotBlocked' t) x)
-> (forall x. Rep (NotBlocked' t) x -> NotBlocked' t)
-> Generic (NotBlocked' t)
forall x. Rep (NotBlocked' t) x -> NotBlocked' t
forall x. NotBlocked' t -> Rep (NotBlocked' t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (NotBlocked' t) x -> NotBlocked' t
forall t x. NotBlocked' t -> Rep (NotBlocked' t) x
$cto :: forall t x. Rep (NotBlocked' t) x -> NotBlocked' t
$cfrom :: forall t x. NotBlocked' t -> Rep (NotBlocked' t) x
Generic)

-- | 'ReallyNotBlocked' is the unit.
--   'MissingClauses' is dominant.
--   @'StuckOn'{}@ should be propagated, if tied, we take the left.
instance Semigroup (NotBlocked' t) where
  NotBlocked' t
ReallyNotBlocked <> :: NotBlocked' t -> NotBlocked' t -> NotBlocked' t
<> NotBlocked' t
b = NotBlocked' t
b
  -- MissingClauses is dominant (absorptive)
  b :: NotBlocked' t
b@NotBlocked' t
MissingClauses <> NotBlocked' t
_ = NotBlocked' t
b
  NotBlocked' t
_ <> b :: NotBlocked' t
b@NotBlocked' t
MissingClauses = NotBlocked' t
b
  -- StuckOn is second strongest
  b :: NotBlocked' t
b@StuckOn{}      <> NotBlocked' t
_ = NotBlocked' t
b
  NotBlocked' t
_ <> b :: NotBlocked' t
b@StuckOn{}      = NotBlocked' t
b
  NotBlocked' t
b <> NotBlocked' t
_                = NotBlocked' t
b

instance Monoid (NotBlocked' t) where
  -- ReallyNotBlocked is neutral
  mempty :: NotBlocked' t
mempty  = NotBlocked' t
forall t. NotBlocked' t
ReallyNotBlocked
  mappend :: NotBlocked' t -> NotBlocked' t -> NotBlocked' t
mappend = NotBlocked' t -> NotBlocked' t -> NotBlocked' t
forall a. Semigroup a => a -> a -> a
(<>)

instance NFData t => NFData (NotBlocked' t)

-- | What is causing the blocking? Or in other words which metas or problems need to be solved to
--   unblock the blocked computation/constraint.
data Blocker = UnblockOnAll (Set Blocker)
             | UnblockOnAny (Set Blocker)
             | UnblockOnMeta MetaId     -- ^ Unblock if meta is instantiated
             | UnblockOnProblem ProblemId
  deriving (Typeable Blocker
DataType
Constr
Typeable Blocker
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Blocker -> c Blocker)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Blocker)
-> (Blocker -> Constr)
-> (Blocker -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Blocker))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Blocker))
-> ((forall b. Data b => b -> b) -> Blocker -> Blocker)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocker -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocker -> r)
-> (forall u. (forall d. Data d => d -> u) -> Blocker -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Blocker -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Blocker -> m Blocker)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Blocker -> m Blocker)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Blocker -> m Blocker)
-> Data Blocker
Blocker -> DataType
Blocker -> Constr
(forall b. Data b => b -> b) -> Blocker -> Blocker
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Blocker -> c Blocker
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Blocker
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Blocker -> u
forall u. (forall d. Data d => d -> u) -> Blocker -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Blocker -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Blocker -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Blocker -> m Blocker
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Blocker -> m Blocker
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Blocker
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Blocker -> c Blocker
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Blocker)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Blocker)
$cUnblockOnProblem :: Constr
$cUnblockOnMeta :: Constr
$cUnblockOnAny :: Constr
$cUnblockOnAll :: Constr
$tBlocker :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Blocker -> m Blocker
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Blocker -> m Blocker
gmapMp :: (forall d. Data d => d -> m d) -> Blocker -> m Blocker
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Blocker -> m Blocker
gmapM :: (forall d. Data d => d -> m d) -> Blocker -> m Blocker
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Blocker -> m Blocker
gmapQi :: Int -> (forall d. Data d => d -> u) -> Blocker -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Blocker -> u
gmapQ :: (forall d. Data d => d -> u) -> Blocker -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Blocker -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Blocker -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Blocker -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Blocker -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Blocker -> r
gmapT :: (forall b. Data b => b -> b) -> Blocker -> Blocker
$cgmapT :: (forall b. Data b => b -> b) -> Blocker -> Blocker
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Blocker)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Blocker)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Blocker)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Blocker)
dataTypeOf :: Blocker -> DataType
$cdataTypeOf :: Blocker -> DataType
toConstr :: Blocker -> Constr
$ctoConstr :: Blocker -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Blocker
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Blocker
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Blocker -> c Blocker
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Blocker -> c Blocker
$cp1Data :: Typeable Blocker
Data, Int -> Blocker -> ShowS
[Blocker] -> ShowS
Blocker -> String
(Int -> Blocker -> ShowS)
-> (Blocker -> String) -> ([Blocker] -> ShowS) -> Show Blocker
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Blocker] -> ShowS
$cshowList :: [Blocker] -> ShowS
show :: Blocker -> String
$cshow :: Blocker -> String
showsPrec :: Int -> Blocker -> ShowS
$cshowsPrec :: Int -> Blocker -> ShowS
Show, Blocker -> Blocker -> Bool
(Blocker -> Blocker -> Bool)
-> (Blocker -> Blocker -> Bool) -> Eq Blocker
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Blocker -> Blocker -> Bool
$c/= :: Blocker -> Blocker -> Bool
== :: Blocker -> Blocker -> Bool
$c== :: Blocker -> Blocker -> Bool
Eq, Eq Blocker
Eq Blocker
-> (Blocker -> Blocker -> Ordering)
-> (Blocker -> Blocker -> Bool)
-> (Blocker -> Blocker -> Bool)
-> (Blocker -> Blocker -> Bool)
-> (Blocker -> Blocker -> Bool)
-> (Blocker -> Blocker -> Blocker)
-> (Blocker -> Blocker -> Blocker)
-> Ord Blocker
Blocker -> Blocker -> Bool
Blocker -> Blocker -> Ordering
Blocker -> Blocker -> Blocker
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Blocker -> Blocker -> Blocker
$cmin :: Blocker -> Blocker -> Blocker
max :: Blocker -> Blocker -> Blocker
$cmax :: Blocker -> Blocker -> Blocker
>= :: Blocker -> Blocker -> Bool
$c>= :: Blocker -> Blocker -> Bool
> :: Blocker -> Blocker -> Bool
$c> :: Blocker -> Blocker -> Bool
<= :: Blocker -> Blocker -> Bool
$c<= :: Blocker -> Blocker -> Bool
< :: Blocker -> Blocker -> Bool
$c< :: Blocker -> Blocker -> Bool
compare :: Blocker -> Blocker -> Ordering
$ccompare :: Blocker -> Blocker -> Ordering
$cp1Ord :: Eq Blocker
Ord, (forall x. Blocker -> Rep Blocker x)
-> (forall x. Rep Blocker x -> Blocker) -> Generic Blocker
forall x. Rep Blocker x -> Blocker
forall x. Blocker -> Rep Blocker x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Blocker x -> Blocker
$cfrom :: forall x. Blocker -> Rep Blocker x
Generic)

instance NFData Blocker

alwaysUnblock :: Blocker
alwaysUnblock :: Blocker
alwaysUnblock = Set Blocker -> Blocker
UnblockOnAll Set Blocker
forall a. Set a
Set.empty

neverUnblock :: Blocker
neverUnblock :: Blocker
neverUnblock = Set Blocker -> Blocker
UnblockOnAny Set Blocker
forall a. Set a
Set.empty

unblockOnAll :: Set Blocker -> Blocker
unblockOnAll :: Set Blocker -> Blocker
unblockOnAll Set Blocker
us =
  case Set Blocker -> Set Blocker
allViewS Set Blocker
us of
    Set Blocker
us | [Blocker
u] <- Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
us -> Blocker
u
    Set Blocker
us                        -> Set Blocker -> Blocker
UnblockOnAll Set Blocker
us
  where
    allViewS :: Set Blocker -> Set Blocker
allViewS = [Set Blocker] -> Set Blocker
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Blocker] -> Set Blocker)
-> (Set Blocker -> [Set Blocker]) -> Set Blocker -> Set Blocker
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Blocker -> Set Blocker) -> [Blocker] -> [Set Blocker]
forall a b. (a -> b) -> [a] -> [b]
map Blocker -> Set Blocker
allView ([Blocker] -> [Set Blocker])
-> (Set Blocker -> [Blocker]) -> Set Blocker -> [Set Blocker]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList
    allView :: Blocker -> Set Blocker
allView (UnblockOnAll Set Blocker
us) = Set Blocker -> Set Blocker
allViewS Set Blocker
us
    allView Blocker
u                 = Blocker -> Set Blocker
forall a. a -> Set a
Set.singleton Blocker
u

unblockOnAny :: Set Blocker -> Blocker
unblockOnAny :: Set Blocker -> Blocker
unblockOnAny Set Blocker
us =
  case Set Blocker -> Set Blocker
anyViewS Set Blocker
us of
    Set Blocker
us | [Blocker
u] <- Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
us        -> Blocker
u
    Set Blocker
us | Blocker -> Set Blocker -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Blocker
alwaysUnblock Set Blocker
us -> Blocker
alwaysUnblock
       | Bool
otherwise                   -> Set Blocker -> Blocker
UnblockOnAny Set Blocker
us
  where
    anyViewS :: Set Blocker -> Set Blocker
anyViewS = [Set Blocker] -> Set Blocker
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Blocker] -> Set Blocker)
-> (Set Blocker -> [Set Blocker]) -> Set Blocker -> Set Blocker
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Blocker -> Set Blocker) -> [Blocker] -> [Set Blocker]
forall a b. (a -> b) -> [a] -> [b]
map Blocker -> Set Blocker
anyView ([Blocker] -> [Set Blocker])
-> (Set Blocker -> [Blocker]) -> Set Blocker -> [Set Blocker]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList
    anyView :: Blocker -> Set Blocker
anyView (UnblockOnAny Set Blocker
us) = Set Blocker -> Set Blocker
anyViewS Set Blocker
us
    anyView Blocker
u                 = Blocker -> Set Blocker
forall a. a -> Set a
Set.singleton Blocker
u

unblockOnEither :: Blocker -> Blocker -> Blocker
unblockOnEither :: Blocker -> Blocker -> Blocker
unblockOnEither Blocker
a Blocker
b = Set Blocker -> Blocker
unblockOnAny (Set Blocker -> Blocker) -> Set Blocker -> Blocker
forall a b. (a -> b) -> a -> b
$ [Blocker] -> Set Blocker
forall a. Ord a => [a] -> Set a
Set.fromList [Blocker
a, Blocker
b]

unblockOnMeta :: MetaId -> Blocker
unblockOnMeta :: MetaId -> Blocker
unblockOnMeta = MetaId -> Blocker
UnblockOnMeta

unblockOnProblem :: ProblemId -> Blocker
unblockOnProblem :: ProblemId -> Blocker
unblockOnProblem = ProblemId -> Blocker
UnblockOnProblem

unblockOnAllMetas :: Set MetaId -> Blocker
unblockOnAllMetas :: Set MetaId -> Blocker
unblockOnAllMetas = Set Blocker -> Blocker
unblockOnAll (Set Blocker -> Blocker)
-> (Set MetaId -> Set Blocker) -> Set MetaId -> Blocker
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> Blocker) -> Set MetaId -> Set Blocker
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic MetaId -> Blocker
unblockOnMeta

unblockOnAnyMeta :: Set MetaId -> Blocker
unblockOnAnyMeta :: Set MetaId -> Blocker
unblockOnAnyMeta = Set Blocker -> Blocker
unblockOnAny (Set Blocker -> Blocker)
-> (Set MetaId -> Set Blocker) -> Set MetaId -> Blocker
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> Blocker) -> Set MetaId -> Set Blocker
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic MetaId -> Blocker
unblockOnMeta

onBlockingMetasM :: Monad m => (MetaId -> m Blocker) -> Blocker -> m Blocker
onBlockingMetasM :: (MetaId -> m Blocker) -> Blocker -> m Blocker
onBlockingMetasM MetaId -> m Blocker
f (UnblockOnAll Set Blocker
bs)    = Set Blocker -> Blocker
unblockOnAll (Set Blocker -> Blocker)
-> ([Blocker] -> Set Blocker) -> [Blocker] -> Blocker
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Blocker] -> Set Blocker
forall a. Ord a => [a] -> Set a
Set.fromList ([Blocker] -> Blocker) -> m [Blocker] -> m Blocker
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Blocker -> m Blocker) -> [Blocker] -> m [Blocker]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((MetaId -> m Blocker) -> Blocker -> m Blocker
forall (m :: * -> *).
Monad m =>
(MetaId -> m Blocker) -> Blocker -> m Blocker
onBlockingMetasM MetaId -> m Blocker
f) (Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
bs)
onBlockingMetasM MetaId -> m Blocker
f (UnblockOnAny Set Blocker
bs)    = Set Blocker -> Blocker
unblockOnAny (Set Blocker -> Blocker)
-> ([Blocker] -> Set Blocker) -> [Blocker] -> Blocker
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Blocker] -> Set Blocker
forall a. Ord a => [a] -> Set a
Set.fromList ([Blocker] -> Blocker) -> m [Blocker] -> m Blocker
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Blocker -> m Blocker) -> [Blocker] -> m [Blocker]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((MetaId -> m Blocker) -> Blocker -> m Blocker
forall (m :: * -> *).
Monad m =>
(MetaId -> m Blocker) -> Blocker -> m Blocker
onBlockingMetasM MetaId -> m Blocker
f) (Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
bs)
onBlockingMetasM MetaId -> m Blocker
f (UnblockOnMeta MetaId
x)    = MetaId -> m Blocker
f MetaId
x
onBlockingMetasM MetaId -> m Blocker
f b :: Blocker
b@UnblockOnProblem{} = Blocker -> m Blocker
forall (f :: * -> *) a. Applicative f => a -> f a
pure Blocker
b

allBlockingMetas :: Blocker -> Set MetaId
allBlockingMetas :: Blocker -> Set MetaId
allBlockingMetas (UnblockOnAll Set Blocker
us)  = [Set MetaId] -> Set MetaId
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set MetaId] -> Set MetaId) -> [Set MetaId] -> Set MetaId
forall a b. (a -> b) -> a -> b
$ (Blocker -> Set MetaId) -> [Blocker] -> [Set MetaId]
forall a b. (a -> b) -> [a] -> [b]
map Blocker -> Set MetaId
allBlockingMetas ([Blocker] -> [Set MetaId]) -> [Blocker] -> [Set MetaId]
forall a b. (a -> b) -> a -> b
$ Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
us
allBlockingMetas (UnblockOnAny Set Blocker
us)  = [Set MetaId] -> Set MetaId
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set MetaId] -> Set MetaId) -> [Set MetaId] -> Set MetaId
forall a b. (a -> b) -> a -> b
$ (Blocker -> Set MetaId) -> [Blocker] -> [Set MetaId]
forall a b. (a -> b) -> [a] -> [b]
map Blocker -> Set MetaId
allBlockingMetas ([Blocker] -> [Set MetaId]) -> [Blocker] -> [Set MetaId]
forall a b. (a -> b) -> a -> b
$ Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
us
allBlockingMetas (UnblockOnMeta MetaId
x)  = MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton MetaId
x
allBlockingMetas UnblockOnProblem{} = Set MetaId
forall a. Set a
Set.empty

allBlockingProblems :: Blocker -> Set ProblemId
allBlockingProblems :: Blocker -> Set ProblemId
allBlockingProblems (UnblockOnAll Set Blocker
us)    = [Set ProblemId] -> Set ProblemId
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set ProblemId] -> Set ProblemId)
-> [Set ProblemId] -> Set ProblemId
forall a b. (a -> b) -> a -> b
$ (Blocker -> Set ProblemId) -> [Blocker] -> [Set ProblemId]
forall a b. (a -> b) -> [a] -> [b]
map Blocker -> Set ProblemId
allBlockingProblems ([Blocker] -> [Set ProblemId]) -> [Blocker] -> [Set ProblemId]
forall a b. (a -> b) -> a -> b
$ Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
us
allBlockingProblems (UnblockOnAny Set Blocker
us)    = [Set ProblemId] -> Set ProblemId
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set ProblemId] -> Set ProblemId)
-> [Set ProblemId] -> Set ProblemId
forall a b. (a -> b) -> a -> b
$ (Blocker -> Set ProblemId) -> [Blocker] -> [Set ProblemId]
forall a b. (a -> b) -> [a] -> [b]
map Blocker -> Set ProblemId
allBlockingProblems ([Blocker] -> [Set ProblemId]) -> [Blocker] -> [Set ProblemId]
forall a b. (a -> b) -> a -> b
$ Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
us
allBlockingProblems UnblockOnMeta{}      = Set ProblemId
forall a. Set a
Set.empty
allBlockingProblems (UnblockOnProblem ProblemId
p) = ProblemId -> Set ProblemId
forall a. a -> Set a
Set.singleton ProblemId
p

-- Note: We pick the All rather than the Any as the semigroup instance.
instance Semigroup Blocker where
  Blocker
x <> :: Blocker -> Blocker -> Blocker
<> Blocker
y = Set Blocker -> Blocker
unblockOnAll (Set Blocker -> Blocker) -> Set Blocker -> Blocker
forall a b. (a -> b) -> a -> b
$ [Blocker] -> Set Blocker
forall a. Ord a => [a] -> Set a
Set.fromList [Blocker
x, Blocker
y]

instance Monoid Blocker where
  mempty :: Blocker
mempty = Blocker
alwaysUnblock
  mappend :: Blocker -> Blocker -> Blocker
mappend = Blocker -> Blocker -> Blocker
forall a. Semigroup a => a -> a -> a
(<>)

instance Pretty Blocker where
  pretty :: Blocker -> Doc
pretty (UnblockOnAll Set Blocker
us)      = Doc
"all" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
"," ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Blocker -> Doc) -> [Blocker] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Blocker -> Doc
forall a. Pretty a => a -> Doc
pretty ([Blocker] -> [Doc]) -> [Blocker] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
us)
  pretty (UnblockOnAny Set Blocker
us)      = Doc
"any" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
"," ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Blocker -> Doc) -> [Blocker] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Blocker -> Doc
forall a. Pretty a => a -> Doc
pretty ([Blocker] -> [Doc]) -> [Blocker] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
us)
  pretty (UnblockOnMeta MetaId
m)      = MetaId -> Doc
forall a. Pretty a => a -> Doc
pretty MetaId
m
  pretty (UnblockOnProblem ProblemId
pid) = Doc
"problem" Doc -> Doc -> Doc
<+> ProblemId -> Doc
forall a. Pretty a => a -> Doc
pretty ProblemId
pid

-- | Something where a meta variable may block reduction. Notably a top-level meta is considered
--   blocking. This did not use to be the case (pre Aug 2020).
data Blocked' t a
  = Blocked    { Blocked' t a -> Blocker
theBlocker      :: Blocker,       Blocked' t a -> a
ignoreBlocking :: a }
  | NotBlocked { Blocked' t a -> NotBlocked' t
blockingStatus  :: NotBlocked' t, ignoreBlocking :: a }
  deriving (Typeable (Blocked' t a)
DataType
Constr
Typeable (Blocked' t a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Blocked' t a -> c (Blocked' t a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Blocked' t a))
-> (Blocked' t a -> Constr)
-> (Blocked' t a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Blocked' t a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Blocked' t a)))
-> ((forall b. Data b => b -> b) -> Blocked' t a -> Blocked' t a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Blocked' t a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Blocked' t a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a))
-> Data (Blocked' t a)
Blocked' t a -> DataType
Blocked' t a -> Constr
(forall b. Data b => b -> b) -> Blocked' t a -> Blocked' t a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Blocked' t a -> c (Blocked' t a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Blocked' t a)
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Blocked' t a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Blocked' t a -> u
forall u. (forall d. Data d => d -> u) -> Blocked' t a -> [u]
forall t a. (Data t, Data a) => Typeable (Blocked' t a)
forall t a. (Data t, Data a) => Blocked' t a -> DataType
forall t a. (Data t, Data a) => Blocked' t a -> Constr
forall t a.
(Data t, Data a) =>
(forall b. Data b => b -> b) -> Blocked' t a -> Blocked' t a
forall t a u.
(Data t, Data a) =>
Int -> (forall d. Data d => d -> u) -> Blocked' t a -> u
forall t a u.
(Data t, Data a) =>
(forall d. Data d => d -> u) -> Blocked' t a -> [u]
forall t a r r'.
(Data t, Data a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r
forall t a r r'.
(Data t, Data a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r
forall t a (m :: * -> *).
(Data t, Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
forall t a (m :: * -> *).
(Data t, Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
forall t a (c :: * -> *).
(Data t, Data a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Blocked' t a)
forall t a (c :: * -> *).
(Data t, Data a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Blocked' t a -> c (Blocked' t a)
forall t a (t :: * -> *) (c :: * -> *).
(Data t, Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Blocked' t a))
forall t a (t :: * -> * -> *) (c :: * -> *).
(Data t, Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Blocked' t a))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Blocked' t a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Blocked' t a -> c (Blocked' t a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Blocked' t a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Blocked' t a))
$cNotBlocked :: Constr
$cBlocked :: Constr
$tBlocked' :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
$cgmapMo :: forall t a (m :: * -> *).
(Data t, Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
gmapMp :: (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
$cgmapMp :: forall t a (m :: * -> *).
(Data t, Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
gmapM :: (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
$cgmapM :: forall t a (m :: * -> *).
(Data t, Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Blocked' t a -> u
$cgmapQi :: forall t a u.
(Data t, Data a) =>
Int -> (forall d. Data d => d -> u) -> Blocked' t a -> u
gmapQ :: (forall d. Data d => d -> u) -> Blocked' t a -> [u]
$cgmapQ :: forall t a u.
(Data t, Data a) =>
(forall d. Data d => d -> u) -> Blocked' t a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r
$cgmapQr :: forall t a r r'.
(Data t, Data a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r
$cgmapQl :: forall t a r r'.
(Data t, Data a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r
gmapT :: (forall b. Data b => b -> b) -> Blocked' t a -> Blocked' t a
$cgmapT :: forall t a.
(Data t, Data a) =>
(forall b. Data b => b -> b) -> Blocked' t a -> Blocked' t a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Blocked' t a))
$cdataCast2 :: forall t a (t :: * -> * -> *) (c :: * -> *).
(Data t, Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Blocked' t a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Blocked' t a))
$cdataCast1 :: forall t a (t :: * -> *) (c :: * -> *).
(Data t, Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Blocked' t a))
dataTypeOf :: Blocked' t a -> DataType
$cdataTypeOf :: forall t a. (Data t, Data a) => Blocked' t a -> DataType
toConstr :: Blocked' t a -> Constr
$ctoConstr :: forall t a. (Data t, Data a) => Blocked' t a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Blocked' t a)
$cgunfold :: forall t a (c :: * -> *).
(Data t, Data a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Blocked' t a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Blocked' t a -> c (Blocked' t a)
$cgfoldl :: forall t a (c :: * -> *).
(Data t, Data a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Blocked' t a -> c (Blocked' t a)
$cp1Data :: forall t a. (Data t, Data a) => Typeable (Blocked' t a)
Data, Int -> Blocked' t a -> ShowS
[Blocked' t a] -> ShowS
Blocked' t a -> String
(Int -> Blocked' t a -> ShowS)
-> (Blocked' t a -> String)
-> ([Blocked' t a] -> ShowS)
-> Show (Blocked' t a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall t a. (Show a, Show t) => Int -> Blocked' t a -> ShowS
forall t a. (Show a, Show t) => [Blocked' t a] -> ShowS
forall t a. (Show a, Show t) => Blocked' t a -> String
showList :: [Blocked' t a] -> ShowS
$cshowList :: forall t a. (Show a, Show t) => [Blocked' t a] -> ShowS
show :: Blocked' t a -> String
$cshow :: forall t a. (Show a, Show t) => Blocked' t a -> String
showsPrec :: Int -> Blocked' t a -> ShowS
$cshowsPrec :: forall t a. (Show a, Show t) => Int -> Blocked' t a -> ShowS
Show, a -> Blocked' t b -> Blocked' t a
(a -> b) -> Blocked' t a -> Blocked' t b
(forall a b. (a -> b) -> Blocked' t a -> Blocked' t b)
-> (forall a b. a -> Blocked' t b -> Blocked' t a)
-> Functor (Blocked' t)
forall a b. a -> Blocked' t b -> Blocked' t a
forall a b. (a -> b) -> Blocked' t a -> Blocked' t b
forall t a b. a -> Blocked' t b -> Blocked' t a
forall t a b. (a -> b) -> Blocked' t a -> Blocked' t b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Blocked' t b -> Blocked' t a
$c<$ :: forall t a b. a -> Blocked' t b -> Blocked' t a
fmap :: (a -> b) -> Blocked' t a -> Blocked' t b
$cfmap :: forall t a b. (a -> b) -> Blocked' t a -> Blocked' t b
Functor, Blocked' t a -> Bool
(a -> m) -> Blocked' t a -> m
(a -> b -> b) -> b -> Blocked' t a -> b
(forall m. Monoid m => Blocked' t m -> m)
-> (forall m a. Monoid m => (a -> m) -> Blocked' t a -> m)
-> (forall m a. Monoid m => (a -> m) -> Blocked' t a -> m)
-> (forall a b. (a -> b -> b) -> b -> Blocked' t a -> b)
-> (forall a b. (a -> b -> b) -> b -> Blocked' t a -> b)
-> (forall b a. (b -> a -> b) -> b -> Blocked' t a -> b)
-> (forall b a. (b -> a -> b) -> b -> Blocked' t a -> b)
-> (forall a. (a -> a -> a) -> Blocked' t a -> a)
-> (forall a. (a -> a -> a) -> Blocked' t a -> a)
-> (forall a. Blocked' t a -> [a])
-> (forall a. Blocked' t a -> Bool)
-> (forall a. Blocked' t a -> Int)
-> (forall a. Eq a => a -> Blocked' t a -> Bool)
-> (forall a. Ord a => Blocked' t a -> a)
-> (forall a. Ord a => Blocked' t a -> a)
-> (forall a. Num a => Blocked' t a -> a)
-> (forall a. Num a => Blocked' t a -> a)
-> Foldable (Blocked' t)
forall a. Eq a => a -> Blocked' t a -> Bool
forall a. Num a => Blocked' t a -> a
forall a. Ord a => Blocked' t a -> a
forall m. Monoid m => Blocked' t m -> m
forall a. Blocked' t a -> Bool
forall a. Blocked' t a -> Int
forall a. Blocked' t a -> [a]
forall a. (a -> a -> a) -> Blocked' t a -> a
forall t a. Eq a => a -> Blocked' t a -> Bool
forall t a. Num a => Blocked' t a -> a
forall t a. Ord a => Blocked' t a -> a
forall m a. Monoid m => (a -> m) -> Blocked' t a -> m
forall t m. Monoid m => Blocked' t m -> m
forall t a. Blocked' t a -> Bool
forall t a. Blocked' t a -> Int
forall t a. Blocked' t a -> [a]
forall b a. (b -> a -> b) -> b -> Blocked' t a -> b
forall a b. (a -> b -> b) -> b -> Blocked' t a -> b
forall t a. (a -> a -> a) -> Blocked' t a -> a
forall t m a. Monoid m => (a -> m) -> Blocked' t a -> m
forall t b a. (b -> a -> b) -> b -> Blocked' t a -> b
forall t a b. (a -> b -> b) -> b -> Blocked' t a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Blocked' t a -> a
$cproduct :: forall t a. Num a => Blocked' t a -> a
sum :: Blocked' t a -> a
$csum :: forall t a. Num a => Blocked' t a -> a
minimum :: Blocked' t a -> a
$cminimum :: forall t a. Ord a => Blocked' t a -> a
maximum :: Blocked' t a -> a
$cmaximum :: forall t a. Ord a => Blocked' t a -> a
elem :: a -> Blocked' t a -> Bool
$celem :: forall t a. Eq a => a -> Blocked' t a -> Bool
length :: Blocked' t a -> Int
$clength :: forall t a. Blocked' t a -> Int
null :: Blocked' t a -> Bool
$cnull :: forall t a. Blocked' t a -> Bool
toList :: Blocked' t a -> [a]
$ctoList :: forall t a. Blocked' t a -> [a]
foldl1 :: (a -> a -> a) -> Blocked' t a -> a
$cfoldl1 :: forall t a. (a -> a -> a) -> Blocked' t a -> a
foldr1 :: (a -> a -> a) -> Blocked' t a -> a
$cfoldr1 :: forall t a. (a -> a -> a) -> Blocked' t a -> a
foldl' :: (b -> a -> b) -> b -> Blocked' t a -> b
$cfoldl' :: forall t b a. (b -> a -> b) -> b -> Blocked' t a -> b
foldl :: (b -> a -> b) -> b -> Blocked' t a -> b
$cfoldl :: forall t b a. (b -> a -> b) -> b -> Blocked' t a -> b
foldr' :: (a -> b -> b) -> b -> Blocked' t a -> b
$cfoldr' :: forall t a b. (a -> b -> b) -> b -> Blocked' t a -> b
foldr :: (a -> b -> b) -> b -> Blocked' t a -> b
$cfoldr :: forall t a b. (a -> b -> b) -> b -> Blocked' t a -> b
foldMap' :: (a -> m) -> Blocked' t a -> m
$cfoldMap' :: forall t m a. Monoid m => (a -> m) -> Blocked' t a -> m
foldMap :: (a -> m) -> Blocked' t a -> m
$cfoldMap :: forall t m a. Monoid m => (a -> m) -> Blocked' t a -> m
fold :: Blocked' t m -> m
$cfold :: forall t m. Monoid m => Blocked' t m -> m
Foldable, Functor (Blocked' t)
Foldable (Blocked' t)
Functor (Blocked' t)
-> Foldable (Blocked' t)
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Blocked' t a -> f (Blocked' t b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Blocked' t (f a) -> f (Blocked' t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Blocked' t a -> m (Blocked' t b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Blocked' t (m a) -> m (Blocked' t a))
-> Traversable (Blocked' t)
(a -> f b) -> Blocked' t a -> f (Blocked' t b)
forall t. Functor (Blocked' t)
forall t. Foldable (Blocked' t)
forall t (m :: * -> *) a.
Monad m =>
Blocked' t (m a) -> m (Blocked' t a)
forall t (f :: * -> *) a.
Applicative f =>
Blocked' t (f a) -> f (Blocked' t a)
forall t (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Blocked' t a -> m (Blocked' t b)
forall t (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Blocked' t a -> f (Blocked' t b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
Blocked' t (m a) -> m (Blocked' t a)
forall (f :: * -> *) a.
Applicative f =>
Blocked' t (f a) -> f (Blocked' t a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Blocked' t a -> m (Blocked' t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Blocked' t a -> f (Blocked' t b)
sequence :: Blocked' t (m a) -> m (Blocked' t a)
$csequence :: forall t (m :: * -> *) a.
Monad m =>
Blocked' t (m a) -> m (Blocked' t a)
mapM :: (a -> m b) -> Blocked' t a -> m (Blocked' t b)
$cmapM :: forall t (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Blocked' t a -> m (Blocked' t b)
sequenceA :: Blocked' t (f a) -> f (Blocked' t a)
$csequenceA :: forall t (f :: * -> *) a.
Applicative f =>
Blocked' t (f a) -> f (Blocked' t a)
traverse :: (a -> f b) -> Blocked' t a -> f (Blocked' t b)
$ctraverse :: forall t (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Blocked' t a -> f (Blocked' t b)
$cp2Traversable :: forall t. Foldable (Blocked' t)
$cp1Traversable :: forall t. Functor (Blocked' t)
Traversable, (forall x. Blocked' t a -> Rep (Blocked' t a) x)
-> (forall x. Rep (Blocked' t a) x -> Blocked' t a)
-> Generic (Blocked' t a)
forall x. Rep (Blocked' t a) x -> Blocked' t a
forall x. Blocked' t a -> Rep (Blocked' t a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t a x. Rep (Blocked' t a) x -> Blocked' t a
forall t a x. Blocked' t a -> Rep (Blocked' t a) x
$cto :: forall t a x. Rep (Blocked' t a) x -> Blocked' t a
$cfrom :: forall t a x. Blocked' t a -> Rep (Blocked' t a) x
Generic)

instance Decoration (Blocked' t) where
  traverseF :: (a -> m b) -> Blocked' t a -> m (Blocked' t b)
traverseF a -> m b
f (Blocked Blocker
b a
x)     = Blocker -> b -> Blocked' t b
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b (b -> Blocked' t b) -> m b -> m (Blocked' t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
x
  traverseF a -> m b
f (NotBlocked NotBlocked' t
nb a
x) = NotBlocked' t -> b -> Blocked' t b
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' t
nb (b -> Blocked' t b) -> m b -> m (Blocked' t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
x

-- | Blocking on _all_ blockers.
instance Applicative (Blocked' t) where
  pure :: a -> Blocked' t a
pure = a -> Blocked' t a
forall a t. a -> Blocked' t a
notBlocked
  Blocked' t (a -> b)
f <*> :: Blocked' t (a -> b) -> Blocked' t a -> Blocked' t b
<*> Blocked' t a
e = ((Blocked' t (a -> b)
f Blocked' t (a -> b) -> () -> Blocked' t ()
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ()) Blocked' t () -> Blocked' t () -> Blocked' t ()
forall a. Monoid a => a -> a -> a
`mappend` (Blocked' t a
e Blocked' t a -> () -> Blocked' t ()
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ())) Blocked' t () -> b -> Blocked' t b
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Blocked' t (a -> b) -> a -> b
forall t a. Blocked' t a -> a
ignoreBlocking Blocked' t (a -> b)
f (Blocked' t a -> a
forall t a. Blocked' t a -> a
ignoreBlocking Blocked' t a
e)

instance Semigroup a => Semigroup (Blocked' t a) where
  Blocked Blocker
x a
a    <> :: Blocked' t a -> Blocked' t a -> Blocked' t a
<> Blocked Blocker
y a
b    = Blocker -> a -> Blocked' t a
forall t a. Blocker -> a -> Blocked' t a
Blocked (Blocker
x Blocker -> Blocker -> Blocker
forall a. Semigroup a => a -> a -> a
<> Blocker
y) (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
b)
  b :: Blocked' t a
b@Blocked{}    <> NotBlocked{}   = Blocked' t a
b
  NotBlocked{}   <> b :: Blocked' t a
b@Blocked{}    = Blocked' t a
b
  NotBlocked NotBlocked' t
x a
a <> NotBlocked NotBlocked' t
y a
b = NotBlocked' t -> a -> Blocked' t a
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked (NotBlocked' t
x NotBlocked' t -> NotBlocked' t -> NotBlocked' t
forall a. Semigroup a => a -> a -> a
<> NotBlocked' t
y) (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
b)

instance (Semigroup a, Monoid a) => Monoid (Blocked' t a) where
  mempty :: Blocked' t a
mempty = a -> Blocked' t a
forall a t. a -> Blocked' t a
notBlocked a
forall a. Monoid a => a
mempty
  mappend :: Blocked' t a -> Blocked' t a -> Blocked' t a
mappend = Blocked' t a -> Blocked' t a -> Blocked' t a
forall a. Semigroup a => a -> a -> a
(<>)

instance (NFData t, NFData a) => NFData (Blocked' t a)

-- | When trying to reduce @f es@, on match failed on one
--   elimination @e ∈ es@ that came with info @r :: NotBlocked@.
--   @stuckOn e r@ produces the new @NotBlocked@ info.
--
--   'MissingClauses' must be propagated, as this is blockage
--   that can be lifted in the future (as more clauses are added).
--
--   @'StuckOn' e0@ is also propagated, since it provides more
--   precise information as @StuckOn e@ (as @e0@ is the original
--   reason why reduction got stuck and usually a subterm of @e@).
--   An information like @StuckOn (Apply (Arg info (Var i [])))@
--   (stuck on a variable) could be used by the lhs/coverage checker
--   to trigger a split on that (pattern) variable.
--
--   In the remaining cases for @r@, we are terminally stuck
--   due to @StuckOn e@.  Propagating @'AbsurdMatch'@ does not
--   seem useful.
--
--   'Underapplied' must not be propagated, as this would mean
--   that @f es@ is underapplied, which is not the case (it is stuck).
--   Note that 'Underapplied' can only arise when projection patterns were
--   missing to complete the original match (in @e@).
--   (Missing ordinary pattern would mean the @e@ is of function type,
--   but we cannot match against something of function type.)
stuckOn :: Elim' t -> NotBlocked' t -> NotBlocked' t
stuckOn :: Elim' t -> NotBlocked' t -> NotBlocked' t
stuckOn Elim' t
e NotBlocked' t
r =
  case NotBlocked' t
r of
    NotBlocked' t
MissingClauses   -> NotBlocked' t
r
    StuckOn{}        -> NotBlocked' t
r
    NotBlocked' t
Underapplied     -> NotBlocked' t
r'
    NotBlocked' t
AbsurdMatch      -> NotBlocked' t
r'
    NotBlocked' t
ReallyNotBlocked -> NotBlocked' t
r'
  where r' :: NotBlocked' t
r' = Elim' t -> NotBlocked' t
forall t. Elim' t -> NotBlocked' t
StuckOn Elim' t
e

---------------------------------------------------------------------------
-- * Handling blocked terms.
---------------------------------------------------------------------------

blockedOn :: Blocker -> a -> Blocked' t a
blockedOn :: Blocker -> a -> Blocked' t a
blockedOn Blocker
b | Blocker
alwaysUnblock Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
b = a -> Blocked' t a
forall a t. a -> Blocked' t a
notBlocked
            | Bool
otherwise          = Blocker -> a -> Blocked' t a
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b

blocked :: MetaId -> a -> Blocked' t a
blocked :: MetaId -> a -> Blocked' t a
blocked = Blocker -> a -> Blocked' t a
forall t a. Blocker -> a -> Blocked' t a
Blocked (Blocker -> a -> Blocked' t a)
-> (MetaId -> Blocker) -> MetaId -> a -> Blocked' t a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> Blocker
unblockOnMeta

notBlocked :: a -> Blocked' t a
notBlocked :: a -> Blocked' t a
notBlocked = NotBlocked' t -> a -> Blocked' t a
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' t
forall t. NotBlocked' t
ReallyNotBlocked

blocked_ :: MetaId -> Blocked' t ()
blocked_ :: MetaId -> Blocked' t ()
blocked_ MetaId
x = MetaId -> () -> Blocked' t ()
forall a t. MetaId -> a -> Blocked' t a
blocked MetaId
x ()

notBlocked_ :: Blocked' t ()
notBlocked_ :: Blocked' t ()
notBlocked_ = () -> Blocked' t ()
forall a t. a -> Blocked' t a
notBlocked ()

-----------------------------------------------------------------------------
-- * Waking up logic
-----------------------------------------------------------------------------

-- | Should a constraint wake up or not? If not, we might refine the unblocker.
data WakeUp = WakeUp | DontWakeUp (Maybe Blocker)
  deriving (Int -> WakeUp -> ShowS
[WakeUp] -> ShowS
WakeUp -> String
(Int -> WakeUp -> ShowS)
-> (WakeUp -> String) -> ([WakeUp] -> ShowS) -> Show WakeUp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [WakeUp] -> ShowS
$cshowList :: [WakeUp] -> ShowS
show :: WakeUp -> String
$cshow :: WakeUp -> String
showsPrec :: Int -> WakeUp -> ShowS
$cshowsPrec :: Int -> WakeUp -> ShowS
Show, WakeUp -> WakeUp -> Bool
(WakeUp -> WakeUp -> Bool)
-> (WakeUp -> WakeUp -> Bool) -> Eq WakeUp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WakeUp -> WakeUp -> Bool
$c/= :: WakeUp -> WakeUp -> Bool
== :: WakeUp -> WakeUp -> Bool
$c== :: WakeUp -> WakeUp -> Bool
Eq)

wakeUpWhen :: (constr -> Bool) -> (constr -> WakeUp) -> constr -> WakeUp
wakeUpWhen :: (constr -> Bool) -> (constr -> WakeUp) -> constr -> WakeUp
wakeUpWhen constr -> Bool
guard constr -> WakeUp
wake constr
c | constr -> Bool
guard constr
c   = constr -> WakeUp
wake constr
c
                        | Bool
otherwise = Maybe Blocker -> WakeUp
DontWakeUp Maybe Blocker
forall a. Maybe a
Nothing

wakeUpWhen_ :: (constr -> Bool) -> constr -> WakeUp
wakeUpWhen_ :: (constr -> Bool) -> constr -> WakeUp
wakeUpWhen_ constr -> Bool
p = (constr -> Bool) -> (constr -> WakeUp) -> constr -> WakeUp
forall constr.
(constr -> Bool) -> (constr -> WakeUp) -> constr -> WakeUp
wakeUpWhen constr -> Bool
p (WakeUp -> constr -> WakeUp
forall a b. a -> b -> a
const WakeUp
WakeUp)

wakeIfBlockedOnProblem :: ProblemId -> Blocker -> WakeUp
wakeIfBlockedOnProblem :: ProblemId -> Blocker -> WakeUp
wakeIfBlockedOnProblem ProblemId
pid Blocker
u
  | Blocker
u' Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock = WakeUp
WakeUp
  | Bool
otherwise           = Maybe Blocker -> WakeUp
DontWakeUp (Blocker -> Maybe Blocker
forall a. a -> Maybe a
Just Blocker
u')
  where
    u' :: Blocker
u' = ProblemId -> Blocker -> Blocker
unblockProblem ProblemId
pid Blocker
u

wakeIfBlockedOnMeta :: MetaId -> Blocker -> WakeUp
wakeIfBlockedOnMeta :: MetaId -> Blocker -> WakeUp
wakeIfBlockedOnMeta MetaId
x Blocker
u
  | Blocker
u' Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock = WakeUp
WakeUp
  | Bool
otherwise           = Maybe Blocker -> WakeUp
DontWakeUp (Blocker -> Maybe Blocker
forall a. a -> Maybe a
Just Blocker
u')
  where
    u' :: Blocker
u' = MetaId -> Blocker -> Blocker
unblockMeta MetaId
x Blocker
u

unblockMeta :: MetaId -> Blocker -> Blocker
unblockMeta :: MetaId -> Blocker -> Blocker
unblockMeta MetaId
x u :: Blocker
u@(UnblockOnMeta MetaId
y) | MetaId
x MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
y    = Blocker
alwaysUnblock
                                  | Bool
otherwise = Blocker
u
unblockMeta MetaId
_ u :: Blocker
u@UnblockOnProblem{} = Blocker
u
unblockMeta MetaId
x (UnblockOnAll Set Blocker
us)    = Set Blocker -> Blocker
unblockOnAll (Set Blocker -> Blocker) -> Set Blocker -> Blocker
forall a b. (a -> b) -> a -> b
$ (Blocker -> Blocker) -> Set Blocker -> Set Blocker
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (MetaId -> Blocker -> Blocker
unblockMeta MetaId
x) Set Blocker
us
unblockMeta MetaId
x (UnblockOnAny Set Blocker
us)    = Set Blocker -> Blocker
unblockOnAny (Set Blocker -> Blocker) -> Set Blocker -> Blocker
forall a b. (a -> b) -> a -> b
$ (Blocker -> Blocker) -> Set Blocker -> Set Blocker
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (MetaId -> Blocker -> Blocker
unblockMeta MetaId
x) Set Blocker
us

unblockProblem :: ProblemId -> Blocker -> Blocker
unblockProblem :: ProblemId -> Blocker -> Blocker
unblockProblem ProblemId
p u :: Blocker
u@(UnblockOnProblem ProblemId
q) | ProblemId
p ProblemId -> ProblemId -> Bool
forall a. Eq a => a -> a -> Bool
== ProblemId
q    = Blocker
alwaysUnblock
                                        | Bool
otherwise = Blocker
u
unblockProblem ProblemId
_ u :: Blocker
u@UnblockOnMeta{} = Blocker
u
unblockProblem ProblemId
p (UnblockOnAll Set Blocker
us) = Set Blocker -> Blocker
unblockOnAll (Set Blocker -> Blocker) -> Set Blocker -> Blocker
forall a b. (a -> b) -> a -> b
$ (Blocker -> Blocker) -> Set Blocker -> Set Blocker
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (ProblemId -> Blocker -> Blocker
unblockProblem ProblemId
p) Set Blocker
us
unblockProblem ProblemId
p (UnblockOnAny Set Blocker
us) = Set Blocker -> Blocker
unblockOnAny (Set Blocker -> Blocker) -> Set Blocker -> Blocker
forall a b. (a -> b) -> a -> b
$ (Blocker -> Blocker) -> Set Blocker -> Set Blocker
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (ProblemId -> Blocker -> Blocker
unblockProblem ProblemId
p) Set Blocker
us