{-# LANGUAGE CPP #-}
{-# LANGUAGE Strict #-}
{-# LANGUAGE MagicHash #-}
{-# OPTIONS_GHC -Wno-redundant-bang-patterns #-}
{-# OPTIONS_GHC -fmax-worker-args=20 #-}

#if __GLASGOW_HASKELL__ > 902
{-# OPTIONS_GHC -fworker-wrapper-cbv #-}
#endif

{- |
Computing the occurrence graph for a mutual block. This is used to compute polarities of arguments
and to check positivity.

- We do a traversal over internal syntax.
- The occurrence graph is 'NodeMap (NodeMap Edge)', where 'NodeMap' is a mutable hashtable keyed by
  graph nodes. The outer keys are sources and the inner keys are targets. We insert edges into the
  graph during the traversal.
- An edge from source to target means that source occurs in target.
- A graph node is either 'DefNode QName', which is a definition site of a mutual name, or 'ArgNode
  QName Int', which is an argument of a mutual name, indexed left-right starting from 0.
- An edge contains an 'Occurrence', the 'Range' of the actual occurrence in the internal syntax and
  an 'OccursPath' that can be used to produce a textual warning message.

The occurrence graph is imprecise in several ways.

- We only normalize types of data constructors and don't compute anything else.
- We have at most a single edge between two nodes. We aggregate multiple actual occurrences into a
  single edge, using 'mergeEdges'.

Lastly, applications of mutual names to arguments is handled in a rather imprecise way.  See Issue
1984 for illustration:

@
mutual
  record Fun (A : Set) (B : A → Set) : Set where
    field fun : (x : A) → B x

  data U : Set where
    Π : (A : U) (B : El A → U) → U

  El : U → Set
  El (Π A B) = Fun (El A) (λ x → El (B x))
@

In this case:

- @Fun@ occurs in @El@.
- @El A@ occurs in the first argument of @Fun@.
- The first argument of @Fun@ occurs in @Fun@.

In short, when we apply a mutual name to an argument, we view that as if the argument was
__substituted__ inside the body of the mutual name definition.

Hence, @Fun@ "occurs" in @Fun@, and it does so negatively. This is kinda bogus, because @Fun@ could
be moved outside of the mutual block.

A potential fix of this issue would be to first split the mutual block into strongly connected
components based on only QName occurrences, and afterwards do the current occurrence analysis for
each sub-block.

__Immutable representation__

Instead of using the mutable hashtable, we use immutable "generic" graphs from
'Agda.Utils.Graph.AdjacencyMap.Unidirectional' for printing warnings and debug messages, and also to
define tests in internal property tests. One reason is convenience. Another reason is that the
previous (less optimized) implementation before PR 8411 used the generic graphs, and we just reuse
the old implementation for printing. See 'toGenericGraph' and 'fromGenericGraph'.
-}

module Agda.TypeChecking.Positivity.OccurrenceAnalysis (
    Node
  , pattern DefNode
  , pattern ArgNode
  , Edge(..)
  , type OccGraph
  , buildOccurrenceGraph
  , stronglyConnComp
  , transitiveOccurrence
  , adjacencyList
  , lookupNode
  , toGenericGraph
  , fromGenericGraph
  ) where

import Prelude hiding ( null, (!!) )

import Data.Coerce
import Data.Foldable (foldl')
import Data.Hashable
import Data.IntMap.Strict (IntMap)
import Data.IntMap.Strict qualified as IntMap
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Sequence (Seq, pattern (:|>))
import Data.Sequence qualified as DS
import Data.Graph qualified
import Data.Word
import Data.Bits
import Control.Exception
import System.IO.Unsafe

import Agda.Interaction.Options.Base (optCumulativity, optOccurrence, optPolarity)
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Position (HasRange(..), noRange, Range)
import Agda.TypeChecking.Functions
import Agda.TypeChecking.Monad hiding (getOccurrencesFromType)
import Agda.TypeChecking.Patterns.Match (properlyMatching)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Positivity.Warnings qualified as W
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope

import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty qualified as P
import Agda.Utils.ExpandCase
import Agda.Utils.Hash
import Agda.Utils.HashTable qualified as HT
import Agda.Utils.Impossible
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.SemiRing
import Agda.Utils.Size
import Agda.Utils.StrictReader
import Agda.Utils.Graph.AdjacencyMap.Unidirectional qualified as Graph
import Agda.Utils.MinimalArray.MutableLifted qualified as MArr
import Agda.Utils.MinimalArray.Lifted qualified as Arr


-- Maps keyed by Node
----------------------------------------------------------------------------------------------------

type NodeMap v = HT.HashTableLL Node v

-- | Getting the "found" and "not found" branches as arguments. We
--   do this to fuse away the 'Maybe' in the lookup result.
{-# INLINE lookupNode #-}
lookupNode :: Node -> NodeMap v -> (v -> IO a) -> IO a -> IO a
lookupNode :: forall v a. Node -> NodeMap v -> (v -> IO a) -> IO a -> IO a
lookupNode Node
node NodeMap v
map v -> IO a
found IO a
notfound = Node -> NodeMap v -> (v -> IO a) -> IO a -> IO a
forall a k v (ks :: * -> * -> *) (vs :: * -> * -> *).
(MVector ks k, MVector vs v, Hashable k) =>
k -> HashTable ks k vs v -> (v -> IO a) -> IO a -> IO a
HT.lookupCPS Node
node NodeMap v
map v -> IO a
found IO a
notfound

{-# INLINE lookupMutual #-}
lookupMutual :: QName -> (Int -> OccM a) -> OccM a -> OccM a
lookupMutual :: forall a. QName -> (Int -> OccM a) -> OccM a -> OccM a
lookupMutual QName
q Int -> OccM a
found OccM a
notfound = (OccEnv -> TCM a) -> OccM a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT \OccEnv
e -> (IORef TCState -> TCEnv -> IO a) -> TCM a
forall (m :: * -> *) a. (IORef TCState -> TCEnv -> m a) -> TCMT m a
TCM \IORef TCState
tcs TCEnv
tce ->
  QName
-> HashTable MVector QName MVector Int
-> (Int -> IO a)
-> IO a
-> IO a
forall a k v (ks :: * -> * -> *) (vs :: * -> * -> *).
(MVector ks k, MVector vs v, Hashable k) =>
k -> HashTable ks k vs v -> (v -> IO a) -> IO a -> IO a
HT.lookupCPS QName
q (OccEnv -> HashTable MVector QName MVector Int
mutuals OccEnv
e)
    (\Int
x -> TCM a -> IORef TCState -> TCEnv -> IO a
forall (m :: * -> *) a. TCMT m a -> IORef TCState -> TCEnv -> m a
unTCM (OccM a -> OccEnv -> TCM a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Int -> OccM a
found Int
x) OccEnv
e) IORef TCState
tcs TCEnv
tce)
    (TCM a -> IORef TCState -> TCEnv -> IO a
forall (m :: * -> *) a. TCMT m a -> IORef TCState -> TCEnv -> m a
unTCM (OccM a -> OccEnv -> TCM a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT OccM a
notfound OccEnv
e) IORef TCState
tcs TCEnv
tce)

{-# NOINLINE insertMutual #-}
insertMutual :: Mutuals -> QName -> Int -> IO ()
insertMutual :: HashTable MVector QName MVector Int -> QName -> Int -> IO ()
insertMutual HashTable MVector QName MVector Int
muts QName
q Int
arity = HashTable MVector QName MVector Int -> QName -> Int -> IO ()
forall k (vs :: * -> * -> *) v (ks :: * -> * -> *).
(Hashable k, MVector vs v, MVector ks k) =>
HashTable ks k vs v -> k -> v -> IO ()
HT.insert HashTable MVector QName MVector Int
muts QName
q Int
arity

{-# NOINLINE insertNode #-}
insertNode :: Node -> v -> NodeMap v -> IO ()
insertNode :: forall v. Node -> v -> NodeMap v -> IO ()
insertNode Node
n v
v NodeMap v
map = NodeMap v -> Node -> v -> IO ()
forall k (vs :: * -> * -> *) v (ks :: * -> * -> *).
(Hashable k, MVector vs v, MVector ks k) =>
HashTable ks k vs v -> k -> v -> IO ()
HT.insert NodeMap v
map Node
n v
v

{-# NOINLINE nodeMapToList #-}
nodeMapToList :: NodeMap v -> IO [(Node, v)]
nodeMapToList :: forall v. NodeMap v -> IO [(Node, v)]
nodeMapToList NodeMap v
map = IO [(Node, v)] -> IO [(Node, v)]
forall a b. Coercible a b => a -> b
coerce (NodeMap v -> IO [(Node, v)]
forall k (ks :: * -> * -> *) (vs :: * -> * -> *) v.
(Hashable k, MVector ks k, MVector vs v) =>
HashTable ks k vs v -> IO [(k, v)]
HT.toList NodeMap v
map)

{-# NOINLINE cloneNodeMap #-}
cloneNodeMap :: NodeMap v -> IO (NodeMap v)
cloneNodeMap :: forall v. NodeMap v -> IO (NodeMap v)
cloneNodeMap = HashTable MVector Node MVector v
-> IO (HashTable MVector Node MVector v)
forall (ks :: * -> * -> *) k (vs :: * -> * -> *) v.
(MVector ks k, MVector vs v) =>
HashTable ks k vs v -> IO (HashTable ks k vs v)
HT.clone

-- Occurrence graph
----------------------------------------------------------------------------------------------------

-- | Meaning of the graph: the keys in the outer NodeMap occur in the keys of the inner NodeMap.
type OccGraph = NodeMap (NodeMap (Edge OccursWhere))

{-# NOINLINE addEdgeToGraph #-}
addEdgeToGraph :: Node -> Node -> Edge OccursWhere -> OccGraph -> IO ()
addEdgeToGraph :: Node -> Node -> Edge OccursWhere -> OccGraph -> IO ()
addEdgeToGraph Node
src Node
tgt Edge OccursWhere
e OccGraph
graph = Node
-> OccGraph
-> (NodeMap (Edge OccursWhere) -> IO ())
-> IO ()
-> IO ()
forall v a. Node -> NodeMap v -> (v -> IO a) -> IO a -> IO a
lookupNode Node
src OccGraph
graph
  (\NodeMap (Edge OccursWhere)
tgts -> Node
-> NodeMap (Edge OccursWhere)
-> (Edge OccursWhere -> IO ())
-> IO ()
-> IO ()
forall v a. Node -> NodeMap v -> (v -> IO a) -> IO a -> IO a
lookupNode Node
tgt NodeMap (Edge OccursWhere)
tgts
    (\Edge OccursWhere
e' -> Node -> Edge OccursWhere -> NodeMap (Edge OccursWhere) -> IO ()
forall v. Node -> v -> NodeMap v -> IO ()
insertNode Node
tgt (Edge OccursWhere -> Edge OccursWhere -> Edge OccursWhere
forall a. Edge a -> Edge a -> Edge a
mergeEdges Edge OccursWhere
e Edge OccursWhere
e') NodeMap (Edge OccursWhere)
tgts)
    (Node -> Edge OccursWhere -> NodeMap (Edge OccursWhere) -> IO ()
forall v. Node -> v -> NodeMap v -> IO ()
insertNode Node
tgt Edge OccursWhere
e NodeMap (Edge OccursWhere)
tgts))
  (do
    tgts <- IO (NodeMap (Edge OccursWhere))
forall (ks :: * -> * -> *) k (vs :: * -> * -> *) v.
(MVector ks k, MVector vs v) =>
IO (HashTable ks k vs v)
HT.empty
    insertNode tgt e tgts
    insertNode src tgts graph)

{-# NOINLINE adjacencyList #-}
adjacencyList :: OccGraph -> IO [(Node, Node, Edge OccursWhere)]
adjacencyList :: OccGraph -> IO [(Node, Node, Edge OccursWhere)]
adjacencyList OccGraph
graph = do
  assocs <- OccGraph -> IO [(Node, NodeMap (Edge OccursWhere))]
forall v. NodeMap v -> IO [(Node, v)]
nodeMapToList OccGraph
graph
  assocs <- forM assocs \(Node
src, NodeMap (Edge OccursWhere)
tgts) -> (Node
src,) ([(Node, Edge OccursWhere)] -> (Node, [(Node, Edge OccursWhere)]))
-> IO [(Node, Edge OccursWhere)]
-> IO (Node, [(Node, Edge OccursWhere)])
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NodeMap (Edge OccursWhere) -> IO [(Node, Edge OccursWhere)]
forall v. NodeMap v -> IO [(Node, v)]
nodeMapToList NodeMap (Edge OccursWhere)
tgts
  pure [(src, tgt, e) | (src, tgts) <- assocs, (tgt, e) <- tgts]

{-# NOINLINE addTargetNodesAsSource #-}
-- | For every node appearing as a target but not as a source, add it as a source node with empty
--   map for targets. This is an invariant that's required by Data.Graph.stronglyConnComp.
addTargetNodesAsSource :: OccGraph -> IO OccGraph
addTargetNodesAsSource :: OccGraph -> IO OccGraph
addTargetNodesAsSource OccGraph
graph = do
  graph' <- OccGraph -> IO OccGraph
forall v. NodeMap v -> IO (NodeMap v)
cloneNodeMap OccGraph
graph
  HT.forAssocs graph \Node
src NodeMap (Edge OccursWhere)
tgts ->
    NodeMap (Edge OccursWhere)
-> (Node -> Edge OccursWhere -> IO ()) -> IO ()
forall (ks :: * -> * -> *) k (vs :: * -> * -> *) v.
(MVector ks k, MVector vs v) =>
HashTable ks k vs v -> (k -> v -> IO ()) -> IO ()
HT.forAssocs NodeMap (Edge OccursWhere)
tgts \Node
tgt Edge OccursWhere
_ -> Node
-> OccGraph
-> (NodeMap (Edge OccursWhere) -> IO ())
-> IO ()
-> IO ()
forall v a. Node -> NodeMap v -> (v -> IO a) -> IO a -> IO a
lookupNode Node
tgt OccGraph
graph
      (\NodeMap (Edge OccursWhere)
_ -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
      (do
        edges <- IO (NodeMap (Edge OccursWhere))
forall (ks :: * -> * -> *) k (vs :: * -> * -> *) v.
(MVector ks k, MVector vs v) =>
IO (HashTable ks k vs v)
HT.empty
        insertNode tgt edges graph')
  pure graph'

{-# NOINLINE stronglyConnComp #-}
-- | Strongly connected components, in reverse topological order.
stronglyConnComp :: OccGraph -> IO [Data.Graph.SCC Node]
stronglyConnComp :: OccGraph -> IO [SCC Node]
stronglyConnComp OccGraph
graph = do
  graph  <- OccGraph -> IO OccGraph
addTargetNodesAsSource OccGraph
graph
  assocs <- nodeMapToList graph
  assocs <- forM assocs \(Node
src, NodeMap (Edge OccursWhere)
tgts) -> (Node
src,Node
src,) ([Node] -> (Node, Node, [Node]))
-> ([(Node, Edge OccursWhere)] -> [Node])
-> [(Node, Edge OccursWhere)]
-> (Node, Node, [Node])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Node, Edge OccursWhere) -> Node)
-> [(Node, Edge OccursWhere)] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map' (Node, Edge OccursWhere) -> Node
forall a b. (a, b) -> a
fst ([(Node, Edge OccursWhere)] -> (Node, Node, [Node]))
-> IO [(Node, Edge OccursWhere)] -> IO (Node, Node, [Node])
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> NodeMap (Edge OccursWhere) -> IO [(Node, Edge OccursWhere)]
forall v. NodeMap v -> IO [(Node, v)]
nodeMapToList NodeMap (Edge OccursWhere)
tgts
  pure $! Data.Graph.stronglyConnComp assocs

{-# NOINLINE toGenericGraph #-}
-- | Convert to generic Utils graph, for the purpose of testing and warning rendering.
toGenericGraph :: OccGraph -> Graph.Graph Node (Edge W.OccursWhere)
toGenericGraph :: OccGraph -> Graph Node (Edge OccursWhere)
toGenericGraph OccGraph
graph = IO (Graph Node (Edge OccursWhere)) -> Graph Node (Edge OccursWhere)
forall a. IO a -> a
unsafeDupablePerformIO do

  let convEdge :: Edge OccursWhere -> Edge W.OccursWhere
      convEdge :: Edge OccursWhere -> Edge OccursWhere
convEdge (Edge Occurrence
occ (OccursWhere Range
rng OccursPath
path)) = Occurrence -> OccursWhere -> Edge OccursWhere
forall a. Occurrence -> a -> Edge a
Edge Occurrence
occ (Range -> OccursPath -> OccursWhere
convPath Range
rng OccursPath
path)

      convPath :: Range -> OccursPath -> W.OccursWhere
      convPath :: Range -> OccursPath -> OccursWhere
convPath Range
rng OccursPath
path = let

        go' :: OccursPath -> Seq W.Where
        go' :: OccursPath -> Seq Where
go' = \case
          OccursPath
Root            -> Seq Where
forall a. Monoid a => a
mempty
          MutDefArg OccursPath
p QName
x Int
i -> OccursPath -> Seq Where
go' OccursPath
p Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> QName -> Int -> Where
W.DefArg QName
x Int
i
          LeftOfArrow OccursPath
p   -> OccursPath -> Seq Where
go' OccursPath
p Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Where
W.LeftOfArrow
          DefArg OccursPath
p QName
x Int
i    -> OccursPath -> Seq Where
go' OccursPath
p Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> QName -> Int -> Where
W.DefArg QName
x Int
i
          UnderInf OccursPath
p      -> OccursPath -> Seq Where
go' OccursPath
p Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Where
W.UnderInf
          VarArg OccursPath
p Int
i Occurrence
o    -> OccursPath -> Seq Where
go' OccursPath
p Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Occurrence -> Int -> Where
W.VarArg Occurrence
o Int
i
          MetaArg OccursPath
p       -> OccursPath -> Seq Where
go' OccursPath
p Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Where
W.MetaArg
          ConArgType OccursPath
p QName
x  -> OccursPath -> Seq Where
go' OccursPath
p Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> QName -> Where
W.ConArgType QName
x
          IndArgType OccursPath
p QName
x  -> OccursPath -> Seq Where
go' OccursPath
p Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> QName -> Where
W.IndArgType QName
x
          ConEndpoint OccursPath
p QName
x -> OccursPath -> Seq Where
go' OccursPath
p Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> QName -> Where
W.ConEndpoint QName
x
          InClause OccursPath
p Int
i    -> OccursPath -> Seq Where
go' OccursPath
p Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Int -> Where
W.InClause Int
i
          Matched OccursPath
p       -> OccursPath -> Seq Where
go' OccursPath
p Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Where
W.Matched
          InIndex OccursPath
p       -> OccursPath -> Seq Where
go' OccursPath
p Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Where
W.InIndex
          InSort OccursPath
p        -> OccursPath -> Seq Where
go' OccursPath
p Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Where
W.InSort
          InDefOf OccursPath
p QName
x     -> OccursPath -> Seq Where
go' OccursPath
p Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> QName -> Where
W.InDefOf QName
x

        go :: OccursPath -> (Seq W.Where, Seq W.Where)
        go :: OccursPath -> (Seq Where, Seq Where)
go = \case
          OccursPath
Root            -> (Seq Where
forall a. Monoid a => a
mempty, Seq Where
forall a. Monoid a => a
mempty)
          MutDefArg OccursPath
p QName
x Int
i -> let s1 :: Seq Where
s1 = OccursPath -> Seq Where
go' OccursPath
p
                                 s2 :: Seq Where
s2 = Where -> Seq Where
forall a. a -> Seq a
DS.singleton (QName -> Int -> Where
W.DefArg QName
x Int
i)
                             in (Seq Where
s1, Seq Where
s2)
          LeftOfArrow OccursPath
p   -> (Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Where
W.LeftOfArrow)   (Seq Where -> Seq Where)
-> (Seq Where, Seq Where) -> (Seq Where, Seq Where)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> OccursPath -> (Seq Where, Seq Where)
go OccursPath
p
          DefArg OccursPath
p QName
x Int
i    -> (Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> QName -> Int -> Where
W.DefArg QName
x Int
i)    (Seq Where -> Seq Where)
-> (Seq Where, Seq Where) -> (Seq Where, Seq Where)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> OccursPath -> (Seq Where, Seq Where)
go OccursPath
p
          UnderInf OccursPath
p      -> (Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Where
W.UnderInf)      (Seq Where -> Seq Where)
-> (Seq Where, Seq Where) -> (Seq Where, Seq Where)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> OccursPath -> (Seq Where, Seq Where)
go OccursPath
p
          VarArg OccursPath
p Int
i Occurrence
o    -> (Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Occurrence -> Int -> Where
W.VarArg Occurrence
o Int
i)    (Seq Where -> Seq Where)
-> (Seq Where, Seq Where) -> (Seq Where, Seq Where)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> OccursPath -> (Seq Where, Seq Where)
go OccursPath
p
          MetaArg OccursPath
p       -> (Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Where
W.MetaArg)       (Seq Where -> Seq Where)
-> (Seq Where, Seq Where) -> (Seq Where, Seq Where)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> OccursPath -> (Seq Where, Seq Where)
go OccursPath
p
          ConArgType OccursPath
p QName
x  -> (Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> QName -> Where
W.ConArgType QName
x)  (Seq Where -> Seq Where)
-> (Seq Where, Seq Where) -> (Seq Where, Seq Where)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> OccursPath -> (Seq Where, Seq Where)
go OccursPath
p
          IndArgType OccursPath
p QName
x  -> (Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> QName -> Where
W.IndArgType QName
x)  (Seq Where -> Seq Where)
-> (Seq Where, Seq Where) -> (Seq Where, Seq Where)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> OccursPath -> (Seq Where, Seq Where)
go OccursPath
p
          ConEndpoint OccursPath
p QName
x -> (Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> QName -> Where
W.ConEndpoint QName
x) (Seq Where -> Seq Where)
-> (Seq Where, Seq Where) -> (Seq Where, Seq Where)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> OccursPath -> (Seq Where, Seq Where)
go OccursPath
p
          InClause OccursPath
p Int
i    -> (Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Int -> Where
W.InClause Int
i)    (Seq Where -> Seq Where)
-> (Seq Where, Seq Where) -> (Seq Where, Seq Where)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> OccursPath -> (Seq Where, Seq Where)
go OccursPath
p
          Matched OccursPath
p       -> (Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Where
W.Matched)       (Seq Where -> Seq Where)
-> (Seq Where, Seq Where) -> (Seq Where, Seq Where)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> OccursPath -> (Seq Where, Seq Where)
go OccursPath
p
          InIndex OccursPath
p       -> (Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Where
W.InIndex)       (Seq Where -> Seq Where)
-> (Seq Where, Seq Where) -> (Seq Where, Seq Where)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> OccursPath -> (Seq Where, Seq Where)
go OccursPath
p
          InSort OccursPath
p        -> (Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Where
W.InSort)        (Seq Where -> Seq Where)
-> (Seq Where, Seq Where) -> (Seq Where, Seq Where)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> OccursPath -> (Seq Where, Seq Where)
go OccursPath
p
          InDefOf OccursPath
p QName
x     -> (Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> QName -> Where
W.InDefOf QName
x)     (Seq Where -> Seq Where)
-> (Seq Where, Seq Where) -> (Seq Where, Seq Where)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> OccursPath -> (Seq Where, Seq Where)
go OccursPath
p

        in case OccursPath -> (Seq Where, Seq Where)
go OccursPath
path of (Seq Where
s1, Seq Where
s2) -> Range -> Seq Where -> Seq Where -> OccursWhere
W.OccursWhere Range
rng Seq Where
s1 Seq Where
s2

  let go :: Map Node (Map Node (Edge W.OccursWhere))
         -> (Node, Node, Edge OccursWhere)
         -> Map Node (Map Node (Edge W.OccursWhere))
      go :: Map Node (Map Node (Edge OccursWhere))
-> (Node, Node, Edge OccursWhere)
-> Map Node (Map Node (Edge OccursWhere))
go Map Node (Map Node (Edge OccursWhere))
m (Node
src, Node
tgt, Edge OccursWhere -> Edge OccursWhere
convEdge -> Edge OccursWhere
e) =
          (Map Node (Edge OccursWhere)
 -> Map Node (Edge OccursWhere) -> Map Node (Edge OccursWhere))
-> Node
-> Map Node (Edge OccursWhere)
-> Map Node (Map Node (Edge OccursWhere))
-> Map Node (Map Node (Edge OccursWhere))
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (\Map Node (Edge OccursWhere)
_ -> Node
-> Edge OccursWhere
-> Map Node (Edge OccursWhere)
-> Map Node (Edge OccursWhere)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Node
tgt Edge OccursWhere
e) Node
src (Node -> Edge OccursWhere -> Map Node (Edge OccursWhere)
forall k a. k -> a -> Map k a
Map.singleton Node
tgt Edge OccursWhere
e) (Map Node (Map Node (Edge OccursWhere))
 -> Map Node (Map Node (Edge OccursWhere)))
-> Map Node (Map Node (Edge OccursWhere))
-> Map Node (Map Node (Edge OccursWhere))
forall a b. (a -> b) -> a -> b
$
          (Map Node (Edge OccursWhere)
 -> Map Node (Edge OccursWhere) -> Map Node (Edge OccursWhere))
-> Node
-> Map Node (Edge OccursWhere)
-> Map Node (Map Node (Edge OccursWhere))
-> Map Node (Map Node (Edge OccursWhere))
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (\Map Node (Edge OccursWhere)
_ Map Node (Edge OccursWhere)
tgts -> Map Node (Edge OccursWhere)
tgts) Node
tgt Map Node (Edge OccursWhere)
forall a. Monoid a => a
mempty (Map Node (Map Node (Edge OccursWhere))
 -> Map Node (Map Node (Edge OccursWhere)))
-> Map Node (Map Node (Edge OccursWhere))
-> Map Node (Map Node (Edge OccursWhere))
forall a b. (a -> b) -> a -> b
$
          Map Node (Map Node (Edge OccursWhere))
m

  assocs <- OccGraph -> IO [(Node, Node, Edge OccursWhere)]
adjacencyList OccGraph
graph
  pure $! Graph.Graph $! foldl' go mempty assocs

-- | Make a graph from a generic one. We use this in testing in Internal.TypeChecking.Positivity
--   where it's much more convenient to generate immutable graphs. Note: we ignore occurrence
--   location info.
{-# NOINLINE fromGenericGraph #-}
fromGenericGraph :: Graph.Graph Node (Edge a) -> OccGraph
fromGenericGraph :: forall a. Graph Node (Edge a) -> OccGraph
fromGenericGraph (Graph.Graph Map Node (Map Node (Edge a))
graph) = IO OccGraph -> OccGraph
forall a. IO a -> a
unsafeDupablePerformIO do
  graph' <- IO OccGraph
forall (ks :: * -> * -> *) k (vs :: * -> * -> *) v.
(MVector ks k, MVector vs v) =>
IO (HashTable ks k vs v)
HT.empty
  forM_ (Map.toList graph) \(Node
src, Map Node (Edge a)
tgts) ->
    [(Node, Edge a)] -> ((Node, Edge a) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map Node (Edge a) -> [(Node, Edge a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Node (Edge a)
tgts) \(Node
tgt, Edge Occurrence
o a
_) ->
      Node -> Node -> Edge OccursWhere -> OccGraph -> IO ()
addEdgeToGraph Node
src Node
tgt (Occurrence -> OccursWhere -> Edge OccursWhere
forall a. Occurrence -> a -> Edge a
Edge Occurrence
o (Range -> OccursPath -> OccursWhere
OccursWhere Range
forall a. Range' a
noRange OccursPath
Root)) OccGraph
graph'
  pure graph'


-- Occurrence analysis
----------------------------------------------------------------------------------------------------

{-
Occurrence analysis is a single traversal over definitions which builds a mutable graph in IO.  We
keep track of the "path" during traversal that leads from the current position to a top definition.
-}

-- | Top-level arg index that a local variable was bound in, arg polarity of the var itself.
data DefArgInEnv = DefArgInEnv Int [Occurrence]
  deriving Int -> DefArgInEnv -> ShowS
[DefArgInEnv] -> ShowS
DefArgInEnv -> ArgName
(Int -> DefArgInEnv -> ShowS)
-> (DefArgInEnv -> ArgName)
-> ([DefArgInEnv] -> ShowS)
-> Show DefArgInEnv
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DefArgInEnv -> ShowS
showsPrec :: Int -> DefArgInEnv -> ShowS
$cshow :: DefArgInEnv -> ArgName
show :: DefArgInEnv -> ArgName
$cshowList :: [DefArgInEnv] -> ShowS
showList :: [DefArgInEnv] -> ShowS
Show

-- | Mutual definition names in the block.
--   Each name is mapped to an arity. It's meaningful for 'FunctionDefn'-s; see 'preprocessMutuals'
--   for docs. For everything else it's set to @maxBound :: Int@.
type Mutuals = HT.HashTableLU QName Int

data OccEnv = OccEnv {
    OccEnv -> QName
topDef     :: QName         -- ^ The definition we're working under (as n-th definition in the mutual block)
  , OccEnv -> [DefArgInEnv]
topDefArgs :: [DefArgInEnv] -- ^ Occurrence info for definition args.
  , OccEnv -> Maybe QName
inf        :: Maybe QName   -- ^ Name for ∞ builtin.
  , OccEnv -> Occurrence
sortOcc    :: Occurrence    -- ^ Occurrence to compose with when descending into a 'Sort'.
                                --   See 'sortOccurrence'.
  , OccEnv -> Int
locals     :: Int           -- ^ Number of local binders (on the top of the definition args).
  , OccEnv -> HashTable MVector QName MVector Int
mutuals    :: Mutuals       -- ^ Set of mutual QName-s in the block.
  , OccEnv -> Node
target     :: Node          -- ^ We add occurrences pointing to this node.
  , OccEnv -> OccursPath
path       :: OccursPath    -- ^ Path from the target node to the current position.
  , OccEnv -> Occurrence
occ        :: Occurrence    -- ^ Occurence of current position.
  , OccEnv -> OccGraph
graph      :: OccGraph      -- ^ Graph that's being built.
  }

type OccM = ReaderT OccEnv TCM

instance PrettyTCMWithNode (Edge OccursWhere) where
  prettyTCMWithNode :: forall n (m :: * -> *).
(PrettyTCM n, MonadPretty m) =>
WithNode n (Edge OccursWhere) -> m Doc
prettyTCMWithNode (WithNode n
n (Edge Occurrence
o (OccursWhere Range
_ OccursPath
w))) = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ Occurrence -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Occurrence -> m Doc
prettyTCM Occurrence
o m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> n -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => n -> m Doc
prettyTCM n
n
    , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ OccursPath -> Doc
forall a. Pretty a => a -> Doc
P.pretty OccursPath
w
    ]

{-# INLINE underPath #-}
underPath :: (OccursPath -> OccursPath) -> OccM a -> OccM a
underPath :: forall a. (OccursPath -> OccursPath) -> OccM a -> OccM a
underPath OccursPath -> OccursPath
f = (OccEnv -> OccEnv)
-> ReaderT OccEnv (TCMT IO) a -> ReaderT OccEnv (TCMT IO) a
forall a.
(OccEnv -> OccEnv)
-> ReaderT OccEnv (TCMT IO) a -> ReaderT OccEnv (TCMT IO) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local \OccEnv
env -> OccEnv
env {path = f (path env)}

{-# INLINE underOcc #-}
underOcc :: Occurrence -> OccM a -> OccM a
underOcc :: forall a. Occurrence -> OccM a -> OccM a
underOcc Occurrence
p = (OccEnv -> OccEnv)
-> ReaderT OccEnv (TCMT IO) a -> ReaderT OccEnv (TCMT IO) a
forall a.
(OccEnv -> OccEnv)
-> ReaderT OccEnv (TCMT IO) a -> ReaderT OccEnv (TCMT IO) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local \OccEnv
env -> OccEnv
env {occ = otimes (occ env) p}

{-# INLINE underBinder #-}
underBinder :: OccM a -> OccM a
underBinder :: forall a. OccM a -> OccM a
underBinder = (OccEnv -> OccEnv)
-> ReaderT OccEnv (TCMT IO) a -> ReaderT OccEnv (TCMT IO) a
forall a.
(OccEnv -> OccEnv)
-> ReaderT OccEnv (TCMT IO) a -> ReaderT OccEnv (TCMT IO) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local \OccEnv
env -> OccEnv
env {locals = locals env + 1}

{-# INLINE underPathOcc #-}
-- | Modify the current path and 'otimes' a new 'Occurrence' to the
--   current occurrence.
underPathOcc :: (OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathOcc :: forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathOcc OccursPath -> OccursPath
f Occurrence
p = (OccEnv -> OccEnv)
-> ReaderT OccEnv (TCMT IO) a -> ReaderT OccEnv (TCMT IO) a
forall a.
(OccEnv -> OccEnv)
-> ReaderT OccEnv (TCMT IO) a -> ReaderT OccEnv (TCMT IO) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local \OccEnv
e -> OccEnv
e {path = f (path e), occ = otimes (occ e) p}

{-# INLINE underPathSetOcc #-}
-- | Modify the current path and set the current 'Occurence' to
--   the given value.
underPathSetOcc :: (OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathSetOcc :: forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathSetOcc OccursPath -> OccursPath
f Occurrence
p = (OccEnv -> OccEnv)
-> ReaderT OccEnv (TCMT IO) a -> ReaderT OccEnv (TCMT IO) a
forall a.
(OccEnv -> OccEnv)
-> ReaderT OccEnv (TCMT IO) a -> ReaderT OccEnv (TCMT IO) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local \OccEnv
e -> OccEnv
e {path = f (path e), occ = p}

getOccurrencesFromType :: Type -> TCM [Occurrence]
getOccurrencesFromType :: Type'' Term Term -> TCM [Occurrence]
getOccurrencesFromType Type'' Term Term
a = (PragmaOptions -> Bool
optPolarity (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) TCMT IO Bool -> (Bool -> TCM [Occurrence]) -> TCM [Occurrence]
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Bool
False -> [Occurrence] -> TCM [Occurrence]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  Bool
True  -> do
    let go :: Type -> ReduceM [Occurrence]
        go :: Type'' Term Term -> ReduceM [Occurrence]
go Type'' Term Term
a = (Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl (Type'' Term Term -> Term)
-> ReduceM (Type'' Term Term) -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type'' Term Term -> ReduceM (Type'' Term Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type'' Term Term
a) ReduceM Term
-> (Term -> ReduceM [Occurrence]) -> ReduceM [Occurrence]
forall a b. ReduceM a -> (a -> ReduceM b) -> ReduceM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Pi Dom' Term (Type'' Term Term)
a Abs (Type'' Term Term)
b -> do
            let p :: Occurrence
p = ModalPolarity -> Occurrence
modalPolarityToOccurrence (ModalPolarity -> Occurrence) -> ModalPolarity -> Occurrence
forall a b. (a -> b) -> a -> b
$ PolarityModality -> ModalPolarity
modPolarityAnn (PolarityModality -> ModalPolarity)
-> PolarityModality -> ModalPolarity
forall a b. (a -> b) -> a -> b
$ Dom' Term (Type'' Term Term) -> PolarityModality
forall a. LensModalPolarity a => a -> PolarityModality
getModalPolarity Dom' Term (Type'' Term Term)
a
            -- We're working under a Strict pragma, and we want this to be lazy,
            -- because we might have under-applied names where we don't want to
            -- unnecessarily compute types.
            ~ps <- Dom' Term (Type'' Term Term)
-> Abs (Type'' Term Term)
-> (Type'' Term Term -> ReduceM [Occurrence])
-> ReduceM [Occurrence]
forall a b.
Dom' Term (Type'' Term Term)
-> Abs a -> (a -> ReduceM b) -> ReduceM b
underAbsReduceM Dom' Term (Type'' Term Term)
a Abs (Type'' Term Term)
b \Type'' Term Term
b -> Type'' Term Term -> ReduceM [Occurrence]
go Type'' Term Term
b
            pure (p:ps)
          Term
_ -> [Occurrence] -> ReduceM [Occurrence]
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    ReduceM [Occurrence] -> TCM [Occurrence]
forall a. ReduceM a -> TCMT IO a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (Type'' Term Term -> ReduceM [Occurrence]
go Type'' Term Term
a)

addRawEdge :: Range -> Occurrence -> Node -> Node -> OccM ()
addRawEdge :: Range -> Occurrence -> Node -> Node -> ReaderT OccEnv (TCMT IO) ()
addRawEdge Range
rng Occurrence
occ Node
src Node
tgt = do
  path   <- (OccEnv -> OccursPath) -> ReaderT OccEnv (TCMT IO) OccursPath
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccEnv -> OccursPath
path
  graph  <- asks graph
  let e = Occurrence -> OccursWhere -> Edge OccursWhere
forall a. Occurrence -> a -> Edge a
Edge Occurrence
occ (Range -> OccursPath -> OccursWhere
OccursWhere Range
rng OccursPath
path)
  lift $ lift $ addEdgeToGraph src tgt e graph

addEdge :: Range -> Node -> OccM ()
addEdge :: Range -> Node -> ReaderT OccEnv (TCMT IO) ()
addEdge Range
rng Node
src = do
  target <- (OccEnv -> Node) -> ReaderT OccEnv (TCMT IO) Node
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccEnv -> Node
target
  path   <- asks path
  occ    <- asks occ
  graph  <- asks graph
  expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case Occurrence
occ of
    Occurrence
Unused -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Occurrence
occ    -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret do
      let e :: Edge OccursWhere
e = Occurrence -> OccursWhere -> Edge OccursWhere
forall a. Occurrence -> a -> Edge a
Edge Occurrence
occ (Range -> OccursPath -> OccursWhere
OccursWhere Range
rng OccursPath
path)
      TCMT IO () -> ReaderT OccEnv (TCMT IO) ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT OccEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO () -> ReaderT OccEnv (TCMT IO) ())
-> TCMT IO () -> ReaderT OccEnv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ IO () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => m a -> TCMT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> TCMT IO ()) -> IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Edge OccursWhere -> OccGraph -> IO ()
addEdgeToGraph Node
src Node
target Edge OccursWhere
e OccGraph
graph

-- | Recurse into an argument of a non-mutual definition.
occurrencesInDefArg :: QName -> Occurrence -> Int -> Elim -> OccM ()
occurrencesInDefArg :: QName
-> Occurrence -> Int -> Elim' Term -> ReaderT OccEnv (TCMT IO) ()
occurrencesInDefArg QName
d Occurrence
p Int
i Elim' Term
e = ((ReaderT OccEnv (TCMT IO) ()
  -> Result (ReaderT OccEnv (TCMT IO) ()))
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case Occurrence
p of
  Occurrence
Unused -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Occurrence
p      -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath)
-> Occurrence
-> ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathOcc (\OccursPath
p -> OccursPath -> QName -> Int -> OccursPath
DefArg OccursPath
p QName
d Int
i) Occurrence
p (ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ())
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Elim' Term -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Elim' Term
e

-- | Recurse into an argument of an argument of the top definition.
occurrencesInDefArgArg :: Occurrence -> Int -> Elim -> OccM ()
occurrencesInDefArgArg :: Occurrence -> Int -> Elim' Term -> ReaderT OccEnv (TCMT IO) ()
occurrencesInDefArgArg Occurrence
p Int
i Elim' Term
e = ((ReaderT OccEnv (TCMT IO) ()
  -> Result (ReaderT OccEnv (TCMT IO) ()))
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case Occurrence
p of
  Occurrence
Unused -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Occurrence
p      -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath)
-> Occurrence
-> ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathOcc (\OccursPath
x -> OccursPath -> Int -> Occurrence -> OccursPath
VarArg OccursPath
x Int
i Occurrence
p) Occurrence
p (ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ())
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Elim' Term -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Elim' Term
e

-- | Recurse into an argument of a mutual definition.
occurrencesInMutDefArg :: QName -> Occurrence -> Int -> Elim -> OccM ()
occurrencesInMutDefArg :: QName
-> Occurrence -> Int -> Elim' Term -> ReaderT OccEnv (TCMT IO) ()
occurrencesInMutDefArg QName
d Occurrence
p Int
i Elim' Term
e = ((ReaderT OccEnv (TCMT IO) ()
  -> Result (ReaderT OccEnv (TCMT IO) ()))
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case Occurrence
p of
  Occurrence
Unused -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Occurrence
p      -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ (OccEnv -> OccEnv)
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a.
(OccEnv -> OccEnv)
-> ReaderT OccEnv (TCMT IO) a -> ReaderT OccEnv (TCMT IO) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\OccEnv
e -> OccEnv
e {path = MutDefArg (path e) d i, target = ArgNode d i, occ = p}) (ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ())
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
                    Elim' Term -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Elim' Term
e

-- | The 'Occurrence' to compose with when the analysis descends from a 'Term'
--   into a 'Sort' (issue #8688).
--
--   Without @--cumulativity@, distinct universes are unrelated: @Set x@ and
--   @Set y@ are neither equal nor in a subtyping relation unless @x@ and @y@ are
--   equal.  So whatever a sort depends on has to be compared invariantly by the
--   conversion checker, and we return 'Mixed'.
--
--   With @--cumulativity@, universes are monotone in their level
--   (@Set x =< Set y@ iff @x =< y@, see @leqSort@ in
--   "Agda.TypeChecking.Conversion"), so a /positive/ occurrence is justified.
--
--   We deliberately return 'JustPos' and not 'StrictPos' here.  Both give
--   'Agda.TypeChecking.Polarity.Covariant' polarity, but only 'StrictPos' would
--   be accepted by the positivity checker, and an occurrence inside a sort must
--   not count as strictly positive: a definition like
--   @data D : Setω where c : Set (f D) → D@ defines @D@ by quantifying over a
--   universe whose size depends on @D@ itself.
--
--   Since @--no-cumulativity@ is a /coinfective/ option, a module that does not
--   use cumulativity can never import occurrence information that was computed
--   with cumulativity turned on.
sortOccurrence :: HasOptions m => m Occurrence
sortOccurrence :: forall (m :: * -> *). HasOptions m => m Occurrence
sortOccurrence = do
  cumulativity <- PragmaOptions -> Bool
optCumulativity (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  pure $! if cumulativity then JustPos else Mixed

-- | The initial 'Occurrence' when processing a definition.
mutualDefOcc :: Definition -> Occurrence
mutualDefOcc :: Definition -> Occurrence
mutualDefOcc Definition
d = case Definition -> Defn
theDef Definition
d of
  Datatype{} -> Occurrence
GuardPos
  Record{ recEtaEquality' :: Defn -> EtaEquality
recEtaEquality' = EtaEquality NoEta{} EtaProvenance
_ } -> Occurrence
GuardPos
  Defn
_ -> Occurrence
StrictPos

class ComputeOccurrences a where
  occurrences :: a -> OccM ()

  {-# INLINE occurrences #-}
  default occurrences :: (Foldable t, ComputeOccurrences b, a ~ t b) => a -> OccM ()
  occurrences = (b -> ReaderT OccEnv (TCMT IO) ())
-> t b -> ReaderT OccEnv (TCMT IO) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ b -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences

instance ComputeOccurrences Term where
  occurrences :: Term -> ReaderT OccEnv (TCMT IO) ()
occurrences Term
t = ((ReaderT OccEnv (TCMT IO) ()
  -> Result (ReaderT OccEnv (TCMT IO) ()))
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case Term -> Term
unSpine Term
t of

    Var Int
x [Elim' Term]
es -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret do
      locals <- (OccEnv -> Int) -> ReaderT OccEnv (TCMT IO) Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccEnv -> Int
locals

      -- it's a locally bound variable, all args are Mixed occurrence,
      -- we don't record an occurrence for the variable
      if x < locals then do
        let elims Int
i [a]
es = ((ReaderT OccEnv (TCMT IO) ()
  -> Result (ReaderT OccEnv (TCMT IO) ()))
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case [a]
es of
              []   -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
              a
e:[a]
es -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath)
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a. (OccursPath -> OccursPath) -> OccM a -> OccM a
underPath (\OccursPath
p -> OccursPath -> Int -> Occurrence -> OccursPath
VarArg OccursPath
p Int
i Occurrence
Mixed) (a -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences a
e) ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b.
ReaderT OccEnv (TCMT IO) a
-> ReaderT OccEnv (TCMT IO) b -> ReaderT OccEnv (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> [a] -> ReaderT OccEnv (TCMT IO) ()
elims (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [a]
es

        underOcc Mixed $ elims 0 es

      -- it's bound in a top-level definition argument
      else do
        let elims Int
i [Occurrence]
ps [Elim' Term]
es = ((ReaderT OccEnv (TCMT IO) ()
  -> Result (ReaderT OccEnv (TCMT IO) ()))
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case ([Occurrence]
ps, [Elim' Term]
es) of
              ([Occurrence]
_   , []  ) -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
              ([]  , Elim' Term
e:[Elim' Term]
es) -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ Occurrence -> Int -> Elim' Term -> ReaderT OccEnv (TCMT IO) ()
occurrencesInDefArgArg Occurrence
Mixed Int
i Elim' Term
e ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b.
ReaderT OccEnv (TCMT IO) a
-> ReaderT OccEnv (TCMT IO) b -> ReaderT OccEnv (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> [Occurrence] -> [Elim' Term] -> ReaderT OccEnv (TCMT IO) ()
elims (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [] [Elim' Term]
es
              (Occurrence
p:[Occurrence]
ps, Elim' Term
e:[Elim' Term]
es) -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ Occurrence -> Int -> Elim' Term -> ReaderT OccEnv (TCMT IO) ()
occurrencesInDefArgArg Occurrence
p Int
i Elim' Term
e     ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b.
ReaderT OccEnv (TCMT IO) a
-> ReaderT OccEnv (TCMT IO) b -> ReaderT OccEnv (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> [Occurrence] -> [Elim' Term] -> ReaderT OccEnv (TCMT IO) ()
elims (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Occurrence]
ps [Elim' Term]
es
        topDefArgs <- asks topDefArgs
        topDef     <- asks topDef
        let DefArgInEnv argix ps = topDefArgs !! (x - locals)
        addEdge noRange (ArgNode topDef argix)
        elims 0 ps es

    Def QName
d [Elim' Term]
es -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ (OccEnv -> Maybe QName) -> ReaderT OccEnv (TCMT IO) (Maybe QName)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccEnv -> Maybe QName
inf ReaderT OccEnv (TCMT IO) (Maybe QName)
-> (Maybe QName -> ReaderT OccEnv (TCMT IO) ())
-> ReaderT OccEnv (TCMT IO) ()
forall a b.
ReaderT OccEnv (TCMT IO) a
-> (a -> ReaderT OccEnv (TCMT IO) b) -> ReaderT OccEnv (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case

      -- check for ∞ application
      Just QName
inf | QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
inf -> case [Elim' Term]
es of
        []     -> () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        [Elim' Term
_]    -> () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- unused arg
        [Elim' Term
_, Elim' Term
e] -> (OccursPath -> OccursPath)
-> Occurrence
-> ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathOcc OccursPath -> OccursPath
UnderInf Occurrence
GuardPos (ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ())
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Elim' Term -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Elim' Term
e
        [Elim' Term]
_      -> ReaderT OccEnv (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__

      Maybe QName
_ -> do
        QName
-> (Int -> ReaderT OccEnv (TCMT IO) ())
-> ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) ()
forall a. QName -> (Int -> OccM a) -> OccM a -> OccM a
lookupMutual QName
d

          -- it's a mutual definition
          (\Int
arity -> do
            let range :: Range
range = QName -> Range
forall a. HasRange a => a -> Range
getRange QName
d
            Range -> Node -> ReaderT OccEnv (TCMT IO) ()
addEdge Range
range (QName -> Node
DefNode QName
d)
            ((ReaderT OccEnv (TCMT IO) ()
  -> Result (ReaderT OccEnv (TCMT IO) ()))
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case [Elim' Term]
es of
              [] -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()  -- we skip the mutualDefOcc in this case
              [Elim' Term]
es -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret do
                def <- TCM Definition -> ReaderT OccEnv (TCMT IO) Definition
forall (m :: * -> *) a. Monad m => m a -> ReaderT OccEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Definition -> ReaderT OccEnv (TCMT IO) Definition)
-> TCM Definition -> ReaderT OccEnv (TCMT IO) Definition
forall a b. (a -> b) -> a -> b
$ QName -> TCM Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d
                let defOcc = Definition -> Occurrence
mutualDefOcc Definition
def
                let elims QName
d Occurrence
p Int
i Int
arity [Elim' Term]
es = ((ReaderT OccEnv (TCMT IO) ()
  -> Result (ReaderT OccEnv (TCMT IO) ()))
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case [Elim' Term]
es of
                      []   -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                      Elim' Term
e:[Elim' Term]
es -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ ((ReaderT OccEnv (TCMT IO) ()
  -> Result (ReaderT OccEnv (TCMT IO) ()))
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
arity of

                        Bool
True  -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret do
                          QName
-> Occurrence -> Int -> Elim' Term -> ReaderT OccEnv (TCMT IO) ()
occurrencesInMutDefArg QName
d Occurrence
p Int
i Elim' Term
e
                          QName
-> Occurrence
-> Int
-> Int
-> [Elim' Term]
-> ReaderT OccEnv (TCMT IO) ()
elims QName
d Occurrence
p (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
arity [Elim' Term]
es

                        -- we're over the formal arity of the definition so every arg occurs Mixed
                        -- in its definition
                        Bool
False -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret do
                          Range -> Occurrence -> Node -> Node -> ReaderT OccEnv (TCMT IO) ()
addRawEdge Range
range Occurrence
Mixed (QName -> Int -> Node
ArgNode QName
d Int
i) (QName -> Node
DefNode QName
d)
                          QName
-> Occurrence -> Int -> Elim' Term -> ReaderT OccEnv (TCMT IO) ()
occurrencesInMutDefArg QName
d Occurrence
p Int
i Elim' Term
e
                          QName
-> Occurrence
-> Int
-> Int
-> [Elim' Term]
-> ReaderT OccEnv (TCMT IO) ()
elims QName
d Occurrence
p (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
arity [Elim' Term]
es
                elims d defOcc 0 arity es
          )

          -- it's not a mutual definition, we use existing defArgOccurrences
          -- in each argument in the Elims
          (do
            def <- TCM Definition -> ReaderT OccEnv (TCMT IO) Definition
forall (m :: * -> *) a. Monad m => m a -> ReaderT OccEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Definition -> ReaderT OccEnv (TCMT IO) Definition)
-> TCM Definition -> ReaderT OccEnv (TCMT IO) Definition
forall a b. (a -> b) -> a -> b
$ QName -> TCM Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d
            case theDef def of
              Constructor{} -> do
                let elims :: Int -> [Elim' Term] -> ReaderT OccEnv (TCMT IO) ()
elims Int
i [Elim' Term]
es = ((ReaderT OccEnv (TCMT IO) ()
  -> Result (ReaderT OccEnv (TCMT IO) ()))
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case [Elim' Term]
es of
                      []   -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                      Elim' Term
e:[Elim' Term]
es -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret do QName
-> Occurrence -> Int -> Elim' Term -> ReaderT OccEnv (TCMT IO) ()
occurrencesInDefArg QName
d Occurrence
StrictPos Int
i Elim' Term
e
                                     Int -> [Elim' Term] -> ReaderT OccEnv (TCMT IO) ()
elims (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Elim' Term]
es
                Int -> [Elim' Term] -> ReaderT OccEnv (TCMT IO) ()
elims Int
0 [Elim' Term]
es

              Defn
_ -> do
                -- process Elims where we get Occurrence information from the type
                -- of the definition
                let elims' :: QName -> Int -> [Occurrence] -> Elims -> OccM ()
                    elims' :: QName
-> Int
-> [Occurrence]
-> [Elim' Term]
-> ReaderT OccEnv (TCMT IO) ()
elims' QName
d Int
i [Occurrence]
ps [Elim' Term]
es = ((ReaderT OccEnv (TCMT IO) ()
  -> Result (ReaderT OccEnv (TCMT IO) ()))
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case ([Occurrence]
ps, [Elim' Term]
es) of
                      ([Occurrence]
_   , []  ) -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                      (Occurrence
p:[Occurrence]
ps, Elim' Term
e:[Elim' Term]
es) -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret do QName
-> Occurrence -> Int -> Elim' Term -> ReaderT OccEnv (TCMT IO) ()
occurrencesInDefArg QName
d Occurrence
p Int
i Elim' Term
e
                                             QName
-> Int
-> [Occurrence]
-> [Elim' Term]
-> ReaderT OccEnv (TCMT IO) ()
elims' QName
d (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Occurrence]
ps [Elim' Term]
es
                      ([],   Elim' Term
e:[Elim' Term]
es) -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret do QName
-> Occurrence -> Int -> Elim' Term -> ReaderT OccEnv (TCMT IO) ()
occurrencesInDefArg QName
d Occurrence
Mixed Int
i Elim' Term
e
                                             QName
-> Int
-> [Occurrence]
-> [Elim' Term]
-> ReaderT OccEnv (TCMT IO) ()
elims' QName
d (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Occurrence]
ps [Elim' Term]
es

                -- process Elims where we get Occurrences from defArgOccurrences
                let elims :: QName -> Type -> Int -> [Occurrence] -> Elims -> OccM ()
                    elims :: QName
-> Type'' Term Term
-> Int
-> [Occurrence]
-> [Elim' Term]
-> ReaderT OccEnv (TCMT IO) ()
elims QName
d Type'' Term Term
a Int
i [Occurrence]
ps [Elim' Term]
es = ((ReaderT OccEnv (TCMT IO) ()
  -> Result (ReaderT OccEnv (TCMT IO) ()))
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case ([Occurrence]
ps, [Elim' Term]
es) of
                      ([Occurrence]
_   , []  ) -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                      (Occurrence
p:[Occurrence]
ps, Elim' Term
e:[Elim' Term]
es) -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret do QName
-> Occurrence -> Int -> Elim' Term -> ReaderT OccEnv (TCMT IO) ()
occurrencesInDefArg QName
d Occurrence
p Int
i Elim' Term
e
                                             QName
-> Type'' Term Term
-> Int
-> [Occurrence]
-> [Elim' Term]
-> ReaderT OccEnv (TCMT IO) ()
elims QName
d Type'' Term Term
a (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Occurrence]
ps [Elim' Term]
es
                      ([]  , Elim' Term
e:[Elim' Term]
es) -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret do ps <- TCM [Occurrence] -> ReaderT OccEnv (TCMT IO) [Occurrence]
forall (m :: * -> *) a. Monad m => m a -> ReaderT OccEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM [Occurrence] -> ReaderT OccEnv (TCMT IO) [Occurrence])
-> TCM [Occurrence] -> ReaderT OccEnv (TCMT IO) [Occurrence]
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TCM [Occurrence]
getOccurrencesFromType Type'' Term Term
a
                                             elims' d i (drop i ps) (e:es)

                let defOcc :: Occurrence
defOcc = Definition -> Occurrence
mutualDefOcc Definition
def
                let argOccs :: [Occurrence]
argOccs = Definition -> [Occurrence]
defArgOccurrences Definition
def
                Occurrence
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a. Occurrence -> OccM a -> OccM a
underOcc Occurrence
defOcc (ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ())
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ QName
-> Type'' Term Term
-> Int
-> [Occurrence]
-> [Elim' Term]
-> ReaderT OccEnv (TCMT IO) ()
elims QName
d (Definition -> Type'' Term Term
defType Definition
def) Int
0 [Occurrence]
argOccs [Elim' Term]
es
          )

    Con ConHead
_ ConInfo
_ [Elim' Term]
es -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ [Elim' Term] -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences [Elim' Term]
es
    MetaV MetaId
m [Elim' Term]
es -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath)
-> Occurrence
-> ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathSetOcc OccursPath -> OccursPath
MetaArg Occurrence
Mixed ([Elim' Term] -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences [Elim' Term]
es)
    Pi Dom' Term (Type'' Term Term)
a Abs (Type'' Term Term)
b     -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath)
-> Occurrence
-> ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathOcc OccursPath -> OccursPath
LeftOfArrow Occurrence
JustNeg (Dom' Term (Type'' Term Term) -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Dom' Term (Type'' Term Term)
a) ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b.
ReaderT OccEnv (TCMT IO) a
-> ReaderT OccEnv (TCMT IO) b -> ReaderT OccEnv (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Abs (Type'' Term Term) -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Abs (Type'' Term Term)
b
    Lam ArgInfo
_ Abs Term
t    -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ Abs Term -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Abs Term
t
    Level Level' Term
l    -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ Level' Term -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Level' Term
l
    Lit{}      -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    -- Andreas, 2026-08-27, issue #8688: we have to descend into sorts.
    -- How an occurrence inside a sort is counted depends on @--cumulativity@,
    -- see 'sortOccurrence'.
    Sort Sort' Term
s     -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret do
      o <- (OccEnv -> Occurrence) -> ReaderT OccEnv (TCMT IO) Occurrence
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccEnv -> Occurrence
sortOcc
      underPathOcc InSort o $ occurrences s
    -- Jesper, 2020-01-12: this information is also used for the
    -- occurs check, so we need to look under DontCare (see #4371)
    DontCare Term
t -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ Term -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Term
t
    Dummy{}    -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Record that every matched argument of a def occurs in the def.
addClauseArgMatches :: NAPs -> OccM ()
addClauseArgMatches :: NAPs -> ReaderT OccEnv (TCMT IO) ()
addClauseArgMatches NAPs
ps = (OccursPath -> OccursPath)
-> Occurrence
-> ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathSetOcc OccursPath -> OccursPath
Matched Occurrence
Mixed (ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ())
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Int -> NAPs -> ReaderT OccEnv (TCMT IO) ()
go Int
0 NAPs
ps where
  go :: Int -> NAPs -> OccM ()
  go :: Int -> NAPs -> ReaderT OccEnv (TCMT IO) ()
go Int
i NAPs
ps = ((ReaderT OccEnv (TCMT IO) ()
  -> Result (ReaderT OccEnv (TCMT IO) ()))
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case NAPs
ps of
    []   -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    NamedArg DeBruijnPattern
p:NAPs
ps -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret do
      TCMT IO Bool -> ReaderT OccEnv (TCMT IO) Bool
forall (m :: * -> *) a. Monad m => m a -> ReaderT OccEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (DeBruijnPattern -> TCMT IO Bool
forall (m :: * -> *) a. HasConstInfo m => Pattern' a -> m Bool
properlyMatching (Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> Named NamedName DeBruijnPattern -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern
forall e. Arg e -> e
unArg NamedArg DeBruijnPattern
p)) ReaderT OccEnv (TCMT IO) Bool
-> (Bool -> ReaderT OccEnv (TCMT IO) ())
-> ReaderT OccEnv (TCMT IO) ()
forall a b.
ReaderT OccEnv (TCMT IO) a
-> (a -> ReaderT OccEnv (TCMT IO) b) -> ReaderT OccEnv (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Bool
True  -> do topDef <- (OccEnv -> QName) -> ReaderT OccEnv (TCMT IO) QName
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccEnv -> QName
topDef
                    addEdge noRange (ArgNode topDef i)
        Bool
False -> () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      Int -> NAPs -> ReaderT OccEnv (TCMT IO) ()
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) NAPs
ps

instance ComputeOccurrences Clause where
  occurrences :: Clause -> ReaderT OccEnv (TCMT IO) ()
occurrences Clause
cl = do
    let ps :: NAPs
ps = Clause -> NAPs
namedClausePats Clause
cl
    -- TODO #3733: handle hcomp/transp clauses properly
    if NAPs -> Bool
hasDefP NAPs
ps then
      () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    else do
      -- add edges for matched args
      NAPs -> ReaderT OccEnv (TCMT IO) ()
addClauseArgMatches NAPs
ps

      let collectArgs :: NAPs -> [DefArgInEnv]
          collectArgs :: NAPs -> [DefArgInEnv]
collectArgs NAPs
ps = IntMap DefArgInEnv -> [DefArgInEnv]
forall a. IntMap a -> [a]
IntMap.elems (IntMap DefArgInEnv -> [DefArgInEnv])
-> IntMap DefArgInEnv -> [DefArgInEnv]
forall a b. (a -> b) -> a -> b
$ Int -> NAPs -> IntMap DefArgInEnv -> IntMap DefArgInEnv
go Int
0 NAPs
ps IntMap DefArgInEnv
forall a. Monoid a => a
mempty where
            go :: Int -> NAPs -> IntMap DefArgInEnv -> IntMap DefArgInEnv
            go :: Int -> NAPs -> IntMap DefArgInEnv -> IntMap DefArgInEnv
go Int
i []     IntMap DefArgInEnv
acc = IntMap DefArgInEnv
acc
            go Int
i (NamedArg DeBruijnPattern
p:NAPs
ps) IntMap DefArgInEnv
acc =
              -- TODO: we get crappy GHC Core for Pattern' foldl'
              let acc' :: IntMap DefArgInEnv
acc' = (IntMap DefArgInEnv -> DBPatVar -> IntMap DefArgInEnv)
-> IntMap DefArgInEnv -> DeBruijnPattern -> IntMap DefArgInEnv
forall b a. (b -> a -> b) -> b -> Pattern' a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl'
                          (\IntMap DefArgInEnv
acc DBPatVar
j -> Int -> DefArgInEnv -> IntMap DefArgInEnv -> IntMap DefArgInEnv
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert (DBPatVar -> Int
dbPatVarIndex DBPatVar
j) (Int -> [Occurrence] -> DefArgInEnv
DefArgInEnv Int
i []) IntMap DefArgInEnv
acc)
                          IntMap DefArgInEnv
acc (Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> Named NamedName DeBruijnPattern -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern
forall e. Arg e -> e
unArg NamedArg DeBruijnPattern
p)
              in Int -> NAPs -> IntMap DefArgInEnv -> IntMap DefArgInEnv
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) NAPs
ps IntMap DefArgInEnv
acc'

      let items :: [DefArgInEnv]
items = NAPs -> [DefArgInEnv]
collectArgs NAPs
ps
      -- process body
      (OccEnv -> OccEnv)
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a.
(OccEnv -> OccEnv)
-> ReaderT OccEnv (TCMT IO) a -> ReaderT OccEnv (TCMT IO) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\OccEnv
env -> OccEnv
env {topDefArgs = items}) do
        Maybe Term -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences (Maybe Term -> ReaderT OccEnv (TCMT IO) ())
-> Maybe Term -> ReaderT OccEnv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
cl

-- | Occurrences in a sort.
--
--   The traversal stays on the level of sorts: we only descend into
--   subexpressions that are sorts themselves, or that are part of the identity
--   of the sort (the 'Level' of a universe, the eliminations of a stuck sort).
--   In particular we do /not/ descend into the 'Dom' of a 'PiSort': that is the
--   type of the domain, living one level below, and it is only stored in the
--   'PiSort' for context extension (see the documentation of 'PiSort').
instance ComputeOccurrences Sort where
  occurrences :: Sort' Term -> ReaderT OccEnv (TCMT IO) ()
occurrences Sort' Term
s = ((ReaderT OccEnv (TCMT IO) ()
  -> Result (ReaderT OccEnv (TCMT IO) ()))
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case Sort' Term
s of
    Univ Univ
_ Level' Term
l       -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ Level' Term -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Level' Term
l
    Inf Univ
_ Integer
_        -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Sort' Term
SizeUniv       -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Sort' Term
LockUniv       -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Sort' Term
LevelUniv      -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Sort' Term
IntervalUniv   -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    -- NB: we skip the domain type stored in the 'PiSort', see the note above.
    PiSort Dom' Term Term
_ Sort' Term
s1 Abs (Sort' Term)
s2 -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath)
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a. (OccursPath -> OccursPath) -> OccM a -> OccM a
underPath OccursPath -> OccursPath
LeftOfArrow (Sort' Term -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Sort' Term
s1) ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b.
ReaderT OccEnv (TCMT IO) a
-> ReaderT OccEnv (TCMT IO) b -> ReaderT OccEnv (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Abs (Sort' Term) -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Abs (Sort' Term)
s2
    FunSort Sort' Term
s1 Sort' Term
s2  -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath)
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a. (OccursPath -> OccursPath) -> OccM a -> OccM a
underPath OccursPath -> OccursPath
LeftOfArrow (Sort' Term -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Sort' Term
s1) ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b.
ReaderT OccEnv (TCMT IO) a
-> ReaderT OccEnv (TCMT IO) b -> ReaderT OccEnv (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort' Term -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Sort' Term
s2
    UnivSort Sort' Term
s     -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ Sort' Term -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Sort' Term
s
    -- @MetaS x es@ and @DefS q es@ are just the applications @x es@ and @q es@
    -- that happen to be sorts, so we reuse the corresponding 'Term' cases
    -- rather than duplicating the (subtle) treatment of eliminations.
    MetaS MetaId
x [Elim' Term]
es     -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ Term -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences (Term -> ReaderT OccEnv (TCMT IO) ())
-> Term -> ReaderT OccEnv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ MetaId -> [Elim' Term] -> Term
MetaV MetaId
x [Elim' Term]
es
    DefS QName
q [Elim' Term]
es      -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ Term -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences (Term -> ReaderT OccEnv (TCMT IO) ())
-> Term -> ReaderT OccEnv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ QName -> [Elim' Term] -> Term
Def QName
q [Elim' Term]
es
    DummyS ArgName
_       -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

instance ComputeOccurrences Level where
  occurrences :: Level' Term -> ReaderT OccEnv (TCMT IO) ()
occurrences (Max Integer
_ [PlusLevel' Term]
as) = [PlusLevel' Term] -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences [PlusLevel' Term]
as

instance ComputeOccurrences PlusLevel where
  occurrences :: PlusLevel' Term -> ReaderT OccEnv (TCMT IO) ()
occurrences (Plus Integer
_ Term
l) = Term -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Term
l

instance ComputeOccurrences Type where
  occurrences :: Type'' Term Term -> ReaderT OccEnv (TCMT IO) ()
occurrences (El Sort' Term
_ Term
v) = Term -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Term
v

instance ComputeOccurrences a => ComputeOccurrences (Tele a) where
  occurrences :: Tele a -> ReaderT OccEnv (TCMT IO) ()
occurrences Tele a
EmptyTel        = ReaderT OccEnv (TCMT IO) ()
forall a. Monoid a => a
mempty
  occurrences (ExtendTel a
a Abs (Tele a)
b) = a -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences a
a ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b.
ReaderT OccEnv (TCMT IO) a
-> ReaderT OccEnv (TCMT IO) b -> ReaderT OccEnv (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Abs (Tele a) -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Abs (Tele a)
b

instance ComputeOccurrences a => ComputeOccurrences (Abs a) where
  {-# INLINE occurrences #-}
  occurrences :: Abs a -> ReaderT OccEnv (TCMT IO) ()
occurrences = \case
    Abs ArgName
_ a
t   -> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a. OccM a -> OccM a
underBinder (ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ())
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ a -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences a
t
    NoAbs ArgName
_ a
t -> a -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences a
t

instance ComputeOccurrences a => ComputeOccurrences (Elim' a) where
  occurrences :: Elim' a -> ReaderT OccEnv (TCMT IO) ()
occurrences = \case
    Proj{}       -> ReaderT OccEnv (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    Apply Arg a
a      -> Arg a -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences Arg a
a
    IApply a
x a
y a
a -> a -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences a
x ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b.
ReaderT OccEnv (TCMT IO) a
-> ReaderT OccEnv (TCMT IO) b -> ReaderT OccEnv (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences a
y ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b.
ReaderT OccEnv (TCMT IO) a
-> ReaderT OccEnv (TCMT IO) b -> ReaderT OccEnv (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences a
a -- TODO Andrea: conservative

instance (ComputeOccurrences x, ComputeOccurrences a) => ComputeOccurrences (Boundary' x a) where
  occurrences :: Boundary' x a -> ReaderT OccEnv (TCMT IO) ()
occurrences = [(x, (a, a))] -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences ([(x, (a, a))] -> ReaderT OccEnv (TCMT IO) ())
-> (Boundary' x a -> [(x, (a, a))])
-> Boundary' x a
-> ReaderT OccEnv (TCMT IO) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Boundary' x a -> [(x, (a, a))]
forall x a. Boundary' x a -> [(x, (a, a))]
theBoundary

-- András 2026-02-18: CAUTION. Make sure to only use this instance if
-- there's no Path or Occurrence to be adjusted.
instance ComputeOccurrences a => ComputeOccurrences [a] where
  occurrences :: [a] -> ReaderT OccEnv (TCMT IO) ()
occurrences = \case
    []   -> () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    a
a:[a]
as -> a -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences a
a ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b.
ReaderT OccEnv (TCMT IO) a
-> ReaderT OccEnv (TCMT IO) b -> ReaderT OccEnv (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [a] -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences [a]
as

instance ComputeOccurrences a => ComputeOccurrences (Arg a)
instance ComputeOccurrences a => ComputeOccurrences (Dom a)
instance ComputeOccurrences a => ComputeOccurrences (Maybe a)

instance (ComputeOccurrences a, ComputeOccurrences b) => ComputeOccurrences (a, b) where
  {-# INLINE occurrences #-}
  occurrences :: (a, b) -> ReaderT OccEnv (TCMT IO) ()
occurrences (a
x, b
y) = a -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences a
x ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b.
ReaderT OccEnv (TCMT IO) a
-> ReaderT OccEnv (TCMT IO) b -> ReaderT OccEnv (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> b -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences b
y

instance ComputeOccurrences Int where
  {-# INLINE occurrences #-}
  occurrences :: Int -> ReaderT OccEnv (TCMT IO) ()
occurrences Int
_ = () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Compute occurrences in a given definition.
computeDefOccurrences :: QName -> Maybe [Clause] -> OccM ()
computeDefOccurrences :: QName -> Maybe [Clause] -> ReaderT OccEnv (TCMT IO) ()
computeDefOccurrences QName
q Maybe [Clause]
clauses = QName
-> (Definition -> ReaderT OccEnv (TCMT IO) ())
-> ReaderT OccEnv (TCMT IO) ()
forall (m :: * -> *) a.
HasConstInfo m =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q \Definition
def -> do
  ArgName -> Int -> TCMT IO Doc -> ReaderT OccEnv (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos" Int
25 do
    let a :: IsAbstract
a = Definition -> IsAbstract
defAbstract Definition
def
    m   <- Lens' TCEnv AbstractMode -> TCMT IO AbstractMode
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (AbstractMode -> f AbstractMode) -> TCEnv -> f TCEnv
Lens' TCEnv AbstractMode
eAbstractMode
    cur <- viewTC eCurrentModule
    o   <- viewTC eCurrentOpaqueId
    "computeOccurrences" <+> prettyTCM q <+> text (show a) <+> text (show o) <+> text (show m)
      <+> prettyTCM cur

  let paramsToDefArgs :: Telescope -> TCM [DefArgInEnv]
      paramsToDefArgs :: Tele (Dom' Term (Type'' Term Term)) -> TCM [DefArgInEnv]
paramsToDefArgs Tele (Dom' Term (Type'' Term Term))
tel = Int
-> [Dom' Term (ArgName, Type'' Term Term)]
-> [DefArgInEnv]
-> TCM [DefArgInEnv]
forall {t} {a}.
Int
-> [Dom' t (a, Type'' Term Term)]
-> [DefArgInEnv]
-> TCM [DefArgInEnv]
go Int
0 (Tele (Dom' Term (Type'' Term Term))
-> [Dom' Term (ArgName, Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom' Term (Type'' Term Term))
tel) [] where
        go :: Int
-> [Dom' t (a, Type'' Term Term)]
-> [DefArgInEnv]
-> TCM [DefArgInEnv]
go Int
i [Dom' t (a, Type'' Term Term)]
as [DefArgInEnv]
acc = ((TCM [DefArgInEnv] -> Result (TCM [DefArgInEnv]))
 -> Result (TCM [DefArgInEnv]))
-> TCM [DefArgInEnv]
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \TCM [DefArgInEnv] -> Result (TCM [DefArgInEnv])
ret -> case [Dom' t (a, Type'' Term Term)]
as of
          []   -> TCM [DefArgInEnv] -> Result (TCM [DefArgInEnv])
ret (TCM [DefArgInEnv] -> Result (TCM [DefArgInEnv]))
-> TCM [DefArgInEnv] -> Result (TCM [DefArgInEnv])
forall a b. (a -> b) -> a -> b
$ [DefArgInEnv] -> TCM [DefArgInEnv]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [DefArgInEnv]
acc
          Dom' t (a, Type'' Term Term)
a:[Dom' t (a, Type'' Term Term)]
as -> TCM [DefArgInEnv] -> Result (TCM [DefArgInEnv])
ret do occs <- Type'' Term Term -> TCM [Occurrence]
getOccurrencesFromType ((a, Type'' Term Term) -> Type'' Term Term
forall a b. (a, b) -> b
snd (Dom' t (a, Type'' Term Term) -> (a, Type'' Term Term)
forall t e. Dom' t e -> e
unDom Dom' t (a, Type'' Term Term)
a))
                         go (i + 1) as (DefArgInEnv i occs : acc)

  let defOcc :: Occurrence
defOcc = Definition -> Occurrence
mutualDefOcc Definition
def
  (OccursPath -> OccursPath)
-> Occurrence
-> ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathOcc (OccursPath -> QName -> OccursPath
`InDefOf` QName
q) Occurrence
defOcc (ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ())
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ ((ReaderT OccEnv (TCMT IO) ()
  -> Result (ReaderT OccEnv (TCMT IO) ()))
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case Definition -> Defn
theDef Definition
def of

    Function{} -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret do
      -- eta-expanded clauses are already computed by
      -- etaExpandFunctionClauses
      cs <- case Maybe [Clause]
clauses of
        Just [Clause]
cs -> [Clause] -> ReaderT OccEnv (TCMT IO) [Clause]
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Clause]
cs
        Maybe [Clause]
Nothing -> ReaderT OccEnv (TCMT IO) [Clause]
forall a. HasCallStack => a
__IMPOSSIBLE__

      performAnalysis <- lift $ optOccurrence <$> pragmaOptions
      if performAnalysis then do
        let clauses Int
i [a]
cs = ((ReaderT OccEnv (TCMT IO) ()
  -> Result (ReaderT OccEnv (TCMT IO) ()))
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case [a]
cs of
              []   -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
              a
c:[a]
cs -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath)
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a. (OccursPath -> OccursPath) -> OccM a -> OccM a
underPath (OccursPath -> Int -> OccursPath
`InClause` Int
i) (a -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences a
c) ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b.
ReaderT OccEnv (TCMT IO) a
-> ReaderT OccEnv (TCMT IO) b -> ReaderT OccEnv (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> [a] -> ReaderT OccEnv (TCMT IO) ()
clauses (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [a]
cs
        clauses 0 cs
      else case cs of
        []   -> ReaderT OccEnv (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__

        -- András 2026-02-18: this looks dodgy?
        Clause
cl:[Clause]
_ -> (OccursPath -> OccursPath)
-> Occurrence
-> ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathSetOcc OccursPath -> OccursPath
Matched Occurrence
Mixed do
          let go :: Int -> NAPs -> ReaderT OccEnv (TCMT IO) ()
go Int
i NAPs
ps = ((ReaderT OccEnv (TCMT IO) ()
  -> Result (ReaderT OccEnv (TCMT IO) ()))
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case NAPs
ps of
                []   -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                NamedArg DeBruijnPattern
_:NAPs
ps -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret do d <- (OccEnv -> QName) -> ReaderT OccEnv (TCMT IO) QName
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccEnv -> QName
topDef
                               addEdge noRange (ArgNode q i)
                               go (i + 1) ps
          Int -> NAPs -> ReaderT OccEnv (TCMT IO) ()
go Int
0 (Clause -> NAPs
namedClausePats Clause
cl)

    -- Andreas, 2026-08-29, issue #8696:
    -- A data or record type created by a module application (a /copy/) is
    -- defined by the pattern-less clause  @N.D = M.D args@.  As for function
    -- clauses (see 'preprocessMutuals') we have to eta-expand it, otherwise
    -- the analysis sees no occurrence of the parameters and indices of @N.D@
    -- and wrongly concludes that they are all 'Unused'.
    Datatype{dataClause :: Defn -> Maybe Clause
dataClause = Just Clause
c} -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ Clause -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences (Clause -> ReaderT OccEnv (TCMT IO) ())
-> ReaderT OccEnv (TCMT IO) Clause -> ReaderT OccEnv (TCMT IO) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM Clause -> ReaderT OccEnv (TCMT IO) Clause
forall (m :: * -> *) a. Monad m => m a -> ReaderT OccEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Clause -> TCM Clause
etaExpandCopyClause Clause
c)

    Datatype{dataPars :: Defn -> Int
dataPars = Int
np0, dataCons :: Defn -> [QName]
dataCons = [QName]
cs, dataTranspIx :: Defn -> Maybe QName
dataTranspIx = Maybe QName
trx} -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret do
      -- Andreas, 2013-02-27 (later edited by someone else): First,
      -- include each index of an inductive family.
      TelV telD _ <- TCM (TelV (Type'' Term Term))
-> ReaderT OccEnv (TCMT IO) (TelV (Type'' Term Term))
forall (m :: * -> *) a. Monad m => m a -> ReaderT OccEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (TelV (Type'' Term Term))
 -> ReaderT OccEnv (TCMT IO) (TelV (Type'' Term Term)))
-> TCM (TelV (Type'' Term Term))
-> ReaderT OccEnv (TCMT IO) (TelV (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TCM (TelV (Type'' Term Term))
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type'' Term Term -> m (TelV (Type'' Term Term))
telView (Type'' Term Term -> TCM (TelV (Type'' Term Term)))
-> Type'' Term Term -> TCM (TelV (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ Definition -> Type'' Term Term
defType Definition
def
      -- Andreas, 2017-04-26, issue #2554: count first index as parameter if it has type Size.
      -- We compute sizeIndex=1 if first first index has type Size, otherwise sizeIndex==0
      sizeIndex <- lift $ caseList (drop np0 $ telToList telD) (pure 0) \Dom' Term (ArgName, Type'' Term Term)
dom [Dom' Term (ArgName, Type'' Term Term)]
_ ->
                          TCMT IO (Maybe BoundedSize)
-> TCM Int -> (BoundedSize -> TCM Int) -> TCM Int
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Dom' Term (ArgName, Type'' Term Term)
-> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Dom' Term (ArgName, Type'' Term Term) -> m (Maybe BoundedSize)
isSizeType Dom' Term (ArgName, Type'' Term Term)
dom) (Int -> TCM Int
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
0) \BoundedSize
_ ->
                          Int -> TCM Int
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
1

      let np = Int
np0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
sizeIndex -- number of parameters

      -- add edge for size index, if it exists
      expand \ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret -> case Int
sizeIndex of
        Int
1 -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ Range -> Node -> ReaderT OccEnv (TCMT IO) ()
addEdge Range
forall a. Range' a
noRange (QName -> Int -> Node
ArgNode QName
q Int
np0)
        Int
_ -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret (ReaderT OccEnv (TCMT IO) ()
 -> Result (ReaderT OccEnv (TCMT IO) ()))
-> ReaderT OccEnv (TCMT IO) ()
-> Result (ReaderT OccEnv (TCMT IO) ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv (TCMT IO) ()
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

      -- add edges for indices
      underPathSetOcc InIndex Mixed $
        rangeM_ np (size telD - 1) \Int
i -> Range -> Node -> ReaderT OccEnv (TCMT IO) ()
addEdge Range
forall a. Range' a
noRange (QName -> Int -> Node
ArgNode QName
q Int
i)


      -- Then, we compute the occurrences in the constructor types.
      --------------------------------------------------------------------------------

      -- If the data type has a transport constructor (i.e. it's an
      -- indexed family in cubical mode) we should also consider it for
      -- positivity.
      cs <- maybe (pure cs) (\QName
c -> [QName] -> ReaderT OccEnv (TCMT IO) [QName]
forall a. a -> ReaderT OccEnv (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([QName]
cs [QName] -> [QName] -> [QName]
forall a. [a] -> [a] -> [a]
++! [QName
c])) trx
      forM_ cs \QName
c -> do
         -- Andreas, 2020-02-15, issue #4447:
         -- Allow UnconfimedReductions here to make sure we get the constructor type
         -- in same way as it was obtained when the data types was checked.
        (TelV tel t, bnd) <- TCM (TelV (Type'' Term Term), Boundary' Int Term)
-> ReaderT
     OccEnv (TCMT IO) (TelV (Type'' Term Term), Boundary' Int Term)
forall (m :: * -> *) a. Monad m => m a -> ReaderT OccEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (TelV (Type'' Term Term), Boundary' Int Term)
 -> ReaderT
      OccEnv (TCMT IO) (TelV (Type'' Term Term), Boundary' Int Term))
-> TCM (TelV (Type'' Term Term), Boundary' Int Term)
-> ReaderT
     OccEnv (TCMT IO) (TelV (Type'' Term Term), Boundary' Int Term)
forall a b. (a -> b) -> a -> b
$ AllowedReductions
-> TCM (TelV (Type'' Term Term), Boundary' Int Term)
-> TCM (TelV (Type'' Term Term), Boundary' Int Term)
forall (m :: * -> *) a.
MonadTCEnv m =>
AllowedReductions -> m a -> m a
putAllowedReductions AllowedReductions
allReductions (TCM (TelV (Type'' Term Term), Boundary' Int Term)
 -> TCM (TelV (Type'' Term Term), Boundary' Int Term))
-> TCM (TelV (Type'' Term Term), Boundary' Int Term)
-> TCM (TelV (Type'' Term Term), Boundary' Int Term)
forall a b. (a -> b) -> a -> b
$
                                    Type'' Term Term
-> TCM (TelV (Type'' Term Term), Boundary' Int Term)
forall (m :: * -> *).
PureTCM m =>
Type'' Term Term -> m (TelV (Type'' Term Term), Boundary' Int Term)
telViewPathBoundary (Type'' Term Term
 -> TCM (TelV (Type'' Term Term), Boundary' Int Term))
-> (Definition -> Type'' Term Term)
-> Definition
-> TCM (TelV (Type'' Term Term), Boundary' Int Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type'' Term Term
defType (Definition -> TCM (TelV (Type'' Term Term), Boundary' Int Term))
-> TCM Definition
-> TCM (TelV (Type'' Term Term), Boundary' Int Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCM Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
c
        let (tel0,tel1) = splitTelescopeAt np tel
        -- Do not collect occurrences in the data parameters.
        -- Normalization needed e.g. for test/succeed/Bush.agda.
        -- (Actually, for Bush.agda, reducing the parameters should be sufficient.)
        tel1' <- lift $ addContext tel0 $ normalise tel1
        pvars <- lift $ paramsToDefArgs tel0

        local (\OccEnv
env -> OccEnv
env {topDefArgs = pvars}) do
          -- edges in the types of constructor arguments
          underPath (`ConArgType` c) $ occurrences tel1'

          local (\OccEnv
env -> OccEnv
env {locals = size tel - np}) do

            -- edges in path boundary
            underPath (`ConEndpoint` c) $ occurrences bnd

            -- Occurrences in the indices of the data type the constructor targets.
            -- Andreas, 2020-02-15, issue #4447:
            -- WAS: @t@ is not necessarily a data type, but it could be something
            -- that reduces to a data type once UnconfirmedReductions are confirmed
            -- as safe by the termination checker.
            -- In any case, if @t@ is not showing itself as the data type, we need to
            -- do something conservative.  We will just collect *all* occurrences
            -- and flip their sign (variance) using 'LeftOfArrow'.
            case unEl t of
              Def QName
q' [Elim' Term]
vs
                | QName
q QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
q' -> do
                    let indices :: [Arg Term]
indices = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ [Elim' Term] -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims ([Elim' Term] -> Maybe [Arg Term])
-> [Elim' Term] -> Maybe [Arg Term]
forall a b. (a -> b) -> a -> b
$ Int -> [Elim' Term] -> [Elim' Term]
forall a. Int -> [a] -> [a]
drop Int
np [Elim' Term]
vs
                    (OccursPath -> OccursPath)
-> Occurrence
-> ReaderT OccEnv (TCMT IO) ()
-> ReaderT OccEnv (TCMT IO) ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathSetOcc (OccursPath -> QName -> OccursPath
`IndArgType` QName
c) Occurrence
Mixed (ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ())
-> ReaderT OccEnv (TCMT IO) () -> ReaderT OccEnv (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Arg Term] -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences [Arg Term]
indices
                | Bool
otherwise -> ReaderT OccEnv (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- this ought to be impossible now (but wasn't, see #4447)
              Pi{}       -> ReaderT OccEnv (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- eliminated  by telView
              MetaV{}    -> ReaderT OccEnv (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a constructor target; should have been solved by now
              Var{}      -> ReaderT OccEnv (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a constructor target
              Sort{}     -> ReaderT OccEnv (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a constructor target
              Lam{}      -> ReaderT OccEnv (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
              Lit{}      -> ReaderT OccEnv (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
              Con{}      -> ReaderT OccEnv (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
              Level{}    -> ReaderT OccEnv (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
              DontCare{} -> ReaderT OccEnv (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
              Dummy{}    -> ReaderT OccEnv (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- See the 'Datatype' case above for why we eta-expand.
    Record{recClause :: Defn -> Maybe Clause
recClause = Just Clause
c} -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret do
      Clause -> ReaderT OccEnv (TCMT IO) ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv (TCMT IO) ()
occurrences (Clause -> ReaderT OccEnv (TCMT IO) ())
-> ReaderT OccEnv (TCMT IO) Clause -> ReaderT OccEnv (TCMT IO) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM Clause -> ReaderT OccEnv (TCMT IO) Clause
forall (m :: * -> *) a. Monad m => m a -> ReaderT OccEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Clause -> TCM Clause
etaExpandCopyClause Clause
c)

    Record{recPars :: Defn -> Int
recPars = Int
np, recTel :: Defn -> Tele (Dom' Term (Type'' Term Term))
recTel = Tele (Dom' Term (Type'' Term Term))
tel} -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret do
      let (Tele (Dom' Term (Type'' Term Term))
tel0, Tele (Dom' Term (Type'' Term Term))
tel1) = Int
-> Tele (Dom' Term (Type'' Term Term))
-> (Tele (Dom' Term (Type'' Term Term)),
    Tele (Dom' Term (Type'' Term Term)))
splitTelescopeAt Int
np Tele (Dom' Term (Type'' Term Term))
tel
      pvars <- TCM [DefArgInEnv] -> ReaderT OccEnv (TCMT IO) [DefArgInEnv]
forall (m :: * -> *) a. Monad m => m a -> ReaderT OccEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM [DefArgInEnv] -> ReaderT OccEnv (TCMT IO) [DefArgInEnv])
-> TCM [DefArgInEnv] -> ReaderT OccEnv (TCMT IO) [DefArgInEnv]
forall a b. (a -> b) -> a -> b
$ Tele (Dom' Term (Type'' Term Term)) -> TCM [DefArgInEnv]
paramsToDefArgs Tele (Dom' Term (Type'' Term Term))
tel0
      local (\OccEnv
env -> OccEnv
env {topDefArgs = pvars}) do
        occurrences =<< liftTCM (addContext tel0 (normalise tel1))
        -- Andreas, 2017-01-01, issue #1899, treat like data types

    -- Arguments to other kinds of definitions are hard-wired.
    Constructor{}      -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret ReaderT OccEnv (TCMT IO) ()
forall a. Monoid a => a
mempty
    Axiom{}            -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret ReaderT OccEnv (TCMT IO) ()
forall a. Monoid a => a
mempty
    DataOrRecSig{}     -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret ReaderT OccEnv (TCMT IO) ()
forall a. Monoid a => a
mempty
    Primitive{}        -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret ReaderT OccEnv (TCMT IO) ()
forall a. Monoid a => a
mempty
    PrimitiveSort{}    -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret ReaderT OccEnv (TCMT IO) ()
forall a. Monoid a => a
mempty
    GeneralizableVar{} -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret ReaderT OccEnv (TCMT IO) ()
forall a. Monoid a => a
mempty
    AbstractDefn{}     -> ReaderT OccEnv (TCMT IO) () -> Result (ReaderT OccEnv (TCMT IO) ())
ret ReaderT OccEnv (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Prepare the defining clause of a data or record type copy (issue #8696)
--   for occurrence analysis by eta-expanding it, so that the parameters and
--   indices of the copy appear as pattern variables in the clause.
etaExpandCopyClause :: Clause -> TCM Clause
etaExpandCopyClause :: Clause -> TCM Clause
etaExpandCopyClause Clause
c = (Int, Clause) -> Clause
forall a b. (a, b) -> b
snd ((Int, Clause) -> Clause) -> TCMT IO (Int, Clause) -> TCM Clause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Clause -> TCMT IO (Int, Clause)
forall (tcm :: * -> *). PureTCM tcm => Clause -> tcm (Int, Clause)
etaExpandClause (Clause -> TCMT IO (Int, Clause))
-> TCM Clause -> TCMT IO (Int, Clause)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Clause -> TCM Clause
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Clause
c)

-- | Pre-pass that eta-expands function clauses and records the "formal arity" of the function in
--   the signature. Any argument beyond this arity is considered to have 'Mixed' polarity.
--   The analysis does not compute terms (or types) and cannot see arities that depend on argument values,
--   it can only look at arities of eta-expanded definition clauses.
--   See also issue 8564.
--   We return the original names paired with the eta-expanded clauses.
--   We also build up 'Mutuals' and record arities for each QName.
--   A definition that's not a Function gets @maxBound@ for arity.
preprocessMutuals :: [QName] -> Mutuals -> TCM [(QName, Maybe [Clause])]
preprocessMutuals :: [QName]
-> HashTable MVector QName MVector Int
-> TCM [(QName, Maybe [Clause])]
preprocessMutuals [QName]
qs HashTable MVector QName MVector Int
mutuals = [QName]
-> (QName -> TCMT IO (QName, Maybe [Clause]))
-> TCM [(QName, Maybe [Clause])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [QName]
qs \QName
q -> QName
-> (Definition -> TCMT IO (QName, Maybe [Clause]))
-> TCMT IO (QName, Maybe [Clause])
forall (m :: * -> *) a.
HasConstInfo m =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q \Definition
def -> case Definition -> Defn
theDef Definition
def of

  -- Postulates and primities are taken to be external to the mutual block.
  -- User-given polarity pragmas may influence occurrence computation
  -- in their arguments, but that's it.
  Axiom{}     -> (QName, Maybe [Clause]) -> TCMT IO (QName, Maybe [Clause])
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName
q, Maybe [Clause]
forall a. Maybe a
Nothing)
  Primitive{} -> (QName, Maybe [Clause]) -> TCMT IO (QName, Maybe [Clause])
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName
q, Maybe [Clause]
forall a. Maybe a
Nothing)

  Function {funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs} -> do
    cs <- (Clause -> TCMT IO (Int, Clause))
-> [Clause] -> TCMT IO [(Int, Clause)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Clause -> TCMT IO (Int, Clause)
forall (tcm :: * -> *). PureTCM tcm => Clause -> tcm (Int, Clause)
etaExpandClause ([Clause] -> TCMT IO [(Int, Clause)])
-> TCMT IO [Clause] -> TCMT IO [(Int, Clause)]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Clause] -> TCMT IO [Clause]
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull [Clause]
cs
    let !arity   = case [(Int, Clause)]
cs of []       -> Int
0
                              (Int
c,Clause
_):[(Int, Clause)]
cs -> (Int -> (Int, Clause) -> Int) -> Int -> [(Int, Clause)] -> Int
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Int
acc (Int
arity, Clause
_) -> Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
acc Int
arity) Int
c [(Int, Clause)]
cs
    let !clauses = ((Int, Clause) -> Clause) -> [(Int, Clause)] -> [Clause]
forall a b. (a -> b) -> [a] -> [b]
map' (Int, Clause) -> Clause
forall a b. (a, b) -> b
snd [(Int, Clause)]
cs
    lift $ insertMutual mutuals q arity

    reportSDoc "tc.pos.preprocess" 30 $
      "added function" <+> prettyTCM q <+> "to mutual block with arity" <+> pretty arity
    pure (q, Just clauses)

  Defn
_ -> do
    ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.preprocess" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"added definition" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"to mutual block"
    IO () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => m a -> TCMT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> TCMT IO ()) -> IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ HashTable MVector QName MVector Int -> QName -> Int -> IO ()
insertMutual HashTable MVector QName MVector Int
mutuals QName
q Int
forall a. Bounded a => a
maxBound
    (QName, Maybe [Clause]) -> TCMT IO (QName, Maybe [Clause])
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName
q, Maybe [Clause]
forall a. Maybe a
Nothing)

buildOccurrenceGraph :: [QName] -> TCM (OccGraph, Mutuals)
buildOccurrenceGraph :: [QName] -> TCM (OccGraph, HashTable MVector QName MVector Int)
buildOccurrenceGraph [QName]
qs = do
  inf <- Maybe QName
-> (CoinductionKit -> Maybe QName)
-> Maybe CoinductionKit
-> Maybe QName
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe QName
forall a. Maybe a
Nothing (\CoinductionKit
x -> QName -> Maybe QName
forall a. a -> Maybe a
Just (QName -> Maybe QName) -> QName -> Maybe QName
forall a b. (a -> b) -> a -> b
$! CoinductionKit -> QName
nameOfInf CoinductionKit
x) (Maybe CoinductionKit -> Maybe QName)
-> TCMT IO (Maybe CoinductionKit) -> TCMT IO (Maybe QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Maybe CoinductionKit)
coinductionKit
  so  <- sortOccurrence

  mutuals <- lift HT.empty
  qs      <- preprocessMutuals qs mutuals

  graph <- lift HT.empty
  TCM \IORef TCState
st TCEnv
tce -> [(QName, Maybe [Clause])]
-> ((QName, Maybe [Clause]) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(QName, Maybe [Clause])]
qs \(QName
q, Maybe [Clause]
clauses) -> do
    let env :: OccEnv
env = QName
-> [DefArgInEnv]
-> Maybe QName
-> Occurrence
-> Int
-> HashTable MVector QName MVector Int
-> Node
-> OccursPath
-> Occurrence
-> OccGraph
-> OccEnv
OccEnv QName
q [] Maybe QName
inf Occurrence
so Int
0 HashTable MVector QName MVector Int
mutuals (QName -> Node
DefNode QName
q) OccursPath
Root Occurrence
StrictPos OccGraph
graph
    TCMT IO () -> IORef TCState -> TCEnv -> IO ()
forall (m :: * -> *) a. TCMT m a -> IORef TCState -> TCEnv -> m a
unTCM (ReaderT OccEnv (TCMT IO) () -> OccEnv -> TCMT IO ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (QName -> Maybe [Clause] -> ReaderT OccEnv (TCMT IO) ()
computeDefOccurrences QName
q Maybe [Clause]
clauses) OccEnv
env) IORef TCState
st TCEnv
tce

  pure (graph, mutuals)

-- Computing transitive occurrences, to be used in positivity checking
----------------------------------------------------------------------------------------------------

data Seen = Seen Node Occurrence
  deriving (Seen -> Seen -> Bool
(Seen -> Seen -> Bool) -> (Seen -> Seen -> Bool) -> Eq Seen
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Seen -> Seen -> Bool
== :: Seen -> Seen -> Bool
$c/= :: Seen -> Seen -> Bool
/= :: Seen -> Seen -> Bool
Eq, Int -> Seen -> ShowS
[Seen] -> ShowS
Seen -> ArgName
(Int -> Seen -> ShowS)
-> (Seen -> ArgName) -> ([Seen] -> ShowS) -> Show Seen
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Seen -> ShowS
showsPrec :: Int -> Seen -> ShowS
$cshow :: Seen -> ArgName
show :: Seen -> ArgName
$cshowList :: [Seen] -> ShowS
showList :: [Seen] -> ShowS
Show)

instance Hashable Seen where
  hashWithSalt :: Int -> Seen -> Int
hashWithSalt Int
h (Seen Node
x Occurrence
y) =
    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 -> Node -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
h Node
x) Word -> Word -> Word
`combineWord` Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Occurrence -> Int
forall a. Enum a => a -> Int
fromEnum Occurrence
y))

-- | Set of visited nodes during graph search.
type SeenNodes = HT.HashTableLL Seen ()

memberSeen :: Seen -> SeenNodes -> IO Bool
memberSeen :: Seen -> SeenNodes -> IO Bool
memberSeen Seen
x SeenNodes
map = SeenNodes -> Seen -> IO (Maybe ())
forall k (ks :: * -> * -> *) (vs :: * -> * -> *) v.
(Hashable k, MVector ks k, MVector vs v) =>
HashTable ks k vs v -> k -> IO (Maybe v)
HT.lookup SeenNodes
map Seen
x IO (Maybe ()) -> (Maybe () -> IO Bool) -> IO Bool
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Maybe ()
Nothing -> Bool -> IO Bool
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
  Maybe ()
_       -> Bool -> IO Bool
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True

{-# NOINLINE insertSeen #-}
insertSeen :: Seen -> SeenNodes -> IO ()
insertSeen :: Seen -> SeenNodes -> IO ()
insertSeen Seen
x SeenNodes
map = SeenNodes -> Seen -> () -> IO ()
forall k (vs :: * -> * -> *) v (ks :: * -> * -> *).
(Hashable k, MVector vs v, MVector ks k) =>
HashTable ks k vs v -> k -> v -> IO ()
HT.insert SeenNodes
map Seen
x ()

-- | Exception for short-circuiting when finding a Mixed path from source to target.
instance Exception Occurrence

-- | Search for transitive occurrences through the occurrence graph. We compute the 'oplus' sum of
--   all paths from the source to the target. This is not as bad as it sounds, becuse a) we can
--   short-circuit a search when a 'Mixed' path is found b) only 4 possible 'Occurrences' remain,
--   (discounting 'Mixed' and 'Unused') and we can use a DFS where each node is visited at most 4
--   times, for each 'Occurence' of the path to the node from the source.
transitiveOccurrence :: OccGraph -> Node -> Node -> IO Occurrence
transitiveOccurrence :: OccGraph -> Node -> Node -> IO Occurrence
transitiveOccurrence OccGraph
graph Node
src Node
tgt = do

      -- Function for visiting a node.
  let go :: OccGraph -> Node -> Node -> Occurrence -> Occurrence -> SeenNodes -> IO Occurrence
      go :: OccGraph
-> Node
-> Node
-> Occurrence
-> Occurrence
-> SeenNodes
-> IO Occurrence
go OccGraph
graph Node
tgt Node
src Occurrence
path Occurrence
acc SeenNodes
seen = do
        let s :: Seen
s = Node -> Occurrence -> Seen
Seen Node
src Occurrence
path
        Seen -> SeenNodes -> IO Bool
memberSeen Seen
s SeenNodes
seen IO Bool -> (Bool -> IO Occurrence) -> IO Occurrence
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Bool
True  -> Occurrence -> IO Occurrence
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Occurrence
acc
          Bool
False -> do
            Seen -> SeenNodes -> IO ()
insertSeen Seen
s SeenNodes
seen
            if Node
src Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
tgt then
              case Occurrence -> Occurrence -> Occurrence
forall a. SemiRing a => a -> a -> a
oplus Occurrence
path Occurrence
acc of
                Occurrence
Mixed -> Occurrence -> IO Occurrence
forall e a. (HasCallStack, Exception e) => e -> IO a
throwIO Occurrence
Mixed  -- Mixed path found, abort search
                Occurrence
acc   -> OccGraph
-> Node
-> Node
-> Occurrence
-> Occurrence
-> SeenNodes
-> IO Occurrence
go' OccGraph
graph Node
tgt Node
src Occurrence
path Occurrence
acc SeenNodes
seen
            else
              OccGraph
-> Node
-> Node
-> Occurrence
-> Occurrence
-> SeenNodes
-> IO Occurrence
go' OccGraph
graph Node
tgt Node
src Occurrence
path Occurrence
acc SeenNodes
seen

      -- Function for visiting the children of a node
      go' :: OccGraph -> Node -> Node -> Occurrence -> Occurrence -> SeenNodes -> IO Occurrence
      go' :: OccGraph
-> Node
-> Node
-> Occurrence
-> Occurrence
-> SeenNodes
-> IO Occurrence
go' OccGraph
graph Node
tgt Node
src Occurrence
path Occurrence
acc SeenNodes
seen = Node
-> OccGraph
-> (NodeMap (Edge OccursWhere) -> IO Occurrence)
-> IO Occurrence
-> IO Occurrence
forall v a. Node -> NodeMap v -> (v -> IO a) -> IO a -> IO a
lookupNode Node
src OccGraph
graph
        (\NodeMap (Edge OccursWhere)
map -> Node
-> NodeMap (Edge OccursWhere)
-> (Edge OccursWhere -> IO Occurrence)
-> IO Occurrence
-> IO Occurrence
forall v a. Node -> NodeMap v -> (v -> IO a) -> IO a -> IO a
lookupNode Node
tgt NodeMap (Edge OccursWhere)
map
          -- if there's a direct edge to the target, we follow that first.
          -- this should make it faster to find Mixed edges (if there's one)
          (\(Edge Occurrence
occ OccursWhere
_) -> do
            acc <- OccGraph
-> Node
-> Node
-> Occurrence
-> Occurrence
-> SeenNodes
-> IO Occurrence
go OccGraph
graph Node
tgt Node
tgt (Occurrence -> Occurrence -> Occurrence
forall a. SemiRing a => a -> a -> a
otimes Occurrence
path Occurrence
occ) Occurrence
acc SeenNodes
seen
            goMap graph tgt map path acc seen)

          (OccGraph
-> Node
-> NodeMap (Edge OccursWhere)
-> Occurrence
-> Occurrence
-> SeenNodes
-> IO Occurrence
goMap OccGraph
graph Node
tgt NodeMap (Edge OccursWhere)
map Occurrence
path Occurrence
acc SeenNodes
seen))

        (Occurrence -> IO Occurrence
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Occurrence
acc)

      -- Function for traversing the map of children for a node
      goMap :: OccGraph -> Node -> NodeMap (Edge OccursWhere) -> Occurrence -> Occurrence -> SeenNodes -> IO Occurrence
      goMap :: OccGraph
-> Node
-> NodeMap (Edge OccursWhere)
-> Occurrence
-> Occurrence
-> SeenNodes
-> IO Occurrence
goMap OccGraph
graph Node
tgt NodeMap (Edge OccursWhere)
map Occurrence
path Occurrence
acc SeenNodes
seen =
        NodeMap (Edge OccursWhere)
-> Occurrence
-> (Node -> Edge OccursWhere -> Occurrence -> IO Occurrence)
-> IO Occurrence
forall (ks :: * -> * -> *) k (vs :: * -> * -> *) v acc.
(MVector ks k, MVector vs v) =>
HashTable ks k vs v -> acc -> (k -> v -> acc -> IO acc) -> IO acc
HT.forAssocsAccum NodeMap (Edge OccursWhere)
map Occurrence
acc \Node
src (Edge Occurrence
occ OccursWhere
_) Occurrence
acc ->
          if Node
src Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
tgt then Occurrence -> IO Occurrence
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Occurrence
acc -- already covered this case in go'
                        else OccGraph
-> Node
-> Node
-> Occurrence
-> Occurrence
-> SeenNodes
-> IO Occurrence
go OccGraph
graph Node
tgt Node
src (Occurrence -> Occurrence -> Occurrence
forall a. SemiRing a => a -> a -> a
otimes Occurrence
path Occurrence
occ) Occurrence
acc SeenNodes
seen

  seen <- IO SeenNodes
forall (ks :: * -> * -> *) k (vs :: * -> * -> *) v.
(MVector ks k, MVector vs v) =>
IO (HashTable ks k vs v)
HT.empty
  go' graph tgt src StrictPos Unused seen `catch` pure