module Agda.TypeChecking.Polarity where

import Control.Monad.State

import Data.Maybe

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.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 Occurrence
o = case Occurrence
o of
  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 :: QName -> TCM ()
polarityFromPositivity :: QName -> TCM ()
polarityFromPositivity QName
x = QName -> (Definition -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
x ((Definition -> TCM ()) -> TCM ())
-> (Definition -> TCM ()) -> TCM ()
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)
  VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.polarity.set" Int
15 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
    VerboseKey
"Polarity of " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
x VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" from positivity: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [Polarity] -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow [Polarity]
pol0

  -- set the polarity in the signature (not the final polarity, though)
  QName -> [Polarity] -> TCM ()
setPolarity QName
x ([Polarity] -> TCM ()) -> [Polarity] -> TCM ()
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 :: [QName] -> TCM ()
computePolarity :: [QName] -> TCM ()
computePolarity [QName]
xs = do

 -- Andreas, 2017-04-26, issue #2554
 -- First, for mutual definitions, obtain a crude polarity from positivity.
 Bool -> TCM () -> TCM ()
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) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ (QName -> TCM ()) -> [QName] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ QName -> TCM ()
polarityFromPositivity [QName]
xs

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

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

  -- set the polarity in the signature
  QName -> [Polarity] -> TCM ()
setPolarity QName
x ([Polarity] -> TCM ()) -> [Polarity] -> TCM ()
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 :: Type -> [Polarity] -> [Polarity] -> TCM [Polarity]
dependentPolarity :: Type -> [Polarity] -> [Polarity] -> TCM [Polarity]
dependentPolarity Type
t [Polarity]
_      []          = [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return []  -- all remaining are 'Invariant'
dependentPolarity Type
t []     (Polarity
_ : [Polarity]
_)     = TCM [Polarity]
forall a. HasCallStack => a
__IMPOSSIBLE__
dependentPolarity Type
t (Polarity
q:[Polarity]
qs) pols :: [Polarity]
pols@(Polarity
p:[Polarity]
ps) = do
  Term
t <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Type -> Term
forall t a. Type'' t a -> a
unEl Type
t
  VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.polarity.dep" Int
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"dependentPolarity t = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t
  VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.polarity.dep" Int
70 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"dependentPolarity t = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> (Term -> VerboseKey) -> Term -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> VerboseKey
forall a. Show a => a -> VerboseKey
show) Term
t
  case Term
t of
    Pi Dom Type
dom Abs Type
b -> do
      [Polarity]
ps <- Dom Type -> Abs Type -> (Type -> TCM [Polarity]) -> TCM [Polarity]
forall t a (m :: * -> *) b.
(Subst t a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
dom Abs Type
b ((Type -> TCM [Polarity]) -> TCM [Polarity])
-> (Type -> TCM [Polarity]) -> TCM [Polarity]
forall a b. (a -> b) -> a -> b
$ \ Type
c -> Type -> [Polarity] -> [Polarity] -> TCM [Polarity]
dependentPolarity Type
c [Polarity]
qs [Polarity]
ps
      let fallback :: TCMT IO Polarity
fallback = TCMT IO Bool
-> TCMT IO Polarity -> TCMT IO Polarity -> TCMT IO 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)
-> TCMT IO (Maybe BoundedSize) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO (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 -> TCMT IO Polarity
forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
p) (Polarity -> TCMT IO 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!
          TCMT IO Bool
-> TCMT IO Polarity -> TCMT IO Polarity -> TCMT IO Polarity
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Int -> Type -> [Polarity] -> TCMT IO Bool
relevantInIgnoringNonvariant Int
0 (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b) [Polarity]
ps)
            {- then -} (Polarity -> TCMT IO Polarity
forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Invariant)
            {- else -} TCMT IO Polarity
fallback
        Abs Type
_ -> TCMT IO Polarity
fallback
      [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Polarity] -> TCM [Polarity]) -> [Polarity] -> TCM [Polarity]
forall a b. (a -> b) -> a -> b
$ Polarity
p Polarity -> [Polarity] -> [Polarity]
forall a. a -> [a] -> [a]
: [Polarity]
ps
    Term
_ -> [Polarity] -> TCM [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 :: Nat -> Type -> [Polarity] -> TCM Bool
relevantInIgnoringNonvariant :: Int -> Type -> [Polarity] -> TCMT IO Bool
relevantInIgnoringNonvariant Int
i Type
t []     = Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO 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) = do
  Term
t <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Type -> Term
forall t a. Type'' t a -> a
unEl Type
t
  case Term
t of
    Pi 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 -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
              else Int -> Type -> [Polarity] -> TCMT IO Bool
relevantInIgnoringNonvariant (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b) [Polarity]
ps
    Term
_ -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Term -> Bool
forall t. Free t => Int -> t -> Bool
`relevantInIgnoringSortAnn` Term
t

------------------------------------------------------------------------
-- * 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 :: QName -> [Polarity] -> TCM [Polarity]
sizePolarity :: QName -> [Polarity] -> TCM [Polarity]
sizePolarity QName
d [Polarity]
pol0 = do
  let exit :: TCM [Polarity]
exit = [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return [Polarity]
pol0
  TCMT IO Bool -> TCM [Polarity] -> TCM [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
sizedTypesOption TCM [Polarity]
exit (TCM [Polarity] -> TCM [Polarity])
-> TCM [Polarity] -> TCM [Polarity]
forall a b. (a -> b) -> a -> b
$ {- else -} do
    Definition
def <- QName -> TCMT IO 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 (VerboseKey, Type)]
parTel, [Dom (VerboseKey, Type)]
ixTel) = Int
-> [Dom (VerboseKey, Type)]
-> ([Dom (VerboseKey, Type)], [Dom (VerboseKey, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
np ([Dom (VerboseKey, Type)]
 -> ([Dom (VerboseKey, Type)], [Dom (VerboseKey, Type)]))
-> [Dom (VerboseKey, Type)]
-> ([Dom (VerboseKey, Type)], [Dom (VerboseKey, Type)])
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Tele (Dom Type)
tel
        case [Dom (VerboseKey, Type)]
ixTel of
          []                 -> TCM [Polarity]
exit  -- No size index
          Dom{unDom :: forall t e. Dom' t e -> e
unDom = (VerboseKey
_,Type
a)} : [Dom (VerboseKey, Type)]
_ -> TCMT IO Bool -> TCM [Polarity] -> TCM [Polarity] -> TCM [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)
-> TCMT IO (Maybe BoundedSize) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Type
a) TCM [Polarity]
exit (TCM [Polarity] -> TCM [Polarity])
-> TCM [Polarity] -> TCM [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] -> TCM ()
setPolarity QName
d ([Polarity] -> TCM ()) -> [Polarity] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Polarity]
polCo
            -- and seek confirm it by looking at the constructor types
            let check :: QName -> TCMT IO Bool
check QName
c = do
                  Type
t <- Definition -> Type
defType (Definition -> Type) -> TCMT IO Definition -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
                  Tele (Dom Type) -> TCMT IO Bool -> TCMT IO Bool
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([Dom (VerboseKey, Type)] -> Tele (Dom Type)
telFromList [Dom (VerboseKey, Type)]
parTel) (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO 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 -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Type -> TCMT IO (TelV Type))
-> TCMT IO Type -> TCMT IO (TelV Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Type
t Type -> [Arg Term] -> TCMT IO Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m) =>
Type -> a -> m Type
`piApplyM` [Arg Term]
pars)
                    case Tele (Dom Type)
conTel of
                      Tele (Dom Type)
EmptyTel  -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False  -- no size argument
                      ExtendTel Dom Type
arg  Abs (Tele (Dom Type))
tel ->
                        TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
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)
-> TCMT IO (Maybe BoundedSize) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO (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
arg)) (Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ do -- also no size argument
                          -- First constructor argument has type Size

                          -- check that only positive occurences in tel
                          let isPos :: TCMT IO Bool
isPos = Dom Type
-> Abs (Tele (Dom Type))
-> (Tele (Dom Type) -> TCMT IO Bool)
-> TCMT IO Bool
forall t a (m :: * -> *) b.
(Subst t a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
arg Abs (Tele (Dom Type))
tel ((Tele (Dom Type) -> TCMT IO Bool) -> TCMT IO Bool)
-> (Tele (Dom Type) -> TCMT IO Bool) -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ \ Tele (Dom Type)
tel -> do
                                [Polarity]
pols <- (Int -> Type -> TCMT IO Polarity)
-> [Int] -> [Type] -> TCM [Polarity]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Int -> Type -> TCMT IO Polarity
forall a. HasPolarity a => Int -> a -> TCMT IO Polarity
polarity [Int
0..] ([Type] -> TCM [Polarity]) -> [Type] -> TCM [Polarity]
forall a b. (a -> b) -> a -> b
$ (Dom (VerboseKey, Type) -> Type)
-> [Dom (VerboseKey, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ((VerboseKey, Type) -> Type
forall a b. (a, b) -> b
snd ((VerboseKey, Type) -> Type)
-> (Dom (VerboseKey, Type) -> (VerboseKey, Type))
-> Dom (VerboseKey, Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (VerboseKey, Type) -> (VerboseKey, Type)
forall t e. Dom' t e -> e
unDom) ([Dom (VerboseKey, Type)] -> [Type])
-> [Dom (VerboseKey, Type)] -> [Type]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Tele (Dom Type)
tel
                                VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.polarity.size" Int
25 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
                                  VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"to pass size polarity check, the following polarities need all to be covariant: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [Polarity] -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow [Polarity]
pols
                                Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ (Polarity -> Bool) -> [Polarity] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Polarity -> [Polarity] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Polarity
Nonvariant, Polarity
Covariant]) [Polarity]
pols

                          -- check that the size argument appears in the
                          -- right spot in the target type
                          let sizeArg :: Int
sizeArg = Abs (Tele (Dom Type)) -> Int
forall a. Sized a => a -> Int
size Abs (Tele (Dom Type))
tel
                              isLin :: TCMT IO Bool
isLin = Tele (Dom Type) -> TCMT IO Bool -> TCMT IO Bool
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
conTel (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ QName -> Int -> Type -> TCMT IO Bool
checkSizeIndex QName
d Int
sizeArg Type
target

                          Bool
ok <- TCMT IO Bool
isPos TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` TCMT IO Bool
isLin
                          VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.polarity.size" Int
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
                            TCM Doc
"constructor" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                            VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (if Bool
ok then VerboseKey
"passes" else VerboseKey
"fails") TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                            TCM Doc
"size polarity check"
                          Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok

            TCMT IO Bool -> TCM [Polarity] -> TCM [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM ([TCMT IO Bool] -> TCMT IO Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM ([TCMT IO Bool] -> TCMT IO Bool) -> [TCMT IO Bool] -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ (QName -> TCMT IO Bool) -> [QName] -> [TCMT IO Bool]
forall a b. (a -> b) -> [a] -> [b]
map QName -> TCMT IO Bool
check [QName]
cons)
                ([Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return [Polarity]
polIn) -- no, does not conform to the rules of sized types
              (TCM [Polarity] -> TCM [Polarity])
-> TCM [Polarity] -> TCM [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]) -> TCM ()
modifyArgOccurrences QName
d (([Occurrence] -> [Occurrence]) -> TCM ())
-> ([Occurrence] -> [Occurrence]) -> TCM ()
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] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return [Polarity]
polCo
      Defn
_ -> TCM [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 :: QName -> Nat -> Type -> TCM Bool
checkSizeIndex :: QName -> Int -> Type -> TCMT IO Bool
checkSizeIndex QName
d Int
i Type
a = do
  VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.polarity.size" Int
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc -> TCM Doc
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ TCM Doc
"checking that constructor target type " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
    , TCM Doc
"  is data type " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
    , TCM Doc
"  and has size index (successor(s) of) " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM 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 Elims
es -> do
      TCMT IO (Maybe QName) -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m (Maybe a) -> m () -> m ()
whenNothingM (QName -> QName -> TCMT IO (Maybe QName)
forall (m :: * -> *).
HasConstInfo m =>
QName -> QName -> m (Maybe QName)
sameDef QName
d QName
d0) TCM ()
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) -> TCMT IO (Maybe Int) -> TCMT IO Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Maybe Int)
getNumberOfParameters QName
d0
      let (Elims
pars, Apply Arg Term
ix : Elims
ixs) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
np Elims
es
      DeepSizeView
s <- Term -> TCM DeepSizeView
deepSizeView (Term -> TCM DeepSizeView) -> Term -> TCM 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 Int
j Int
_ | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j
          -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Bool
forall t. Free t => Int -> t -> Bool
freeIn Int
i (Elims
pars Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
ixs)
        DeepSizeView
_ -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Term
_ -> TCMT IO Bool
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | @polarities i a@ computes the list of polarities of de Bruijn index @i@
--   in syntactic entity @a@.
class HasPolarity a where
  polarities :: Nat -> a -> TCM [Polarity]

-- | @polarity i a@ computes the polarity of de Bruijn index @i@
--   in syntactic entity @a@ by taking the infimum of all 'polarities'.
polarity :: HasPolarity a => Nat -> a -> TCM Polarity
polarity :: Int -> a -> TCMT IO Polarity
polarity Int
i a
x = do
  [Polarity]
ps <- Int -> a -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i a
x
  case [Polarity]
ps of
    [] -> Polarity -> TCMT IO Polarity
forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Nonvariant
    [Polarity]
ps -> Polarity -> TCMT IO Polarity
forall (m :: * -> *) a. Monad m => a -> m a
return (Polarity -> TCMT IO Polarity) -> Polarity -> TCMT IO Polarity
forall a b. (a -> b) -> a -> b
$ (Polarity -> Polarity -> Polarity) -> [Polarity] -> Polarity
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Polarity -> Polarity -> Polarity
(/\) [Polarity]
ps

instance HasPolarity a => HasPolarity (Arg a) where
  polarities :: Int -> Arg a -> TCM [Polarity]
polarities Int
i = Int -> a -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i (a -> TCM [Polarity]) -> (Arg a -> a) -> Arg a -> TCM [Polarity]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg a -> a
forall e. Arg e -> e
unArg

instance HasPolarity a => HasPolarity (Dom a) where
  polarities :: Int -> Dom a -> TCM [Polarity]
polarities Int
i = Int -> a -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i (a -> TCM [Polarity]) -> (Dom a -> a) -> Dom a -> TCM [Polarity]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom a -> a
forall t e. Dom' t e -> e
unDom

instance HasPolarity a => HasPolarity (Abs a) where
  polarities :: Int -> Abs a -> TCM [Polarity]
polarities Int
i (Abs   VerboseKey
_ a
b) = Int -> a -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) a
b
  polarities Int
i (NoAbs VerboseKey
_ a
v) = Int -> a -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i a
v

instance HasPolarity a => HasPolarity [a] where
  polarities :: Int -> [a] -> TCM [Polarity]
polarities Int
i [a]
xs = [[Polarity]] -> [Polarity]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Polarity]] -> [Polarity])
-> TCMT IO [[Polarity]] -> TCM [Polarity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> TCM [Polarity]) -> [a] -> TCMT IO [[Polarity]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int -> a -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i) [a]
xs

instance (HasPolarity a, HasPolarity b) => HasPolarity (a, b) where
  polarities :: Int -> (a, b) -> TCM [Polarity]
polarities Int
i (a
x, b
y) = [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
(++) ([Polarity] -> [Polarity] -> [Polarity])
-> TCM [Polarity] -> TCMT IO ([Polarity] -> [Polarity])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> a -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i a
x TCMT IO ([Polarity] -> [Polarity])
-> TCM [Polarity] -> TCM [Polarity]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> b -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i b
y

instance HasPolarity Type where
  polarities :: Int -> Type -> TCM [Polarity]
polarities Int
i (El Sort' Term
_ Term
v) = Int -> Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Term
v

instance HasPolarity a => HasPolarity (Elim' a) where
  polarities :: Int -> Elim' a -> TCM [Polarity]
polarities Int
i Proj{}    = [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return []
  polarities Int
i (Apply Arg a
a) = Int -> Arg a -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Arg a
a
  polarities Int
i (IApply a
x a
y a
a) = Int -> (a, (a, a)) -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i (a
x,(a
y,a
a))

instance HasPolarity Term where
  polarities :: Int -> Term -> TCM [Polarity]
polarities Int
i Term
v = do
   Term
v <- Term -> TCMT IO Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v
   case Term
v of
    -- Andreas, 2012-09-06: taking the polarities of the arguments
    -- without taking the variance of the function into account seems wrong.
    Var Int
n Elims
ts  | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i -> (Polarity
Covariant Polarity -> [Polarity] -> [Polarity]
forall a. a -> [a] -> [a]
:) ([Polarity] -> [Polarity])
-> ([Polarity] -> [Polarity]) -> [Polarity] -> [Polarity]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Polarity -> Polarity) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map (Polarity -> Polarity -> Polarity
forall a b. a -> b -> a
const Polarity
Invariant) ([Polarity] -> [Polarity]) -> TCM [Polarity] -> TCM [Polarity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Elims -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Elims
ts
              | Bool
otherwise -> (Polarity -> Polarity) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map (Polarity -> Polarity -> Polarity
forall a b. a -> b -> a
const Polarity
Invariant) ([Polarity] -> [Polarity]) -> TCM [Polarity] -> TCM [Polarity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Elims -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Elims
ts
    Lam ArgInfo
_ Abs Term
t    -> Int -> Abs Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Abs Term
t
    Lit Literal
_      -> [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Level Level
l    -> Int -> Level -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Level
l
    Def QName
x Elims
ts   -> do
      [Polarity]
pols <- QName -> TCM [Polarity]
forall (m :: * -> *). HasConstInfo m => QName -> m [Polarity]
getPolarity QName
x
      let compose :: Polarity -> [Polarity] -> [Polarity]
compose Polarity
p [Polarity]
ps = (Polarity -> Polarity) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map (Polarity -> Polarity -> Polarity
composePol Polarity
p) [Polarity]
ps
      [[Polarity]] -> [Polarity]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Polarity]] -> [Polarity])
-> ([[Polarity]] -> [[Polarity]]) -> [[Polarity]] -> [Polarity]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Polarity -> [Polarity] -> [Polarity])
-> [Polarity] -> [[Polarity]] -> [[Polarity]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Polarity -> [Polarity] -> [Polarity]
compose ([Polarity]
pols [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
++ Polarity -> [Polarity]
forall a. a -> [a]
repeat Polarity
Invariant) ([[Polarity]] -> [Polarity])
-> TCMT IO [[Polarity]] -> TCM [Polarity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Elim' Term -> TCM [Polarity]) -> Elims -> TCMT IO [[Polarity]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int -> Elim' Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i) Elims
ts
    Con ConHead
_ ConInfo
_ Elims
ts -> Int -> Elims -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Elims
ts -- constructors can be seen as monotone in all args.
    Pi Dom Type
a Abs Type
b     -> [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
(++) ([Polarity] -> [Polarity] -> [Polarity])
-> TCM [Polarity] -> TCMT IO ([Polarity] -> [Polarity])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Polarity -> Polarity) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map Polarity -> Polarity
neg ([Polarity] -> [Polarity]) -> TCM [Polarity] -> TCM [Polarity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Dom Type -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Dom Type
a) TCMT IO ([Polarity] -> [Polarity])
-> TCM [Polarity] -> TCM [Polarity]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> Abs Type -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Abs Type
b
    Sort Sort' Term
s     -> [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- polarities i s -- return []
    MetaV MetaId
_ Elims
ts -> (Polarity -> Polarity) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map (Polarity -> Polarity -> Polarity
forall a b. a -> b -> a
const Polarity
Invariant) ([Polarity] -> [Polarity]) -> TCM [Polarity] -> TCM [Polarity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Elims -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Elims
ts
    DontCare Term
t -> Int -> Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Term
t -- return []
    Dummy{}    -> [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return []

instance HasPolarity Level where
  polarities :: Int -> Level -> TCM [Polarity]
polarities Int
i (Max Integer
_ [PlusLevel' Term]
as) = Int -> [PlusLevel' Term] -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i [PlusLevel' Term]
as

instance HasPolarity PlusLevel where
  polarities :: Int -> PlusLevel' Term -> TCM [Polarity]
polarities Int
i (Plus Integer
_ LevelAtom' Term
l) = Int -> LevelAtom' Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i LevelAtom' Term
l

instance HasPolarity LevelAtom where
  polarities :: Int -> LevelAtom' Term -> TCM [Polarity]
polarities Int
i LevelAtom' Term
l = case LevelAtom' Term
l of
    MetaLevel MetaId
_ Elims
vs   -> (Polarity -> Polarity) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map (Polarity -> Polarity -> Polarity
forall a b. a -> b -> a
const Polarity
Invariant) ([Polarity] -> [Polarity]) -> TCM [Polarity] -> TCM [Polarity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Elims -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Elims
vs
    BlockedLevel MetaId
_ Term
v -> Int -> Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Term
v
    NeutralLevel NotBlocked
_ Term
v -> Int -> Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Term
v
    UnreducedLevel Term
v -> Int -> Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Term
v