{-# 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 : Type) (B : A → Type) : Type where
    field fun : (x : A) → B x

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

  El : U → Type
  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
'Mikan.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 Mikan.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 Mikan.Interaction.Options.Base (optOccurrence)
import Mikan.Syntax.Internal
import Mikan.Syntax.Position (HasRange(..), noRange, Range)
import Mikan.TypeChecking.Functions
import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Patterns.Match (properlyMatching)
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Positivity.Occurrence
import Mikan.TypeChecking.Positivity.Warnings qualified as W
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Telescope

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

-- 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 (Maybe OccMutual)
isMutual :: QName -> OccM (Maybe OccMutual)
isMutual QName
q = do
  mutuals <- (OccEnv -> Mutuals) -> ReaderT OccEnv TCM Mutuals
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccEnv -> Mutuals
mutuals
  lift $ lift $ HT.lookup mutuals q

{-# NOINLINE insertMutual #-}
-- | Try to insert a 'QName' into the mutual definitions we have to
-- check. Does nothing if the 'QName' does not have a "body" that
-- meaningfully participate in mutual recursion, and thus should have
-- occurrences in its arguments be treated as though the function is
-- nonmutual.
--
-- Returns 'True' if the definition forces the mutual block to have
-- occurrence analysis performed on functions.
insertMutual :: Mutuals -> QName -> TCM Bool
insertMutual :: Mutuals -> QName -> TCM Bool
insertMutual Mutuals
muts QName
q = QName -> (Definition -> TCM Bool) -> TCM Bool
forall (m :: * -> *) a.
HasConstInfo m =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q \case
  -- Axioms (postulates, undefined functions) and primitives can be
  -- placed inside mutual blocks but they do not have a body to "use"
  -- their arguments.
  -- If we add them to the mutuals set, arguments passed to these names
  -- would get treated as unused.
  Defn { theDef :: Definition -> Defn
theDef = Axiom{}     } -> Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
  Defn { theDef :: Definition -> Defn
theDef = Primitive{} } -> Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

  Definition
def -> do
    TelV tel _ <- Lens' TCEnv (SmallSet AllowedReduction)
-> (SmallSet AllowedReduction -> SmallSet AllowedReduction)
-> TCMT IO (TelV Type)
-> TCMT IO (TelV Type)
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (SmallSet AllowedReduction -> f (SmallSet AllowedReduction))
-> TCEnv -> f TCEnv
Lens' TCEnv (SmallSet AllowedReduction)
eAllowedReductions (AllowedReduction
-> SmallSet AllowedReduction -> SmallSet AllowedReduction
forall a. SmallSetElement a => a -> SmallSet a -> SmallSet a
SmallSet.delete AllowedReduction
TypeLevelReductions) (TCMT IO (TelV Type) -> TCMT IO (TelV Type))
-> TCMT IO (TelV Type) -> TCMT IO (TelV Type)
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Definition -> Type
defType Definition
def)
    let !arity = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
    reportSDoc "tc.pos.init" 30 $ "added definition" <+> prettyTCM q <+> "to mutual block with initial arity" <+> pretty arity
    lift $ HT.insert muts q $ OccMutual
      { occMutualArity     = arity
      , occMutualOccurence = mutualDefOcc def
      }
    pure case theDef def of
      Datatype{} -> Bool
True
      Record{}   -> Bool
True
      Defn
_          -> Bool
False

{-# 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
          VarArg 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.VarArg 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
          InLevel OccursPath
p       -> OccursPath -> Seq Where
go' OccursPath
p Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Where
W.InLevel
          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
          VarArg OccursPath
p Int
i      -> (Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Int -> Where
W.VarArg 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
          InLevel OccursPath
p       -> (Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
:|> Where
W.InLevel)       (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.
data DefArgInEnv = DefArgInEnv Int
  deriving Int -> DefArgInEnv -> ShowS
[DefArgInEnv] -> ShowS
DefArgInEnv -> VerboseKey
(Int -> DefArgInEnv -> ShowS)
-> (DefArgInEnv -> VerboseKey)
-> ([DefArgInEnv] -> ShowS)
-> Show DefArgInEnv
forall a.
(Int -> a -> ShowS)
-> (a -> VerboseKey) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DefArgInEnv -> ShowS
showsPrec :: Int -> DefArgInEnv -> ShowS
$cshow :: DefArgInEnv -> VerboseKey
show :: DefArgInEnv -> VerboseKey
$cshowList :: [DefArgInEnv] -> ShowS
showList :: [DefArgInEnv] -> ShowS
Show

-- | Summarized information about a definition in the mutual block we
-- are positivity-checking.
data OccMutual = OccMutual
  { OccMutual -> Int
occMutualArity     :: !Int
    -- ^ Number of leading 'Pi's in the declared type of the function.
    -- Occurrences in arguments past this arity are treated as though
    -- the occurrence was 'Mixed' in an arbitrary (non-mutual) function.
  , OccMutual -> Occurrence
occMutualOccurence :: !Occurrence
    -- ^ Default (optimistic) occurrence for the arguments inside the
    -- 'occMutualArity'.
  }
  deriving Int -> OccMutual -> ShowS
[OccMutual] -> ShowS
OccMutual -> VerboseKey
(Int -> OccMutual -> ShowS)
-> (OccMutual -> VerboseKey)
-> ([OccMutual] -> ShowS)
-> Show OccMutual
forall a.
(Int -> a -> ShowS)
-> (a -> VerboseKey) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> OccMutual -> ShowS
showsPrec :: Int -> OccMutual -> ShowS
$cshow :: OccMutual -> VerboseKey
show :: OccMutual -> VerboseKey
$cshowList :: [OccMutual] -> ShowS
showList :: [OccMutual] -> ShowS
Show

-- | Set of mutual definition names in the block.
type Mutuals = HT.HashTableLL QName OccMutual

data OccEnv = OccEnv
  { OccEnv -> QName
topDef           :: QName         -- ^ The definition we're working under.
  , OccEnv -> [DefArgInEnv]
topDefArgs       :: [DefArgInEnv] -- ^ Occurrence info for definition args.
  , OccEnv -> Int
locals           :: Int           -- ^ Number of local binders (on the top of the definition args).
  , OccEnv -> Mutuals
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.
  , OccEnv -> Bool
analyseFunctions :: Bool
    -- ^ Whether occurrence analysis should look into the bodies of
    -- functions.
    -- This can be expensive, so we can disable this for mutual blocks
    -- that consist *entirely* of functions (every argument gets marked
    -- Mixed), but it is unsound to disable this for mutual blocks that
    -- consist of mixed function/data declarations.
  }

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}

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

-- | Add occurrences from the 'Elims' of an application of
--   a mutual definition.
occurrencesInMutElims :: QName -> OccMutual -> Elims -> OccM ()
occurrencesInMutElims :: QName -> OccMutual -> Elims -> OccM ()
occurrencesInMutElims QName
def (OccMutual Int
arity Occurrence
occ) Elims
es =
  Elims -> (Int -> Elim -> OccM ()) -> OccM ()
forall (m :: * -> *) a.
(Monad m, ExpandCase LiftedRep (m ())) =>
[a] -> (Int -> a -> m ()) -> m ()
iforM_ Elims
es \Int
i Elim
e -> do
    if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
arity then
      -- Argument outside the arity (arguments counted from zero, arity
      -- counted from 1): keep the original target for occurrences, add
      -- the function to the path, as if it pointed outside the mutual
      -- block.
      QName -> Occurrence -> Int -> Elim -> OccM ()
occurrencesInDefArg QName
def Occurrence
Mixed Int
i Elim
e
    else do
      -- Argument within the arity: edges point towards the ArgNode
      -- instead.
      let enter :: OccEnv -> OccEnv
enter OccEnv
e = OccEnv
e { path = MutDefArg (path e) def i, target = ArgNode def i, occ = occ }
      (OccEnv -> OccEnv) -> OccM () -> OccM ()
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 -> OccEnv
enter (OccM () -> OccM ()) -> OccM () -> OccM ()
forall a b. (a -> b) -> a -> b
$
        Elim -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Elim
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 -> OccM ()) -> t b -> OccM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ b -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences

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

    Var Int
x Elims
es -> OccM () -> Result LiftedRep (OccM ())
ret do
      locals <- (OccEnv -> Int) -> ReaderT OccEnv TCM Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccEnv -> Int
locals

      -- The variable is bound in a top-level definition argument: we
      -- record that the argument occurs in the definition.
      unless (x < locals) do
        topDefArgs <- asks topDefArgs
        topDef     <- asks topDef
        let DefArgInEnv argix = topDefArgs !! (x - locals)
        addEdge noRange (ArgNode topDef argix)

      -- We recurse into the variable's arguments, treating them all as Mixed.
      underOcc Mixed $ iforM_ es \Int
i Elim
e ->
        (OccursPath -> OccursPath) -> OccM () -> OccM ()
forall a. (OccursPath -> OccursPath) -> OccM a -> OccM a
underPath (OccursPath -> Int -> OccursPath
`VarArg` Int
i) (Elim -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Elim
e)

    Def QName
d Elims
es -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ do
      isMut <- QName -> OccM (Maybe OccMutual)
isMutual QName
d
      expand \OccM () -> Result LiftedRep (OccM ())
ret -> case Maybe OccMutual
isMut of
        -- It's a definition in the same mutual block. Any occurrences
        -- here will have their *target* set to a DefArg of @d@.
        Just OccMutual
mut -> OccM () -> Result LiftedRep (OccM ())
ret do
          Range -> Node -> OccM ()
addEdge (QName -> Range
forall a. HasRange a => a -> Range
getRange QName
d) (QName -> Node
DefNode QName
d)
          QName -> OccMutual -> Elims -> OccM ()
occurrencesInMutElims QName
d OccMutual
mut Elims
es

        -- It's not a mutual definition. Occurrences here will keep
        -- their target, and will have the occurrences multiplied by
        -- that from the defArgOccurrences (or, if the application is
        -- oversatured, Mixed).
        Maybe OccMutual
Nothing -> OccM () -> Result LiftedRep (OccM ())
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{} -> Elims -> (Int -> Elim -> OccM ()) -> OccM ()
forall (m :: * -> *) a.
(Monad m, ExpandCase LiftedRep (m ())) =>
[a] -> (Int -> a -> m ()) -> m ()
iforM_ Elims
es ((Int -> Elim -> OccM ()) -> OccM ())
-> (Int -> Elim -> OccM ()) -> OccM ()
forall a b. (a -> b) -> a -> b
$ QName -> Occurrence -> Int -> Elim -> OccM ()
occurrencesInDefArg QName
d Occurrence
StrictPos
            Defn
_ -> do
              let
                -- process Elims where we get Occurrences from 'defArgOccurrences',
                -- and then fall back to Mixed.
                --
                -- This is equivalent to
                -- @
                -- iforM_ (zip (argOccs ++ repeat Mixed) es) \i (o, e) ->
                --   occurrencesInDefArg d o i e
                -- @
                --
                -- but results in much better core.
                elims :: QName -> Int -> [Occurrence] -> Elims -> OccM ()
                elims :: QName -> Int -> [Occurrence] -> Elims -> OccM ()
elims QName
d Int
i [Occurrence]
occs Elims
es = ((OccM () -> Result LiftedRep (OccM ()))
 -> Result LiftedRep (OccM ()))
-> OccM ()
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \OccM () -> Result LiftedRep (OccM ())
ret -> case ([Occurrence]
occs, Elims
es) of
                  ([Occurrence]
_   , []  ) -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ () -> OccM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                  (Occurrence
o:[Occurrence]
occs, Elim
e:Elims
es) -> OccM () -> Result LiftedRep (OccM ())
ret do
                    QName -> Occurrence -> Int -> Elim -> OccM ()
occurrencesInDefArg QName
d Occurrence
o Int
i Elim
e
                    QName -> Int -> [Occurrence] -> Elims -> OccM ()
elims QName
d (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Occurrence]
occs Elims
es
                  ([]  , Elims
es) ->
                    -- process leftover Elims as Mixed after we have run out of Occurrences
                    OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ Elims -> (Int -> Elim -> OccM ()) -> OccM ()
forall (m :: * -> *) a.
(Monad m, ExpandCase LiftedRep (m ())) =>
[a] -> (Int -> a -> m ()) -> m ()
iforM_ Elims
es \Int
j Elim
e ->
                      QName -> Occurrence -> Int -> Elim -> OccM ()
occurrencesInDefArg QName
d Occurrence
Mixed (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j) Elim
e

                defOcc :: Occurrence
defOcc  = Definition -> Occurrence
mutualDefOcc Definition
def
                argOccs :: [Occurrence]
argOccs = Definition -> [Occurrence]
defArgOccurrences Definition
def

              Occurrence -> OccM () -> OccM ()
forall a. Occurrence -> OccM a -> OccM a
underOcc Occurrence
defOcc (OccM () -> OccM ()) -> OccM () -> OccM ()
forall a b. (a -> b) -> a -> b
$ QName -> Int -> [Occurrence] -> Elims -> OccM ()
elims QName
d Int
0 [Occurrence]
argOccs Elims
es

    Con ConHead
_ ConInfo
_ Elims
es -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ Elims -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Elims
es
    MetaV MetaId
m Elims
es -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath) -> Occurrence -> OccM () -> OccM ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathSetOcc OccursPath -> OccursPath
MetaArg Occurrence
Mixed (Elims -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Elims
es)
    Pi Dom Type
a Abs Type
b     -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath) -> Occurrence -> OccM () -> OccM ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathOcc OccursPath -> OccursPath
LeftOfArrow Occurrence
JustNeg (Dom Type -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Dom Type
a) OccM () -> OccM () -> OccM ()
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 -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Abs Type
b
    Lam ArgInfo
_ Abs Term
t    -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ Abs Term -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Abs Term
t
    Level Level
l    -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ Level -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Level
l

    -- we use "in a universe level" for occurrences in sorts because
    -- that's the only place a /user/ can write an occurrence, the
    -- heuristic being that anyone who can tie themselves into a knot
    -- where an occurrence is only in a piSort can probably untie the
    -- explanation back.
    Sort Sort
l     -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath) -> Occurrence -> OccM () -> OccM ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathOcc OccursPath -> OccursPath
InLevel Occurrence
Mixed (OccM () -> OccM ()) -> OccM () -> OccM ()
forall a b. (a -> b) -> a -> b
$ Sort -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Sort
l

    -- 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 -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ Term -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Term
t

    Lit{}      -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ () -> OccM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Dummy{}    -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ () -> OccM ()
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 -> OccM ()
addClauseArgMatches NAPs
ps =
  (OccursPath -> OccursPath) -> Occurrence -> OccM () -> OccM ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathSetOcc OccursPath -> OccursPath
Matched Occurrence
StrictPos (OccM () -> OccM ()) -> OccM () -> OccM ()
forall a b. (a -> b) -> a -> b
$
  NAPs -> (Int -> NamedArg DeBruijnPattern -> OccM ()) -> OccM ()
forall (m :: * -> *) a.
(Monad m, ExpandCase LiftedRep (m ())) =>
[a] -> (Int -> a -> m ()) -> m ()
iforM_ NAPs
ps \Int
i NamedArg DeBruijnPattern
p -> do
    TCM Bool -> ReaderT OccEnv TCM 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)) ReaderT OccEnv TCM Bool -> (Bool -> OccM ()) -> OccM ()
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 -> () -> OccM ()
forall a. a -> ReaderT OccEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

instance ComputeOccurrences Clause where
  occurrences :: Clause -> OccM ()
occurrences Clause
cl = do
    -- The code for assigning Unused occurrences to arguments that do
    -- not appear in the graph assumes that the clauses to functions
    -- (incl., here, data/record copies) bind *at least* arguments up to
    -- the arity in the type. So if we have (fake syntax for a datatype
    -- copy)
    --
    --   module M (x : A) where data D (y : B) ...
    --   data N.D (y : B) ...
    --   data N.D = M.D a
    --
    -- i.e. N.D has arity 1, but its defining clause does not mention
    -- the (y : B) argument, we assume N.D's 1st argument is Unused.
    -- Eta-expanding the clause to
    --
    --   data N.D (y : B) = M.D a y
    --
    -- correctly propagates the polarity of M.D's 2nd argument.
    cl <- Clause -> ReaderT OccEnv TCM Clause
forall (tcm :: * -> *). PureTCM tcm => Clause -> tcm Clause
etaExpandClause (Clause -> ReaderT OccEnv TCM Clause)
-> ReaderT OccEnv TCM Clause -> ReaderT OccEnv TCM Clause
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Clause -> ReaderT OccEnv TCM Clause
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Clause
cl

    let ps = Clause -> NAPs
namedClausePats Clause
cl
    addClauseArgMatches ps

    let 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 -> 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 = NAPs -> [DefArgInEnv]
collectArgs NAPs
ps
    -- process body
    local (\OccEnv
env -> OccEnv
env {topDefArgs = items}) do
      occurrences $ clauseBody cl

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

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

instance ComputeOccurrences Type where
  occurrences :: Type -> OccM ()
occurrences (El Sort
_ Term
v) = Term -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Term
v

instance ComputeOccurrences Sort where
  occurrences :: Sort -> OccM ()
occurrences Sort
s = ((OccM () -> Result LiftedRep (OccM ()))
 -> Result LiftedRep (OccM ()))
-> OccM ()
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \OccM () -> Result LiftedRep (OccM ())
ret -> case Sort
s of
    Univ Univ
_ Level
l     -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ Level -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Level
l
    UnivSort Sort
a   -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ Sort -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Sort
a
    PiSort Dom' Term Term
_ Sort
a Abs Sort
b -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath) -> Occurrence -> OccM () -> OccM ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathOcc OccursPath -> OccursPath
LeftOfArrow Occurrence
JustNeg (Sort -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Sort
a) OccM () -> OccM () -> OccM ()
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 Sort -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Abs Sort
b
    FunSort  Sort
a Sort
b -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ (OccursPath -> OccursPath) -> Occurrence -> OccM () -> OccM ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathOcc OccursPath -> OccursPath
LeftOfArrow Occurrence
JustNeg (Sort -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Sort
a) OccM () -> OccM () -> OccM ()
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
>> Sort -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Sort
b
    MetaS MetaId
m Elims
as   -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ Term -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences (MetaId -> Elims -> Term
MetaV MetaId
m Elims
as)
    DefS  QName
m Elims
as   -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ Term -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences (QName -> Elims -> Term
Def QName
m Elims
as)
    Inf{}        -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ OccM ()
forall a. Monoid a => a
mempty
    Sort
LevelUniv    -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ OccM ()
forall a. Monoid a => a
mempty
    Sort
IntervalUniv -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ OccM ()
forall a. Monoid a => a
mempty
    Sort
CofUniv      -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ OccM ()
forall a. Monoid a => a
mempty
    DummyS VerboseKey
s     -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ VerboseKey -> OccM ()
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
VerboseKey -> m a
__IMPOSSIBLE_VERBOSE__ (VerboseKey
"dummy sort:" VerboseKey -> ShowS
forall a. [a] -> [a] -> [a]
++! VerboseKey
s)

instance ComputeOccurrences a => ComputeOccurrences (Tele a) where
  occurrences :: Tele a -> OccM ()
occurrences Tele a
EmptyTel        = OccM ()
forall a. Monoid a => a
mempty
  occurrences (ExtendTel a
a Abs (Tele a)
b) = a -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences a
a OccM () -> OccM () -> OccM ()
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) -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Abs (Tele a)
b

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

instance ComputeOccurrences a => ComputeOccurrences (Elim' a) where
  occurrences :: Elim' a -> OccM ()
occurrences = \case
    Proj{}       -> OccM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    Apply Arg a
a      -> Arg a -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Arg a
a
    IApply a
x a
y a
a -> a -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences a
x OccM () -> OccM () -> OccM ()
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 -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences a
y OccM () -> OccM () -> OccM ()
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 -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences a
a -- TODO Andrea: conservative

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

instance ComputeOccurrences Int where
  {-# INLINE occurrences #-}
  occurrences :: Int -> OccM ()
occurrences Int
_ = () -> OccM ()
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 -> OccM ()
computeDefOccurrences QName
q = QName -> (Definition -> OccM ()) -> OccM ()
forall (m :: * -> *) a.
HasConstInfo m =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q \Definition
def -> do
  VerboseKey -> Int -> TCMT IO Doc -> OccM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"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 -> [DefArgInEnv]
      paramsToDefArgs :: Tele (Dom Type) -> [DefArgInEnv]
paramsToDefArgs =
        -- This is morally @[ DefArgInEnv i | i <- [size tel - 1, size tel - 2 .. 0] ]@
        -- but it only performs a single traversal of the telescope.
        (Int -> [DefArgInEnv] -> [DefArgInEnv])
-> [DefArgInEnv] -> Tele (Dom Type) -> [DefArgInEnv]
forall b a. (Int -> b -> b) -> b -> Tele a -> b
foldTeleIndices (\Int
i [DefArgInEnv]
acc -> Int -> DefArgInEnv
DefArgInEnv Int
i DefArgInEnv -> [DefArgInEnv] -> [DefArgInEnv]
forall a. a -> [a] -> [a]
: [DefArgInEnv]
acc) []
  let defOcc :: Occurrence
defOcc = Definition -> Occurrence
mutualDefOcc Definition
def
  (OccursPath -> OccursPath) -> Occurrence -> OccM () -> OccM ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathOcc (OccursPath -> QName -> OccursPath
`InDefOf` QName
q) Occurrence
defOcc (OccM () -> OccM ()) -> OccM () -> OccM ()
forall a b. (a -> b) -> a -> b
$ ((OccM () -> Result LiftedRep (OccM ()))
 -> Result LiftedRep (OccM ()))
-> OccM ()
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \OccM () -> Result LiftedRep (OccM ())
ret -> case Definition -> Defn
theDef Definition
def of

    Function{funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs} -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ ReaderT OccEnv TCM Bool -> OccM () -> OccM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((OccEnv -> Bool) -> ReaderT OccEnv TCM Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccEnv -> Bool
analyseFunctions) (OccM () -> OccM ()) -> OccM () -> OccM ()
forall a b. (a -> b) -> a -> b
$
      [Clause] -> (Int -> Clause -> OccM ()) -> OccM ()
forall (m :: * -> *) a.
(Monad m, ExpandCase LiftedRep (m ())) =>
[a] -> (Int -> a -> m ()) -> m ()
iforM_ [Clause]
cs \Int
i Clause
c -> Bool -> OccM () -> OccM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Clause -> Bool
forall a. HasDefP a => a -> Bool
hasDefP Clause
c) do
        (OccursPath -> OccursPath) -> OccM () -> OccM ()
forall a. (OccursPath -> OccursPath) -> OccM a -> OccM a
underPath (OccursPath -> Int -> OccursPath
`InClause` Int
i) (Clause -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Clause
c)

    Datatype{dataClause :: Defn -> Maybe Clause
dataClause = Just Clause
c} -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ Clause -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Clause
c
    Record{recClause :: Defn -> Maybe Clause
recClause = Just Clause
c}    -> OccM () -> Result LiftedRep (OccM ())
ret (OccM () -> Result LiftedRep (OccM ()))
-> OccM () -> Result LiftedRep (OccM ())
forall a b. (a -> b) -> a -> b
$ Clause -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences Clause
c

    Datatype{dataPars :: Defn -> Int
dataPars = Int
np, dataCons :: Defn -> [QName]
dataCons = [QName]
cs, dataTranspIx :: Defn -> Maybe QName
dataTranspIx = Maybe QName
trx} -> OccM () -> Result LiftedRep (OccM ())
ret do
      -- Andreas, 2013-02-27 (later edited by someone else): First,
      -- include each index of an inductive family.
      TelV telD _ <- TCMT IO (TelV Type) -> ReaderT OccEnv TCM (TelV Type)
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 (TelV Type) -> ReaderT OccEnv TCM (TelV Type))
-> TCMT IO (TelV Type) -> ReaderT OccEnv TCM (TelV Type)
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Type -> TCMT IO (TelV Type)) -> Type -> TCMT IO (TelV Type)
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def

      -- add edges for indices
      underPathSetOcc InIndex Mixed $
        rangeM_ np (size telD - 1) \Int
i -> Range -> Node -> OccM ()
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, Boundary)
-> ReaderT OccEnv TCM (TelV Type, Boundary)
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, Boundary)
 -> ReaderT OccEnv TCM (TelV Type, Boundary))
-> TCM (TelV Type, Boundary)
-> ReaderT OccEnv TCM (TelV Type, Boundary)
forall a b. (a -> b) -> a -> b
$ SmallSet AllowedReduction
-> TCM (TelV Type, Boundary) -> TCM (TelV Type, Boundary)
forall (m :: * -> *) a.
MonadTCEnv m =>
SmallSet AllowedReduction -> m a -> m a
putAllowedReductions SmallSet AllowedReduction
allReductions (TCM (TelV Type, Boundary) -> TCM (TelV Type, Boundary))
-> TCM (TelV Type, Boundary) -> TCM (TelV Type, Boundary)
forall a b. (a -> b) -> a -> b
$
                                    Type -> TCM (TelV Type, Boundary)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type, Boundary)
telViewPathBoundary (Type -> TCM (TelV Type, Boundary))
-> (Definition -> Type) -> Definition -> TCM (TelV Type, Boundary)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType (Definition -> TCM (TelV Type, Boundary))
-> TCM Definition -> TCM (TelV Type, Boundary)
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

        local (\OccEnv
env -> OccEnv
env {topDefArgs = paramsToDefArgs tel0}) 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' Elims
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
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims (Elims -> Maybe [Arg Term]) -> Elims -> Maybe [Arg Term]
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Elims
forall a. Int -> [a] -> [a]
drop Int
np Elims
vs
                    (OccursPath -> OccursPath) -> Occurrence -> OccM () -> OccM ()
forall a.
(OccursPath -> OccursPath) -> Occurrence -> OccM a -> OccM a
underPathSetOcc (OccursPath -> QName -> OccursPath
`IndArgType` QName
c) Occurrence
Mixed (OccM () -> OccM ()) -> OccM () -> OccM ()
forall a b. (a -> b) -> a -> b
$ [Arg Term] -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences [Arg Term]
indices
                | Bool
otherwise -> OccM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- this ought to be impossible now (but wasn't, see #4447)
              Pi{}       -> OccM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- eliminated  by telView
              MetaV{}    -> OccM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a constructor target; should have been solved by now
              Var{}      -> OccM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a constructor target
              Sort{}     -> OccM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a constructor target
              Lam{}      -> OccM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
              Lit{}      -> OccM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
              Con{}      -> OccM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
              Level{}    -> OccM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
              DontCare{} -> OccM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
              Dummy{}    -> OccM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

    Record{recPars :: Defn -> Int
recPars = Int
np, recTel :: Defn -> Tele (Dom Type)
recTel = Tele (Dom Type)
tel} -> OccM () -> Result LiftedRep (OccM ())
ret do
      let (Tele (Dom Type)
tel0, Tele (Dom Type)
tel1) = Int -> Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type))
splitTelescopeAt Int
np Tele (Dom Type)
tel
      (OccEnv -> OccEnv) -> OccM () -> OccM ()
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 = paramsToDefArgs tel0}) do
        Tele (Dom Type) -> OccM ()
forall a. ComputeOccurrences a => a -> OccM ()
occurrences (Tele (Dom Type) -> OccM ())
-> ReaderT OccEnv TCM (Tele (Dom Type)) -> OccM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM (Tele (Dom Type)) -> ReaderT OccEnv TCM (Tele (Dom Type))
forall a. TCM a -> ReaderT OccEnv TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (Tele (Dom Type) -> TCM (Tele (Dom Type)) -> TCM (Tele (Dom Type))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
tel0 (Tele (Dom Type) -> TCM (Tele (Dom Type))
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Tele (Dom Type)
tel1))
        -- Andreas, 2017-01-01, issue #1899, treat like data types

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

-- | Build an occurrence graph from a list of definition names.
buildOccurrenceGraph :: [QName] -> TCM (OccGraph, Mutuals)
buildOccurrenceGraph :: [QName] -> TCM (OccGraph, Mutuals)
buildOccurrenceGraph [QName]
qs = do
  mutuals <- IO Mutuals -> TCMT IO Mutuals
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 Mutuals
forall (ks :: * -> * -> *) k (vs :: * -> * -> *) v.
(MVector ks k, MVector vs v) =>
IO (HashTable ks k vs v)
HT.empty
  tainted <- mapM (insertMutual mutuals) qs
  opt     <- optOccurrence <$> pragmaOptions

  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]
-> Int
-> Mutuals
-> Node
-> OccursPath
-> Occurrence
-> OccGraph
-> Bool
-> OccEnv
OccEnv QName
q [] Int
0 Mutuals
mutuals (QName -> Node
DefNode QName
q) OccursPath
Root Occurrence
StrictPos OccGraph
graph (Bool
opt Bool -> Bool -> Bool
|| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
tainted)
    TCMT IO () -> IORef TCState -> TCEnv -> IO ()
forall (m :: * -> *) a. TCMT m a -> IORef TCState -> TCEnv -> m a
unTCM (OccM () -> OccEnv -> TCMT IO ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (QName -> OccM ()
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 -> VerboseKey
(Int -> Seen -> ShowS)
-> (Seen -> VerboseKey) -> ([Seen] -> ShowS) -> Show Seen
forall a.
(Int -> a -> ShowS)
-> (a -> VerboseKey) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Seen -> ShowS
showsPrec :: Int -> Seen -> ShowS
$cshow :: Seen -> VerboseKey
show :: Seen -> VerboseKey
$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