4175a7f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Coverage checker should ignore hidden arguments

Since they're required to be inferred from other arguments, they make no contribution to coverage checking. Fixes #1710

commit4175a7f5cd2f08958735f0f61c5c5ae53323323e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 20 Dec 2014, 23:05 (12 years ago) parent57cd38a

2 files changed+12−4

unifiedsplit

src/Idris/AbsSyntax.hs+9−2

@@ -1850,8 +1850,15 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

18501850 mty <- match' ty ty'

18511851 ms <- match' s s'

18521852 return (mt ++ mty ++ ms)

1853− match (PHidden x) y = match' x y

1854− match x (PHidden y) = match' x y

1853+ match (PHidden x) (PHidden y)

1854+ | RightOK xs <- match x y = return xs -- to collect variables

1855+ | otherwise = return [] -- Otherwise hidden things are unmatchable

1856+ match (PHidden x) y

1857+ | RightOK xs <- match x y = return xs

1858+ | otherwise = return []

1859+ match x (PHidden y)

1860+ | RightOK xs <- match x y = return xs

1861+ | otherwise = return []

18551862 match (PUnifyLog x) y = match' x y

18561863 match x (PUnifyLog y) = match' x y

18571864 match (PNoImplicits x) y = match' x y

src/Idris/Coverage.hs+3−2

@@ -56,7 +56,8 @@ genClauses fc n xs given

5656 = do i <- getIState

5757 let lhs_tms = map (\x -> delab' i x True True) xs

5858 -- if a placeholder was given, don't bother generating cases for it

59− let lhs_tms' = zipWith mergePlaceholders lhs_tms given

59+ let lhs_tms' = zipWith mergePlaceholders lhs_tms

60+ (map (stripUnmatchable i) given)

6061 let lhss = map pUnApply lhs_tms'

6162

6263 let argss = transpose lhss

@@ -93,7 +94,7 @@ genClauses fc n xs given

9394

9495 -- Return whether the given clause matches none of the input clauses

9596 -- (xs)

96− noMatch i tm = all (\x -> case matchClause i (delab' i x True True) tm of

97+ noMatch i tm = all (\x -> case matchClause i (stripUnmatchable i (delab' i x True True)) tm of

9798 Right ms -> False

9899 Left miss -> True) xs

99100