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.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.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.Monad
#include "../undefined.h"
import Agda.Utils.Impossible
data SplitClause = SClause
{ scTel :: Telescope
, scPerm :: Permutation
, scPats :: [Arg Pattern]
, scSubst :: [Term]
}
type Covering = [SplitClause]
data SplitError = NotADatatype Type
| IrrelevantDatatype Type
| CoinductiveDatatype Type
| NoRecordConstructor Type
| CantSplit QName Telescope Args Args [Term]
| GenericSplitError String
deriving (Show)
instance PrettyTCM SplitError where
prettyTCM err = case err of
NotADatatype t -> fsep $
pwords "Cannot pattern match on non-datatype" ++ [prettyTCM t]
IrrelevantDatatype t -> fsep $
pwords "Cannot pattern match on datatype" ++ [prettyTCM t] ++
pwords "since it is declared irrelevant"
CoinductiveDatatype t -> fsep $
pwords "Cannot pattern match on the coinductive type" ++ [prettyTCM t]
NoRecordConstructor t -> fsep $
pwords "Cannot pattern match on record" ++ [prettyTCM t] ++
pwords "because it has no constructor"
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
typeOfVar :: Telescope -> Nat -> Arg Type
typeOfVar tel n
| n >= len = __IMPOSSIBLE__
| otherwise = fmap snd
$ ts !! fromIntegral n
where
len = genericLength ts
ts = reverse $ telToList tel
checkCoverage :: QName -> TCM ()
checkCoverage f = do
d <- getConstInfo f
TelV gamma _ <- telView $ defType d
let defn = theDef d
case defn of
Function{ funProjection = proj, funClauses = cs@(_:_) } -> do
let n = genericLength $ clausePats $ head cs
np = maybe 0 snd proj
gamma' = telFromList $ genericTake n $ genericDrop np $ telToList gamma
xs = map (fmap $ const $ VarP "_") $ telToList gamma'
reportSDoc "tc.cover.top" 10 $ vcat
[ text "Coverage checking"
, nest 2 $ vcat $ map (text . show . clausePats) cs
]
(used, pss) <- cover cs $ SClause gamma' (idP n) xs (idSub gamma')
whenM (optCompletenessCheck <$> pragmaOptions) $
case pss of
[] -> return ()
_ ->
setCurrentRange (getRange cs) $
typeError $ CoverageFailure f pss
case Set.toList $ Set.difference (Set.fromList [0..genericLength cs 1]) used of
[] -> return ()
is -> do
let unreached = map ((cs !!) . fromIntegral) is
setCurrentRange (getRange unreached) $
typeError $ UnreachableClauses f (map clausePats unreached)
_ -> __IMPOSSIBLE__
cover :: [Clause] -> SplitClause -> TCM (Set Nat, [[Arg Pattern]])
cover cs (SClause tel perm ps _) = 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..] (genericTake i cs), matchLits c ps perm ]
reportSLn "tc.cover.cover" 10 $ "literal matches: " ++ show is
return (Set.fromList (i : is), [])
No -> return (Set.empty, [ps])
Block x -> do
r <- split Inductive tel perm ps x
case r of
Left err -> case err of
CantSplit c tel us vs _ -> typeError $ CoverageCantSplitOn c tel us vs
NotADatatype a -> typeError $ CoverageCantSplitType a
IrrelevantDatatype a -> typeError $ CoverageCantSplitIrrelevantType a
CoinductiveDatatype a -> typeError $ CoverageCantSplitType a
NoRecordConstructor a -> typeError $ CoverageCantSplitType a
GenericSplitError s -> fail $ "failed to split: " ++ s
Right scs -> (Set.unions -*- concat) . unzip <$> mapM (cover cs) scs
isDatatype :: (MonadTCM tcm, MonadException SplitError tcm) =>
Induction -> Arg Type ->
tcm (QName, [Arg Term], [Arg Term], [QName])
isDatatype ind at = do
let t = unArg at
t' <- liftTCM $ reduce t
case 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 ->
throwException $ CoinductiveDatatype t
| argRelevance at == Irrelevant && not splitOnIrrelevantDataAllowed ->
throwException $ IrrelevantDatatype t
| otherwise -> do
let (ps, is) = genericSplitAt np args
return (d, ps, is, cs)
Record{recPars = np, recCon = c, recNamedCon = hasCon} ->
if hasCon then return (d, args, [], [c])
else throwException $ NoRecordConstructor t
_ -> throwException $ NotADatatype t
_ -> throwException $ NotADatatype t
computeNeighbourhood :: Telescope -> Telescope -> Permutation -> QName -> Args -> Args -> Nat -> OneHolePatterns -> QName -> CoverM [SplitClause]
computeNeighbourhood delta1 delta2 perm d pars ixs hix hps con = do
dtype <- liftTCM $ (`piApply` pars) . defType <$> getConstInfo d
Con con [] <- liftTCM $ constructorForm =<< normalise (Con con [])
ctype <- liftTCM $ defType <$> getConstInfo con
TelV gamma (El _ (Def _ cixs)) <- liftTCM $ telView (ctype `piApply` pars)
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 = [ Var i [] | i <- [0..size delta2' 1] ]
++ [ raise (size delta2') conv ]
++ [ Var i [] | i <- [size delta2' + size gamma ..] ]
let conp = ConP con Nothing $ map (fmap VarP) $ teleArgNames gamma
ps = plugHole conp hps
ps' = substs 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 = substs rho' ps''
let rsub = substs rho' rho
debugFinal theta' rperm rps
return [SClause theta' rperm rps rsub]
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)
]
splitClause :: Clause -> Nat -> TCM (Either SplitError Covering)
splitClause c x =
split Inductive (clauseTel c) (clausePerm c) (clausePats c) x
splitClauseWithAbs :: Clause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))
splitClauseWithAbs c x =
split' Inductive (clauseTel c) (clausePerm c) (clausePats c) x
split :: Induction
-> Telescope -> Permutation -> [Arg Pattern] -> Nat
-> TCM (Either SplitError Covering)
split ind tel perm ps x = do
r <- split' ind tel perm ps x
return $ case r of
Left err -> Left err
Right (Left _) -> Right []
Right (Right c) -> Right c
split' :: Induction
-> Telescope -> Permutation -> [Arg Pattern] -> Nat
-> TCM (Either SplitError (Either SplitClause Covering))
split' ind tel perm ps x = liftTCM $ runExceptionT $ do
debugInit tel perm x ps
(delta1, delta2) <- do
let (tel1, _ : tel2) = genericSplitAt (size tel x 1) $ telToList tel
return (telFromList tel1, telFromList tel2)
let t = typeOfVar tel x
(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 !! fromIntegral 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 pars ixs
ns <- concat <$> mapM (computeNeighbourhood delta1 delta2 perm d pars ixs hix hps) cons
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 = []
}
(_ : _ : _) | unusableRelevance (argRelevance t) ->
throwException $ IrrelevantDatatype (unArg t)
_ -> return $ Right ns
where
inContextOfT :: MonadTCM tcm => tcm a -> tcm a
inContextOfT = escapeContext (fromIntegral x + 1)
debugInit tel perm x ps =
liftTCM $ reportSDoc "tc.cover.top" 10 $ vcat
[ text "TypeChecking.Rules.LHS.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 =" <+> prettyTCM delta2
, text "t =" <+> inContextOfT (prettyTCM t)
]