coverage 0.1.0.2 → 0.1.0.3

raw patch · 9 files changed

+279/−283 lines, 9 filesdep +HUnitdep ~hspecPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: HUnit

Dependency ranges changed: hspec

API changes (from Hackage documentation)

Files

• coverage.cabal +7/−7
• src/Control/Coverage.hs +51/−0
• src/Control/Coverage/Internal.hs +211/−0
• src/Coverage.hs +0/−50
• src/Coverage/Internal.hs +0/−210
• tests/CoverageSpec.hs +3/−5
• tests/CoverageSupport.hs +2/−2
• tests/CoverageUnitSpec.hs +5/−7
• tests/Spec.hs +0/−2

@@ -1,5 +1,5 @@ name:                coverage-version:             0.1.0.2+version:             0.1.0.3 synopsis:            Exhaustivity Checking Library homepage:            https://github.com/nicodelpiano/coverage bug-reports:         https://github.com/nicodelpiano/coverage/issues@@ -9,7 +9,7 @@ author:              Nicolas Del Piano <ndel314@gmail.com> maintainer:          Nicolas Del Piano <ndel314@gmail.com> copyright:           (c) 2015 Nicolas Del Piano-category:            Development+category:            Control build-type:          Simple extra-source-files:  README.md cabal-version:       >=1.10@@ -24,21 +24,21 @@  library   ghc-options:         -Wall-  exposed-modules:     Coverage-                       Coverage.Internal+  exposed-modules:     Control.Coverage+                       Control.Coverage.Internal   -- other-modules:   -- other-extensions:   build-depends:       base >=4.7 && <4.8   hs-source-dirs:      src   default-language:    Haskell2010 -test-suite tests+test-suite hspec   type:       exitcode-stdio-1.0   ghc-options:       -Wall   hs-source-dirs:-      tests, .+      tests   main-is:       Spec.hs   other-modules:@@ -46,5 +46,5 @@       CoverageSupport       CoverageUnitSpec   build-depends:-      base >=4.7 && <4.8, coverage, QuickCheck >=2.7, hspec   == 2.*+      base >=4.7 && <4.8, coverage, QuickCheck >=2.7, HUnit -any, hspec -any   default-language:    Haskell2010

@@ -0,0 +1,51 @@+-----------------------------------------------------------------------------+--+-- Module      :  Control.Coverage+-- Copyright   :  (c) 2015 Nicolas Del Piano+-- License     :  MIT+--+-- Maintainer  :  Nicolas Del Piano <ndel314@gmail.com>+-- Stability   :  experimental+-- Portability :+--+-- |+-- Exhaustivity checking main function.+--+-----------------------------------------------------------------------------++module Control.Coverage+  ( check+  , Binder(..)+  , Guard(..)+  , makeEnv+  , Check(..)+  , Redundant(..)+  ) where++import Control.Coverage.Internal++import Data.List (foldl', nub)+import Data.Maybe (fromMaybe)++import Control.Applicative ((<$>), liftA2)++-- |+-- Given a list of alternatives, `check` generates the proper set of uncovered cases.+--+check :: (Eq lit) => Environment -> [Alternative lit] -> Check lit+check env cas = applyRedundant (fmap nub) . applyUncovered nub . foldl' step initial $ cas+  where+  initial = makeCheck [uncovers] $ Redundant []+    where uncovers = if null cas then initialize $ length . fst . head $ cas else []++  step :: (Eq lit) => Check lit -> Alternative lit -> Check lit+  step ch ca =+    let (missed, pr) = unzip $ map (missingAlternative env ca) $ getUncovered ch+        cond = liftA2 (&&) (or <$> sequence pr) $ mr . getRedundant $ ch+    in applyRedundant (\_ -> if fromMaybe True cond then getRedundant ch else fmap (fst ca :) $ getRedundant ch)+       . applyUncovered (\unc -> if fromMaybe True cond then concat missed else unc) $ ch+      where+      mr :: Redundant [Binders lit] -> Maybe Bool+      mr DontKnow = Nothing+      mr NotRedundant = Just False+      mr (Redundant _) = Just True

@@ -0,0 +1,211 @@+-----------------------------------------------------------------------------+--+-- Module      :  Control.Coverage.Internal+-- Copyright   :  (c) 2015 Nicolas Del Piano+-- License     :  MIT+--+-- Maintainer  :  Nicolas Del Piano <ndel314@gmail.com>+-- Stability   :  experimental+-- Portability :+--+-- |+-- Module for internal representation.+--+-----------------------------------------------------------------------------++module Control.Coverage.Internal where++import Data.List (sortBy)+import Data.Function (on)+import Data.Maybe (fromMaybe)++import Control.Applicative (Applicative, (<*>), pure, liftA2)+import Control.Arrow (first)++-- | A type synonym for names. +type Name = String++-- | A collection of binders, as used to match products, in product binders+-- or collections of binders in top-level declarations.+type Binders lit = [Binder lit]++-- |+-- Binders+--+data Binder lit+  = Var (Maybe Name)+  | Lit lit+  | Tagged Name (Binder lit)+  | Product (Binders lit)+  | Record [(Name, Binder lit)]+  deriving (Show, Eq)++-- | Environment+--+-- The language implementor should provide an environment to let+-- the checker lookup for constructors' names (just for one type for now).+newtype Environment = Environment { envInfo :: Name -> Maybe [Name] }++makeEnv :: (Name -> Maybe [Name]) -> Environment+makeEnv info = Environment { envInfo = info }++defaultEnv :: Environment+defaultEnv = makeEnv (\_ -> Nothing)++-- | Guards and alternatives+-- +-- Guard are abstract, and it is up to the language implementor to interpret+-- guards abstractly. Guards can catch all cases, or represent some opaque+-- expression which cannot be analysed.+data Guard = CatchAll+           | Opaque+  deriving (Show, Eq)++-- | A case alternative consists of a collection of binders which match+-- a collection of values, and an optional guard.+type Alternative lit = (Binders lit, Maybe Guard)++-- | Data-type for redundant cases representation.+data Redundant a = DontKnow | NotRedundant | Redundant a+  deriving (Show, Eq)++-- | Functor instance for Redundant (TODO: proofs).+instance Functor Redundant where+  fmap _ DontKnow      = DontKnow+  fmap _ NotRedundant  = NotRedundant+  fmap f (Redundant r) = Redundant $ f r++-- | Applicative instance for Redundant.+instance Applicative Redundant where+  pure = Redundant++  DontKnow <*> _      = DontKnow+  NotRedundant <*> _  = NotRedundant+  (Redundant f) <*> m = fmap f m++-- | Check wraps both uncovered and redundant cases.+data Check lit = Check+  { getUncovered :: [Binders lit]+  , getRedundant :: Redundant [Binders lit]+  } deriving (Show, Eq) ++makeCheck :: [Binders lit] -> Redundant [Binders lit] -> Check lit+makeCheck bs red = Check+  { getUncovered = bs+  , getRedundant = red }++applyUncovered :: ([Binders lit] -> [Binders lit]) -> Check lit -> Check lit+applyUncovered f c = makeCheck (f $ getUncovered c) (getRedundant c)++applyRedundant :: (Redundant [Binders lit] -> Redundant [Binders lit]) -> Check lit -> Check lit+applyRedundant f c = makeCheck (getUncovered c) (f $ getRedundant c)++-- | Wildcard+wildcard :: Binder lit+wildcard = Var Nothing++-- |+-- Applies a function over two lists of tuples that may lack elements.+--+genericMerge :: Ord a =>+  (a -> Maybe b -> Maybe c -> d) ->+  [(a, b)] ->+  [(a, c)] ->+  [d]+genericMerge _ [] [] = []+genericMerge f bs [] = map (\(s, b) -> f s (Just b) Nothing) bs+genericMerge f [] bs = map (\(s, b) -> f s Nothing (Just b)) bs+genericMerge f bsl@((s, b):bs) bsr@((s', b'):bs')+  | s < s' = (f s (Just b) Nothing) : genericMerge f bs bsr+  | s > s' = (f s' Nothing (Just b')) : genericMerge f bsl bs'+  | otherwise = (f s (Just b) (Just b')) : genericMerge f bs bs'++-- | Returns the uncovered set after one binder is applied to the set of+-- values represented by another.+missingSingle :: (Eq lit) => Environment -> Binder lit -> Binder lit -> ([Binder lit], Maybe Bool)+missingSingle _ _ (Var _) = ([], pure True)+missingSingle env (Var _) (Product ps) =+  first (map Product) $ missingMultiple env (initialize $ length ps) ps+missingSingle env p@(Product ps) (Product ps')+  | length ps == length ps' = first (map Product) $ missingMultiple env ps ps'+  | otherwise = ([p], pure False)+missingSingle env (Var _) cb@(Tagged con _) =+  (concatMap (\cp -> fst $ missingSingle env cp cb) $ tagEnv, pure True)+  where+  tag :: (Eq lit) => Name -> Binder lit+  tag n = Tagged n wildcard++  tagEnv :: (Eq lit) => [Binder lit]+  tagEnv = map tag+           . fromMaybe (error $ "Constructor name '" ++ con ++ "' not in the scope of the current environment in missingSingle.")+           . envInfo env $ con+missingSingle env c@(Tagged tag bs) (Tagged tag' bs')+  | tag == tag' = let (bs'', pr) = missingSingle env bs bs' in (map (Tagged tag) bs'', pr)+  | otherwise = ([c], pure False)+missingSingle env (Var _) (Record bs) =+  (map (Record . zip names) $ miss, pr)+  where+  (miss, pr) = missingMultiple env (initialize $ length bs) binders++  (names, binders) = unzip bs+missingSingle env (Record bs) (Record bs') =+  (map (Record . zip sortedNames) $ allMisses, pr)+  where+  (allMisses, pr) = uncurry (missingMultiple env) $ unzip binders++  sortNames = sortBy (compare `on` fst)+  +  (sbs, sbs') = (sortNames bs, sortNames bs')++  compB :: a -> Maybe a -> Maybe a -> (a, a)+  compB e b b' = (fm b, fm b')+    where+    fm = fromMaybe e++  compBS :: Eq a => b -> a -> Maybe b -> Maybe b -> (a, (b, b))+  compBS e s b b' = (s, compB e b b')++  (sortedNames, binders) = unzip $ genericMerge (compBS (Var Nothing)) sbs sbs'+missingSingle _ b@(Lit l) (Lit l')+  | l == l' = ([], pure True)+  | otherwise = ([b], pure False) +missingSingle _ b _ = ([b], Nothing) ++-- |+-- Generates a list of initial binders.+--+initialize :: Int -> [Binder lit]+initialize = flip replicate $ wildcard++-- |+-- `missingMultiple` returns the whole set of uncovered cases.+--+missingMultiple :: (Eq lit) => Environment -> Binders lit -> Binders lit -> ([Binders lit], Maybe Bool)+missingMultiple env = go+  where+  go [] [] = ([], pure True)+  go (x:xs) (y:ys) = (map (: xs) missed ++ fmap (x :) missed', liftA2 (&&) pr1 pr2)+    where+    (missed, pr1) = missingSingle env x y+    (missed', pr2) = go xs ys+  go _ _ = error "Error in missingMultiple: invalid length of argument binders."++-- |+-- `missingCases` applies `missingMultiple` to an alternative.+--+missingCases :: (Eq lit) => Environment -> Binders lit -> Alternative lit -> ([Binders lit], Maybe Bool)+missingCases env unc = missingMultiple env unc . fst++-- |+-- `missingAlternative` is `missingCases` with guard handling.+--+missingAlternative :: (Eq lit) => Environment -> Alternative lit -> Binders lit -> ([Binders lit], Maybe Bool)+missingAlternative env alt unc+  | isExhaustiveGuard $ snd alt = mcases+  | otherwise = ([unc], snd mcases)+  where+  mcases = missingCases env unc alt++  isExhaustiveGuard :: Maybe Guard -> Bool+  isExhaustiveGuard (Just Opaque) = False+  isExhaustiveGuard _ = True

@@ -1,50 +0,0 @@------------------------------------------------------------------------------------ Module      :  Coverage--- Copyright   :  (c) 2015 Nicolas Del Piano--- License     :  MIT------ Maintainer  :  Nicolas Del Piano <ndel314@gmail.com>--- Stability   :  experimental--- Portability :------ |--- Exhaustivity checking main function.-----------------------------------------------------------------------------------module Coverage-  ( check-  , Binder(..)-  , Guard(..)-  , makeEnv-  , Check(..)-  , Redundant(..)-  ) where--import Coverage.Internal--import Data.List (foldl', nub)-import Data.Maybe (fromMaybe)--import Control.Applicative ((<$>), liftA2)---- |--- Given a list of alternatives, `check` generates the proper set of uncovered cases.----check :: (Eq lit) => Environment -> [Alternative lit] -> Check lit-check env cas = applyRedundant (fmap nub) . applyUncovered nub . foldl' step initial $ cas-  where-  initial = makeCheck [initialize $ length . fst . head $ cas] $ Redundant []--  step :: (Eq lit) => Check lit -> Alternative lit -> Check lit-  step ch ca =-    let (missed, pr) = unzip $ map (missingAlternative env ca) $ getUncovered ch-        cond = liftA2 (&&) (or <$> sequence pr) $ mr . getRedundant $ ch-    in applyRedundant (\_ -> if fromMaybe True cond then getRedundant ch else fmap (fst ca :) $ getRedundant ch)-       . applyUncovered (\unc -> if fromMaybe True cond then concat missed else unc) $ ch-      where-      mr :: Redundant [Binders lit] -> Maybe Bool-      mr DontKnow = Nothing-      mr NotRedundant = Just False-      mr (Redundant _) = Just True

@@ -1,210 +0,0 @@------------------------------------------------------------------------------------ Module      :  Coverage.Internal--- Copyright   :  (c) 2015 Nicolas Del Piano--- License     :  MIT------ Maintainer  :  Nicolas Del Piano <ndel314@gmail.com>--- Stability   :  experimental--- Portability :------ |--- Module for internal representation.-----------------------------------------------------------------------------------module Coverage.Internal where--import Data.List (sortBy)-import Data.Function (on)-import Data.Maybe (fromMaybe)--import Control.Applicative (Applicative, (<*>), pure, liftA2)-import Control.Arrow (first)---- | A type synonym for names. -type Name = String---- | A collection of binders, as used to match products, in product binders--- or collections of binders in top-level declarations.-type Binders lit = [Binder lit]---- |--- Binders----data Binder lit-  = Var (Maybe Name)-  | Lit lit-  | Tagged Name (Binder lit)-  | Product (Binders lit)-  | Record [(Name, Binder lit)]-  deriving (Show, Eq)---- | Environment------ The language implementor should provide an environment to let--- the checker lookup for constructors' names (just for one type for now).-newtype Environment = Environment { envInfo :: Name -> Maybe [Name] }--makeEnv :: (Name -> Maybe [Name]) -> Environment-makeEnv info = Environment { envInfo = info }--defaultEnv :: Environment-defaultEnv = makeEnv (\_ -> Nothing)---- | Guards and alternatives--- --- Guard are abstract, and it is up to the language implementor to interpret--- guards abstractly. Guards can catch all cases, or represent some opaque--- expression which cannot be analysed.-data Guard = CatchAll | Opaque-  deriving (Show, Eq)---- | A case alternative consists of a collection of binders which match--- a collection of values, and an optional guard.-type Alternative lit = (Binders lit, Maybe Guard)---- | Data-type for redundant cases representation.-data Redundant a = DontKnow | NotRedundant | Redundant a-  deriving (Show, Eq)---- | Functor instance for Redundant (TODO: proofs).-instance Functor Redundant where-  fmap _ DontKnow      = DontKnow-  fmap _ NotRedundant  = NotRedundant-  fmap f (Redundant r) = Redundant $ f r---- | Applicative instance for Redundant.-instance Applicative Redundant where-  pure = Redundant--  DontKnow <*> _      = DontKnow-  NotRedundant <*> _  = NotRedundant-  (Redundant f) <*> m = fmap f m---- | Check wraps both uncovered and redundant cases.-data Check lit = Check-  { getUncovered :: [Binders lit]-  , getRedundant :: Redundant [Binders lit]-  } deriving (Show, Eq) --makeCheck :: [Binders lit] -> Redundant [Binders lit] -> Check lit-makeCheck bs red = Check-  { getUncovered = bs-  , getRedundant = red }--applyUncovered :: ([Binders lit] -> [Binders lit]) -> Check lit -> Check lit-applyUncovered f c = makeCheck (f $ getUncovered c) (getRedundant c)--applyRedundant :: (Redundant [Binders lit] -> Redundant [Binders lit]) -> Check lit -> Check lit-applyRedundant f c = makeCheck (getUncovered c) (f $ getRedundant c)---- | Wildcard-wildcard :: Binder lit-wildcard = Var Nothing---- |--- Applies a function over two lists of tuples that may lack elements.----genericMerge :: Ord a =>-  (a -> Maybe b -> Maybe c -> d) ->-  [(a, b)] ->-  [(a, c)] ->-  [d]-genericMerge _ [] [] = []-genericMerge f bs [] = map (\(s, b) -> f s (Just b) Nothing) bs-genericMerge f [] bs = map (\(s, b) -> f s Nothing (Just b)) bs-genericMerge f bsl@((s, b):bs) bsr@((s', b'):bs')-  | s < s' = (f s (Just b) Nothing) : genericMerge f bs bsr-  | s > s' = (f s' Nothing (Just b')) : genericMerge f bsl bs'-  | otherwise = (f s (Just b) (Just b')) : genericMerge f bs bs'---- | Returns the uncovered set after one binder is applied to the set of--- values represented by another.-missingSingle :: (Eq lit) => Environment -> Binder lit -> Binder lit -> ([Binder lit], Maybe Bool)-missingSingle _ _ (Var _) = ([], pure True)-missingSingle env (Var _) (Product ps) =-  first (map Product) $ missingMultiple env (initialize $ length ps) ps-missingSingle env p@(Product ps) (Product ps')-  | length ps == length ps' = first (map Product) $ missingMultiple env ps ps'-  | otherwise = ([p], pure False)-missingSingle env (Var _) cb@(Tagged con _) =-  (concatMap (\cp -> fst $ missingSingle env cp cb) $ tagEnv, pure True)-  where-  tag :: (Eq lit) => Name -> Binder lit-  tag n = Tagged n wildcard--  tagEnv :: (Eq lit) => [Binder lit]-  tagEnv = map tag-           . fromMaybe (error $ "Constructor name '" ++ con ++ "' not in the scope of the current environment in missingSingle.")-           . envInfo env $ con-missingSingle env c@(Tagged tag bs) (Tagged tag' bs')-  | tag == tag' = let (bs'', pr) = missingSingle env bs bs' in (map (Tagged tag) bs'', pr)-  | otherwise = ([c], pure False)-missingSingle env (Var _) (Record bs) =-  (map (Record . zip names) $ miss, pr)-  where-  (miss, pr) = missingMultiple env (initialize $ length bs) binders--  (names, binders) = unzip bs-missingSingle env (Record bs) (Record bs') =-  (map (Record . zip sortedNames) $ allMisses, pr)-  where-  (allMisses, pr) = uncurry (missingMultiple env) $ unzip binders--  sortNames = sortBy (compare `on` fst)-  -  (sbs, sbs') = (sortNames bs, sortNames bs')--  compB :: a -> Maybe a -> Maybe a -> (a, a)-  compB e b b' = (fm b, fm b')-    where-    fm = fromMaybe e--  compBS :: Eq a => b -> a -> Maybe b -> Maybe b -> (a, (b, b))-  compBS e s b b' = (s, compB e b b')--  (sortedNames, binders) = unzip $ genericMerge (compBS (Var Nothing)) sbs sbs'-missingSingle _ b@(Lit l) (Lit l')-  | l == l' = ([], pure True)-  | otherwise = ([b], pure False) -missingSingle _ b _ = ([b], Nothing) ---- |--- Generates a list of initial binders.----initialize :: Int -> [Binder lit]-initialize = flip replicate $ wildcard---- |--- `missingMultiple` returns the whole set of uncovered cases.----missingMultiple :: (Eq lit) => Environment -> Binders lit -> Binders lit -> ([Binders lit], Maybe Bool)-missingMultiple env = go-  where-  go [] [] = ([], pure True)-  go (x:xs) (y:ys) = (map (: xs) missed ++ fmap (x :) missed', liftA2 (&&) pr1 pr2)-    where-    (missed, pr1) = missingSingle env x y-    (missed', pr2) = go xs ys-  go _ _ = error "Error in missingMultiple: invalid length of argument binders."---- |--- `missingCases` applies `missingMultiple` to an alternative.----missingCases :: (Eq lit) => Environment -> Binders lit -> Alternative lit -> ([Binders lit], Maybe Bool)-missingCases env unc = missingMultiple env unc . fst---- |--- `missingAlternative` is `missingCases` with guard handling.----missingAlternative :: (Eq lit) => Environment -> Alternative lit -> Binders lit -> ([Binders lit], Maybe Bool)-missingAlternative env alt unc-  | isExhaustiveGuard $ snd alt = mcases-  | otherwise = ([unc], snd mcases)-  where-  mcases = missingCases env unc alt--  isExhaustiveGuard :: Maybe Guard -> Bool-  isExhaustiveGuard (Just Opaque) = False-  isExhaustiveGuard _ = True

@@ -15,19 +15,17 @@  module CoverageSpec (main, spec) where -import Coverage-import Coverage.Internal+import Control.Coverage+import Control.Coverage.Internal import CoverageSupport  import Test.Hspec-import Test.HUnit import Test.QuickCheck -import Control.Exception (evaluate)- spec :: Spec spec = do   describe "Test suite" $ do+     describe "missingSingle" $ do       it "between any binder and `Var _` should be `[]`" $         property $ \b n -> fst (missingSingle defaultEnv (b :: Binder String) (Var n)) == []

@@ -15,7 +15,7 @@     module CoverageSupport where -import Coverage.Internal+import Control.Coverage.Internal  import Control.Monad (liftM, liftM2, liftM3) @@ -33,7 +33,7 @@ -- genRec :: (Eq a, Arbitrary a) => Int -> Gen [(Name, Binder a)] genRec 0 = return []-genRec n = liftM3 (\n b -> (:) (n, b)) arbitrary arbitrary (genRec (n-1))+genRec n = liftM3 (\k b -> (:) (k, b)) arbitrary arbitrary (genRec (n-1))  -- | -- Specific generators for each type of binder.

@@ -15,13 +15,10 @@  module CoverageUnitSpec (main, spec) where -import Coverage-import Coverage.Internal-import CoverageSupport+import Control.Coverage+import Control.Coverage.Internal  import Test.Hspec-import Test.HUnit-import Test.QuickCheck  import Control.Exception (evaluate) @@ -59,6 +56,7 @@ tagged_def6 :: [Alternative ()] tagged_def6 = [([wildcard, wildcard, wildcard], Nothing), ([z, z, z], Nothing)] +fromRedundant :: Redundant [a] -> [a] fromRedundant (Redundant bs) = bs fromRedundant _ = [] @@ -119,10 +117,10 @@      describe "Product" $ do       it "product_def1 is exhaustive" $ do-        (getUncovered $ check env record_def1) `shouldBe` []+        (getUncovered $ check env product_def1) `shouldBe` []        it "product_def2 is not exhaustive" $ do-        (getUncovered $ check env record_def2) `shouldBe` [[Record [("bar", s wildcard), ("foo", s wildcard)]], [Record [("bar", wildcard), ("foo", s $ s wildcard)]]]+        (getUncovered $ check env product_def2) `shouldBe` [[Product [Tagged "Succ" (Var Nothing),Var Nothing]],[Product [Var Nothing,Tagged "Succ" (Var Nothing)]]]   main :: IO () main = hspec spec

@@ -1,3 +1,1 @@ {-# OPTIONS_GHC -F -pgmF hspec-discover #-}--import Exhaustive.Internal