{-# LANGUAGE NondecreasingIndentation #-}

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

import Prelude hiding ( null, (!!) )

import Control.DeepSeq
import Data.Either
import Data.Foldable (toList)
import Data.Foldable qualified as Fold
import Data.Function (on)
import Data.Graph (SCC(..))
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Sequence (Seq)
import Data.Sequence qualified as DS
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Strict.These

import Agda.Syntax.Common
import Agda.Syntax.Info qualified as Info
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Benchmark (MonadBench, Phase)
import Agda.TypeChecking.Monad.Benchmark qualified as Bench
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Positivity.OccurrenceAnalysis
import Agda.TypeChecking.Positivity.Warnings qualified as W
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Warnings

import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Syntax.Common.Pretty qualified as P
import Agda.Utils.Functor
import Agda.Utils.Graph.AdjacencyMap.Unidirectional qualified as Graph
import Agda.Utils.List
import Agda.Utils.List1 qualified as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Size

import Agda.Utils.Impossible

----------------------------------------------------------------------------------------------------

-- | Check that the datatypes in the mutual block containing the given
--   declarations are strictly positive.
--
--   Find polarity of datatypes parameters and indices.
--
--   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 = Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Positivity] do

  let qs :: [QName]
qs = Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
qset
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.pos.tick" Int
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

  -- Collect relevant information about the block.
  [QName]
-> TCM
     (Maybe [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)])
preprocessBlock [QName]
qs TCM
  (Maybe [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)])
-> (Maybe
      [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]
    -> TCM ())
-> TCM ()
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]
Nothing -> do
      () -> TCM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- skip the whole thing if there's nothing to check
    Just [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]
blockInfo -> do

      -- compute the occurrence graph
      --------------------------------------------------------------------------------
      (g, mutuals) <- [QName] -> TCM (OccGraph, Mutuals)
buildOccurrenceGraph [QName]
qs
      sccs <- lift $ stronglyConnComp g

      -- /lazily computed/ generic graph for debug printing and warnings
      let ggeneric = OccGraph -> Graph Node (Edge OccursWhere)
toGenericGraph OccGraph
g

      reportSDoc "tc.pos.tick" 100 $ "constructed graph"
      reportSLn "tc.pos.graph" 5 $ "Positivity graph: N=" ++ show (size $ Graph.nodes ggeneric) ++
                                   " E=" ++ show (length $ Graph.edges ggeneric)
      reportSDoc "tc.pos.graph" 10 $ vcat
        [ "positivity graph for" <+> fsep (map prettyTCM qs)
        , nest 2 $ prettyTCM ggeneric
        ]

      -- set mutual blocks
      --------------------------------------------------------------------------------
      reportSDoc "tc.pos.graph.sccs" 10 $ do
        let (triv, others) = partitionEithers $ for sccs $ \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
        sep [ text $ show (length triv) ++ " trivial sccs"
            , text $ show (length others) ++ " non-trivial sccs with lengths " ++
                show (map length others)
            ]
      reportSLn "tc.pos.graph.sccs" 15 $
        "  sccs = " ++ prettyShow [ scc | CyclicSCC scc <- sccs ]

      -- #7133: Note that the graph doesn't necessarily contain all of qs in the case where there are no
      -- occurrences of a name, but we still need to setMutual for them.
      let ~sccMap = Map.unions [ case scc of
                                   AcyclicSCC (DefNode QName
q) -> QName -> [QName] -> Map QName [QName]
forall k a. k -> a -> Map k a
Map.singleton QName
q []
                                   AcyclicSCC ArgNode{}   -> Map QName [QName]
forall a. Monoid a => a
mempty
                                   CyclicSCC [Node]
scc          -> [(QName, [QName])] -> Map QName [QName]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (QName
q, [QName]
qs) | QName
q <- [QName]
qs ]
                                     where qs :: [QName]
qs = [ QName
q | DefNode QName
q <- [Node]
scc ]
                               | scc <- sccs ]

      inAbstractMode $ forM_ qs \QName
q -> do
        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) do

          let qs :: [QName]
qs = [QName] -> Maybe [QName] -> [QName]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [QName] -> [QName]) -> Maybe [QName] -> [QName]
forall a b. (a -> b) -> a -> b
$ QName -> Map QName [QName] -> Maybe [QName]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
q Map QName [QName]
sccMap
          [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.pos.mutual" Int
10 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"setting " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
q [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" to " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                                         if | [QName] -> Bool
forall a. Null a => a -> Bool
null [QName]
qs        -> [Char]
"non-recursive"
                                            | [QName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
qs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 -> [Char]
"recursive"
                                            | Bool
otherwise      -> [Char]
"mutually recursive"
          QName -> [QName] -> TCM ()
setMutual QName
q [QName]
qs

      forM_ blockInfo \(QName
q, Int
arity, Maybe (PositivityCheck, DataOrRecord)
dataTypeOrRec, Bool
_) -> QName -> (Definition -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
HasConstInfo m =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q \Definition
_ -> do

        -- set argument occurrences
        --------------------------------------------------------------------------------
        Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (Int
arity Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) do
          [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.pos.args" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"computing arg occurrences 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

          -- If there is no outgoing edge @ArgNode q i@, all @n@ arguments are @Unused@.
          -- Otherwise, we obtain the occurrences from the Graph.
          !args <- [Int] -> (Int -> TCMT IO Occurrence) -> TCMT IO [Occurrence]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int
0 .. Int
arityInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1] \Int
i -> IO Occurrence -> TCMT IO Occurrence
forall (m :: * -> *) a. Monad m => m a -> TCMT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Occurrence -> TCMT IO Occurrence)
-> IO Occurrence -> TCMT IO Occurrence
forall a b. (a -> b) -> a -> b
$ OccGraph -> Node -> Node -> IO Occurrence
transitiveOccurrence OccGraph
g (QName -> Int -> Node
ArgNode QName
q Int
i) (QName -> Node
DefNode QName
q)
              --   [0 .. max m (arity - 1)] -- triggers issue #3049

          reportSDoc "tc.pos.args" 10 $ sep
            [ "args of" <+> prettyTCM q <+> "="
            , nest 2 $ prettyList $ map prettyTCM args
            ]

          let mergeOccs :: [Occurrence] -> [Occurrence] -> [Occurrence]
              mergeOccs [Occurrence]
poccs [Occurrence]
toccs =
                -- Lucas, 2022-12-01:
                -- `poccs` are the occurences computed by the positivity-checker
                -- `toccs` are the occurences/polarities explicitely given by the user
                --   (and enforced through type-checking)
                -- We consider the polarities explicitely given (toccs) to take priority over the ones
                -- found out by the positivity checker.
                -- Note: Alas, this is hard to enforce given that non-annotated variables are
                -- always annotated with Mixed polarity. If the annotated polarity is Mixed,
                -- for now we always rely on the result from the positivity analysis.
                [Occurrence] -> [Occurrence] -> [These Occurrence Occurrence]
forall a b. [a] -> [b] -> [These a b]
align [Occurrence]
poccs [Occurrence]
toccs [These Occurrence Occurrence]
-> (These Occurrence Occurrence -> Occurrence) -> [Occurrence]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (Occurrence -> Occurrence -> Occurrence)
-> These Occurrence Occurrence -> Occurrence
forall a. (a -> a -> a) -> These a a -> a
mergeThese (\Occurrence
a Occurrence
b -> if Occurrence
b Occurrence -> Occurrence -> Bool
forall a. Eq a => a -> a -> Bool
== Occurrence
Mixed then Occurrence
a else Occurrence
b)

          !oldOccs <- getArgOccurrences q
          let !newOccs = let x :: [Occurrence]
x = [Occurrence] -> [Occurrence] -> [Occurrence]
mergeOccs [Occurrence]
args [Occurrence]
oldOccs in [Occurrence] -> [Occurrence] -> [Occurrence]
forall a b. NFData a => a -> b -> b
deepseq [Occurrence]
x [Occurrence]
x
          setArgOccurrences q newOccs
          reportSDoc "tc.pos.tick" 100 $ "set args"


        -- check positivity
        --------------------------------------------------------------------------------
        case Maybe (PositivityCheck, DataOrRecord)
dataTypeOrRec of
          Maybe (PositivityCheck, DataOrRecord)
Nothing -> () -> TCM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Just (PositivityCheck
pc, DataOrRecord
dr) -> do
            [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.pos.check" Int
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 ~Graph Node (Edge (Seq OccursWhere))
ggeneric' = (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)
ggeneric

                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
W.productOfEdgesInBoundedWalk
                         (\(Edge Occurrence
o Seq OccursWhere
_) -> Occurrence
o) Graph Node (Edge (Seq OccursWhere))
ggeneric' (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 :: [Char] -> Occurrence -> TCMT IO Doc
how [Char]
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]
++ [Char] -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
                      [Char] -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
", 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. See Issue 1614.
            -- Andreas, 2026-02-27:
            -- This information now comes either with the mututal block
            -- or with the data/record type, see issue #3355.
            loop <- do
              posCheck <- TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
positivityCheckEnabled
              let nopc = PositivityCheck
NoPositivityCheck
              if Info.mutualPositivityCheck mi == nopc || pc == nopc || not posCheck then
                pure Nothing
              else do
                loop <- lift $ transitiveOccurrence g (DefNode q) (DefNode q)
                when (loop <= JustPos) $ warning $ NotStrictlyPositive q (reason JustPos)
                pure $ Just loop

            let checkInduction :: QName -> TCM ()
                checkInduction QName
q =
                  -- 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, HasCallStack) =>
QName -> m Definition
getConstInfo QName
q) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
                    Range' SrcFile -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (QName -> Range' SrcFile
forall a. HasNameBindingSite a => a -> Range' SrcFile
nameBindingSite QName
q) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
                      Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Warning
RecursiveRecordNeedsInductivity QName
q

            -- Recursivity needs to be declared for inductive records.
            -- Eta should be off for unguarded records.
            case dr of
              DataOrRecord
IsData -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              IsRecord PatternOrCopattern
pat -> do
                loop <- case Maybe Occurrence
loop of
                  Maybe Occurrence
Nothing   -> IO Occurrence -> TCMT IO Occurrence
forall (m :: * -> *) a. Monad m => m a -> TCMT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Occurrence -> TCMT IO Occurrence)
-> IO Occurrence -> TCMT IO Occurrence
forall a b. (a -> b) -> a -> b
$ OccGraph -> Node -> Node -> IO Occurrence
transitiveOccurrence OccGraph
g (QName -> Node
DefNode QName
q) (QName -> Node
DefNode QName
q)
                  Just Occurrence
loop -> Occurrence -> TCMT IO Occurrence
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Occurrence
loop
                case loop of
                  Occurrence
o | Occurrence
o Occurrence -> Occurrence -> Bool
forall a. Ord a => a -> a -> Bool
<= Occurrence
StrictPos -> do
                    [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.pos.record" Int
5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Occurrence -> TCMT IO Doc
how [Char]
"not guarded" Occurrence
StrictPos
                    QName -> TCM ()
unguardedRecord QName
q
                    QName -> TCM ()
checkInduction QName
q
                  Occurrence
o | Occurrence
o Occurrence -> Occurrence -> Bool
forall a. Ord a => a -> a -> Bool
<= Occurrence
GuardPos -> do
                    [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.pos.record" Int
5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Occurrence -> TCMT IO Doc
how [Char]
"recursive" Occurrence
GuardPos
                    QName -> TCM ()
checkInduction QName
q
                  Occurrence
Unused -> [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.pos.record" Int
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"
                  Occurrence
_ -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.pos.tick" Int
100 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checked positivity"

getDefArity :: Definition -> TCM Int
getDefArity :: Definition -> TCM Int
getDefArity Definition
def = do
  let go :: Type -> Int -> ReduceM Int
      go :: Type'' Term Term -> Int -> ReduceM Int
go !Type'' Term Term
a !Int
n = (Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl (Type'' Term Term -> Term)
-> ReduceM (Type'' Term Term) -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type'' Term Term -> ReduceM (Type'' Term Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type'' Term Term
a) ReduceM Term -> (Term -> ReduceM Int) -> ReduceM Int
forall a b. ReduceM a -> (a -> ReduceM b) -> ReduceM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Pi Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b -> Dom (Type'' Term Term)
-> Abs (Type'' Term Term)
-> (Type'' Term Term -> ReduceM Int)
-> ReduceM Int
forall a b.
Dom (Type'' Term Term) -> Abs a -> (a -> ReduceM b) -> ReduceM b
underAbsReduceM Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b \Type'' Term Term
b -> Type'' Term Term -> Int -> ReduceM Int
go Type'' Term Term
b (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
        Term
_      -> Int -> ReduceM Int
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
n
  n <- ReduceM Int -> TCM Int
forall a. ReduceM a -> TCMT IO a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (Type'' Term Term -> Int -> ReduceM Int
go (Definition -> Type'' Term Term
defType Definition
def) Int
0)
  pure $! n - projectionArgs def

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

isDatatype :: Definition -> Maybe (PositivityCheck, DataOrRecord)
isDatatype :: Definition -> Maybe (PositivityCheck, DataOrRecord)
isDatatype Definition
def = do
  case Definition -> Defn
theDef Definition
def of
    Datatype{dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
Nothing, PositivityCheck
dataPositivityCheck :: PositivityCheck
dataPositivityCheck :: Defn -> PositivityCheck
dataPositivityCheck} ->
      (PositivityCheck, DataOrRecord)
-> Maybe (PositivityCheck, DataOrRecord)
forall a. a -> Maybe a
Just (PositivityCheck
dataPositivityCheck, DataOrRecord
forall p. DataOrRecord' p
IsData)
    Record  {recClause :: Defn -> Maybe Clause
recClause  = Maybe Clause
Nothing, PositivityCheck
recPositivityCheck :: PositivityCheck
recPositivityCheck :: Defn -> PositivityCheck
recPositivityCheck, PatternOrCopattern
recPatternMatching :: PatternOrCopattern
recPatternMatching :: Defn -> PatternOrCopattern
recPatternMatching } ->
      (PositivityCheck, DataOrRecord)
-> Maybe (PositivityCheck, DataOrRecord)
forall a. a -> Maybe a
Just (PositivityCheck
recPositivityCheck, PatternOrCopattern -> DataOrRecord
forall p. p -> DataOrRecord' p
IsRecord PatternOrCopattern
recPatternMatching)
    Defn
_ -> Maybe (PositivityCheck, DataOrRecord)
forall a. Maybe a
Nothing

-- Result: [(name, arity, data or record, do we need to setMutual)] or Nothing if we don't need any
-- occurrence analysis.
preprocessBlock :: [QName] -> TCM (Maybe ([(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]))
preprocessBlock :: [QName]
-> TCM
     (Maybe [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)])
preprocessBlock [QName]
qs = do
  let go :: [QName]
-> TCMT
     IO [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]
go []     = [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]
-> TCMT
     IO [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
      go (QName
q:[QName]
qs) = QName
-> (Definition
    -> TCMT
         IO [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)])
-> TCMT
     IO [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]
forall (m :: * -> *) a.
HasConstInfo m =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q \Definition
def -> do
        !arity <- case Defn -> Bool
hasDefinition (Definition -> Defn
theDef Definition
def) of
          Bool
True  -> Definition -> TCM Int
getDefArity Definition
def
          Bool
False -> Int -> TCM Int
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
0
        let !dr = Definition -> Maybe (PositivityCheck, DataOrRecord)
isDatatype Definition
def
        let !needToSetMutual = Maybe [QName] -> Bool
forall a. Maybe a -> Bool
isNothing (Defn -> Maybe [QName]
getMutual_ (Definition -> Defn
theDef Definition
def))
        !rest <- go qs
        pure ((q, arity, dr, needToSetMutual) : rest)
  info <- [QName]
-> TCMT
     IO [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]
go [QName]
qs
  case any (\(QName
_, Int
arity, Maybe (PositivityCheck, DataOrRecord)
dr, Bool
setMut) -> Int
arity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0 Bool -> Bool -> Bool
|| Maybe (PositivityCheck, DataOrRecord) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (PositivityCheck, DataOrRecord)
dr Bool -> Bool -> Bool
|| Bool
setMut) info of
    Bool
True -> Maybe [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]
-> TCM
     (Maybe [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)])
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]
 -> TCM
      (Maybe
         [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]))
-> Maybe
     [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]
-> TCM
     (Maybe [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)])
forall a b. (a -> b) -> a -> b
$ [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]
-> Maybe
     [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]
forall a. a -> Maybe a
Just [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]
info
    Bool
_    -> Maybe [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]
-> TCM
     (Maybe [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)])
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]
forall a. Maybe a
Nothing


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

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

instance PrettyTCM (Seq W.OccursWhere) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Seq OccursWhere -> m Doc
prettyTCM =
    (([Char], Doc) -> Doc) -> m ([Char], 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 ([Char], Doc) -> Doc
forall a b. (a, b) -> b
snd (m ([Char], Doc) -> m Doc)
-> (Seq OccursWhere -> m ([Char], Doc)) -> Seq OccursWhere -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OccursWhere] -> m ([Char], Doc)
forall (m :: * -> *).
MonadPretty m =>
[OccursWhere] -> m ([Char], Doc)
prettyOWs ([OccursWhere] -> m ([Char], Doc))
-> (Seq OccursWhere -> [OccursWhere])
-> Seq OccursWhere
-> m ([Char], 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 = [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"first"
      nth a
1 = [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"second"
      nth a
2 = [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"third"
      nth a
n = [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ a -> [Char]
forall a. Show a => a -> [Char]
show (a
n a -> a -> a
forall a. Num a => a -> a -> a
+ a
1) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"th"

      -- Removes consecutive duplicates.
      uniq :: [W.OccursWhere] -> [W.OccursWhere]
      uniq :: [OccursWhere] -> [OccursWhere]
uniq = (NonEmpty OccursWhere -> OccursWhere)
-> [NonEmpty OccursWhere] -> [OccursWhere]
forall a b. (a -> b) -> [a] -> [b]
map NonEmpty OccursWhere -> OccursWhere
forall a. NonEmpty a -> a
List1.head ([NonEmpty OccursWhere] -> [OccursWhere])
-> ([OccursWhere] -> [NonEmpty OccursWhere])
-> [OccursWhere]
-> [OccursWhere]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OccursWhere -> OccursWhere -> Bool)
-> [OccursWhere] -> [NonEmpty OccursWhere]
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> Bool) -> f a -> [NonEmpty a]
List1.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' (W.OccursWhere Range' SrcFile
_ Seq Where
_ Seq Where
ws) = Seq Where
ws

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

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

      prettyWs :: MonadPretty m => Seq W.Where -> m (String, Doc)
      prettyWs :: forall (m :: * -> *). MonadPretty m => Seq Where -> m ([Char], 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
        [W.InDefOf QName
d, Where
W.InIndex] ->
          (,) [Char]
"is" (Doc -> ([Char], Doc)) -> m Doc -> m ([Char], 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 ([Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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]
_ ->
          (,) [Char]
"occurs" (Doc -> ([Char], Doc)) -> m Doc -> m ([Char], 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 => W.Where -> [m Doc]
      prettyW :: forall (m :: * -> *). MonadPretty m => Where -> [m Doc]
prettyW = \case
        Where
W.LeftOfArrow  -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"to the left of an arrow"
        W.DefArg QName
q Int
i   -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in the" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ Int -> [m Doc]
forall {a} {m :: * -> *}.
(Eq a, Num a, Applicative m, Show a) =>
a -> [m Doc]
nth Int
i [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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
W.UnderInf     -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"under" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
                           [do -- this cannot fail if an 'UnderInf' has been generated
                            inf <- QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinInf
                            prettyTCM inf]
        W.VarArg Occurrence
p Int
i   -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in an argument of a bound variable at position" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Int -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Int -> m Doc
prettyTCM Int
i]
                         [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which uses its argument with polarity" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ Occurrence -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Occurrence
p ]
        Where
W.MetaArg      -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in an argument of a metavariable"
        W.ConArgType QName
c -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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]
        W.IndArgType QName
c -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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]
        W.ConEndpoint QName
c -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in an endpoint of the target of the" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
                           [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"higher 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]
        W.InClause Int
i   -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in the" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ Int -> [m Doc]
forall {a} {m :: * -> *}.
(Eq a, Num a, Applicative m, Show a) =>
a -> [m Doc]
nth Int
i [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"clause"
        Where
W.Matched      -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"as matched against"
        Where
W.InIndex      -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"as an index"
        W.InDefOf QName
d    -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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 :: W.OccursWhere -> W.OccursWhere
      adjustLeftOfArrow :: OccursWhere -> OccursWhere
adjustLeftOfArrow (W.OccursWhere Range' SrcFile
r Seq Where
cs Seq Where
os) =
        Range' SrcFile -> Seq Where -> Seq Where -> OccursWhere
W.OccursWhere Range' SrcFile
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 W.LeftOfArrow{} = Bool
True
        isArrow Where
_               = Bool
False