module Agda.TypeChecking.Polarity where
import Control.Monad.State
import Data.Maybe
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Datatypes (getNumberOfParameters)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.SizedTypes
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Free
import Agda.TypeChecking.Positivity.Occurrence
import Agda.Utils.List
import Agda.Utils.Maybe ( whenNothingM )
import Agda.Utils.Monad
import Agda.Utils.Pretty ( prettyShow )
import Agda.Utils.Size
import Agda.Utils.Impossible
(/\) :: Polarity -> Polarity -> Polarity
Nonvariant /\ :: Polarity -> Polarity -> Polarity
/\ b :: Polarity
b = Polarity
b
a :: Polarity
a /\ Nonvariant = Polarity
a
a :: Polarity
a /\ b :: Polarity
b | Polarity
a Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
b = Polarity
a
| Bool
otherwise = Polarity
Invariant
neg :: Polarity -> Polarity
neg :: Polarity -> Polarity
neg Covariant = Polarity
Contravariant
neg Contravariant = Polarity
Covariant
neg Invariant = Polarity
Invariant
neg Nonvariant = Polarity
Nonvariant
composePol :: Polarity -> Polarity -> Polarity
composePol :: Polarity -> Polarity -> Polarity
composePol Nonvariant _ = Polarity
Nonvariant
composePol _ Nonvariant = Polarity
Nonvariant
composePol Invariant _ = Polarity
Invariant
composePol Covariant x :: Polarity
x = Polarity
x
composePol Contravariant x :: Polarity
x = Polarity -> Polarity
neg Polarity
x
polFromOcc :: Occurrence -> Polarity
polFromOcc :: Occurrence -> Polarity
polFromOcc o :: Occurrence
o = case Occurrence
o of
GuardPos -> Polarity
Covariant
StrictPos -> Polarity
Covariant
JustPos -> Polarity
Covariant
JustNeg -> Polarity
Contravariant
Mixed -> Polarity
Invariant
Unused -> Polarity
Nonvariant
nextPolarity :: [Polarity] -> (Polarity, [Polarity])
nextPolarity :: [Polarity] -> (Polarity, [Polarity])
nextPolarity [] = (Polarity
Invariant, [])
nextPolarity (p :: Polarity
p : ps :: [Polarity]
ps) = (Polarity
p, [Polarity]
ps)
purgeNonvariant :: [Polarity] -> [Polarity]
purgeNonvariant :: [Polarity] -> [Polarity]
purgeNonvariant = (Polarity -> Polarity) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map (\ p :: Polarity
p -> if Polarity
p Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
Nonvariant then Polarity
Covariant else Polarity
p)
polarityFromPositivity :: QName -> TCM ()
polarityFromPositivity :: QName -> TCM ()
polarityFromPositivity x :: QName
x = QName -> (Definition -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
x ((Definition -> TCM ()) -> TCM ())
-> (Definition -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ def :: Definition
def -> do
let npars :: Int
npars = Definition -> Int
droppedPars Definition
def
let pol0 :: [Polarity]
pol0 = Int -> Polarity -> [Polarity]
forall a. Int -> a -> [a]
replicate Int
npars Polarity
Nonvariant [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
++ (Occurrence -> Polarity) -> [Occurrence] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> Polarity
polFromOcc (Definition -> [Occurrence]
defArgOccurrences Definition
def)
VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.polarity.set" 15 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
"Polarity of " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
x VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ " from positivity: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [Polarity] -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow [Polarity]
pol0
QName -> [Polarity] -> TCM ()
setPolarity QName
x ([Polarity] -> TCM ()) -> [Polarity] -> TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> [Polarity] -> [Polarity]
forall a. Int -> [a] -> [a]
drop Int
npars [Polarity]
pol0
computePolarity :: [QName] -> TCM ()
computePolarity :: [QName] -> TCM ()
computePolarity xs :: [QName]
xs = do
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([QName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 2) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ (QName -> TCM ()) -> [QName] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ QName -> TCM ()
polarityFromPositivity [QName]
xs
[QName] -> (QName -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [QName]
xs ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ x :: QName
x -> QName -> (Definition -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
x ((Definition -> TCM ()) -> TCM ())
-> (Definition -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ def :: Definition
def -> do
VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.polarity.set" 25 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "Refining polarity of " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
x
let npars :: Int
npars = Definition -> Int
droppedPars Definition
def
let pol0 :: [Polarity]
pol0 = Int -> Polarity -> [Polarity]
forall a. Int -> a -> [a]
replicate Int
npars Polarity
Nonvariant [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
++ (Occurrence -> Polarity) -> [Occurrence] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> Polarity
polFromOcc (Definition -> [Occurrence]
defArgOccurrences Definition
def)
VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.polarity.set" 15 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
"Polarity of " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
x VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ " from positivity: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [Polarity] -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow [Polarity]
pol0
[Polarity]
pol1 <- QName -> [Polarity] -> TCM [Polarity]
sizePolarity QName
x [Polarity]
pol0
let t :: Type
t = Definition -> Type
defType Definition
def
VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc "tc.polarity.set" 15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
"Refining polarity with type " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc "tc.polarity.set" 60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
"Refining polarity with type (raw): " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> (Type -> VerboseKey) -> Type -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Type -> VerboseKey
forall a. Show a => a -> VerboseKey
show) Type
t
[Polarity]
pol <- Type -> [Polarity] -> [Polarity] -> TCM [Polarity]
dependentPolarity Type
t (Defn -> [Polarity] -> [Polarity]
enablePhantomTypes (Definition -> Defn
theDef Definition
def) [Polarity]
pol1) [Polarity]
pol1
VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.polarity.set" 10 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "Polarity of " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
x VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ ": " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [Polarity] -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow [Polarity]
pol
QName -> [Polarity] -> TCM ()
setPolarity QName
x ([Polarity] -> TCM ()) -> [Polarity] -> TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> [Polarity] -> [Polarity]
forall a. Int -> [a] -> [a]
drop Int
npars [Polarity]
pol
enablePhantomTypes :: Defn -> [Polarity] -> [Polarity]
enablePhantomTypes :: Defn -> [Polarity] -> [Polarity]
enablePhantomTypes def :: Defn
def pol :: [Polarity]
pol = case Defn
def of
Datatype{ dataPars :: Defn -> Int
dataPars = Int
np } -> Int -> [Polarity]
enable Int
np
Record { recPars :: Defn -> Int
recPars = Int
np } -> Int -> [Polarity]
enable Int
np
_ -> [Polarity]
pol
where enable :: Int -> [Polarity]
enable np :: Int
np = let (pars :: [Polarity]
pars, rest :: [Polarity]
rest) = Int -> [Polarity] -> ([Polarity], [Polarity])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
np [Polarity]
pol
in [Polarity] -> [Polarity]
purgeNonvariant [Polarity]
pars [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
++ [Polarity]
rest
dependentPolarity :: Type -> [Polarity] -> [Polarity] -> TCM [Polarity]
dependentPolarity :: Type -> [Polarity] -> [Polarity] -> TCM [Polarity]
dependentPolarity t :: Type
t _ [] = [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return []
dependentPolarity t :: Type
t [] (_ : _) = TCM [Polarity]
forall a. HasCallStack => a
__IMPOSSIBLE__
dependentPolarity t :: Type
t (q :: Polarity
q:qs :: [Polarity]
qs) pols :: [Polarity]
pols@(p :: Polarity
p:ps :: [Polarity]
ps) = do
Term
t <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Type -> Term
forall t a. Type'' t a -> a
unEl Type
t
VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc "tc.polarity.dep" 20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ "dependentPolarity t = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t
VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc "tc.polarity.dep" 70 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ "dependentPolarity t = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> (Term -> VerboseKey) -> Term -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> VerboseKey
forall a. Show a => a -> VerboseKey
show) Term
t
case Term
t of
Pi dom :: Dom Type
dom b :: Abs Type
b -> do
[Polarity]
ps <- Dom Type -> Abs Type -> (Type -> TCM [Polarity]) -> TCM [Polarity]
forall t a (m :: * -> *) b.
(Subst t a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
dom Abs Type
b ((Type -> TCM [Polarity]) -> TCM [Polarity])
-> (Type -> TCM [Polarity]) -> TCM [Polarity]
forall a b. (a -> b) -> a -> b
$ \ c :: Type
c -> Type -> [Polarity] -> [Polarity] -> TCM [Polarity]
dependentPolarity Type
c [Polarity]
qs [Polarity]
ps
let fallback :: TCMT IO Polarity
fallback = TCMT IO Bool
-> TCMT IO Polarity -> TCMT IO Polarity -> TCMT IO Polarity
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Maybe BoundedSize -> Bool
forall a. Maybe a -> Bool
isJust (Maybe BoundedSize -> Bool)
-> TCMT IO (Maybe BoundedSize) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom)) (Polarity -> TCMT IO Polarity
forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
p) (Polarity -> TCMT IO Polarity
forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
q)
Polarity
p <- case Abs Type
b of
Abs{} | Polarity
p Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
/= Polarity
Invariant ->
TCMT IO Bool
-> TCMT IO Polarity -> TCMT IO Polarity -> TCMT IO Polarity
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Int -> Type -> [Polarity] -> TCMT IO Bool
relevantInIgnoringNonvariant 0 (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b) [Polarity]
ps)
(Polarity -> TCMT IO Polarity
forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Invariant)
TCMT IO Polarity
fallback
_ -> TCMT IO Polarity
fallback
[Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Polarity] -> TCM [Polarity]) -> [Polarity] -> TCM [Polarity]
forall a b. (a -> b) -> a -> b
$ Polarity
p Polarity -> [Polarity] -> [Polarity]
forall a. a -> [a] -> [a]
: [Polarity]
ps
_ -> [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return [Polarity]
pols
relevantInIgnoringNonvariant :: Nat -> Type -> [Polarity] -> TCM Bool
relevantInIgnoringNonvariant :: Int -> Type -> [Polarity] -> TCMT IO Bool
relevantInIgnoringNonvariant i :: Int
i t :: Type
t [] = Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Type -> Bool
forall t. Free t => Int -> t -> Bool
`relevantInIgnoringSortAnn` Type
t
relevantInIgnoringNonvariant i :: Int
i t :: Type
t (p :: Polarity
p:ps :: [Polarity]
ps) = do
Term
t <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Type -> Term
forall t a. Type'' t a -> a
unEl Type
t
case Term
t of
Pi a :: Dom Type
a b :: Abs Type
b -> if Polarity
p Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
/= Polarity
Nonvariant Bool -> Bool -> Bool
&& Int
i Int -> Dom Type -> Bool
forall t. Free t => Int -> t -> Bool
`relevantInIgnoringSortAnn` Dom Type
a then Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
else Int -> Type -> [Polarity] -> TCMT IO Bool
relevantInIgnoringNonvariant (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b) [Polarity]
ps
_ -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Term -> Bool
forall t. Free t => Int -> t -> Bool
`relevantInIgnoringSortAnn` Term
t
sizePolarity :: QName -> [Polarity] -> TCM [Polarity]
sizePolarity :: QName -> [Polarity] -> TCM [Polarity]
sizePolarity d :: QName
d pol0 :: [Polarity]
pol0 = do
let exit :: TCM [Polarity]
exit = [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return [Polarity]
pol0
TCMT IO Bool -> TCM [Polarity] -> TCM [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
sizedTypesOption TCM [Polarity]
exit (TCM [Polarity] -> TCM [Polarity])
-> TCM [Polarity] -> TCM [Polarity]
forall a b. (a -> b) -> a -> b
$ do
Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
case Definition -> Defn
theDef Definition
def of
Datatype{ dataPars :: Defn -> Int
dataPars = Int
np, dataCons :: Defn -> [QName]
dataCons = [QName]
cons } -> do
let TelV tel :: Tele (Dom Type)
tel _ = Type -> TelV Type
telView' (Type -> TelV Type) -> Type -> TelV Type
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
(parTel :: [Dom (VerboseKey, Type)]
parTel, ixTel :: [Dom (VerboseKey, Type)]
ixTel) = Int
-> [Dom (VerboseKey, Type)]
-> ([Dom (VerboseKey, Type)], [Dom (VerboseKey, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
np ([Dom (VerboseKey, Type)]
-> ([Dom (VerboseKey, Type)], [Dom (VerboseKey, Type)]))
-> [Dom (VerboseKey, Type)]
-> ([Dom (VerboseKey, Type)], [Dom (VerboseKey, Type)])
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Tele (Dom Type)
tel
case [Dom (VerboseKey, Type)]
ixTel of
[] -> TCM [Polarity]
exit
Dom{unDom :: forall t e. Dom' t e -> e
unDom = (_,a :: Type
a)} : _ -> TCMT IO Bool -> TCM [Polarity] -> TCM [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((Maybe BoundedSize -> Maybe BoundedSize -> Bool
forall a. Eq a => a -> a -> Bool
/= BoundedSize -> Maybe BoundedSize
forall a. a -> Maybe a
Just BoundedSize
BoundedNo) (Maybe BoundedSize -> Bool)
-> TCMT IO (Maybe BoundedSize) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Type
a) TCM [Polarity]
exit (TCM [Polarity] -> TCM [Polarity])
-> TCM [Polarity] -> TCM [Polarity]
forall a b. (a -> b) -> a -> b
$ do
let pol :: [Polarity]
pol = Int -> [Polarity] -> [Polarity]
forall a. Int -> [a] -> [a]
take Int
np [Polarity]
pol0
polCo :: [Polarity]
polCo = [Polarity]
pol [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
++ [Polarity
Covariant]
polIn :: [Polarity]
polIn = [Polarity]
pol [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
++ [Polarity
Invariant]
QName -> [Polarity] -> TCM ()
setPolarity QName
d ([Polarity] -> TCM ()) -> [Polarity] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Polarity]
polCo
let check :: QName -> TCMT IO Bool
check c :: QName
c = do
Type
t <- Definition -> Type
defType (Definition -> Type) -> TCMT IO Definition -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
Tele (Dom Type) -> TCMT IO Bool -> TCMT IO Bool
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([Dom (VerboseKey, Type)] -> Tele (Dom Type)
telFromList [Dom (VerboseKey, Type)]
parTel) (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ do
let pars :: [Arg Term]
pars = (Int -> Arg Term) -> [Int] -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> (Int -> Term) -> Int -> Arg Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var) ([Int] -> [Arg Term]) -> [Int] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
np
TelV conTel :: Tele (Dom Type)
conTel target :: Type
target <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Type -> TCMT IO (TelV Type))
-> TCMT IO Type -> TCMT IO (TelV Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Type
t Type -> [Arg Term] -> TCMT IO Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m) =>
Type -> a -> m Type
`piApplyM` [Arg Term]
pars)
case Tele (Dom Type)
conTel of
EmptyTel -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
ExtendTel arg :: Dom Type
arg tel :: Abs (Tele (Dom Type))
tel ->
TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((Maybe BoundedSize -> Maybe BoundedSize -> Bool
forall a. Eq a => a -> a -> Bool
/= BoundedSize -> Maybe BoundedSize
forall a. a -> Maybe a
Just BoundedSize
BoundedNo) (Maybe BoundedSize -> Bool)
-> TCMT IO (Maybe BoundedSize) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
arg)) (Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ do
let isPos :: TCMT IO Bool
isPos = Dom Type
-> Abs (Tele (Dom Type))
-> (Tele (Dom Type) -> TCMT IO Bool)
-> TCMT IO Bool
forall t a (m :: * -> *) b.
(Subst t a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
arg Abs (Tele (Dom Type))
tel ((Tele (Dom Type) -> TCMT IO Bool) -> TCMT IO Bool)
-> (Tele (Dom Type) -> TCMT IO Bool) -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ \ tel :: Tele (Dom Type)
tel -> do
[Polarity]
pols <- (Int -> Type -> TCMT IO Polarity)
-> [Int] -> [Type] -> TCM [Polarity]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Int -> Type -> TCMT IO Polarity
forall a. HasPolarity a => Int -> a -> TCMT IO Polarity
polarity [0..] ([Type] -> TCM [Polarity]) -> [Type] -> TCM [Polarity]
forall a b. (a -> b) -> a -> b
$ (Dom (VerboseKey, Type) -> Type)
-> [Dom (VerboseKey, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ((VerboseKey, Type) -> Type
forall a b. (a, b) -> b
snd ((VerboseKey, Type) -> Type)
-> (Dom (VerboseKey, Type) -> (VerboseKey, Type))
-> Dom (VerboseKey, Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (VerboseKey, Type) -> (VerboseKey, Type)
forall t e. Dom' t e -> e
unDom) ([Dom (VerboseKey, Type)] -> [Type])
-> [Dom (VerboseKey, Type)] -> [Type]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Tele (Dom Type)
tel
VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc "tc.polarity.size" 25 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "to pass size polarity check, the following polarities need all to be covariant: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [Polarity] -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow [Polarity]
pols
Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ (Polarity -> Bool) -> [Polarity] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Polarity -> [Polarity] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Polarity
Nonvariant, Polarity
Covariant]) [Polarity]
pols
let sizeArg :: Int
sizeArg = Abs (Tele (Dom Type)) -> Int
forall a. Sized a => a -> Int
size Abs (Tele (Dom Type))
tel
isLin :: TCMT IO Bool
isLin = Tele (Dom Type) -> TCMT IO Bool -> TCMT IO Bool
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
conTel (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ QName -> Int -> Type -> TCMT IO Bool
checkSizeIndex QName
d Int
sizeArg Type
target
Bool
ok <- TCMT IO Bool
isPos TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` TCMT IO Bool
isLin
VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc "tc.polarity.size" 15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
"constructor" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (if Bool
ok then "passes" else "fails") TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
"size polarity check"
Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok
TCMT IO Bool -> TCM [Polarity] -> TCM [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM ([TCMT IO Bool] -> TCMT IO Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM ([TCMT IO Bool] -> TCMT IO Bool) -> [TCMT IO Bool] -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ (QName -> TCMT IO Bool) -> [QName] -> [TCMT IO Bool]
forall a b. (a -> b) -> [a] -> [b]
map QName -> TCMT IO Bool
check [QName]
cons)
([Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return [Polarity]
polIn)
(TCM [Polarity] -> TCM [Polarity])
-> TCM [Polarity] -> TCM [Polarity]
forall a b. (a -> b) -> a -> b
$ do
QName -> ([Occurrence] -> [Occurrence]) -> TCM ()
modifyArgOccurrences QName
d (([Occurrence] -> [Occurrence]) -> TCM ())
-> ([Occurrence] -> [Occurrence]) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ occ :: [Occurrence]
occ -> Int -> [Occurrence] -> [Occurrence]
forall a. Int -> [a] -> [a]
take Int
np [Occurrence]
occ [Occurrence] -> [Occurrence] -> [Occurrence]
forall a. [a] -> [a] -> [a]
++ [Occurrence
JustPos]
[Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return [Polarity]
polCo
_ -> TCM [Polarity]
exit
checkSizeIndex :: QName -> Nat -> Type -> TCM Bool
checkSizeIndex :: QName -> Int -> Type -> TCMT IO Bool
checkSizeIndex d :: QName
d i :: Int
i a :: Type
a = do
VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc "tc.polarity.size" 15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc -> TCM Doc
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
[ "checking that constructor target type " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
, " is data type " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
, " and has size index (successor(s) of) " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> Term
var Int
i)
]
case Type -> Term
forall t a. Type'' t a -> a
unEl Type
a of
Def d0 :: QName
d0 es :: Elims
es -> do
TCMT IO (Maybe QName) -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m (Maybe a) -> m () -> m ()
whenNothingM (QName -> QName -> TCMT IO (Maybe QName)
forall (m :: * -> *).
HasConstInfo m =>
QName -> QName -> m (Maybe QName)
sameDef QName
d QName
d0) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
Int
np <- Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Int -> Int) -> TCMT IO (Maybe Int) -> TCMT IO Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Maybe Int)
getNumberOfParameters QName
d0
let (pars :: Elims
pars, Apply ix :: Arg Term
ix : ixs :: Elims
ixs) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
np Elims
es
DeepSizeView
s <- Term -> TCM DeepSizeView
deepSizeView (Term -> TCM DeepSizeView) -> Term -> TCM DeepSizeView
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
ix
case DeepSizeView
s of
DSizeVar j :: Int
j _ | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j
-> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Bool
forall t. Free t => Int -> t -> Bool
freeIn Int
i (Elims
pars Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
ixs)
_ -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
_ -> TCMT IO Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
class HasPolarity a where
polarities :: Nat -> a -> TCM [Polarity]
polarity :: HasPolarity a => Nat -> a -> TCM Polarity
polarity :: Int -> a -> TCMT IO Polarity
polarity i :: Int
i x :: a
x = do
[Polarity]
ps <- Int -> a -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i a
x
case [Polarity]
ps of
[] -> Polarity -> TCMT IO Polarity
forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Nonvariant
ps :: [Polarity]
ps -> Polarity -> TCMT IO Polarity
forall (m :: * -> *) a. Monad m => a -> m a
return (Polarity -> TCMT IO Polarity) -> Polarity -> TCMT IO Polarity
forall a b. (a -> b) -> a -> b
$ (Polarity -> Polarity -> Polarity) -> [Polarity] -> Polarity
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Polarity -> Polarity -> Polarity
(/\) [Polarity]
ps
instance HasPolarity a => HasPolarity (Arg a) where
polarities :: Int -> Arg a -> TCM [Polarity]
polarities i :: Int
i = Int -> a -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i (a -> TCM [Polarity]) -> (Arg a -> a) -> Arg a -> TCM [Polarity]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg a -> a
forall e. Arg e -> e
unArg
instance HasPolarity a => HasPolarity (Dom a) where
polarities :: Int -> Dom a -> TCM [Polarity]
polarities i :: Int
i = Int -> a -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i (a -> TCM [Polarity]) -> (Dom a -> a) -> Dom a -> TCM [Polarity]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom a -> a
forall t e. Dom' t e -> e
unDom
instance HasPolarity a => HasPolarity (Abs a) where
polarities :: Int -> Abs a -> TCM [Polarity]
polarities i :: Int
i (Abs _ b :: a
b) = Int -> a -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) a
b
polarities i :: Int
i (NoAbs _ v :: a
v) = Int -> a -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i a
v
instance HasPolarity a => HasPolarity [a] where
polarities :: Int -> [a] -> TCM [Polarity]
polarities i :: Int
i xs :: [a]
xs = [[Polarity]] -> [Polarity]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Polarity]] -> [Polarity])
-> TCMT IO [[Polarity]] -> TCM [Polarity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> TCM [Polarity]) -> [a] -> TCMT IO [[Polarity]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int -> a -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i) [a]
xs
instance (HasPolarity a, HasPolarity b) => HasPolarity (a, b) where
polarities :: Int -> (a, b) -> TCM [Polarity]
polarities i :: Int
i (x :: a
x, y :: b
y) = [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
(++) ([Polarity] -> [Polarity] -> [Polarity])
-> TCM [Polarity] -> TCMT IO ([Polarity] -> [Polarity])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> a -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i a
x TCMT IO ([Polarity] -> [Polarity])
-> TCM [Polarity] -> TCM [Polarity]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> b -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i b
y
instance HasPolarity Type where
polarities :: Int -> Type -> TCM [Polarity]
polarities i :: Int
i (El _ v :: Term
v) = Int -> Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Term
v
instance HasPolarity a => HasPolarity (Elim' a) where
polarities :: Int -> Elim' a -> TCM [Polarity]
polarities i :: Int
i Proj{} = [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return []
polarities i :: Int
i (Apply a :: Arg a
a) = Int -> Arg a -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Arg a
a
polarities i :: Int
i (IApply x :: a
x y :: a
y a :: a
a) = Int -> (a, (a, a)) -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i (a
x,(a
y,a
a))
instance HasPolarity Term where
polarities :: Int -> Term -> TCM [Polarity]
polarities i :: Int
i v :: Term
v = do
Term
v <- Term -> TCMT IO Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v
case Term
v of
Var n :: Int
n ts :: Elims
ts | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i -> (Polarity
Covariant Polarity -> [Polarity] -> [Polarity]
forall a. a -> [a] -> [a]
:) ([Polarity] -> [Polarity])
-> ([Polarity] -> [Polarity]) -> [Polarity] -> [Polarity]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Polarity -> Polarity) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map (Polarity -> Polarity -> Polarity
forall a b. a -> b -> a
const Polarity
Invariant) ([Polarity] -> [Polarity]) -> TCM [Polarity] -> TCM [Polarity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Elims -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Elims
ts
| Bool
otherwise -> (Polarity -> Polarity) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map (Polarity -> Polarity -> Polarity
forall a b. a -> b -> a
const Polarity
Invariant) ([Polarity] -> [Polarity]) -> TCM [Polarity] -> TCM [Polarity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Elims -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Elims
ts
Lam _ t :: Abs Term
t -> Int -> Abs Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Abs Term
t
Lit _ -> [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return []
Level l :: Level
l -> Int -> Level -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Level
l
Def x :: QName
x ts :: Elims
ts -> do
[Polarity]
pols <- QName -> TCM [Polarity]
forall (m :: * -> *). HasConstInfo m => QName -> m [Polarity]
getPolarity QName
x
let compose :: Polarity -> [Polarity] -> [Polarity]
compose p :: Polarity
p ps :: [Polarity]
ps = (Polarity -> Polarity) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map (Polarity -> Polarity -> Polarity
composePol Polarity
p) [Polarity]
ps
[[Polarity]] -> [Polarity]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Polarity]] -> [Polarity])
-> ([[Polarity]] -> [[Polarity]]) -> [[Polarity]] -> [Polarity]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Polarity -> [Polarity] -> [Polarity])
-> [Polarity] -> [[Polarity]] -> [[Polarity]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Polarity -> [Polarity] -> [Polarity]
compose ([Polarity]
pols [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
++ Polarity -> [Polarity]
forall a. a -> [a]
repeat Polarity
Invariant) ([[Polarity]] -> [Polarity])
-> TCMT IO [[Polarity]] -> TCM [Polarity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Elim -> TCM [Polarity]) -> Elims -> TCMT IO [[Polarity]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int -> Elim -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i) Elims
ts
Con _ _ ts :: Elims
ts -> Int -> Elims -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Elims
ts
Pi a :: Dom Type
a b :: Abs Type
b -> [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
(++) ([Polarity] -> [Polarity] -> [Polarity])
-> TCM [Polarity] -> TCMT IO ([Polarity] -> [Polarity])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Polarity -> Polarity) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map Polarity -> Polarity
neg ([Polarity] -> [Polarity]) -> TCM [Polarity] -> TCM [Polarity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Dom Type -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Dom Type
a) TCMT IO ([Polarity] -> [Polarity])
-> TCM [Polarity] -> TCM [Polarity]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> Abs Type -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Abs Type
b
Sort s :: Sort
s -> [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return []
MetaV _ ts :: Elims
ts -> (Polarity -> Polarity) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map (Polarity -> Polarity -> Polarity
forall a b. a -> b -> a
const Polarity
Invariant) ([Polarity] -> [Polarity]) -> TCM [Polarity] -> TCM [Polarity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Elims -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Elims
ts
DontCare t :: Term
t -> Int -> Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Term
t
Dummy{} -> [Polarity] -> TCM [Polarity]
forall (m :: * -> *) a. Monad m => a -> m a
return []
instance HasPolarity Level where
polarities :: Int -> Level -> TCM [Polarity]
polarities i :: Int
i (Max _ as :: [PlusLevel' Term]
as) = Int -> [PlusLevel' Term] -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i [PlusLevel' Term]
as
instance HasPolarity PlusLevel where
polarities :: Int -> PlusLevel' Term -> TCM [Polarity]
polarities i :: Int
i (Plus _ l :: LevelAtom' Term
l) = Int -> LevelAtom' Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i LevelAtom' Term
l
instance HasPolarity LevelAtom where
polarities :: Int -> LevelAtom' Term -> TCM [Polarity]
polarities i :: Int
i l :: LevelAtom' Term
l = case LevelAtom' Term
l of
MetaLevel _ vs :: Elims
vs -> (Polarity -> Polarity) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map (Polarity -> Polarity -> Polarity
forall a b. a -> b -> a
const Polarity
Invariant) ([Polarity] -> [Polarity]) -> TCM [Polarity] -> TCM [Polarity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Elims -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Elims
vs
BlockedLevel _ v :: Term
v -> Int -> Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Term
v
NeutralLevel _ v :: Term
v -> Int -> Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Term
v
UnreducedLevel v :: Term
v -> Int -> Term -> TCM [Polarity]
forall a. HasPolarity a => Int -> a -> TCM [Polarity]
polarities Int
i Term
v