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.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 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
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, 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@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  = forall t. NotBlocked' t
ReallyNotBlocked
  mappend :: NotBlocked' t -> NotBlocked' t -> NotBlocked' t
mappend = 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
             | UnblockOnDef QName       -- ^ Unblock when function is defined
  deriving (Int -> Blocker -> ShowS
[Blocker] -> ShowS
Blocker -> String
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
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
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
Ord, 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 forall a. Set a
Set.empty

neverUnblock :: Blocker
neverUnblock :: Blocker
neverUnblock = Set Blocker -> Blocker
UnblockOnAny 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] <- 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 = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Blocker -> Set Blocker
allView forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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                 = 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] <- forall a. Set a -> [a]
Set.toList Set Blocker
us        -> Blocker
u
    Set Blocker
us | 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 = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Blocker -> Set Blocker
anyView forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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                 = 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 forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
Set.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *).
Monad m =>
(MetaId -> m Blocker) -> Blocker -> m Blocker
onBlockingMetasM MetaId -> m Blocker
f) (forall a. Set a -> [a]
Set.toList Set Blocker
bs)
onBlockingMetasM MetaId -> m Blocker
f (UnblockOnAny Set Blocker
bs)    = Set Blocker -> Blocker
unblockOnAny forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
Set.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *).
Monad m =>
(MetaId -> m Blocker) -> Blocker -> m Blocker
onBlockingMetasM MetaId -> m Blocker
f) (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{} = forall (f :: * -> *) a. Applicative f => a -> f a
pure Blocker
b
onBlockingMetasM MetaId -> m Blocker
f b :: Blocker
b@UnblockOnDef{}     = forall (f :: * -> *) a. Applicative f => a -> f a
pure Blocker
b

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

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

allBlockingDefs :: Blocker -> Set QName
allBlockingDefs :: Blocker -> Set QName
allBlockingDefs (UnblockOnAll Set Blocker
us)  = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Blocker -> Set QName
allBlockingDefs forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Blocker
us
allBlockingDefs (UnblockOnAny Set Blocker
us)  = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Blocker -> Set QName
allBlockingDefs forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Blocker
us
allBlockingDefs UnblockOnMeta{}    = forall a. Set a
Set.empty
allBlockingDefs UnblockOnProblem{} = forall a. Set a
Set.empty
allBlockingDefs (UnblockOnDef QName
q)   = 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" forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
"," forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Blocker
us)
  pretty (UnblockOnAny Set Blocker
us)      = Doc
"any" forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
"," forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Blocker
us)
  pretty (UnblockOnMeta MetaId
m)      = forall a. Pretty a => a -> Doc
pretty MetaId
m
  pretty (UnblockOnProblem ProblemId
pid) = Doc
"problem" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty ProblemId
pid
  pretty (UnblockOnDef QName
q)       = Doc
"definition" Doc -> Doc -> 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
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, 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
<$ :: forall a b. a -> Blocked' t b -> Blocked' t a
$c<$ :: forall t a b. a -> Blocked' t b -> Blocked' t a
fmap :: forall a b. (a -> b) -> Blocked' t a -> Blocked' t b
$cfmap :: forall t a b. (a -> b) -> Blocked' t a -> Blocked' t b
Functor, forall a. Blocked' t a -> Bool
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 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 :: forall a. Num a => Blocked' t a -> a
$cproduct :: forall t a. Num a => Blocked' t a -> a
sum :: forall a. Num a => Blocked' t a -> a
$csum :: forall t a. Num a => Blocked' t a -> a
minimum :: forall a. Ord a => Blocked' t a -> a
$cminimum :: forall t a. Ord a => Blocked' t a -> a
maximum :: forall a. Ord a => Blocked' t a -> a
$cmaximum :: forall t a. Ord a => Blocked' t a -> a
elem :: forall a. Eq a => a -> Blocked' t a -> Bool
$celem :: forall t a. Eq a => a -> Blocked' t a -> Bool
length :: forall a. Blocked' t a -> Int
$clength :: forall t a. Blocked' t a -> Int
null :: forall a. Blocked' t a -> Bool
$cnull :: forall t a. Blocked' t a -> Bool
toList :: forall a. Blocked' t a -> [a]
$ctoList :: forall t a. Blocked' t a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Blocked' t a -> a
$cfoldl1 :: forall t a. (a -> a -> a) -> Blocked' t a -> a
foldr1 :: forall a. (a -> a -> a) -> Blocked' t a -> a
$cfoldr1 :: forall t a. (a -> a -> a) -> Blocked' t a -> a
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
$cfoldl :: forall t b a. (b -> a -> 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
$cfoldr :: forall t a b. (a -> b -> b) -> b -> Blocked' t a -> b
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
$cfoldMap :: forall t m a. Monoid m => (a -> m) -> Blocked' t a -> m
fold :: forall m. Monoid m => Blocked' t m -> m
$cfold :: forall t m. Monoid m => Blocked' t m -> m
Foldable, 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 (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Blocked' t a -> f (Blocked' t b)
sequence :: forall (m :: * -> *) a.
Monad m =>
Blocked' t (m a) -> m (Blocked' t a)
$csequence :: forall t (m :: * -> *) a.
Monad m =>
Blocked' t (m a) -> m (Blocked' t a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(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 :: forall (f :: * -> *) a.
Applicative f =>
Blocked' t (f a) -> f (Blocked' t a)
$csequenceA :: forall t (f :: * -> *) a.
Applicative f =>
Blocked' t (f a) -> f (Blocked' t a)
traverse :: 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)
Traversable, 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 :: 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)     = forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
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) = forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' t
nb 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 = 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 forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ()) forall a. Monoid a => a -> a -> a
`mappend` (Blocked' t a
e forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ())) forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> forall t a. Blocked' t a -> a
ignoreBlocking Blocked' t (a -> b)
f (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    = forall t a. Blocker -> a -> Blocked' t a
Blocked (Blocker -> Blocker -> Blocker
unblockOnBoth Blocker
x Blocker
y) (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 = forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked (NotBlocked' t
x forall a. Semigroup a => a -> a -> a
<> NotBlocked' t
y) (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 = forall a t. a -> Blocked' t a
notBlocked forall a. Monoid a => a
mempty
  mappend :: Blocked' t a -> Blocked' t a -> Blocked' t a
mappend = 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' = 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 forall a. Eq a => a -> a -> Bool
== Blocker
b = forall a t. a -> Blocked' t a
notBlocked
            | Bool
otherwise          = 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 = forall t a. Blocker -> a -> Blocked' t a
Blocked 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 = forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked forall t. NotBlocked' t
ReallyNotBlocked

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

notBlocked_ :: Blocked' t ()
notBlocked_ :: forall t. Blocked' t ()
notBlocked_ = 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
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
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 :: 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 forall a. Maybe a
Nothing

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

wakeIfBlockedOnProblem :: ProblemId -> Blocker -> WakeUp
wakeIfBlockedOnProblem :: ProblemId -> Blocker -> WakeUp
wakeIfBlockedOnProblem ProblemId
pid Blocker
u
  | Blocker
u' forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock = WakeUp
WakeUp
  | Bool
otherwise           = Maybe Blocker -> WakeUp
DontWakeUp (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' forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock = WakeUp
WakeUp
  | Bool
otherwise           = Maybe Blocker -> WakeUp
DontWakeUp (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' forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock = WakeUp
WakeUp
  | Bool
otherwise           = Maybe Blocker -> WakeUp
DontWakeUp (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 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 forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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 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 forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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 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 forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (QName -> Blocker -> Blocker
unblockDef QName
q) Set Blocker
us