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

git.iko.soy/Idris-dev

on master help sign in

Coverage checker should ignore hidden arguments

4175a7fEdwin Brady12 years ago

src/Idris/AbsSyntax.hs+9−2

compare with master

unifiedsplit

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

1850 mty <- match' ty ty'

1851 ms <- match' s s'

1852 return (mt ++ mty ++ ms)

1853− match (PHidden x) 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 []

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

1859+ match x (PHidden y)

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

1861+ | otherwise = return []

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

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

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

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

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

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

src/Idris/Coverage.hs+3−2

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

56 = do i <- getIState

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

58 -- 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)

60 let lhss = map pUnApply lhs_tms'

61 let lhss = map pUnApply lhs_tms'

62 let argss = transpose lhss

63 let argss = transpose lhss

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

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

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

95 -- (xs)

96 -- (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

97 Right ms -> False

98 Right ms -> False

98 Left miss -> True) xs

99 Left miss -> True) xs

100