    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | Occurrences.

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

    import Prelude hiding (null)

    import Control.DeepSeq
    import Control.Monad

    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.Common.Pretty
    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.List1 (List1)
    import Agda.Utils.Null
    import Agda.Utils.SemiRing
    import Agda.Utils.Size

    import Agda.Utils.Impossible

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

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

    -- | List of polarities stemming from POLARITY pragma.
    type PragmaPolarities = List1 (Ranged Occurrence)

    -- | 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
    $cshowsPrec :: Int -> OccursWhere -> ShowS
    showsPrec :: Int -> OccursWhere -> ShowS
    $cshow :: OccursWhere -> String
    show :: OccursWhere -> String
    $cshowList :: [OccursWhere] -> ShowS
    showList :: [OccursWhere] -> ShowS
    Show, OccursWhere -> OccursWhere -> Bool
    (OccursWhere -> OccursWhere -> Bool)
    -> (OccursWhere -> OccursWhere -> Bool) -> Eq OccursWhere
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: OccursWhere -> OccursWhere -> Bool
    == :: OccursWhere -> OccursWhere -> Bool
    $c/= :: OccursWhere -> OccursWhere -> Bool
    /= :: 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
    $ccompare :: OccursWhere -> OccursWhere -> Ordering
    compare :: OccursWhere -> OccursWhere -> Ordering
    $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
    >= :: OccursWhere -> OccursWhere -> Bool
    $cmax :: OccursWhere -> OccursWhere -> OccursWhere
    max :: OccursWhere -> OccursWhere -> OccursWhere
    $cmin :: OccursWhere -> OccursWhere -> OccursWhere
    min :: OccursWhere -> OccursWhere -> OccursWhere
    Ord, (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
    $cfrom :: forall x. OccursWhere -> Rep OccursWhere x
    from :: forall x. OccursWhere -> Rep OccursWhere x
    $cto :: forall x. Rep OccursWhere x -> OccursWhere
    to :: forall x. Rep OccursWhere x -> OccursWhere
    Generic)

    instance NFData OccursWhere

    instance Null OccursWhere where
      empty :: OccursWhere
    empty = Range -> Seq Where -> Seq Where -> OccursWhere
    OccursWhere Range
    forall a. Null a => a
    empty Seq Where
    forall a. Null a => a
    empty Seq Where
    forall a. Null a => a
    empty
      null :: OccursWhere -> Bool
    null (OccursWhere Range
    r Seq Where
    wh1 Seq Where
    wh2) = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and [ Range -> Bool
    forall a. Null a => a -> Bool
    null Range
    r, Seq Where -> Bool
    forall a. Null a => a -> Bool
    null Seq Where
    wh1, Seq Where -> Bool
    forall a. Null a => a -> Bool
    null Seq Where
    wh2 ]

    -- | 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 Occurrence Nat  -- ^ as an argument to a bound variable.
                               --   The polarity, if given, is the polarity of
                               --   the argument the occurence is in
      | MetaArg                -- ^ as an argument of a metavariable
      | ConArgType QName       -- ^ in the type of a constructor
      | IndArgType QName       -- ^ in a datatype index of a constructor
      | ConEndpoint QName
                               -- ^ in an endpoint of a higher 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
    $cshowsPrec :: Int -> Where -> ShowS
    showsPrec :: Int -> Where -> ShowS
    $cshow :: Where -> String
    show :: Where -> String
    $cshowList :: [Where] -> ShowS
    showList :: [Where] -> ShowS
    Show, Where -> Where -> Bool
    (Where -> Where -> Bool) -> (Where -> Where -> Bool) -> Eq Where
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Where -> Where -> Bool
    == :: Where -> Where -> Bool
    $c/= :: Where -> Where -> Bool
    /= :: 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
    $ccompare :: Where -> Where -> Ordering
    compare :: Where -> Where -> Ordering
    $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
    >= :: Where -> Where -> Bool
    $cmax :: Where -> Where -> Where
    max :: Where -> Where -> Where
    $cmin :: Where -> Where -> Where
    min :: Where -> Where -> Where
    Ord, (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
    $cfrom :: forall x. Where -> Rep Where x
    from :: forall x. Where -> Rep Where x
    $cto :: forall x. Rep Where x -> Where
    to :: forall x. Rep Where x -> Where
    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 (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
    $cshowsPrec :: Int -> Occurrence -> ShowS
    showsPrec :: Int -> Occurrence -> ShowS
    $cshow :: Occurrence -> String
    show :: Occurrence -> String
    $cshowList :: [Occurrence] -> ShowS
    showList :: [Occurrence] -> ShowS
    Show, Occurrence -> Occurrence -> Bool
    (Occurrence -> Occurrence -> Bool)
    -> (Occurrence -> Occurrence -> Bool) -> Eq Occurrence
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Occurrence -> Occurrence -> Bool
    == :: Occurrence -> Occurrence -> Bool
    $c/= :: Occurrence -> Occurrence -> Bool
    /= :: 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
    $ccompare :: Occurrence -> Occurrence -> Ordering
    compare :: Occurrence -> Occurrence -> Ordering
    $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
    >= :: Occurrence -> Occurrence -> Bool
    $cmax :: Occurrence -> Occurrence -> Occurrence
    max :: Occurrence -> Occurrence -> Occurrence
    $cmin :: Occurrence -> Occurrence -> Occurrence
    min :: Occurrence -> Occurrence -> 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
    $csucc :: Occurrence -> Occurrence
    succ :: Occurrence -> Occurrence
    $cpred :: Occurrence -> Occurrence
    pred :: Occurrence -> Occurrence
    $ctoEnum :: Int -> Occurrence
    toEnum :: Int -> Occurrence
    $cfromEnum :: Occurrence -> Int
    fromEnum :: Occurrence -> Int
    $cenumFrom :: Occurrence -> [Occurrence]
    enumFrom :: Occurrence -> [Occurrence]
    $cenumFromThen :: Occurrence -> Occurrence -> [Occurrence]
    enumFromThen :: Occurrence -> Occurrence -> [Occurrence]
    $cenumFromTo :: Occurrence -> Occurrence -> [Occurrence]
    enumFromTo :: Occurrence -> Occurrence -> [Occurrence]
    $cenumFromThenTo :: Occurrence -> Occurrence -> Occurrence -> [Occurrence]
    enumFromThenTo :: Occurrence -> Occurrence -> Occurrence -> [Occurrence]
    Enum, Occurrence
    Occurrence -> Occurrence -> Bounded Occurrence
    forall a. a -> a -> Bounded a
    $cminBound :: Occurrence
    minBound :: Occurrence
    $cmaxBound :: Occurrence
    maxBound :: Occurrence
    Bounded)

    -- Pretty instances.

    instance Pretty Occurrence where
      pretty :: Occurrence -> Doc
    pretty = String -> Doc
    forall a. String -> Doc a
    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 Int
    i   -> Doc
    "DefArg"     Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    q Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Int -> Doc
    forall a. Pretty a => a -> Doc
    pretty Int
    i
        Where
    UnderInf     -> Doc
    "UnderInf"
        VarArg Occurrence
    k Int
    i   -> Doc
    "VarArg" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Occurrence -> Doc
    forall a. Pretty a => a -> Doc
    pretty Occurrence
    k Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Int -> Doc
    forall a. Pretty a => a -> Doc
    pretty Int
    i
        Where
    MetaArg      -> Doc
    "MetaArg"
        ConArgType QName
    q -> Doc
    "ConArgType" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    q
        IndArgType QName
    q -> Doc
    "IndArgType" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    q
        ConEndpoint QName
    q
                     -> Doc
    "ConEndpoint" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    q
        InClause Int
    i   -> Doc
    "InClause"   Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Int -> Doc
    forall a. Pretty a => a -> Doc
    pretty Int
    i
        Where
    Matched      -> Doc
    "Matched"
        Where
    IsIndex      -> Doc
    "IsIndex"
        InDefOf QName
    q    -> Doc
    "InDefOf"    Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> 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
    forall a. Doc a -> Doc a -> Doc a
    <+> [Where] -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Seq Where -> [Where]
    forall a. Seq a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList Seq Where
    ws1) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Where] -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Seq Where -> [Where]
    forall a. Seq a -> [a]
    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 -> () -> ()
    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 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 -> Int
    size    (OccursWhere Range
    _ Seq Where
    cs Seq Where
    os) = Int
    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
      natSize :: OccursWhere -> Peano
    natSize (OccursWhere Range
    _ Seq Where
    cs Seq Where
    os) = Peano
    1 Peano -> Peano -> Peano
    forall a. Num a => a -> a -> a
    + Seq Where -> Peano
    forall a. Sized a => a -> Peano
    natSize Seq Where
    cs Peano -> Peano -> Peano
    forall a. Num a => a -> a -> a
    + Seq Where -> Peano
    forall a. Sized a => a -> Peano
    natSize 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 a. Eq a => a -> [a] -> 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 a. Eq a => a -> [a] -> 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 a. Eq a => a -> [a] -> 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 a. (a -> a -> a) -> [a] -> a
    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

    modalPolarityToOccurrence :: ModalPolarity -> Occurrence
    modalPolarityToOccurrence :: ModalPolarity -> Occurrence
    modalPolarityToOccurrence = \case
      ModalPolarity
    UnusedPolarity -> Occurrence
    Unused
      ModalPolarity
    StrictlyPositive -> Occurrence
    StrictPos
      ModalPolarity
    Positive -> Occurrence
    JustPos
      ModalPolarity
    Negative -> Occurrence
    JustNeg
      ModalPolarity
    MixedPolarity -> Occurrence
    Mixed