module Agda.TypeChecking.Polarity where
import Control.Applicative
import Control.Monad.State
import Data.List
import Data.Maybe
import Data.Traversable (traverse)
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Free hiding (Occurrence(..))
import Agda.TypeChecking.Positivity.Occurrence
import Agda.Interaction.Options
import Agda.Utils.List
import Agda.Utils.Maybe ( whenNothingM )
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
(/\) :: 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 Covariant else p)
computePolarity :: QName -> TCM ()
computePolarity x = inConcreteOrAbstractMode x $ do
reportSLn "tc.polarity.set" 25 $ "Computing polarity of " ++ show x
def <- getConstInfo x
let npars = droppedPars def
let pol0 = replicate npars Nonvariant ++ 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 <- dependentPolarity t (enablePhantomTypes (theDef def) pol1) pol1
reportSLn "tc.polarity.set" 10 $ "Polarity of " ++ show x ++ ": " ++ show pol
setPolarity x $ drop npars pol
t <- if (defAbstract def == AbstractDef)
then return t
else 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] -> [Polarity] -> TCM [Polarity]
dependentPolarity t _ [] = return []
dependentPolarity t [] (_ : _) = __IMPOSSIBLE__
dependentPolarity t (q:qs) pols@(p:ps) = do
t <- reduce $ unEl t
case ignoreSharing t of
Pi dom b -> do
let c = absBody b
ps <- dependentPolarity c qs ps
let mp = ifM (isJust <$> isSizeType (unDom dom)) (return p) (return q)
p <- case b of
Abs{} | p /= Invariant ->
ifM (relevantInIgnoringNonvariant 0 c ps)
(return Invariant)
mp
_ -> mp
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 mapRelevance 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, namedClausePats = ps} =
let adjPat p Nonvariant
| properlyMatching (namedArg p) = __IMPOSSIBLE__
| otherwise = mapRelevance mkUnused p
adjPat p _ = p
ps' = zipWith adjPat ps (pol ++ repeat Invariant)
rels0 = getRelevance <$> (concatMap (patternVars . fmap namedThing) ps')
rels = permute perm rels0
updateDom UnusedArg = mapRelevance mkUnused
updateDom r = id
tel' = telFromList $ zipWith updateDom rels $ telToList tel
in cl { namedClausePats = 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
let isPos = underAbstraction arg tel $ \ tel -> do
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: " ++ show pols
return $ all (`elem` [Nonvariant, Covariant]) pols
let sizeArg = size tel
isLin = addContext conTel $ checkSizeIndex d np sizeArg target
ok <- isPos `and2M` isLin
reportSDoc "tc.polarity.size" 15 $
text "constructor" <+> prettyTCM c <+>
text (if ok then "passes" else "fails") <+>
text "size polarity check"
return ok
ifNotM (andM $ map check cons)
(return polIn)
$ do
modifyArgOccurrences d $ \ occ -> take np occ ++ [JustPos]
return polCo
_ -> exit
checkSizeIndex :: QName -> Nat -> Nat -> Type -> TCM Bool
checkSizeIndex d np i a = do
reportSDoc "tc.polarity.size" 15 $ withShowAllArguments $
text "checking that constructor target type " <+> prettyTCM a <+>
text "is data type " <+> prettyTCM d <+>
text "has size index successor of " <+> prettyTCM (var i)
case ignoreSharing $ unEl a of
Def d0 es -> do
whenNothingM (sameDef d d0) __IMPOSSIBLE__
s <- sizeView $ unArg ix
case s of
SizeSuc v | Var j [] <- ignoreSharing v, i == j
-> return $ not $ freeIn i (pars ++ ixs)
_ -> return False
where
(pars, Apply ix : ixs) = genericSplitAt np es
_ -> __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 (I.Arg a) where
polarities i = polarities i . unArg
instance HasPolarity a => HasPolarity (I.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 a => HasPolarity (Elim' a) where
polarities i (Proj p) = return []
polarities i (Apply a) = polarities i a
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
ExtLam{} -> __IMPOSSIBLE__
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