-- | Occurrences.

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

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.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
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
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
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, 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
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
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
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, 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 (Nat -> Occurrence -> ShowS
[Occurrence] -> ShowS
Occurrence -> String
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
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
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]
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
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 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
<+> forall a. Pretty a => a -> Doc
pretty QName
q Doc -> Doc -> 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
<+> forall a. Pretty a => a -> Doc
pretty QName
q
    IndArgType QName
q -> Doc
"IndArgType" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty QName
q
    InClause Nat
i   -> Doc
"InClause"   Doc -> Doc -> 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
<+> 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. Pretty a => a -> Doc
pretty (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq Where
ws1) Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty (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 = seq :: forall a b. a -> b -> b
seq Occurrence
x ()

instance KillRange Occurrence where
  killRange :: Occurrence -> Occurrence
killRange = 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 forall a. Num a => a -> a -> a
+ forall a. Sized a => a -> Nat
size Seq Where
cs forall a. Num a => a -> a -> a
+ 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 = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. HasCallStack => a
__IMPOSSIBLE__
  [ ( Occurrence
JustPos
    , [((forall a. Eq a => a -> a -> Bool
/= Occurrence
Unused), (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Occurrence
Mixed, Occurrence
JustNeg, Occurrence
JustPos]))]
    )
  , ( Occurrence
StrictPos
    , [ ((forall a. Eq a => a -> a -> Bool
/= Occurrence
Unused), (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Occurrence
Mixed, Occurrence
JustNeg, Occurrence
JustPos]))
      , ((Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Occurrence
Unused, Occurrence
GuardPos])), forall a b. a -> b -> a
const Bool
True)
      ]
    )
  , ( Occurrence
GuardPos
    , [((forall a. Eq a => a -> a -> Bool
/= Occurrence
Unused), 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 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  -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Just [(Occurrence -> Bool, Occurrence -> Bool)]
ess ->
      case forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Occurrence
occ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. Edge n e -> e
Graph.label)
                    (Occurrence -> Bool
some forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Occurrence
occ forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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]
_) -> forall a. a -> Maybe a
Just (forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 forall a. SemiRing a => a -> a -> a
otimes (forall a b. (a -> b) -> [a] -> [b]
map forall n e. Edge n e -> e
Graph.label [Edge n e]
es))
        Just []         -> forall a. HasCallStack => a
__IMPOSSIBLE__
        Maybe [Edge n e]
Nothing         -> forall a. Maybe a
Nothing