module Agda.TypeChecking.Polarity where
import Control.Applicative
import Control.Monad.State
import Control.Monad.Error
import Data.List
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Positivity
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Free
import Agda.TypeChecking.Monad.Builtin
import Agda.Interaction.Options
import Agda.Utils.Monad
import Agda.Utils.Impossible
import Agda.Utils.Size
#include "../undefined.h"
getArity :: QName -> TCM Arity
getArity x = do
def <- theDef <$> getConstInfo x
case def of
Axiom{} -> return 0
Function{ funClauses = c : _ } -> return $ genericLength (clausePats $ translatedClause c)
Function{ funClauses = [] } -> return 0
Datatype{ dataPars = np, dataIxs = ni } -> return np
Record{ recPars = n } -> return n
Constructor{} -> return 0
Primitive{} -> return 0
computePolarity :: QName -> TCM ()
computePolarity x = do
reportSLn "tc.polarity.set" 15 $ "Computing polarity of " ++ show x
n <- getArity x
reportSLn "tc.polarity.set" 20 $ " arity = " ++ show n
pol0 <- mapM getPol [0..n 1]
setPolarity x $ pol0 ++ [Covariant]
pol1 <- sizePolarity x
let pol = pol0 ++ pol1
reportSLn "tc.polarity.set" 10 $ "Polarity of " ++ show x ++ ": " ++ show pol
setPolarity x pol
where
getPol :: Nat -> TCM Polarity
getPol i = do
o <- getArgOccurrence x i
case o of
Positive -> return Covariant
Negative -> return Invariant
Unused -> return Invariant
sizePolarity :: QName -> TCM [Polarity]
sizePolarity d =
ifM (not . optSizedTypes <$> pragmaOptions) (return []) $ 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
[] -> return []
Arg _ _ (_, a) : _ -> ifM (not <$> isSizeType a) (return []) $ do
let check c = do
t <- defType <$> getConstInfo c
addCtxTel (telFromList parTel) $ do
let pars = reverse [ defaultArg $ Var i [] | i <- [0..np 1] ]
TelV conTel target <- telView =<< (t `piApplyM` pars)
case conTel of
EmptyTel -> return False
ExtendTel arg tel ->
ifM (not <$> isSizeType (unArg arg)) (return False) $ do
isPos <- underAbstraction arg tel $ \tel -> do
pols <- zipWithM polarity [0..] $ map (snd . unArg) $ telToList tel
return $ all (== Covariant) pols
let sizeArg = size tel
isLin <- checkSizeIndex np sizeArg target
return $ isPos && isLin
ifM (and <$> mapM check cons)
(return [Covariant])
(return [Invariant])
_ -> return []
checkSizeIndex :: Nat -> Nat -> Type -> TCM Bool
checkSizeIndex np i (El _ (Def _ args)) = do
let excl = not $ freeIn i (pars ++ ixs)
s <- sizeView ix
case s of
SizeSuc (Var j []) -> return $ and [ excl, i == j ]
_ -> return False
where
(pars, Arg _ _ ix : ixs) = genericSplitAt np args
checkSizeIndex _ _ _ = __IMPOSSIBLE__
(/\) :: Polarity -> Polarity -> Polarity
a /\ b | a == b = a
| otherwise = Invariant
neg :: Polarity -> Polarity
neg Covariant = Contravariant
neg Contravariant = Covariant
neg Invariant = Invariant
composePol :: Polarity -> Polarity -> Polarity
composePol Invariant _ = Invariant
composePol Covariant x = x
composePol Contravariant x = neg x
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 Covariant
ps -> return $ foldr1 (/\) ps
instance HasPolarity a => HasPolarity (Arg a) where
polarities i = polarities i . unArg
instance HasPolarity a => HasPolarity (Abs a) where
polarities i = polarities (i + 1) . absBody
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 = case v of
Var n ts | n == i -> (Covariant :) <$> polarities i ts
| otherwise -> polarities i ts
Lam _ t -> polarities i t
Lit _ -> return []
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
Fun a b -> (++) <$> (map neg <$> polarities i a) <*> polarities i b
Sort _ -> return []
MetaV _ ts -> map (const Invariant) <$> polarities i ts
DontCare -> return []