inspection-testing

GHC plugin to do inspection testing https://github.com/nomeata/inspection-testing

Latest on Hackage:0.4.2.4

See all snapshots inspection-testing appears in

MIT licensed by Joachim Breitner
Maintained by [email protected]

Module documentation for 0.2.0.1

This version can be pinned in stack with:[email protected]:d7847f3cdedc27e3237b607e0683ed158b48c9d31e88ee22d3e9a9ce04b441ef,4742

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:

{-# 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

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: lhs === rhs passed.
inspection testing successful
      expected successes: 1

See the examples/ directory for more examples of working proofs.

If an assertion fails, for example

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 -dsuppress-idinfo
[5 of 5] Compiling Simple           ( examples/Simple.hs, examples/Simple.o )
examples/Simple.hs:14:1: lhs === rhs passed.
examples/Simple.hs:20:1: bad1 === bad2 failed:
    LHS:
        bad1 :: Int
        bad1 = I# 4#

    RHS:
        bad2 :: Int
        bad2 = I# 5#


examples/Simple.hs: error:
    inspection testing unsuccessful
          expected successes: 1
         unexpected failures: 1

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.

Help, I am drowining in Core!

inspection-testing prints the Core more or less like GHC would, and the same flags can be used to control the level of detail. In particular, you might want to pass to GHC a selection of the following flags:

-dsuppress-idinfo -dsuppress-coercions -dsuppress-type-applications
-dsuppress-module-prefixes -dsuppress-type-signatures -dsuppress-uniques

Can I comment or help?

Sure! We can use the GitHub issue tracker for discussions, and obviously contributions are welcome.

Changes

Revision history for inspection-testing

0.2.0.1 – 2018-02-02

  • Support GHC HEAD (8.5)

0.2 – 2018-01-17

  • With $(inspectTest obligation) you can now get the result of inspection testing at run-time, for integration into your test suite.

0.1.2 – 2017-11-20

  • Make (==-) a bit more liberal, and look through variable redefinitions that only change the type

0.1.1.2 – 2017-11-12

  • Hotfix: Do not abort if there are expected failures

0.1.1.1 – 2017-11-12

  • Show summary stats
  • Pull in less tests, to make inclusion in stackage easier

0.1.1 – 2017-11-09

  • More complete output when (===) fails
  • Variant (==-) that ignores types when comparing terms

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