-- | Computing the polarity (variance) of function arguments,
--   for the sake of subtyping.

module Agda.TypeChecking.Polarity
  ( -- * Polarity computation
    computePolarity
    -- * Auxiliary functions
  , composePol
  , nextPolarity
  , purgeNonvariant
  , polFromOcc
  ) where

import Control.Monad  ( forM_, zipWithM )

import Data.Maybe
import Data.Semigroup ( Semigroup(..) )

import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Internal

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Datatypes (getNumberOfParameters)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.SizedTypes
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Free
import Agda.TypeChecking.Positivity.Occurrence

import Agda.Utils.List
import Agda.Utils.Maybe ( whenNothingM )
import Agda.Utils.Monad
import Agda.Utils.Pretty ( prettyShow )
import Agda.Utils.Singleton
import Agda.Utils.Size

import Agda.Utils.Impossible

------------------------------------------------------------------------
-- * Polarity lattice.
------------------------------------------------------------------------

-- | Infimum on the information lattice.
--   'Invariant' is bottom (dominant for inf),
--   'Nonvariant' is top (neutral for inf).
(/\) :: Polarity -> Polarity -> Polarity
Polarity
Nonvariant /\ :: Polarity -> Polarity -> Polarity
/\ Polarity
b = Polarity
b
Polarity
a /\ Polarity
Nonvariant = Polarity
a
Polarity
a /\ Polarity
b | Polarity
a Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
b    = Polarity
a
       | Bool
otherwise = Polarity
Invariant

-- | 'Polarity' negation, swapping monotone and antitone.
neg :: Polarity -> Polarity
neg :: Polarity -> Polarity
neg Polarity
Covariant     = Polarity
Contravariant
neg Polarity
Contravariant = Polarity
Covariant
neg Polarity
Invariant     = Polarity
Invariant
neg Polarity
Nonvariant    = Polarity
Nonvariant

-- | What is the polarity of a function composition?
composePol :: Polarity -> Polarity -> Polarity
composePol :: Polarity -> Polarity -> Polarity
composePol Polarity
Nonvariant Polarity
_    = Polarity
Nonvariant
composePol Polarity
_ Polarity
Nonvariant    = Polarity
Nonvariant
composePol Polarity
Invariant Polarity
_     = Polarity
Invariant
composePol Polarity
Covariant Polarity
x     = Polarity
x
composePol Polarity
Contravariant Polarity
x = Polarity -> Polarity
neg Polarity
x

polFromOcc :: Occurrence -> Polarity
polFromOcc :: Occurrence -> Polarity
polFromOcc = \case
  Occurrence
GuardPos  -> Polarity
Covariant
  Occurrence
StrictPos -> Polarity
Covariant
  Occurrence
JustPos   -> Polarity
Covariant
  Occurrence
JustNeg   -> Polarity
Contravariant
  Occurrence
Mixed     -> Polarity
Invariant
  Occurrence
Unused    -> Polarity
Nonvariant

------------------------------------------------------------------------
-- * Auxiliary functions
------------------------------------------------------------------------

-- | Get the next polarity from a list, 'Invariant' if empty.
nextPolarity :: [Polarity] -> (Polarity, [Polarity])
nextPolarity :: [Polarity] -> (Polarity, [Polarity])
nextPolarity []       = (Polarity
Invariant, [])
nextPolarity (Polarity
p : [Polarity]
ps) = (Polarity
p, [Polarity]
ps)

-- | Replace 'Nonvariant' by 'Covariant'.
--   (Arbitrary bias, but better than 'Invariant', see issue 1596).
purgeNonvariant :: [Polarity] -> [Polarity]
purgeNonvariant :: [Polarity] -> [Polarity]
purgeNonvariant = (Polarity -> Polarity) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map (\ Polarity
p -> if Polarity
p Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
Nonvariant then Polarity
Covariant else Polarity
p)


-- | A quick transliterations of occurrences to polarities.
polarityFromPositivity
  :: (HasConstInfo m, MonadTCEnv m, MonadTCState m, MonadDebug m)
  => QName -> m ()
polarityFromPositivity :: forall (m :: * -> *).
(HasConstInfo m, MonadTCEnv m, MonadTCState m, MonadDebug m) =>
QName -> m ()
polarityFromPositivity QName
x = QName -> (Definition -> m ()) -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
x ((Definition -> m ()) -> m ()) -> (Definition -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ Definition
def -> do

  -- Get basic polarity from positivity analysis.
  let npars :: Int
npars = Definition -> Int
droppedPars Definition
def
  let pol0 :: [Polarity]
pol0 = Int -> Polarity -> [Polarity]
forall a. Int -> a -> [a]
replicate Int
npars Polarity
Nonvariant [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
++ (Occurrence -> Polarity) -> [Occurrence] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> Polarity
polFromOcc (Definition -> [Occurrence]
defArgOccurrences Definition
def)
  [Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.polarity.set" Int
15 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$
    [Char]
"Polarity of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" from positivity: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Polarity] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [Polarity]
pol0

  -- set the polarity in the signature (not the final polarity, though)
  QName -> [Polarity] -> m ()
forall (m :: * -> *).
(MonadTCState m, MonadDebug m) =>
QName -> [Polarity] -> m ()
setPolarity QName
x ([Polarity] -> m ()) -> [Polarity] -> m ()
forall a b. (a -> b) -> a -> b
$ Int -> [Polarity] -> [Polarity]
forall a. Int -> [a] -> [a]
drop Int
npars [Polarity]
pol0

------------------------------------------------------------------------
-- * Computing the polarity of a symbol.
------------------------------------------------------------------------

-- | Main function of this module.
computePolarity
  :: ( HasOptions m, HasConstInfo m, HasBuiltins m
     , MonadTCEnv m, MonadTCState m, MonadReduce m, MonadAddContext m, MonadTCError m
     , MonadDebug m, MonadPretty m )
  => [QName] -> m ()
computePolarity :: forall (m :: * -> *).
(HasOptions m, HasConstInfo m, HasBuiltins m, MonadTCEnv m,
 MonadTCState m, MonadReduce m, MonadAddContext m, MonadTCError m,
 MonadDebug m, MonadPretty m) =>
[QName] -> m ()
computePolarity [QName]
xs = do

 -- Andreas, 2017-04-26, issue #2554
 -- First, for mutual definitions, obtain a crude polarity from positivity.
 Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([QName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ (QName -> m ()) -> [QName] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ QName -> m ()
forall (m :: * -> *).
(HasConstInfo m, MonadTCEnv m, MonadTCState m, MonadDebug m) =>
QName -> m ()
polarityFromPositivity [QName]
xs

 -- Then, refine it.
 [QName] -> (QName -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [QName]
xs ((QName -> m ()) -> m ()) -> (QName -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ QName
x -> QName -> (Definition -> m ()) -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
x ((Definition -> m ()) -> m ()) -> (Definition -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ Definition
def -> do
  [Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.polarity.set" Int
25 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Refining polarity of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
x

  -- Again: get basic polarity from positivity analysis.
  let npars :: Int
npars = Definition -> Int
droppedPars Definition
def
  let pol0 :: [Polarity]
pol0 = Int -> Polarity -> [Polarity]
forall a. Int -> a -> [a]
replicate Int
npars Polarity
Nonvariant [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
++ (Occurrence -> Polarity) -> [Occurrence] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> Polarity
polFromOcc (Definition -> [Occurrence]
defArgOccurrences Definition
def)
  [Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.polarity.set" Int
15 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$
    [Char]
"Polarity of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" from positivity: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Polarity] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [Polarity]
pol0

{-
  -- get basic polarity from shape of def (arguments matched on or not?)
  def      <- getConstInfo x
  let usagePol = usagePolarity $ theDef def
  reportSLn "tc.polarity.set" 15 $ "Polarity of " ++ prettyShow x ++ " from definition form: " ++ prettyShow usagePol
  let n = genericLength usagePol  -- n <- getArity x
  reportSLn "tc.polarity.set" 20 $ "  arity = " ++ show n

  -- refine polarity by positivity information
  pol0 <- zipWith (/\) usagePol <$> mapM getPol [0..n - 1]
  reportSLn "tc.polarity.set" 15 $ "Polarity of " ++ prettyShow x ++ " from positivity: " ++ prettyShow pol0
-}

  -- compute polarity of sized types
  [Polarity]
pol1 <- QName -> [Polarity] -> m [Polarity]
forall (m :: * -> *).
(HasOptions m, HasConstInfo m, HasBuiltins m, ReadTCState m,
 MonadTCEnv m, MonadTCState m, MonadReduce m, MonadAddContext m,
 MonadTCError m, MonadDebug m, MonadPretty m) =>
QName -> [Polarity] -> m [Polarity]
sizePolarity QName
x [Polarity]
pol0

  -- refine polarity again by using type information
  let t :: Type
t = Definition -> Type
defType Definition
def
  -- Instantiation takes place in Rules.Decl.instantiateDefinitionType
  -- t <- instantiateFull t -- Andreas, 2014-04-11 Issue 1099: needed for
  --                        -- variable occurrence test in  dependentPolarity.
  [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.set" Int
15 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Refining polarity with type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
  [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.set" Int
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Refining polarity with type (raw): " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> (Type -> [Char]) -> Type -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Type -> [Char]
forall a. Show a => a -> [Char]
show) Type
t

  [Polarity]
pol <- Type -> [Polarity] -> [Polarity] -> m [Polarity]
forall (m :: * -> *).
(HasOptions m, HasBuiltins m, MonadReduce m, MonadAddContext m,
 MonadDebug m) =>
Type -> [Polarity] -> [Polarity] -> m [Polarity]
dependentPolarity Type
t (Defn -> [Polarity] -> [Polarity]
enablePhantomTypes (Definition -> Defn
theDef Definition
def) [Polarity]
pol1) [Polarity]
pol1
  [Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.polarity.set" Int
10 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Polarity of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Polarity] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [Polarity]
pol

  -- set the polarity in the signature
  QName -> [Polarity] -> m ()
forall (m :: * -> *).
(MonadTCState m, MonadDebug m) =>
QName -> [Polarity] -> m ()
setPolarity QName
x ([Polarity] -> m ()) -> [Polarity] -> m ()
forall a b. (a -> b) -> a -> b
$ Int -> [Polarity] -> [Polarity]
forall a. Int -> [a] -> [a]
drop Int
npars [Polarity]
pol -- purgeNonvariant pol -- temporarily disable non-variance

-- | Data and record parameters are used as phantom arguments all over
--   the test suite (and possibly in user developments).
--   @enablePhantomTypes@ turns 'Nonvariant' parameters to 'Covariant'
--   to enable phantoms.
enablePhantomTypes :: Defn -> [Polarity] -> [Polarity]
enablePhantomTypes :: Defn -> [Polarity] -> [Polarity]
enablePhantomTypes Defn
def [Polarity]
pol = case Defn
def of
  Datatype{ dataPars :: Defn -> Int
dataPars = Int
np } -> Int -> [Polarity]
enable Int
np
  Record  { recPars :: Defn -> Int
recPars  = Int
np } -> Int -> [Polarity]
enable Int
np
  Defn
_                         -> [Polarity]
pol
  where enable :: Int -> [Polarity]
enable Int
np = let ([Polarity]
pars, [Polarity]
rest) = Int -> [Polarity] -> ([Polarity], [Polarity])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
np [Polarity]
pol
                    in  [Polarity] -> [Polarity]
purgeNonvariant [Polarity]
pars [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
++ [Polarity]
rest

{- UNUSED
-- | Extract a basic approximate polarity info from the shape of definition.
--   Arguments that are matched against get 'Invariant', others 'Nonvariant'.
--   For data types, parameters get 'Nonvariant', indices 'Invariant'.
usagePolarity :: Defn -> [Polarity]
usagePolarity def = case def of
    Axiom{}                                 -> []
    Function{ funClauses = [] }             -> []
    Function{ funClauses = cs }             -> usage $ map namedClausePats cs
    Datatype{ dataPars = np, dataIxs = ni } -> genericReplicate np Nonvariant
    Record{ recPars = n }                   -> genericReplicate n Nonvariant
    Constructor{}                           -> []
    Primitive{}                             -> []
  where
    usage = foldr1 (zipWith (/\)) . map (map (usagePat . namedArg))
    usagePat VarP{} = Nonvariant
    usagePat DotP{} = Nonvariant
    usagePat ConP{} = Invariant
    usagePat LitP{} = Invariant
-}

-- | Make arguments 'Invariant' if the type of a not-'Nonvariant'
--   later argument depends on it.
--   Also, enable phantom types by turning 'Nonvariant' into something
--   else if it is a data/record parameter but not a size argument. [See issue 1596]
--
--   Precondition: the "phantom" polarity list has the same length as the polarity list.
dependentPolarity
  :: (HasOptions m, HasBuiltins m, MonadReduce m, MonadAddContext m, MonadDebug m)
  => Type -> [Polarity] -> [Polarity] -> m [Polarity]
dependentPolarity :: forall (m :: * -> *).
(HasOptions m, HasBuiltins m, MonadReduce m, MonadAddContext m,
 MonadDebug m) =>
Type -> [Polarity] -> [Polarity] -> m [Polarity]
dependentPolarity Type
t [Polarity]
_      []          = [Polarity] -> m [Polarity]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []  -- all remaining are 'Invariant'
dependentPolarity Type
t []     (Polarity
_ : [Polarity]
_)     = m [Polarity]
forall a. HasCallStack => a
__IMPOSSIBLE__
dependentPolarity Type
t (Polarity
q:[Polarity]
qs) pols :: [Polarity]
pols@(Polarity
p:[Polarity]
ps) = do
  Term
t <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Type -> Term
forall t a. Type'' t a -> a
unEl Type
t
  [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.dep" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"dependentPolarity t = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t
  [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.dep" Int
70 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"dependentPolarity t = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> (Term -> [Char]) -> Term -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> [Char]
forall a. Show a => a -> [Char]
show) Term
t
  case Term
t of
    Pi Dom Type
dom Abs Type
b -> do
      [Polarity]
ps <- Dom Type -> Abs Type -> (Type -> m [Polarity]) -> m [Polarity]
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
dom Abs Type
b ((Type -> m [Polarity]) -> m [Polarity])
-> (Type -> m [Polarity]) -> m [Polarity]
forall a b. (a -> b) -> a -> b
$ \ Type
c -> Type -> [Polarity] -> [Polarity] -> m [Polarity]
forall (m :: * -> *).
(HasOptions m, HasBuiltins m, MonadReduce m, MonadAddContext m,
 MonadDebug m) =>
Type -> [Polarity] -> [Polarity] -> m [Polarity]
dependentPolarity Type
c [Polarity]
qs [Polarity]
ps
      let fallback :: m Polarity
fallback = m Bool -> m Polarity -> m Polarity -> m Polarity
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Maybe BoundedSize -> Bool
forall a. Maybe a -> Bool
isJust (Maybe BoundedSize -> Bool) -> m (Maybe BoundedSize) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Type -> m (Maybe BoundedSize)
isSizeType (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom)) (Polarity -> m Polarity
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
p) (Polarity -> m Polarity
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
q)
      Polarity
p <- case Abs Type
b of
        Abs{} | Polarity
p Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
/= Polarity
Invariant  ->
          -- Andreas, 2014-04-11 see Issue 1099
          -- Free variable analysis is not in the monad,
          -- hence metas must have been instantiated before!
          m Bool -> m Polarity -> m Polarity -> m Polarity
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Int -> Type -> [Polarity] -> m Bool
forall (m :: * -> *).
MonadReduce m =>
Int -> Type -> [Polarity] -> m Bool
relevantInIgnoringNonvariant Int
0 (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b) [Polarity]
ps)
            {- then -} (Polarity -> m Polarity
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Invariant)
            {- else -} m Polarity
fallback
        Abs Type
_ -> m Polarity
fallback
      [Polarity] -> m [Polarity]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Polarity] -> m [Polarity]) -> [Polarity] -> m [Polarity]
forall a b. (a -> b) -> a -> b
$ Polarity
p Polarity -> [Polarity] -> [Polarity]
forall a. a -> [a] -> [a]
: [Polarity]
ps
    Term
_ -> [Polarity] -> m [Polarity]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [Polarity]
pols

-- | Check whether a variable is relevant in a type expression,
--   ignoring domains of non-variant arguments.
relevantInIgnoringNonvariant :: MonadReduce m => Nat -> Type -> [Polarity] -> m Bool
relevantInIgnoringNonvariant :: forall (m :: * -> *).
MonadReduce m =>
Int -> Type -> [Polarity] -> m Bool
relevantInIgnoringNonvariant Int
i Type
t []     = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Type -> Bool
forall t. Free t => Int -> t -> Bool
`relevantInIgnoringSortAnn` Type
t
relevantInIgnoringNonvariant Int
i Type
t (Polarity
p:[Polarity]
ps) =
  Type
-> (Type -> m Bool) -> (Dom Type -> Abs Type -> m Bool) -> m Bool
forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPiType Type
t
    {-then-} (\ Type
t -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Type -> Bool
forall t. Free t => Int -> t -> Bool
`relevantInIgnoringSortAnn` Type
t) ((Dom Type -> Abs Type -> m Bool) -> m Bool)
-> (Dom Type -> Abs Type -> m Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$
    {-else-} \ Dom Type
a Abs Type
b ->
      if Polarity
p Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
/= Polarity
Nonvariant Bool -> Bool -> Bool
&& Int
i Int -> Dom Type -> Bool
forall t. Free t => Int -> t -> Bool
`relevantInIgnoringSortAnn` Dom Type
a
        then Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        else Int -> Type -> [Polarity] -> m Bool
forall (m :: * -> *).
MonadReduce m =>
Int -> Type -> [Polarity] -> m Bool
relevantInIgnoringNonvariant (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b) [Polarity]
ps

------------------------------------------------------------------------
-- * Sized types
------------------------------------------------------------------------

-- | Hack for polarity of size indices.
--   As a side effect, this sets the positivity of the size index.
--   See test/succeed/PolaritySizeSucData.agda for a case where this is needed.
sizePolarity
  :: forall m .
     ( HasOptions m, HasConstInfo m, HasBuiltins m, ReadTCState m
     , MonadTCEnv m, MonadTCState m, MonadReduce m, MonadAddContext m, MonadTCError m
     , MonadDebug m, MonadPretty m )
  => QName -> [Polarity] -> m [Polarity]
sizePolarity :: forall (m :: * -> *).
(HasOptions m, HasConstInfo m, HasBuiltins m, ReadTCState m,
 MonadTCEnv m, MonadTCState m, MonadReduce m, MonadAddContext m,
 MonadTCError m, MonadDebug m, MonadPretty m) =>
QName -> [Polarity] -> m [Polarity]
sizePolarity QName
d [Polarity]
pol0 = do
  let exit :: m [Polarity]
exit = [Polarity] -> m [Polarity]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [Polarity]
pol0
  m Bool -> m [Polarity] -> m [Polarity] -> m [Polarity]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM m Bool
forall (m :: * -> *). HasOptions m => m Bool
sizedTypesOption m [Polarity]
exit (m [Polarity] -> m [Polarity]) -> m [Polarity] -> m [Polarity]
forall a b. (a -> b) -> a -> b
$ {- else -} do
    Definition
def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
    case Definition -> Defn
theDef Definition
def of
      Datatype{ dataPars :: Defn -> Int
dataPars = Int
np, dataCons :: Defn -> [QName]
dataCons = [QName]
cons } -> do
        let TelV Tele (Dom Type)
tel Type
_      = Type -> TelV Type
telView' (Type -> TelV Type) -> Type -> TelV Type
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
            ([Dom ([Char], Type)]
parTel, [Dom ([Char], Type)]
ixTel) = Int
-> [Dom ([Char], Type)]
-> ([Dom ([Char], Type)], [Dom ([Char], Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
np ([Dom ([Char], Type)]
 -> ([Dom ([Char], Type)], [Dom ([Char], Type)]))
-> [Dom ([Char], Type)]
-> ([Dom ([Char], Type)], [Dom ([Char], Type)])
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel
        case [Dom ([Char], Type)]
ixTel of
          []                 -> m [Polarity]
exit  -- No size index
          Dom{unDom :: forall t e. Dom' t e -> e
unDom = ([Char]
_,Type
a)} : [Dom ([Char], Type)]
_ -> m Bool -> m [Polarity] -> m [Polarity] -> m [Polarity]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((Maybe BoundedSize -> Maybe BoundedSize -> Bool
forall a. Eq a => a -> a -> Bool
/= BoundedSize -> Maybe BoundedSize
forall a. a -> Maybe a
Just BoundedSize
BoundedNo) (Maybe BoundedSize -> Bool) -> m (Maybe BoundedSize) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Type -> m (Maybe BoundedSize)
isSizeType Type
a) m [Polarity]
exit (m [Polarity] -> m [Polarity]) -> m [Polarity] -> m [Polarity]
forall a b. (a -> b) -> a -> b
$ do
            -- we assume the size index to be 'Covariant' ...
            let pol :: [Polarity]
pol   = Int -> [Polarity] -> [Polarity]
forall a. Int -> [a] -> [a]
take Int
np [Polarity]
pol0
                polCo :: [Polarity]
polCo = [Polarity]
pol [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
++ [Polarity
Covariant]
                polIn :: [Polarity]
polIn = [Polarity]
pol [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
++ [Polarity
Invariant]
            QName -> [Polarity] -> m ()
forall (m :: * -> *).
(MonadTCState m, MonadDebug m) =>
QName -> [Polarity] -> m ()
setPolarity QName
d ([Polarity] -> m ()) -> [Polarity] -> m ()
forall a b. (a -> b) -> a -> b
$ [Polarity]
polCo
            -- and seek confirm it by looking at the constructor types
            let check :: QName -> m Bool
                check :: QName -> m Bool
check QName
c = do
                  Type
t <- Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
                  Tele (Dom Type) -> m Bool -> m Bool
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 ([Dom ([Char], Type)] -> Tele (Dom Type)
telFromList [Dom ([Char], Type)]
parTel) (m Bool -> m Bool) -> m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ do
                    let pars :: [Arg Term]
pars = (Int -> Arg Term) -> [Int] -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> (Int -> Term) -> Int -> Arg Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var) ([Int] -> [Arg Term]) -> [Int] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
np
                    TelV Tele (Dom Type)
conTel Type
target <- Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Type -> m (TelV Type)) -> m Type -> m (TelV Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Type
t Type -> [Arg Term] -> m Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
Type -> [Arg Term] -> m Type
`piApplyM` [Arg Term]
pars)
                    Type -> Tele (Dom Type) -> m Bool
loop Type
target Tele (Dom Type)
conTel
                  where
                  loop :: Type -> Telescope -> m Bool
                  -- no suitable size argument
                  loop :: Type -> Tele (Dom Type) -> m Bool
loop Type
_ Tele (Dom Type)
EmptyTel = do
                    [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.size" Int
15 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
                      TCMT IO Doc
"constructor" 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
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"fails size polarity check"
                    Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

                  -- try argument @dom@
                  loop Type
target (ExtendTel Dom Type
dom Abs (Tele (Dom Type))
tel) = do
                    Maybe BoundedSize
isSz <- Dom Type -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Dom Type -> m (Maybe BoundedSize)
isSizeType Dom Type
dom
                    Dom Type
-> Abs (Tele (Dom Type)) -> (Tele (Dom Type) -> m Bool) -> m Bool
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
dom Abs (Tele (Dom Type))
tel ((Tele (Dom Type) -> m Bool) -> m Bool)
-> (Tele (Dom Type) -> m Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ \ Tele (Dom Type)
tel -> do
                      let continue :: m Bool
continue = Type -> Tele (Dom Type) -> m Bool
loop Type
target Tele (Dom Type)
tel

                      -- check that dom == Size
                      if Maybe BoundedSize
isSz Maybe BoundedSize -> Maybe BoundedSize -> Bool
forall a. Eq a => a -> a -> Bool
/= BoundedSize -> Maybe BoundedSize
forall a. a -> Maybe a
Just BoundedSize
BoundedNo then m Bool
continue else do

                        -- check that the size argument appears in the
                        -- right spot in the target type
                        let sizeArg :: Int
sizeArg = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
                        Bool
isLin <- Tele (Dom Type) -> m Bool -> m Bool
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)
tel (m Bool -> m Bool) -> m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ QName -> Int -> Type -> m Bool
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadDebug m, MonadPretty m,
 MonadTCError m) =>
QName -> Int -> Type -> m Bool
checkSizeIndex QName
d Int
sizeArg Type
target
                        if Bool -> Bool
not Bool
isLin then m Bool
continue else do

                          -- check that only positive occurences in tel
                          [Polarity]
pols <- (Int -> Type -> m Polarity) -> [Int] -> [Type] -> m [Polarity]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Int -> Type -> m Polarity
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> a -> m Polarity
polarity [Int
0..] ([Type] -> m [Polarity]) -> [Type] -> m [Polarity]
forall a b. (a -> b) -> a -> b
$ (Dom ([Char], Type) -> Type) -> [Dom ([Char], Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (([Char], Type) -> Type
forall a b. (a, b) -> b
snd (([Char], Type) -> Type)
-> (Dom ([Char], Type) -> ([Char], Type))
-> Dom ([Char], Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom ([Char], Type) -> ([Char], Type)
forall t e. Dom' t e -> e
unDom) ([Dom ([Char], Type)] -> [Type]) -> [Dom ([Char], Type)] -> [Type]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel
                          [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.size" Int
25 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
                            [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"to pass size polarity check, the following polarities need all to be covariant: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Polarity] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [Polarity]
pols
                          if (Polarity -> Bool) -> [Polarity] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Polarity -> [Polarity] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Polarity
Nonvariant, Polarity
Covariant]) [Polarity]
pols then m Bool
continue else do
                            [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.size" Int
15 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
                              TCMT IO Doc
"constructor" 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
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"passes size polarity check"
                            Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

            m Bool -> m [Polarity] -> m [Polarity] -> m [Polarity]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM ([m Bool] -> m Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM ([m Bool] -> m Bool) -> [m Bool] -> m Bool
forall a b. (a -> b) -> a -> b
$ (QName -> m Bool) -> [QName] -> [m Bool]
forall a b. (a -> b) -> [a] -> [b]
map QName -> m Bool
check [QName]
cons)
                ([Polarity] -> m [Polarity]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [Polarity]
polIn) -- no, does not conform to the rules of sized types
              (m [Polarity] -> m [Polarity]) -> m [Polarity] -> m [Polarity]
forall a b. (a -> b) -> a -> b
$ do  -- yes, we have a sized type here
                -- Andreas, 2015-07-01
                -- As a side effect, mark the size also covariant for subsequent
                -- positivity checking (which feeds back into polarity analysis).
                QName -> ([Occurrence] -> [Occurrence]) -> m ()
forall (m :: * -> *).
MonadTCState m =>
QName -> ([Occurrence] -> [Occurrence]) -> m ()
modifyArgOccurrences QName
d (([Occurrence] -> [Occurrence]) -> m ())
-> ([Occurrence] -> [Occurrence]) -> m ()
forall a b. (a -> b) -> a -> b
$ \ [Occurrence]
occ -> Int -> [Occurrence] -> [Occurrence]
forall a. Int -> [a] -> [a]
take Int
np [Occurrence]
occ [Occurrence] -> [Occurrence] -> [Occurrence]
forall a. [a] -> [a] -> [a]
++ [Occurrence
JustPos]
                [Polarity] -> m [Polarity]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [Polarity]
polCo
      Defn
_ -> m [Polarity]
exit

-- | @checkSizeIndex d i a@ checks that constructor target type @a@
--   has form @d ps (↑ⁿ i) idxs@ where @|ps| = np(d)@.
--
--   Precondition: @a@ is reduced and of form @d ps idxs0@.
checkSizeIndex
  :: (HasConstInfo m, ReadTCState m, MonadDebug m, MonadPretty m, MonadTCError m)
  => QName -> Nat -> Type -> m Bool
checkSizeIndex :: forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadDebug m, MonadPretty m,
 MonadTCError m) =>
QName -> Int -> Type -> m Bool
checkSizeIndex QName
d Int
i Type
a = do
  [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.size" Int
15 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments (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, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"checking that constructor target type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
    , TCMT IO Doc
"  is data 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
d
    , TCMT IO Doc
"  and has size index (successor(s) of) " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Int -> Term
var Int
i)
    ]
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
a of
    Def QName
d0 [Elim]
es -> do
      m (Maybe QName) -> m () -> m ()
forall (m :: * -> *) a. Monad m => m (Maybe a) -> m () -> m ()
whenNothingM (QName -> QName -> m (Maybe QName)
forall (m :: * -> *).
HasConstInfo m =>
QName -> QName -> m (Maybe QName)
sameDef QName
d QName
d0) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      Int
np <- Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Int -> Int) -> m (Maybe Int) -> m Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe Int)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Int)
getNumberOfParameters QName
d0
      let ([Elim]
pars, Apply Arg Term
ix : [Elim]
ixs) = Int -> [Elim] -> ([Elim], [Elim])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
np [Elim]
es
      DeepSizeView
s <- Term -> m DeepSizeView
forall (m :: * -> *).
(PureTCM m, MonadTCError m) =>
Term -> m DeepSizeView
deepSizeView (Term -> m DeepSizeView) -> Term -> m DeepSizeView
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
ix
      case DeepSizeView
s of
        DSizeVar (ProjectedVar Int
j []) Int
_ | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j
          -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Int -> [Elim] -> Bool
forall t. Free t => Int -> t -> Bool
freeIn Int
i ([Elim]
pars [Elim] -> [Elim] -> [Elim]
forall a. [a] -> [a] -> [a]
++ [Elim]
ixs)
        DeepSizeView
_ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Term
_ -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | @polarity i a@ computes the least polarity of de Bruijn index @i@
--   in syntactic entity @a@.
polarity
  :: (HasPolarity a, HasConstInfo m, MonadReduce m)
  => Nat -> a -> m Polarity
polarity :: forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> a -> m Polarity
polarity Int
i a
x = LeastPolarity m -> m Polarity
forall (m :: * -> *). LeastPolarity m -> m Polarity
getLeastPolarity (LeastPolarity m -> m Polarity) -> LeastPolarity m -> m Polarity
forall a b. (a -> b) -> a -> b
$ Int -> Polarity -> a -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
polarity' Int
i Polarity
Covariant a
x

-- | A monoid for lazily computing the infimum of the polarities of a variable in some object.
-- Allows short-cutting.

newtype LeastPolarity m = LeastPolarity { forall (m :: * -> *). LeastPolarity m -> m Polarity
getLeastPolarity :: m Polarity}

instance Monad m => Singleton Polarity (LeastPolarity m) where
  singleton :: Polarity -> LeastPolarity m
singleton = m Polarity -> LeastPolarity m
forall (m :: * -> *). m Polarity -> LeastPolarity m
LeastPolarity (m Polarity -> LeastPolarity m)
-> (Polarity -> m Polarity) -> Polarity -> LeastPolarity m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Polarity -> m Polarity
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return

instance Monad m => Semigroup (LeastPolarity m) where
  LeastPolarity m Polarity
mp <> :: LeastPolarity m -> LeastPolarity m -> LeastPolarity m
<> LeastPolarity m Polarity
mq = m Polarity -> LeastPolarity m
forall (m :: * -> *). m Polarity -> LeastPolarity m
LeastPolarity (m Polarity -> LeastPolarity m) -> m Polarity -> LeastPolarity m
forall a b. (a -> b) -> a -> b
$ do
    m Polarity
mp m Polarity -> (Polarity -> m Polarity) -> m Polarity
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Polarity
Invariant  -> Polarity -> m Polarity
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Invariant  -- Shortcut for the absorbing element.
      Polarity
Nonvariant -> m Polarity
mq                -- The neutral element.
      Polarity
p          -> (Polarity
p Polarity -> Polarity -> Polarity
/\) (Polarity -> Polarity) -> m Polarity -> m Polarity
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Polarity
mq

instance Monad m => Monoid (LeastPolarity m) where
  mempty :: LeastPolarity m
mempty  = Polarity -> LeastPolarity m
forall el coll. Singleton el coll => el -> coll
singleton Polarity
Nonvariant
  mappend :: LeastPolarity m -> LeastPolarity m -> LeastPolarity m
mappend = LeastPolarity m -> LeastPolarity m -> LeastPolarity m
forall a. Semigroup a => a -> a -> a
(<>)

-- | Bind for 'LeastPolarity'.
(>>==) :: Monad m => m a -> (a -> LeastPolarity m) -> LeastPolarity m
m a
m >>== :: forall (m :: * -> *) a.
Monad m =>
m a -> (a -> LeastPolarity m) -> LeastPolarity m
>>== a -> LeastPolarity m
k = m Polarity -> LeastPolarity m
forall (m :: * -> *). m Polarity -> LeastPolarity m
LeastPolarity (m Polarity -> LeastPolarity m) -> m Polarity -> LeastPolarity m
forall a b. (a -> b) -> a -> b
$ m a
m m a -> (a -> m Polarity) -> m Polarity
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= LeastPolarity m -> m Polarity
forall (m :: * -> *). LeastPolarity m -> m Polarity
getLeastPolarity (LeastPolarity m -> m Polarity)
-> (a -> LeastPolarity m) -> a -> m Polarity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> LeastPolarity m
k

-- | @polarity' i p a@ computes the least polarity of de Bruijn index @i@
--   in syntactic entity @a@, where root occurrences count as @p@.
--
--   Ignores occurrences in sorts.
class HasPolarity a where
  polarity'
    :: (HasConstInfo m, MonadReduce m)
    => Nat -> Polarity -> a -> LeastPolarity m

  default polarity'
    :: (HasConstInfo m, MonadReduce m, HasPolarity b, Foldable t, t b ~ a)
    => Nat -> Polarity -> a -> LeastPolarity m
  polarity' Int
i = (b -> LeastPolarity m) -> a -> LeastPolarity m
(b -> LeastPolarity m) -> t b -> LeastPolarity m
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 -> LeastPolarity m) -> a -> LeastPolarity m)
-> (Polarity -> b -> LeastPolarity m)
-> Polarity
-> a
-> LeastPolarity m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Polarity -> b -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> b -> LeastPolarity m
polarity' Int
i

instance HasPolarity a => HasPolarity [a]
instance HasPolarity a => HasPolarity (Arg a)
instance HasPolarity a => HasPolarity (Dom a)
instance HasPolarity a => HasPolarity (Elim' a)
instance HasPolarity a => HasPolarity (Level' a)
instance HasPolarity a => HasPolarity (PlusLevel' a)

-- | Does not look into sort.
instance HasPolarity a => HasPolarity (Type'' t a)

instance (HasPolarity a, HasPolarity b) => HasPolarity (a, b) where
  polarity' :: forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> (a, b) -> LeastPolarity m
polarity' Int
i Polarity
p (a
x, b
y) = Int -> Polarity -> a -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
polarity' Int
i Polarity
p a
x LeastPolarity m -> LeastPolarity m -> LeastPolarity m
forall a. Semigroup a => a -> a -> a
<> Int -> Polarity -> b -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> b -> LeastPolarity m
polarity' Int
i Polarity
p b
y

instance HasPolarity a => HasPolarity (Abs a) where
  polarity' :: forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> Abs a -> LeastPolarity m
polarity' Int
i Polarity
p (Abs   [Char]
_ a
b) = Int -> Polarity -> a -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
polarity' (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Polarity
p a
b
  polarity' Int
i Polarity
p (NoAbs [Char]
_ a
v) = Int -> Polarity -> a -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
polarity' Int
i Polarity
p a
v

instance HasPolarity Term where
  polarity' :: forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> Term -> LeastPolarity m
polarity' Int
i Polarity
p Term
v = Term -> m Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v m Term -> (Term -> LeastPolarity m) -> LeastPolarity m
forall (m :: * -> *) a.
Monad m =>
m a -> (a -> LeastPolarity m) -> LeastPolarity m
>>== \case
    -- Andreas, 2012-09-06: taking the polarity' of the arguments
    -- without taking the variance of the function into account seems wrong.
    Var Int
n [Elim]
ts
      | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i    -> Polarity -> LeastPolarity m
forall el coll. Singleton el coll => el -> coll
singleton Polarity
p LeastPolarity m -> LeastPolarity m -> LeastPolarity m
forall a. Semigroup a => a -> a -> a
<> Int -> Polarity -> [Elim] -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> [Elim] -> LeastPolarity m
polarity' Int
i Polarity
Invariant [Elim]
ts
      | Bool
otherwise -> Int -> Polarity -> [Elim] -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> [Elim] -> LeastPolarity m
polarity' Int
i Polarity
Invariant [Elim]
ts
    Lam ArgInfo
_ Abs Term
t       -> Int -> Polarity -> Abs Term -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> Abs Term -> LeastPolarity m
polarity' Int
i Polarity
p Abs Term
t
    Lit Literal
_         -> LeastPolarity m
forall a. Monoid a => a
mempty
    Level Level
l       -> Int -> Polarity -> Level -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> Level -> LeastPolarity m
polarity' Int
i Polarity
p Level
l
    Def QName
x [Elim]
ts      -> QName -> m [Polarity]
forall (m :: * -> *). HasConstInfo m => QName -> m [Polarity]
getPolarity QName
x m [Polarity] -> ([Polarity] -> LeastPolarity m) -> LeastPolarity m
forall (m :: * -> *) a.
Monad m =>
m a -> (a -> LeastPolarity m) -> LeastPolarity m
>>== \ [Polarity]
pols ->
                       let ps :: [Polarity]
ps = (Polarity -> Polarity) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map (Polarity -> Polarity -> Polarity
composePol Polarity
p) [Polarity]
pols [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
++ Polarity -> [Polarity]
forall a. a -> [a]
repeat Polarity
Invariant
                       in  [LeastPolarity m] -> LeastPolarity m
forall a. Monoid a => [a] -> a
mconcat ([LeastPolarity m] -> LeastPolarity m)
-> [LeastPolarity m] -> LeastPolarity m
forall a b. (a -> b) -> a -> b
$ (Polarity -> Elim -> LeastPolarity m)
-> [Polarity] -> [Elim] -> [LeastPolarity m]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Int -> Polarity -> Elim -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> Elim -> LeastPolarity m
polarity' Int
i) [Polarity]
ps [Elim]
ts
    Con ConHead
_ ConInfo
_ [Elim]
ts    -> Int -> Polarity -> [Elim] -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> [Elim] -> LeastPolarity m
polarity' Int
i Polarity
p [Elim]
ts   -- Constructors can be seen as monotone in all args.
    Pi Dom Type
a Abs Type
b        -> Int -> Polarity -> Dom Type -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> Dom Type -> LeastPolarity m
polarity' Int
i (Polarity -> Polarity
neg Polarity
p) Dom Type
a LeastPolarity m -> LeastPolarity m -> LeastPolarity m
forall a. Semigroup a => a -> a -> a
<> Int -> Polarity -> Abs Type -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> Abs Type -> LeastPolarity m
polarity' Int
i Polarity
p Abs Type
b
    Sort Sort
s        -> LeastPolarity m
forall a. Monoid a => a
mempty -- polarity' i p s -- mempty
    MetaV MetaId
_ [Elim]
ts    -> Int -> Polarity -> [Elim] -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> [Elim] -> LeastPolarity m
polarity' Int
i Polarity
Invariant [Elim]
ts
    DontCare Term
t    -> Int -> Polarity -> Term -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> Term -> LeastPolarity m
polarity' Int
i Polarity
p Term
t -- mempty
    Dummy{}       -> LeastPolarity m
forall a. Monoid a => a
mempty