module Agda.TypeChecking.Coverage where
import Control.Monad
import Control.Monad.Error
import Control.Applicative hiding (empty)
import Data.List
import qualified Data.Set as Set
import Data.Set (Set)
import qualified Data.Traversable as Trav
import Agda.Syntax.Position
import qualified Agda.Syntax.Common as Common
import Agda.Syntax.Common hiding (Arg,Dom)
import qualified Agda.Syntax.Common as C
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Closure
import Agda.TypeChecking.Monad.Trace
import Agda.TypeChecking.Monad.Signature
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.Exception
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Rules.LHS.Problem (FlexibleVar(..),flexibleVarFromHiding)
import Agda.TypeChecking.Rules.LHS.Unify
import Agda.TypeChecking.Rules.LHS.Instantiate
import Agda.TypeChecking.Rules.LHS
import qualified Agda.TypeChecking.Rules.LHS.Split as Split
import Agda.TypeChecking.Coverage.Match
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Datatypes (getConForm)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Records (isRecordType)
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Irrelevance
import Agda.Interaction.Options
import Agda.Utils.Functor (for, ($>))
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Size
import Agda.Utils.Tuple
#include "../undefined.h"
import Agda.Utils.Impossible
data SplitClause = SClause
{ scTel :: Telescope
, scPerm :: Permutation
, scPats :: [I.NamedArg Pattern]
, scSubst :: Substitution
, scTarget :: Maybe (I.Arg Type)
}
data Covering = Covering
{ covSplitArg :: Nat
, covSplitClauses :: [(QName, SplitClause)]
}
splitClauses :: Covering -> [SplitClause]
splitClauses (Covering _ qcs) = map snd qcs
clauseToSplitClause :: Clause -> SplitClause
clauseToSplitClause cl = SClause
{ scTel = clauseTel cl
, scPerm = clausePerm cl
, scPats = namedClausePats cl
, scSubst = idS
, scTarget = clauseType cl
}
type CoverM = ExceptionT SplitError TCM
checkCoverage :: QName -> TCM ()
checkCoverage f = do
d <- getConstInfo f
case theDef d of
Function{ funProjection = Nothing, funClauses = cs@(_:_) } -> do
coverageCheck f (defType d) cs
return ()
Function{ funProjection = Just _ } -> __IMPOSSIBLE__
_ -> __IMPOSSIBLE__
coverageCheck :: QName -> Type -> [Clause] -> TCM SplitTree
coverageCheck f t cs = do
TelV gamma a <- telView t
let
n = size gamma
lgamma = telToList gamma
xs = map (argFromDom . fmap (namedVarP . fst)) $ lgamma
sc = SClause gamma (idP n) xs idS $ Just $ defaultArg a
reportSDoc "tc.cover.top" 10 $ vcat
[ text $ "Coverage checking " ++ show f
, nest 2 $ vcat $ map (text . show . clausePats) cs
]
(splitTree, used, pss) <- cover f cs sc
reportSDoc "tc.cover.splittree" 10 $ vcat
[ text "generated split tree for" <+> prettyTCM f
, text $ show splitTree
]
whenM (optCompletenessCheck <$> pragmaOptions) $
unless (null pss) $
setCurrentRange (getRange cs) $
typeError $ CoverageFailure f (map (map $ fmap namedThing) pss)
let is = Set.toList $ Set.difference (Set.fromList [0..genericLength cs 1]) used
unless (null is) $ do
let unreached = map (cs !!) is
setCurrentRange (getRange unreached) $
typeError $ UnreachableClauses f (map clausePats unreached)
return splitTree
cover :: QName -> [Clause] -> SplitClause -> TCM (SplitTree, Set Nat, [[I.NamedArg Pattern]])
cover f cs sc@(SClause tel perm ps _ target) = do
reportSDoc "tc.cover.cover" 10 $ vcat
[ text "checking coverage of pattern:"
, nest 2 $ text "tel =" <+> prettyTCM tel
, nest 2 $ text "perm =" <+> text (show perm)
, nest 2 $ text "ps =" <+> text (show ps)
]
let ups = map (fmap namedThing) ps
case match cs ups perm of
Yes i -> do
reportSLn "tc.cover.cover" 10 $ "pattern covered by clause " ++ show i
let is = [ j | (j, c) <- zip [0..i1] cs, matchLits c ups perm ]
reportSLn "tc.cover.cover" 10 $ "literal matches: " ++ show is
return (SplittingDone (size tel), Set.fromList (i : is), [])
No -> do
reportSLn "tc.cover" 20 $ "pattern is not covered"
return (SplittingDone (size tel), Set.empty, [ps])
BlockP -> do
reportSLn "tc.cover" 20 $ "blocked by projection pattern"
let done = return (SplittingDone (size tel), Set.empty, [ps])
caseMaybeM (splitResult f sc) done $ \ (Covering n scs) -> do
(projs, (trees, useds, psss)) <- mapSnd unzip3 . unzip <$> do
forM scs $ \ (proj, sc') -> (proj,) <$> do cover f cs =<< fixTarget sc'
let tree = SplitAt n $ zip projs trees
return (tree, Set.unions useds, concat psss)
Block bs -> do
reportSLn "tc.cover.strategy" 20 $ "blocking vars = " ++ show bs
xs <- splitStrategy bs tel
r <- altM1 (split Inductive sc) xs
case r of
Left err -> case err of
CantSplit c tel us vs _ -> typeError $ CoverageCantSplitOn c tel us vs
NotADatatype a -> enterClosure a $ typeError . CoverageCantSplitType
IrrelevantDatatype a -> enterClosure a $ typeError . CoverageCantSplitIrrelevantType
CoinductiveDatatype a -> enterClosure a $ typeError . CoverageCantSplitType
GenericSplitError s -> fail $ "failed to split: " ++ s
Right (Covering n []) ->
return (SplittingDone (size tel), Set.empty, [])
Right (Covering n scs) -> do
(trees, useds, psss) <- unzip3 <$> mapM (cover f cs) (map snd scs)
let tree = SplitAt n $ zipWith (\ (q,_) t -> (q,t)) scs trees
return (tree, Set.unions useds, concat psss)
splitStrategy :: BlockingVars -> Telescope -> TCM BlockingVars
splitStrategy bs tel = return $ updateLast clearBlockingVarCons xs
where
xs = bs
isDatatype :: (MonadTCM tcm, MonadException SplitError tcm) =>
Induction -> Dom Type ->
tcm (QName, [Arg Term], [Arg Term], [QName])
isDatatype ind at = do
let t = unDom at
throw f = throwException . f =<< do liftTCM $ buildClosure t
t' <- liftTCM $ reduce t
case ignoreSharing $ unEl t' of
Def d es -> do
let ~(Just args) = allApplyElims es
def <- liftTCM $ theDef <$> getConstInfo d
splitOnIrrelevantDataAllowed <- liftTCM $ optExperimentalIrrelevance <$> pragmaOptions
case def of
Datatype{dataPars = np, dataCons = cs, dataInduction = i}
| i == CoInductive && ind /= CoInductive ->
throw CoinductiveDatatype
| isIrrelevant at && not splitOnIrrelevantDataAllowed ->
throw IrrelevantDatatype
| otherwise -> do
let (ps, is) = genericSplitAt np args
return (d, ps, is, cs)
Record{recPars = np, recConHead = con} ->
return (d, args, [], [conName con])
_ -> throw NotADatatype
_ -> throw NotADatatype
fixTarget :: SplitClause -> TCM SplitClause
fixTarget sc@SClause{ scSubst = sigma, scTarget = target } =
caseMaybe target (return sc) $ \ a -> do
reportSDoc "tc.cover.target" 20 $
text "target type before substitution: " <+> prettyTCM a
TelV tel b <- telView $ applySubst sigma $ unArg a
reportSDoc "tc.cover.target" 10 $
text "telescope (after substitution): " <+> prettyTCM tel
let n = size tel
lgamma = telToList tel
xs = for lgamma $ \ (Common.Dom ai (x, _)) -> Common.Arg ai $ namedVarP "_"
if (n == 0) then return sc { scTarget = Just $ a $> b }
else return $ SClause
{ scTel = telFromList $ telToList (scTel sc) ++ lgamma
, scPerm = liftP n $ scPerm sc
, scPats = scPats sc ++ xs
, scSubst = liftS n $ sigma
, scTarget = Just $ a $> b
}
computeNeighbourhood
:: Telescope
-> PatVarName
-> Telescope
-> Permutation
-> QName
-> Args
-> Args
-> Nat
-> OneHolePatterns
-> QName
-> CoverM (Maybe SplitClause)
computeNeighbourhood delta1 n delta2 perm d pars ixs hix hps c = do
dtype <- liftTCM $ (`piApply` pars) . defType <$> getConstInfo d
con <- liftTCM $ getConForm c
con <- return $ con { conName = c }
ctype <- liftTCM $ defType <$> getConInfo con
(gamma0, cixs) <- do
TelV gamma0 (El _ d) <- liftTCM $ telView (ctype `piApply` pars)
let Def _ es = ignoreSharing d
Just cixs = allApplyElims es
return (gamma0, cixs)
let preserve (x, t@(El _ (Def d' _))) | d == d' = (n, t)
preserve (x, (El s (Shared p))) = preserve (x, El s $ derefPtr p)
preserve p = p
gammal = map (fmap preserve) . telToList $ gamma0
gamma = telFromList gammal
debugInit con ctype d pars ixs cixs delta1 delta2 gamma hps hix
let gammaDelta1 = gammal ++ telToList delta1
makeFlex i d = flexibleVarFromHiding (getHiding d) i
flex = zipWith makeFlex [0 .. size gammaDelta1 1] gammaDelta1
let conIxs = drop (size pars) cixs
givenIxs = raise (size gamma) ixs
r <- addCtxTel (delta1 `abstract` gamma) $
unifyIndices flex (raise (size gamma) dtype) conIxs givenIxs
case r of
NoUnify _ _ _ -> do
debugNoUnify
return Nothing
DontKnow _ -> do
debugCantSplit
throwException $ CantSplit (conName con) (delta1 `abstract` gamma) conIxs givenIxs
(map (var . flexVar) flex)
Unifies sub -> do
debugSubst "sub" sub
let conv = Con con $ teleArgs gamma
delta2' = subst conv $ raiseFrom 1 (size gamma) delta2
debugTel "delta2'" delta2'
let rho = liftS (size delta2') $ conv :# raiseS (size gamma)
let conp = ConP con Nothing $ map (fmap namedVarP) $ teleArgNames gamma
ps = plugHole conp hps
ps' = applySubst rho ps
debugPlugged ps ps'
let pad n xs x = xs ++ replicate (max 0 $ n size xs) x
sub' = replicate (size delta2') Nothing ++
pad (size delta1 + size gamma) (raise (size delta2') sub) Nothing
debugSubst "sub'" sub'
let theta = delta1 `abstract` gamma `abstract` delta2'
debugTel "theta" theta
(theta', iperm, rho', _) <- liftTCM $ instantiateTel sub' theta
debugTel "theta'" theta'
debugShow "iperm" iperm
let perm' = expandP hix (size gamma) perm
rperm = iperm `composeP` perm'
debugShow "perm'" perm'
debugShow "rperm" rperm
let ps'' = instantiatePattern sub' perm' ps'
rps = applySubst rho' ps''
let rsub = applySubst rho' rho
debugFinal theta' rperm rps
return $ Just $ SClause theta' rperm rps rsub Nothing
where
debugInit con ctype d pars ixs cixs delta1 delta2 gamma hps hix =
liftTCM $ reportSDoc "tc.cover.split.con" 20 $ vcat
[ text "computeNeighbourhood"
, nest 2 $ vcat
[ text "con =" <+> prettyTCM con
, text "ctype =" <+> prettyTCM ctype
, text "hps =" <+> text (show hps)
, text "d =" <+> prettyTCM d
, text "pars =" <+> prettyList (map prettyTCM pars)
, text "ixs =" <+> addCtxTel delta1 (prettyList (map prettyTCM ixs))
, text "cixs =" <+> do addCtxTel gamma $ prettyList (map prettyTCM cixs)
, text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> prettyTCM delta2
, text "gamma =" <+> prettyTCM gamma
, text "hix =" <+> text (show hix)
]
]
debugNoUnify =
liftTCM $ reportSLn "tc.cover.split.con" 20 " Constructor impossible!"
debugCantSplit =
liftTCM $ reportSLn "tc.cover.split.con" 20 " Bad split!"
debugSubst s sub =
liftTCM $ reportSDoc "tc.cover.split.con" 20 $ nest 2 $ vcat
[ text (s ++ " =") <+> brackets (fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) sub)
]
debugTel s tel =
liftTCM $ reportSDoc "tc.cover.split.con" 20 $ nest 2 $ vcat
[ text (s ++ " =") <+> prettyTCM tel
]
debugShow s x =
liftTCM $ reportSDoc "tc.cover.split.con" 20 $ nest 2 $ vcat
[ text (s ++ " =") <+> text (show x)
]
debugPlugged ps ps' =
liftTCM $ reportSDoc "tc.cover.split.con" 20 $ nest 2 $ vcat
[ text "ps =" <+> text (show ps)
, text "ps' =" <+> text (show ps')
]
debugFinal tel perm ps =
liftTCM $ reportSDoc "tc.cover.split.con" 20 $ nest 2 $ vcat
[ text "rtel =" <+> prettyTCM tel
, text "rperm =" <+> text (show perm)
, text "rps =" <+> text (show ps)
]
splitClauseWithAbsurd :: Clause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))
splitClauseWithAbsurd c x = split' Inductive (clauseToSplitClause c) (BlockingVar x Nothing)
splitLast :: Induction -> Telescope -> [I.NamedArg Pattern] -> TCM (Either SplitError Covering)
splitLast ind tel ps = split ind sc (BlockingVar 0 Nothing)
where sc = SClause tel (idP $ size tel) ps __IMPOSSIBLE__ Nothing
split :: Induction
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError Covering)
split ind sc x = fmap (blendInAbsurdClause (splitDbIndexToLevel sc x)) <$>
split' ind sc x
where
blendInAbsurdClause :: Nat -> Either SplitClause Covering -> Covering
blendInAbsurdClause n = either (const $ Covering n []) id
splitDbIndexToLevel :: SplitClause -> BlockingVar -> Nat
splitDbIndexToLevel sc@SClause{ scTel = tel, scPerm = perm } x =
dbIndexToLevel tel perm $ blockingVarNo x
dbIndexToLevel tel perm x = if n < 0 then __IMPOSSIBLE__ else n
where n = if k < 0 then __IMPOSSIBLE__ else permute perm [0..] !! k
k = size tel x 1
split' :: Induction
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError (Either SplitClause Covering))
split' ind sc@(SClause tel perm ps _ target) (BlockingVar x mcons) = liftTCM $ runExceptionT $ do
debugInit tel perm x ps
(n, t, delta1, delta2) <- do
let (tel1, C.Dom info (n, t) : tel2) = genericSplitAt (size tel x 1) $ telToList tel
return (n, C.Dom info t, telFromList tel1, telFromList tel2)
(hps, hix) <- do
let holes = reverse $ permute perm $ zip [0..] $ allHolesWithContents ps
unless (length holes == length (telToList tel)) $
fail "split: bad holes or tel"
let (hix, (VarP s, hps)) = holes !! x
debugHoleAndType delta1 delta2 s hps t
return (hps, hix)
(d, pars, ixs, cons) <- inContextOfT $ isDatatype ind t
ns <- catMaybes <$> do
forM cons $ \ con ->
fmap (con,) <$> do
Trav.mapM (\sc -> lift $ fixTarget $ sc { scTarget = target }) =<< do
computeNeighbourhood delta1 n delta2 perm d pars ixs hix hps con
case ns of
[] -> do
let absurd = VarP "()"
return $ Left $ SClause
{ scTel = telFromList $ telToList delta1 ++
[fmap ((,) "()") t] ++
telToList delta2
, scPerm = perm
, scPats = plugHole absurd hps
, scSubst = idS
, scTarget = Nothing
}
(_ : _ : _) | unusableRelevance (getRelevance t) ->
throwException . IrrelevantDatatype =<< do liftTCM $ buildClosure (unDom t)
_ | Just pcons' <- mcons,
let pcons = map conName pcons',
let cons = (map fst ns),
let diff = Set.fromList cons Set.\\ Set.fromList pcons,
not (Set.null diff) -> do
liftTCM $ reportSDoc "tc.cover.precomputed" 10 $ vcat
[ hsep $ text "pcons =" : map prettyTCM pcons
, hsep $ text "cons =" : map prettyTCM cons
]
throwException (GenericSplitError "precomputed set of constructors does not cover all cases")
_ -> return $ Right $ Covering xDBLevel ns
where
xDBLevel = dbIndexToLevel tel perm x
inContextOfT :: MonadTCM tcm => tcm a -> tcm a
inContextOfT = addCtxTel tel . escapeContext (x + 1)
inContextOfDelta2 :: MonadTCM tcm => tcm a -> tcm a
inContextOfDelta2 = addCtxTel tel . escapeContext x
debugInit tel perm x ps =
liftTCM $ reportSDoc "tc.cover.top" 10 $ vcat
[ text "TypeChecking.Coverage.split': split"
, nest 2 $ vcat
[ text "tel =" <+> prettyTCM tel
, text "perm =" <+> text (show perm)
, text "x =" <+> text (show x)
, text "ps =" <+> text (show ps)
]
]
debugHoleAndType delta1 delta2 s hps t =
liftTCM $ reportSDoc "tc.cover.top" 10 $ nest 2 $ vcat $
[ text "p =" <+> text (patVarNameToString s)
, text "hps =" <+> text (show hps)
, text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> inContextOfDelta2 (prettyTCM delta2)
, text "t =" <+> inContextOfT (prettyTCM t)
]
splitResult :: QName -> SplitClause -> TCM (Maybe Covering)
splitResult f sc@(SClause tel perm ps _ target) = do
reportSDoc "tc.cover.split" 10 $ vcat
[ text "splitting result:"
, nest 2 $ text "f =" <+> text (show f)
, nest 2 $ text "target =" <+> (addContext tel $ maybe empty prettyTCM target)
]
let done = return Nothing
caseMaybe target done $ \ t -> do
isR <- addCtxTel tel $ isRecordType $ unArg t
case isR of
Just (_r, vs, Record{ recFields = fs }) -> do
reportSDoc "tc.cover" 20 $ sep
[ text $ "we are of record type _r = " ++ show _r
, text "applied to parameters vs = " <+> (addCtxTel tel $ prettyTCM vs)
, text $ "and have fields fs = " ++ show fs
]
fvs <- freeVarsToApply f
let es = patternsToElims perm ps
let self = defaultArg $ Def f (map Apply fvs) `applyE` es
pargs = vs ++ [self]
reportSDoc "tc.cover" 20 $ sep
[ text "we are self = " <+> (addCtxTel tel $ prettyTCM $ unArg self)
]
let
n = permRange perm
Just . Covering n <$> do
forM fs $ \ proj -> do
dType <- defType <$> do getConstInfo $ unArg proj
let
target' = Just $ proj $> dType `apply` pargs
sc' = sc { scPats = scPats sc ++ [fmap (Named Nothing . ProjP) proj]
, scTarget = target'
}
return (unArg proj, sc')
_ -> done