|
definition:
|
verifyMissingBranches :: TermDomain a => Expr -> Int -> [BranchExpr] -> VerifyStateM a ()
verifyMissingBranches _ _ [] = do
currfn <- getCurrentFuncName
error $ "Function " ++ snd currfn ++ " contains case with empty branches!"
verifyMissingBranches exp casevar (Branch (LPattern lit) _ : bs) = do
incrIncompleteCases
currfn <- getCurrentFuncName
let lits = lit : map (patLiteral . branchPattern) bs
cvtype <- getVarTypes >>= return . getVarType casevar
unless (isSubtypeOf cvtype (foldr1 lubType (map aLit lits))) $ do
printIfVerb 3 $ showIncompleteBranch currfn exp [] ++ "\n"
showVarExpTypes
addMissingCase exp []
verifyMissingBranches exp casevar (Branch (Pattern qc _) _ : bs) = do
consinfos <- getConsInfos
let otherqs = map ((\p -> (patCons p, length(patArgs p))) . branchPattern) bs
siblings = siblingsOfCons consinfos qc
missingcs = siblings \\ otherqs -- constructors having no branches
currfn <- getCurrentFuncName
unless (null missingcs) $ do
printIfVerb 0 $ -- just for checking in order to refactor in the future...
"MISSING CONSTRUCTORS " ++ show missingcs ++ " IN FUNCTION " ++ snd currfn
incrIncompleteCases
cvtype <- getVarTypes >>= return . getVarType casevar
let posscs = map fst
(filter (\(c,ar) -> let ctype = aCons c (anyTypes ar)
in joinType cvtype ctype /= emptyType)
missingcs)
cond <- getExpandedCondition
unless (null posscs) $
if cond == fcTrue
then do
printIfVerb 3 $ showIncompleteBranch currfn exp posscs ++ "\n"
showVarExpTypes
addMissingCase exp posscs
else do
showVarExpTypes
unsatcons <- fmap concat $ mapM checkMissCons posscs
unless (null unsatcons) $ do
printIfVerb 3 $
"UNCOVERED CONSTRUCTORS: " ++ unwords (map snd unsatcons)
setNewFunCondition currfn nfcFalse
addMissingCase exp unsatcons
where
-- check whether a constructor is excluded by the current call condition:
checkMissCons cs = do
printIfVerb 4 $ "CHECKING UNREACHABILITY OF CONSTRUCTOR " ++ snd cs
consinfos <- getConsInfos
let iscons = transTester consinfos cs (Var casevar)
bcond <- getExpandedCondition
unsat <- isUnsatisfiable (fcAnd iscons bcond)
return $ if unsat then [] else [cs]
|