{-# LANGUAGE BangPatterns         #-}
{-# LANGUAGE TypeFamilies         #-}  -- for type equality ~
{-# LANGUAGE UndecidableInstances #-}

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

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.Monoid (mconcat)
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.Position (HasRange(..), noRange)
import Agda.TypeChecking.Datatypes ( isDataOrRecordType )
import Agda.TypeChecking.Functions
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin (builtinInf, getBuiltin', CoinductionKit(..), coinductionKit)
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 = Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
qset
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.pos.tick" VerboseLevel
100 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"positivity of" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [QName] -> TCM 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) =
        Graph Node Occurrence -> (Graph Node Occurrence, [SCC Node])
forall n e.
(Ord n, Eq e, StarSemiRing e) =>
Graph n e -> (Graph n e, [SCC n])
Graph.gaussJordanFloydWarshallMcNaughtonYamada (Graph Node Occurrence -> (Graph Node Occurrence, [SCC Node]))
-> Graph Node Occurrence -> (Graph Node Occurrence, [SCC Node])
forall a b. (a -> b) -> a -> b
$ (Edge OccursWhere -> Occurrence)
-> Graph Node (Edge OccursWhere) -> Graph Node Occurrence
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Edge OccursWhere -> Occurrence
forall a. Edge a -> Occurrence
occ Graph Node (Edge OccursWhere)
g
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.pos.tick" VerboseLevel
100 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"constructed graph"
  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.pos.graph" VerboseLevel
5 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Positivity graph: N=" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Set Node -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size (Set Node -> VerboseLevel) -> Set Node -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ Graph Node (Edge OccursWhere) -> Set Node
forall n e. Graph n e -> Set n
Graph.nodes Graph Node (Edge OccursWhere)
g) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
                               VerboseKey
" E=" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show ([Edge Node (Edge OccursWhere)] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length ([Edge Node (Edge OccursWhere)] -> VerboseLevel)
-> [Edge Node (Edge OccursWhere)] -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ Graph Node (Edge OccursWhere) -> [Edge Node (Edge OccursWhere)]
forall n e. Graph n e -> [Edge n e]
Graph.edges Graph Node (Edge OccursWhere)
g)
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.pos.graph" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ TCM Doc
"positivity graph for" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (QName -> TCM Doc) -> [QName] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [QName]
qs)
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Graph Node (Edge OccursWhere) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Graph Node (Edge OccursWhere)
g
    ]
  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.pos.graph" VerboseLevel
5 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
    VerboseKey
"Positivity graph (completed): E=" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show ([Edge Node Occurrence] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length ([Edge Node Occurrence] -> VerboseLevel)
-> [Edge Node Occurrence] -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ Graph Node Occurrence -> [Edge Node Occurrence]
forall n e. Graph n e -> [Edge n e]
Graph.edges Graph Node Occurrence
gstar)
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.pos.graph" VerboseLevel
50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ TCM Doc
"transitive closure of positivity graph for" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
      [QName] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [QName]
qs
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Graph Node Occurrence -> TCM Doc
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
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.pos.tick" VerboseLevel
100 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"set args"

  -- check positivity for all strongly connected components of the graph for qs
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.pos.graph.sccs" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    let ([Node]
triv, [[Node]]
others) = [Either Node [Node]] -> ([Node], [[Node]])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either Node [Node]] -> ([Node], [[Node]]))
-> [Either Node [Node]] -> ([Node], [[Node]])
forall a b. (a -> b) -> a -> b
$ [SCC Node]
-> (SCC Node -> Either Node [Node]) -> [Either Node [Node]]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [SCC Node]
sccs ((SCC Node -> Either Node [Node]) -> [Either Node [Node]])
-> (SCC Node -> Either Node [Node]) -> [Either Node [Node]]
forall a b. (a -> b) -> a -> b
$ \case
          AcyclicSCC Node
v -> Node -> Either Node [Node]
forall a b. a -> Either a b
Left Node
v
          CyclicSCC [Node]
vs -> [Node] -> Either Node [Node]
forall a b. b -> Either a b
Right [Node]
vs
    [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show ([Node] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Node]
triv) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" trivial sccs"
        , VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show ([[Node]] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [[Node]]
others) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" non-trivial sccs with lengths " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
            [VerboseLevel] -> VerboseKey
forall a. Show a => a -> VerboseKey
show (([Node] -> VerboseLevel) -> [[Node]] -> [VerboseLevel]
forall a b. (a -> b) -> [a] -> [b]
map [Node] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [[Node]]
others)
        ]
  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.pos.graph.sccs" VerboseLevel
15 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
    VerboseKey
"  sccs = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [[Node]] -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow [ [Node]
scc | CyclicSCC [Node]
scc <- [SCC Node]
sccs ]
  [SCC Node] -> (SCC Node -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [SCC Node]
sccs ((SCC Node -> TCM ()) -> TCM ()) -> (SCC Node -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \case
    -- If the mutuality information has never been set, we set it to []
    AcyclicSCC (DefNode QName
q) -> TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Maybe [QName] -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe [QName] -> Bool) -> TCMT IO (Maybe [QName]) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Maybe [QName])
getMutual QName
q) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.pos.mutual" VerboseLevel
10 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"setting " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
q VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" to non-recursive"
      -- Andreas, 2017-04-26, issue #2555
      -- We should not have @DefNode@s pointing outside our formal mutual block.
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member QName
q Set QName
qset) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      QName -> [QName] -> TCM ()
setMutual QName
q []
    AcyclicSCC (ArgNode{}) -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    CyclicSCC [Node]
scc          -> [QName] -> TCM ()
setMut [ QName
q | DefNode QName
q <- [Node]
scc ]
  (QName -> TCM ()) -> [QName] -> TCM ()
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
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.pos.tick" VerboseLevel
100 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM 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 = QName -> (Definition -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q ((Definition -> TCM ()) -> TCM ())
-> (Definition -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Definition
_def -> do
      -- we check positivity only for data or record definitions
      TCMT IO (Maybe DataOrRecord) -> (DataOrRecord -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (QName -> TCMT IO (Maybe DataOrRecord)
isDatatype QName
q) ((DataOrRecord -> TCM ()) -> TCM ())
-> (DataOrRecord -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ DataOrRecord
dr -> do
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.pos.check" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Checking positivity of" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q

        let loop :: Maybe Occurrence
            loop :: Maybe Occurrence
loop = Node -> Node -> Graph Node Occurrence -> Maybe Occurrence
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' = (Edge OccursWhere -> Edge (Seq OccursWhere))
-> Graph Node (Edge OccursWhere)
-> Graph Node (Edge (Seq OccursWhere))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((OccursWhere -> Seq OccursWhere)
-> Edge OccursWhere -> Edge (Seq OccursWhere)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap OccursWhere -> Seq OccursWhere
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 (Edge (Seq OccursWhere) -> Occurrence)
-> Graph Node (Edge (Seq OccursWhere))
-> Node
-> Node
-> Occurrence
-> Maybe (Edge (Seq OccursWhere))
forall e n.
(SemiRing e, Ord n) =>
(e -> Occurrence) -> Graph n e -> n -> n -> Occurrence -> Maybe e
productOfEdgesInBoundedWalk
                     Edge (Seq OccursWhere) -> Occurrence
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           -> Seq OccursWhere
forall a. HasCallStack => a
__IMPOSSIBLE__

            how :: String -> Occurrence -> TCM Doc
            how :: VerboseKey -> Occurrence -> TCM Doc
how VerboseKey
msg Occurrence
bound = [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
                  [QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q] [TCM Doc] -> [TCM Doc] -> [TCM Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [TCM Doc]
forall (m :: * -> *). Monad m => VerboseKey -> [m Doc]
pwords VerboseKey
"is" [TCM Doc] -> [TCM Doc] -> [TCM Doc]
forall a. [a] -> [a] -> [a]
++
                  VerboseKey -> [TCM Doc]
forall (m :: * -> *). Monad m => VerboseKey -> [m Doc]
pwords (VerboseKey
msg VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
", because it occurs") [TCM Doc] -> [TCM Doc] -> [TCM Doc]
forall a. [a] -> [a] -> [a]
++
                  [Seq OccursWhere -> TCM Doc
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.
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (MutualInfo -> PositivityCheck
Info.mutualPositivityCheck MutualInfo
mi PositivityCheck -> PositivityCheck -> Bool
forall a. Eq a => a -> a -> Bool
== PositivityCheck
YesPositivityCheck) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
          TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
positivityCheckEnabled (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
            case Maybe Occurrence
loop of
            Just Occurrence
o | Occurrence
o Occurrence -> Occurrence -> Bool
forall a. Ord a => a -> a -> Bool
<= Occurrence
JustPos ->
              Warning -> TCM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Seq OccursWhere -> Warning
NotStrictlyPositive QName
q (Occurrence -> Seq OccursWhere
reason Occurrence
JustPos)
            Maybe Occurrence
_ -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

        -- if we find an unguarded record, mark it as such
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DataOrRecord
dr DataOrRecord -> DataOrRecord -> Bool
forall a. Eq a => a -> a -> Bool
== DataOrRecord
IsRecord) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
          case Maybe Occurrence
loop of
            Just Occurrence
o | Occurrence
o Occurrence -> Occurrence -> Bool
forall a. Ord a => a -> a -> Bool
<= Occurrence
StrictPos -> do
              VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.pos.record" VerboseLevel
5 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Occurrence -> TCM Doc
how VerboseKey
"not guarded" Occurrence
StrictPos
              QName -> TCM ()
unguardedRecord QName
q
              QName -> TCM ()
checkInduction QName
q
            -- otherwise, if the record is recursive, mark it as well
            Just Occurrence
o | Occurrence
o Occurrence -> Occurrence -> Bool
forall a. Ord a => a -> a -> Bool
<= Occurrence
GuardPos -> do
              VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.pos.record" VerboseLevel
5 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Occurrence -> TCM Doc
how VerboseKey
"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
              VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.pos.record" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
                TCM Doc
"record type " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                TCM Doc
"is not recursive"
              QName -> TCM ()
nonRecursiveRecord QName
q
            Maybe Occurrence
_ -> () -> TCM ()
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.
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (MutualInfo -> PositivityCheck
Info.mutualPositivityCheck MutualInfo
mi PositivityCheck -> PositivityCheck -> Bool
forall a. Eq a => a -> a -> Bool
== PositivityCheck
YesPositivityCheck) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
positivityCheckEnabled (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        -- Check whether the recursive record has been declared as
        -- 'Inductive' or 'Coinductive'.  Otherwise, error.
        TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Maybe Induction -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Induction -> Bool)
-> (Definition -> Maybe Induction) -> Definition -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Maybe Induction
recInduction (Defn -> Maybe Induction)
-> (Definition -> Defn) -> Definition -> Maybe Induction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> Bool) -> TCMT IO Definition -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
          Range -> TCM () -> TCM ()
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange (Name -> Range
nameBindingSite (Name -> Range) -> Name -> Range
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
q) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
            TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM ()) -> TCM Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
              TCM Doc
"Recursive record" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
              TCM 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 -> TCMT IO (Maybe DataOrRecord)
isDatatype QName
q = do
      Defn
def <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
      Maybe DataOrRecord -> TCMT IO (Maybe DataOrRecord)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe DataOrRecord -> TCMT IO (Maybe DataOrRecord))
-> Maybe DataOrRecord -> TCMT IO (Maybe DataOrRecord)
forall a b. (a -> b) -> a -> b
$ case Defn
def of
        Datatype{dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
Nothing} -> DataOrRecord -> Maybe DataOrRecord
forall a. a -> Maybe a
Just DataOrRecord
IsData
        Record  {recClause :: Defn -> Maybe Clause
recClause  = Maybe Clause
Nothing} -> DataOrRecord -> Maybe DataOrRecord
forall a. a -> Maybe a
Just DataOrRecord
IsRecord
        Defn
_ -> Maybe DataOrRecord
forall a. Maybe a
Nothing

    -- Set the mutually recursive identifiers for a SCC.
    setMut :: [QName] -> TCM ()
    setMut :: [QName] -> TCM ()
setMut [] = () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- nothing to do
    setMut [QName]
qs = [QName] -> (QName -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [QName]
qs ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ QName
q -> do
      VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.pos.mutual" VerboseLevel
10 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"setting " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
q VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" 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 ]
      [QName] -> (QName -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [QName]
qs ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ QName
q -> QName -> (Definition -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q ((Definition -> TCM ()) -> TCM ())
-> (Definition -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Definition
def -> Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Defn -> Bool
hasDefinition (Defn -> Bool) -> Defn -> Bool
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.pos.args" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"checking args of" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
        VerboseLevel
n <- Definition -> TCM VerboseLevel
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 :: VerboseLevel -> Occurrence
findOcc VerboseLevel
i = Occurrence -> Maybe Occurrence -> Occurrence
forall a. a -> Maybe a -> a
fromMaybe Occurrence
Unused (Maybe Occurrence -> Occurrence) -> Maybe Occurrence -> Occurrence
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Graph Node Occurrence -> Maybe Occurrence
forall n e. Ord n => n -> n -> Graph n e -> Maybe e
Graph.lookup (QName -> VerboseLevel -> Node
ArgNode QName
q VerboseLevel
i) (QName -> Node
DefNode QName
q) Graph Node Occurrence
g
            args :: [Occurrence]
args = -- caseMaybe (Map.lookup q maxs) (replicate n Unused) $ \ m ->
              (VerboseLevel -> Occurrence) -> [VerboseLevel] -> [Occurrence]
forall a b. (a -> b) -> [a] -> [b]
map VerboseLevel -> Occurrence
findOcc [VerboseLevel
0 .. VerboseLevel
nVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-VerboseLevel
1]  -- [0 .. max m (n - 1)] -- triggers issue #3049
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.pos.args" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
          [ TCM Doc
"args of" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"="
          , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (Occurrence -> TCM Doc) -> [Occurrence] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> TCM Doc
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.
        QName -> [Occurrence] -> TCM ()
setArgOccurrences QName
q ([Occurrence] -> TCM ()) -> [Occurrence] -> TCM ()
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
        Constructor{}      -> Bool
False
        Function{}         -> Bool
True
        Datatype{}         -> Bool
True
        Record{}           -> Bool
True

getDefArity :: Definition -> TCM Int
getDefArity :: Definition -> TCM VerboseLevel
getDefArity Definition
def = do
  let dropped :: VerboseLevel
dropped = case Definition -> Defn
theDef Definition
def of
        defn :: Defn
defn@Function{} -> Defn -> VerboseLevel
projectionArgs Defn
defn
        Defn
_ -> VerboseLevel
0
  -- TODO: instantiateFull followed by arity could perhaps be
  -- optimised, presumably the instantiation can be performed
  -- lazily.
  VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
subtract VerboseLevel
dropped (VerboseLevel -> VerboseLevel)
-> (Type -> VerboseLevel) -> Type -> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> VerboseLevel
arity (Type -> VerboseLevel) -> TCMT IO Type -> TCM VerboseLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Definition -> Type
defType Definition
def)

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

data Item = AnArg Nat
          | ADef QName
  deriving (Item -> Item -> Bool
(Item -> Item -> Bool) -> (Item -> Item -> Bool) -> Eq Item
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
Eq Item
-> (Item -> Item -> Ordering)
-> (Item -> Item -> Bool)
-> (Item -> Item -> Bool)
-> (Item -> Item -> Bool)
-> (Item -> Item -> Bool)
-> (Item -> Item -> Item)
-> (Item -> Item -> Item)
-> Ord 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
$cp1Ord :: Eq Item
Ord, VerboseLevel -> Item -> VerboseKey -> VerboseKey
[Item] -> VerboseKey -> VerboseKey
Item -> VerboseKey
(VerboseLevel -> Item -> VerboseKey -> VerboseKey)
-> (Item -> VerboseKey)
-> ([Item] -> VerboseKey -> VerboseKey)
-> Show Item
forall a.
(VerboseLevel -> a -> VerboseKey -> VerboseKey)
-> (a -> VerboseKey) -> ([a] -> VerboseKey -> VerboseKey) -> Show a
showList :: [Item] -> VerboseKey -> VerboseKey
$cshowList :: [Item] -> VerboseKey -> VerboseKey
show :: Item -> VerboseKey
$cshow :: Item -> VerboseKey
showsPrec :: VerboseLevel -> Item -> VerboseKey -> VerboseKey
$cshowsPrec :: VerboseLevel -> Item -> VerboseKey -> VerboseKey
Show)

instance HasRange Item where
  getRange :: Item -> Range
getRange (AnArg VerboseLevel
_) = Range
forall a. Range' a
noRange
  getRange (ADef QName
qn)   = QName -> Range
forall t. HasRange t => t -> Range
getRange 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 = OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder
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 VerboseLevel
-> OccurrencesBuilder -> Maybe OccurrencesBuilder'
pp Maybe VerboseLevel
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 VerboseLevel
-> OccurrencesBuilder -> Maybe OccurrencesBuilder'
pp !Maybe VerboseLevel
m = \case
    Concat [OccurrencesBuilder]
obs -> case (OccurrencesBuilder -> Maybe OccurrencesBuilder')
-> [OccurrencesBuilder] -> [OccurrencesBuilder']
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Maybe VerboseLevel
-> OccurrencesBuilder -> Maybe OccurrencesBuilder'
pp Maybe VerboseLevel
m) [OccurrencesBuilder]
obs of
      []  -> Maybe OccurrencesBuilder'
forall a. Maybe a
Nothing
      [OccurrencesBuilder']
obs -> OccurrencesBuilder' -> Maybe OccurrencesBuilder'
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 (OccurrencesBuilder' -> OccurrencesBuilder')
-> Maybe OccurrencesBuilder' -> Maybe OccurrencesBuilder'
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe VerboseLevel
-> OccurrencesBuilder -> Maybe OccurrencesBuilder'
pp Maybe VerboseLevel
m OccurrencesBuilder
ob

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

    OccursHere Item
i -> do
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
keep
      OccurrencesBuilder' -> Maybe OccurrencesBuilder'
forall (m :: * -> *) a. Monad m => a -> m a
return (Item -> OccurrencesBuilder'
OccursHere' Item
i)
      where
      keep :: Bool
keep = case (Maybe VerboseLevel
m, Item
i) of
        (Maybe VerboseLevel
Nothing, Item
_)      -> Bool
True
        (Maybe VerboseLevel
_, ADef QName
_)       -> Bool
True
        (Just VerboseLevel
m, AnArg VerboseLevel
i) -> VerboseLevel
i VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
< VerboseLevel
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 =
  (Integer -> Integer -> Integer)
-> [(Item, Integer)] -> Map Item Integer
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) ([(Item, Integer)] -> Map Item Integer)
-> (OccurrencesBuilder -> [(Item, Integer)])
-> OccurrencesBuilder
-> Map Item Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  (OccurrencesBuilder' -> [(Item, Integer)] -> [(Item, Integer)])
-> [(Item, Integer)] -> OccurrencesBuilder' -> [(Item, Integer)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip OccurrencesBuilder' -> [(Item, Integer)] -> [(Item, Integer)]
flatten' [] (OccurrencesBuilder' -> [(Item, Integer)])
-> (OccurrencesBuilder -> OccurrencesBuilder')
-> OccurrencesBuilder
-> [(Item, Integer)]
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)    = (OccurrencesBuilder'
 -> ([(Item, Integer)] -> [(Item, Integer)])
 -> [(Item, Integer)]
 -> [(Item, Integer)])
-> ([(Item, Integer)] -> [(Item, Integer)])
-> [OccurrencesBuilder']
-> [(Item, Integer)]
-> [(Item, Integer)]
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 ([(Item, Integer)] -> [(Item, Integer)])
-> ([(Item, Integer)] -> [(Item, Integer)])
-> [(Item, Integer)]
-> [(Item, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Item, Integer)] -> [(Item, Integer)]
f) [(Item, Integer)] -> [(Item, Integer)]
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) (Item, Integer) -> [(Item, Integer)] -> [(Item, Integer)]
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 => Semigroup (OccM a) where
  OccM a
ma <> :: OccM a -> OccM a -> OccM a
<> OccM a
mb = (a -> a -> a) -> OccM a -> OccM a -> OccM a
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>) OccM a
ma OccM a
mb

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

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

withExtendedOccEnv' :: [Maybe Item] -> OccM a -> OccM a
withExtendedOccEnv' :: [Maybe Item] -> OccM a -> OccM a
withExtendedOccEnv' [Maybe Item]
is = (OccEnv -> OccEnv) -> OccM a -> OccM a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((OccEnv -> OccEnv) -> OccM a -> OccM a)
-> (OccEnv -> OccEnv) -> OccM a -> OccM a
forall a b. (a -> b) -> a -> b
$ \ OccEnv
e -> OccEnv
e { vars :: [Maybe Item]
vars = [Maybe Item]
is [Maybe Item] -> [Maybe Item] -> [Maybe Item]
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 :: [Maybe Item] -> a -> TCM OccurrencesBuilder
getOccurrences [Maybe Item]
vars a
a = do
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.pos.occ" VerboseLevel
70 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"computing occurrences in " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (a -> VerboseKey
forall a. Show a => a -> VerboseKey
show a
a)
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.pos.occ" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"computing occurrences in " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
a
  Maybe CoinductionKit
kit <- TCM (Maybe CoinductionKit)
coinductionKit
  OccurrencesBuilder -> TCM OccurrencesBuilder
forall (m :: * -> *) a. Monad m => a -> m a
return (OccurrencesBuilder -> TCM OccurrencesBuilder)
-> OccurrencesBuilder -> TCM OccurrencesBuilder
forall a b. (a -> b) -> a -> b
$ Reader OccEnv OccurrencesBuilder -> OccEnv -> OccurrencesBuilder
forall r a. Reader r a -> r -> a
runReader (a -> Reader OccEnv OccurrencesBuilder
forall a.
ComputeOccurrences a =>
a -> Reader OccEnv OccurrencesBuilder
occurrences a
a) (OccEnv -> OccurrencesBuilder) -> OccEnv -> OccurrencesBuilder
forall a b. (a -> b) -> a -> b
$ [Maybe Item] -> Maybe QName -> OccEnv
OccEnv [Maybe Item]
vars (Maybe QName -> OccEnv) -> Maybe QName -> OccEnv
forall a b. (a -> b) -> a -> b
$ (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CoinductionKit -> QName
nameOfInf Maybe CoinductionKit
kit

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

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

instance ComputeOccurrences Clause where
  occurrences :: Clause -> Reader OccEnv OccurrencesBuilder
occurrences Clause
cl = do
    let ps :: NAPs
ps    = Clause -> NAPs
namedClausePats Clause
cl
        items :: [Maybe Item]
items = IntMap (Maybe Item) -> [Maybe Item]
forall a. IntMap a -> [a]
IntMap.elems (IntMap (Maybe Item) -> [Maybe Item])
-> IntMap (Maybe Item) -> [Maybe Item]
forall a b. (a -> b) -> a -> b
$ NAPs -> IntMap (Maybe Item)
patItems NAPs
ps -- sorted from low to high DBI
    ([OccurrencesBuilder] -> OccurrencesBuilder
Concat (((VerboseLevel, Arg (Named NamedName (Pattern' DBPatVar)))
 -> Maybe OccurrencesBuilder)
-> [(VerboseLevel, Arg (Named NamedName (Pattern' DBPatVar)))]
-> [OccurrencesBuilder]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (VerboseLevel, Arg (Named NamedName (Pattern' DBPatVar)))
-> Maybe OccurrencesBuilder
forall name a.
(VerboseLevel, Arg (Named name (Pattern' a)))
-> Maybe OccurrencesBuilder
matching ([VerboseLevel]
-> NAPs
-> [(VerboseLevel, Arg (Named NamedName (Pattern' DBPatVar)))]
forall a b. [a] -> [b] -> [(a, b)]
zip [VerboseLevel
0..] NAPs
ps)) OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder
forall a. Semigroup a => a -> a -> a
<>) (OccurrencesBuilder -> OccurrencesBuilder)
-> Reader OccEnv OccurrencesBuilder
-> Reader OccEnv OccurrencesBuilder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      [Maybe Item]
-> Reader OccEnv OccurrencesBuilder
-> Reader OccEnv OccurrencesBuilder
forall a. [Maybe Item] -> OccM a -> OccM a
withExtendedOccEnv' [Maybe Item]
items (Reader OccEnv OccurrencesBuilder
 -> Reader OccEnv OccurrencesBuilder)
-> Reader OccEnv OccurrencesBuilder
-> Reader OccEnv OccurrencesBuilder
forall a b. (a -> b) -> a -> b
$
        Maybe Term -> Reader OccEnv OccurrencesBuilder
forall a.
ComputeOccurrences a =>
a -> Reader OccEnv OccurrencesBuilder
occurrences (Maybe Term -> Reader OccEnv OccurrencesBuilder)
-> Maybe Term -> Reader OccEnv OccurrencesBuilder
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
cl
    where
      matching :: (VerboseLevel, Arg (Named name (Pattern' a)))
-> Maybe OccurrencesBuilder
matching (VerboseLevel
i, Arg (Named name (Pattern' a))
p)
        | Pattern' a -> Bool
forall a. Pattern' a -> Bool
properlyMatching (Named name (Pattern' a) -> Pattern' a
forall name a. Named name a -> a
namedThing (Named name (Pattern' a) -> Pattern' a)
-> Named name (Pattern' a) -> Pattern' a
forall a b. (a -> b) -> a -> b
$ Arg (Named name (Pattern' a)) -> Named name (Pattern' a)
forall e. Arg e -> e
unArg Arg (Named name (Pattern' a))
p) =
            OccurrencesBuilder -> Maybe OccurrencesBuilder
forall a. a -> Maybe a
Just (OccurrencesBuilder -> Maybe OccurrencesBuilder)
-> OccurrencesBuilder -> Maybe OccurrencesBuilder
forall a b. (a -> b) -> a -> b
$ Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs Where
Matched (OccurrencesBuilder -> OccurrencesBuilder)
-> OccurrencesBuilder -> OccurrencesBuilder
forall a b. (a -> b) -> a -> b
$ Item -> OccurrencesBuilder
OccursHere (Item -> OccurrencesBuilder) -> Item -> OccurrencesBuilder
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Item
AnArg VerboseLevel
i
        | Bool
otherwise                  = Maybe OccurrencesBuilder
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 = [IntMap (Maybe Item)] -> IntMap (Maybe Item)
forall a. Monoid a => [a] -> a
mconcat ([IntMap (Maybe Item)] -> IntMap (Maybe Item))
-> [IntMap (Maybe Item)] -> IntMap (Maybe Item)
forall a b. (a -> b) -> a -> b
$ (VerboseLevel
 -> Arg (Named NamedName (Pattern' DBPatVar))
 -> IntMap (Maybe Item))
-> [VerboseLevel] -> NAPs -> [IntMap (Maybe Item)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith VerboseLevel
-> Arg (Named NamedName (Pattern' DBPatVar)) -> IntMap (Maybe Item)
patItem [VerboseLevel
0..] NAPs
ps

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

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

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

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

    Con ConHead
_ ConInfo
_ Elims
args -> Elims -> Reader OccEnv OccurrencesBuilder
forall a.
ComputeOccurrences a =>
a -> Reader OccEnv OccurrencesBuilder
occurrences Elims
args
    MetaV MetaId
_ Elims
args -> Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs Where
MetaArg (OccurrencesBuilder -> OccurrencesBuilder)
-> Reader OccEnv OccurrencesBuilder
-> Reader OccEnv OccurrencesBuilder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> Reader OccEnv OccurrencesBuilder
forall a.
ComputeOccurrences a =>
a -> Reader OccEnv OccurrencesBuilder
occurrences Elims
args
    Pi Dom Type
a Abs Type
b       -> (Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs Where
LeftOfArrow (OccurrencesBuilder -> OccurrencesBuilder)
-> Reader OccEnv OccurrencesBuilder
-> Reader OccEnv OccurrencesBuilder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> Reader OccEnv OccurrencesBuilder
forall a.
ComputeOccurrences a =>
a -> Reader OccEnv OccurrencesBuilder
occurrences Dom Type
a) Reader OccEnv OccurrencesBuilder
-> Reader OccEnv OccurrencesBuilder
-> Reader OccEnv OccurrencesBuilder
forall a. Semigroup a => a -> a -> a
<> Abs Type -> Reader OccEnv OccurrencesBuilder
forall a.
ComputeOccurrences a =>
a -> Reader OccEnv OccurrencesBuilder
occurrences Abs Type
b
    Lam ArgInfo
_ Abs Term
b      -> Abs Term -> Reader OccEnv OccurrencesBuilder
forall a.
ComputeOccurrences a =>
a -> Reader OccEnv OccurrencesBuilder
occurrences Abs Term
b
    Level Level
l      -> Level -> Reader OccEnv OccurrencesBuilder
forall a.
ComputeOccurrences a =>
a -> Reader OccEnv OccurrencesBuilder
occurrences Level
l
    Lit{}        -> Reader OccEnv OccurrencesBuilder
forall a. Monoid a => a
mempty
    Sort{}       -> Reader OccEnv OccurrencesBuilder
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   -> Term -> Reader OccEnv OccurrencesBuilder
forall a.
ComputeOccurrences a =>
a -> Reader OccEnv OccurrencesBuilder
occurrences Term
v
    Dummy{}      -> Reader OccEnv OccurrencesBuilder
forall a. Monoid a => a
mempty

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

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

instance ComputeOccurrences LevelAtom where
  occurrences :: LevelAtom' Term -> Reader OccEnv OccurrencesBuilder
occurrences = Term -> Reader OccEnv OccurrencesBuilder
forall a.
ComputeOccurrences a =>
a -> Reader OccEnv OccurrencesBuilder
occurrences (Term -> Reader OccEnv OccurrencesBuilder)
-> (LevelAtom' Term -> Term)
-> LevelAtom' Term
-> Reader OccEnv OccurrencesBuilder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LevelAtom' Term -> Term
unLevelAtom
      -- MetaLevel x es -> occurrences $ MetaV x es
      -- Andreas, 2016-07-25, issue 2108
      -- NOT: OccursAs MetaArg <$> occurrences es
      -- since we need to unSpine!
      -- (Otherwise, we run into __IMPOSSIBLE__ at Proj elims)

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

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

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

instance ComputeOccurrences a => ComputeOccurrences (Elim' a) where
  occurrences :: Elim' a -> Reader OccEnv OccurrencesBuilder
occurrences Proj{}         = Reader OccEnv OccurrencesBuilder
forall a. HasCallStack => a
__IMPOSSIBLE__  -- unSpine
  occurrences (Apply Arg a
a)      = Arg a -> Reader OccEnv OccurrencesBuilder
forall a.
ComputeOccurrences a =>
a -> Reader OccEnv OccurrencesBuilder
occurrences Arg a
a
  occurrences (IApply a
x a
y a
a) = (a, (a, a)) -> Reader OccEnv OccurrencesBuilder
forall a.
ComputeOccurrences a =>
a -> Reader OccEnv 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) -> Reader OccEnv OccurrencesBuilder
occurrences (a
x, b
y) = a -> Reader OccEnv OccurrencesBuilder
forall a.
ComputeOccurrences a =>
a -> Reader OccEnv OccurrencesBuilder
occurrences a
x Reader OccEnv OccurrencesBuilder
-> Reader OccEnv OccurrencesBuilder
-> Reader OccEnv OccurrencesBuilder
forall a. Semigroup a => a -> a -> a
<> b -> Reader OccEnv OccurrencesBuilder
forall a.
ComputeOccurrences a =>
a -> Reader OccEnv 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 (OccurrencesBuilder -> Map Item Integer)
-> TCM OccurrencesBuilder -> TCM (Map Item Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM OccurrencesBuilder
computeOccurrences' QName
q

-- | Computes the occurrences in the given definition.
computeOccurrences' :: QName -> TCM OccurrencesBuilder
computeOccurrences' :: QName -> TCM OccurrencesBuilder
computeOccurrences' QName
q = QName
-> (Definition -> TCM OccurrencesBuilder) -> TCM OccurrencesBuilder
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q ((Definition -> TCM OccurrencesBuilder) -> TCM OccurrencesBuilder)
-> (Definition -> TCM OccurrencesBuilder) -> TCM OccurrencesBuilder
forall a b. (a -> b) -> a -> b
$ \ Definition
def -> do
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.pos" VerboseLevel
25 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    let a :: IsAbstract
a = Definition -> IsAbstract
defAbstract Definition
def
    AbstractMode
m <- (TCEnv -> AbstractMode) -> TCMT IO AbstractMode
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> AbstractMode
envAbstractMode
    ModuleName
cur <- (TCEnv -> ModuleName) -> TCMT IO ModuleName
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> ModuleName
envCurrentModule
    TCM Doc
"computeOccurrences" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (IsAbstract -> VerboseKey
forall a. Show a => a -> VerboseKey
show IsAbstract
a) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (AbstractMode -> VerboseKey
forall a. Show a => a -> VerboseKey
show AbstractMode
m)
      TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
cur
  Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs (QName -> Where
InDefOf QName
q) (OccurrencesBuilder -> OccurrencesBuilder)
-> TCM OccurrencesBuilder -> TCM OccurrencesBuilder
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 <- (Clause -> TCMT IO Clause) -> [Clause] -> TCMT IO [Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Clause -> TCMT IO Clause
forall (tcm :: * -> *). MonadTCM tcm => Clause -> tcm Clause
etaExpandClause ([Clause] -> TCMT IO [Clause])
-> TCMT IO [Clause] -> TCMT IO [Clause]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Clause] -> TCMT IO [Clause]
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull [Clause]
cs
      [OccurrencesBuilder] -> OccurrencesBuilder
Concat ([OccurrencesBuilder] -> OccurrencesBuilder)
-> ([OccurrencesBuilder] -> [OccurrencesBuilder])
-> [OccurrencesBuilder]
-> OccurrencesBuilder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VerboseLevel -> OccurrencesBuilder -> OccurrencesBuilder)
-> [VerboseLevel] -> [OccurrencesBuilder] -> [OccurrencesBuilder]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs (Where -> OccurrencesBuilder -> OccurrencesBuilder)
-> (VerboseLevel -> Where)
-> VerboseLevel
-> OccurrencesBuilder
-> OccurrencesBuilder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> Where
InClause) [VerboseLevel
0..] ([OccurrencesBuilder] -> OccurrencesBuilder)
-> TCMT IO [OccurrencesBuilder] -> TCM OccurrencesBuilder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        (Clause -> TCM OccurrencesBuilder)
-> [Clause] -> TCMT IO [OccurrencesBuilder]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Maybe Item] -> Clause -> TCM OccurrencesBuilder
forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCM OccurrencesBuilder
getOccurrences []) [Clause]
cs

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

    Record{recClause :: Defn -> Maybe Clause
recClause = Just Clause
c} -> [Maybe Item] -> Clause -> TCM OccurrencesBuilder
forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCM OccurrencesBuilder
getOccurrences [] (Clause -> TCM OccurrencesBuilder)
-> TCMT IO Clause -> TCM OccurrencesBuilder
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Clause -> TCMT IO Clause
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Clause
c
    Record{recPars :: Defn -> VerboseLevel
recPars = VerboseLevel
np, recTel :: Defn -> Tele (Dom Type)
recTel = Tele (Dom Type)
tel} -> do
      let tel' :: Tele (Dom Type)
tel' = [Dom (VerboseKey, Type)] -> Tele (Dom Type)
telFromList ([Dom (VerboseKey, Type)] -> Tele (Dom Type))
-> [Dom (VerboseKey, Type)] -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ VerboseLevel
-> [Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)]
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
np ([Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)])
-> [Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Tele (Dom Type)
tel
          vars :: [Maybe Item]
vars = (VerboseLevel -> Maybe Item) -> [VerboseLevel] -> [Maybe Item]
forall a b. (a -> b) -> [a] -> [b]
map (Item -> Maybe Item
forall a. a -> Maybe a
Just (Item -> Maybe Item)
-> (VerboseLevel -> Item) -> VerboseLevel -> Maybe Item
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> Item
AnArg) ([VerboseLevel] -> [Maybe Item]) -> [VerboseLevel] -> [Maybe Item]
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [VerboseLevel]
forall a. Integral a => a -> [a]
downFrom VerboseLevel
np
      [Maybe Item] -> Tele (Dom Type) -> TCM OccurrencesBuilder
forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCM OccurrencesBuilder
getOccurrences [Maybe Item]
vars (Tele (Dom Type) -> TCM OccurrencesBuilder)
-> TCMT IO (Tele (Dom Type)) -> TCM OccurrencesBuilder
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Tele (Dom Type) -> TCMT IO (Tele (Dom Type))
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Tele (Dom Type)
tel' -- Andreas, 2017-01-01, issue #1899, treat like data types

    -- Arguments to other kinds of definitions are hard-wired.
    Constructor{}      -> TCM OccurrencesBuilder
forall a. Monoid a => a
mempty
    Axiom{}            -> TCM OccurrencesBuilder
forall a. Monoid a => a
mempty
    DataOrRecSig{}     -> TCM OccurrencesBuilder
forall a. Monoid a => a
mempty
    Primitive{}        -> TCM OccurrencesBuilder
forall a. Monoid a => a
mempty
    GeneralizableVar{} -> TCM OccurrencesBuilder
forall a. Monoid a => a
mempty
    AbstractDefn{}     -> TCM OccurrencesBuilder
forall a. HasCallStack => a
__IMPOSSIBLE__

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

data Node = DefNode !QName
          | ArgNode !QName !Nat
  deriving (Node -> Node -> Bool
(Node -> Node -> Bool) -> (Node -> Node -> Bool) -> Eq Node
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
Eq Node
-> (Node -> Node -> Ordering)
-> (Node -> Node -> Bool)
-> (Node -> Node -> Bool)
-> (Node -> Node -> Bool)
-> (Node -> Node -> Bool)
-> (Node -> Node -> Node)
-> (Node -> Node -> Node)
-> Ord 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
$cp1Ord :: Eq Node
Ord)

-- | Edge labels for the positivity graph.
data Edge a = Edge !Occurrence a
  deriving (Edge a -> Edge a -> Bool
(Edge a -> Edge a -> Bool)
-> (Edge a -> Edge a -> Bool) -> Eq (Edge a)
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, Eq (Edge a)
Eq (Edge a)
-> (Edge a -> Edge a -> Ordering)
-> (Edge a -> Edge a -> Bool)
-> (Edge a -> Edge a -> Bool)
-> (Edge a -> Edge a -> Bool)
-> (Edge a -> Edge a -> Bool)
-> (Edge a -> Edge a -> Edge a)
-> (Edge a -> Edge a -> Edge a)
-> Ord (Edge a)
Edge a -> Edge a -> Bool
Edge a -> Edge a -> Ordering
Edge a -> Edge a -> Edge a
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
$cp1Ord :: forall a. Ord a => Eq (Edge a)
Ord, VerboseLevel -> Edge a -> VerboseKey -> VerboseKey
[Edge a] -> VerboseKey -> VerboseKey
Edge a -> VerboseKey
(VerboseLevel -> Edge a -> VerboseKey -> VerboseKey)
-> (Edge a -> VerboseKey)
-> ([Edge a] -> VerboseKey -> VerboseKey)
-> Show (Edge a)
forall a.
Show a =>
VerboseLevel -> Edge a -> VerboseKey -> VerboseKey
forall a. Show a => [Edge a] -> VerboseKey -> VerboseKey
forall a. Show a => Edge a -> VerboseKey
forall a.
(VerboseLevel -> a -> VerboseKey -> VerboseKey)
-> (a -> VerboseKey) -> ([a] -> VerboseKey -> VerboseKey) -> Show a
showList :: [Edge a] -> VerboseKey -> VerboseKey
$cshowList :: forall a. Show a => [Edge a] -> VerboseKey -> VerboseKey
show :: Edge a -> VerboseKey
$cshow :: forall a. Show a => Edge a -> VerboseKey
showsPrec :: VerboseLevel -> Edge a -> VerboseKey -> VerboseKey
$cshowsPrec :: forall a.
Show a =>
VerboseLevel -> Edge a -> VerboseKey -> VerboseKey
Show, a -> Edge b -> Edge a
(a -> b) -> Edge a -> Edge b
(forall a b. (a -> b) -> Edge a -> Edge b)
-> (forall a b. a -> Edge b -> Edge a) -> Functor Edge
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
<$ :: a -> Edge b -> Edge a
$c<$ :: forall a b. a -> Edge b -> Edge a
fmap :: (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 :: 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)   = Occurrence -> a -> Edge a
forall a. Occurrence -> a -> Edge a
Edge Occurrence
Mixed a
w
mergeEdges e :: Edge a
e@(Edge Occurrence
JustNeg a
w)   Edge a
_                    = Occurrence -> a -> 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 = Occurrence -> Seq OccursWhere -> Edge (Seq OccursWhere)
forall a. Occurrence -> a -> Edge a
Edge Occurrence
forall a. SemiRing a => a
ozero Seq OccursWhere
forall a. Seq a
DS.empty
  oone :: Edge (Seq OccursWhere)
oone  = Occurrence -> Seq OccursWhere -> Edge (Seq OccursWhere)
forall a. Occurrence -> a -> Edge a
Edge Occurrence
forall a. SemiRing a => a
oone  Seq OccursWhere
forall a. Seq a
DS.empty

  oplus :: Edge (Seq OccursWhere)
-> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere)
oplus = Edge (Seq OccursWhere)
-> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere)
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) = Occurrence -> Seq OccursWhere -> Edge (Seq OccursWhere)
forall a. Occurrence -> a -> Edge a
Edge (Occurrence -> Occurrence -> Occurrence
forall a. SemiRing a => a -> a -> a
otimes Occurrence
o1 Occurrence
o2) (Seq OccursWhere
w1 Seq OccursWhere -> Seq OccursWhere -> Seq OccursWhere
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 =
  (Edge OccursWhere -> Edge OccursWhere -> Edge OccursWhere)
-> [Edge Node (Edge OccursWhere)] -> Graph Node (Edge OccursWhere)
forall n e. Ord n => (e -> e -> e) -> [Edge n e] -> Graph n e
Graph.fromEdgesWith Edge OccursWhere -> Edge OccursWhere -> Edge OccursWhere
forall a. Edge a -> Edge a -> Edge a
mergeEdges ([Edge Node (Edge OccursWhere)] -> Graph Node (Edge OccursWhere))
-> ([[Edge Node (Edge OccursWhere)]]
    -> [Edge Node (Edge OccursWhere)])
-> [[Edge Node (Edge OccursWhere)]]
-> Graph Node (Edge OccursWhere)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Edge Node (Edge OccursWhere)]] -> [Edge Node (Edge OccursWhere)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Edge Node (Edge OccursWhere)]] -> Graph Node (Edge OccursWhere))
-> TCMT IO [[Edge Node (Edge OccursWhere)]]
-> TCM (Graph Node (Edge OccursWhere))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    (QName -> TCMT IO [Edge Node (Edge OccursWhere)])
-> [QName] -> TCMT IO [[Edge Node (Edge OccursWhere)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM QName -> TCMT IO [Edge Node (Edge OccursWhere)]
defGraph (Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
qs)
  where
    defGraph :: QName -> TCM [Graph.Edge Node (Edge OccursWhere)]
    defGraph :: QName -> TCMT IO [Edge Node (Edge OccursWhere)]
defGraph QName
q = QName
-> (Definition -> TCMT IO [Edge Node (Edge OccursWhere)])
-> TCMT IO [Edge Node (Edge OccursWhere)]
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q ((Definition -> TCMT IO [Edge Node (Edge OccursWhere)])
 -> TCMT IO [Edge Node (Edge OccursWhere)])
-> (Definition -> TCMT IO [Edge Node (Edge OccursWhere)])
-> TCMT IO [Edge Node (Edge OccursWhere)]
forall a b. (a -> b) -> a -> b
$ \ Definition
_def -> do
      OccurrencesBuilder
occs <- QName -> TCM OccurrencesBuilder
computeOccurrences' QName
q

      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.pos.occs" VerboseLevel
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        ((TCM Doc
"Occurrences in" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q) TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> TCM Doc
":")
          TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$+$
        (VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
           ((Item, Integer) -> TCM Doc) -> [(Item, Integer)] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\(Item
i, Integer
n) ->
                   (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (Item -> VerboseKey
forall a. Show a => a -> VerboseKey
show Item
i) TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> TCM Doc
":") TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (Integer -> VerboseKey
forall a. Show a => a -> VerboseKey
show Integer
n) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                   TCM Doc
"occurrences") ([(Item, Integer)] -> [TCM Doc]) -> [(Item, Integer)] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$
           ((Item, Integer) -> (Item, Integer) -> Ordering)
-> [(Item, Integer)] -> [(Item, Integer)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Integer -> Integer -> Ordering)
-> ((Item, Integer) -> Integer)
-> (Item, Integer)
-> (Item, Integer)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Item, Integer) -> Integer
forall a b. (a, b) -> b
snd) ([(Item, Integer)] -> [(Item, Integer)])
-> [(Item, Integer)] -> [(Item, Integer)]
forall a b. (a -> b) -> a -> b
$
           Map Item Integer -> [(Item, Integer)]
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
-> TCMT IO [Edge Node (Edge OccursWhere)]
computeEdges Set QName
qs QName
q OccurrencesBuilder
occs

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

      [Edge Node (Edge OccursWhere)]
-> TCMT IO [Edge Node (Edge OccursWhere)]
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
-> TCMT IO [Edge Node (Edge OccursWhere)]
computeEdges Set QName
muts QName
q OccurrencesBuilder
ob =
  (([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
-> [Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)]
forall a b. (a -> b) -> a -> b
$ []) (([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
 -> [Edge Node (Edge OccursWhere)])
-> TCMT
     IO
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
-> TCMT IO [Edge Node (Edge OccursWhere)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Occurrence
-> OccurrencesBuilder'
-> Node
-> Seq Where
-> Seq Where
-> TCMT
     IO
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
mkEdge Occurrence
StrictPos (OccurrencesBuilder -> OccurrencesBuilder'
preprocess OccurrencesBuilder
ob)
                    Node
forall a. HasCallStack => a
__IMPOSSIBLE__ Seq Where
forall a. Seq a
DS.empty Seq Where
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
-> TCMT
     IO
     ([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 ->
      (TCMT
   IO
   ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
 -> TCMT
      IO
      ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
 -> TCMT
      IO
      ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)]))
-> TCMT
     IO
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
-> [TCMT
      IO
      ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])]
-> TCMT
     IO
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
 -> ([Edge Node (Edge OccursWhere)]
     -> [Edge Node (Edge OccursWhere)])
 -> [Edge Node (Edge OccursWhere)]
 -> [Edge Node (Edge OccursWhere)])
-> TCMT
     IO
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
-> TCMT
     IO
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
-> TCMT
     IO
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
-> ([Edge Node (Edge OccursWhere)]
    -> [Edge Node (Edge OccursWhere)])
-> [Edge Node (Edge OccursWhere)]
-> [Edge Node (Edge OccursWhere)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)) (([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
-> TCMT
     IO
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
forall (m :: * -> *) a. Monad m => a -> m a
return [Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)]
forall a. a -> a
id)
            [ Occurrence
-> OccurrencesBuilder'
-> Node
-> Seq Where
-> Seq Where
-> TCMT
     IO
     ([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
-> TCMT
     IO
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
mk = Occurrence
-> OccurrencesBuilder'
-> Node
-> Seq Where
-> Seq Where
-> TCMT
     IO
     ([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
-> TCMT
     IO
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
mk Node
to Seq Where
cs            (Seq Where
os Seq Where -> Where -> Seq Where
forall a. Seq a -> a -> Seq a
DS.|> Where
w)
        Just Node
to -> Node
-> Seq Where
-> Seq Where
-> TCMT
     IO
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
mk Node
to (Seq Where
cs Seq Where -> Seq Where -> Seq Where
forall a. Seq a -> Seq a -> Seq a
DS.>< Seq Where
os) (Where -> Seq Where
forall a. a -> Seq a
DS.singleton Where
w)

    OccursHere' Item
i ->
      let o :: OccursWhere
o = Range -> Seq Where -> Seq Where -> OccursWhere
OccursWhere (Item -> Range
forall t. HasRange t => t -> Range
getRange Item
i) Seq Where
cs Seq Where
os in
      case Item
i of
        AnArg VerboseLevel
i ->
          ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
-> TCMT
     IO
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
forall (m :: * -> *) a. Monad m => a -> m a
return (([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
 -> TCMT
      IO
      ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)]))
-> ([Edge Node (Edge OccursWhere)]
    -> [Edge Node (Edge OccursWhere)])
-> TCMT
     IO
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
forall a b. (a -> b) -> a -> b
$ Bool
-> ([Edge Node (Edge OccursWhere)]
    -> [Edge Node (Edge OccursWhere)])
-> [Edge Node (Edge OccursWhere)]
-> [Edge Node (Edge OccursWhere)]
forall a. Bool -> (a -> a) -> a -> a
applyUnless (Occurrence -> Bool
forall a. Null a => a -> Bool
null Occurrence
pol) (Edge :: forall n e. n -> n -> e -> Edge n e
Graph.Edge
            { source :: Node
Graph.source = QName -> VerboseLevel -> Node
ArgNode QName
q VerboseLevel
i
            , target :: Node
Graph.target = Node
to
            , label :: Edge OccursWhere
Graph.label  = Occurrence -> OccursWhere -> Edge OccursWhere
forall a. Occurrence -> a -> Edge a
Edge Occurrence
pol OccursWhere
o
            } Edge Node (Edge OccursWhere)
-> [Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)]
forall a. a -> [a] -> [a]
:)
        ADef QName
q' ->
          -- Andreas, 2017-04-26, issue #2555
          -- Skip nodes pointing outside the mutual block.
          ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
-> TCMT
     IO
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
forall (m :: * -> *) a. Monad m => a -> m a
return (([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
 -> TCMT
      IO
      ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)]))
-> ([Edge Node (Edge OccursWhere)]
    -> [Edge Node (Edge OccursWhere)])
-> TCMT
     IO
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
forall a b. (a -> b) -> a -> b
$ Bool
-> ([Edge Node (Edge OccursWhere)]
    -> [Edge Node (Edge OccursWhere)])
-> [Edge Node (Edge OccursWhere)]
-> [Edge Node (Edge OccursWhere)]
forall a. Bool -> (a -> a) -> a -> a
applyUnless (Occurrence -> Bool
forall a. Null a => a -> Bool
null Occurrence
pol Bool -> Bool -> Bool
|| QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember QName
q' Set QName
muts)
            (Edge :: forall n e. n -> n -> e -> Edge n e
Graph.Edge
               { source :: Node
Graph.source = QName -> Node
DefNode QName
q'
               , target :: Node
Graph.target = Node
to
               , label :: Edge OccursWhere
Graph.label  = Occurrence -> OccursWhere -> Edge OccursWhere
forall a. Occurrence -> a -> Edge a
Edge Occurrence
pol OccursWhere
o
               } Edge Node (Edge OccursWhere)
-> [Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)]
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 Where
w = case Where
w of
    Where
VarArg         -> TCM (Maybe Node, Occurrence)
forall a. TCMT IO (Maybe a, Occurrence)
mixed
    Where
MetaArg        -> TCM (Maybe Node, Occurrence)
forall a. TCMT IO (Maybe a, Occurrence)
mixed
    Where
LeftOfArrow    -> TCM (Maybe Node, Occurrence)
negative
    DefArg QName
d VerboseLevel
i     -> do
      Occurrence
pol' <- QName -> TCMT IO Occurrence
isGuarding QName
d
      if QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member QName
d Set QName
muts
        then (Maybe Node, Occurrence) -> TCM (Maybe Node, Occurrence)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node -> Maybe Node
forall a. a -> Maybe a
Just (QName -> VerboseLevel -> Node
ArgNode QName
d VerboseLevel
i), Occurrence
pol')
        else Occurrence -> TCM (Maybe Node, Occurrence)
addPol (Occurrence -> TCM (Maybe Node, Occurrence))
-> TCMT IO Occurrence -> TCM (Maybe Node, Occurrence)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Occurrence -> Occurrence -> Occurrence
forall a. SemiRing a => a -> a -> a
otimes Occurrence
pol' (Occurrence -> Occurrence)
-> TCMT IO Occurrence -> TCMT IO Occurrence
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> VerboseLevel -> TCMT IO Occurrence
getArgOccurrence QName
d VerboseLevel
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
_   -> TCM (Maybe Node, Occurrence)
forall a. TCMT IO (Maybe a, Occurrence)
mixed
    InClause VerboseLevel
_     -> TCM (Maybe Node, Occurrence)
keepGoing
    Where
Matched        -> TCM (Maybe Node, Occurrence)
forall a. TCMT IO (Maybe a, Occurrence)
mixed -- consider arguments matched against as used
    Where
IsIndex        -> TCM (Maybe Node, Occurrence)
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
      (Maybe Node, Occurrence) -> TCM (Maybe Node, Occurrence)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node -> Maybe Node
forall a. a -> Maybe a
Just (QName -> Node
DefNode QName
d), Occurrence
pol')
    where
    keepGoing :: TCM (Maybe Node, Occurrence)
keepGoing   = (Maybe Node, Occurrence) -> TCM (Maybe Node, Occurrence)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Node
forall a. Maybe a
Nothing, Occurrence
pol)
    mixed :: TCMT IO (Maybe a, Occurrence)
mixed       = (Maybe a, Occurrence) -> TCMT IO (Maybe a, Occurrence)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a
forall a. Maybe a
Nothing, Occurrence
Mixed)
    negative :: TCM (Maybe Node, Occurrence)
negative    = (Maybe Node, Occurrence) -> TCM (Maybe Node, Occurrence)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Node
forall a. Maybe a
Nothing, Occurrence -> Occurrence -> Occurrence
forall a. SemiRing a => a -> a -> a
otimes Occurrence
pol Occurrence
JustNeg)
    addPol :: Occurrence -> TCM (Maybe Node, Occurrence)
addPol Occurrence
pol' = (Maybe Node, Occurrence) -> TCM (Maybe Node, Occurrence)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Node
forall a. Maybe a
Nothing, Occurrence -> Occurrence -> Occurrence
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 -> TCMT IO (Maybe DataOrRecord)
isDataOrRecordType QName
d
    Occurrence -> TCMT IO Occurrence
forall (m :: * -> *) a. Monad m => a -> m a
return (Occurrence -> TCMT IO Occurrence)
-> Occurrence -> TCMT IO Occurrence
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   -> QName -> Doc
forall a. Pretty a => a -> Doc
P.pretty QName
q
    ArgNode QName
q VerboseLevel
i -> QName -> Doc
forall a. Pretty a => a -> Doc
P.pretty QName
q Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> VerboseKey -> Doc
P.text (VerboseKey
"." VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
i)

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

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

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

      -- Removes consecutive duplicates.
      uniq :: [OccursWhere] -> [OccursWhere]
      uniq :: [OccursWhere] -> [OccursWhere]
uniq = ([OccursWhere] -> OccursWhere) -> [[OccursWhere]] -> [OccursWhere]
forall a b. (a -> b) -> [a] -> [b]
map [OccursWhere] -> OccursWhere
forall a. [a] -> a
head ([[OccursWhere]] -> [OccursWhere])
-> ([OccursWhere] -> [[OccursWhere]])
-> [OccursWhere]
-> [OccursWhere]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OccursWhere -> OccursWhere -> Bool)
-> [OccursWhere] -> [[OccursWhere]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
List.groupBy (Seq Where -> Seq Where -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Seq Where -> Seq Where -> Bool)
-> (OccursWhere -> Seq Where) -> OccursWhere -> OccursWhere -> 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 :: [OccursWhere] -> m (VerboseKey, Doc)
prettyOWs []  = m (VerboseKey, Doc)
forall a. HasCallStack => a
__IMPOSSIBLE__
      prettyOWs [OccursWhere
o] = do
        (VerboseKey
s, Doc
d) <- OccursWhere -> m (VerboseKey, Doc)
forall (m :: * -> *).
MonadPretty m =>
OccursWhere -> m (VerboseKey, Doc)
prettyOW OccursWhere
o
        (VerboseKey, Doc) -> m (VerboseKey, Doc)
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseKey
s, Doc
d Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
".")
      prettyOWs (OccursWhere
o:[OccursWhere]
os) = do
        (VerboseKey
s1, Doc
d1) <- OccursWhere -> m (VerboseKey, Doc)
forall (m :: * -> *).
MonadPretty m =>
OccursWhere -> m (VerboseKey, Doc)
prettyOW  OccursWhere
o
        (VerboseKey
s2, Doc
d2) <- [OccursWhere] -> m (VerboseKey, Doc)
forall (m :: * -> *).
MonadPretty m =>
[OccursWhere] -> m (VerboseKey, Doc)
prettyOWs [OccursWhere]
os
        (VerboseKey, Doc) -> m (VerboseKey, Doc)
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseKey
s1, Doc
d1 Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (Doc
"," Doc -> Doc -> Doc
P.<+> Doc
"which" Doc -> Doc -> Doc
P.<+> VerboseKey -> Doc
P.text VerboseKey
s2 Doc -> Doc -> Doc
P.$$ Doc
d2))

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

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

      prettyW :: MonadPretty m => Where -> [m Doc]
      prettyW :: Where -> [m Doc]
prettyW Where
w = case Where
w of
        Where
LeftOfArrow  -> VerboseKey -> [m Doc]
forall (m :: * -> *). Monad m => VerboseKey -> [m Doc]
pwords VerboseKey
"to the left of an arrow"
        DefArg QName
q VerboseLevel
i   -> VerboseKey -> [m Doc]
forall (m :: * -> *). Monad m => VerboseKey -> [m Doc]
pwords VerboseKey
"in the" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> [m Doc]
forall a (m :: * -> *).
(Eq a, Num a, Monad m, Show a) =>
a -> [m Doc]
nth VerboseLevel
i [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [m Doc]
forall (m :: * -> *). Monad m => VerboseKey -> [m Doc]
pwords VerboseKey
"argument of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
                          [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q]
        Where
UnderInf     -> VerboseKey -> [m Doc]
forall (m :: * -> *). Monad m => VerboseKey -> [m Doc]
pwords VerboseKey
"under" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
                        [do -- this cannot fail if an 'UnderInf' has been generated
                            Def QName
inf Elims
_ <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseKey -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => VerboseKey -> m (Maybe Term)
getBuiltin' VerboseKey
builtinInf
                            QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
inf]
        Where
VarArg       -> VerboseKey -> [m Doc]
forall (m :: * -> *). Monad m => VerboseKey -> [m Doc]
pwords VerboseKey
"in an argument of a bound variable"
        Where
MetaArg      -> VerboseKey -> [m Doc]
forall (m :: * -> *). Monad m => VerboseKey -> [m Doc]
pwords VerboseKey
"in an argument of a metavariable"
        ConArgType QName
c -> VerboseKey -> [m Doc]
forall (m :: * -> *). Monad m => VerboseKey -> [m Doc]
pwords VerboseKey
"in the type of the constructor" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c]
        IndArgType QName
c -> VerboseKey -> [m Doc]
forall (m :: * -> *). Monad m => VerboseKey -> [m Doc]
pwords VerboseKey
"in an index of the target type of the constructor" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c]
        InClause VerboseLevel
i   -> VerboseKey -> [m Doc]
forall (m :: * -> *). Monad m => VerboseKey -> [m Doc]
pwords VerboseKey
"in the" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> [m Doc]
forall a (m :: * -> *).
(Eq a, Num a, Monad m, Show a) =>
a -> [m Doc]
nth VerboseLevel
i [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [m Doc]
forall (m :: * -> *). Monad m => VerboseKey -> [m Doc]
pwords VerboseKey
"clause"
        Where
Matched      -> VerboseKey -> [m Doc]
forall (m :: * -> *). Monad m => VerboseKey -> [m Doc]
pwords VerboseKey
"as matched against"
        Where
IsIndex      -> VerboseKey -> [m Doc]
forall (m :: * -> *). Monad m => VerboseKey -> [m Doc]
pwords VerboseKey
"as an index"
        InDefOf QName
d    -> VerboseKey -> [m Doc]
forall (m :: * -> *). Monad m => VerboseKey -> [m Doc]
pwords VerboseKey
"in the definition of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
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 ((Where -> Bool) -> Seq Where -> Seq Where
forall a. (a -> Bool) -> Seq a -> Seq a
DS.filter (Bool -> Bool
not (Bool -> Bool) -> (Where -> Bool) -> Where -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Where -> Bool
isArrow) Seq Where
cs) (Seq Where -> OccursWhere) -> Seq Where -> OccursWhere
forall a b. (a -> b) -> a -> b
$
          Seq Where
noArrows
            Seq Where -> Seq Where -> Seq Where
forall a. Seq a -> Seq a -> Seq a
DS.><
          case Seq Where -> ViewL Where
forall a. Seq a -> ViewL a
DS.viewl Seq Where
startsWithArrow of
            ViewL Where
DS.EmptyL  -> Seq Where
forall a. Seq a
DS.empty
            Where
w DS.:< Seq Where
ws -> Where
w Where -> Seq Where -> Seq Where
forall a. a -> Seq a -> Seq a
DS.<| (Where -> Bool) -> Seq Where -> Seq Where
forall a. (a -> Bool) -> Seq a -> Seq a
DS.filter (Bool -> Bool
not (Bool -> Bool) -> (Where -> Bool) -> Where -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Where -> Bool
isArrow) Seq Where
ws
        where
        (Seq Where
noArrows, Seq Where
startsWithArrow) = (Where -> Bool) -> Seq Where -> (Seq Where, Seq Where)
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