inspection-testing (empty) → 0.1
raw patch · 14 files changed
+921/−0 lines, 14 filesdep +basedep +bytestringdep +containerssetup-changed
Dependencies added: base, bytestring, containers, generic-lens, ghc, inspection-testing, template-haskell, text
Files
- ChangeLog.md +17/−0
- LICENSE +20/−0
- README.md +84/−0
- Setup.hs +2/−0
- Test/Inspection.hs +171/−0
- Test/Inspection/Core.hs +140/−0
- Test/Inspection/Internal.hs +21/−0
- Test/Inspection/Plugin.hs +197/−0
- examples/Fusion.hs +29/−0
- examples/GenericLens.hs +48/−0
- examples/NS_NP.hs +44/−0
- examples/Simple.hs +17/−0
- examples/Text.hs +28/−0
- inspection-testing.cabal +103/−0
+ ChangeLog.md view
@@ -0,0 +1,17 @@+# Revision history for inspection-testing++## 0.1 -- 2017-11-09++* Repackaged as inspection-testing++## 0.1.1 -- 2017-09-05++* Also run simplifier in stage 0++## 0.1 -- 2017-08-26++* Initial release to hackage++## 0 -- 2017-02-06++* Development of ghc-proofs commences
+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2017 Joachim Breitner++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ README.md view
@@ -0,0 +1,84 @@+Inspection Testing for Haskell+==============================++This GHC plugin allows you to embed assertions about the intermediate code into+your Haskell code, and have them checked by GHC. This is called _inspection+testing_ (as it automates what you do when you manually inspect the+intermediate code).++Synopsis+--------++See the `Test.Inspection` module for the documentation, but there really isn't much+more to it than:++```haskell+{-# LANGAUGE TemplateHaskell #-}+{-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-}+module Simple where++import Test.Inspection+import Data.Maybe++lhs, rhs :: (a -> b) -> Maybe a -> Bool+lhs f x = isNothing (fmap f x)+rhs f Nothing = True+rhs f (Just _) = False++inspect $ 'lhs === 'rhs+```++If you compile this, you will reassurringly read:++```+$ ghc Simple.hs+[1 of 1] Compiling Simple ( Simple.hs, Simple.o )+examples/Simple.hs:14:1: inspecting lhs === rhs+Test.Inspection tested 1 obligation+```++See the [`examples/`](examples/) directory for more examples of working proofs.++If an assertion fails, for example++```haskell+bad1, bad2 :: Int+bad1 = 2 + 2+bad2 = 5++inspect $ 'bad1 === 'bad2+```+then the compiler will tell you so, and abort the compilation:+```+$ ghc Simple.hs+[1 of 1] Compiling Simple ( Simple.hs, Simple.o )+examples/Simple.hs:20:1: inspecting bad1 === bad2+Obligation fails+ LHS: ghc-prim-0.5.1.0:GHC.Types.I# 4#+ RHS: ghc-prim-0.5.1.0:GHC.Types.I# 5#+examples/Simple.hs: error: inspection testing unsuccessful+```++What can I check for+--------------------++Currently, inspection-testing supports++ * checking two definitions to be equal (useful in the context of generic programming)+ * checking the absence of a certain type (useful in the context of list or stream fusion)+ * checking the absence of allocation (generally useful)++Possible further applications includes++ * checking that all recursive functions are (efficiently called) join-points+ * asserting strictness properties (e.g. in `Data.Map.Strict`)+ * peforming some of these checks only within recursive loops++Let me know if you need any of these, or have further ideas.++Can I comment or help?+----------------------++Sure! We can use the GitHub issue tracker for discussions, and obviously+contributions are welcome.+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ Test/Inspection.hs view
@@ -0,0 +1,171 @@+-- |+-- Description : Inspection Testing for Haskell+-- Copyright : (c) Joachim Breitner, 2017+-- License : MIT+-- Maintainer : mail@joachim-breitner.de+-- Portability : GHC specifc+--+-- This module supports the accompanying GHC plugin "Test.Inspection.Plugin" and adds+-- to GHC the ability to do inspeciton testing.++{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE StandaloneDeriving #-}+module Test.Inspection (+ -- * Synopsis+ -- $synposis++ -- * Registering obligations+ inspect,+ -- * Defining obligations+ Obligation(..), mkObligation, Property(..), (===), (=/=), hasNoType, ) where++import Control.Monad+import Language.Haskell.TH+import Language.Haskell.TH.Syntax (getQ, putQ, liftData)+import Data.Data++import Data.Maybe (fromMaybe)+import qualified Data.Set as S++import Test.Inspection.Internal++{- $synposis++To use inspection testing, you need to++ 1. enable the @TemplateHaskell@ langauge extension+ 2. load the plugin using @-fplugin Test.Inspection.Plugin@+ 3. declare your proof obligations using 'inspect'++An example module is++@+{-\# LANGAUGE TemplateHaskell \#-}+{-\# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin \#-}+module Simple where++import Test.Inspection+import Data.Maybe++lhs, rhs :: (a -> b) -> Maybe a -> Bool+lhs f x = isNothing (fmap f x)+rhs f Nothing = True+rhs f (Just _) = False++inspect $ 'lhs === 'rhs+@+-}++-- Description of test obligations++-- | This data type describes an inspection testing obligation.+--+-- It is recommended to build it using 'mkObligation', for backwards+-- compatibility when new fields are added. You can also use the more+-- memonic convenience functions like '(===)' or 'hasNoType'.+--+-- The obligation needs to be passed to 'inspect'.+data Obligation = Obligation+ { target :: Name+ -- ^ The target of a test obligation; invariably the name of a local+ -- definition. To get the name of a function @foo@, write @'foo@. This requires+ -- @{-\# LANGAUGE TemplateHaskell \#-}@.+ , property :: Property+ -- ^ The property of the target to be checked.+ , testName :: Maybe String+ -- ^ An optional name for the test+ , expectFail :: Bool+ -- ^ Do we expect this property to fail?+ , srcLoc :: Maybe Loc+ -- ^ The source location where this obligation is defined.+ -- This is filled in by 'inspect'.+ }+ deriving Data++-- | Properties of the obligation target to be checked.+data Property+ -- | Are the two functions equal?+ --+ -- More precisely: @f@ is equal to @g@ if either the definition of @f@ is+ -- @f = g@, or the definition of @g@ is @g = f@, or if the definitions are+ -- @f = e@ and @g = e@.+ = EqualTo Name++ -- | Does this type not occur anywhere in the definition of the function+ -- (neither locally bound nor passed as arguments)+ | NoType Name++ -- | Does this function perform no heap allocations.+ | NoAllocation+ deriving Data++allLocalNames :: Obligation -> [Name]+allLocalNames obl = target obl : goProp (property obl)+ where+ goProp :: Property -> [Name]+ goProp (EqualTo n) = [n]+ goProp _ = []++-- | Creates an inspection obligation for the given function name+-- with default values for the optional fields.+mkObligation :: Name -> Property -> Obligation+mkObligation target prop = Obligation+ { target = target+ , property = prop+ , testName = Nothing+ , srcLoc = Nothing+ , expectFail = False+ }++-- | Convenience function to declare two functions to be equal+(===) :: Name -> Name -> Obligation+(===) = mkEquality False+infix 1 ===++-- | Convenience function to declare two functions to be equal, but expect the test to fail+-- (This is useful for documentation purposes, or as a TODO list.)+(=/=) :: Name -> Name -> Obligation+(=/=) = mkEquality True+infix 1 =/=++mkEquality :: Bool -> Name -> Name -> Obligation+mkEquality expectFail n1 n2 = (mkObligation n1 (EqualTo n2)) { expectFail = expectFail }++-- | Convenience function to declare that a function’s implementation does not+-- mention a type+--+-- @inspect $ fusedFunction `hasNoType` ''[]@+hasNoType :: Name -> Name -> Obligation+hasNoType n tn = mkObligation n (NoType tn)++-- The exported TH functions++-- | As seen in the example above, the entry point to inspection testing is the+-- 'inspect' function, to which you pass an 'Obligation'.+inspect :: Obligation -> Q [Dec]+inspect obl = do+ loc <- location+ annExpr <- liftData (obl { srcLoc = Just loc })+ rememberDs <- concat <$> mapM rememberName (allLocalNames obl)+ pure $ PragmaD (AnnP ModuleAnnotation annExpr) : rememberDs++-- We need to ensure that names refernced in obligations are kept alive+-- We do so by annotating them with 'KeepAlive'++newtype SeenNames = SeenNames (S.Set Name)++-- Annotate each name only once+nameSeen :: Name -> Q Bool+nameSeen n = do+ SeenNames s <- fromMaybe (SeenNames S.empty) <$> getQ+ let seen = n `S.member` s+ unless seen $ putQ $ SeenNames (S.insert n s)+ pure seen++rememberName :: Name -> Q [Dec]+rememberName n = do+ seen <- nameSeen n+ if seen then return [] else do+ kaExpr <- liftData KeepAlive+ pure [ PragmaD (AnnP (ValueAnnotation n) kaExpr) ]
+ Test/Inspection/Core.hs view
@@ -0,0 +1,140 @@+-- | This module implements some of analyses of Core expressions necessary for+-- "Test.Inspection". Normally, users of this pacakge can ignore this module. +{-# LANGUAGE CPP #-}+module Test.Inspection.Core+ ( slice+ , eqSlice+ , freeOfType+ , doesNotAllocate+ ) where++import CoreSyn+import CoreUtils+import TyCoRep+import Type+import Var+import Id+import Name+import VarEnv+import Literal (nullAddrLit)++import qualified Data.Set as S+import Data.Maybe+import State+import Control.Monad++-- | Selects those bindings that define the given variable+slice :: [(Var, CoreExpr)] -> Var -> [(Var,CoreExpr)]+slice binds v = [(v,e) | (v,e) <- binds, v `S.member` used ]+ where+ used = execState (goV v) S.empty++ local = S.fromList (map fst binds)+ goV v | v `S.member` local = do+ seen <- gets (v `S.member`)+ unless seen $ do+ modify (S.insert v)+ let Just e = lookup v binds+ go e+ | otherwise = return ()++ go (Var v) = goV v+ go (Lit _ ) = pure ()+ go (App e arg) | isTypeArg arg = go e+ go (App e arg) = go e >> go arg+ go (Lam b e) | isTyVar b = go e+ go (Lam _ e) = go e+ go (Let bind body) = mapM_ go (rhssOfBind bind) >> go body+ go (Case s _ _ alts) = go s >> mapM_ goA alts+ go (Cast e _) = go e+ go (Tick _ e) = go e+ go (Type _) = pure ()+ go (Coercion _) = pure ()++ goA (_, _, e) = go e++-- | This is a heuristic, which only works if both slices+-- have auxillary variables in the right order.+-- (This is mostly to work-around the buggy CSE in GHC-8.0)+-- It also breaks if there is shadowing.+eqSlice :: [(Var, CoreExpr)] -> [(Var, CoreExpr)] -> Bool+eqSlice slice1 slice2 =+ eqExpr emptyInScopeSet (Let (Rec slice1) (Lit nullAddrLit))+ (Let (Rec slice2) (Lit nullAddrLit))++-- | Returns @True@ if the given core expression mentions no type constructor+-- anywhere that has the given name.+freeOfType :: [(Var, CoreExpr)] -> Name -> Maybe (Var, CoreExpr)+freeOfType slice tcN = listToMaybe [ (v,e) | (v,e) <- slice, not (go e) ]+ where+ goV v = goT (varType v)++ go (Var v) = goV v+ go (Lit _ ) = True+ go (App e a) = go e && go a+ go (Lam b e) = goV b && go e+ go (Let bind body) = all goB (flattenBinds [bind]) && go body+ go (Case s b _ alts) = go s && goV b && all goA alts+ go (Cast e _) = go e+ go (Tick _ e) = go e+ go (Type t) = (goT t)+ go (Coercion _) = True++ goB (b, e) = goV b && go e++ goA (_,pats, e) = all goV pats && go e++ goT (TyVarTy _) = True+ goT (AppTy t1 t2) = goT t1 && goT t2+ goT (TyConApp tc ts) = getName tc /= tcN && all goT ts+ -- ↑ This is the crucial bit+ goT (ForAllTy _ t) = goT t+#if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0)+ goT (FunTy t1 t2) = goT t1 && goT t2+#endif+ goT (LitTy _) = True+ goT (CastTy t _) = goT t+ goT (CoercionTy _) = True++-- | True if the given variable binding does not allocate, if called fully+-- satisfied.+--+-- It currently does not look through function calls, which of course could+-- allocate. It should probably at least look through local function calls.+--+-- The variable is important to know the arity of the function.+doesNotAllocate :: [(Var, CoreExpr)] -> Maybe (Var, CoreExpr)+doesNotAllocate slice = listToMaybe [ (v,e) | (v,e) <- slice, not (go (idArity v) e) ]+ where+ go _ (Var v)+ | isDataConWorkId v, idArity v > 0 = False+ go a (Var v) = (a >= idArity v)+ go _ (Lit _ ) = True+ go a (App e arg) | isTypeArg arg = go a e+ go a (App e arg) = go (a+1) e && goArg arg+ go a (Lam b e) | isTyVar b = go a e+ go 0 (Lam _ _) = False+ go a (Lam _ e) = go (a-1) e+ go a (Let bind body) = all goB (flattenBinds [bind]) && go a body+ go a (Case s _ _ alts) = go 0 s && all (goA a) alts+ go a (Cast e _) = go a e+ go a (Tick _ e) = go a e+ go _ (Type _) = True+ go _ (Coercion _) = True++ goArg e | exprIsTrivial e = go 0 e+ | isUnliftedType (exprType e) = go 0 e+ | otherwise = False++ goB (b, e)+#if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0)+ | isJoinId b = go (idArity b) e+#endif+ -- Not sure when a local function definition allocates…+ | isFunTy (idType b) = go (idArity b) e+ | isUnliftedType (idType b) = go (idArity b) e+ | otherwise = False+ -- A let binding allocates if any variable is not a join point and not+ -- unlifted++ goA a (_,_, e) = go a e
+ Test/Inspection/Internal.hs view
@@ -0,0 +1,21 @@+-- |+-- Description : Inspection testing+-- Copyright : (c) Joachim Breitner, 2017+-- License : MIT+-- Maintainer : mail@joachim-breitner.de+-- Portability : GHC specifc+--+{-# LANGUAGE DeriveDataTypeable #-}+module Test.Inspection.Internal (KeepAlive(..)) where++import Data.Data++-- | An annotation to keep names alive+data KeepAlive = KeepAlive+ deriving Data++{-+keep_alive :: a+keep_alive = keep_alive+{-# NOINLINE keep_alive #-}+-}
+ Test/Inspection/Plugin.hs view
@@ -0,0 +1,197 @@+-- | See "Test.Inspection".+{-# LANGUAGE CPP #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE MultiWayIf #-}+module Test.Inspection.Plugin (plugin) where++import Control.Monad+import System.Exit+import Data.Either+import Data.Maybe+import Data.List+import Data.Bifunctor+import qualified Language.Haskell.TH.Syntax as TH++import GhcPlugins hiding (SrcLoc)++import Test.Inspection.Internal (KeepAlive(..))+import Test.Inspection (Obligation(..), Property(..))+import Test.Inspection.Core++-- | The plugin. It supports the option @-fplugin-opt=Test.Inspection.Plugin=keep-going@ to+-- ignore a failing build.+plugin :: Plugin+plugin = defaultPlugin { installCoreToDos = install }++data UponFailure = AbortCompilation | KeepGoing deriving Eq++install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]+install args passes = return $ passes ++ [pass]+ where+ pass = CoreDoPluginPass "Test.Inspection" (proofPass upon_failure)+ upon_failure | "keep-going" `elem` args = KeepGoing+ | otherwise = AbortCompilation+++extractObligations :: ModGuts -> (ModGuts, [Obligation])+extractObligations guts = (guts { mg_rules = rules', mg_anns = anns_clean }, obligations)+ where+ rules' = mg_rules guts+ (anns', obligations) = partitionMaybe findObligationAnn (mg_anns guts)+ anns_clean = filter (not . isKeepAliveAnn) anns'++isKeepAliveAnn :: Annotation -> Bool+isKeepAliveAnn (Annotation (NamedTarget _) payload)+ | Just KeepAlive <- fromSerialized deserializeWithData payload+ = True+isKeepAliveAnn _+ = False++findObligationAnn :: Annotation -> Maybe Obligation+findObligationAnn (Annotation (ModuleTarget _) payload)+ | Just obl <- fromSerialized deserializeWithData payload+ = Just obl+findObligationAnn _+ = Nothing++prettyObligation :: Module -> Obligation -> String+prettyObligation mod (Obligation {..}) =+ maybe "" myPrettySrcLoc srcLoc ++ ": " +++ "inspecting " ++ prettyProperty mod target property +++ (if expectFail then " (failure expected)" else "")++prettyProperty :: Module -> TH.Name -> Property -> String+prettyProperty mod target (EqualTo n2) = showTHName mod target ++ " === " ++ showTHName mod n2+prettyProperty mod target (NoType t) = showTHName mod target ++ " `hasNoType` " ++ showTHName mod t+prettyProperty mod target NoAllocation = showTHName mod target ++ " does not allocate"++-- | Like show, but omit the module name if it is he current module+showTHName :: Module -> TH.Name -> String+showTHName mod (TH.Name occ (TH.NameQ m))+ | moduleNameString (moduleName mod) == TH.modString m = TH.occString occ+showTHName mod (TH.Name occ (TH.NameG _ _ m))+ | moduleNameString (moduleName mod) == TH.modString m = TH.occString occ+showTHName _ n = show n++checkObligation :: ModGuts -> Obligation -> CoreM Bool+checkObligation guts obl = do+ putMsgS $ prettyObligation (mg_module guts) obl++ res <- checkProperty guts (target obl) (property obl)++ case (res, expectFail obl) of+ -- Property holds+ (Nothing, False) -> do+ return True+ (Nothing, True) -> do+ putMsgS "Obligation passes unexpectedly"+ return False+ -- Property does not hold+ (Just reportMsg, False) -> do+ putMsgS "Obligation fails"+ reportMsg+ return False+ (Just _, True) -> do+ return True++type Result = Maybe (CoreM ())++lookupNameInGuts :: ModGuts -> Name -> Maybe (Var, CoreExpr)+lookupNameInGuts guts n = listToMaybe+ [ (v,e)+ | (v,e) <- flattenBinds (mg_binds guts)+ , getName v == n+ ]++checkProperty :: ModGuts -> TH.Name -> Property -> CoreM Result+checkProperty guts thn1 (EqualTo thn2) = do+ Just n1 <- thNameToGhcName thn1+ Just n2 <- thNameToGhcName thn2++ let p1 = lookupNameInGuts guts n1+ let p2 = lookupNameInGuts guts n2++ if | n1 == n2+ -> return Nothing+ -- Ok if one points to another+ | Just (_, Var other) <- p1, getName other == n2+ -> return Nothing+ | Just (_, Var other) <- p2, getName other == n1+ -> return Nothing+ -- OK if they have the same expression+ | Just (v1, _) <- p1+ , Just (v2, _) <- p2+ , eqSlice (slice binds v1) (slice binds v2)+ -> return Nothing+ -- Not ok if the expression differ+ | Just (_, e1) <- p1+ , Just (_, e2) <- p2+ -> pure . Just $ do+ putMsg $+ nest 4 (hang (text "LHS" <> colon) 4 (ppr e1)) $$+ nest 4 (hang (text "RHS" <> colon) 4 (ppr e2))+ -- Not ok if both names are bound externally+ | Nothing <- p1+ , Nothing <- p2+ -> pure . Just $ do+ putMsg $ ppr n1 <+> text " and " <+> ppr n2 <+>+ text "are different external names"+ where+ binds = flattenBinds (mg_binds guts)++checkProperty guts thn (NoType tht) = do+ Just n <- thNameToGhcName thn+ Just t <- thNameToGhcName tht+ case lookupNameInGuts guts n of+ Nothing -> pure . Just $ do+ putMsg $ ppr n <+> text "is not a local name"+ Just (v, _) -> case freeOfType (slice binds v) t of+ Just (v',e') -> pure . Just $ putMsg $ nest 4 (ppr v' <+> text "=" <+> ppr e')+ Nothing -> pure Nothing+ where binds = flattenBinds (mg_binds guts)++checkProperty guts thn NoAllocation = do+ Just n <- thNameToGhcName thn+ case lookupNameInGuts guts n of+ Nothing -> pure . Just $ do+ putMsg $ ppr n <+> text "is not a local name"+ Just (v, _) -> case doesNotAllocate (slice binds v) of+ Just (v',e') -> pure . Just $ putMsg $ nest 4 (ppr v' <+> text "=" <+> ppr e')+ Nothing -> pure Nothing+ where binds = flattenBinds (mg_binds guts)++proofPass :: UponFailure -> ModGuts -> CoreM ModGuts+proofPass upon_failure guts = do+ dflags <- getDynFlags+ when (optLevel dflags < 1) $+ warnMsg $ fsep $ map text $ words "Test.Inspection: Compilation without -O detected. Expect optimizations to fail."++ let (guts', obligations) = extractObligations guts+ ok <- and <$> mapM (checkObligation guts') obligations+ if ok+ then do+ let (_m,n) = bimap length length $ partition expectFail obligations+ putMsg $ text "Test.Inspection tested" <+> ppr n <+>+ text "obligation" <> (if n == 1 then empty else text "s")+ else do+ case upon_failure of+ AbortCompilation -> do+ errorMsg $ text "inspection testing unsuccessful"+ liftIO $ exitFailure -- kill the compiler. Is there a nicer way?+ KeepGoing -> do+ warnMsg $ text "inspection testing unsuccessful"+ return guts'++++partitionMaybe :: (a -> Maybe b) -> [a] -> ([a], [b])+partitionMaybe f = partitionEithers . map (\x -> maybe (Left x) Right (f x))++-- | like prettySrcLoc, but omits the module name+myPrettySrcLoc :: TH.Loc -> String+myPrettySrcLoc TH.Loc {..}+ = foldr (++) ""+ [ loc_filename, ":"+ , show (fst loc_start), ":"+ , show (snd loc_start)+ ]
+ examples/Fusion.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE TemplateHaskell #-}+{-# OPTIONS_GHC -fplugin Test.Inspection.Plugin #-}+module Fusion where++import Test.Inspection+import Data.List (foldl', sort)++sumUp1 :: Int -> Bool+sumUp1 n = sum [1..n] > 1000++sumUp2 :: Int -> Bool+sumUp2 n | 1 > n = False+sumUp2 n = go 1 0 > 1000+ where+ go m s | m == n = (s + m)+ | otherwise = go (m+1) (s+m)++-- Example for a non-fusing funtion+sumUpSort :: Int -> Int+sumUpSort n = sum . sort $ [1..n]++inspect $ 'sumUp1 === 'sumUp2+inspect $ 'sumUp1 `hasNoType` ''[]+inspect $ ('sumUp1 `hasNoType` ''Int) { expectFail = True }+inspect $ mkObligation 'sumUp1 NoAllocation+inspect $ ('sumUpSort `hasNoType` ''[]) { expectFail = True }++main :: IO ()+main = return ()
+ examples/GenericLens.hs view
@@ -0,0 +1,48 @@+{-# LANGUAGE RankNTypes, DeriveGeneric, TypeApplications, DataKinds, ExistentialQuantification, TemplateHaskell #-}+{-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-}+module GenericLens (main) where++import GHC.Generics+import Data.Generics.Product+import Test.Inspection++data Record = MkRecord { fieldA :: Int+ , fieldB :: Bool+ } deriving Generic++type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s++fieldALensManual :: Lens' Record Int+fieldALensManual f (MkRecord a b) = (\a -> MkRecord a b) <$> f a++-- Coyoneda optimization++data Coyoneda f b = forall a. Coyoneda (a -> b) (f a)++instance Functor (Coyoneda f) where+ fmap f (Coyoneda g fa) = Coyoneda (f . g) fa++inj :: Functor f => Coyoneda f a -> f a+inj (Coyoneda f a) = fmap f a++proj :: Functor f => f a -> Coyoneda f a+proj fa = Coyoneda id fa++ravel :: Functor f => ((a -> Coyoneda f b) -> (s -> Coyoneda f t))+ -> (a -> f b) -> (s -> f t)+ravel coy f s = inj $ coy (\a -> proj (f a)) s++-- the examples++fieldALensGeneric :: Lens' Record Int+fieldALensGeneric = field @"fieldA"++fieldALensGenericYoneda :: Lens' Record Int+fieldALensGenericYoneda = ravel (field @"fieldA")++main :: IO ()+main = return ()++-- the check+inspect $ 'fieldALensManual === 'fieldALensGenericYoneda+
+ examples/NS_NP.hs view
@@ -0,0 +1,44 @@+{-# LANGUAGE GADTs, TypeFamilies, DataKinds, PolyKinds, TypeOperators #-}+{-# LANGUAGE TemplateHaskell #-}+{-# OPTIONS_GHC -O #-}+{-# OPTIONS_GHC -fplugin Test.Inspection.Plugin #-}+module NS_NP where++import Test.Inspection++data NS (f :: k -> *) (xs :: [k]) where+ Z :: f x -> NS f (x : xs)+ S :: !(NS f xs) -> NS f (x : xs)++data NP (f :: k -> *) (xs :: [k]) where+ Nil :: NP f '[]+ (:*) :: f x -> !(NP f xs) -> NP f (x : xs)++newtype I a = I a++from :: Ordering -> NS (NP I) '[ '[], '[], '[] ]+from = \ x -> case x of+ LT -> Z Nil+ EQ -> S (Z Nil)+ GT -> S (S (Z Nil))+{-# INLINE from #-}++to :: NS (NP I) '[ '[], '[], '[] ] -> Ordering+to = \ x -> case x of+ (Z Nil) -> LT+ (S (Z Nil)) -> EQ+ (S (S (Z Nil))) -> GT+ _ -> error "unreachable"+{-# INLINE to #-}++roundtrip :: Ordering -> Ordering+roundtrip = to . from+{-# INLINE roundtrip #-}++roundtrip_id :: Ordering -> Ordering+roundtrip_id x = x++main :: IO ()+main = return ()++inspect $ 'roundtrip === 'roundtrip_id
+ examples/Simple.hs view
@@ -0,0 +1,17 @@+{-# LANGUAGE TemplateHaskell #-}+{-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-}+module Simple where++import Test.Inspection+import Data.Maybe++lhs, rhs :: (a -> b) -> Maybe a -> Bool+lhs f x = isNothing (fmap f x)++rhs f Nothing = True+rhs f (Just _) = False++inspect $ 'lhs === 'rhs++main :: IO ()+main = return ()
+ examples/Text.hs view
@@ -0,0 +1,28 @@+{-# LANGUAGE TemplateHaskell #-}+{-# OPTIONS_GHC -fplugin Test.Inspection.Plugin #-}+module Text where++import Test.Inspection++import Data.Text as T+import Data.Text.Encoding as E+import Data.ByteString (ByteString)++-- Some cases of successful fusion:+toUpperString :: String -> String+toUpperString = T.unpack . T.toUpper . T.pack++toUpperBytestring :: ByteString -> String+toUpperBytestring = T.unpack . T.toUpper . E.decodeUtf8++-- This is the example from the text documentation.+-- Unfortunately it fails, the problem seems to be T.length.+countChars :: ByteString -> Int+countChars = T.length . T.toUpper . E.decodeUtf8++inspect $ 'toUpperString `hasNoType` ''T.Text+inspect $ 'toUpperBytestring `hasNoType` ''T.Text+inspect $ ('countChars `hasNoType` ''T.Text) { expectFail = True }++main :: IO ()+main = return ()
+ inspection-testing.cabal view
@@ -0,0 +1,103 @@+name: inspection-testing+version: 0.1+synopsis: GHC plugin to do inspection esting+description: Some carefully crafted libraries make promises to their+ users beyond functionality and performance.+ .+ Examples are: Fusion libraries promise intermediate data+ structures to be eliminated. Generic programming libraries promise+ that the generic implementation is identical to the+ hand-written one. Some libraries may promise allocation-free+ or branch-free code.+ .+ Conventionally, the modus operandi in all these cases is+ that the library author manually inspects the (intermediate or+ final) code produced by the compiler. This is not only+ tedious, but makes it very likely that some change, either+ in the library itself or the surrounding eco-system,+ breaks the library’s promised without anyone noticing.+ .+ This package provides a disciplined way of specifying such+ properties, and have them checked by the compiler. This way,+ this checking can be part of the ususal development cycle+ and regressions caught early.+ .+ See the documentation in "Test.Inspection" or the project+ webpage for more examples and more information.+category: Testing, Compiler Plugin+homepage: https://github.com/nomeata/inspection-testing+license: MIT+license-file: LICENSE+author: Joachim Breitner+maintainer: mail@joachim-breitner.de+copyright: 2017 Joachim Breitner+build-type: Simple+extra-source-files: ChangeLog.md, README.md+cabal-version: >=1.10+Tested-With: GHC == 8.0.2, GHC == 8.2.*, GHC == 8.3.*++source-repository head+ type: git+ location: git://github.com/nomeata/inspection-testing.git++library+ exposed-modules: Test.Inspection+ Test.Inspection.Plugin+ Test.Inspection.Internal+ Test.Inspection.Core+ build-depends: base >=4.9 && <4.12+ build-depends: ghc >= 8.0.2 && <8.4+ build-depends: template-haskell+ build-depends: containers+ default-language: Haskell2010+ ghc-options: -Wall -Wno-name-shadowing++test-suite NS_NP+ type: exitcode-stdio-1.0+ hs-source-dirs: examples+ main-is: NS_NP.hs+ build-depends: inspection-testing+ build-depends: base >=4.9 && <4.12+ default-language: Haskell2010+ ghc-options: -main-is NS_NP+++test-suite generic-lens+ type: exitcode-stdio-1.0+ hs-source-dirs: examples+ main-is: GenericLens.hs+ build-depends: inspection-testing+ build-depends: base >=4.9 && <4.12+ build-depends: generic-lens ==0.4.0.1+ default-language: Haskell2010+ ghc-options: -main-is GenericLens++test-suite simple+ type: exitcode-stdio-1.0+ hs-source-dirs: examples+ main-is: Simple.hs+ build-depends: inspection-testing+ build-depends: base >=4.9 && <4.12+ default-language: Haskell2010+ ghc-options: -main-is Simple++test-suite fusion+ type: exitcode-stdio-1.0+ hs-source-dirs: examples+ main-is: Fusion.hs+ build-depends: inspection-testing+ build-depends: base >=4.9 && <4.12+ default-language: Haskell2010+ ghc-options: -main-is Fusion++test-suite text+ type: exitcode-stdio-1.0+ hs-source-dirs: examples+ main-is: Text.hs+ build-depends: inspection-testing+ build-depends: base >=4.9 && <4.12+ build-depends: text ==1.2.2.2+ build-depends: bytestring+ default-language: Haskell2010+ ghc-options: -main-is Text+