{-# 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 )
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 :: Nat
npars = Definition -> Nat
droppedPars Definition
def
  let pol0 :: [Polarity]
pol0 = Nat -> Polarity -> [Polarity]
forall a. Nat -> a -> [a]
replicate Nat
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] -> Nat -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.polarity.set" Nat
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
$ Nat -> [Polarity] -> [Polarity]
forall a. Nat -> [a] -> [a]
drop Nat
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] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.set" Nat
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] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [QName]
xs Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
>= Nat
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] -> Nat -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.polarity.set" Nat
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 :: Nat
npars = Definition -> Nat
droppedPars Definition
def
  let pol0 :: [Polarity]
pol0 = Nat -> Polarity -> [Polarity]
forall a. Nat -> a -> [a]
replicate Nat
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] -> Nat -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.polarity.set" Nat
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
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 -> Nat
dataPars = Nat
np } -> Nat -> [Polarity]
enable Nat
np
  Record  { recPars :: Defn -> Nat
recPars  = Nat
np } -> Nat -> [Polarity]
enable Nat
np
  Defn
_                         -> [Polarity]
pol
  where enable :: Nat -> [Polarity]
enable Nat
np = let ([Polarity]
pars, [Polarity]
rest) = Nat -> [Polarity] -> ([Polarity], [Polarity])
forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
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 -> [Polarity] -> [Polarity] -> ReduceM [Polarity]
dependentPolarity Type
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
-> [Polarity] -> [Polarity] -> StateT VarSet ReduceM [Polarity]
go Type
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 Type -> StateT VarSet ReduceM a -> StateT VarSet ReduceM a
extendEnv [Char]
x Dom Type
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 Type -> ReduceEnv -> ReduceEnv
extendReduceEnv [Char]
x Dom Type
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
-> [Polarity] -> [Polarity] -> StateT VarSet ReduceM [Polarity]
go Type
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 -> VarSet
forall t. Free t => VarSet -> t -> VarSet
`setRelInIgnoring` Type
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] -> Nat -> TCMT IO Doc -> ReduceM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.dep" Nat
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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
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] -> Nat -> TCMT IO Doc -> ReduceM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.dep" Nat
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 -> [Char]) -> Type -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [Char]
forall a. Show a => a -> [Char]
show) Type
t
      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
forall t a. Type'' t a -> a
unEl Type
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 Type
dom Abs Type
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 -> ReduceM (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Type -> m (Maybe BoundedSize)
isSizeType (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
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 Type -> VarSet
forall t. Free t => VarSet -> t -> VarSet
`setRelInIgnoring` Dom Type
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
b of
            Abs [Char]
x Type
t -> [Char]
-> Dom Type
-> StateT VarSet ReduceM [Polarity]
-> StateT VarSet ReduceM [Polarity]
forall a.
[Char]
-> Dom Type -> StateT VarSet ReduceM a -> StateT VarSet ReduceM a
extendEnv [Char]
x Dom Type
dom do
              (VarSet -> VarSet) -> StateT VarSet ReduceM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Nat -> VarSet -> VarSet
VarSet.weaken Nat
1)
              case Polarity
p of
                Polarity
Invariant -> do
                  !ps <- Type
-> [Polarity] -> [Polarity] -> StateT VarSet ReduceM [Polarity]
go Type
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 (Nat -> VarSet -> VarSet
VarSet.insert Nat
0)
                  !ps <- Type
-> [Polarity] -> [Polarity] -> StateT VarSet ReduceM [Polarity]
go Type
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
t -> do
              !ps <- Type
-> [Polarity] -> [Polarity] -> StateT VarSet ReduceM [Polarity]
go Type
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 -> Nat
dataPars = Nat
np, dataCons :: Defn -> [QName]
dataCons = [QName]
cons } -> do
        let TelV Tele (Dom Type)
tel Type
_      = Type -> TelV Type
telView' (Type -> TelV Type) -> Type -> TelV Type
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
            ([Dom ([Char], Type)]
parTel, [Dom ([Char], Type)]
ixTel) = Nat
-> [Dom ([Char], Type)]
-> ([Dom ([Char], Type)], [Dom ([Char], Type)])
forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
np ([Dom ([Char], Type)]
 -> ([Dom ([Char], Type)], [Dom ([Char], Type)]))
-> [Dom ([Char], Type)]
-> ([Dom ([Char], Type)], [Dom ([Char], Type)])
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel
        case [Dom ([Char], Type)]
ixTel of
          []                 -> TCM [Polarity]
exit  -- No size index
          Dom{unDom :: forall t e. Dom' t e -> e
unDom = ([Char]
_,Type
a)} : [Dom ([Char], Type)]
_ -> TCMT IO Bool -> TCM [Polarity] -> TCM [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((Maybe BoundedSize -> Maybe BoundedSize -> Bool
forall a. Eq a => a -> a -> Bool
/= BoundedSize -> Maybe BoundedSize
forall a. a -> Maybe a
Just BoundedSize
BoundedNo) (Maybe BoundedSize -> Bool)
-> TCMT IO (Maybe BoundedSize) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Type -> 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   = Nat -> [Polarity] -> [Polarity]
forall a. Nat -> [a] -> [a]
take Nat
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
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, HasCallStack) =>
QName -> m Definition
getConstInfo QName
c
                  addContext (telFromList parTel) $ do
                    let pars = (Nat -> Arg Term) -> [Nat] -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> (Nat -> Term) -> Nat -> Arg Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Term
var) ([Nat] -> [Arg Term]) -> [Nat] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom Nat
np
                    TelV conTel target <- telView =<< (t `piApplyM` pars)
                    loop target conTel
                  where
                  loop :: Type -> Telescope -> TCM Bool
                  -- no suitable size argument
                  loop :: Type -> Tele (Dom Type) -> TCMT IO Bool
loop Type
_ Tele (Dom Type)
EmptyTel = do
                    [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.size" Nat
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
target (ExtendTel Dom Type
dom Abs (Tele (Dom Type))
tel) = do
                    isSz <- Dom Type -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Dom Type -> m (Maybe BoundedSize)
isSizeType Dom Type
dom
                    underAbstraction dom tel $ \ Tele (Dom Type)
tel -> do
                      let continue :: TCMT IO Bool
continue = Type -> Tele (Dom Type) -> TCMT IO Bool
loop Type
target Tele (Dom Type)
tel

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

                        -- check that the size argument appears in the
                        -- right spot in the target type
                        let sizeArg :: Nat
sizeArg = Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel
                        isLin <- Tele (Dom Type) -> 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 Type) -> m a -> m a
addContext Tele (Dom Type)
tel (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ QName -> Nat -> Type -> TCMT IO Bool
checkSizeIndex QName
d Nat
sizeArg Type
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 -> Nat -> [Occurrence] -> [Occurrence]
forall a. Nat -> [a] -> [a]
take Nat
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 -> Nat -> Type -> TCMT IO Bool
checkSizeIndex QName
d Nat
i Type
a = do
  [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.size" Nat
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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
    , TCMT IO Doc
"  is data type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
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 (Nat -> Term
var Nat
i)
    ]
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
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 <- Nat -> Maybe Nat -> Nat
forall a. a -> Maybe a -> a
fromMaybe Nat
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Nat -> Nat) -> TCMT IO (Maybe Nat) -> TCMT IO Nat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Maybe Nat)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe Nat)
getNumberOfParameters QName
d0
      let (pars, Apply ix : ixs) = splitAt np es
      s <- deepSizeView $ unArg ix
      case s of
        DSizeVar (ProjectedVar Nat
j []) Nat
_ | Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
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
$ Nat -> [Elim] -> Bool
forall t. Free t => Nat -> t -> Bool
freeIn Nat
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) =>
Nat -> a -> m Polarity
polarity Nat
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
$ Nat -> Polarity -> a -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> a -> LeastPolarity m
polarity' Nat
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' Nat
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
. Nat -> Polarity -> b -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> b -> LeastPolarity m
polarity' Nat
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) =>
Nat -> Polarity -> (a, b) -> LeastPolarity m
polarity' Nat
i Polarity
p (a
x, b
y) = Nat -> Polarity -> a -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> a -> LeastPolarity m
polarity' Nat
i Polarity
p a
x LeastPolarity m -> LeastPolarity m -> LeastPolarity m
forall a. Semigroup a => a -> a -> a
<> Nat -> Polarity -> b -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> b -> LeastPolarity m
polarity' Nat
i Polarity
p b
y

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

instance HasPolarity Term where
  polarity' :: forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> Term -> LeastPolarity m
polarity' Nat
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 Nat
n [Elim]
ts
      | Nat
n Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
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
<> Nat -> Polarity -> [Elim] -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> [Elim] -> LeastPolarity m
polarity' Nat
i Polarity
Invariant [Elim]
ts
      | Bool
otherwise -> Nat -> Polarity -> [Elim] -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> [Elim] -> LeastPolarity m
polarity' Nat
i Polarity
Invariant [Elim]
ts
    Lam ArgInfo
_ Abs Term
t       -> Nat -> Polarity -> Abs Term -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> Abs Term -> LeastPolarity m
polarity' Nat
i Polarity
p Abs Term
t
    Lit Literal
_         -> LeastPolarity m
forall a. Monoid a => a
mempty
    Level Level
l       -> Nat -> Polarity -> Level -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> Level -> LeastPolarity m
polarity' Nat
i Polarity
p Level
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 (Nat -> Polarity -> Elim -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> Elim -> LeastPolarity m
polarity' Nat
i) ListInf Polarity
ps [Elim]
ts
    Con ConHead
_ ConInfo
_ [Elim]
ts    -> Nat -> Polarity -> [Elim] -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> [Elim] -> LeastPolarity m
polarity' Nat
i Polarity
p [Elim]
ts   -- Constructors can be seen as monotone in all args.
    Pi Dom Type
a Abs Type
b        -> Nat -> Polarity -> Dom Type -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> Dom Type -> LeastPolarity m
polarity' Nat
i (Polarity -> Polarity
neg Polarity
p) Dom Type
a LeastPolarity m -> LeastPolarity m -> LeastPolarity m
forall a. Semigroup a => a -> a -> a
<> Nat -> Polarity -> Abs Type -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> Abs Type -> LeastPolarity m
polarity' Nat
i Polarity
p Abs Type
b
    Sort Sort
s        -> LeastPolarity m
forall a. Monoid a => a
mempty -- polarity' i p s -- mempty
    MetaV MetaId
_ [Elim]
ts    -> Nat -> Polarity -> [Elim] -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> [Elim] -> LeastPolarity m
polarity' Nat
i Polarity
Invariant [Elim]
ts
    DontCare Term
t    -> Nat -> Polarity -> Term -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Nat -> Polarity -> Term -> LeastPolarity m
polarity' Nat
i Polarity
p Term
t -- mempty
    Dummy{}       -> LeastPolarity m
forall a. Monoid a => a
mempty