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
Nonvariant /\ :: Polarity -> Polarity -> Polarity
/\ b :: Polarity
b = Polarity
b
a :: Polarity
a /\ Nonvariant = Polarity
a
a :: Polarity
a /\ b :: 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 Covariant     = Polarity
Contravariant
neg Contravariant = Polarity
Covariant
neg Invariant     = Polarity
Invariant
neg Nonvariant    = Polarity
Nonvariant

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

polFromOcc :: Occurrence -> Polarity
polFromOcc :: Occurrence -> Polarity
polFromOcc o :: Occurrence
o = case Occurrence
o of
  GuardPos  -> Polarity
Covariant
  StrictPos -> Polarity
Covariant
  JustPos   -> Polarity
Covariant
  JustNeg   -> Polarity
Contravariant
  Mixed     -> Polarity
Invariant
  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 (p :: Polarity
p : ps :: [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 (\ p :: 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 x :: 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
$ \ def :: 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 "tc.polarity.set" 15 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
    "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]
++ " 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 xs :: [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
>= 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
$ \ x :: 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
$ \ def :: Definition
def -> do
  VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.polarity.set" 25 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "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 "tc.polarity.set" 15 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
    "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]
++ " 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 "tc.polarity.set" 15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    "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 "tc.polarity.set" 60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    "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 "tc.polarity.set" 10 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "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
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 def :: Defn
def pol :: [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
  _                         -> [Polarity]
pol
  where enable :: Int -> [Polarity]
enable np :: Int
np = let (pars :: [Polarity]
pars, rest :: [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 t :: Type
t _      []          = [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return []  -- all remaining are 'Invariant'
dependentPolarity t :: Type
t []     (_ : _)     = TCM [Polarity]
forall a. HasCallStack => a
__IMPOSSIBLE__
dependentPolarity t :: Type
t (q :: Polarity
q:qs :: [Polarity]
qs) pols :: [Polarity]
pols@(p :: Polarity
p:ps :: [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 "tc.polarity.dep" 20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ "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 "tc.polarity.dep" 70 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ "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 :: Dom Type
dom b :: 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
$ \ c :: 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 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
        _ -> 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
    _ -> [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 i :: Int
i t :: 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 i :: Int
i t :: Type
t (p :: Polarity
p:ps :: [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 a :: Dom Type
a b :: 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
+ 1) (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b) [Polarity]
ps
    _ -> 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 d :: QName
d pol0 :: [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 tel :: Tele (Dom Type)
tel _      = Type -> TelV Type
telView' (Type -> TelV Type) -> Type -> TelV Type
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
            (parTel :: [Dom (VerboseKey, Type)]
parTel, ixTel :: [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 = (_,a :: Type
a)} : _ -> 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 c :: 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 conTel :: Tele (Dom Type)
conTel target :: 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
                      EmptyTel  -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False  -- no size argument
                      ExtendTel arg :: Dom Type
arg  tel :: 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
$ \ tel :: 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 [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 "tc.polarity.size" 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
$ "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 "tc.polarity.size" 15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
                            "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 "passes" else "fails") TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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
$ \ occ :: [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
      _ -> 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 d :: QName
d i :: Int
i a :: Type
a = do
  VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc "tc.polarity.size" 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
    [ "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
    , "  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
    , "  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 d0 :: QName
d0 es :: 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 (pars :: Elims
pars, Apply ix :: Arg Term
ix : ixs :: 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 j :: Int
j _ | 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)
        _ -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    _ -> 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 i :: Int
i x :: 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
    ps :: [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 i :: 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 i :: 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 i :: Int
i (Abs   _ b :: 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
+ 1) a
b
  polarities i :: Int
i (NoAbs _ v :: 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 i :: Int
i xs :: [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 i :: Int
i (x :: a
x, y :: 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 i :: Int
i (El _ v :: 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 i :: Int
i Proj{}    = [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return []
  polarities i :: Int
i (Apply a :: Arg a
a) = Int -> Arg a -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Arg a
a
  polarities i :: Int
i (IApply x :: a
x y :: a
y a :: 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 i :: Int
i v :: 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 n :: Int
n ts :: 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 _ t :: Abs Term
t    -> Int -> Abs Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Abs Term
t
    Lit _      -> [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Level l :: Level
l    -> Int -> Level -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Level
l
    Def x :: QName
x ts :: Elims
ts   -> do
      [Polarity]
pols <- QName -> TCM [Polarity]
forall (m :: * -> *). HasConstInfo m => QName -> m [Polarity]
getPolarity QName
x
      let compose :: Polarity -> [Polarity] -> [Polarity]
compose p :: Polarity
p ps :: [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 -> 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 -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i) Elims
ts
    Con _ _ ts :: 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 a :: Dom Type
a b :: 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 s :: Sort
s     -> [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- polarities i s -- return []
    MetaV _ ts :: 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 t :: 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 i :: Int
i (Max _ as :: [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 i :: Int
i (Plus _ l :: 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 i :: Int
i l :: LevelAtom' Term
l = case LevelAtom' Term
l of
    MetaLevel _ vs :: 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 _ v :: Term
v -> Int -> Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Term
v
    NeutralLevel _ v :: Term
v -> Int -> Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Term
v
    UnreducedLevel v :: Term
v -> Int -> Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Term
v