{-# LANGUAGE NondecreasingIndentation #-}

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

import Prelude hiding ( null )

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

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

import Debug.Trace

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

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

import Agda.Utils.Impossible

type Graph n e = Graph.Graph n e

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

  -- check positivity for all strongly connected components of the graph for qs
  ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.graph.sccs" Nat
10 (TCMT IO Doc -> TCM ()) -> TCMT IO 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
    [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Nat -> ArgName
forall a. Show a => a -> ArgName
show ([Node] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Node]
triv) ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" trivial sccs"
        , ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Nat -> ArgName
forall a. Show a => a -> ArgName
show ([[Node]] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [[Node]]
others) ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" non-trivial sccs with lengths " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++
            [Nat] -> ArgName
forall a. Show a => a -> ArgName
show (([Node] -> Nat) -> [[Node]] -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
map [Node] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [[Node]]
others)
        ]
  ArgName -> Nat -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> ArgName -> m ()
reportSLn ArgName
"tc.pos.graph.sccs" Nat
15 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$
    ArgName
"  sccs = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ [[Node]] -> ArgName
forall a. Pretty a => a -> ArgName
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
      ArgName -> Nat -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> ArgName -> m ()
reportSLn ArgName
"tc.pos.mutual" Nat
10 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
"setting " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ QName -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow QName
q ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" to non-recursive"
      -- Andreas, 2017-04-26, issue #2555
      -- We should not have @DefNode@s pointing outside our formal mutual block.
      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 a. a -> TCMT IO a
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
  ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.tick" Nat
100 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checked positivity"

  where
    checkPos :: Graph Node (Edge OccursWhere) ->
                Graph Node Occurrence ->
                QName -> TCM ()
    checkPos :: Graph Node (Edge OccursWhere)
-> Graph Node Occurrence -> QName -> TCM ()
checkPos Graph Node (Edge OccursWhere)
g Graph Node Occurrence
gstar QName
q = 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
        ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.check" Nat
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checking positivity of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q

        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 a b. (a -> b) -> Graph Node a -> Graph Node b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((OccursWhere -> Seq OccursWhere)
-> Edge OccursWhere -> Edge (Seq OccursWhere)
forall a b. (a -> b) -> Edge a -> Edge b
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 :: ArgName -> Occurrence -> TCMT IO Doc
how ArgName
msg Occurrence
bound = [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
                  [QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ ArgName -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"is" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
                  ArgName -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords (ArgName
msg ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
", because it occurs") [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
                  [Seq OccursWhere -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Seq OccursWhere -> 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 :: * -> *).
(HasCallStack, 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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

        -- if we find an unguarded record, mark it as such
        case DataOrRecord
dr of
          DataOrRecord
IsData -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          IsRecord PatternOrCopattern
pat -> case Maybe Occurrence
loop of
            Just Occurrence
o | Occurrence
o Occurrence -> Occurrence -> Bool
forall a. Ord a => a -> a -> Bool
<= Occurrence
StrictPos -> do
              ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.record" Nat
5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> Occurrence -> TCMT IO Doc
how ArgName
"not guarded" Occurrence
StrictPos
              QName -> PatternOrCopattern -> TCM ()
unguardedRecord QName
q PatternOrCopattern
pat
              QName -> TCM ()
checkInduction QName
q
            -- otherwise, if the record is recursive, mark it as well
            Just Occurrence
o | Occurrence
o Occurrence -> Occurrence -> Bool
forall a. Ord a => a -> a -> Bool
<= Occurrence
GuardPos -> do
              ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.record" Nat
5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> Occurrence -> TCMT IO Doc
how ArgName
"recursive" Occurrence
GuardPos
              QName -> TCM ()
recursiveRecord QName
q
              QName -> TCM ()
checkInduction QName
q
            -- If the record is not recursive, switch on eta
            -- unless it is coinductive or a no-eta-equality record.
            Maybe Occurrence
Nothing -> do
              ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.record" Nat
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
                TCMT IO Doc
"record type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                TCMT IO Doc
"is not recursive"
              QName -> TCM ()
nonRecursiveRecord QName
q
            Maybe Occurrence
_ -> () -> TCM ()
forall a. a -> TCMT IO a
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 (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m 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.
(HasCallStack, MonadTCError 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 ()) -> TCMT IO Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
              TCMT IO Doc
"Recursive record" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
              TCMT IO Doc
"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 a. a -> TCMT IO a
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, PatternOrCopattern
recPatternMatching :: PatternOrCopattern
recPatternMatching :: Defn -> PatternOrCopattern
recPatternMatching } -> DataOrRecord -> Maybe DataOrRecord
forall a. a -> Maybe a
Just (DataOrRecord -> Maybe DataOrRecord)
-> DataOrRecord -> Maybe DataOrRecord
forall a b. (a -> b) -> a -> b
$ PatternOrCopattern -> DataOrRecord
IsRecord PatternOrCopattern
recPatternMatching
        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 a. a -> TCMT IO a
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
      ArgName -> Nat -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> ArgName -> m ()
reportSLn ArgName
"tc.pos.mutual" Nat
10 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
"setting " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ QName -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow QName
q ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" to (mutually) recursive"
      QName -> [QName] -> TCM ()
setMutual QName
q [QName]
qs
      -- TODO: The previous line produces data of quadratic size
      -- (which has to be processed upon serialization).  Presumably qs is
      -- usually short, but in some cases (for instance for generated
      -- code) it may be long. Wouldn't it be better to assign a
      -- unique identifier to each SCC, and avoid storing lists?

    -- Set the polarity of the arguments to a couple of definitions
    setArgOccs :: Set QName -> [QName] -> Graph Node Occurrence -> TCM ()
    setArgOccs :: Set QName -> [QName] -> Graph Node Occurrence -> TCM ()
setArgOccs Set QName
qset [QName]
qs Graph Node Occurrence
g = do
      -- Andreas, 2018-05-11, issue #3049: we need to be pessimistic about
      -- argument polarity beyond the formal arity of the function.
      --
      -- -- Compute a map from each name in q to the maximal argument index
      -- let maxs = Map.fromListWith max
      --      [ (q, i) | ArgNode q i <- Set.toList $ Graph.nodes g, q `Set.member` qset ]
      [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
        ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.args" Nat
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checking args of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q
        Nat
n <- Definition -> TCM Nat
getDefArity Definition
def
        -- If there is no outgoing edge @ArgNode q i@, all @n@ arguments are @Unused@.
        -- Otherwise, we obtain the occurrences from the Graph.
        let findOcc :: Nat -> Occurrence
findOcc Nat
i = 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 -> Nat -> Node
ArgNode QName
q Nat
i) (QName -> Node
DefNode QName
q) Graph Node Occurrence
g
            args :: [Occurrence]
args = -- caseMaybe (Map.lookup q maxs) (replicate n Unused) $ \ m ->
              (Nat -> Occurrence) -> [Nat] -> [Occurrence]
forall a b. (a -> b) -> [a] -> [b]
map Nat -> Occurrence
findOcc [Nat
0 .. Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1]  -- [0 .. max m (n - 1)] -- triggers issue #3049
        ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.args" Nat
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"args of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"="
          , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Occurrence -> TCMT IO Doc) -> [Occurrence] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Occurrence -> 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 ()
forall (m :: * -> *).
MonadTCState m =>
QName -> [Occurrence] -> m ()
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
        PrimitiveSort{}    -> Bool
False
        Constructor{}      -> Bool
False
        Function{}         -> Bool
True
        Datatype{}         -> Bool
True
        Record{}           -> Bool
True

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

-- 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
$c== :: Item -> Item -> Bool
== :: Item -> Item -> Bool
$c/= :: Item -> Item -> Bool
/= :: 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
$ccompare :: Item -> Item -> Ordering
compare :: Item -> Item -> Ordering
$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
>= :: Item -> Item -> Bool
$cmax :: Item -> Item -> Item
max :: Item -> Item -> Item
$cmin :: Item -> Item -> Item
min :: Item -> Item -> Item
Ord, Nat -> Item -> ArgName -> ArgName
[Item] -> ArgName -> ArgName
Item -> ArgName
(Nat -> Item -> ArgName -> ArgName)
-> (Item -> ArgName) -> ([Item] -> ArgName -> ArgName) -> Show Item
forall a.
(Nat -> a -> ArgName -> ArgName)
-> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
$cshowsPrec :: Nat -> Item -> ArgName -> ArgName
showsPrec :: Nat -> Item -> ArgName -> ArgName
$cshow :: Item -> ArgName
show :: Item -> ArgName
$cshowList :: [Item] -> ArgName -> ArgName
showList :: [Item] -> ArgName -> ArgName
Show)

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

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

type Occurrences = Map Item [OccursWhere]

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

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

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

-- | The monoid laws only hold up to flattening of 'Concat'.
instance Monoid OccurrencesBuilder where
  mempty :: OccurrencesBuilder
mempty  = [OccurrencesBuilder] -> OccurrencesBuilder
Concat []
  mappend :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder
mappend = 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 Nat -> OccurrencesBuilder -> Maybe OccurrencesBuilder'
pp Maybe Nat
forall a. Maybe a
Nothing OccurrencesBuilder
ob of
  Maybe OccurrencesBuilder'
Nothing -> [OccurrencesBuilder'] -> OccurrencesBuilder'
Concat' []
  Just OccurrencesBuilder'
ob -> OccurrencesBuilder'
ob
  where
  pp :: Maybe Nat  -- Variables larger than or equal to this number, if any,
                   -- are not retained.
     -> OccurrencesBuilder
     -> Maybe OccurrencesBuilder'
  pp :: Maybe Nat -> OccurrencesBuilder -> Maybe OccurrencesBuilder'
pp !Maybe Nat
m = \case
    Concat [OccurrencesBuilder]
obs -> case (OccurrencesBuilder -> Maybe OccurrencesBuilder')
-> [OccurrencesBuilder] -> [OccurrencesBuilder']
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Maybe Nat -> OccurrencesBuilder -> Maybe OccurrencesBuilder'
pp Maybe Nat
m) [OccurrencesBuilder]
obs of
      []  -> Maybe OccurrencesBuilder'
forall a. Maybe a
Nothing
      [OccurrencesBuilder']
obs -> OccurrencesBuilder' -> Maybe OccurrencesBuilder'
forall a. a -> Maybe a
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 Nat -> OccurrencesBuilder -> Maybe OccurrencesBuilder'
pp Maybe Nat
m OccurrencesBuilder
ob

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

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

-- | An interpreter for 'OccurrencesBuilder'.
--
-- WARNING: There can be lots of sharing between the generated
-- 'OccursWhere' entries. Traversing all of these entries could be
-- expensive. (See 'computeEdges' for an example.)
flatten :: OccurrencesBuilder -> Map Item Integer
flatten :: OccurrencesBuilder -> Map Item Integer
flatten =
  (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 a b. (a -> b -> b) -> b -> [a] -> b
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, Monoid a) => Monoid (OccM a) where
  mempty :: OccM a
mempty  = a -> OccM a
forall a. a -> ReaderT OccEnv Identity 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)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence

withExtendedOccEnv :: Maybe Item -> OccM a -> OccM a
withExtendedOccEnv :: forall a. 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' :: forall a. [Maybe Item] -> OccM a -> OccM a
withExtendedOccEnv' [Maybe Item]
is = (OccEnv -> OccEnv)
-> ReaderT OccEnv Identity a -> ReaderT OccEnv Identity a
forall a.
(OccEnv -> OccEnv)
-> ReaderT OccEnv Identity a -> ReaderT OccEnv Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((OccEnv -> OccEnv)
 -> ReaderT OccEnv Identity a -> ReaderT OccEnv Identity a)
-> (OccEnv -> OccEnv)
-> ReaderT OccEnv Identity a
-> ReaderT OccEnv Identity 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 :: forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCMT IO OccurrencesBuilder
getOccurrences [Maybe Item]
vars a
a = do
  ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.occ" Nat
70 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"computing occurrences in " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (a -> ArgName
forall a. Show a => a -> ArgName
show a
a)
  ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.occ" Nat
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"computing occurrences in " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
a
  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)
-> (Maybe CoinductionKit -> OccEnv)
-> Maybe CoinductionKit
-> OccurrencesBuilder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe Item] -> Maybe QName -> OccEnv
OccEnv [Maybe Item]
vars (Maybe QName -> OccEnv)
-> (Maybe CoinductionKit -> Maybe QName)
-> Maybe CoinductionKit
-> OccEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CoinductionKit -> QName
nameOfInf (Maybe CoinductionKit -> OccurrencesBuilder)
-> TCMT IO (Maybe CoinductionKit) -> TCMT IO OccurrencesBuilder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Maybe CoinductionKit)
coinductionKit

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 m a. Monoid m => (a -> m) -> t a -> m
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
    -- TODO #3733: handle hcomp/transp clauses properly
    if NAPs -> Bool
hasDefP NAPs
ps then OccurrencesBuilder -> Reader OccEnv OccurrencesBuilder
forall a. a -> ReaderT OccEnv Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return OccurrencesBuilder
forall a. Monoid a => a
mempty else do
    ([OccurrencesBuilder] -> OccurrencesBuilder
Concat (((Nat, Arg (Named NamedName DeBruijnPattern))
 -> Maybe OccurrencesBuilder)
-> [(Nat, Arg (Named NamedName DeBruijnPattern))]
-> [OccurrencesBuilder]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Nat, Arg (Named NamedName DeBruijnPattern))
-> Maybe OccurrencesBuilder
forall {name} {a}.
(Nat, Arg (Named name (Pattern' a))) -> Maybe OccurrencesBuilder
matching ([Nat] -> NAPs -> [(Nat, Arg (Named NamedName DeBruijnPattern))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Nat
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 :: (Nat, Arg (Named name (Pattern' a))) -> Maybe OccurrencesBuilder
matching (Nat
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
$ Nat -> Item
AnArg Nat
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
$ (Nat
 -> Arg (Named NamedName DeBruijnPattern) -> IntMap (Maybe Item))
-> [Nat] -> NAPs -> [IntMap (Maybe Item)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Nat -> Arg (Named NamedName DeBruijnPattern) -> IntMap (Maybe Item)
patItem [Nat
0..] NAPs
ps

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

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

instance ComputeOccurrences Term where
  occurrences :: Term -> Reader OccEnv OccurrencesBuilder
occurrences Term
v = case Term -> Term
unSpine Term
v of
    Var Nat
i Elims
args -> ((OccEnv -> OccurrencesBuilder) -> Reader OccEnv OccurrencesBuilder
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ([Maybe Item] -> OccurrencesBuilder
occI ([Maybe Item] -> OccurrencesBuilder)
-> (OccEnv -> [Maybe Item]) -> OccEnv -> OccurrencesBuilder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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] -> Nat -> Maybe Item
forall a. a -> [a] -> Nat -> a
indexWithDefault Maybe Item
unbound [Maybe Item]
vars Nat
i
      unbound :: Maybe Item
unbound = (ArgName -> Maybe Item -> Maybe Item)
-> Maybe Item -> ArgName -> Maybe Item
forall a b c. (a -> b -> c) -> b -> a -> c
flip ArgName -> Maybe Item -> Maybe Item
forall a. ArgName -> a -> a
trace Maybe Item
forall a. HasCallStack => a
__IMPOSSIBLE__ (ArgName -> Maybe Item) -> ArgName -> Maybe Item
forall a b. (a -> b) -> a -> b
$
              ArgName
"impossible: occurrence of de Bruijn index " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ Nat -> ArgName
forall a. Show a => a -> ArgName
show Nat
i ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++
              ArgName
" in vars " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ (OccEnv -> [Maybe Item]) -> ArgName
forall a. Show a => a -> ArgName
show OccEnv -> [Maybe Item]
vars ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" 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 :: Nat -> 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)
-> (Nat -> Where)
-> Nat
-> OccurrencesBuilder
-> OccurrencesBuilder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Nat -> Where
DefArg QName
d else \ Nat
n ->
            -- the principal argument of builtin INF (∞) is the second (n==1)
            -- the first is a level argument (n==0, counting from 0!)
            if Nat
n Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
1 then Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs Where
UnderInf else Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs (QName -> Nat -> Where
DefArg QName
d Nat
n)
      [OccurrencesBuilder]
occs <- (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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim -> Reader OccEnv OccurrencesBuilder
forall a.
ComputeOccurrences a =>
a -> Reader OccEnv OccurrencesBuilder
occurrences Elims
args
      OccurrencesBuilder -> Reader OccEnv OccurrencesBuilder
forall a. a -> ReaderT OccEnv Identity a
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]
: (Nat -> OccurrencesBuilder -> OccurrencesBuilder)
-> [Nat] -> [OccurrencesBuilder] -> [OccurrencesBuilder]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Nat -> OccurrencesBuilder -> OccurrencesBuilder
occsAs [Nat
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
_ Term
l) = Term -> Reader OccEnv OccurrencesBuilder
forall a.
ComputeOccurrences a =>
a -> Reader OccEnv OccurrencesBuilder
occurrences Term
l

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   ArgName
_ 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 ArgName
_ 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)
-> TCMT IO OccurrencesBuilder -> TCM (Map Item Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO OccurrencesBuilder
computeOccurrences' QName
q

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

    Datatype{dataClause :: Defn -> Maybe Clause
dataClause = Just Clause
c} -> [Maybe Item] -> Clause -> TCMT IO OccurrencesBuilder
forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCMT IO OccurrencesBuilder
getOccurrences [] (Clause -> TCMT IO OccurrencesBuilder)
-> TCMT IO Clause -> TCMT IO 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 -> Nat
dataPars = Nat
np0, dataCons :: Defn -> [QName]
dataCons = [QName]
cs}       -> do
      -- Andreas, 2013-02-27 (later edited by someone else): First,
      -- include each index of an inductive family.
      TelV Tele (Dom Type)
tel Type
_ <- 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
      Nat
sizeIndex <- [Dom (ArgName, Type)]
-> TCM Nat
-> (Dom (ArgName, Type) -> [Dom (ArgName, Type)] -> TCM Nat)
-> TCM Nat
forall a b. [a] -> b -> (a -> [a] -> b) -> b
caseList (Nat -> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
forall a. Nat -> [a] -> [a]
drop Nat
np0 ([Dom (ArgName, Type)] -> [Dom (ArgName, Type)])
-> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
tel) (Nat -> TCM Nat
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Nat
0) ((Dom (ArgName, Type) -> [Dom (ArgName, Type)] -> TCM Nat)
 -> TCM Nat)
-> (Dom (ArgName, Type) -> [Dom (ArgName, Type)] -> TCM Nat)
-> TCM Nat
forall a b. (a -> b) -> a -> b
$ \ Dom (ArgName, Type)
dom [Dom (ArgName, Type)]
_ -> do
        TCMT IO (Maybe BoundedSize)
-> TCM Nat -> (BoundedSize -> TCM Nat) -> TCM Nat
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Dom (ArgName, Type) -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Dom (ArgName, Type) -> m (Maybe BoundedSize)
isSizeType Dom (ArgName, Type)
dom) (Nat -> TCM Nat
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Nat
0) ((BoundedSize -> TCM Nat) -> TCM Nat)
-> (BoundedSize -> TCM Nat) -> TCM Nat
forall a b. (a -> b) -> a -> b
$ \ BoundedSize
_ -> Nat -> TCM Nat
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Nat
1
      let np :: Nat
np = Nat
np0 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
sizeIndex
      let xs :: [Nat]
xs = [Nat
np .. Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1] -- argument positions corresponding to indices
      let ioccs :: OccurrencesBuilder
ioccs = [OccurrencesBuilder] -> OccurrencesBuilder
Concat ([OccurrencesBuilder] -> OccurrencesBuilder)
-> [OccurrencesBuilder] -> OccurrencesBuilder
forall a b. (a -> b) -> a -> b
$ (Nat -> OccurrencesBuilder) -> [Nat] -> [OccurrencesBuilder]
forall a b. (a -> b) -> [a] -> [b]
map (Item -> OccurrencesBuilder
OccursHere (Item -> OccurrencesBuilder)
-> (Nat -> Item) -> Nat -> OccurrencesBuilder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Item
AnArg) [Nat
np0 .. Nat
np Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1]
                        [OccurrencesBuilder]
-> [OccurrencesBuilder] -> [OccurrencesBuilder]
forall a. [a] -> [a] -> [a]
++ (Nat -> OccurrencesBuilder) -> [Nat] -> [OccurrencesBuilder]
forall a b. (a -> b) -> [a] -> [b]
map (Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs Where
IsIndex (OccurrencesBuilder -> OccurrencesBuilder)
-> (Nat -> OccurrencesBuilder) -> Nat -> OccurrencesBuilder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Item -> OccurrencesBuilder
OccursHere (Item -> OccurrencesBuilder)
-> (Nat -> Item) -> Nat -> OccurrencesBuilder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Item
AnArg) [Nat]
xs
      -- Then, we compute the occurrences in the constructor types.
      let conOcc :: QName -> TCMT IO OccurrencesBuilder
conOcc QName
c = do
            -- Andreas, 2020-02-15, issue #4447:
            -- Allow UnconfimedReductions here to make sure we get the constructor type
            -- in same way as it was obtained when the data types was checked.
            TelV Tele (Dom Type)
tel Type
t <- 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)
forall (m :: * -> *). PureTCM m => Type -> m (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
            let (Tele (Dom Type)
tel0,Tele (Dom Type)
tel1) = Nat -> Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type))
splitTelescopeAt Nat
np Tele (Dom Type)
tel
            -- Do not collect occurrences in the data parameters.
            -- Normalization needed e.g. for test/succeed/Bush.agda.
            -- (Actually, for Bush.agda, reducing the parameters should be sufficient.)
            Tele (Dom Type)
tel1' <- Tele (Dom Type)
-> TCMT IO (Tele (Dom Type)) -> TCMT IO (Tele (Dom Type))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
tel0 (TCMT IO (Tele (Dom Type)) -> TCMT IO (Tele (Dom Type)))
-> TCMT IO (Tele (Dom Type)) -> TCMT IO (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ 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
$ Tele (Dom Type)
tel1
            let vars :: Nat -> [Maybe Item]
vars = (Nat -> Maybe Item) -> [Nat] -> [Maybe Item]
forall a b. (a -> b) -> [a] -> [b]
map (Item -> Maybe Item
forall a. a -> Maybe a
Just (Item -> Maybe Item) -> (Nat -> Item) -> Nat -> Maybe Item
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Item
AnArg) ([Nat] -> [Maybe Item]) -> (Nat -> [Nat]) -> Nat -> [Maybe Item]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom
            -- Occurrences in the types of the constructor arguments.
            TCMT IO OccurrencesBuilder
-> TCMT IO OccurrencesBuilder -> TCMT IO OccurrencesBuilder
forall a. Monoid a => a -> a -> a
mappend (Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs (QName -> Where
ConArgType QName
c) (OccurrencesBuilder -> OccurrencesBuilder)
-> TCMT IO OccurrencesBuilder -> TCMT IO OccurrencesBuilder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe Item] -> Tele (Dom Type) -> TCMT IO OccurrencesBuilder
forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCMT IO OccurrencesBuilder
getOccurrences (Nat -> [Maybe Item]
vars Nat
np) Tele (Dom Type)
tel1') (TCMT IO OccurrencesBuilder -> TCMT IO OccurrencesBuilder)
-> TCMT IO OccurrencesBuilder -> TCMT IO 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 :: TCMT IO OccurrencesBuilder
fallback = Where -> OccurrencesBuilder -> OccurrencesBuilder
OccursAs Where
LeftOfArrow (OccurrencesBuilder -> OccurrencesBuilder)
-> TCMT IO OccurrencesBuilder -> TCMT IO OccurrencesBuilder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe Item] -> Type -> TCMT IO OccurrencesBuilder
forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCMT IO OccurrencesBuilder
getOccurrences (Nat -> [Maybe Item]
vars (Nat -> [Maybe Item]) -> Nat -> [Maybe Item]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel) Type
t -- NB::Defined but not used
              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
$ Nat -> Elims -> Elims
forall a. Nat -> [a] -> [a]
drop Nat
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
. Nat -> OccurrencesBuilder -> OccurrencesBuilder
OnlyVarsUpTo Nat
np (OccurrencesBuilder -> OccurrencesBuilder)
-> TCMT IO OccurrencesBuilder -> TCMT IO OccurrencesBuilder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe Item] -> [Arg Term] -> TCMT IO OccurrencesBuilder
forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCMT IO OccurrencesBuilder
getOccurrences (Nat -> [Maybe Item]
vars (Nat -> [Maybe Item]) -> Nat -> [Maybe Item]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel) [Arg Term]
indices
                  | Bool
otherwise -> TCMT IO OccurrencesBuilder
forall a. HasCallStack => a
__IMPOSSIBLE__  -- fallback -- this ought to be impossible now (but wasn't, see #4447)
                Pi{}       -> TCMT IO OccurrencesBuilder
forall a. HasCallStack => a
__IMPOSSIBLE__  -- eliminated  by telView
                MetaV{}    -> TCMT IO OccurrencesBuilder
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a constructor target; should have been solved by now
                Var{}      -> TCMT IO OccurrencesBuilder
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a constructor target
                Sort{}     -> TCMT IO OccurrencesBuilder
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a constructor target
                Lam{}      -> TCMT IO OccurrencesBuilder
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
                Lit{}      -> TCMT IO OccurrencesBuilder
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
                Con{}      -> TCMT IO OccurrencesBuilder
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
                Level{}    -> TCMT IO OccurrencesBuilder
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
                DontCare{} -> TCMT IO OccurrencesBuilder
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not a type
                Dummy{}    -> TCMT IO OccurrencesBuilder
forall a. HasCallStack => a
__IMPOSSIBLE__
      [TCMT IO OccurrencesBuilder] -> TCMT IO OccurrencesBuilder
forall a. Monoid a => [a] -> a
mconcat ([TCMT IO OccurrencesBuilder] -> TCMT IO OccurrencesBuilder)
-> [TCMT IO OccurrencesBuilder] -> TCMT IO OccurrencesBuilder
forall a b. (a -> b) -> a -> b
$ OccurrencesBuilder -> TCMT IO OccurrencesBuilder
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OccurrencesBuilder
ioccs TCMT IO OccurrencesBuilder
-> [TCMT IO OccurrencesBuilder] -> [TCMT IO OccurrencesBuilder]
forall a. a -> [a] -> [a]
: (QName -> TCMT IO OccurrencesBuilder)
-> [QName] -> [TCMT IO OccurrencesBuilder]
forall a b. (a -> b) -> [a] -> [b]
map QName -> TCMT IO OccurrencesBuilder
conOcc [QName]
cs

    Record{recClause :: Defn -> Maybe Clause
recClause = Just Clause
c} -> [Maybe Item] -> Clause -> TCMT IO OccurrencesBuilder
forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCMT IO OccurrencesBuilder
getOccurrences [] (Clause -> TCMT IO OccurrencesBuilder)
-> TCMT IO Clause -> TCMT IO 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 -> Nat
recPars = Nat
np, recTel :: Defn -> Tele (Dom Type)
recTel = Tele (Dom Type)
tel} -> do
      let (Tele (Dom Type)
tel0,Tele (Dom Type)
tel1) = Nat -> Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type))
splitTelescopeAt Nat
np Tele (Dom Type)
tel
          vars :: [Maybe Item]
vars = (Nat -> Maybe Item) -> [Nat] -> [Maybe Item]
forall a b. (a -> b) -> [a] -> [b]
map (Item -> Maybe Item
forall a. a -> Maybe a
Just (Item -> Maybe Item) -> (Nat -> Item) -> Nat -> Maybe Item
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Item
AnArg) ([Nat] -> [Maybe Item]) -> [Nat] -> [Maybe Item]
forall a b. (a -> b) -> a -> b
$ Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom Nat
np
      [Maybe Item] -> Tele (Dom Type) -> TCMT IO OccurrencesBuilder
forall a.
(Show a, PrettyTCM a, ComputeOccurrences a) =>
[Maybe Item] -> a -> TCMT IO OccurrencesBuilder
getOccurrences [Maybe Item]
vars (Tele (Dom Type) -> TCMT IO OccurrencesBuilder)
-> TCMT IO (Tele (Dom Type)) -> TCMT IO OccurrencesBuilder
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Tele (Dom Type)
-> TCMT IO (Tele (Dom Type)) -> TCMT IO (Tele (Dom Type))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
tel0 (Tele (Dom Type) -> TCMT IO (Tele (Dom Type))
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Tele (Dom Type)
tel1) -- Andreas, 2017-01-01, issue #1899, treat like data types

    -- Arguments to other kinds of definitions are hard-wired.
    Constructor{}      -> TCMT IO OccurrencesBuilder
forall a. Monoid a => a
mempty
    Axiom{}            -> TCMT IO OccurrencesBuilder
forall a. Monoid a => a
mempty
    DataOrRecSig{}     -> TCMT IO OccurrencesBuilder
forall a. Monoid a => a
mempty
    Primitive{}        -> TCMT IO OccurrencesBuilder
forall a. Monoid a => a
mempty
    PrimitiveSort{}    -> TCMT IO OccurrencesBuilder
forall a. Monoid a => a
mempty
    GeneralizableVar{} -> TCMT IO OccurrencesBuilder
forall a. Monoid a => a
mempty
    AbstractDefn{}     -> TCMT IO 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
$c== :: Node -> Node -> Bool
== :: Node -> Node -> Bool
$c/= :: Node -> Node -> Bool
/= :: 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
$ccompare :: Node -> Node -> Ordering
compare :: Node -> Node -> Ordering
$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
>= :: Node -> Node -> Bool
$cmax :: Node -> Node -> Node
max :: Node -> Node -> Node
$cmin :: Node -> Node -> Node
min :: Node -> Node -> 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
$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
/= :: 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
$ccompare :: forall a. Ord a => Edge a -> Edge a -> Ordering
compare :: Edge a -> Edge a -> Ordering
$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
>= :: Edge a -> Edge a -> Bool
$cmax :: forall a. Ord a => Edge a -> Edge a -> Edge a
max :: Edge a -> Edge a -> Edge a
$cmin :: forall a. Ord a => Edge a -> Edge a -> Edge a
min :: Edge a -> Edge a -> Edge a
Ord, Nat -> Edge a -> ArgName -> ArgName
[Edge a] -> ArgName -> ArgName
Edge a -> ArgName
(Nat -> Edge a -> ArgName -> ArgName)
-> (Edge a -> ArgName)
-> ([Edge a] -> ArgName -> ArgName)
-> Show (Edge a)
forall a. Show a => Nat -> Edge a -> ArgName -> ArgName
forall a. Show a => [Edge a] -> ArgName -> ArgName
forall a. Show a => Edge a -> ArgName
forall a.
(Nat -> a -> ArgName -> ArgName)
-> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
$cshowsPrec :: forall a. Show a => Nat -> Edge a -> ArgName -> ArgName
showsPrec :: Nat -> Edge a -> ArgName -> ArgName
$cshow :: forall a. Show a => Edge a -> ArgName
show :: Edge a -> ArgName
$cshowList :: forall a. Show a => [Edge a] -> ArgName -> ArgName
showList :: [Edge a] -> ArgName -> ArgName
Show, (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
$cfmap :: forall a b. (a -> b) -> Edge a -> Edge b
fmap :: forall a b. (a -> b) -> Edge a -> Edge b
$c<$ :: forall a b. a -> Edge b -> Edge a
<$ :: forall a b. a -> Edge b -> Edge a
Functor)

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

mergeEdges :: Edge a -> Edge a -> Edge a
mergeEdges :: forall a. Edge a -> Edge a -> Edge a
mergeEdges Edge a
_                    e :: Edge a
e@(Edge Occurrence
Mixed a
_)     = Edge a
e -- dominant
mergeEdges e :: Edge a
e@(Edge Occurrence
Mixed a
_)     Edge a
_                    = Edge a
e
mergeEdges (Edge Occurrence
Unused a
_)      Edge a
e                    = Edge a
e -- neutral
mergeEdges Edge a
e                    (Edge Occurrence
Unused a
_)      = Edge a
e
mergeEdges (Edge Occurrence
JustNeg a
_)     e :: Edge a
e@(Edge Occurrence
JustNeg a
_)   = Edge a
e
mergeEdges Edge a
_                    e :: Edge a
e@(Edge Occurrence
JustNeg a
w)   = 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 -> TCMT IO OccurrencesBuilder
computeOccurrences' QName
q

      ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.occs" Nat
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        ((TCMT IO Doc
"Occurrences in" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
":")
          TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$+$
        Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
           ((Item, Integer) -> TCMT IO Doc)
-> [(Item, Integer)] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\(Item
i, Integer
n) ->
                   (Item -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Item
i TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
":") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (Integer -> ArgName
forall a. Show a => a -> ArgName
show Integer
n) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                   TCMT IO Doc
"occurrences") ([(Item, Integer)] -> [TCMT IO Doc])
-> [(Item, Integer)] -> [TCMT IO 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

      ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.pos.occs.edges" Nat
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"Edges:"
          TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$+$
        Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
           (Edge Node (Edge OccursWhere) -> TCMT IO Doc)
-> [Edge Node (Edge OccursWhere)] -> [TCMT IO 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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Node -> m Doc
prettyTCM (Edge Node (Edge OccursWhere) -> Node
forall n e. Edge n e -> n
Graph.source Edge Node (Edge OccursWhere)
e) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                   TCMT IO Doc
"-[" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Occurrence -> Doc
forall a. Pretty a => a -> Doc
P.pretty Occurrence
o) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
",") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                                 Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (OccursWhere -> Doc
forall a. Pretty a => a -> Doc
P.pretty OccursWhere
w) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"]->" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                   Node -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Node -> 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 a. a -> TCMT IO a
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 a b. (a -> b -> b) -> b -> [a] -> b
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 a. a -> TCMT IO a
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 a. HasRange a => a -> Range
getRange Item
i) Seq Where
cs Seq Where
os in
      case Item
i of
        AnArg Nat
i ->
          ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
-> TCMT
     IO
     ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
forall a. a -> TCMT IO a
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) (Graph.Edge
            { source :: Node
Graph.source = QName -> Nat -> Node
ArgNode QName
q Nat
i
            , target :: Node
Graph.target = Node
to
            , label :: Edge OccursWhere
Graph.label  = 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 a. a -> TCMT IO a
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)
            (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 = \case
    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 Nat
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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Node -> Maybe Node
forall a. a -> Maybe a
Just (QName -> Nat -> Node
ArgNode QName
d Nat
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 -> Nat -> TCMT IO Occurrence
getArgOccurrence QName
d Nat
i
    Where
UnderInf       -> Occurrence -> TCM (Maybe Node, Occurrence)
addPol Occurrence
GuardPos -- Andreas, 2012-06-09: ∞ is guarding
    ConArgType QName
_   -> TCM (Maybe Node, Occurrence)
keepGoing
    IndArgType QName
_   -> TCM (Maybe Node, Occurrence)
forall {a}. TCMT IO (Maybe a, Occurrence)
mixed
    InClause Nat
_     -> 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 a. a -> TCMT IO a
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 a. a -> TCMT IO a
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 a. a -> TCMT IO a
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 a. a -> TCMT IO a
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 a. a -> TCMT IO a
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 a. a -> TCMT IO a
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 Nat
i -> QName -> Doc
forall a. Pretty a => a -> Doc
P.pretty QName
q Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> ArgName -> Doc
P.text (ArgName
"." ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ Nat -> ArgName
forall a. Show a => a -> ArgName
show Nat
i)

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

instance PrettyTCM (Seq OccursWhere) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Seq OccursWhere -> m Doc
prettyTCM =
    ((ArgName, Doc) -> Doc) -> m (ArgName, Doc) -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName, Doc) -> Doc
forall a b. (a, b) -> b
snd (m (ArgName, Doc) -> m Doc)
-> (Seq OccursWhere -> m (ArgName, Doc))
-> Seq OccursWhere
-> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OccursWhere] -> m (ArgName, Doc)
forall (m :: * -> *).
MonadPretty m =>
[OccursWhere] -> m (ArgName, Doc)
prettyOWs ([OccursWhere] -> m (ArgName, Doc))
-> (Seq OccursWhere -> [OccursWhere])
-> Seq OccursWhere
-> m (ArgName, 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 a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList
    where
      nth :: a -> [m Doc]
nth a
0 = ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"first"
      nth a
1 = ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"second"
      nth a
2 = ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"third"
      nth a
n = ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords (ArgName -> [m Doc]) -> ArgName -> [m Doc]
forall a b. (a -> b) -> a -> b
$ a -> ArgName
forall a. Show a => a -> ArgName
show (a
n a -> a -> a
forall a. Num a => a -> a -> a
+ a
1) ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
"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. HasCallStack => [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 :: forall (m :: * -> *).
MonadPretty m =>
[OccursWhere] -> m (ArgName, Doc)
prettyOWs []  = m (ArgName, Doc)
forall a. HasCallStack => a
__IMPOSSIBLE__
      prettyOWs [OccursWhere
o] = do
        (ArgName
s, Doc
d) <- OccursWhere -> m (ArgName, Doc)
forall (m :: * -> *).
MonadPretty m =>
OccursWhere -> m (ArgName, Doc)
prettyOW OccursWhere
o
        (ArgName, Doc) -> m (ArgName, Doc)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgName
s, Doc
d Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
".")
      prettyOWs (OccursWhere
o:[OccursWhere]
os) = do
        (ArgName
s1, Doc
d1) <- OccursWhere -> m (ArgName, Doc)
forall (m :: * -> *).
MonadPretty m =>
OccursWhere -> m (ArgName, Doc)
prettyOW  OccursWhere
o
        (ArgName
s2, Doc
d2) <- [OccursWhere] -> m (ArgName, Doc)
forall (m :: * -> *).
MonadPretty m =>
[OccursWhere] -> m (ArgName, Doc)
prettyOWs [OccursWhere]
os
        (ArgName, Doc) -> m (ArgName, Doc)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgName
s1, Doc
d1 Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (Doc
"," Doc -> Doc -> Doc
P.<+> Doc
"which" Doc -> Doc -> Doc
P.<+> ArgName -> Doc
P.text ArgName
s2 Doc -> Doc -> Doc
P.$$ Doc
d2))

      prettyOW :: MonadPretty m => OccursWhere -> m (String, Doc)
      prettyOW :: forall (m :: * -> *).
MonadPretty m =>
OccursWhere -> m (ArgName, Doc)
prettyOW (OccursWhere Range
_ Seq Where
cs Seq Where
ws)
        | Seq Where -> Bool
forall a. Null a => a -> Bool
null Seq Where
cs   = Seq Where -> m (ArgName, Doc)
forall (m :: * -> *).
MonadPretty m =>
Seq Where -> m (ArgName, Doc)
prettyWs Seq Where
ws
        | Bool
otherwise = do
            (ArgName
s, Doc
d1) <- Seq Where -> m (ArgName, Doc)
forall (m :: * -> *).
MonadPretty m =>
Seq Where -> m (ArgName, Doc)
prettyWs Seq Where
ws
            (ArgName
_, Doc
d2) <- Seq Where -> m (ArgName, Doc)
forall (m :: * -> *).
MonadPretty m =>
Seq Where -> m (ArgName, Doc)
prettyWs Seq Where
cs
            (ArgName, Doc) -> m (ArgName, Doc)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgName
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 :: forall (m :: * -> *).
MonadPretty m =>
Seq Where -> m (ArgName, Doc)
prettyWs Seq Where
ws = case Seq Where -> [Where]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Seq Where
ws of
        [InDefOf QName
d, Where
IsIndex] ->
          (,) ArgName
"is" (Doc -> (ArgName, Doc)) -> m Doc -> m (ArgName, Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d])
        [Where]
_ ->
          (,) ArgName
"occurs" (Doc -> (ArgName, Doc)) -> m Doc -> m (ArgName, 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 a. a -> m a
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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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 :: forall (m :: * -> *). MonadPretty m => Where -> [m Doc]
prettyW = \case
        Where
LeftOfArrow  -> ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"to the left of an arrow"
        DefArg QName
q Nat
i   -> ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"in the" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ Nat -> [m Doc]
forall {a} {m :: * -> *}.
(Eq a, Num a, Applicative m, Show a) =>
a -> [m Doc]
nth Nat
i [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q]
        Where
UnderInf     -> ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"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
<$> ArgName -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
getBuiltin' ArgName
builtinInf
                            QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
inf]
        Where
VarArg       -> ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"in an argument of a bound variable"
        Where
MetaArg      -> ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"in an argument of a metavariable"
        ConArgType QName
c -> ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c]
        IndArgType QName
c -> ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c]
        InClause Nat
i   -> ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"in the" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ Nat -> [m Doc]
forall {a} {m :: * -> *}.
(Eq a, Num a, Applicative m, Show a) =>
a -> [m Doc]
nth Nat
i [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"clause"
        Where
Matched      -> ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"as matched against"
        Where
IsIndex      -> ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"as an index"
        InDefOf QName
d    -> ArgName -> [m Doc]
forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
pwords ArgName
"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
forall (m :: * -> *). MonadPretty m => QName -> 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