{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.TypeChecking.Positivity.Warnings where

import Prelude hiding (null)

import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Control.DeepSeq

import Data.Foldable (toList, msum)
import Data.Sequence (Seq)
import GHC.Generics

import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty
import Agda.Syntax.Internal
import Agda.Syntax.Position (Range)
import Agda.TypeChecking.Positivity.Occurrence (Occurrence(..))

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

{-
András 2026-03-11: these definitions are only used to represent and render positivity warnings.
They used to be the basis of the main occurrence/positivity implementation. I rewrote the main
implementation in PR 8411 but I left the warning rendering as it is.
-}

-- | 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' SrcFile -> Seq Where -> Seq Where -> OccursWhere
OccursWhere Range' SrcFile
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' SrcFile
r Seq Where
wh1 Seq Where
wh2) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ Range' SrcFile -> Bool
forall a. Null a => a -> Bool
null Range' SrcFile
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.
  | 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
  | InIndex                -- ^ 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

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
InIndex      -> 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' SrcFile
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)

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