-- | 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 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 = forall a b. (a -> b) -> [a] -> [b]
map (\ Polarity
p -> if Polarity
p 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 = forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
x 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 = forall a. Int -> a -> [a]
replicate Int
npars Polarity
Nonvariant forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> Polarity
polFromOcc (Definition -> [Occurrence]
defArgOccurrences Definition
def)
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.polarity.set" Int
15 forall a b. (a -> b) -> a -> b
$
    [Char]
"Polarity of " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
x forall a. [a] -> [a] -> [a]
++ [Char]
" from positivity: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow [Polarity]
pol0

  -- set the polarity in the signature (not the final polarity, though)
  forall (m :: * -> *).
(MonadTCState m, MonadDebug m) =>
QName -> [Polarity] -> m ()
setPolarity QName
x forall a b. (a -> b) -> a -> b
$ 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.
 forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
xs forall a. Ord a => a -> a -> Bool
>= Int
2) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall (m :: * -> *).
(HasConstInfo m, MonadTCEnv m, MonadTCState m, MonadDebug m) =>
QName -> m ()
polarityFromPositivity [QName]
xs

 -- Then, refine it.
 forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [QName]
xs forall a b. (a -> b) -> a -> b
$ \ QName
x -> forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
x forall a b. (a -> b) -> a -> b
$ \ Definition
def -> do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.polarity.set" Int
25 forall a b. (a -> b) -> a -> b
$ [Char]
"Refining polarity of " forall a. [a] -> [a] -> [a]
++ 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 = forall a. Int -> a -> [a]
replicate Int
npars Polarity
Nonvariant forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> Polarity
polFromOcc (Definition -> [Occurrence]
defArgOccurrences Definition
def)
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.polarity.set" Int
15 forall a b. (a -> b) -> a -> b
$
    [Char]
"Polarity of " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
x forall a. [a] -> [a] -> [a]
++ [Char]
" from positivity: " forall a. [a] -> [a] -> [a]
++ 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 <- 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.
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.set" Int
15 forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Refining polarity with type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.set" Int
60 forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Refining polarity with type (raw): " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
.forall a. Show a => a -> [Char]
show) Type
t

  [Polarity]
pol <- 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
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.polarity.set" Int
10 forall a b. (a -> b) -> a -> b
$ [Char]
"Polarity of " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
x forall a. [a] -> [a] -> [a]
++ [Char]
": " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow [Polarity]
pol

  -- set the polarity in the signature
  forall (m :: * -> *).
(MonadTCState m, MonadDebug m) =>
QName -> [Polarity] -> m ()
setPolarity QName
x forall a b. (a -> b) -> a -> b
$ 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) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
np [Polarity]
pol
                    in  [Polarity] -> [Polarity]
purgeNonvariant [Polarity]
pars 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]
_      []          = forall (m :: * -> *) a. Monad m => a -> m a
return []  -- all remaining are 'Invariant'
dependentPolarity Type
t []     (Polarity
_ : [Polarity]
_)     = forall a. HasCallStack => a
__IMPOSSIBLE__
dependentPolarity Type
t (Polarity
q:[Polarity]
qs) pols :: [Polarity]
pols@(Polarity
p:[Polarity]
ps) = do
  Term
t <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall t a. Type'' t a -> a
unEl Type
t
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.dep" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"dependentPolarity t = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.dep" Int
70 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"dependentPolarity t = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) Term
t
  case Term
t of
    Pi Dom Type
dom Abs Type
b -> do
      [Polarity]
ps <- forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
dom Abs Type
b forall a b. (a -> b) -> a -> b
$ \ Type
c -> 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 = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType (forall t e. Dom' t e -> e
unDom Dom Type
dom)) (forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
p) (forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
q)
      Polarity
p <- case Abs Type
b of
        Abs{} | Polarity
p 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!
          forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *).
MonadReduce m =>
Int -> Type -> [Polarity] -> m Bool
relevantInIgnoringNonvariant Int
0 (forall a. Subst a => Abs a -> a
absBody Abs Type
b) [Polarity]
ps)
            {- then -} (forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Invariant)
            {- else -} m Polarity
fallback
        Abs Type
_ -> m Polarity
fallback
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Polarity
p forall a. a -> [a] -> [a]
: [Polarity]
ps
    Term
_ -> 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 []     = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int
i forall t. Free t => Int -> t -> Bool
`relevantInIgnoringSortAnn` Type
t
relevantInIgnoringNonvariant Int
i Type
t (Polarity
p:[Polarity]
ps) =
  forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPiType Type
t
    {-then-} (\ Type
t -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int
i forall t. Free t => Int -> t -> Bool
`relevantInIgnoringSortAnn` Type
t) forall a b. (a -> b) -> a -> b
$
    {-else-} \ Dom Type
a Abs Type
b ->
      if Polarity
p forall a. Eq a => a -> a -> Bool
/= Polarity
Nonvariant Bool -> Bool -> Bool
&& Int
i forall t. Free t => Int -> t -> Bool
`relevantInIgnoringSortAnn` Dom Type
a
        then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        else forall (m :: * -> *).
MonadReduce m =>
Int -> Type -> [Polarity] -> m Bool
relevantInIgnoringNonvariant (Int
i forall a. Num a => a -> a -> a
+ Int
1) (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 = forall (m :: * -> *) a. Monad m => a -> m a
return [Polarity]
pol0
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM forall (m :: * -> *). HasOptions m => m Bool
sizedTypesOption m [Polarity]
exit forall a b. (a -> b) -> a -> b
$ {- else -} do
    Definition
def <- 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' forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
            ([Dom ([Char], Type)]
parTel, [Dom ([Char], Type)]
ixTel) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
np forall a b. (a -> b) -> a -> b
$ 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)]
_ -> forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((forall a. Eq a => a -> a -> Bool
/= forall a. a -> Maybe a
Just BoundedSize
BoundedNo) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Type
a) m [Polarity]
exit forall a b. (a -> b) -> a -> b
$ do
            -- we assume the size index to be 'Covariant' ...
            let pol :: [Polarity]
pol   = forall a. Int -> [a] -> [a]
take Int
np [Polarity]
pol0
                polCo :: [Polarity]
polCo = [Polarity]
pol forall a. [a] -> [a] -> [a]
++ [Polarity
Covariant]
                polIn :: [Polarity]
polIn = [Polarity]
pol forall a. [a] -> [a] -> [a]
++ [Polarity
Invariant]
            forall (m :: * -> *).
(MonadTCState m, MonadDebug m) =>
QName -> [Polarity] -> m ()
setPolarity QName
d 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
                  forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([Dom ([Char], Type)] -> Tele (Dom Type)
telFromList [Dom ([Char], Type)]
parTel) forall a b. (a -> b) -> a -> b
$ do
                    let pars :: [Arg Term]
pars = forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Arg a
defaultArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var) forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom Int
np
                    TelV Tele (Dom Type)
conTel Type
target <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Type
t forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> 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
                    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.size" Int
15 forall a b. (a -> b) -> a -> b
$
                      TCMT IO Doc
"constructor" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"fails size polarity check"
                    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 <- forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Dom Type
dom
                    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 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 forall a. Eq a => a -> a -> Bool
/= 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 = forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
                        Bool
isLin <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> a -> m Polarity
polarity [Int
0..] forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel
                          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.size" Int
25 forall a b. (a -> b) -> a -> b
$
                            forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"to pass size polarity check, the following polarities need all to be covariant: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow [Polarity]
pols
                          if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Polarity
Nonvariant, Polarity
Covariant]) [Polarity]
pols then m Bool
continue else do
                            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.size" Int
15 forall a b. (a -> b) -> a -> b
$
                              TCMT IO Doc
"constructor" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"passes size polarity check"
                            forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

            forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map QName -> m Bool
check [QName]
cons)
                (forall (m :: * -> *) a. Monad m => a -> m a
return [Polarity]
polIn) -- no, does not conform to the rules of sized types
              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).
                forall (m :: * -> *).
MonadTCState m =>
QName -> ([Occurrence] -> [Occurrence]) -> m ()
modifyArgOccurrences QName
d forall a b. (a -> b) -> a -> b
$ \ [Occurrence]
occ -> forall a. Int -> [a] -> [a]
take Int
np [Occurrence]
occ forall a. [a] -> [a] -> [a]
++ [Occurrence
JustPos]
                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
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.size" Int
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"checking that constructor target type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
    , TCMT IO Doc
"  is data type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
    , TCMT IO Doc
"  and has size index (successor(s) of) " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> Term
var Int
i)
    ]
  case forall t a. Type'' t a -> a
unEl Type
a of
    Def QName
d0 [Elim]
es -> do
      forall (m :: * -> *) a. Monad m => m (Maybe a) -> m () -> m ()
whenNothingM (forall (m :: * -> *).
HasConstInfo m =>
QName -> QName -> m (Maybe QName)
sameDef QName
d QName
d0) forall a. HasCallStack => a
__IMPOSSIBLE__
      Int
np <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Int)
getNumberOfParameters QName
d0
      let ([Elim]
pars, Apply Arg Term
ix : [Elim]
ixs) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
np [Elim]
es
      DeepSizeView
s <- forall (m :: * -> *).
(PureTCM m, MonadTCError m) =>
Term -> m DeepSizeView
deepSizeView forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
ix
      case DeepSizeView
s of
        DSizeVar (ProjectedVar Int
j []) Int
_ | Int
i forall a. Eq a => a -> a -> Bool
== Int
j
          -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall t. Free t => Int -> t -> Bool
freeIn Int
i ([Elim]
pars forall a. [a] -> [a] -> [a]
++ [Elim]
ixs)
        DeepSizeView
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Term
_ -> 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 = forall (m :: * -> *). LeastPolarity m -> m Polarity
getLeastPolarity forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(HasPolarity a, 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 = forall (m :: * -> *). m Polarity -> LeastPolarity m
LeastPolarity forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (m :: * -> *). m Polarity -> LeastPolarity m
LeastPolarity forall a b. (a -> b) -> a -> b
$ do
    m Polarity
mp forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Polarity
Invariant  -> 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
/\) 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  = forall el coll. Singleton el coll => el -> coll
singleton Polarity
Nonvariant
  mappend :: LeastPolarity m -> LeastPolarity m -> LeastPolarity m
mappend = 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 = forall (m :: * -> *). m Polarity -> LeastPolarity m
LeastPolarity forall a b. (a -> b) -> a -> b
$ m a
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *). LeastPolarity m -> m Polarity
getLeastPolarity 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 = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> 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) = forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
polarity' Int
i Polarity
p a
x forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> 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) = forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
polarity' (Int
i forall a. Num a => a -> a -> a
+ Int
1) Polarity
p a
b
  polarity' Int
i Polarity
p (NoAbs [Char]
_ a
v) = forall a (m :: * -> *).
(HasPolarity a, 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 = forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v 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 forall a. Eq a => a -> a -> Bool
== Int
i    -> forall el coll. Singleton el coll => el -> coll
singleton Polarity
p forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
polarity' Int
i Polarity
Invariant [Elim]
ts
      | Bool
otherwise -> forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
polarity' Int
i Polarity
Invariant [Elim]
ts
    Lam ArgInfo
_ Abs Term
t       -> forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
polarity' Int
i Polarity
p Abs Term
t
    Lit Literal
_         -> forall a. Monoid a => a
mempty
    Level Level
l       -> forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
polarity' Int
i Polarity
p Level
l
    Def QName
x [Elim]
ts      -> forall (m :: * -> *). HasConstInfo m => QName -> m [Polarity]
getPolarity QName
x forall (m :: * -> *) a.
Monad m =>
m a -> (a -> LeastPolarity m) -> LeastPolarity m
>>== \ [Polarity]
pols ->
                       let ps :: [Polarity]
ps = forall a b. (a -> b) -> [a] -> [b]
map (Polarity -> Polarity -> Polarity
composePol Polarity
p) [Polarity]
pols forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat Polarity
Invariant
                       in  forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
polarity' Int
i) [Polarity]
ps [Elim]
ts
    Con ConHead
_ ConInfo
_ [Elim]
ts    -> forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> 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        -> forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
polarity' Int
i (Polarity -> Polarity
neg Polarity
p) Dom Type
a forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
polarity' Int
i Polarity
p Abs Type
b
    Sort Sort
s        -> forall a. Monoid a => a
mempty -- polarity' i p s -- mempty
    MetaV MetaId
_ [Elim]
ts    -> forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
polarity' Int
i Polarity
Invariant [Elim]
ts
    DontCare Term
t    -> forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
polarity' Int
i Polarity
p Term
t -- mempty
    Dummy{}       -> forall a. Monoid a => a
mempty