module Agda.TypeChecking.Polarity where
import Control.Applicative
import Control.Monad.State
import Control.Monad.Error
import Data.List
import Data.Traversable (traverse)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Positivity
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Free hiding (Occurrence(..))
import Agda.TypeChecking.Monad.Builtin
import Agda.Interaction.Options
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Impossible
import Agda.Utils.Size
#include "../undefined.h"
(/\) :: Polarity -> Polarity -> Polarity
Nonvariant /\ b = b
a /\ Nonvariant = a
a /\ b | a == b = a
| otherwise = Invariant
neg :: Polarity -> Polarity
neg Covariant = Contravariant
neg Contravariant = Covariant
neg Invariant = Invariant
neg Nonvariant = Nonvariant
composePol :: Polarity -> Polarity -> Polarity
composePol Nonvariant _ = Nonvariant
composePol _ Nonvariant = Nonvariant
composePol Invariant _ = Invariant
composePol Covariant x = x
composePol Contravariant x = neg x
polFromOcc :: Occurrence -> Polarity
polFromOcc o = case o of
GuardPos -> Covariant
StrictPos -> Covariant
JustPos -> Covariant
JustNeg -> Contravariant
Mixed -> Invariant
Unused -> Nonvariant
nextPolarity :: [Polarity] -> (Polarity, [Polarity])
nextPolarity [] = (Invariant, [])
nextPolarity (p : ps) = (p, ps)
purgeNonvariant :: [Polarity] -> [Polarity]
purgeNonvariant = map (\ p -> if p == Nonvariant then Invariant else p)
computePolarity :: QName -> TCM ()
computePolarity x = do
reportSLn "tc.polarity.set" 25 $ "Computing polarity of " ++ show x
def <- getConstInfo x
let pol0 = map polFromOcc $ defArgOccurrences def
reportSLn "tc.polarity.set" 15 $ "Polarity of " ++ show x ++ " from positivity: " ++ show pol0
pol1 <- sizePolarity x pol0
let t = defType def
reportSDoc "tc.polarity.set" 15 $ text "Refining polarity with type " <+> prettyTCM t
pol <- enablePhantomTypes (theDef def) <$> dependentPolarity t pol1
reportSLn "tc.polarity.set" 10 $ "Polarity of " ++ show x ++ ": " ++ show pol
setPolarity x $ pol
t <- nonvariantToUnusedArg pol t
modifySignature $ updateDefinition x $
updateTheDef (nonvariantToUnusedArgInDef pol) . updateDefType (const t)
enablePhantomTypes :: Defn -> [Polarity] -> [Polarity]
enablePhantomTypes def pol = case def of
Datatype{ dataPars = np } -> enable np
Record { recPars = np } -> enable np
_ -> pol
where enable np = let (pars, rest) = genericSplitAt np pol
in purgeNonvariant pars ++ rest
dependentPolarity :: Type -> [Polarity] -> TCM [Polarity]
dependentPolarity t [] = return []
dependentPolarity t pols@(p:ps) = do
t <- reduce $ unEl t
case ignoreSharing t of
Pi a b -> do
let c = absBody b
ps <- dependentPolarity c ps
p <- case b of
Abs{} | p /= Invariant ->
ifM (relevantInIgnoringNonvariant 0 c ps)
(return Invariant)
(return p)
_ -> return p
return $ p : ps
_ -> return pols
relevantInIgnoringNonvariant :: Nat -> Type -> [Polarity] -> TCM Bool
relevantInIgnoringNonvariant i t [] = return $ i `relevantInIgnoringSortAnn` t
relevantInIgnoringNonvariant i t (p:ps) = do
t <- reduce $ unEl t
case ignoreSharing t of
Pi a b -> if p /= Nonvariant && i `relevantInIgnoringSortAnn` a then return True
else relevantInIgnoringNonvariant (i + 1) (absBody b) ps
_ -> return $ i `relevantInIgnoringSortAnn` t
mkUnused :: Relevance -> Relevance
mkUnused Relevant = UnusedArg
mkUnused r = r
nonvariantToUnusedArg :: [Polarity] -> Type -> TCM Type
nonvariantToUnusedArg [] t = return t
nonvariantToUnusedArg (p:ps) t = do
t <- reduce t
case ignoreSharingType t of
El s (Pi a b) -> do
let a' = if p == Nonvariant then mapDomRelevance mkUnused a else a
El s . Pi a' <$> traverse (nonvariantToUnusedArg ps) b
_ -> return t
nonvariantToUnusedArgInDef :: [Polarity] -> Defn -> Defn
nonvariantToUnusedArgInDef pol def = case def of
Function { funClauses = cl } ->
def { funClauses = map (nonvariantToUnusedArgInClause pol) cl }
_ -> def
nonvariantToUnusedArgInClause :: [Polarity] -> Clause -> Clause
nonvariantToUnusedArgInClause pol cl@Clause{clauseTel = tel, clausePerm = perm, clausePats = ps} =
let adjPat p Nonvariant
| properlyMatching (unArg p) = __IMPOSSIBLE__
| otherwise = mapArgRelevance mkUnused p
adjPat p _ = p
ps' = zipWith adjPat ps (pol ++ repeat Invariant)
rels0 = argRelevance <$> (patternVars =<< ps')
rels = permute perm rels0
updateDom UnusedArg = mapDomRelevance mkUnused
updateDom r = id
tel' = telFromList $ zipWith updateDom rels $ telToList tel
in cl { clausePats = ps', clauseTel = tel'}
sizePolarity :: QName -> [Polarity] -> TCM [Polarity]
sizePolarity d pol0 = do
let exit = return pol0
ifM (not . optSizedTypes <$> pragmaOptions) exit $ do
def <- getConstInfo d
case theDef def of
Datatype{ dataPars = np, dataCons = cons } -> do
let TelV tel _ = telView' $ defType def
(parTel, ixTel) = genericSplitAt np $ telToList tel
case ixTel of
[] -> exit
Dom _ _ (_, a) : _ -> ifM ((/= Just BoundedNo) <$> isSizeType a) exit $ do
let pol = genericTake np pol0
polCo = pol ++ [Covariant]
polIn = pol ++ [Invariant]
setPolarity d $ polCo
let check c = do
t <- defType <$> getConstInfo c
addCtxTel (telFromList parTel) $ do
let pars = map (defaultArg . var) $ downFrom np
TelV conTel target <- telView =<< (t `piApplyM` pars)
case conTel of
EmptyTel -> return False
ExtendTel arg tel ->
ifM ((/= Just BoundedNo) <$> isSizeType (unDom arg)) (return False) $ do
isPos <- underAbstraction arg tel $ \tel -> do
pols <- zipWithM polarity [0..] $ map (snd . unDom) $ telToList tel
return $ all (`elem` [Nonvariant, Covariant]) pols
let sizeArg = size tel
isLin <- checkSizeIndex np sizeArg target
return $ isPos && isLin
ifM (andM $ map check cons)
(return polCo)
(return polIn)
_ -> exit
checkSizeIndex :: Nat -> Nat -> Type -> TCM Bool
checkSizeIndex np i a =
case ignoreSharing $ unEl a of
Def _ args -> do
let excl = not $ freeIn i (pars ++ ixs)
s <- sizeView ix
case s of
SizeSuc v | Var j [] <- ignoreSharing v
-> return $ and [ excl, i == j ]
_ -> return False
where
(pars, Arg _ _ ix : ixs) = genericSplitAt np args
_ -> __IMPOSSIBLE__
class HasPolarity a where
polarities :: Nat -> a -> TCM [Polarity]
polarity :: HasPolarity a => Nat -> a -> TCM Polarity
polarity i x = do
ps <- polarities i x
case ps of
[] -> return Nonvariant
ps -> return $ foldr1 (/\) ps
instance HasPolarity a => HasPolarity (Arg a) where
polarities i = polarities i . unArg
instance HasPolarity a => HasPolarity (Dom a) where
polarities i = polarities i . unDom
instance HasPolarity a => HasPolarity (Abs a) where
polarities i (Abs _ b) = polarities (i + 1) b
polarities i (NoAbs _ v) = polarities i v
instance HasPolarity a => HasPolarity [a] where
polarities i xs = concat <$> mapM (polarities i) xs
instance (HasPolarity a, HasPolarity b) => HasPolarity (a, b) where
polarities i (x, y) = (++) <$> polarities i x <*> polarities i y
instance HasPolarity Type where
polarities i (El _ v) = polarities i v
instance HasPolarity Term where
polarities i v = do
v <- instantiate v
case v of
Var n ts | n == i -> (Covariant :) . map (const Invariant) <$> polarities i ts
| otherwise -> map (const Invariant) <$> polarities i ts
Lam _ t -> polarities i t
Lit _ -> return []
Level l -> polarities i l
Def x ts -> do
pols <- getPolarity x
let compose p ps = map (composePol p) ps
concat . zipWith compose (pols ++ repeat Invariant) <$> mapM (polarities i) ts
Con _ ts -> polarities i ts
Pi a b -> (++) <$> (map neg <$> polarities i a) <*> polarities i b
Sort s -> return []
MetaV _ ts -> map (const Invariant) <$> polarities i ts
Shared p -> polarities i $ derefPtr p
DontCare t -> polarities i t
instance HasPolarity Level where
polarities i (Max as) = polarities i as
instance HasPolarity PlusLevel where
polarities i ClosedLevel{} = return []
polarities i (Plus _ l) = polarities i l
instance HasPolarity LevelAtom where
polarities i l = case l of
MetaLevel _ vs -> map (const Invariant) <$> polarities i vs
BlockedLevel _ v -> polarities i v
NeutralLevel v -> polarities i v
UnreducedLevel v -> polarities i v