{-# LANGUAGE DeriveDataTypeable #-}


-- | 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 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 (Int -> OccursWhere -> ShowS
[OccursWhere] -> ShowS
OccursWhere -> String
(Int -> OccursWhere -> ShowS)
-> (OccursWhere -> String)
-> ([OccursWhere] -> ShowS)
-> Show OccursWhere
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OccursWhere] -> ShowS
$cshowList :: [OccursWhere] -> ShowS
show :: OccursWhere -> String
$cshow :: OccursWhere -> String
showsPrec :: Int -> OccursWhere -> ShowS
$cshowsPrec :: Int -> 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
$cp1Ord :: Eq OccursWhere
Ord, Typeable OccursWhere
DataType
Constr
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.
    Int -> (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 d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OccursWhere -> c OccursWhere
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> 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)
$cOccursWhere :: Constr
$tOccursWhere :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> OccursWhere -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> OccursWhere -> u
gmapQ :: (forall d. Data d => d -> u) -> OccursWhere -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> OccursWhere -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable OccursWhere
Data)

-- | 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 (Int -> Where -> ShowS
[Where] -> ShowS
Where -> String
(Int -> Where -> ShowS)
-> (Where -> String) -> ([Where] -> ShowS) -> Show Where
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Where] -> ShowS
$cshowList :: [Where] -> ShowS
show :: Where -> String
$cshow :: Where -> String
showsPrec :: Int -> Where -> ShowS
$cshowsPrec :: Int -> 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
$cp1Ord :: Eq Where
Ord, Typeable Where
DataType
Constr
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. Int -> (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 d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Where -> c Where
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> 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)
$cInDefOf :: Constr
$cIsIndex :: Constr
$cMatched :: Constr
$cInClause :: Constr
$cIndArgType :: Constr
$cConArgType :: Constr
$cMetaArg :: Constr
$cVarArg :: Constr
$cUnderInf :: Constr
$cDefArg :: Constr
$cLeftOfArrow :: Constr
$tWhere :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Where -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Where -> u
gmapQ :: (forall d. Data d => d -> u) -> Where -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Where -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Where
Data)

-- | 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
DataType
Constr
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.
    Int -> (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 d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Occurrence -> c Occurrence
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> 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)
$cUnused :: Constr
$cGuardPos :: Constr
$cStrictPos :: Constr
$cJustPos :: Constr
$cJustNeg :: Constr
$cMixed :: Constr
$tOccurrence :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Occurrence -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Occurrence -> u
gmapQ :: (forall d. Data d => d -> u) -> Occurrence -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Occurrence -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Occurrence
Data, Int -> Occurrence -> ShowS
[Occurrence] -> ShowS
Occurrence -> String
(Int -> Occurrence -> ShowS)
-> (Occurrence -> String)
-> ([Occurrence] -> ShowS)
-> Show Occurrence
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Occurrence] -> ShowS
$cshowList :: [Occurrence] -> ShowS
show :: Occurrence -> String
$cshow :: Occurrence -> String
showsPrec :: Int -> Occurrence -> ShowS
$cshowsPrec :: Int -> 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
$cp1Ord :: Eq Occurrence
Ord, Int -> Occurrence
Occurrence -> Int
Occurrence -> [Occurrence]
Occurrence -> Occurrence
Occurrence -> Occurrence -> [Occurrence]
Occurrence -> Occurrence -> Occurrence -> [Occurrence]
(Occurrence -> Occurrence)
-> (Occurrence -> Occurrence)
-> (Int -> Occurrence)
-> (Occurrence -> Int)
-> (Occurrence -> [Occurrence])
-> (Occurrence -> Occurrence -> [Occurrence])
-> (Occurrence -> Occurrence -> [Occurrence])
-> (Occurrence -> Occurrence -> Occurrence -> [Occurrence])
-> Enum Occurrence
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (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 -> Int
$cfromEnum :: Occurrence -> Int
toEnum :: Int -> Occurrence
$ctoEnum :: Int -> 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
    Unused    -> "_"
    Mixed     -> "*"
    JustNeg   -> "-"
    JustPos   -> "+"
    StrictPos -> "++"
    GuardPos  -> "g+"

instance Pretty Where where
  pretty :: Where -> Doc
pretty = \case
    LeftOfArrow  -> "LeftOfArrow"
    DefArg q :: QName
q i :: Int
i   -> "DefArg"     Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q Doc -> Doc -> Doc
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
i
    UnderInf     -> "UnderInf"
    VarArg       -> "VarArg"
    MetaArg      -> "MetaArg"
    ConArgType q :: QName
q -> "ConArgType" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q
    IndArgType q :: QName
q -> "IndArgType" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q
    InClause i :: Int
i   -> "InClause"   Doc -> Doc -> Doc
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
i
    Matched      -> "Matched"
    IsIndex      -> "IsIndex"
    InDefOf q :: QName
q    -> "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 _r :: Range
_r ws1 :: Seq Where
ws1 ws2 :: Seq Where
ws2 ->
      "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 x :: Occurrence
x = Occurrence -> () -> ()
forall a b. a -> b -> b
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 Mixed _           = Occurrence
Mixed     -- dominant
  oplus _ Mixed           = Occurrence
Mixed
  oplus Unused o :: Occurrence
o          = Occurrence
o         -- neutral
  oplus o :: Occurrence
o Unused          = Occurrence
o
  oplus JustNeg  JustNeg  = Occurrence
JustNeg
  oplus JustNeg  o :: Occurrence
o        = Occurrence
Mixed     -- negative and any form of positve
  oplus o :: Occurrence
o        JustNeg  = Occurrence
Mixed
  oplus GuardPos o :: Occurrence
o        = Occurrence
o         -- second-rank neutral
  oplus o :: Occurrence
o GuardPos        = Occurrence
o
  oplus StrictPos o :: Occurrence
o       = Occurrence
o         -- third-rank neutral
  oplus o :: Occurrence
o StrictPos       = Occurrence
o
  oplus JustPos JustPos   = Occurrence
JustPos

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

instance StarSemiRing Occurrence where
  ostar :: Occurrence -> Occurrence
ostar Mixed     = Occurrence
Mixed
  ostar JustNeg   = Occurrence
Mixed
  ostar JustPos   = Occurrence
JustPos
  ostar StrictPos = Occurrence
StrictPos
  ostar GuardPos  = Occurrence
StrictPos
  ostar 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 -> Int
size (OccursWhere _ cs :: Seq Where
cs os :: Seq Where
os) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Seq Where -> Int
forall a. Sized a => a -> Int
size Seq Where
cs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Seq Where -> Int
forall a. Sized a => a -> Int
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, [(Occurrence -> Bool, Occurrence -> Bool)])]
-> Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
  [ ( 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 :: (e -> Occurrence) -> Graph n e -> n -> n -> Occurrence -> Maybe e
productOfEdgesInBoundedWalk occ :: e -> Occurrence
occ g :: Graph n e
g u :: n
u v :: n
v bound :: 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
    Nothing  -> Maybe e
forall a. HasCallStack => a
__IMPOSSIBLE__
    Just ess :: [(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
                | (every :: Occurrence -> Bool
every, some :: Occurrence -> Bool
some) <- [(Occurrence -> Bool, Occurrence -> Bool)]
ess
                ] of
        Just es :: [Edge n e]
es@(_ : _) -> 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__
        Nothing         -> Maybe e
forall a. Maybe a
Nothing