{-# LANGUAGE MagicHash #-}

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

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

import Prelude hiding ( zip, zipWith )

import Control.Monad  ( forM_, zipWithM )

import Data.Maybe

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

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Benchmark (MonadBench)
import Agda.TypeChecking.Monad.Benchmark qualified as Bench
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.ListInf qualified as ListInf
import Agda.Utils.Maybe ( whenNothingM, whenJust )
import Agda.Utils.Monad
import Agda.Syntax.Common.Pretty ( prettyShow )
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Zip
import Agda.Utils.VarSet (VarSet)
import Agda.Utils.VarSet qualified as VarSet
import Agda.Utils.StrictState

import Agda.Utils.Impossible

import Agda.Syntax.Position
import Debug.Trace

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

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

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

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

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

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

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

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


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

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

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

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

-- | Main function of this module.
computePolarity :: [QName] -> TCM ()
computePolarity :: [QName] -> TCM ()
computePolarity [QName]
xs = Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Polarity] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
 [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.set" Int
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"computePolarity" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [QName] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [QName] -> m Doc
prettyTCM [QName]
xs

 -- Andreas, 2017-04-26, issue #2554
 -- First, for mutual definitions, obtain a crude polarity from positivity.
 Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when ([QName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2) (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 ()
forall (m :: * -> *).
(HasConstInfo m, MonadTCState m) =>
QName -> m ()
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.
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
  [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.polarity.set" Int
25 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Refining polarity of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
x

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

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

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

  -- compute polarity of sized types
  pol1 <- QName -> [Polarity] -> TCM [Polarity]
sizePolarity QName
x [Polarity]
pol0

  -- refine polarity again by using type information
  let t = Definition -> Type'' Term Term
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.
  reportSDoc "tc.polarity.set" 15 $
    "Refining polarity with type " <+> prettyTCM t
  reportSDoc "tc.polarity.set" 90 $
    "Refining polarity with type (raw): " <+> (text .show) t

  pol <- liftReduce $ dependentPolarity t (enablePhantomTypes (theDef def) pol1) pol1
  reportSLn "tc.polarity.set" 10 $ "Polarity of " ++ prettyShow x ++ ": " ++ prettyShow pol

  -- set the polarity in the signature
  setPolarity x $ drop npars 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] -> ReduceM [Polarity]
dependentPolarity :: Type'' Term Term -> [Polarity] -> [Polarity] -> ReduceM [Polarity]
dependentPolarity Type'' Term Term
t [Polarity]
qs [Polarity]
ps
  | (Polarity -> Bool) -> [Polarity] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
Invariant) [Polarity]
qs Bool -> Bool -> Bool
&& (Polarity -> Bool) -> [Polarity] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
Invariant) [Polarity]
ps = [Polarity] -> ReduceM [Polarity]
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Polarity]
ps -- Nothing can be possibly adjusted
  | Bool
otherwise = StateT VarSet ReduceM [Polarity] -> VarSet -> ReduceM [Polarity]
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Type'' Term Term
-> [Polarity] -> [Polarity] -> StateT VarSet ReduceM [Polarity]
go Type'' Term Term
t [Polarity]
qs [Polarity]
ps) VarSet
forall a. Monoid a => a
mempty where

  -- 2026-02-26 András: this should exist more generically!
  {-# INLINE extendEnv #-}
  extendEnv :: String -> Dom Type -> StateT VarSet ReduceM a -> StateT VarSet ReduceM a
  extendEnv :: forall a.
[Char]
-> Dom' Term (Type'' Term Term)
-> StateT VarSet ReduceM a
-> StateT VarSet ReduceM a
extendEnv [Char]
x Dom' Term (Type'' Term Term)
a StateT VarSet ReduceM a
act = (VarSet -> ReduceM (Pair a VarSet)) -> StateT VarSet ReduceM a
forall s (m :: * -> *) a. (s -> m (Pair a s)) -> StateT s m a
StateT \VarSet
s -> (ReduceEnv -> Pair a VarSet) -> ReduceM (Pair a VarSet)
forall a. (ReduceEnv -> a) -> ReduceM a
ReduceM \ReduceEnv
e ->
    ReduceM (Pair a VarSet) -> ReduceEnv -> Pair a VarSet
forall a. ReduceM a -> ReduceEnv -> a
unReduceM (StateT VarSet ReduceM a -> VarSet -> ReduceM (Pair a VarSet)
forall s (m :: * -> *) a. StateT s m a -> s -> m (Pair a s)
runStateT# StateT VarSet ReduceM a
act VarSet
s) (ReduceEnv -> Pair a VarSet) -> ReduceEnv -> Pair a VarSet
forall a b. (a -> b) -> a -> b
$! [Char] -> Dom' Term (Type'' Term Term) -> ReduceEnv -> ReduceEnv
extendReduceEnv [Char]
x Dom' Term (Type'' Term Term)
a ReduceEnv
e

  -- Andreas, 2014-04-11 see Issue 1099
  -- Free variable analysis is not in the monad,
  -- hence metas must have been instantiated before!
  go :: Type -> [Polarity] -> [Polarity] -> StateT VarSet ReduceM [Polarity]
  go :: Type'' Term Term
-> [Polarity] -> [Polarity] -> StateT VarSet ReduceM [Polarity]
go Type'' Term Term
t [Polarity]
qs [Polarity]
ps = case ([Polarity]
qs, [Polarity]
ps) of
    ([Polarity]
_, []) -> do
      (VarSet -> VarSet) -> StateT VarSet ReduceM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (VarSet -> Type'' Term Term -> VarSet
forall t. Free t => VarSet -> t -> VarSet
`setRelInIgnoring` Type'' Term Term
t)
      [Polarity] -> StateT VarSet ReduceM [Polarity]
forall a. a -> StateT VarSet ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    ([], Polarity
_:[Polarity]
_) ->
      StateT VarSet ReduceM [Polarity]
forall a. HasCallStack => a
__IMPOSSIBLE__
    (Polarity
q:[Polarity]
qs, pols :: [Polarity]
pols@(Polarity
p:[Polarity]
ps)) -> do
      ReduceM () -> StateT VarSet ReduceM ()
forall (m :: * -> *) a. Monad m => m a -> StateT VarSet m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ReduceM () -> StateT VarSet ReduceM ())
-> ReduceM () -> StateT VarSet ReduceM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> TCMT IO Doc -> ReduceM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.dep" Int
20 (TCMT IO Doc -> ReduceM ()) -> TCMT IO Doc -> ReduceM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"dependentPolarity t = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t
      ReduceM () -> StateT VarSet ReduceM ()
forall (m :: * -> *) a. Monad m => m a -> StateT VarSet m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ReduceM () -> StateT VarSet ReduceM ())
-> ReduceM () -> StateT VarSet ReduceM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> TCMT IO Doc -> ReduceM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.dep" Int
70 (TCMT IO Doc -> ReduceM ()) -> TCMT IO Doc -> ReduceM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"dependentPolarity t = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (Type'' Term Term -> [Char]) -> Type'' Term Term -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type'' Term Term -> [Char]
forall a. Show a => a -> [Char]
show) Type'' Term Term
t
      ReduceM Term -> StateT VarSet ReduceM Term
forall (m :: * -> *) a. Monad m => m a -> StateT VarSet m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Term -> ReduceM Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
t)) StateT VarSet ReduceM Term
-> (Term -> StateT VarSet ReduceM [Polarity])
-> StateT VarSet ReduceM [Polarity]
forall a b.
StateT VarSet ReduceM a
-> (a -> StateT VarSet ReduceM b) -> StateT VarSet ReduceM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Pi Dom' Term (Type'' Term Term)
dom Abs (Type'' Term Term)
b -> do
          let phantom :: StateT VarSet ReduceM Polarity
phantom | Polarity
p Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
/= Polarity
q = StateT VarSet ReduceM Bool
-> StateT VarSet ReduceM Polarity
-> StateT VarSet ReduceM Polarity
-> StateT VarSet ReduceM Polarity
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (ReduceM Bool -> StateT VarSet ReduceM Bool
forall (m :: * -> *) a. Monad m => m a -> StateT VarSet m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe BoundedSize -> Bool
forall a. Maybe a -> Bool
isJust (Maybe BoundedSize -> Bool)
-> ReduceM (Maybe BoundedSize) -> ReduceM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type'' Term Term -> ReduceM (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Type'' Term Term -> m (Maybe BoundedSize)
isSizeType (Dom' Term (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom Dom' Term (Type'' Term Term)
dom)))
                                     (Polarity -> StateT VarSet ReduceM Polarity
forall a. a -> StateT VarSet ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Polarity
p) (Polarity -> StateT VarSet ReduceM Polarity
forall a. a -> StateT VarSet ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Polarity
q)
                      | Bool
otherwise = Polarity -> StateT VarSet ReduceM Polarity
forall a. a -> StateT VarSet ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Polarity
p
              finish :: Polarity -> [Polarity] -> StateT VarSet ReduceM [Polarity]
finish Polarity
p [Polarity]
ps = do
                Bool -> StateT VarSet ReduceM () -> StateT VarSet ReduceM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (Polarity
p Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
/= Polarity
Nonvariant) ((VarSet -> VarSet) -> StateT VarSet ReduceM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (VarSet -> Dom' Term (Type'' Term Term) -> VarSet
forall t. Free t => VarSet -> t -> VarSet
`setRelInIgnoring` Dom' Term (Type'' Term Term)
dom))
                [Polarity] -> StateT VarSet ReduceM [Polarity]
forall a. a -> StateT VarSet ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Polarity
pPolarity -> [Polarity] -> [Polarity]
forall a. a -> [a] -> [a]
:[Polarity]
ps)
          case Abs (Type'' Term Term)
b of
            Abs [Char]
x Type'' Term Term
t -> [Char]
-> Dom' Term (Type'' Term Term)
-> StateT VarSet ReduceM [Polarity]
-> StateT VarSet ReduceM [Polarity]
forall a.
[Char]
-> Dom' Term (Type'' Term Term)
-> StateT VarSet ReduceM a
-> StateT VarSet ReduceM a
extendEnv [Char]
x Dom' Term (Type'' Term Term)
dom do
              (VarSet -> VarSet) -> StateT VarSet ReduceM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Int -> VarSet -> VarSet
VarSet.weaken Int
1)
              case Polarity
p of
                Polarity
Invariant -> do
                  !ps <- Type'' Term Term
-> [Polarity] -> [Polarity] -> StateT VarSet ReduceM [Polarity]
go Type'' Term Term
t [Polarity]
qs [Polarity]
ps
                  !p  <- phantom
                  modify (VarSet.strengthen 1)
                  finish p ps
                Polarity
_ -> do
                  (VarSet -> VarSet) -> StateT VarSet ReduceM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Int -> VarSet -> VarSet
VarSet.insert Int
0)
                  !ps <- Type'' Term Term
-> [Polarity] -> [Polarity] -> StateT VarSet ReduceM [Polarity]
go Type'' Term Term
t [Polarity]
qs [Polarity]
ps
                  !p <- gets (VarSet.member 0) >>= \case
                    -- binder doesn't occur in the rest
                    Bool
True -> StateT VarSet ReduceM Polarity
phantom
                    -- binder occurs in the rest
                    Bool
False -> Polarity -> StateT VarSet ReduceM Polarity
forall a. a -> StateT VarSet ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Polarity
Invariant
                  modify (VarSet.strengthen 1)
                  finish p ps
            NoAbs [Char]
_ Type'' Term Term
t -> do
              !ps <- Type'' Term Term
-> [Polarity] -> [Polarity] -> StateT VarSet ReduceM [Polarity]
go Type'' Term Term
t [Polarity]
qs [Polarity]
ps
              !p  <- phantom
              finish p ps
        Term
t -> do
          (VarSet -> VarSet) -> StateT VarSet ReduceM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (VarSet -> Term -> VarSet
forall t. Free t => VarSet -> t -> VarSet
`setRelInIgnoring` Term
t)
          [Polarity] -> StateT VarSet ReduceM [Polarity]
forall a. a -> StateT VarSet ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Polarity]
pols

------------------------------------------------------------------------
-- * 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 a. a -> TCMT IO a
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
    def <- QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d
    case theDef def of
      Datatype{ dataPars :: Defn -> Int
dataPars = Int
np, dataCons :: Defn -> [QName]
dataCons = [QName]
cons } -> do
        let TelV Tele (Dom' Term (Type'' Term Term))
tel Type'' Term Term
_      = Type'' Term Term -> TelV (Type'' Term Term)
telView' (Type'' Term Term -> TelV (Type'' Term Term))
-> Type'' Term Term -> TelV (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Definition -> Type'' Term Term
defType Definition
def
            ([Dom ([Char], Type'' Term Term)]
parTel, [Dom ([Char], Type'' Term Term)]
ixTel) = Int
-> [Dom ([Char], Type'' Term Term)]
-> ([Dom ([Char], Type'' Term Term)],
    [Dom ([Char], Type'' Term Term)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
np ([Dom ([Char], Type'' Term Term)]
 -> ([Dom ([Char], Type'' Term Term)],
     [Dom ([Char], Type'' Term Term)]))
-> [Dom ([Char], Type'' Term Term)]
-> ([Dom ([Char], Type'' Term Term)],
    [Dom ([Char], Type'' Term Term)])
forall a b. (a -> b) -> a -> b
$ Tele (Dom' Term (Type'' Term Term))
-> [Dom ([Char], Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom' Term (Type'' Term Term))
tel
        case [Dom ([Char], Type'' Term Term)]
ixTel of
          []                 -> TCM [Polarity]
exit  -- No size index
          (Dom ([Char], Type'' Term Term) -> ([Char], Type'' Term Term)
forall t e. Dom' t e -> e
unDom -> ([Char]
_,Type'' Term Term
a)) : [Dom ([Char], Type'' Term Term)]
_ -> 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'' Term Term -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Type'' Term Term -> m (Maybe BoundedSize)
isSizeType Type'' Term Term
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 ()
forall (m :: * -> *).
(MonadTCState m, MonadDebug m) =>
QName -> [Polarity] -> m ()
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 -> TCM Bool
                check :: QName -> TCMT IO Bool
check QName
c = do
                  t <- Definition -> Type'' Term Term
defType (Definition -> Type'' Term Term)
-> TCMT IO Definition -> TCMT IO (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
c
                  addContext (telFromList parTel) $ do
                    let 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 target <- telView =<< (t `piApplyM` pars)
                    loop target conTel
                  where
                  loop :: Type -> Telescope -> TCM Bool
                  -- no suitable size argument
                  loop :: Type'' Term Term
-> Tele (Dom' Term (Type'' Term Term)) -> TCMT IO Bool
loop Type'' Term Term
_ Tele (Dom' Term (Type'' Term Term))
EmptyTel = do
                    [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.size" Int
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
                      TCMT IO Doc
"constructor" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"fails size polarity check"
                    Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

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

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

                        -- check that the size argument appears in the
                        -- right spot in the target type
                        let sizeArg :: Int
sizeArg = Tele (Dom' Term (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term (Type'' Term Term))
tel
                        isLin <- Tele (Dom' Term (Type'' Term Term)) -> TCMT IO Bool -> TCMT IO Bool
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom' Term (Type'' Term Term)) -> m a -> m a
addContext Tele (Dom' Term (Type'' Term Term))
tel (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ QName -> Int -> Type'' Term Term -> TCMT IO Bool
checkSizeIndex QName
d Int
sizeArg Type'' Term Term
target
                        if not isLin then continue else do

                          -- check that only positive occurences in tel
                          pols <- zipWithM polarity [0..] $ map (snd . unDom) $ telToList tel
                          reportSDoc "tc.polarity.size" 25 $
                            text $ "to pass size polarity check, the following polarities need all to be covariant: " ++ prettyShow pols
                          if any (`notElem` [Nonvariant, Covariant]) pols then continue else do
                            reportSDoc "tc.polarity.size" 15 $
                              "constructor" <+> prettyTCM c <+> "passes size polarity check"
                            return True

            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 a. a -> TCMT IO a
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 ()
forall (m :: * -> *).
MonadTCState m =>
QName -> ([Occurrence] -> [Occurrence]) -> m ()
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 a. a -> TCMT IO a
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'' Term Term -> TCMT IO Bool
checkSizeIndex QName
d Int
i Type'' Term Term
a = do
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.size" Int
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"checking that constructor target type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
a
    , TCMT IO Doc
"  is data type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d
    , TCMT IO Doc
"  and has size index (successor(s) of) " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Int -> Term
var Int
i)
    ]
  case Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
a of
    Def QName
d0 [Elim]
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__
      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)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe Int)
getNumberOfParameters QName
d0
      let (pars, Apply ix : ixs) = splitAt np es
      s <- deepSizeView $ unArg ix
      case s of
        DSizeVar (ProjectedVar Int
j []) Int
_ | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j
          -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
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 -> [Elim] -> Bool
forall t. Free t => Int -> t -> Bool
freeIn Int
i ([Elim]
pars [Elim] -> [Elim] -> [Elim]
forall a. [a] -> [a] -> [a]
++ [Elim]
ixs)
        DeepSizeView
_ -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Term
_ -> TCMT IO Bool
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

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

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

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

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

  default polarity'
    :: (HasConstInfo m, MonadReduce m, HasPolarity b, Foldable t, t b ~ a)
    => Nat -> Polarity -> a -> LeastPolarity m
  polarity' Int
i = (b -> LeastPolarity m) -> a -> LeastPolarity m
(b -> LeastPolarity m) -> t b -> LeastPolarity m
forall m a. Monoid m => (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((b -> LeastPolarity m) -> a -> LeastPolarity m)
-> (Polarity -> b -> LeastPolarity m)
-> Polarity
-> a
-> LeastPolarity m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Polarity -> b -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> b -> LeastPolarity m
polarity' Int
i

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

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

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

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

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