{-# OPTIONS_GHC -Wunused-imports #-}

-- | Occurrences.

module Agda.TypeChecking.Positivity.Occurrence where

import Prelude hiding (null)
import Control.DeepSeq
import Data.Hashable

import Agda.Syntax.Common
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common.Pretty qualified as P
import Agda.Syntax.Position
import Agda.Utils.Hash
import Agda.Utils.List1 (List1)
import Agda.Utils.Null
import Agda.Utils.SemiRing


-- Occurrences
----------------------------------------------------------------------------------------------------

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

-- | 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)

instance P.Pretty Occurrence where
  pretty :: Occurrence -> Doc
pretty = String -> Doc
forall a. String -> Doc a
P.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 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

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

-- Paths to occurrences
----------------------------------------------------------------------------------------------------

data OccursPath
  = Root
  | LeftOfArrow !OccursPath
  | DefArg !OccursPath !QName !Nat      -- ^ in the nth argument of a defined constant
  | MutDefArg !OccursPath !QName !Nat   -- ^ in the nth argument of a def in the current mutual block.
                                        --   (def given by Int index in the block)
  | UnderInf !OccursPath                -- ^ in the principal argument of built-in ∞
  | VarArg !OccursPath !Nat !Occurrence -- ^ as an argument to a bound variable with given polarity.
                                        --   The polarity is only used for warning printing.
  | MetaArg !OccursPath                 -- ^ as an argument of a metavariable
  | ConArgType !OccursPath !QName       -- ^ in the type of a constructor
  | IndArgType !OccursPath !QName       -- ^ in a datatype index of a constructor
  | ConEndpoint !OccursPath !QName      -- ^ in an endpoint of a higher constructor
  | InClause !OccursPath !Nat           -- ^ in the nth clause of a defined function
  | Matched !OccursPath                 -- ^ matched against in a clause of a defined function
  | InIndex !OccursPath                 -- ^ is an index of an inductive family
  | InDefOf !OccursPath !QName          -- ^ in the definition of a constant
  deriving OccursPath -> OccursPath -> Bool
(OccursPath -> OccursPath -> Bool)
-> (OccursPath -> OccursPath -> Bool) -> Eq OccursPath
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: OccursPath -> OccursPath -> Bool
== :: OccursPath -> OccursPath -> Bool
$c/= :: OccursPath -> OccursPath -> Bool
/= :: OccursPath -> OccursPath -> Bool
Eq

instance NFData OccursPath where
  rnf :: OccursPath -> ()
rnf OccursPath
x = OccursPath -> () -> ()
forall a b. a -> b -> b
seq OccursPath
x ()

instance Show OccursPath where
  show :: OccursPath -> String
show OccursPath
p = OccursPath -> ShowS
go OccursPath
p [] where
    go :: OccursPath -> ShowS
go OccursPath
p String
acc = case OccursPath
p of
      OccursPath
Root            -> String
acc
      LeftOfArrow OccursPath
p   -> OccursPath -> ShowS
go OccursPath
p ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
" InLeftOfArrow" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
acc
      DefArg OccursPath
p QName
q Int
i    -> OccursPath -> ShowS
go OccursPath
p ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
" InDefArg "      String -> ShowS
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
P.prettyShow QName
q String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Pretty a => a -> String
P.prettyShow Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
acc
      MutDefArg OccursPath
p QName
q Int
i -> OccursPath -> ShowS
go OccursPath
p ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
" InMutDefArg "   String -> ShowS
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
P.prettyShow QName
q String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Pretty a => a -> String
P.prettyShow Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
acc
      UnderInf OccursPath
p      -> OccursPath -> ShowS
go OccursPath
p ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
" InUnderInf" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
acc
      VarArg OccursPath
p Int
i Occurrence
o    -> OccursPath -> ShowS
go OccursPath
p ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
" InVarArg "      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Pretty a => a -> String
P.prettyShow Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Occurrence -> String
forall a. Pretty a => a -> String
P.prettyShow Occurrence
o String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
acc
      MetaArg OccursPath
p       -> OccursPath -> ShowS
go OccursPath
p ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
" InMetaArg" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
acc
      ConArgType OccursPath
p QName
q  -> OccursPath -> ShowS
go OccursPath
p ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
" InConArgType "  String -> ShowS
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
P.prettyShow QName
q String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
acc
      IndArgType OccursPath
p QName
q  -> OccursPath -> ShowS
go OccursPath
p ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
" InIndArgType "  String -> ShowS
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
P.prettyShow QName
q String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
acc
      ConEndpoint OccursPath
p QName
q -> OccursPath -> ShowS
go OccursPath
p ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
" InConEndpoint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
P.prettyShow QName
q String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
acc
      InClause OccursPath
p Int
i    -> OccursPath -> ShowS
go OccursPath
p ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
" InClause "    String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Pretty a => a -> String
P.prettyShow Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
acc
      Matched OccursPath
p       -> OccursPath -> ShowS
go OccursPath
p ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
" Matched" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
acc
      InIndex OccursPath
p       -> OccursPath -> ShowS
go OccursPath
p ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
" InIndex" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
acc
      InDefOf OccursPath
p QName
q     -> OccursPath -> ShowS
go OccursPath
p ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
" InDefOf " String -> ShowS
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
P.prettyShow QName
q String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
acc

instance P.Pretty OccursPath where
  pretty :: OccursPath -> Doc
pretty = String -> Doc
forall a. String -> Doc a
P.text (String -> Doc) -> (OccursPath -> String) -> OccursPath -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccursPath -> String
forall a. Show a => a -> String
show

data OccursWhere = OccursWhere !Range !OccursPath
  deriving (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, 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)

instance P.Pretty OccursWhere where
  pretty :: OccursWhere -> Doc
pretty (OccursWhere Range' SrcFile
x OccursPath
y) = Doc
"OccursWhere" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> Range' SrcFile -> Doc
forall a. Pretty a => a -> Doc
P.pretty Range' SrcFile
x Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> OccursPath -> Doc
forall a. Pretty a => a -> Doc
P.pretty OccursPath
y


-- Occurrence graph nodes
----------------------------------------------------------------------------------------------------

data Node
  = DefNode QName       -- ^ Definition site of a mutual definition
  | ArgNode QName Int   -- ^ Occurrence of the nth definition argument inside
                        --   the definition.
  deriving (Node -> Node -> Bool
(Node -> Node -> Bool) -> (Node -> Node -> Bool) -> Eq Node
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Node -> Node -> Bool
== :: Node -> Node -> Bool
$c/= :: Node -> Node -> Bool
/= :: Node -> Node -> Bool
Eq, Eq Node
Eq Node =>
(Node -> Node -> Ordering)
-> (Node -> Node -> Bool)
-> (Node -> Node -> Bool)
-> (Node -> Node -> Bool)
-> (Node -> Node -> Bool)
-> (Node -> Node -> Node)
-> (Node -> Node -> Node)
-> Ord Node
Node -> Node -> Bool
Node -> Node -> Ordering
Node -> Node -> Node
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 :: Node -> Node -> Ordering
compare :: Node -> Node -> Ordering
$c< :: Node -> Node -> Bool
< :: Node -> Node -> Bool
$c<= :: Node -> Node -> Bool
<= :: Node -> Node -> Bool
$c> :: Node -> Node -> Bool
> :: Node -> Node -> Bool
$c>= :: Node -> Node -> Bool
>= :: Node -> Node -> Bool
$cmax :: Node -> Node -> Node
max :: Node -> Node -> Node
$cmin :: Node -> Node -> Node
min :: Node -> Node -> Node
Ord, Int -> Node -> ShowS
[Node] -> ShowS
Node -> String
(Int -> Node -> ShowS)
-> (Node -> String) -> ([Node] -> ShowS) -> Show Node
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Node -> ShowS
showsPrec :: Int -> Node -> ShowS
$cshow :: Node -> String
show :: Node -> String
$cshowList :: [Node] -> ShowS
showList :: [Node] -> ShowS
Show)

instance Hashable Node where
  hashWithSalt :: Int -> Node -> Int
hashWithSalt Int
h = \case
    DefNode QName
x   -> Int
h Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 Int -> QName -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` QName
x
    ArgNode QName
x Int
i -> Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral
                    (Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
h Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2 Int -> QName -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` QName
x) Word -> Word -> Word
`combineWord` Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i)

instance P.Pretty Node where
  pretty :: Node -> Doc
pretty = \case
    DefNode QName
q   -> QName -> Doc
forall a. Pretty a => a -> Doc
P.pretty QName
q
    ArgNode QName
q Int
i -> QName -> Doc
forall a. Pretty a => a -> Doc
P.pretty QName
q Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
forall a. String -> Doc a
P.text (String
"." String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)

-- Occurrence graph edges
----------------------------------------------------------------------------------------------------

data Edge a = Edge !Occurrence !a
  deriving (Edge a -> Edge a -> Bool
(Edge a -> Edge a -> Bool)
-> (Edge a -> Edge a -> Bool) -> Eq (Edge a)
forall a. Eq a => Edge a -> Edge a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Edge a -> Edge a -> Bool
== :: Edge a -> Edge a -> Bool
$c/= :: forall a. Eq a => Edge a -> Edge a -> Bool
/= :: Edge a -> Edge a -> Bool
Eq, Eq (Edge a)
Eq (Edge a) =>
(Edge a -> Edge a -> Ordering)
-> (Edge a -> Edge a -> Bool)
-> (Edge a -> Edge a -> Bool)
-> (Edge a -> Edge a -> Bool)
-> (Edge a -> Edge a -> Bool)
-> (Edge a -> Edge a -> Edge a)
-> (Edge a -> Edge a -> Edge a)
-> Ord (Edge a)
Edge a -> Edge a -> Bool
Edge a -> Edge a -> Ordering
Edge a -> Edge a -> Edge a
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
forall a. Ord a => Eq (Edge a)
forall a. Ord a => Edge a -> Edge a -> Bool
forall a. Ord a => Edge a -> Edge a -> Ordering
forall a. Ord a => Edge a -> Edge a -> Edge a
$ccompare :: forall a. Ord a => Edge a -> Edge a -> Ordering
compare :: Edge a -> Edge a -> Ordering
$c< :: forall a. Ord a => Edge a -> Edge a -> Bool
< :: Edge a -> Edge a -> Bool
$c<= :: forall a. Ord a => Edge a -> Edge a -> Bool
<= :: Edge a -> Edge a -> Bool
$c> :: forall a. Ord a => Edge a -> Edge a -> Bool
> :: Edge a -> Edge a -> Bool
$c>= :: forall a. Ord a => Edge a -> Edge a -> Bool
>= :: Edge a -> Edge a -> Bool
$cmax :: forall a. Ord a => Edge a -> Edge a -> Edge a
max :: Edge a -> Edge a -> Edge a
$cmin :: forall a. Ord a => Edge a -> Edge a -> Edge a
min :: Edge a -> Edge a -> Edge a
Ord, Int -> Edge a -> ShowS
[Edge a] -> ShowS
Edge a -> String
(Int -> Edge a -> ShowS)
-> (Edge a -> String) -> ([Edge a] -> ShowS) -> Show (Edge a)
forall a. Show a => Int -> Edge a -> ShowS
forall a. Show a => [Edge a] -> ShowS
forall a. Show a => Edge a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Edge a -> ShowS
showsPrec :: Int -> Edge a -> ShowS
$cshow :: forall a. Show a => Edge a -> String
show :: Edge a -> String
$cshowList :: forall a. Show a => [Edge a] -> ShowS
showList :: [Edge a] -> ShowS
Show, (forall a b. (a -> b) -> Edge a -> Edge b)
-> (forall a b. a -> Edge b -> Edge a) -> Functor Edge
forall a b. a -> Edge b -> Edge a
forall a b. (a -> b) -> Edge a -> Edge b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Edge a -> Edge b
fmap :: forall a b. (a -> b) -> Edge a -> Edge b
$c<$ :: forall a b. a -> Edge b -> Edge a
<$ :: forall a b. a -> Edge b -> Edge a
Functor)

mergeEdges :: Edge a -> Edge a -> Edge a
mergeEdges :: forall a. Edge a -> Edge a -> Edge a
mergeEdges Edge a
_                    e :: Edge a
e@(Edge Occurrence
Mixed a
_)     = Edge a
e -- dominant
mergeEdges e :: Edge a
e@(Edge Occurrence
Mixed a
_)     Edge a
_                    = Edge a
e
mergeEdges (Edge Occurrence
Unused a
_)      Edge a
e                    = Edge a
e -- neutral
mergeEdges Edge a
e                    (Edge Occurrence
Unused a
_)      = Edge a
e
mergeEdges (Edge Occurrence
JustNeg a
_)     e :: Edge a
e@(Edge Occurrence
JustNeg a
_)   = Edge a
e
mergeEdges Edge a
_                    e :: Edge a
e@(Edge Occurrence
JustNeg a
a)   = Occurrence -> a -> Edge a
forall a. Occurrence -> a -> Edge a
Edge Occurrence
Mixed a
a
mergeEdges e :: Edge a
e@(Edge Occurrence
JustNeg a
a)   Edge a
_                    = Occurrence -> a -> Edge a
forall a. Occurrence -> a -> Edge a
Edge Occurrence
Mixed a
a
mergeEdges Edge a
_                    e :: Edge a
e@(Edge Occurrence
JustPos a
_)   = Edge a
e -- dominates strict pos.
mergeEdges e :: Edge a
e@(Edge Occurrence
JustPos a
_)   Edge a
_                    = Edge a
e
mergeEdges Edge a
_                    e :: Edge a
e@(Edge Occurrence
StrictPos a
_) = Edge a
e -- dominates 'GuardPos'
mergeEdges e :: Edge a
e@(Edge Occurrence
StrictPos a
_) Edge a
_                    = Edge a
e
mergeEdges (Edge Occurrence
GuardPos a
_)    e :: Edge a
e@(Edge Occurrence
GuardPos a
_)  = Edge a
e

instance Monoid a => SemiRing (Edge a) where
  ozero :: Edge a
ozero = Occurrence -> a -> Edge a
forall a. Occurrence -> a -> Edge a
Edge Occurrence
forall a. SemiRing a => a
ozero a
forall a. Monoid a => a
mempty
  oone :: Edge a
oone  = Occurrence -> a -> Edge a
forall a. Occurrence -> a -> Edge a
Edge Occurrence
forall a. SemiRing a => a
oone  a
forall a. Monoid a => a
mempty
  oplus :: Edge a -> Edge a -> Edge a
oplus = Edge a -> Edge a -> Edge a
forall a. Edge a -> Edge a -> Edge a
mergeEdges
  otimes :: Edge a -> Edge a -> Edge a
otimes (Edge Occurrence
o1 a
w1) (Edge Occurrence
o2 a
w2) = Occurrence -> a -> Edge a
forall a. Occurrence -> a -> Edge a
Edge (Occurrence -> Occurrence -> Occurrence
forall a. SemiRing a => a -> a -> a
otimes Occurrence
o1 Occurrence
o2) (a
w1 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
w2)