module Agda.TypeChecking.Coverage where
import Control.Monad
import Control.Monad.Error
import Control.Applicative
import Data.List
import qualified Data.Set as Set
import Data.Set (Set)
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Internal
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.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.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Primitive (constructorForm)
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Irrelevance
import Agda.Interaction.Options
import Agda.Utils.Permutation
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
#include "../undefined.h"
import Agda.Utils.Impossible
data SplitClause = SClause
{ scTel :: Telescope
, scPerm :: Permutation
, scPats :: [Arg Pattern]
, scSubst :: Substitution
, scTarget :: Maybe 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 = clausePats cl
, scSubst = __IMPOSSIBLE__
, scTarget = Nothing
}
data SplitError = NotADatatype (Closure Type)
| IrrelevantDatatype (Closure Type)
| CoinductiveDatatype (Closure Type)
| CantSplit QName Telescope Args Args [Term]
| GenericSplitError String
deriving (Show)
instance PrettyTCM SplitError where
prettyTCM err = case err of
NotADatatype t -> enterClosure t $ \ t -> fsep $
pwords "Cannot pattern match on non-datatype" ++ [prettyTCM t]
IrrelevantDatatype t -> enterClosure t $ \ t -> fsep $
pwords "Cannot pattern match on datatype" ++ [prettyTCM t] ++
pwords "since it is declared irrelevant"
CoinductiveDatatype t -> enterClosure t $ \ t -> fsep $
pwords "Cannot pattern match on the coinductive type" ++ [prettyTCM t]
CantSplit c tel cIxs gIxs flex -> addCtxTel tel $ vcat
[ fsep $ pwords "Cannot decide whether there should be a case for the constructor" ++ [prettyTCM c <> text ","] ++
pwords "since the unification gets stuck on unifying the inferred indices"
, nest 2 $ prettyTCM cIxs
, fsep $ pwords "with the expected indices"
, nest 2 $ prettyTCM gIxs
]
GenericSplitError s -> fsep $
pwords "Split failed:" ++ pwords s
instance Error SplitError where
noMsg = strMsg ""
strMsg = GenericSplitError
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 (const $ VarP "_")) $ lgamma
sc = SClause gamma (idP n) xs idS $ Just a
reportSDoc "tc.cover.top" 10 $ vcat
[ text "Coverage checking"
, nest 2 $ vcat $ map (text . show . clausePats) cs
]
(splitTree, used, pss) <- cover 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 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 :: [Clause] -> SplitClause -> TCM (SplitTree, Set Nat, [[Arg Pattern]])
cover 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)
]
case match cs ps 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 ps perm ]
reportSLn "tc.cover.cover" 10 $ "literal matches: " ++ show is
return (SplittingDone (size tel), Set.fromList (i : is), [])
No -> return (SplittingDone (size tel), Set.empty, [ps])
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 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 (mapSnd (const Nothing)) 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 args -> do
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
| domRelevance at == Irrelevant && not splitOnIrrelevantDataAllowed ->
throw IrrelevantDatatype
| otherwise -> do
let (ps, is) = genericSplitAt np args
return (d, ps, is, cs)
Record{recPars = np, recCon = c} ->
return (d, args, [], [c])
_ -> throw NotADatatype
_ -> throw NotADatatype
computeNeighbourhood :: Telescope -> String -> Telescope -> Permutation -> QName -> Args -> Args -> Nat -> OneHolePatterns -> QName -> CoverM [SplitClause]
computeNeighbourhood delta1 n delta2 perm d pars ixs hix hps con = do
dtype <- liftTCM $ (`piApply` pars) . defType <$> getConstInfo d
Con con [] <- liftTCM $ ignoreSharing <$> (constructorForm =<< normalise (Con con []))
ctype <- liftTCM $ defType <$> getConstInfo con
(gamma0, cixs) <- do
TelV gamma0 (El _ d) <- liftTCM $ telView (ctype `piApply` pars)
let Def _ cixs = ignoreSharing d
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
gamma = telFromList . map (fmap preserve) . telToList $ gamma0
debugInit con ctype pars ixs cixs delta1 delta2 gamma hps hix
let flex = [0..size delta1 + size gamma 1]
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 []
DontKnow _ -> do
debugCantSplit
throwException $ CantSplit con (delta1 `abstract` gamma) conIxs givenIxs
[ var i | i <- 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 VarP) $ 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 [SClause theta' rperm rps rsub Nothing]
where
debugInit con ctype 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 "pars =" <+> prettyList (map prettyTCM pars)
, text "ixs =" <+> addCtxTel (delta1 `abstract` gamma) (prettyList (map prettyTCM ixs))
, text "cixs =" <+> 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)
]
splitClauseWithAbs :: Clause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))
splitClauseWithAbs c x = split' Inductive (clauseToSplitClause c) (x, Nothing)
splitLast :: Induction -> Telescope -> [Arg Pattern] -> TCM (Either SplitError Covering)
splitLast ind tel ps = split ind sc (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
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 $ fst x
dbIndexToLevel tel perm x = if n < 0 then __IMPOSSIBLE__ else n
where n = permute perm [0..] !! (size tel x 1)
split' :: Induction
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError (Either SplitClause Covering))
split' ind sc@(SClause tel perm ps _ target) (x, mcons) = liftTCM $ runExceptionT $ do
debugInit tel perm x ps
(n, t, delta1, delta2) <- do
let (tel1, Dom h r (n, t) : tel2) = genericSplitAt (size tel x 1) $ telToList tel
return (n, Dom h r 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
liftTCM $ whenM (optWithoutK <$> pragmaOptions) $
inContextOfT $ Split.wellFormedIndices (unDom t)
ns <- concat <$> do
forM cons $ \ con ->
map (con,) <$> do
mapM fixTarget =<<
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 (domRelevance t) ->
throwException . IrrelevantDatatype =<< do liftTCM $ buildClosure (unDom t)
_ | Just pcons <- mcons,
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
fixTarget :: SplitClause -> CoverM SplitClause
fixTarget sc@SClause{ scSubst = sigma } =
flip (maybe $ return sc) target $ \ a -> do
TelV tel b <- lift $ telView $ applySubst sigma a
let n = size tel
lgamma = telToList tel
xs = map (argFromDom . fmap (const $ VarP "_")) $ lgamma
if (n == 0) then return sc { scTarget = Just 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 b
}
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 s
, text "hps =" <+> text (show hps)
, text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> inContextOfDelta2 (prettyTCM delta2)
, text "t =" <+> inContextOfT (prettyTCM t)
]