4bd5a5b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Small coverage checker fix

Need to generate possible cases by looking at the patterns, not by looking at the function type alone. Of course, this is what it was trying to do, but there was a mistake... Fixes #397

commit4bd5a5b67153a9f577d773656d26698f4e945311 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 19 Jul 2013, 20:30 (13 years ago) parentc0ff0e8

1 file changed+5−1

compare with master

unifiedsplit

src/Idris/Coverage.hs+5−1

src/Idris/Coverage.hs+5−1

@@ -50,8 +50,12 @@ genClauses fc n xs given

5050 logLvl 10 $ show argss ++ "\n" ++ show all_args

5151 logLvl 10 $ "Original: \n" ++

5252 showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)

53+ -- add an infinite supply of explicit arguments to update the possible

54+ -- cases for (the return type may be variadic, or function type, sp

55+ -- there may be more case splitting that the idris_implicits record

56+ -- suggests)

5357 let parg = case lookupCtxt n (idris_implicits i) of

54− (p : _) -> p

58+ (p : _) -> p ++ repeat (PExp 0 False Placeholder "")

5559 _ -> repeat (pexp Placeholder)

5660 let tryclauses = mkClauses parg all_args

5761 logLvl 2 $ show (length tryclauses) ++ " initially to check"