module Agda.Syntax.Internal.Blockers where

import Control.DeepSeq

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

import GHC.Generics (Generic)

import Agda.Syntax.Common
import Agda.Syntax.Abstract.Name (QName)
import Agda.Syntax.Internal.Elim

import Agda.Syntax.Common.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 QName
    -- ^ We ran out of clauses for 'QName', 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
$cshowsPrec :: forall t. Show t => Int -> NotBlocked' t -> ShowS
showsPrec :: Int -> NotBlocked' t -> ShowS
$cshow :: forall t. Show t => NotBlocked' t -> String
show :: NotBlocked' t -> String
$cshowList :: forall t. Show t => [NotBlocked' t] -> ShowS
showList :: [NotBlocked' t] -> ShowS
Show, (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
$cfrom :: forall t x. NotBlocked' t -> Rep (NotBlocked' t) x
from :: forall x. NotBlocked' t -> Rep (NotBlocked' t) x
$cto :: forall t x. Rep (NotBlocked' t) x -> NotBlocked' t
to :: forall x. Rep (NotBlocked' t) x -> NotBlocked' t
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@MissingClauses{} <> NotBlocked' t
_ = NotBlocked' t
b
  NotBlocked' t
_ <> b :: NotBlocked' t
b@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)

instance Pretty t => Pretty (NotBlocked' t) where
  pretty :: NotBlocked' t -> Doc
pretty = \case
    StuckOn Elim' t
e        -> Doc
"elimination" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Elim' t -> Doc
forall a. Pretty a => a -> Doc
pretty Elim' t
e
    NotBlocked' t
Underapplied     -> Doc
"missing elimination (underapplied)"
    NotBlocked' t
AbsurdMatch      -> Doc
"absurd match"
    MissingClauses QName
x -> Doc
"missing clause for" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x
    NotBlocked' t
ReallyNotBlocked -> Doc
"(not stuck)"

-- | 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
             | UnblockOnDef QName       -- ^ Unblock when function is defined
  deriving (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
$cshowsPrec :: Int -> Blocker -> ShowS
showsPrec :: Int -> Blocker -> ShowS
$cshow :: Blocker -> String
show :: Blocker -> String
$cshowList :: [Blocker] -> ShowS
showList :: [Blocker] -> ShowS
Show, Blocker -> Blocker -> Bool
(Blocker -> Blocker -> Bool)
-> (Blocker -> Blocker -> Bool) -> Eq Blocker
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Blocker -> Blocker -> Bool
== :: Blocker -> Blocker -> Bool
$c/= :: Blocker -> Blocker -> Bool
/= :: 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
$ccompare :: Blocker -> Blocker -> Ordering
compare :: Blocker -> Blocker -> Ordering
$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
>= :: Blocker -> Blocker -> Bool
$cmax :: Blocker -> Blocker -> Blocker
max :: Blocker -> Blocker -> Blocker
$cmin :: Blocker -> Blocker -> Blocker
min :: Blocker -> Blocker -> 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
$cfrom :: forall x. Blocker -> Rep Blocker x
from :: forall x. Blocker -> Rep Blocker x
$cto :: forall x. Rep Blocker x -> Blocker
to :: forall x. Rep Blocker x -> Blocker
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]

unblockOnBoth :: Blocker -> Blocker -> Blocker
unblockOnBoth :: Blocker -> Blocker -> Blocker
unblockOnBoth Blocker
a Blocker
b = 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
a, Blocker
b]

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

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

unblockOnDef :: QName -> Blocker
unblockOnDef :: QName -> Blocker
unblockOnDef = QName -> Blocker
UnblockOnDef

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 :: forall (m :: * -> *).
Monad m =>
(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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Blocker
b
onBlockingMetasM MetaId -> m Blocker
f b :: Blocker
b@UnblockOnDef{}     = Blocker -> m Blocker
forall a. a -> m a
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
allBlockingMetas UnblockOnDef{}     = 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
allBlockingProblems UnblockOnDef{}       = Set ProblemId
forall a. Set a
Set.empty

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

{- There are two possible instances of Semigroup, so we don't commit
   to either one.
instance Semigroup Blocker where
  x <> y = unblockOnAll $ Set.fromList [x, y]

instance Monoid Blocker where
  mempty = alwaysUnblock
  mappend = (<>)
-}

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
forall a. Doc a -> Doc a -> Doc a
<+> ProblemId -> Doc
forall a. Pretty a => a -> Doc
pretty ProblemId
pid
  pretty (UnblockOnDef QName
q)       = Doc
"definition" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q

-- | 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    { forall t a. Blocked' t a -> Blocker
theBlocker      :: Blocker,       forall t a. Blocked' t a -> a
ignoreBlocking :: a }
  | NotBlocked { forall t a. Blocked' t a -> NotBlocked' t
blockingStatus  :: NotBlocked' t, ignoreBlocking :: a }
  deriving (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 t, Show a) => Int -> Blocked' t a -> ShowS
forall t a. (Show t, Show a) => [Blocked' t a] -> ShowS
forall t a. (Show t, Show a) => Blocked' t a -> String
$cshowsPrec :: forall t a. (Show t, Show a) => Int -> Blocked' t a -> ShowS
showsPrec :: Int -> Blocked' t a -> ShowS
$cshow :: forall t a. (Show t, Show a) => Blocked' t a -> String
show :: Blocked' t a -> String
$cshowList :: forall t a. (Show t, Show a) => [Blocked' t a] -> ShowS
showList :: [Blocked' t a] -> ShowS
Show, (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
$cfmap :: forall t a b. (a -> b) -> Blocked' t a -> Blocked' t b
fmap :: forall a b. (a -> b) -> Blocked' t a -> Blocked' t b
$c<$ :: forall t a b. a -> Blocked' t b -> Blocked' t a
<$ :: forall a b. a -> Blocked' t b -> Blocked' t a
Functor, (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
$cfold :: forall t m. Monoid m => Blocked' t m -> m
fold :: forall m. Monoid m => Blocked' t m -> m
$cfoldMap :: forall t m a. Monoid m => (a -> m) -> Blocked' t a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Blocked' t a -> m
$cfoldMap' :: forall t m a. Monoid m => (a -> m) -> Blocked' t a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Blocked' t a -> m
$cfoldr :: forall t a b. (a -> b -> b) -> b -> Blocked' t a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Blocked' t a -> b
$cfoldr' :: forall t a b. (a -> b -> b) -> b -> Blocked' t a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Blocked' t a -> b
$cfoldl :: forall t b a. (b -> a -> b) -> b -> Blocked' t a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Blocked' t a -> b
$cfoldl' :: forall t b a. (b -> a -> b) -> b -> Blocked' t a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Blocked' t a -> b
$cfoldr1 :: forall t a. (a -> a -> a) -> Blocked' t a -> a
foldr1 :: forall a. (a -> a -> a) -> Blocked' t a -> a
$cfoldl1 :: forall t a. (a -> a -> a) -> Blocked' t a -> a
foldl1 :: forall a. (a -> a -> a) -> Blocked' t a -> a
$ctoList :: forall t a. Blocked' t a -> [a]
toList :: forall a. Blocked' t a -> [a]
$cnull :: forall t a. Blocked' t a -> Bool
null :: forall a. Blocked' t a -> Bool
$clength :: forall t a. Blocked' t a -> Int
length :: forall a. Blocked' t a -> Int
$celem :: forall t a. Eq a => a -> Blocked' t a -> Bool
elem :: forall a. Eq a => a -> Blocked' t a -> Bool
$cmaximum :: forall t a. Ord a => Blocked' t a -> a
maximum :: forall a. Ord a => Blocked' t a -> a
$cminimum :: forall t a. Ord a => Blocked' t a -> a
minimum :: forall a. Ord a => Blocked' t a -> a
$csum :: forall t a. Num a => Blocked' t a -> a
sum :: forall a. Num a => Blocked' t a -> a
$cproduct :: forall t a. Num a => Blocked' t a -> a
product :: forall a. Num a => Blocked' t a -> a
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)
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)
$ctraverse :: forall t (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Blocked' t a -> f (Blocked' t b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Blocked' t a -> f (Blocked' t b)
$csequenceA :: forall t (f :: * -> *) a.
Applicative f =>
Blocked' t (f a) -> f (Blocked' t a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Blocked' t (f a) -> f (Blocked' t a)
$cmapM :: forall t (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Blocked' t a -> m (Blocked' t b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Blocked' t a -> m (Blocked' t b)
$csequence :: forall t (m :: * -> *) a.
Monad m =>
Blocked' t (m a) -> m (Blocked' t a)
sequence :: forall (m :: * -> *) a.
Monad m =>
Blocked' t (m a) -> m (Blocked' t a)
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
$cfrom :: forall t a x. Blocked' t a -> Rep (Blocked' t a) x
from :: forall x. Blocked' t a -> Rep (Blocked' t a) x
$cto :: forall t a x. Rep (Blocked' t a) x -> Blocked' t a
to :: forall x. Rep (Blocked' t a) x -> Blocked' t a
Generic)

instance Decoration (Blocked' t) where
  traverseF :: forall (m :: * -> *) a b.
Functor m =>
(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 :: forall a. a -> Blocked' t a
pure = a -> Blocked' t a
forall a t. a -> Blocked' t a
notBlocked
  Blocked' t (a -> b)
f <*> :: forall a b. 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 -> Blocker -> Blocker
unblockOnBoth Blocker
x 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 :: forall t. Elim' t -> NotBlocked' t -> NotBlocked' t
stuckOn Elim' t
e = \case
    r :: NotBlocked' t
r@MissingClauses{} -> NotBlocked' t
r
    r :: 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 :: forall a t. 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 :: forall a t. 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 :: forall a t. 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_ :: forall t. MetaId -> Blocked' t ()
blocked_ MetaId
x = MetaId -> () -> Blocked' t ()
forall a t. MetaId -> a -> Blocked' t a
blocked MetaId
x ()

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

getBlocker :: Blocked' t a -> Blocker
getBlocker :: forall t a. Blocked' t a -> Blocker
getBlocker (Blocked Blocker
b a
_) = Blocker
b
getBlocker NotBlocked{}  = Blocker
neverUnblock

-----------------------------------------------------------------------------
-- * 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
$cshowsPrec :: Int -> WakeUp -> ShowS
showsPrec :: Int -> WakeUp -> ShowS
$cshow :: WakeUp -> String
show :: WakeUp -> String
$cshowList :: [WakeUp] -> ShowS
showList :: [WakeUp] -> ShowS
Show, WakeUp -> WakeUp -> Bool
(WakeUp -> WakeUp -> Bool)
-> (WakeUp -> WakeUp -> Bool) -> Eq WakeUp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: WakeUp -> WakeUp -> Bool
== :: WakeUp -> WakeUp -> Bool
$c/= :: WakeUp -> WakeUp -> Bool
/= :: WakeUp -> WakeUp -> Bool
Eq)

wakeUpWhen :: (constr -> Bool) -> (constr -> WakeUp) -> constr -> WakeUp
wakeUpWhen :: forall constr.
(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_ :: forall constr. (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

wakeIfBlockedOnDef :: QName -> Blocker -> WakeUp
wakeIfBlockedOnDef :: QName -> Blocker -> WakeUp
wakeIfBlockedOnDef QName
q 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' = QName -> Blocker -> Blocker
unblockDef QName
q 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
_ u :: Blocker
u@UnblockOnDef{}     = 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
_ u :: Blocker
u@UnblockOnDef{}  = 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

unblockDef :: QName -> Blocker -> Blocker
unblockDef :: QName -> Blocker -> Blocker
unblockDef QName
q u :: Blocker
u@(UnblockOnDef QName
q') | QName
q QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
q'   = Blocker
alwaysUnblock
                                 | Bool
otherwise = Blocker
u
unblockDef QName
q u :: Blocker
u@UnblockOnMeta{} = Blocker
u
unblockDef QName
q u :: Blocker
u@UnblockOnProblem{} = Blocker
u
unblockDef QName
q (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 (QName -> Blocker -> Blocker
unblockDef QName
q) Set Blocker
us
unblockDef QName
q (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 (QName -> Blocker -> Blocker
unblockDef QName
q) Set Blocker
us