{-# LANGUAGE MagicHash #-}

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

module Mikan.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 Data.Text.Short (ShortText)

import Mikan.Syntax.Abstract.Name
import Mikan.Syntax.Common
import Mikan.Syntax.Internal

import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Monad.Benchmark (MonadBench)
import Mikan.TypeChecking.Monad.Benchmark qualified as Bench
import Mikan.TypeChecking.Datatypes (getNumberOfParameters)
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Telescope
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.Free
import Mikan.TypeChecking.Positivity.Occurrence

import Mikan.Utils.List
import Mikan.Utils.ListInf qualified as ListInf
import Mikan.Utils.Maybe ( whenNothingM, whenJust )
import Mikan.Utils.Monad
import Mikan.Syntax.Common.Pretty ( prettyShow )
import Mikan.Utils.Singleton
import Mikan.Utils.Size
import Mikan.Utils.Zip
import Mikan.Utils.VarSet (VarSet)
import Mikan.Utils.VarSet qualified as VarSet
import Mikan.Utils.StrictState

import Mikan.Utils.Impossible

import Mikan.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
-}

  -- refine polarity again by using type information
  let t :: Type
t = Definition -> Type
defType Definition
def
  -- Instantiation takes place in Rules.Decl.instantiateDefinitionType
  -- t <- instantiateFull t -- Andreas, 2014-04-11 Issue 1099: needed for
  --                        -- variable occurrence test in  dependentPolarity.
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.set" Int
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Refining polarity with type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.polarity.set" Int
90 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Refining polarity with type (raw): " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> (Type -> [Char]) -> Type -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Type -> [Char]
forall a. Show a => a -> [Char]
show) Type
t

  pol <- ReduceM [Polarity] -> TCMT IO [Polarity]
forall a. ReduceM a -> TCMT IO a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM [Polarity] -> TCMT IO [Polarity])
-> ReduceM [Polarity] -> TCMT IO [Polarity]
forall a b. (a -> b) -> a -> b
$ Type -> [Polarity] -> [Polarity] -> ReduceM [Polarity]
dependentPolarity Type
t (Defn -> [Polarity] -> [Polarity]
enablePhantomTypes (Definition -> Defn
theDef Definition
def) [Polarity]
pol0) [Polarity]
pol0
  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 -> [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 :: ShortText -> Dom Type -> StateT VarSet ReduceM a -> StateT VarSet ReduceM a
  extendEnv :: forall a.
ShortText
-> Dom Type -> StateT VarSet ReduceM a -> StateT VarSet ReduceM a
extendEnv ShortText
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
$! ShortText -> Dom Type -> ReduceEnv -> ReduceEnv
extendReduceEnv ShortText
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
`setFreeInIgnoring` 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] -> 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 -> 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] -> 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 -> [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 = 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
`setFreeInIgnoring` 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 ShortText
x Type
t -> ShortText
-> Dom Type
-> StateT VarSet ReduceM [Polarity]
-> StateT VarSet ReduceM [Polarity]
forall a.
ShortText
-> Dom Type -> StateT VarSet ReduceM a -> StateT VarSet ReduceM a
extendEnv ShortText
x Dom Type
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
-> [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 (Int -> VarSet -> VarSet
VarSet.insert Int
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 ShortText
_ 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
`setFreeInIgnoring` 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

-- | @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   ShortText
_ 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 ShortText
_ 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 Elims
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 -> Elims -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> Elims -> LeastPolarity m
polarity' Int
i Polarity
Invariant Elims
ts
      | Bool
otherwise -> Int -> Polarity -> Elims -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> Elims -> LeastPolarity m
polarity' Int
i Polarity
Invariant Elims
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
l       -> Int -> Polarity -> Level -> 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 -> LeastPolarity m
polarity' Int
i Polarity
p Level
l
    Def QName
x Elims
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 -> Elims -> [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 Elims
ts
    Con ConHead
_ ConInfo
_ Elims
ts    -> Int -> Polarity -> Elims -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> Elims -> LeastPolarity m
polarity' Int
i Polarity
p Elims
ts   -- Constructors can be seen as monotone in all args.
    Pi Dom Type
a Abs Type
b        -> Int -> Polarity -> Dom Type -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> Dom Type -> LeastPolarity m
polarity' Int
i (Polarity -> Polarity
neg Polarity
p) Dom Type
a LeastPolarity m -> LeastPolarity m -> LeastPolarity m
forall a. Semigroup a => a -> a -> a
<> Int -> Polarity -> Abs Type -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> Abs Type -> LeastPolarity m
polarity' Int
i Polarity
p Abs Type
b
    Sort Sort
s        -> LeastPolarity m
forall a. Monoid a => a
mempty -- polarity' i p s -- mempty
    MetaV MetaId
_ Elims
ts    -> Int -> Polarity -> Elims -> LeastPolarity m
forall a (m :: * -> *).
(HasPolarity a, HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> a -> LeastPolarity m
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Int -> Polarity -> Elims -> LeastPolarity m
polarity' Int
i Polarity
Invariant Elims
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