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

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 (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
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 (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
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)
isSizeType (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom)) (Polarity -> m Polarity
forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
p) (Polarity -> m Polarity
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 (m :: * -> *) a. Monad m => a -> m a
return Polarity
Invariant)
            {- else -} m Polarity
fallback
        Abs Type
_ -> m Polarity
fallback
      [Polarity] -> m [Polarity]
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 (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 (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 (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 (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 (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)
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
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
`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
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 (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)
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
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
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 (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 (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 (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
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
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
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 (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 (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
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 (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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Polarity
Invariant  -> Polarity -> m Polarity
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 (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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
polarity' Int
i Polarity
p Term
t -- mempty
    Dummy{}       -> LeastPolarity m
forall a. Monoid a => a
mempty