-- | Occurrences.

module Agda.TypeChecking.Positivity.Occurrence
  ( Occurrence(..)
  , OccursWhere(..)
  , Where(..)
  , boundToEverySome
  , productOfEdgesInBoundedWalk
  ) where

import Control.DeepSeq
import Control.Monad

import Data.Data (Data)

import Data.Foldable (toList)

import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Sequence (Seq)

import GHC.Generics (Generic)

import Agda.Syntax.Common
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Position

import Agda.Utils.Graph.AdjacencyMap.Unidirectional (Graph)
import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph
import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.SemiRing
import Agda.Utils.Size

import Agda.Utils.Impossible

-- Specification of occurrences -------------------------------------------

-- Operations and instances in Agda.TypeChecking.Positivity.

-- | Description of an occurrence.
data OccursWhere
  = OccursWhere Range (Seq Where) (Seq Where)
    -- ^ The elements of the sequences, read from left to right,
    -- explain how to get to the occurrence. The second sequence
    -- includes the main information, and if the first sequence is
    -- non-empty, then it includes information about the context of
    -- the second sequence.
  deriving (Nat -> OccursWhere -> ShowS
[OccursWhere] -> ShowS
OccursWhere -> String
(Nat -> OccursWhere -> ShowS)
-> (OccursWhere -> String)
-> ([OccursWhere] -> ShowS)
-> Show OccursWhere
forall a.
(Nat -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OccursWhere] -> ShowS
$cshowList :: [OccursWhere] -> ShowS
show :: OccursWhere -> String
$cshow :: OccursWhere -> String
showsPrec :: Nat -> OccursWhere -> ShowS
$cshowsPrec :: Nat -> OccursWhere -> ShowS
Show, OccursWhere -> OccursWhere -> Bool
(OccursWhere -> OccursWhere -> Bool)
-> (OccursWhere -> OccursWhere -> Bool) -> Eq OccursWhere
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OccursWhere -> OccursWhere -> Bool
$c/= :: OccursWhere -> OccursWhere -> Bool
== :: OccursWhere -> OccursWhere -> Bool
$c== :: OccursWhere -> OccursWhere -> Bool
Eq, Eq OccursWhere
Eq OccursWhere
-> (OccursWhere -> OccursWhere -> Ordering)
-> (OccursWhere -> OccursWhere -> Bool)
-> (OccursWhere -> OccursWhere -> Bool)
-> (OccursWhere -> OccursWhere -> Bool)
-> (OccursWhere -> OccursWhere -> Bool)
-> (OccursWhere -> OccursWhere -> OccursWhere)
-> (OccursWhere -> OccursWhere -> OccursWhere)
-> Ord OccursWhere
OccursWhere -> OccursWhere -> Bool
OccursWhere -> OccursWhere -> Ordering
OccursWhere -> OccursWhere -> OccursWhere
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 :: OccursWhere -> OccursWhere -> OccursWhere
$cmin :: OccursWhere -> OccursWhere -> OccursWhere
max :: OccursWhere -> OccursWhere -> OccursWhere
$cmax :: OccursWhere -> OccursWhere -> OccursWhere
>= :: OccursWhere -> OccursWhere -> Bool
$c>= :: OccursWhere -> OccursWhere -> Bool
> :: OccursWhere -> OccursWhere -> Bool
$c> :: OccursWhere -> OccursWhere -> Bool
<= :: OccursWhere -> OccursWhere -> Bool
$c<= :: OccursWhere -> OccursWhere -> Bool
< :: OccursWhere -> OccursWhere -> Bool
$c< :: OccursWhere -> OccursWhere -> Bool
compare :: OccursWhere -> OccursWhere -> Ordering
$ccompare :: OccursWhere -> OccursWhere -> Ordering
Ord, Typeable OccursWhere
Typeable OccursWhere
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> OccursWhere -> c OccursWhere)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c OccursWhere)
-> (OccursWhere -> Constr)
-> (OccursWhere -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c OccursWhere))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c OccursWhere))
-> ((forall b. Data b => b -> b) -> OccursWhere -> OccursWhere)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> OccursWhere -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> OccursWhere -> r)
-> (forall u. (forall d. Data d => d -> u) -> OccursWhere -> [u])
-> (forall u.
    Nat -> (forall d. Data d => d -> u) -> OccursWhere -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere)
-> Data OccursWhere
OccursWhere -> DataType
OccursWhere -> Constr
(forall b. Data b => b -> b) -> OccursWhere -> OccursWhere
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. Nat -> (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. Nat -> (forall d. Data d => d -> u) -> OccursWhere -> u
forall u. (forall d. Data d => d -> u) -> OccursWhere -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OccursWhere
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OccursWhere -> c OccursWhere
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OccursWhere)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c OccursWhere)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
gmapQi :: forall u. Nat -> (forall d. Data d => d -> u) -> OccursWhere -> u
$cgmapQi :: forall u. Nat -> (forall d. Data d => d -> u) -> OccursWhere -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> OccursWhere -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> OccursWhere -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
gmapT :: (forall b. Data b => b -> b) -> OccursWhere -> OccursWhere
$cgmapT :: (forall b. Data b => b -> b) -> OccursWhere -> OccursWhere
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c OccursWhere)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c OccursWhere)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OccursWhere)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OccursWhere)
dataTypeOf :: OccursWhere -> DataType
$cdataTypeOf :: OccursWhere -> DataType
toConstr :: OccursWhere -> Constr
$ctoConstr :: OccursWhere -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OccursWhere
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OccursWhere
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OccursWhere -> c OccursWhere
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OccursWhere -> c OccursWhere
Data, (forall x. OccursWhere -> Rep OccursWhere x)
-> (forall x. Rep OccursWhere x -> OccursWhere)
-> Generic OccursWhere
forall x. Rep OccursWhere x -> OccursWhere
forall x. OccursWhere -> Rep OccursWhere x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep OccursWhere x -> OccursWhere
$cfrom :: forall x. OccursWhere -> Rep OccursWhere x
Generic)

instance NFData OccursWhere

-- | One part of the description of an occurrence.
data Where
  = LeftOfArrow
  | DefArg QName Nat -- ^ in the nth argument of a define constant
  | UnderInf         -- ^ in the principal argument of built-in ∞
  | VarArg           -- ^ as an argument to a bound variable
  | MetaArg          -- ^ as an argument of a metavariable
  | ConArgType QName -- ^ in the type of a constructor
  | IndArgType QName -- ^ in a datatype index of a constructor
  | InClause Nat     -- ^ in the nth clause of a defined function
  | Matched          -- ^ matched against in a clause of a defined function
  | IsIndex          -- ^ is an index of an inductive family
  | InDefOf QName    -- ^ in the definition of a constant
  deriving (Nat -> Where -> ShowS
[Where] -> ShowS
Where -> String
(Nat -> Where -> ShowS)
-> (Where -> String) -> ([Where] -> ShowS) -> Show Where
forall a.
(Nat -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Where] -> ShowS
$cshowList :: [Where] -> ShowS
show :: Where -> String
$cshow :: Where -> String
showsPrec :: Nat -> Where -> ShowS
$cshowsPrec :: Nat -> Where -> ShowS
Show, Where -> Where -> Bool
(Where -> Where -> Bool) -> (Where -> Where -> Bool) -> Eq Where
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Where -> Where -> Bool
$c/= :: Where -> Where -> Bool
== :: Where -> Where -> Bool
$c== :: Where -> Where -> Bool
Eq, Eq Where
Eq Where
-> (Where -> Where -> Ordering)
-> (Where -> Where -> Bool)
-> (Where -> Where -> Bool)
-> (Where -> Where -> Bool)
-> (Where -> Where -> Bool)
-> (Where -> Where -> Where)
-> (Where -> Where -> Where)
-> Ord Where
Where -> Where -> Bool
Where -> Where -> Ordering
Where -> Where -> Where
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 :: Where -> Where -> Where
$cmin :: Where -> Where -> Where
max :: Where -> Where -> Where
$cmax :: Where -> Where -> Where
>= :: Where -> Where -> Bool
$c>= :: Where -> Where -> Bool
> :: Where -> Where -> Bool
$c> :: Where -> Where -> Bool
<= :: Where -> Where -> Bool
$c<= :: Where -> Where -> Bool
< :: Where -> Where -> Bool
$c< :: Where -> Where -> Bool
compare :: Where -> Where -> Ordering
$ccompare :: Where -> Where -> Ordering
Ord, Typeable Where
Typeable Where
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Where -> c Where)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Where)
-> (Where -> Constr)
-> (Where -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Where))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Where))
-> ((forall b. Data b => b -> b) -> Where -> Where)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r)
-> (forall u. (forall d. Data d => d -> u) -> Where -> [u])
-> (forall u. Nat -> (forall d. Data d => d -> u) -> Where -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Where -> m Where)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Where -> m Where)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Where -> m Where)
-> Data Where
Where -> DataType
Where -> Constr
(forall b. Data b => b -> b) -> Where -> Where
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. Nat -> (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. Nat -> (forall d. Data d => d -> u) -> Where -> u
forall u. (forall d. Data d => d -> u) -> Where -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Where -> m Where
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Where -> m Where
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Where
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Where -> c Where
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Where)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Where)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Where -> m Where
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Where -> m Where
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Where -> m Where
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Where -> m Where
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Where -> m Where
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Where -> m Where
gmapQi :: forall u. Nat -> (forall d. Data d => d -> u) -> Where -> u
$cgmapQi :: forall u. Nat -> (forall d. Data d => d -> u) -> Where -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Where -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Where -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
gmapT :: (forall b. Data b => b -> b) -> Where -> Where
$cgmapT :: (forall b. Data b => b -> b) -> Where -> Where
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Where)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Where)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Where)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Where)
dataTypeOf :: Where -> DataType
$cdataTypeOf :: Where -> DataType
toConstr :: Where -> Constr
$ctoConstr :: Where -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Where
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Where
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Where -> c Where
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Where -> c Where
Data, (forall x. Where -> Rep Where x)
-> (forall x. Rep Where x -> Where) -> Generic Where
forall x. Rep Where x -> Where
forall x. Where -> Rep Where x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Where x -> Where
$cfrom :: forall x. Where -> Rep Where x
Generic)

instance NFData Where

-- | Subterm occurrences for positivity checking.
--   The constructors are listed in increasing information they provide:
--   @Mixed <= JustPos <= StrictPos <= GuardPos <= Unused@
--   @Mixed <= JustNeg <= Unused@.
data Occurrence
  = Mixed     -- ^ Arbitrary occurrence (positive and negative).
  | JustNeg   -- ^ Negative occurrence.
  | JustPos   -- ^ Positive occurrence, but not strictly positive.
  | StrictPos -- ^ Strictly positive occurrence.
  | GuardPos  -- ^ Guarded strictly positive occurrence (i.e., under ∞).  For checking recursive records.
  | Unused    --  ^ No occurrence.
  deriving (Typeable Occurrence
Typeable Occurrence
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Occurrence -> c Occurrence)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Occurrence)
-> (Occurrence -> Constr)
-> (Occurrence -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Occurrence))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c Occurrence))
-> ((forall b. Data b => b -> b) -> Occurrence -> Occurrence)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Occurrence -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Occurrence -> r)
-> (forall u. (forall d. Data d => d -> u) -> Occurrence -> [u])
-> (forall u.
    Nat -> (forall d. Data d => d -> u) -> Occurrence -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence)
-> Data Occurrence
Occurrence -> DataType
Occurrence -> Constr
(forall b. Data b => b -> b) -> Occurrence -> Occurrence
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. Nat -> (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. Nat -> (forall d. Data d => d -> u) -> Occurrence -> u
forall u. (forall d. Data d => d -> u) -> Occurrence -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Occurrence -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Occurrence -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Occurrence
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Occurrence -> c Occurrence
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Occurrence)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Occurrence)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
gmapQi :: forall u. Nat -> (forall d. Data d => d -> u) -> Occurrence -> u
$cgmapQi :: forall u. Nat -> (forall d. Data d => d -> u) -> Occurrence -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Occurrence -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Occurrence -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Occurrence -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Occurrence -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Occurrence -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Occurrence -> r
gmapT :: (forall b. Data b => b -> b) -> Occurrence -> Occurrence
$cgmapT :: (forall b. Data b => b -> b) -> Occurrence -> Occurrence
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Occurrence)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Occurrence)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Occurrence)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Occurrence)
dataTypeOf :: Occurrence -> DataType
$cdataTypeOf :: Occurrence -> DataType
toConstr :: Occurrence -> Constr
$ctoConstr :: Occurrence -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Occurrence
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Occurrence
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Occurrence -> c Occurrence
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Occurrence -> c Occurrence
Data, Nat -> Occurrence -> ShowS
[Occurrence] -> ShowS
Occurrence -> String
(Nat -> Occurrence -> ShowS)
-> (Occurrence -> String)
-> ([Occurrence] -> ShowS)
-> Show Occurrence
forall a.
(Nat -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Occurrence] -> ShowS
$cshowList :: [Occurrence] -> ShowS
show :: Occurrence -> String
$cshow :: Occurrence -> String
showsPrec :: Nat -> Occurrence -> ShowS
$cshowsPrec :: Nat -> Occurrence -> ShowS
Show, Occurrence -> Occurrence -> Bool
(Occurrence -> Occurrence -> Bool)
-> (Occurrence -> Occurrence -> Bool) -> Eq Occurrence
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Occurrence -> Occurrence -> Bool
$c/= :: Occurrence -> Occurrence -> Bool
== :: Occurrence -> Occurrence -> Bool
$c== :: Occurrence -> Occurrence -> Bool
Eq, Eq Occurrence
Eq Occurrence
-> (Occurrence -> Occurrence -> Ordering)
-> (Occurrence -> Occurrence -> Bool)
-> (Occurrence -> Occurrence -> Bool)
-> (Occurrence -> Occurrence -> Bool)
-> (Occurrence -> Occurrence -> Bool)
-> (Occurrence -> Occurrence -> Occurrence)
-> (Occurrence -> Occurrence -> Occurrence)
-> Ord Occurrence
Occurrence -> Occurrence -> Bool
Occurrence -> Occurrence -> Ordering
Occurrence -> Occurrence -> Occurrence
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 :: Occurrence -> Occurrence -> Occurrence
$cmin :: Occurrence -> Occurrence -> Occurrence
max :: Occurrence -> Occurrence -> Occurrence
$cmax :: Occurrence -> Occurrence -> Occurrence
>= :: Occurrence -> Occurrence -> Bool
$c>= :: Occurrence -> Occurrence -> Bool
> :: Occurrence -> Occurrence -> Bool
$c> :: Occurrence -> Occurrence -> Bool
<= :: Occurrence -> Occurrence -> Bool
$c<= :: Occurrence -> Occurrence -> Bool
< :: Occurrence -> Occurrence -> Bool
$c< :: Occurrence -> Occurrence -> Bool
compare :: Occurrence -> Occurrence -> Ordering
$ccompare :: Occurrence -> Occurrence -> Ordering
Ord, Nat -> Occurrence
Occurrence -> Nat
Occurrence -> [Occurrence]
Occurrence -> Occurrence
Occurrence -> Occurrence -> [Occurrence]
Occurrence -> Occurrence -> Occurrence -> [Occurrence]
(Occurrence -> Occurrence)
-> (Occurrence -> Occurrence)
-> (Nat -> Occurrence)
-> (Occurrence -> Nat)
-> (Occurrence -> [Occurrence])
-> (Occurrence -> Occurrence -> [Occurrence])
-> (Occurrence -> Occurrence -> [Occurrence])
-> (Occurrence -> Occurrence -> Occurrence -> [Occurrence])
-> Enum Occurrence
forall a.
(a -> a)
-> (a -> a)
-> (Nat -> a)
-> (a -> Nat)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Occurrence -> Occurrence -> Occurrence -> [Occurrence]
$cenumFromThenTo :: Occurrence -> Occurrence -> Occurrence -> [Occurrence]
enumFromTo :: Occurrence -> Occurrence -> [Occurrence]
$cenumFromTo :: Occurrence -> Occurrence -> [Occurrence]
enumFromThen :: Occurrence -> Occurrence -> [Occurrence]
$cenumFromThen :: Occurrence -> Occurrence -> [Occurrence]
enumFrom :: Occurrence -> [Occurrence]
$cenumFrom :: Occurrence -> [Occurrence]
fromEnum :: Occurrence -> Nat
$cfromEnum :: Occurrence -> Nat
toEnum :: Nat -> Occurrence
$ctoEnum :: Nat -> Occurrence
pred :: Occurrence -> Occurrence
$cpred :: Occurrence -> Occurrence
succ :: Occurrence -> Occurrence
$csucc :: Occurrence -> Occurrence
Enum, Occurrence
Occurrence -> Occurrence -> Bounded Occurrence
forall a. a -> a -> Bounded a
maxBound :: Occurrence
$cmaxBound :: Occurrence
minBound :: Occurrence
$cminBound :: Occurrence
Bounded)

-- Pretty instances.

instance Pretty Occurrence where
  pretty :: Occurrence -> Doc
pretty = String -> Doc
text (String -> Doc) -> (Occurrence -> String) -> Occurrence -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
    Occurrence
Unused    -> String
"_"
    Occurrence
Mixed     -> String
"*"
    Occurrence
JustNeg   -> String
"-"
    Occurrence
JustPos   -> String
"+"
    Occurrence
StrictPos -> String
"++"
    Occurrence
GuardPos  -> String
"g+"

instance Pretty Where where
  pretty :: Where -> Doc
pretty = \case
    Where
LeftOfArrow  -> Doc
"LeftOfArrow"
    DefArg QName
q Nat
i   -> Doc
"DefArg"     Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q Doc -> Doc -> Doc
<+> Nat -> Doc
forall a. Pretty a => a -> Doc
pretty Nat
i
    Where
UnderInf     -> Doc
"UnderInf"
    Where
VarArg       -> Doc
"VarArg"
    Where
MetaArg      -> Doc
"MetaArg"
    ConArgType QName
q -> Doc
"ConArgType" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q
    IndArgType QName
q -> Doc
"IndArgType" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q
    InClause Nat
i   -> Doc
"InClause"   Doc -> Doc -> Doc
<+> Nat -> Doc
forall a. Pretty a => a -> Doc
pretty Nat
i
    Where
Matched      -> Doc
"Matched"
    Where
IsIndex      -> Doc
"IsIndex"
    InDefOf QName
q    -> Doc
"InDefOf"    Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q

instance Pretty OccursWhere where
  pretty :: OccursWhere -> Doc
pretty = \case
    OccursWhere Range
_r Seq Where
ws1 Seq Where
ws2 ->
      Doc
"OccursWhere _" Doc -> Doc -> Doc
<+> [Where] -> Doc
forall a. Pretty a => a -> Doc
pretty (Seq Where -> [Where]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq Where
ws1) Doc -> Doc -> Doc
<+> [Where] -> Doc
forall a. Pretty a => a -> Doc
pretty (Seq Where -> [Where]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq Where
ws2)

-- Other instances for 'Occurrence'.

instance NFData Occurrence where rnf :: Occurrence -> ()
rnf Occurrence
x = Occurrence -> () -> ()
seq Occurrence
x ()

instance KillRange Occurrence where
  killRange :: Occurrence -> Occurrence
killRange = Occurrence -> Occurrence
forall a. a -> a
id

-- | 'Occurrence' is a complete lattice with least element 'Mixed'
--   and greatest element 'Unused'.
--
--   It forms a commutative semiring where 'oplus' is meet (glb)
--   and 'otimes' is composition. Both operations are idempotent.
--
--   For 'oplus', 'Unused' is neutral (zero) and 'Mixed' is dominant.
--   For 'otimes', 'StrictPos' is neutral (one) and 'Unused' is dominant.

instance SemiRing Occurrence where
  ozero :: Occurrence
ozero = Occurrence
Unused
  oone :: Occurrence
oone  = Occurrence
StrictPos

  oplus :: Occurrence -> Occurrence -> Occurrence
oplus Occurrence
Mixed Occurrence
_           = Occurrence
Mixed     -- dominant
  oplus Occurrence
_ Occurrence
Mixed           = Occurrence
Mixed
  oplus Occurrence
Unused Occurrence
o          = Occurrence
o         -- neutral
  oplus Occurrence
o Occurrence
Unused          = Occurrence
o
  oplus Occurrence
JustNeg  Occurrence
JustNeg  = Occurrence
JustNeg
  oplus Occurrence
JustNeg  Occurrence
o        = Occurrence
Mixed     -- negative and any form of positve
  oplus Occurrence
o        Occurrence
JustNeg  = Occurrence
Mixed
  oplus Occurrence
GuardPos Occurrence
o        = Occurrence
o         -- second-rank neutral
  oplus Occurrence
o Occurrence
GuardPos        = Occurrence
o
  oplus Occurrence
StrictPos Occurrence
o       = Occurrence
o         -- third-rank neutral
  oplus Occurrence
o Occurrence
StrictPos       = Occurrence
o
  oplus Occurrence
JustPos Occurrence
JustPos   = Occurrence
JustPos

  otimes :: Occurrence -> Occurrence -> Occurrence
otimes Occurrence
Unused Occurrence
_            = Occurrence
Unused     -- dominant
  otimes Occurrence
_ Occurrence
Unused            = Occurrence
Unused
  otimes Occurrence
Mixed Occurrence
_             = Occurrence
Mixed      -- second-rank dominance
  otimes Occurrence
_ Occurrence
Mixed             = Occurrence
Mixed
  otimes Occurrence
JustNeg Occurrence
JustNeg     = Occurrence
JustPos
  otimes Occurrence
JustNeg Occurrence
_           = Occurrence
JustNeg    -- third-rank dominance
  otimes Occurrence
_ Occurrence
JustNeg           = Occurrence
JustNeg
  otimes Occurrence
JustPos Occurrence
_           = Occurrence
JustPos    -- fourth-rank dominance
  otimes Occurrence
_ Occurrence
JustPos           = Occurrence
JustPos
  otimes Occurrence
GuardPos Occurrence
_          = Occurrence
GuardPos   -- _ `elem` [StrictPos, GuardPos]
  otimes Occurrence
_ Occurrence
GuardPos          = Occurrence
GuardPos
  otimes Occurrence
StrictPos Occurrence
StrictPos = Occurrence
StrictPos  -- neutral

instance StarSemiRing Occurrence where
  ostar :: Occurrence -> Occurrence
ostar Occurrence
Mixed     = Occurrence
Mixed
  ostar Occurrence
JustNeg   = Occurrence
Mixed
  ostar Occurrence
JustPos   = Occurrence
JustPos
  ostar Occurrence
StrictPos = Occurrence
StrictPos
  ostar Occurrence
GuardPos  = Occurrence
StrictPos
  ostar Occurrence
Unused    = Occurrence
StrictPos

instance Null Occurrence where
  empty :: Occurrence
empty = Occurrence
Unused

-- Other instances for 'OccursWhere'.

-- There is an orphan PrettyTCM instance for Seq OccursWhere in
-- Agda.TypeChecking.Positivity.

instance Sized OccursWhere where
  size :: OccursWhere -> Nat
size (OccursWhere Range
_ Seq Where
cs Seq Where
os) = Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Seq Where -> Nat
forall a. Sized a => a -> Nat
size Seq Where
cs Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Seq Where -> Nat
forall a. Sized a => a -> Nat
size Seq Where
os

-- | The map contains bindings of the form @bound |-> ess@, satisfying
-- the following property: for every non-empty list @w@,
-- @'foldr1' 'otimes' w '<=' bound@ iff
-- @'or' [ 'all' every w '&&' 'any' some w | (every, some) <- ess ]@.

boundToEverySome ::
  Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
boundToEverySome :: Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
boundToEverySome = ([(Occurrence -> Bool, Occurrence -> Bool)]
 -> [(Occurrence -> Bool, Occurrence -> Bool)]
 -> [(Occurrence -> Bool, Occurrence -> Bool)])
-> [(Occurrence, [(Occurrence -> Bool, Occurrence -> Bool)])]
-> Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith [(Occurrence -> Bool, Occurrence -> Bool)]
-> [(Occurrence -> Bool, Occurrence -> Bool)]
-> [(Occurrence -> Bool, Occurrence -> Bool)]
forall a. HasCallStack => a
__IMPOSSIBLE__
  [ ( Occurrence
JustPos
    , [((Occurrence -> Occurrence -> Bool
forall a. Eq a => a -> a -> Bool
/= Occurrence
Unused), (Occurrence -> [Occurrence] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Occurrence
Mixed, Occurrence
JustNeg, Occurrence
JustPos]))]
    )
  , ( Occurrence
StrictPos
    , [ ((Occurrence -> Occurrence -> Bool
forall a. Eq a => a -> a -> Bool
/= Occurrence
Unused), (Occurrence -> [Occurrence] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Occurrence
Mixed, Occurrence
JustNeg, Occurrence
JustPos]))
      , ((Bool -> Bool
not (Bool -> Bool) -> (Occurrence -> Bool) -> Occurrence -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Occurrence -> [Occurrence] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Occurrence
Unused, Occurrence
GuardPos])), Bool -> Occurrence -> Bool
forall a b. a -> b -> a
const Bool
True)
      ]
    )
  , ( Occurrence
GuardPos
    , [((Occurrence -> Occurrence -> Bool
forall a. Eq a => a -> a -> Bool
/= Occurrence
Unused), Bool -> Occurrence -> Bool
forall a b. a -> b -> a
const Bool
True)]
    )
  ]

-- | @productOfEdgesInBoundedWalk occ g u v bound@ returns a value
-- distinct from 'Nothing' iff there is a walk @c@ (a list of edges)
-- in @g@, from @u@ to @v@, for which the product @'foldr1' 'otimes'
-- ('map' occ c) '<=' bound@. In this case the returned value is
-- @'Just' ('foldr1' 'otimes' c)@ for one such walk @c@.
--
-- Preconditions: @u@ and @v@ must belong to @g@, and @bound@ must
-- belong to the domain of @boundToEverySome@.

-- There is a property for this function in
-- Internal.Utils.Graph.AdjacencyMap.Unidirectional.

productOfEdgesInBoundedWalk ::
  (SemiRing e, Ord n) =>
  (e -> Occurrence) -> Graph n e -> n -> n -> Occurrence -> Maybe e
productOfEdgesInBoundedWalk :: forall e n.
(SemiRing e, Ord n) =>
(e -> Occurrence) -> Graph n e -> n -> n -> Occurrence -> Maybe e
productOfEdgesInBoundedWalk e -> Occurrence
occ Graph n e
g n
u n
v Occurrence
bound =
  case Occurrence
-> Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
-> Maybe [(Occurrence -> Bool, Occurrence -> Bool)]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Occurrence
bound Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
boundToEverySome of
    Maybe [(Occurrence -> Bool, Occurrence -> Bool)]
Nothing  -> Maybe e
forall a. HasCallStack => a
__IMPOSSIBLE__
    Just [(Occurrence -> Bool, Occurrence -> Bool)]
ess ->
      case [Maybe [Edge n e]] -> Maybe [Edge n e]
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ (Edge n e -> Bool)
-> (Edge n e -> Bool) -> Graph n e -> n -> n -> Maybe [Edge n e]
forall n e.
Ord n =>
(Edge n e -> Bool)
-> (Edge n e -> Bool) -> Graph n e -> n -> n -> Maybe [Edge n e]
Graph.walkSatisfying
                    (Occurrence -> Bool
every (Occurrence -> Bool)
-> (Edge n e -> Occurrence) -> Edge n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Occurrence
occ (e -> Occurrence) -> (Edge n e -> e) -> Edge n e -> Occurrence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Edge n e -> e
forall n e. Edge n e -> e
Graph.label)
                    (Occurrence -> Bool
some (Occurrence -> Bool)
-> (Edge n e -> Occurrence) -> Edge n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Occurrence
occ (e -> Occurrence) -> (Edge n e -> e) -> Edge n e -> Occurrence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Edge n e -> e
forall n e. Edge n e -> e
Graph.label)
                    Graph n e
g n
u n
v
                | (Occurrence -> Bool
every, Occurrence -> Bool
some) <- [(Occurrence -> Bool, Occurrence -> Bool)]
ess
                ] of
        Just es :: [Edge n e]
es@(Edge n e
_ : [Edge n e]
_) -> e -> Maybe e
forall a. a -> Maybe a
Just ((e -> e -> e) -> [e] -> e
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 e -> e -> e
forall a. SemiRing a => a -> a -> a
otimes ((Edge n e -> e) -> [Edge n e] -> [e]
forall a b. (a -> b) -> [a] -> [b]
map Edge n e -> e
forall n e. Edge n e -> e
Graph.label [Edge n e]
es))
        Just []         -> Maybe e
forall a. HasCallStack => a
__IMPOSSIBLE__
        Maybe [Edge n e]
Nothing         -> Maybe e
forall a. Maybe a
Nothing