{-# 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 (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

{-# NOINLINE isMutual #-}
isMutual :: QName -> OccM Bool
isMutual :: QName -> OccM Bool
isMutual QName
q = do
  mutuals <- (OccEnv -> HashTable MVector QName MVector ())
-> ReaderT OccEnv TCM (HashTable MVector QName MVector ())
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccEnv -> HashTable MVector QName MVector ()
mutuals
  lift $ lift $ HT.hasKey mutuals q

{-# NOINLINE insertMutual #-}
insertMutual :: Mutuals -> QName -> IO ()
insertMutual :: HashTable MVector QName MVector () -> QName -> IO ()
insertMutual HashTable MVector QName MVector ()
muts QName
q = HashTable MVector QName MVector () -> QName -> () -> 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 ()
muts QName
q ()

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

-- | Set of mutual definition names in the block.
type Mutuals = HT.HashTableLU QName ()

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 -> Int
locals     :: Int           -- ^ Number of local binders (on the top of the definition args).
  , OccEnv -> HashTable MVector QName MVector ()
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 TCM a -> ReaderT OccEnv TCM a
forall a.
(OccEnv -> OccEnv) -> ReaderT OccEnv TCM a -> ReaderT OccEnv TCM 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 TCM a -> ReaderT OccEnv TCM a
forall a.
(OccEnv -> OccEnv) -> ReaderT OccEnv TCM a -> ReaderT OccEnv TCM 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 TCM a -> ReaderT OccEnv TCM a
forall a.
(OccEnv -> OccEnv) -> ReaderT OccEnv TCM a -> ReaderT OccEnv TCM 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 TCM a -> ReaderT OccEnv TCM a
forall a.
(OccEnv -> OccEnv) -> ReaderT OccEnv TCM a -> ReaderT OccEnv TCM 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 TCM a -> ReaderT OccEnv TCM a
forall a.
(OccEnv -> OccEnv) -> ReaderT OccEnv TCM a -> ReaderT OccEnv TCM 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 -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) TCM 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)

addEdge :: Range -> Node -> OccM ()
addEdge :: Range -> Node -> ReaderT OccEnv TCM ()
addEdge Range
rng Node
src = do
  target <- (OccEnv -> Node) -> ReaderT OccEnv TCM 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 TCM () -> Result (ReaderT OccEnv TCM ())
ret -> case Occurrence
occ of
    Occurrence
Unused -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Occurrence
occ    -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
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 TCM ()
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 TCM ())
-> TCMT IO () -> ReaderT OccEnv TCM ()
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 TCM ()
occurrencesInDefArg QName
d Occurrence
p Int
i Elim' Term
e = ((ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
 -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret -> case Occurrence
p of
  Occurrence
Unused -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Occurrence
p      -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath)
-> Occurrence -> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
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 TCM () -> ReaderT OccEnv TCM ())
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a b. (a -> b) -> a -> b
$ Elim' Term -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
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 TCM ()
occurrencesInDefArgArg Occurrence
p Int
i Elim' Term
e = ((ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
 -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret -> case Occurrence
p of
  Occurrence
Unused -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Occurrence
p      -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath)
-> Occurrence -> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
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 TCM () -> ReaderT OccEnv TCM ())
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a b. (a -> b) -> a -> b
$ Elim' Term -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
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 TCM ()
occurrencesInMutDefArg QName
d Occurrence
p Int
i Elim' Term
e = ((ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
 -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret -> case Occurrence
p of
  Occurrence
Unused -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Occurrence
p      -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ (OccEnv -> OccEnv)
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a.
(OccEnv -> OccEnv) -> ReaderT OccEnv TCM a -> ReaderT OccEnv TCM 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 TCM () -> ReaderT OccEnv TCM ())
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a b. (a -> b) -> a -> b
$
                    Elim' Term -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences Elim' Term
e

-- | 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
  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 TCM ()) -> t b -> ReaderT OccEnv TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ b -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences

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

    Var Int
x [Elim' Term]
es -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret do
      locals <- (OccEnv -> Int) -> ReaderT OccEnv TCM 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 TCM () -> Result (ReaderT OccEnv TCM ()))
 -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret -> case [a]
es of
              []   -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
              a
e:[a]
es -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath)
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
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 TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences a
e) ReaderT OccEnv TCM ()
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a b.
ReaderT OccEnv TCM a
-> ReaderT OccEnv TCM b -> ReaderT OccEnv TCM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> [a] -> ReaderT OccEnv TCM ()
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 TCM () -> Result (ReaderT OccEnv TCM ()))
 -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret -> case ([Occurrence]
ps, [Elim' Term]
es) of
              ([Occurrence]
_   , []  ) -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
              ([]  , Elim' Term
e:[Elim' Term]
es) -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ Occurrence -> Int -> Elim' Term -> ReaderT OccEnv TCM ()
occurrencesInDefArgArg Occurrence
Mixed Int
i Elim' Term
e ReaderT OccEnv TCM ()
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a b.
ReaderT OccEnv TCM a
-> ReaderT OccEnv TCM b -> ReaderT OccEnv TCM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> [Occurrence] -> [Elim' Term] -> ReaderT OccEnv TCM ()
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 TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ Occurrence -> Int -> Elim' Term -> ReaderT OccEnv TCM ()
occurrencesInDefArgArg Occurrence
p Int
i Elim' Term
e     ReaderT OccEnv TCM ()
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a b.
ReaderT OccEnv TCM a
-> ReaderT OccEnv TCM b -> ReaderT OccEnv TCM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> [Occurrence] -> [Elim' Term] -> ReaderT OccEnv TCM ()
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 TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ (OccEnv -> Maybe QName) -> ReaderT OccEnv TCM (Maybe QName)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccEnv -> Maybe QName
inf ReaderT OccEnv TCM (Maybe QName)
-> (Maybe QName -> ReaderT OccEnv TCM ()) -> ReaderT OccEnv TCM ()
forall a b.
ReaderT OccEnv TCM a
-> (a -> ReaderT OccEnv TCM b) -> ReaderT OccEnv TCM 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 TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        [Elim' Term
_]    -> () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- unused arg
        [Elim' Term
_, Elim' Term
e] -> (OccursPath -> OccursPath)
-> Occurrence -> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathOcc OccursPath -> OccursPath
UnderInf Occurrence
GuardPos (ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ())
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a b. (a -> b) -> a -> b
$ Elim' Term -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences Elim' Term
e
        [Elim' Term]
_      -> ReaderT OccEnv TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

      Maybe QName
_ -> do
        isMut <- QName -> OccM Bool
isMutual QName
d
        expand \ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret -> case Bool
isMut of

          -- it's a mutual definition
          Bool
True -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret do
            Range -> Node -> ReaderT OccEnv TCM ()
addEdge (QName -> Range
forall a. HasRange a => a -> Range
getRange QName
d) (QName -> Node
DefNode QName
d)
            ((ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
 -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret -> case [Elim' Term]
es of
              [] -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()  -- we skip the mutualDefOcc in this case
              [Elim' Term]
es -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret do
                let elims :: QName -> Occurrence -> Int -> [Elim' Term] -> ReaderT OccEnv TCM ()
elims QName
d Occurrence
p Int
i [Elim' Term]
es = ((ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
 -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret -> case [Elim' Term]
es of
                      []   -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                      Elim' Term
e:[Elim' Term]
es -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret do QName -> Occurrence -> Int -> Elim' Term -> ReaderT OccEnv TCM ()
occurrencesInMutDefArg QName
d Occurrence
p Int
i Elim' Term
e
                                     QName -> Occurrence -> Int -> [Elim' Term] -> ReaderT OccEnv TCM ()
elims QName
d Occurrence
p (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Elim' Term]
es

                defOcc <- TCM Occurrence -> ReaderT OccEnv TCM 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 (Definition -> Occurrence
mutualDefOcc (Definition -> Occurrence) -> TCM Definition -> TCM Occurrence
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d)
                elims d defOcc 0 es

          -- it's not a mutual definition, we use existing defArgOccurrences
          -- in each argument in the Elims
          Bool
False -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret do
            def <- TCM Definition -> ReaderT OccEnv TCM 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 TCM Definition)
-> TCM Definition -> ReaderT OccEnv TCM 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 TCM ()
elims Int
i [Elim' Term]
es = ((ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
 -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret -> case [Elim' Term]
es of
                      []   -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                      Elim' Term
e:[Elim' Term]
es -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret do QName -> Occurrence -> Int -> Elim' Term -> ReaderT OccEnv TCM ()
occurrencesInDefArg QName
d Occurrence
StrictPos Int
i Elim' Term
e
                                     Int -> [Elim' Term] -> ReaderT OccEnv TCM ()
elims (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Elim' Term]
es
                Int -> [Elim' Term] -> ReaderT OccEnv TCM ()
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 TCM ()
elims' QName
d Int
i [Occurrence]
ps [Elim' Term]
es = ((ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
 -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret -> case ([Occurrence]
ps, [Elim' Term]
es) of
                      ([Occurrence]
_   , []  ) -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                      (Occurrence
p:[Occurrence]
ps, Elim' Term
e:[Elim' Term]
es) -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret do QName -> Occurrence -> Int -> Elim' Term -> ReaderT OccEnv TCM ()
occurrencesInDefArg QName
d Occurrence
p Int
i Elim' Term
e
                                             QName
-> Int -> [Occurrence] -> [Elim' Term] -> ReaderT OccEnv TCM ()
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 TCM () -> Result (ReaderT OccEnv TCM ())
ret do QName -> Occurrence -> Int -> Elim' Term -> ReaderT OccEnv TCM ()
occurrencesInDefArg QName
d Occurrence
Mixed Int
i Elim' Term
e
                                             QName
-> Int -> [Occurrence] -> [Elim' Term] -> ReaderT OccEnv TCM ()
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 TCM ()
elims QName
d Type'' Term Term
a Int
i [Occurrence]
ps [Elim' Term]
es = ((ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
 -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret -> case ([Occurrence]
ps, [Elim' Term]
es) of
                      ([Occurrence]
_   , []  ) -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                      (Occurrence
p:[Occurrence]
ps, Elim' Term
e:[Elim' Term]
es) -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret do QName -> Occurrence -> Int -> Elim' Term -> ReaderT OccEnv TCM ()
occurrencesInDefArg QName
d Occurrence
p Int
i Elim' Term
e
                                             QName
-> Type'' Term Term
-> Int
-> [Occurrence]
-> [Elim' Term]
-> ReaderT OccEnv TCM ()
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 TCM () -> Result (ReaderT OccEnv TCM ())
ret do ps <- TCM [Occurrence] -> ReaderT OccEnv TCM [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 TCM [Occurrence])
-> TCM [Occurrence] -> ReaderT OccEnv TCM [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 TCM () -> ReaderT OccEnv TCM ()
forall a. Occurrence -> OccM a -> OccM a
underOcc Occurrence
defOcc (ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ())
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a b. (a -> b) -> a -> b
$ QName
-> Type'' Term Term
-> Int
-> [Occurrence]
-> [Elim' Term]
-> ReaderT OccEnv TCM ()
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 TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ [Elim' Term] -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences [Elim' Term]
es
    MetaV MetaId
m [Elim' Term]
es -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath)
-> Occurrence -> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathSetOcc OccursPath -> OccursPath
MetaArg Occurrence
Mixed ([Elim' Term] -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences [Elim' Term]
es)
    Pi Dom' Term (Type'' Term Term)
a Abs (Type'' Term Term)
b     -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath)
-> Occurrence -> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathOcc OccursPath -> OccursPath
LeftOfArrow Occurrence
JustNeg (Dom' Term (Type'' Term Term) -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences Dom' Term (Type'' Term Term)
a) ReaderT OccEnv TCM ()
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a b.
ReaderT OccEnv TCM a
-> ReaderT OccEnv TCM b -> ReaderT OccEnv TCM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Abs (Type'' Term Term) -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences Abs (Type'' Term Term)
b
    Lam ArgInfo
_ Abs Term
t    -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ Abs Term -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences Abs Term
t
    Level Level' Term
l    -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ Level' Term -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences Level' Term
l
    Lit{}      -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Sort{}     -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    -- 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 TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ Term -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences Term
t
    Dummy{}    -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM 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 TCM ()
addClauseArgMatches NAPs
ps = (OccursPath -> OccursPath)
-> Occurrence -> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathSetOcc OccursPath -> OccursPath
Matched Occurrence
Mixed (ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ())
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> NAPs -> ReaderT OccEnv TCM ()
go Int
0 NAPs
ps where
  go :: Int -> NAPs -> OccM ()
  go :: Int -> NAPs -> ReaderT OccEnv TCM ()
go Int
i NAPs
ps = ((ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
 -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret -> case NAPs
ps of
    []   -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    NamedArg DeBruijnPattern
p:NAPs
ps -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret do
      TCM Bool -> OccM 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 -> TCM 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)) OccM Bool
-> (Bool -> ReaderT OccEnv TCM ()) -> ReaderT OccEnv TCM ()
forall a b.
ReaderT OccEnv TCM a
-> (a -> ReaderT OccEnv TCM b) -> ReaderT OccEnv TCM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Bool
True  -> do topDef <- (OccEnv -> QName) -> ReaderT OccEnv TCM 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 TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      Int -> NAPs -> ReaderT OccEnv TCM ()
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 TCM ()
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 TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    else do
      -- add edges for matched args
      NAPs -> ReaderT OccEnv TCM ()
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 TCM () -> ReaderT OccEnv TCM ()
forall a.
(OccEnv -> OccEnv) -> ReaderT OccEnv TCM a -> ReaderT OccEnv TCM 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 TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences (Maybe Term -> ReaderT OccEnv TCM ())
-> Maybe Term -> ReaderT OccEnv TCM ()
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
cl

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

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

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

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

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

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

instance (ComputeOccurrences x, ComputeOccurrences a) => ComputeOccurrences (Boundary' x a) where
  occurrences :: Boundary' x a -> ReaderT OccEnv TCM ()
occurrences = [(x, (a, a))] -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences ([(x, (a, a))] -> ReaderT OccEnv TCM ())
-> (Boundary' x a -> [(x, (a, a))])
-> Boundary' x a
-> ReaderT OccEnv TCM ()
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 TCM ()
occurrences = \case
    []   -> () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    a
a:[a]
as -> a -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences a
a ReaderT OccEnv TCM ()
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a b.
ReaderT OccEnv TCM a
-> ReaderT OccEnv TCM b -> ReaderT OccEnv TCM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [a] -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
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 TCM ()
occurrences (a
x, b
y) = a -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences a
x ReaderT OccEnv TCM ()
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a b.
ReaderT OccEnv TCM a
-> ReaderT OccEnv TCM b -> ReaderT OccEnv TCM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> b -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences b
y

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

-- | Compute occurrences in a given definition.
computeDefOccurrences :: QName -> OccM ()
computeDefOccurrences :: QName -> ReaderT OccEnv TCM ()
computeDefOccurrences QName
q = QName
-> (Definition -> ReaderT OccEnv TCM ()) -> ReaderT OccEnv TCM ()
forall (m :: * -> *) a.
HasConstInfo m =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q \Definition
def -> do
  ArgName -> Int -> TCMT IO Doc -> ReaderT OccEnv TCM ()
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 TCM () -> ReaderT OccEnv TCM ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathOcc (OccursPath -> QName -> OccursPath
`InDefOf` QName
q) Occurrence
defOcc (ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ())
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a b. (a -> b) -> a -> b
$ ((ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
 -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret -> case Definition -> Defn
theDef Definition
def of

    Function{funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs} -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret do

      cs <- TCM [Clause] -> ReaderT OccEnv TCM [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 (TCM [Clause] -> ReaderT OccEnv TCM [Clause])
-> TCM [Clause] -> ReaderT OccEnv TCM [Clause]
forall a b. (a -> b) -> a -> b
$ (Clause -> TCMT IO Clause) -> [Clause] -> TCM [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 Clause
forall (tcm :: * -> *). PureTCM tcm => Clause -> tcm Clause
etaExpandClause ([Clause] -> TCM [Clause]) -> TCM [Clause] -> TCM [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]
cs
      performAnalysis <- lift $ optOccurrence <$> pragmaOptions
      if performAnalysis then do
        let clauses Int
i [a]
cs = ((ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
 -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret -> case [a]
cs of
              []   -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
              a
c:[a]
cs -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath)
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a. (OccursPath -> OccursPath) -> OccM a -> OccM a
underPath (OccursPath -> Int -> OccursPath
`InClause` Int
i) (a -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences a
c) ReaderT OccEnv TCM ()
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a b.
ReaderT OccEnv TCM a
-> ReaderT OccEnv TCM b -> ReaderT OccEnv TCM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> [a] -> ReaderT OccEnv TCM ()
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 TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

        -- András 2026-02-18: this looks dodgy?
        Clause
cl:[Clause]
_ -> (OccursPath -> OccursPath)
-> Occurrence -> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathSetOcc OccursPath -> OccursPath
Matched Occurrence
Mixed do
          let go :: Int -> NAPs -> ReaderT OccEnv TCM ()
go Int
i NAPs
ps = ((ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
 -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret -> case NAPs
ps of
                []   -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                NamedArg DeBruijnPattern
_:NAPs
ps -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret do d <- (OccEnv -> QName) -> ReaderT OccEnv TCM 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 TCM ()
go Int
0 (Clause -> NAPs
namedClausePats Clause
cl)

    Datatype{dataClause :: Defn -> Maybe Clause
dataClause = Just Clause
c} -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ Clause -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences (Clause -> ReaderT OccEnv TCM ())
-> ReaderT OccEnv TCM Clause -> ReaderT OccEnv TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Clause -> ReaderT OccEnv TCM 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 -> TCMT IO Clause
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull 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 TCM () -> Result (ReaderT OccEnv TCM ())
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 TCM (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 TCM (TelV (Type'' Term Term)))
-> TCM (TelV (Type'' Term Term))
-> ReaderT OccEnv TCM (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 TCM () -> Result (ReaderT OccEnv TCM ())
ret -> case Int
sizeIndex of
        Int
1 -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ Range -> Node -> ReaderT OccEnv TCM ()
addEdge Range
forall a. Range' a
noRange (QName -> Int -> Node
ArgNode QName
q Int
np0)
        Int
_ -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret (ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ()))
-> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
forall a b. (a -> b) -> a -> b
$ () -> ReaderT OccEnv TCM ()
forall a. a -> ReaderT OccEnv TCM 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 TCM ()
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 TCM [QName]
forall a. a -> ReaderT OccEnv TCM 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 TCM (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 TCM (TelV (Type'' Term Term), Boundary' Int Term))
-> TCM (TelV (Type'' Term Term), Boundary' Int Term)
-> ReaderT OccEnv TCM (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 TCM () -> ReaderT OccEnv TCM ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathSetOcc (OccursPath -> QName -> OccursPath
`IndArgType` QName
c) Occurrence
Mixed (ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ())
-> ReaderT OccEnv TCM () -> ReaderT OccEnv TCM ()
forall a b. (a -> b) -> a -> b
$ [Arg Term] -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences [Arg Term]
indices
                | Bool
otherwise -> ReaderT OccEnv TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- this ought to be impossible now (but wasn't, see #4447)
              Pi{}       -> ReaderT OccEnv TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- eliminated  by telView
              MetaV{}    -> ReaderT OccEnv TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a constructor target; should have been solved by now
              Var{}      -> ReaderT OccEnv TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a constructor target
              Sort{}     -> ReaderT OccEnv TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a constructor target
              Lam{}      -> ReaderT OccEnv TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
              Lit{}      -> ReaderT OccEnv TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
              Con{}      -> ReaderT OccEnv TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
              Level{}    -> ReaderT OccEnv TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
              DontCare{} -> ReaderT OccEnv TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
              Dummy{}    -> ReaderT OccEnv TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

    Record{recClause :: Defn -> Maybe Clause
recClause = Just Clause
c} -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret do
      Clause -> ReaderT OccEnv TCM ()
forall a. ComputeOccurrences a => a -> ReaderT OccEnv TCM ()
occurrences (Clause -> ReaderT OccEnv TCM ())
-> ReaderT OccEnv TCM Clause -> ReaderT OccEnv TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Clause -> ReaderT OccEnv TCM 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 -> TCMT IO Clause
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull 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 TCM () -> Result (ReaderT OccEnv TCM ())
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 TCM [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 TCM [DefArgInEnv])
-> TCM [DefArgInEnv] -> ReaderT OccEnv TCM [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 TCM () -> Result (ReaderT OccEnv TCM ())
ret ReaderT OccEnv TCM ()
forall a. Monoid a => a
mempty
    Axiom{}            -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret ReaderT OccEnv TCM ()
forall a. Monoid a => a
mempty
    DataOrRecSig{}     -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret ReaderT OccEnv TCM ()
forall a. Monoid a => a
mempty
    Primitive{}        -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret ReaderT OccEnv TCM ()
forall a. Monoid a => a
mempty
    PrimitiveSort{}    -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret ReaderT OccEnv TCM ()
forall a. Monoid a => a
mempty
    GeneralizableVar{} -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret ReaderT OccEnv TCM ()
forall a. Monoid a => a
mempty
    AbstractDefn{}     -> ReaderT OccEnv TCM () -> Result (ReaderT OccEnv TCM ())
ret ReaderT OccEnv TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

buildOccurrenceGraph :: [QName] -> TCM (OccGraph, Mutuals)
buildOccurrenceGraph :: [QName] -> TCM (OccGraph, HashTable MVector QName MVector ())
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

  mutuals <- lift HT.empty
  lift $ forM_ qs $ insertMutual mutuals

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