{-# LANGUAGE NondecreasingIndentation #-}

-- | Check that a datatype is strictly positive.
module Agda.TypeChecking.Positivity where

import Prelude hiding ( null )

import Control.Applicative hiding (empty)
import Control.DeepSeq
import Control.Monad        ( forM_, guard, liftM2 )
import Control.Monad.Reader ( MonadReader(..), asks, Reader, runReader )

import Data.Either
import qualified Data.Foldable as Fold
import Data.Function
import Data.Graph (SCC(..))
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Sequence (Seq)
import qualified Data.Sequence as DS
import Data.Set (Set)
import qualified Data.Set as Set

import Debug.Trace

import Agda.Syntax.Common
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Position (HasRange(..), noRange)
import Agda.TypeChecking.Datatypes ( isDataOrRecordType )
import Agda.TypeChecking.Functions
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Warnings

import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph
import Agda.Utils.Function (applyUnless)
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Pretty (Pretty, prettyShow)
import Agda.Utils.SemiRing
import Agda.Utils.Singleton
import Agda.Utils.Size

import Agda.Utils.Impossible

type Graph n e = Graph.Graph n e

-- | Check that the datatypes in the mutual block containing the given
--   declarations are strictly positive.
--
--   Also add information about positivity and recursivity of records
--   to the signature.
checkStrictlyPositive :: Info.MutualInfo -> Set QName -> TCM ()
checkStrictlyPositive :: MutualInfo -> Set QName -> TCM ()
checkStrictlyPositive MutualInfo
mi Set QName
qset = do
  -- compute the occurrence graph for qs
  let qs :: [QName]
qs = forall a. Set a -> [a]
Set.toList Set QName
qset
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.tick" Nat
100 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"positivity of" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [QName]
qs
  Graph Node (Edge OccursWhere)
g <- Set QName -> TCM (Graph Node (Edge OccursWhere))
buildOccurrenceGraph Set QName
qset
  let (Graph Node Occurrence
gstar, [SCC Node]
sccs) =
        forall n e.
(Ord n, Eq e, StarSemiRing e) =>
Graph n e -> (Graph n e, [SCC n])
Graph.gaussJordanFloydWarshallMcNaughtonYamada forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a}. Edge a -> Occurrence
occ Graph Node (Edge OccursWhere)
g
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.tick" Nat
100 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"constructed graph"
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> ArgName -> m ()
reportSLn ArgName
"tc.pos.graph" Nat
5 forall a b. (a -> b) -> a -> b
$ ArgName
"Positivity graph: N=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show (forall a. Sized a => a -> Nat
size forall a b. (a -> b) -> a -> b
$ forall n e. Graph n e -> Set n
Graph.nodes Graph Node (Edge OccursWhere)
g) forall a. [a] -> [a] -> [a]
++
                               ArgName
" E=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show (forall (t :: * -> *) a. Foldable t => t a -> Nat
length forall a b. (a -> b) -> a -> b
$ forall n e. Graph n e -> [Edge n e]
Graph.edges Graph Node (Edge OccursWhere)
g)
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.graph" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"positivity graph for" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [QName]
qs)
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Graph Node (Edge OccursWhere)
g
    ]
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> ArgName -> m ()
reportSLn ArgName
"tc.pos.graph" Nat
5 forall a b. (a -> b) -> a -> b
$
    ArgName
"Positivity graph (completed): E=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show (forall (t :: * -> *) a. Foldable t => t a -> Nat
length forall a b. (a -> b) -> a -> b
$ forall n e. Graph n e -> [Edge n e]
Graph.edges Graph Node Occurrence
gstar)
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.graph" Nat
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"transitive closure of positivity graph for" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
      forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [QName]
qs
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Graph Node Occurrence
gstar
    ]

  -- remember argument occurrences for qs in the signature
  Set QName -> [QName] -> Graph Node Occurrence -> TCM ()
setArgOccs Set QName
qset [QName]
qs Graph Node Occurrence
gstar
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.tick" Nat
100 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"set args"

  -- check positivity for all strongly connected components of the graph for qs
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.graph.sccs" Nat
10 forall a b. (a -> b) -> a -> b
$ do
    let ([Node]
triv, [[Node]]
others) = forall a b. [Either a b] -> ([a], [b])
partitionEithers forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [SCC Node]
sccs forall a b. (a -> b) -> a -> b
$ \case
          AcyclicSCC Node
v -> forall a b. a -> Either a b
Left Node
v
          CyclicSCC [Node]
vs -> forall a b. b -> Either a b
Right [Node]
vs
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Node]
triv) forall a. [a] -> [a] -> [a]
++ ArgName
" trivial sccs"
        , forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [[Node]]
others) forall a. [a] -> [a] -> [a]
++ ArgName
" non-trivial sccs with lengths " forall a. [a] -> [a] -> [a]
++
            forall a. Show a => a -> ArgName
show (forall a b. (a -> b) -> [a] -> [b]
map forall (t :: * -> *) a. Foldable t => t a -> Nat
length [[Node]]
others)
        ]
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> ArgName -> m ()
reportSLn ArgName
"tc.pos.graph.sccs" Nat
15 forall a b. (a -> b) -> a -> b
$
    ArgName
"  sccs = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
prettyShow [ [Node]
scc | CyclicSCC [Node]
scc <- [SCC Node]
sccs ]
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [SCC Node]
sccs forall a b. (a -> b) -> a -> b
$ \case
    -- If the mutuality information has never been set, we set it to []
    AcyclicSCC (DefNode QName
q) -> forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall a. Maybe a -> Bool
isNothing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM (Maybe [QName])
getMutual QName
q) forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> ArgName -> m ()
reportSLn ArgName
"tc.pos.mutual" Nat
10 forall a b. (a -> b) -> a -> b
$ ArgName
"setting " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
prettyShow QName
q forall a. [a] -> [a] -> [a]
++ ArgName
" to non-recursive"
      -- Andreas, 2017-04-26, issue #2555
      -- We should not have @DefNode@s pointing outside our formal mutual block.
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Ord a => a -> Set a -> Bool
Set.member QName
q Set QName
qset) forall a. HasCallStack => a
__IMPOSSIBLE__
      QName -> [QName] -> TCM ()
setMutual QName
q []
    AcyclicSCC (ArgNode{}) -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    CyclicSCC [Node]
scc          -> [QName] -> TCM ()
setMut [ QName
q | DefNode QName
q <- [Node]
scc ]
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Graph Node (Edge OccursWhere)
-> Graph Node Occurrence -> QName -> TCM ()
checkPos Graph Node (Edge OccursWhere)
g Graph Node Occurrence
gstar) [QName]
qs
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.tick" Nat
100 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checked positivity"

  where
    checkPos :: Graph Node (Edge OccursWhere) ->
                Graph Node Occurrence ->
                QName -> TCM ()
    checkPos :: Graph Node (Edge OccursWhere)
-> Graph Node Occurrence -> QName -> TCM ()
checkPos Graph Node (Edge OccursWhere)
g Graph Node Occurrence
gstar QName
q = forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q forall a b. (a -> b) -> a -> b
$ \ Definition
_def -> do
      -- we check positivity only for data or record definitions
      forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (QName -> TCM (Maybe DataOrRecord)
isDatatype QName
q) forall a b. (a -> b) -> a -> b
$ \ DataOrRecord
dr -> do
        forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.check" Nat
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checking positivity of" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q

        let loop :: Maybe Occurrence
            loop :: Maybe Occurrence
loop = forall n e. Ord n => n -> n -> Graph n e -> Maybe e
Graph.lookup (QName -> Node
DefNode QName
q) (QName -> Node
DefNode QName
q) Graph Node Occurrence
gstar

            g' :: Graph Node (Edge (Seq OccursWhere))
            g' :: Graph Node (Edge (Seq OccursWhere))
g' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Seq a
DS.singleton) Graph Node (Edge OccursWhere)
g

            -- Note the property
            -- Internal.Utils.Graph.AdjacencyMap.Unidirectional.prop_productOfEdgesInBoundedWalk,
            -- which relates productOfEdgesInBoundedWalk to
            -- gaussJordanFloydWarshallMcNaughtonYamada.

            reason :: Occurrence -> Seq OccursWhere
reason Occurrence
bound =
              case forall e n.
(SemiRing e, Ord n) =>
(e -> Occurrence) -> Graph n e -> n -> n -> Occurrence -> Maybe e
productOfEdgesInBoundedWalk
                     forall {a}. Edge a -> Occurrence
occ Graph Node (Edge (Seq OccursWhere))
g' (QName -> Node
DefNode QName
q) (QName -> Node
DefNode QName
q) Occurrence
bound of
                Just (Edge Occurrence
_ Seq OccursWhere
how) -> Seq OccursWhere
how
                Maybe (Edge (Seq OccursWhere))
Nothing           -> forall a. HasCallStack => a
__IMPOSSIBLE__

            how :: String -> Occurrence -> TCM Doc
            how :: ArgName -> Occurrence -> TCMT IO Doc
how ArgName
msg Occurrence
bound = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
                  [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"is" forall a. [a] -> [a] -> [a]
++
                  forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords (ArgName
msg forall a. [a] -> [a] -> [a]
++ ArgName
", because it occurs") forall a. [a] -> [a] -> [a]
++
                  [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Occurrence -> Seq OccursWhere
reason Occurrence
bound)]

        -- if we have a negative loop, raise error

        -- ASR (23 December 2015). We don't raise a strictly positive
        -- error if the NO_POSITIVITY_CHECK pragma was set on in the
        -- mutual block. See Issue 1614.
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (MutualInfo -> PositivityCheck
Info.mutualPositivityCheck MutualInfo
mi forall a. Eq a => a -> a -> Bool
== PositivityCheck
YesPositivityCheck) forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM forall (m :: * -> *). HasOptions m => m Bool
positivityCheckEnabled forall a b. (a -> b) -> a -> b
$
            case Maybe Occurrence
loop of
            Just Occurrence
o | Occurrence
o forall a. Ord a => a -> a -> Bool
<= Occurrence
JustPos ->
              forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ QName -> Seq OccursWhere -> Warning
NotStrictlyPositive QName
q (Occurrence -> Seq OccursWhere
reason Occurrence
JustPos)
            Maybe Occurrence
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

        -- if we find an unguarded record, mark it as such
        case DataOrRecord
dr of
          DataOrRecord
IsData -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
          IsRecord PatternOrCopattern
pat -> case Maybe Occurrence
loop of
            Just Occurrence
o | Occurrence
o forall a. Ord a => a -> a -> Bool
<= Occurrence
StrictPos -> do
              forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.record" Nat
5 forall a b. (a -> b) -> a -> b
$ ArgName -> Occurrence -> TCMT IO Doc
how ArgName
"not guarded" Occurrence
StrictPos
              QName -> PatternOrCopattern -> TCM ()
unguardedRecord QName
q PatternOrCopattern
pat
              QName -> TCM ()
checkInduction QName
q
            -- otherwise, if the record is recursive, mark it as well
            Just Occurrence
o | Occurrence
o forall a. Ord a => a -> a -> Bool
<= Occurrence
GuardPos -> do
              forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.record" Nat
5 forall a b. (a -> b) -> a -> b
$ ArgName -> Occurrence -> TCMT IO Doc
how ArgName
"recursive" Occurrence
GuardPos
              QName -> TCM ()
recursiveRecord QName
q
              QName -> TCM ()
checkInduction QName
q
            -- If the record is not recursive, switch on eta
            -- unless it is coinductive or a no-eta-equality record.
            Maybe Occurrence
Nothing -> do
              forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.record" Nat
10 forall a b. (a -> b) -> a -> b
$
                TCMT IO Doc
"record type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                TCMT IO Doc
"is not recursive"
              QName -> TCM ()
nonRecursiveRecord QName
q
            Maybe Occurrence
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

    checkInduction :: QName -> TCM ()
    checkInduction :: QName -> TCM ()
checkInduction QName
q =
      -- ASR (01 January 2016). We don't raise this error if the
      -- NO_POSITIVITY_CHECK pragma was set on in the record. See
      -- Issue 1760.
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (MutualInfo -> PositivityCheck
Info.mutualPositivityCheck MutualInfo
mi forall a. Eq a => a -> a -> Bool
== PositivityCheck
YesPositivityCheck) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM forall (m :: * -> *). HasOptions m => m Bool
positivityCheckEnabled forall a b. (a -> b) -> a -> b
$ do
        -- Check whether the recursive record has been declared as
        -- 'Inductive' or 'Coinductive'.  Otherwise, error.
        forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Maybe Induction
recInduction forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q) forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (Name -> Range
nameBindingSite forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
q) forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
              TCMT IO Doc
"Recursive record" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
              TCMT IO Doc
"needs to be declared as either inductive or coinductive"

    occ :: Edge a -> Occurrence
occ (Edge Occurrence
o a
_) = Occurrence
o

    isDatatype :: QName -> TCM (Maybe DataOrRecord)
    isDatatype :: QName -> TCM (Maybe DataOrRecord)
isDatatype QName
q = do
      Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Defn
def of
        Datatype{dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
Nothing} -> forall a. a -> Maybe a
Just DataOrRecord
IsData
        Record  {recClause :: Defn -> Maybe Clause
recClause  = Maybe Clause
Nothing, PatternOrCopattern
recPatternMatching :: Defn -> PatternOrCopattern
recPatternMatching :: PatternOrCopattern
recPatternMatching } -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ PatternOrCopattern -> DataOrRecord
IsRecord PatternOrCopattern
recPatternMatching
        Defn
_ -> forall a. Maybe a
Nothing

    -- Set the mutually recursive identifiers for a SCC.
    setMut :: [QName] -> TCM ()
    setMut :: [QName] -> TCM ()
setMut [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- nothing to do
    setMut [QName]
qs = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [QName]
qs forall a b. (a -> b) -> a -> b
$ \ QName
q -> do
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> ArgName -> m ()
reportSLn ArgName
"tc.pos.mutual" Nat
10 forall a b. (a -> b) -> a -> b
$ ArgName
"setting " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
prettyShow QName
q forall a. [a] -> [a] -> [a]
++ ArgName
" to (mutually) recursive"
      QName -> [QName] -> TCM ()
setMutual QName
q [QName]
qs
      -- TODO: The previous line produces data of quadratic size
      -- (which has to be processed upon serialization).  Presumably qs is
      -- usually short, but in some cases (for instance for generated
      -- code) it may be long. Wouldn't it be better to assign a
      -- unique identifier to each SCC, and avoid storing lists?

    -- Set the polarity of the arguments to a couple of definitions
    setArgOccs :: Set QName -> [QName] -> Graph Node Occurrence -> TCM ()
    setArgOccs :: Set QName -> [QName] -> Graph Node Occurrence -> TCM ()
setArgOccs Set QName
qset [QName]
qs Graph Node Occurrence
g = do
      -- Andreas, 2018-05-11, issue #3049: we need to be pessimistic about
      -- argument polarity beyond the formal arity of the function.
      --
      -- -- Compute a map from each name in q to the maximal argument index
      -- let maxs = Map.fromListWith max
      --      [ (q, i) | ArgNode q i <- Set.toList $ Graph.nodes g, q `Set.member` qset ]
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [QName]
qs forall a b. (a -> b) -> a -> b
$ \ QName
q -> forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q forall a b. (a -> b) -> a -> b
$ \ Definition
def -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Defn -> Bool
hasDefinition forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def) forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.args" Nat
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checking args of" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
        Nat
n <- Definition -> TCM Nat
getDefArity Definition
def
        -- If there is no outgoing edge @ArgNode q i@, all @n@ arguments are @Unused@.
        -- Otherwise, we obtain the occurrences from the Graph.
        let findOcc :: Nat -> Occurrence
findOcc Nat
i = forall a. a -> Maybe a -> a
fromMaybe Occurrence
Unused forall a b. (a -> b) -> a -> b
$ forall n e. Ord n => n -> n -> Graph n e -> Maybe e
Graph.lookup (QName -> Nat -> Node
ArgNode QName
q Nat
i) (QName -> Node
DefNode QName
q) Graph Node Occurrence
g
            args :: [Occurrence]
args = -- caseMaybe (Map.lookup q maxs) (replicate n Unused) $ \ m ->
              forall a b. (a -> b) -> [a] -> [b]
map Nat -> Occurrence
findOcc [Nat
0 .. Nat
nforall a. Num a => a -> a -> a
-Nat
1]  -- [0 .. max m (n - 1)] -- triggers issue #3049
        forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.args" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"args of" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"="
          , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Occurrence]
args
          ]
        -- The list args can take a long time to compute, but contains
        -- small elements, and is stored in the interface (right?), so
        -- it is computed deep-strictly.
        forall (m :: * -> *).
MonadTCState m =>
QName -> [Occurrence] -> m ()
setArgOccurrences QName
q forall a b. NFData a => (a -> b) -> a -> b
$!! [Occurrence]
args
      where
      -- Andreas, 2018-11-23, issue #3404
      -- Only assign argument occurrences to things which have a definition.
      -- Things without a definition would be judged "constant" in all arguments,
      -- since no occurrence could possibly be found, naturally.
      hasDefinition :: Defn -> Bool
      hasDefinition :: Defn -> Bool
hasDefinition = \case
        Axiom{}            -> Bool
False
        DataOrRecSig{}     -> Bool
False
        GeneralizableVar{} -> Bool
False
        AbstractDefn{}     -> Bool
False
        Primitive{}        -> Bool
False
        PrimitiveSort{}    -> Bool
False
        Constructor{}      -> Bool
False
        Function{}         -> Bool
True
        Datatype{}         -> Bool
True
        Record{}           -> Bool
True

getDefArity :: Definition -> TCM Int
getDefArity :: Definition -> TCM Nat
getDefArity Definition
def = do
  forall a. Num a => a -> a -> a
subtract (Definition -> Nat
projectionArgs Definition
def) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCM Nat
arity' (Definition -> Type
defType Definition
def)
  where
  -- A variant of "\t -> arity <$> instantiateFull t".
  arity' :: Type -> TCM Int
  arity' :: Type -> TCM Nat
arity' Type
t = do
    Type
t <- forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Type
t
    case forall t a. Type'' t a -> a
unEl Type
t of
      Pi Dom Type
_ Abs Type
t -> forall a. Enum a => a -> a
succ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCM Nat
arity' (forall a. Abs a -> a
unAbs Abs Type
t)
      Term
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return Nat
0

-- Computing occurrences --------------------------------------------------

data Item = AnArg Nat
          | ADef QName
  deriving (Item -> Item -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Item -> Item -> Bool
$c/= :: Item -> Item -> Bool
== :: Item -> Item -> Bool
$c== :: Item -> Item -> Bool
Eq, Eq Item
Item -> Item -> Bool
Item -> Item -> Ordering
Item -> Item -> Item
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Item -> Item -> Item
$cmin :: Item -> Item -> Item
max :: Item -> Item -> Item
$cmax :: Item -> Item -> Item
>= :: Item -> Item -> Bool
$c>= :: Item -> Item -> Bool
> :: Item -> Item -> Bool
$c> :: Item -> Item -> Bool
<= :: Item -> Item -> Bool
$c<= :: Item -> Item -> Bool
< :: Item -> Item -> Bool
$c< :: Item -> Item -> Bool
compare :: Item -> Item -> Ordering
$ccompare :: Item -> Item -> Ordering
Ord, Nat -> Item -> ShowS
[Item] -> ShowS
Item -> ArgName
forall a.
(Nat -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Item] -> ShowS
$cshowList :: [Item] -> ShowS
show :: Item -> ArgName
$cshow :: Item -> ArgName
showsPrec :: Nat -> Item -> ShowS
$cshowsPrec :: Nat -> Item -> ShowS
Show)

instance HasRange Item where
  getRange :: Item -> Range
getRange (AnArg Nat
_) = forall a. Range' a
noRange
  getRange (ADef QName
qn)   = forall a. HasRange a => a -> Range
getRange QName
qn

instance Pretty Item where
  prettyPrec :: Nat -> Item -> Doc
prettyPrec Nat
p (AnArg Nat
i) = Bool -> Doc -> Doc
P.mparens (Nat
p forall a. Ord a => a -> a -> Bool
> Nat
9) forall a b. (a -> b) -> a -> b
$ Doc
"AnArg" Doc -> Doc -> Doc
P.<+> forall a. Pretty a => a -> Doc
P.pretty Nat
i
  prettyPrec Nat
p (ADef QName
qn) = Bool -> Doc -> Doc
P.mparens (Nat
p forall a. Ord a => a -> a -> Bool
> Nat
9) forall a b. (a -> b) -> a -> b
$ Doc
"ADef"  Doc -> Doc -> Doc
P.<+> forall a. Pretty a => a -> Doc
P.pretty QName
qn

type Occurrences = Map Item [OccursWhere]

-- | Used to build 'Occurrences' and occurrence graphs.
data OccurrencesBuilder
  = Concat [OccurrencesBuilder]
  | OccursAs Where OccurrencesBuilder
  | OccursHere Item
  | OnlyVarsUpTo Nat OccurrencesBuilder
    -- ^ @OnlyVarsUpTo n occs@ discards occurrences of de Bruijn index
    -- @>= n@.

-- | Used to build 'Occurrences' and occurrence graphs.
data OccurrencesBuilder'
  = Concat' [OccurrencesBuilder']
  | OccursAs' Where OccurrencesBuilder'
  | OccursHere' Item

-- | The semigroup laws only hold up to flattening of 'Concat'.
instance Semigroup OccurrencesBuilder where
  OccurrencesBuilder
occs1 <> :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder
<> OccurrencesBuilder
occs2 = [OccurrencesBuilder] -> OccurrencesBuilder
Concat [OccurrencesBuilder
occs1, OccurrencesBuilder
occs2]

-- | The monoid laws only hold up to flattening of 'Concat'.
instance Monoid OccurrencesBuilder where
  mempty :: OccurrencesBuilder
mempty  = [OccurrencesBuilder] -> OccurrencesBuilder
Concat []
  mappend :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder
mappend = forall a. Semigroup a => a -> a -> a
(<>)
  mconcat :: [OccurrencesBuilder] -> OccurrencesBuilder
mconcat = [OccurrencesBuilder] -> OccurrencesBuilder
Concat

-- | Removes 'OnlyVarsUpTo' entries.
preprocess :: OccurrencesBuilder -> OccurrencesBuilder'
preprocess :: OccurrencesBuilder -> OccurrencesBuilder'
preprocess OccurrencesBuilder
ob = case Maybe Nat -> OccurrencesBuilder -> Maybe OccurrencesBuilder'
pp forall a. Maybe a
Nothing OccurrencesBuilder
ob of
  Maybe OccurrencesBuilder'
Nothing -> [OccurrencesBuilder'] -> OccurrencesBuilder'
Concat' []
  Just OccurrencesBuilder'
ob -> OccurrencesBuilder'
ob
  where
  pp :: Maybe Nat  -- Variables larger than or equal to this number, if any,
                   -- are not retained.
     -> OccurrencesBuilder
     -> Maybe OccurrencesBuilder'
  pp :: Maybe Nat -> OccurrencesBuilder -> Maybe OccurrencesBuilder'
pp !Maybe Nat
m = \case
    Concat [OccurrencesBuilder]
obs -> case forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Maybe Nat -> OccurrencesBuilder -> Maybe OccurrencesBuilder'
pp Maybe Nat
m) [OccurrencesBuilder]
obs of
      []  -> forall a. Maybe a
Nothing
      [OccurrencesBuilder']
obs -> forall (m :: * -> *) a. Monad m => a -> m a
return ([OccurrencesBuilder'] -> OccurrencesBuilder'
Concat' [OccurrencesBuilder']
obs)

    OccursAs Where
w OccurrencesBuilder
ob -> Where -> OccurrencesBuilder' -> OccurrencesBuilder'
OccursAs' Where
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Nat -> OccurrencesBuilder -> Maybe OccurrencesBuilder'
pp Maybe Nat
m OccurrencesBuilder
ob

    OnlyVarsUpTo Nat
n OccurrencesBuilder
ob -> Maybe Nat -> OccurrencesBuilder -> Maybe OccurrencesBuilder'
pp (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! forall b a. b -> (a -> b) -> Maybe a -> b
maybe Nat
n (forall a. Ord a => a -> a -> a
min Nat
n) Maybe Nat
m) OccurrencesBuilder
ob

    OccursHere Item
i -> do
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
keep
      forall (m :: * -> *) a. Monad m => a -> m a
return (Item -> OccurrencesBuilder'
OccursHere' Item
i)
      where
      keep :: Bool
keep = case (Maybe Nat
m, Item
i) of
        (Maybe Nat
Nothing, Item
_)      -> Bool
True
        (Maybe Nat
_, ADef QName
_)       -> Bool
True
        (Just Nat
m, AnArg Nat
i) -> Nat
i forall a. Ord a => a -> a -> Bool
< Nat
m

-- | An interpreter for 'OccurrencesBuilder'.
--
-- WARNING: There can be lots of sharing between the generated
-- 'OccursWhere' entries. Traversing all of these entries could be
-- expensive. (See 'computeEdges' for an example.)
flatten :: OccurrencesBuilder -> Map Item Integer
flatten :: OccurrencesBuilder -> Map Item Integer
flatten =
  forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. Num a => a -> a -> a
(+) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  forall a b c. (a -> b -> c) -> b -> a -> c
flip OccurrencesBuilder' -> [(Item, Integer)] -> [(Item, Integer)]
flatten' [] forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  OccurrencesBuilder -> OccurrencesBuilder'
preprocess
  where
  flatten'
    :: OccurrencesBuilder'
    -> [(Item, Integer)]
    -> [(Item, Integer)]
  flatten' :: OccurrencesBuilder' -> [(Item, Integer)] -> [(Item, Integer)]
flatten' (Concat' [OccurrencesBuilder']
obs)    = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\OccurrencesBuilder'
occs [(Item, Integer)] -> [(Item, Integer)]
f -> OccurrencesBuilder' -> [(Item, Integer)] -> [(Item, Integer)]
flatten' OccurrencesBuilder'
occs forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Item, Integer)] -> [(Item, Integer)]
f) forall a. a -> a
id [OccurrencesBuilder']
obs
  flatten' (OccursAs' Where
_ OccurrencesBuilder'
ob) = OccurrencesBuilder' -> [(Item, Integer)] -> [(Item, Integer)]
flatten' OccurrencesBuilder'
ob
  flatten' (OccursHere' Item
i)  = ((Item
i, Integer
1) forall a. a -> [a] -> [a]
:)

-- | Context for computing occurrences.
data OccEnv = OccEnv
  { OccEnv -> [Maybe Item]
vars :: [Maybe Item]
    -- ^ Items corresponding to the free variables.
    --
    --   Potential invariant: It seems as if the list has the form
    --   @'genericReplicate' n 'Nothing' ++ 'map' ('Just' . 'AnArg') is@,
    --   for some @n@ and @is@, where @is@ is decreasing
    --   (non-strictly).
  , OccEnv -> Maybe QName
inf  :: Maybe QName
    -- ^ Name for ∞ builtin.
  }

-- | Monad for computing occurrences.
type OccM = Reader OccEnv

instance (Semigroup a, Monoid a) => Monoid (OccM a) where
  mempty :: OccM a
mempty  = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
  mappend :: OccM a -> OccM a -> OccM a
mappend = forall a. Semigroup a => a -> a -> a
(<>)
  mconcat :: [OccM a] -> OccM a
mconcat = forall a. Monoid a => [a] -> a
mconcat forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence

withExtendedOccEnv :: Maybe Item -> OccM a -> OccM a
withExtendedOccEnv :: forall a. Maybe Item -> OccM a -> OccM a
withExtendedOccEnv Maybe Item
i = forall a. [Maybe Item] -> OccM a -> OccM a
withExtendedOccEnv' [Maybe Item
i]

withExtendedOccEnv' :: [Maybe Item] -> OccM a -> OccM a
withExtendedOccEnv' :: forall a. [Maybe Item] -> OccM a -> OccM a
withExtendedOccEnv' [Maybe Item]
is = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ \ OccEnv
e -> OccEnv
e { vars :: [Maybe Item]
vars = [Maybe Item]
is forall a. [a] -> [a] -> [a]
++ OccEnv -> [Maybe Item]
vars OccEnv
e }

-- | Running the monad
getOccurrences
  :: (Show a, PrettyTCM a, ComputeOccurrences a)
  => [Maybe Item]  -- ^ Extension of the 'OccEnv', usually a local variable context.
  -> a
  -> TCM OccurrencesBuilder
getOccurrences :: forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCMT IO OccurrencesBuilder
getOccurrences [Maybe Item]
vars a
a = do
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.occ" Nat
70 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"computing occurrences in " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show a
a)
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.occ" Nat
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"computing occurrences in " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
a
  forall r a. Reader r a -> r -> a
runReader (forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences a
a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe Item] -> Maybe QName -> OccEnv
OccEnv [Maybe Item]
vars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CoinductionKit -> QName
nameOfInf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM (Maybe CoinductionKit)
coinductionKit

class ComputeOccurrences a where
  occurrences :: a -> OccM OccurrencesBuilder

  default occurrences :: (Foldable t, ComputeOccurrences b, t b ~ a) => a -> OccM OccurrencesBuilder
  occurrences = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences

instance ComputeOccurrences Clause where
  occurrences :: Clause -> OccM OccurrencesBuilder
occurrences Clause
cl = do
    let ps :: NAPs
ps    = Clause -> NAPs
namedClausePats Clause
cl
        items :: [Maybe Item]
items = forall a. IntMap a -> [a]
IntMap.elems forall a b. (a -> b) -> a -> b
$ NAPs -> IntMap (Maybe Item)
patItems NAPs
ps -- sorted from low to high DBI
    -- TODO #3733: handle hcomp/transp clauses properly
    if NAPs -> Bool
hasDefP NAPs
ps then forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty else do
    ([OccurrencesBuilder] -> OccurrencesBuilder
Concat (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {name} {a}.
(Nat, Arg (Named name (Pattern' a))) -> Maybe OccurrencesBuilder
matching (forall a b. [a] -> [b] -> [(a, b)]
zip [Nat
0..] NAPs
ps)) forall a. Semigroup a => a -> a -> a
<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      forall a. [Maybe Item] -> OccM a -> OccM a
withExtendedOccEnv' [Maybe Item]
items forall a b. (a -> b) -> a -> b
$
        forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
cl
    where
      matching :: (Nat, Arg (Named name (Pattern' a))) -> Maybe OccurrencesBuilder
matching (Nat
i, Arg (Named name (Pattern' a))
p)
        | forall a. Pattern' a -> Bool
properlyMatching (forall name a. Named name a -> a
namedThing forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg (Named name (Pattern' a))
p) =
            forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs Where
Matched forall a b. (a -> b) -> a -> b
$ Item -> OccurrencesBuilder
OccursHere forall a b. (a -> b) -> a -> b
$ Nat -> Item
AnArg Nat
i
        | Bool
otherwise                  = forall a. Maybe a
Nothing

      -- @patItems ps@ creates a map from the pattern variables of @ps@
      -- to the index of the argument they are bound in.
      patItems :: NAPs -> IntMap (Maybe Item)
patItems NAPs
ps = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Nat -> NamedArg DeBruijnPattern -> IntMap (Maybe Item)
patItem [Nat
0..] NAPs
ps

      -- @patItem i p@ assigns index @i@ to each pattern variable in @p@
      patItem :: Int -> NamedArg DeBruijnPattern -> IntMap (Maybe Item)
      patItem :: Nat -> NamedArg DeBruijnPattern -> IntMap (Maybe Item)
patItem Nat
i NamedArg DeBruijnPattern
p = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Nat -> IntMap (Maybe Item)
makeEntry [Nat]
ixs
        where
          ixs :: [Nat]
ixs = forall a b. (a -> b) -> [a] -> [b]
map DBPatVar -> Nat
dbPatVarIndex forall a b. (a -> b) -> a -> b
$ forall a b. [Either a b] -> [a]
lefts forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars forall a b. (a -> b) -> a -> b
$ forall name a. Named name a -> a
namedThing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamedArg DeBruijnPattern
p

          makeEntry :: Nat -> IntMap (Maybe Item)
makeEntry Nat
x = forall el coll. Singleton el coll => el -> coll
singleton (Nat
x, forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Nat -> Item
AnArg Nat
i)

instance ComputeOccurrences Term where
  occurrences :: Term -> OccM OccurrencesBuilder
occurrences Term
v = case Term -> Term
unSpine Term
v of
    Var Nat
i Elims
args -> (forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ([Maybe Item] -> OccurrencesBuilder
occI forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccEnv -> [Maybe Item]
vars)) forall a. Semigroup a => a -> a -> a
<> (Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs Where
VarArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences Elims
args)
      where
      occI :: [Maybe Item] -> OccurrencesBuilder
occI [Maybe Item]
vars = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty Item -> OccurrencesBuilder
OccursHere forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> Nat -> a
indexWithDefault Maybe Item
unbound [Maybe Item]
vars Nat
i
      unbound :: Maybe Item
unbound = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. ArgName -> a -> a
trace forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$
              ArgName
"impossible: occurrence of de Bruijn index " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Nat
i forall a. [a] -> [a] -> [a]
++
              ArgName
" in vars " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show OccEnv -> [Maybe Item]
vars forall a. [a] -> [a] -> [a]
++ ArgName
" is unbound"

    Def QName
d Elims
args   -> do
      Maybe QName
inf <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccEnv -> Maybe QName
inf
      let occsAs :: Nat -> OccurrencesBuilder -> OccurrencesBuilder
occsAs = if forall a. a -> Maybe a
Just QName
d forall a. Eq a => a -> a -> Bool
/= Maybe QName
inf then Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Nat -> Where
DefArg QName
d else \ Nat
n ->
            -- the principal argument of builtin INF (∞) is the second (n==1)
            -- the first is a level argument (n==0, counting from 0!)
            if Nat
n forall a. Eq a => a -> a -> Bool
== Nat
1 then Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs Where
UnderInf else Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs (QName -> Nat -> Where
DefArg QName
d Nat
n)
      [OccurrencesBuilder]
occs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences Elims
args
      forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OccurrencesBuilder] -> OccurrencesBuilder
Concat forall a b. (a -> b) -> a -> b
$ Item -> OccurrencesBuilder
OccursHere (QName -> Item
ADef QName
d) forall a. a -> [a] -> [a]
: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Nat -> OccurrencesBuilder -> OccurrencesBuilder
occsAs [Nat
0..] [OccurrencesBuilder]
occs

    Con ConHead
_ ConInfo
_ Elims
args -> forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences Elims
args
    MetaV MetaId
_ Elims
args -> Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs Where
MetaArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences Elims
args
    Pi Dom Type
a Abs Type
b       -> (Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs Where
LeftOfArrow forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences Dom Type
a) forall a. Semigroup a => a -> a -> a
<> forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences Abs Type
b
    Lam ArgInfo
_ Abs Term
b      -> forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences Abs Term
b
    Level Level
l      -> forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences Level
l
    Lit{}        -> forall a. Monoid a => a
mempty
    Sort{}       -> forall a. Monoid a => a
mempty
    -- Jesper, 2020-01-12: this information is also used for the
    -- occurs check, so we need to look under DontCare (see #4371)
    DontCare Term
v   -> forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences Term
v
    Dummy{}      -> forall a. Monoid a => a
mempty

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

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

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

instance ComputeOccurrences a => ComputeOccurrences (Tele a) where
  occurrences :: Tele a -> OccM OccurrencesBuilder
occurrences Tele a
EmptyTel        = forall a. Monoid a => a
mempty
  occurrences (ExtendTel a
a Abs (Tele a)
b) = forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences (a
a, Abs (Tele a)
b)

instance ComputeOccurrences a => ComputeOccurrences (Abs a) where
  occurrences :: Abs a -> OccM OccurrencesBuilder
occurrences (Abs   ArgName
_ a
b) = forall a. Maybe Item -> OccM a -> OccM a
withExtendedOccEnv forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences a
b
  occurrences (NoAbs ArgName
_ a
b) = forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences a
b

instance ComputeOccurrences a => ComputeOccurrences (Elim' a) where
  occurrences :: Elim' a -> OccM OccurrencesBuilder
occurrences Proj{}         = forall a. HasCallStack => a
__IMPOSSIBLE__  -- unSpine
  occurrences (Apply Arg a
a)      = forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences Arg a
a
  occurrences (IApply a
x a
y a
a) = forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences (a
x,(a
y,a
a)) -- TODO Andrea: conservative

instance ComputeOccurrences a => ComputeOccurrences (Arg a)   where
instance ComputeOccurrences a => ComputeOccurrences (Dom a)   where
instance ComputeOccurrences a => ComputeOccurrences [a]       where
instance ComputeOccurrences a => ComputeOccurrences (Maybe a) where

instance (ComputeOccurrences a, ComputeOccurrences b) => ComputeOccurrences (a, b) where
  occurrences :: (a, b) -> OccM OccurrencesBuilder
occurrences (a
x, b
y) = forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences a
x forall a. Semigroup a => a -> a -> a
<> forall a. ComputeOccurrences a => a -> OccM OccurrencesBuilder
occurrences b
y

-- | Computes the number of occurrences of different 'Item's in the
-- given definition.
--
-- WARNING: There can be lots of sharing between the 'OccursWhere'
-- entries. Traversing all of these entries could be expensive. (See
-- 'computeEdges' for an example.)
computeOccurrences :: QName -> TCM (Map Item Integer)
computeOccurrences :: QName -> TCM (Map Item Integer)
computeOccurrences QName
q = OccurrencesBuilder -> Map Item Integer
flatten forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO OccurrencesBuilder
computeOccurrences' QName
q

-- | Computes the occurrences in the given definition.
computeOccurrences' :: QName -> TCM OccurrencesBuilder
computeOccurrences' :: QName -> TCMT IO OccurrencesBuilder
computeOccurrences' QName
q = forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q forall a b. (a -> b) -> a -> b
$ \ Definition
def -> do
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos" Nat
25 forall a b. (a -> b) -> a -> b
$ do
    let a :: IsAbstract
a = Definition -> IsAbstract
defAbstract Definition
def
    AbstractMode
m <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> AbstractMode
envAbstractMode
    ModuleName
cur <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> ModuleName
envCurrentModule
    TCMT IO Doc
"computeOccurrences" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show IsAbstract
a) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show AbstractMode
m)
      forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
cur
  Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs (QName -> Where
InDefOf QName
q) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case Definition -> Defn
theDef Definition
def of

    Function{funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs} -> do
      [Clause]
cs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (tcm :: * -> *). MonadTCM tcm => Clause -> tcm Clause
etaExpandClause forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull [Clause]
cs
      [OccurrencesBuilder] -> OccurrencesBuilder
Concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Where
InClause) [Nat
0..] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCMT IO OccurrencesBuilder
getOccurrences []) [Clause]
cs

    Datatype{dataClause :: Defn -> Maybe Clause
dataClause = Just Clause
c} -> forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCMT IO OccurrencesBuilder
getOccurrences [] forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Clause
c
    Datatype{dataPars :: Defn -> Nat
dataPars = Nat
np0, dataCons :: Defn -> [QName]
dataCons = [QName]
cs}       -> do
      -- Andreas, 2013-02-27 (later edited by someone else): First,
      -- include each index of an inductive family.
      TelV Tele (Dom Type)
tel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView forall a b. (a -> b) -> a -> b
$ Definition -> Type
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
      Nat
sizeIndex <- forall a b. [a] -> b -> (a -> [a] -> b) -> b
caseList (forall a. Nat -> [a] -> [a]
drop Nat
np0 forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
tel) (forall (m :: * -> *) a. Monad m => a -> m a
return Nat
0) forall a b. (a -> b) -> a -> b
$ \ Dom (ArgName, Type)
dom [Dom (ArgName, Type)]
_ -> do
        forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Dom (ArgName, Type)
dom) (forall (m :: * -> *) a. Monad m => a -> m a
return Nat
0) forall a b. (a -> b) -> a -> b
$ \ BoundedSize
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Nat
1
      let np :: Nat
np = Nat
np0 forall a. Num a => a -> a -> a
+ Nat
sizeIndex
      let xs :: [Nat]
xs = [Nat
np .. forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel forall a. Num a => a -> a -> a
- Nat
1] -- argument positions corresponding to indices
      let ioccs :: OccurrencesBuilder
ioccs = [OccurrencesBuilder] -> OccurrencesBuilder
Concat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Item -> OccurrencesBuilder
OccursHere forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Item
AnArg) [Nat
np0 .. Nat
np forall a. Num a => a -> a -> a
- Nat
1]
                        forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs Where
IsIndex forall b c a. (b -> c) -> (a -> b) -> a -> c
. Item -> OccurrencesBuilder
OccursHere forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Item
AnArg) [Nat]
xs
      -- Then, we compute the occurrences in the constructor types.
      let conOcc :: QName -> TCMT IO OccurrencesBuilder
conOcc 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 Tele (Dom Type)
tel Type
t <- forall (m :: * -> *) a.
MonadTCEnv m =>
AllowedReductions -> m a -> m a
putAllowedReductions AllowedReductions
allReductions forall a b. (a -> b) -> a -> b
$
              forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
            let (Tele (Dom Type)
tel0,Tele (Dom Type)
tel1) = Nat -> Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type))
splitTelescopeAt Nat
np Tele (Dom Type)
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.)
            Tele (Dom Type)
tel1' <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel0 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise forall a b. (a -> b) -> a -> b
$ Tele (Dom Type)
tel1
            let vars :: Nat -> [Maybe Item]
vars = forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Item
AnArg) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> [a]
downFrom
            -- Occurrences in the types of the constructor arguments.
            forall a. Monoid a => a -> a -> a
mappend (Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs (QName -> Where
ConArgType QName
c) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCMT IO OccurrencesBuilder
getOccurrences (Nat -> [Maybe Item]
vars Nat
np) Tele (Dom Type)
tel1') forall a b. (a -> b) -> a -> b
$ do
              -- 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'.
              let fallback :: TCMT IO OccurrencesBuilder
fallback = Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs Where
LeftOfArrow forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCMT IO OccurrencesBuilder
getOccurrences (Nat -> [Maybe Item]
vars forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel) Type
t -- NB::Defined but not used
              case forall t a. Type'' t a -> a
unEl Type
t of
                Def QName
q' Elims
vs
                  | QName
q forall a. Eq a => a -> a -> Bool
== QName
q' -> do
                      let indices :: [Arg Term]
indices = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims forall a b. (a -> b) -> a -> b
$ forall a. Nat -> [a] -> [a]
drop Nat
np Elims
vs
                      Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs (QName -> Where
IndArgType QName
c) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> OccurrencesBuilder -> OccurrencesBuilder
OnlyVarsUpTo Nat
np forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCMT IO OccurrencesBuilder
getOccurrences (Nat -> [Maybe Item]
vars forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel) [Arg Term]
indices
                  | Bool
otherwise -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- fallback -- this ought to be impossible now (but wasn't, see #4447)
                Pi{}       -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- eliminated  by telView
                MetaV{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a constructor target; should have been solved by now
                Var{}      -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a constructor target
                Sort{}     -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a constructor target
                Lam{}      -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
                Lit{}      -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
                Con{}      -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
                Level{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
                DontCare{} -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
                Dummy{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__
      forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure OccurrencesBuilder
ioccs forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map QName -> TCMT IO OccurrencesBuilder
conOcc [QName]
cs

    Record{recClause :: Defn -> Maybe Clause
recClause = Just Clause
c} -> forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCMT IO OccurrencesBuilder
getOccurrences [] forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Clause
c
    Record{recPars :: Defn -> Nat
recPars = Nat
np, recTel :: Defn -> Tele (Dom Type)
recTel = Tele (Dom Type)
tel} -> do
      let (Tele (Dom Type)
tel0,Tele (Dom Type)
tel1) = Nat -> Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type))
splitTelescopeAt Nat
np Tele (Dom Type)
tel
          vars :: [Maybe Item]
vars = forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Item
AnArg) forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom Nat
np
      forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCMT IO OccurrencesBuilder
getOccurrences [Maybe Item]
vars forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel0 (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.
    Constructor{}      -> forall a. Monoid a => a
mempty
    Axiom{}            -> forall a. Monoid a => a
mempty
    DataOrRecSig{}     -> forall a. Monoid a => a
mempty
    Primitive{}        -> forall a. Monoid a => a
mempty
    PrimitiveSort{}    -> forall a. Monoid a => a
mempty
    GeneralizableVar{} -> forall a. Monoid a => a
mempty
    AbstractDefn{}     -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- Building the occurrence graph ------------------------------------------

data Node = DefNode !QName
          | ArgNode !QName !Nat
  deriving (Node -> Node -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Node -> Node -> Bool
$c/= :: Node -> Node -> Bool
== :: Node -> Node -> Bool
$c== :: Node -> Node -> Bool
Eq, Eq Node
Node -> Node -> Bool
Node -> Node -> Ordering
Node -> Node -> Node
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Node -> Node -> Node
$cmin :: Node -> Node -> Node
max :: Node -> Node -> Node
$cmax :: Node -> Node -> Node
>= :: Node -> Node -> Bool
$c>= :: Node -> Node -> Bool
> :: Node -> Node -> Bool
$c> :: Node -> Node -> Bool
<= :: Node -> Node -> Bool
$c<= :: Node -> Node -> Bool
< :: Node -> Node -> Bool
$c< :: Node -> Node -> Bool
compare :: Node -> Node -> Ordering
$ccompare :: Node -> Node -> Ordering
Ord)

-- | Edge labels for the positivity graph.
data Edge a = Edge !Occurrence a
  deriving (Edge a -> Edge a -> Bool
forall a. Eq a => Edge a -> Edge a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Edge a -> Edge a -> Bool
$c/= :: forall a. Eq a => Edge a -> Edge a -> Bool
== :: Edge a -> Edge a -> Bool
$c== :: forall a. Eq a => Edge a -> Edge a -> Bool
Eq, Edge a -> Edge a -> Bool
Edge a -> Edge a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (Edge a)
forall a. Ord a => Edge a -> Edge a -> Bool
forall a. Ord a => Edge a -> Edge a -> Ordering
forall a. Ord a => Edge a -> Edge a -> Edge a
min :: Edge a -> Edge a -> Edge a
$cmin :: forall a. Ord a => Edge a -> Edge a -> Edge a
max :: Edge a -> Edge a -> Edge a
$cmax :: forall a. Ord a => Edge a -> Edge a -> Edge a
>= :: Edge a -> Edge a -> Bool
$c>= :: forall a. Ord a => Edge a -> Edge a -> Bool
> :: Edge a -> Edge a -> Bool
$c> :: forall a. Ord a => Edge a -> Edge a -> Bool
<= :: Edge a -> Edge a -> Bool
$c<= :: forall a. Ord a => Edge a -> Edge a -> Bool
< :: Edge a -> Edge a -> Bool
$c< :: forall a. Ord a => Edge a -> Edge a -> Bool
compare :: Edge a -> Edge a -> Ordering
$ccompare :: forall a. Ord a => Edge a -> Edge a -> Ordering
Ord, Nat -> Edge a -> ShowS
forall a. Show a => Nat -> Edge a -> ShowS
forall a. Show a => [Edge a] -> ShowS
forall a. Show a => Edge a -> ArgName
forall a.
(Nat -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Edge a] -> ShowS
$cshowList :: forall a. Show a => [Edge a] -> ShowS
show :: Edge a -> ArgName
$cshow :: forall a. Show a => Edge a -> ArgName
showsPrec :: Nat -> Edge a -> ShowS
$cshowsPrec :: forall a. Show a => Nat -> Edge a -> ShowS
Show, forall a b. a -> Edge b -> Edge a
forall a b. (a -> b) -> Edge a -> Edge b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Edge b -> Edge a
$c<$ :: forall a b. a -> Edge b -> Edge a
fmap :: forall a b. (a -> b) -> Edge a -> Edge b
$cfmap :: forall a b. (a -> b) -> Edge a -> Edge b
Functor)

-- | Merges two edges between the same source and target.

mergeEdges :: Edge a -> Edge a -> Edge a
mergeEdges :: forall a. Edge a -> Edge a -> Edge a
mergeEdges Edge a
_                    e :: Edge a
e@(Edge Occurrence
Mixed a
_)     = Edge a
e -- dominant
mergeEdges e :: Edge a
e@(Edge Occurrence
Mixed a
_)     Edge a
_                    = Edge a
e
mergeEdges (Edge Occurrence
Unused a
_)      Edge a
e                    = Edge a
e -- neutral
mergeEdges Edge a
e                    (Edge Occurrence
Unused a
_)      = Edge a
e
mergeEdges (Edge Occurrence
JustNeg a
_)     e :: Edge a
e@(Edge Occurrence
JustNeg a
_)   = Edge a
e
mergeEdges Edge a
_                    e :: Edge a
e@(Edge Occurrence
JustNeg a
w)   = forall a. Occurrence -> a -> Edge a
Edge Occurrence
Mixed a
w
mergeEdges e :: Edge a
e@(Edge Occurrence
JustNeg a
w)   Edge a
_                    = forall a. Occurrence -> a -> Edge a
Edge Occurrence
Mixed a
w
mergeEdges Edge a
_                    e :: Edge a
e@(Edge Occurrence
JustPos a
_)   = Edge a
e -- dominates strict pos.
mergeEdges e :: Edge a
e@(Edge Occurrence
JustPos a
_)   Edge a
_                    = Edge a
e
mergeEdges Edge a
_                    e :: Edge a
e@(Edge Occurrence
StrictPos a
_) = Edge a
e -- dominates 'GuardPos'
mergeEdges e :: Edge a
e@(Edge Occurrence
StrictPos a
_) Edge a
_                    = Edge a
e
mergeEdges (Edge Occurrence
GuardPos a
_)    e :: Edge a
e@(Edge Occurrence
GuardPos a
_)  = Edge a
e

-- | These operations form a semiring if we quotient by the relation
-- \"the 'Occurrence' components are equal\".

instance SemiRing (Edge (Seq OccursWhere)) where
  ozero :: Edge (Seq OccursWhere)
ozero = forall a. Occurrence -> a -> Edge a
Edge forall a. SemiRing a => a
ozero forall a. Seq a
DS.empty
  oone :: Edge (Seq OccursWhere)
oone  = forall a. Occurrence -> a -> Edge a
Edge forall a. SemiRing a => a
oone  forall a. Seq a
DS.empty

  oplus :: Edge (Seq OccursWhere)
-> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere)
oplus = forall a. Edge a -> Edge a -> Edge a
mergeEdges

  otimes :: Edge (Seq OccursWhere)
-> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere)
otimes (Edge Occurrence
o1 Seq OccursWhere
w1) (Edge Occurrence
o2 Seq OccursWhere
w2) = forall a. Occurrence -> a -> Edge a
Edge (forall a. SemiRing a => a -> a -> a
otimes Occurrence
o1 Occurrence
o2) (Seq OccursWhere
w1 forall a. Seq a -> Seq a -> Seq a
DS.>< Seq OccursWhere
w2)

-- | WARNING: There can be lots of sharing between the 'OccursWhere'
-- entries in the edges. Traversing all of these entries could be
-- expensive. (See 'computeEdges' for an example.)
buildOccurrenceGraph :: Set QName -> TCM (Graph Node (Edge OccursWhere))
buildOccurrenceGraph :: Set QName -> TCM (Graph Node (Edge OccursWhere))
buildOccurrenceGraph Set QName
qs =
  forall n e. Ord n => (e -> e -> e) -> [Edge n e] -> Graph n e
Graph.fromEdgesWith forall a. Edge a -> Edge a -> Edge a
mergeEdges forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM QName -> TCM [Edge Node (Edge OccursWhere)]
defGraph (forall a. Set a -> [a]
Set.toList Set QName
qs)
  where
    defGraph :: QName -> TCM [Graph.Edge Node (Edge OccursWhere)]
    defGraph :: QName -> TCM [Edge Node (Edge OccursWhere)]
defGraph QName
q = forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q forall a b. (a -> b) -> a -> b
$ \ Definition
_def -> do
      OccurrencesBuilder
occs <- QName -> TCMT IO OccurrencesBuilder
computeOccurrences' QName
q

      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.occs" Nat
40 forall a b. (a -> b) -> a -> b
$
        ((TCMT IO Doc
"Occurrences in" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q) forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
":")
          forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$+$
        forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
           forall a b. (a -> b) -> [a] -> [b]
map (\(Item
i, Integer
n) ->
                   (forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Item
i forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
":") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show Integer
n) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                   TCMT IO Doc
"occurrences") forall a b. (a -> b) -> a -> b
$
           forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$
           forall k a. Map k a -> [(k, a)]
Map.toList (OccurrencesBuilder -> Map Item Integer
flatten OccurrencesBuilder
occs))

      -- Placing this line before the reportSDoc lines above creates a
      -- space leak: occs is retained for too long.
      [Edge Node (Edge OccursWhere)]
es <- Set QName
-> QName
-> OccurrencesBuilder
-> TCM [Edge Node (Edge OccursWhere)]
computeEdges Set QName
qs QName
q OccurrencesBuilder
occs

      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.occs.edges" Nat
60 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"Edges:"
          forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$+$
        forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
           forall a b. (a -> b) -> [a] -> [b]
map (\Edge Node (Edge OccursWhere)
e ->
                   let Edge Occurrence
o OccursWhere
w = forall n e. Edge n e -> e
Graph.label Edge Node (Edge OccursWhere)
e in
                   forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall n e. Edge n e -> n
Graph.source Edge Node (Edge OccursWhere)
e) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                   TCMT IO Doc
"-[" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Pretty a => a -> Doc
P.pretty Occurrence
o) forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
",") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                                 forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Pretty a => a -> Doc
P.pretty OccursWhere
w) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"]->" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                   forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall n e. Edge n e -> n
Graph.target Edge Node (Edge OccursWhere)
e))
               [Edge Node (Edge OccursWhere)]
es)

      forall (m :: * -> *) a. Monad m => a -> m a
return [Edge Node (Edge OccursWhere)]
es

-- | Computes all non-'ozero' occurrence graph edges represented by
-- the given 'OccurrencesBuilder'.
--
-- WARNING: There can be lots of sharing between the 'OccursWhere'
-- entries in the edges. Traversing all of these entries could be
-- expensive. For instance, for the function @F@ in
-- @benchmark/misc/SlowOccurrences.agda@ a large number of edges from
-- the argument @X@ to the function @F@ are computed. These edges have
-- polarity 'StrictPos', 'JustNeg' or 'JustPos', and contain the
-- following 'OccursWhere' elements:
--
-- * @'OccursWhere' _ 'DS.empty' ('DS.fromList' ['InDefOf' "F", 'InClause' 0])@,
--
-- * @'OccursWhere' _ 'DS.empty' ('DS.fromList' ['InDefOf' "F", 'InClause' 0, 'LeftOfArrow'])@,
--
-- * @'OccursWhere' _ 'DS.empty' ('DS.fromList' ['InDefOf' "F", 'InClause' 0, 'LeftOfArrow', 'LeftOfArrow'])@,
--
-- * @'OccursWhere' _ 'DS.empty' ('DS.fromList' ['InDefOf' "F", 'InClause' 0, 'LeftOfArrow', 'LeftOfArrow', 'LeftOfArrow'])@,
--
-- * and so on.
computeEdges
  :: Set QName
     -- ^ The names in the current mutual block.
  -> QName
     -- ^ The current name.
  -> OccurrencesBuilder
  -> TCM [Graph.Edge Node (Edge OccursWhere)]
computeEdges :: Set QName
-> QName
-> OccurrencesBuilder
-> TCM [Edge Node (Edge OccursWhere)]
computeEdges Set QName
muts QName
q OccurrencesBuilder
ob =
  (forall a b. (a -> b) -> a -> b
$ []) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Occurrence
-> OccurrencesBuilder'
-> Node
-> Seq Where
-> Seq Where
-> TCM
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
mkEdge Occurrence
StrictPos (OccurrencesBuilder -> OccurrencesBuilder'
preprocess OccurrencesBuilder
ob)
                    forall a. HasCallStack => a
__IMPOSSIBLE__ forall a. Seq a
DS.empty forall a. Seq a
DS.empty
  where
  mkEdge
     :: Occurrence
     -> OccurrencesBuilder'
     -> Node          -- The current target node.
     -> DS.Seq Where  -- 'Where' information encountered before the current target
                      -- node was (re)selected.
     -> DS.Seq Where  -- 'Where' information encountered after the current target
                      -- node was (re)selected.
     -> TCM ([Graph.Edge Node (Edge OccursWhere)] ->
             [Graph.Edge Node (Edge OccursWhere)])
  mkEdge :: Occurrence
-> OccurrencesBuilder'
-> Node
-> Seq Where
-> Seq Where
-> TCM
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
mkEdge !Occurrence
pol OccurrencesBuilder'
ob Node
to Seq Where
cs Seq Where
os = case OccurrencesBuilder'
ob of
    Concat' [OccurrencesBuilder']
obs ->
      forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. a -> a
id)
            [ Occurrence
-> OccurrencesBuilder'
-> Node
-> Seq Where
-> Seq Where
-> TCM
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
mkEdge Occurrence
pol OccurrencesBuilder'
ob Node
to Seq Where
cs Seq Where
os | OccurrencesBuilder'
ob <- [OccurrencesBuilder']
obs ]

    OccursAs' Where
w OccurrencesBuilder'
ob -> do
      (Maybe Node
to', Occurrence
pol) <- Node -> Occurrence -> Where -> TCM (Maybe Node, Occurrence)
mkEdge' Node
to Occurrence
pol Where
w
      let mk :: Node
-> Seq Where
-> Seq Where
-> TCM
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
mk = Occurrence
-> OccurrencesBuilder'
-> Node
-> Seq Where
-> Seq Where
-> TCM
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
mkEdge Occurrence
pol OccurrencesBuilder'
ob
      case Maybe Node
to' of
        Maybe Node
Nothing -> Node
-> Seq Where
-> Seq Where
-> TCM
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
mk Node
to Seq Where
cs            (Seq Where
os forall a. Seq a -> a -> Seq a
DS.|> Where
w)
        Just Node
to -> Node
-> Seq Where
-> Seq Where
-> TCM
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
mk Node
to (Seq Where
cs forall a. Seq a -> Seq a -> Seq a
DS.>< Seq Where
os) (forall a. a -> Seq a
DS.singleton Where
w)

    OccursHere' Item
i ->
      let o :: OccursWhere
o = Range -> Seq Where -> Seq Where -> OccursWhere
OccursWhere (forall a. HasRange a => a -> Range
getRange Item
i) Seq Where
cs Seq Where
os in
      case Item
i of
        AnArg Nat
i ->
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Bool -> (a -> a) -> a -> a
applyUnless (forall a. Null a => a -> Bool
null Occurrence
pol) (Graph.Edge
            { source :: Node
Graph.source = QName -> Nat -> Node
ArgNode QName
q Nat
i
            , target :: Node
Graph.target = Node
to
            , label :: Edge OccursWhere
Graph.label  = forall a. Occurrence -> a -> Edge a
Edge Occurrence
pol OccursWhere
o
            } forall a. a -> [a] -> [a]
:)
        ADef QName
q' ->
          -- Andreas, 2017-04-26, issue #2555
          -- Skip nodes pointing outside the mutual block.
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Bool -> (a -> a) -> a -> a
applyUnless (forall a. Null a => a -> Bool
null Occurrence
pol Bool -> Bool -> Bool
|| forall a. Ord a => a -> Set a -> Bool
Set.notMember QName
q' Set QName
muts)
            (Graph.Edge
               { source :: Node
Graph.source = QName -> Node
DefNode QName
q'
               , target :: Node
Graph.target = Node
to
               , label :: Edge OccursWhere
Graph.label  = forall a. Occurrence -> a -> Edge a
Edge Occurrence
pol OccursWhere
o
               } forall a. a -> [a] -> [a]
:)

  -- This function might return a new target node.
  mkEdge'
    :: Node  -- The current target node.
    -> Occurrence
    -> Where
    -> TCM (Maybe Node, Occurrence)
  mkEdge' :: Node -> Occurrence -> Where -> TCM (Maybe Node, Occurrence)
mkEdge' Node
to !Occurrence
pol = \case
    Where
VarArg         -> forall {a}. TCMT IO (Maybe a, Occurrence)
mixed
    Where
MetaArg        -> forall {a}. TCMT IO (Maybe a, Occurrence)
mixed
    Where
LeftOfArrow    -> TCM (Maybe Node, Occurrence)
negative
    DefArg QName
d Nat
i     -> do
      Occurrence
pol' <- QName -> TCMT IO Occurrence
isGuarding QName
d
      if forall a. Ord a => a -> Set a -> Bool
Set.member QName
d Set QName
muts
        then forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (QName -> Nat -> Node
ArgNode QName
d Nat
i), Occurrence
pol')
        else Occurrence -> TCM (Maybe Node, Occurrence)
addPol forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. SemiRing a => a -> a -> a
otimes Occurrence
pol' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Nat -> TCMT IO Occurrence
getArgOccurrence QName
d Nat
i
    Where
UnderInf       -> Occurrence -> TCM (Maybe Node, Occurrence)
addPol Occurrence
GuardPos -- Andreas, 2012-06-09: ∞ is guarding
    ConArgType QName
_   -> TCM (Maybe Node, Occurrence)
keepGoing
    IndArgType QName
_   -> forall {a}. TCMT IO (Maybe a, Occurrence)
mixed
    InClause Nat
_     -> TCM (Maybe Node, Occurrence)
keepGoing
    Where
Matched        -> forall {a}. TCMT IO (Maybe a, Occurrence)
mixed -- consider arguments matched against as used
    Where
IsIndex        -> forall {a}. TCMT IO (Maybe a, Occurrence)
mixed -- And similarly for indices.
    InDefOf QName
d      -> do
      Occurrence
pol' <- QName -> TCMT IO Occurrence
isGuarding QName
d
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (QName -> Node
DefNode QName
d), Occurrence
pol')
    where
    keepGoing :: TCM (Maybe Node, Occurrence)
keepGoing   = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, Occurrence
pol)
    mixed :: TCMT IO (Maybe a, Occurrence)
mixed       = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, Occurrence
Mixed)
    negative :: TCM (Maybe Node, Occurrence)
negative    = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, forall a. SemiRing a => a -> a -> a
otimes Occurrence
pol Occurrence
JustNeg)
    addPol :: Occurrence -> TCM (Maybe Node, Occurrence)
addPol Occurrence
pol' = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, forall a. SemiRing a => a -> a -> a
otimes Occurrence
pol Occurrence
pol')

  isGuarding :: QName -> TCMT IO Occurrence
isGuarding QName
d = do
    Maybe DataOrRecord
isDR <- QName -> TCM (Maybe DataOrRecord)
isDataOrRecordType QName
d
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Maybe DataOrRecord
isDR of
      Just DataOrRecord
IsData -> Occurrence
GuardPos  -- a datatype is guarding
      Maybe DataOrRecord
_           -> Occurrence
StrictPos

-- Pretty-printing -----------------------------------------------------

instance Pretty Node where
  pretty :: Node -> Doc
pretty = \case
    DefNode QName
q   -> forall a. Pretty a => a -> Doc
P.pretty QName
q
    ArgNode QName
q Nat
i -> forall a. Pretty a => a -> Doc
P.pretty QName
q forall a. Semigroup a => a -> a -> a
<> ArgName -> Doc
P.text (ArgName
"." forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Nat
i)

instance PrettyTCM Node where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Node -> m Doc
prettyTCM = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
P.pretty

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
w)) = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Occurrence
o forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM n
n
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
P.pretty OccursWhere
w
    ]

instance PrettyTCM (Seq OccursWhere) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Seq OccursWhere -> m Doc
prettyTCM =
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
MonadPretty m =>
[OccursWhere] -> m (ArgName, Doc)
prettyOWs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map OccursWhere -> OccursWhere
adjustLeftOfArrow forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OccursWhere] -> [OccursWhere]
uniq forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList
    where
      nth :: a -> [m Doc]
nth a
0 = forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"first"
      nth a
1 = forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"second"
      nth a
2 = forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"third"
      nth a
n = forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show (a
n forall a. Num a => a -> a -> a
+ a
1) forall a. [a] -> [a] -> [a]
++ ArgName
"th"

      -- Removes consecutive duplicates.
      uniq :: [OccursWhere] -> [OccursWhere]
      uniq :: [OccursWhere] -> [OccursWhere]
uniq = forall a b. (a -> b) -> [a] -> [b]
map forall a. [a] -> a
head forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Bool) -> [a] -> [[a]]
List.groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` OccursWhere -> Seq Where
snd')
        where
        snd' :: OccursWhere -> Seq Where
snd' (OccursWhere Range
_ Seq Where
_ Seq Where
ws) = Seq Where
ws

      prettyOWs :: MonadPretty m => [OccursWhere] -> m (String, Doc)
      prettyOWs :: forall (m :: * -> *).
MonadPretty m =>
[OccursWhere] -> m (ArgName, Doc)
prettyOWs []  = forall a. HasCallStack => a
__IMPOSSIBLE__
      prettyOWs [OccursWhere
o] = do
        (ArgName
s, Doc
d) <- forall (m :: * -> *).
MonadPretty m =>
OccursWhere -> m (ArgName, Doc)
prettyOW OccursWhere
o
        forall (m :: * -> *) a. Monad m => a -> m a
return (ArgName
s, Doc
d forall a. Semigroup a => a -> a -> a
<> Doc
".")
      prettyOWs (OccursWhere
o:[OccursWhere]
os) = do
        (ArgName
s1, Doc
d1) <- forall (m :: * -> *).
MonadPretty m =>
OccursWhere -> m (ArgName, Doc)
prettyOW  OccursWhere
o
        (ArgName
s2, Doc
d2) <- forall (m :: * -> *).
MonadPretty m =>
[OccursWhere] -> m (ArgName, Doc)
prettyOWs [OccursWhere]
os
        forall (m :: * -> *) a. Monad m => a -> m a
return (ArgName
s1, Doc
d1 forall a. Semigroup a => a -> a -> a
<> (Doc
"," Doc -> Doc -> Doc
P.<+> Doc
"which" Doc -> Doc -> Doc
P.<+> ArgName -> Doc
P.text ArgName
s2 Doc -> Doc -> Doc
P.$$ Doc
d2))

      prettyOW :: MonadPretty m => OccursWhere -> m (String, Doc)
      prettyOW :: forall (m :: * -> *).
MonadPretty m =>
OccursWhere -> m (ArgName, Doc)
prettyOW (OccursWhere Range
_ Seq Where
cs Seq Where
ws)
        | forall a. Null a => a -> Bool
null Seq Where
cs   = forall (m :: * -> *).
MonadPretty m =>
Seq Where -> m (ArgName, Doc)
prettyWs Seq Where
ws
        | Bool
otherwise = do
            (ArgName
s, Doc
d1) <- forall (m :: * -> *).
MonadPretty m =>
Seq Where -> m (ArgName, Doc)
prettyWs Seq Where
ws
            (ArgName
_, Doc
d2) <- forall (m :: * -> *).
MonadPretty m =>
Seq Where -> m (ArgName, Doc)
prettyWs Seq Where
cs
            forall (m :: * -> *) a. Monad m => a -> m a
return (ArgName
s, Doc
d1 Doc -> Doc -> Doc
P.$$ Doc
"(" forall a. Semigroup a => a -> a -> a
<> Doc
d2 forall a. Semigroup a => a -> a -> a
<> Doc
")")

      prettyWs :: MonadPretty m => Seq Where -> m (String, Doc)
      prettyWs :: forall (m :: * -> *).
MonadPretty m =>
Seq Where -> m (ArgName, Doc)
prettyWs Seq Where
ws = case forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Seq Where
ws of
        [InDefOf QName
d, Where
IsIndex] ->
          (,) ArgName
"is" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"an index of" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d])
        [Where]
_ ->
          (,) ArgName
"occurs" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
Fold.foldrM (\Where
w Doc
d -> forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *). MonadPretty m => Where -> [m Doc]
prettyW Where
w)) forall a. Null a => a
empty Seq Where
ws

      prettyW :: MonadPretty m => Where -> [m Doc]
      prettyW :: forall (m :: * -> *). MonadPretty m => Where -> [m Doc]
prettyW = \case
        Where
LeftOfArrow  -> forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"to the left of an arrow"
        DefArg QName
q Nat
i   -> forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"in the" forall a. [a] -> [a] -> [a]
++ forall {a} {m :: * -> *}.
(Eq a, Num a, Applicative m, Show a) =>
a -> [m Doc]
nth Nat
i forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"argument of" forall a. [a] -> [a] -> [a]
++
                          [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q]
        Where
UnderInf     -> forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"under" forall a. [a] -> [a] -> [a]
++
                        [do -- this cannot fail if an 'UnderInf' has been generated
                            Def QName
inf Elims
_ <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
getBuiltin' ArgName
builtinInf
                            forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
inf]
        Where
VarArg       -> forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"in an argument of a bound variable"
        Where
MetaArg      -> forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"in an argument of a metavariable"
        ConArgType QName
c -> forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"in the type of the constructor" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c]
        IndArgType QName
c -> forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"in an index of the target type of the constructor" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c]
        InClause Nat
i   -> forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"in the" forall a. [a] -> [a] -> [a]
++ forall {a} {m :: * -> *}.
(Eq a, Num a, Applicative m, Show a) =>
a -> [m Doc]
nth Nat
i forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"clause"
        Where
Matched      -> forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"as matched against"
        Where
IsIndex      -> forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"as an index"
        InDefOf QName
d    -> forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"in the definition of" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d]

      adjustLeftOfArrow :: OccursWhere -> OccursWhere
      adjustLeftOfArrow :: OccursWhere -> OccursWhere
adjustLeftOfArrow (OccursWhere Range
r Seq Where
cs Seq Where
os) =
        Range -> Seq Where -> Seq Where -> OccursWhere
OccursWhere Range
r (forall a. (a -> Bool) -> Seq a -> Seq a
DS.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Where -> Bool
isArrow) Seq Where
cs) forall a b. (a -> b) -> a -> b
$
          Seq Where
noArrows
            forall a. Seq a -> Seq a -> Seq a
DS.><
          case forall a. Seq a -> ViewL a
DS.viewl Seq Where
startsWithArrow of
            ViewL Where
DS.EmptyL  -> forall a. Seq a
DS.empty
            Where
w DS.:< Seq Where
ws -> Where
w forall a. a -> Seq a -> Seq a
DS.<| forall a. (a -> Bool) -> Seq a -> Seq a
DS.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Where -> Bool
isArrow) Seq Where
ws
        where
        (Seq Where
noArrows, Seq Where
startsWithArrow) = forall a. (a -> Bool) -> Seq a -> (Seq a, Seq a)
DS.breakl Where -> Bool
isArrow Seq Where
os

        isArrow :: Where -> Bool
isArrow LeftOfArrow{} = Bool
True
        isArrow Where
_             = Bool
False