diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -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 diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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. + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/Test/Inspection.hs b/Test/Inspection.hs new file mode 100644 --- /dev/null +++ b/Test/Inspection.hs @@ -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) ] diff --git a/Test/Inspection/Core.hs b/Test/Inspection/Core.hs new file mode 100644 --- /dev/null +++ b/Test/Inspection/Core.hs @@ -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 diff --git a/Test/Inspection/Internal.hs b/Test/Inspection/Internal.hs new file mode 100644 --- /dev/null +++ b/Test/Inspection/Internal.hs @@ -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 #-} +-} diff --git a/Test/Inspection/Plugin.hs b/Test/Inspection/Plugin.hs new file mode 100644 --- /dev/null +++ b/Test/Inspection/Plugin.hs @@ -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) + ] diff --git a/examples/Fusion.hs b/examples/Fusion.hs new file mode 100644 --- /dev/null +++ b/examples/Fusion.hs @@ -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 () diff --git a/examples/GenericLens.hs b/examples/GenericLens.hs new file mode 100644 --- /dev/null +++ b/examples/GenericLens.hs @@ -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 + diff --git a/examples/NS_NP.hs b/examples/NS_NP.hs new file mode 100644 --- /dev/null +++ b/examples/NS_NP.hs @@ -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 diff --git a/examples/Simple.hs b/examples/Simple.hs new file mode 100644 --- /dev/null +++ b/examples/Simple.hs @@ -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 () diff --git a/examples/Text.hs b/examples/Text.hs new file mode 100644 --- /dev/null +++ b/examples/Text.hs @@ -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 () diff --git a/inspection-testing.cabal b/inspection-testing.cabal new file mode 100644 --- /dev/null +++ b/inspection-testing.cabal @@ -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 +