diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,158 +1,163 @@ -# Revision history for inspection-testing - -## 0.6.2 -- 2025-06-13 - -* Fix an bug that would cause a GHC panic -* Fix `=/~` and `=/-` -* Syntax directed comparison of lets - -(all thanks Oleg Grenrus) - -## 0.6.1 -- 2025-06-11 - -* Improve presentation of term inequalities (thanks Oleg Grenrus) - -## 0.6 -- 2025-01-01 - -* Support GHC 9.10.1 (thanks Andre Van Der Merwe) -* Support GHC 9.12 (thanks Erik de Castro Lopo) -* Ignore SourceNote tick (thanks Potato Hatsue) - -## 0.5.0.3 -- 2023-12-29 - -* Support GHC 9.10 (thanks Bodigrim) - -## 0.5.0.2 -- 2023-07-10 - -* Support GHC 9.8 (thanks Bodigrim) - -## 0.5.0.1 -- 2023-01-15 - -* Support mtl-2.3 and GHC 9.6 (thanks Bodigrim) - -## 0.5 -- 2022-06-15 - -* New equivalence `==~` that accepts different order of bindings in lets. (thanks @phadej) -* When printing terms that differ, common up a common prefix of lambdas (thanks @phadej) - -## 0.4.6.1 -- 2022-05-20 - -* Support GHC 9.4 (thanks @parsonsmatt) - -## 0.4.6.0 -- 2020-08-23 - -* Support GHC 9.2 (thanks @Bodigrim) - -## 0.4.5.0 -- 2020-04-28 - -* Export some internals from `Test.Inspection.Plugin`, to make integration into - testing frameworks easier (thanks @Bodigrim) - -## 0.4.4.0 -- 2020-04-21 - -* More GHC-9.0 compatibility (thanks @aadaa-fgtaa) - -## 0.4.3.0 -- 2020-01-26 - -* Ignores HPC ticks in `(==-)` (thanks @konn) -* Add `(=/-)` operator (thanks @lysxia) -* Add skip-O0 plugin option (thanks @AndrasKovacs) -* GHC-9.0 compatibility (thanks @konn) -* CI now runs on Github Actions (thanks @phadej) - -## 0.4.2.4 -- 2020-01-26 - -* Now prints the name of the type class on which a test fails, thanks to - Harendra Kumar -* More examples, thanks to Rafe - -## 0.4.2.3 -- 2020-01-26 - -* Support GHC-8.10, thanks to Ryan Scott via head.hackage for the patch - -## 0.4.2.1 -- 2019-06-07 - -* Bugfix release - -## 0.4.2 -- 2019-06-05 - -* Be less picky if mutually recursive definitions appear in a different order - in the source -* Add obligation `coreOf`, which succeeds, but lets you dump the core of a - single symbol (thanks to @phadej) -* Support `-fplugin-opt=Test.Inspection.Plugin:keep-going-O0` (thanks to @phadej) - -## 0.4.1.2 -- 2019-02-23 - -* Do not force recompilation with GHC >= 8.6 -* Support `-fplugin-opt=Test.Inspection.Plugin:quiet` - -## 0.4.1.1 -- 2018-11-17 - -* Fix a bug with `doesNotUse` and data constructors - -## 0.4.1 -- 2018-11-17 - -* New obligation `doesNotUse` -* Use the Obligation’s testName in the plugin output. -* In `inspect`, do not override `srcLoc` if already present. - -## 0.4 -- 2018-10-12 - -* Support GHC-8.6 -* On GHC-8.4 or newer, `inspect` and `inspectTest` will automatically load the - plugin. - -## 0.3 -- 2018-07-07 - -* On GHC-8.5 or newer, use of `inspect` or `inspectTest` without actually - loading the plugin will cause compilation to fail at type-checking time - (thanks to @adamgundry for the idea) -* Support for `hasNoTypeClass` (thanks to @phadej) -* Support for `hasNoGenerics` (thanks to @isovector) -* No need to keep referenced variables alive using annotations: - Simply mentioning them in a Template Haskell splice keeps them alive! - -## 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 +# Revision history for inspection-testing + +## 0.6.3 -- 2026-01-17 + +* Compatibility with GHC 9.14 +* Remove spurious mtl dependency + +## 0.6.2 -- 2025-06-13 + +* Fix an bug that would cause a GHC panic +* Fix `=/~` and `=/-` +* Syntax directed comparison of lets + +(all thanks Oleg Grenrus) + +## 0.6.1 -- 2025-06-11 + +* Improve presentation of term inequalities (thanks Oleg Grenrus) + +## 0.6 -- 2025-01-01 + +* Support GHC 9.10.1 (thanks Andre Van Der Merwe) +* Support GHC 9.12 (thanks Erik de Castro Lopo) +* Ignore SourceNote tick (thanks Potato Hatsue) + +## 0.5.0.3 -- 2023-12-29 + +* Support GHC 9.10 (thanks Bodigrim) + +## 0.5.0.2 -- 2023-07-10 + +* Support GHC 9.8 (thanks Bodigrim) + +## 0.5.0.1 -- 2023-01-15 + +* Support mtl-2.3 and GHC 9.6 (thanks Bodigrim) + +## 0.5 -- 2022-06-15 + +* New equivalence `==~` that accepts different order of bindings in lets. (thanks @phadej) +* When printing terms that differ, common up a common prefix of lambdas (thanks @phadej) + +## 0.4.6.1 -- 2022-05-20 + +* Support GHC 9.4 (thanks @parsonsmatt) + +## 0.4.6.0 -- 2020-08-23 + +* Support GHC 9.2 (thanks @Bodigrim) + +## 0.4.5.0 -- 2020-04-28 + +* Export some internals from `Test.Inspection.Plugin`, to make integration into + testing frameworks easier (thanks @Bodigrim) + +## 0.4.4.0 -- 2020-04-21 + +* More GHC-9.0 compatibility (thanks @aadaa-fgtaa) + +## 0.4.3.0 -- 2020-01-26 + +* Ignores HPC ticks in `(==-)` (thanks @konn) +* Add `(=/-)` operator (thanks @lysxia) +* Add skip-O0 plugin option (thanks @AndrasKovacs) +* GHC-9.0 compatibility (thanks @konn) +* CI now runs on Github Actions (thanks @phadej) + +## 0.4.2.4 -- 2020-01-26 + +* Now prints the name of the type class on which a test fails, thanks to + Harendra Kumar +* More examples, thanks to Rafe + +## 0.4.2.3 -- 2020-01-26 + +* Support GHC-8.10, thanks to Ryan Scott via head.hackage for the patch + +## 0.4.2.1 -- 2019-06-07 + +* Bugfix release + +## 0.4.2 -- 2019-06-05 + +* Be less picky if mutually recursive definitions appear in a different order + in the source +* Add obligation `coreOf`, which succeeds, but lets you dump the core of a + single symbol (thanks to @phadej) +* Support `-fplugin-opt=Test.Inspection.Plugin:keep-going-O0` (thanks to @phadej) + +## 0.4.1.2 -- 2019-02-23 + +* Do not force recompilation with GHC >= 8.6 +* Support `-fplugin-opt=Test.Inspection.Plugin:quiet` + +## 0.4.1.1 -- 2018-11-17 + +* Fix a bug with `doesNotUse` and data constructors + +## 0.4.1 -- 2018-11-17 + +* New obligation `doesNotUse` +* Use the Obligation’s testName in the plugin output. +* In `inspect`, do not override `srcLoc` if already present. + +## 0.4 -- 2018-10-12 + +* Support GHC-8.6 +* On GHC-8.4 or newer, `inspect` and `inspectTest` will automatically load the + plugin. + +## 0.3 -- 2018-07-07 + +* On GHC-8.5 or newer, use of `inspect` or `inspectTest` without actually + loading the plugin will cause compilation to fail at type-checking time + (thanks to @adamgundry for the idea) +* Support for `hasNoTypeClass` (thanks to @phadej) +* Support for `hasNoGenerics` (thanks to @isovector) +* No need to keep referenced variables alive using annotations: + Simply mentioning them in a Template Haskell splice keeps them alive! + +## 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 diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,20 +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. +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 --- a/README.md +++ b/README.md @@ -1,119 +1,119 @@ -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 -{-# LANGUAGE TemplateHaskell #-} -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/`](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 -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 a a use of certian functions - * checking the absence of allocation (generally useful) - * checking the absence of typeclass-overloaded code - -In general, the checks need to be placed in the same module as the -checked-definition. - -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 drowning 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 - - -It does not seem to do anything (on GHC < 8.4) ----------------------------------------------- - -Add this line to your module: - - {-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-} - -Can I comment or help? ----------------------- - -Sure! We can use the GitHub issue tracker for discussions, and obviously -contributions are welcome. - +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 +{-# LANGUAGE TemplateHaskell #-} +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/`](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 -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 a a use of certian functions + * checking the absence of allocation (generally useful) + * checking the absence of typeclass-overloaded code + +In general, the checks need to be placed in the same module as the +checked-definition. + +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 drowning 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 + + +It does not seem to do anything (on GHC < 8.4) +---------------------------------------------- + +Add this line to your module: + + {-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-} + +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 --- a/Setup.hs +++ b/Setup.hs @@ -1,2 +1,2 @@ -import Distribution.Simple -main = defaultMain +import Distribution.Simple +main = defaultMain diff --git a/examples/DWARF.hs b/examples/DWARF.hs --- a/examples/DWARF.hs +++ b/examples/DWARF.hs @@ -1,18 +1,18 @@ -{-# LANGUAGE TemplateHaskell #-} -{-# OPTIONS_GHC -g #-} -module DWARF (main) where - -import Test.Inspection -import Data.Maybe - -lhs :: (a -> b) -> Maybe a -> Bool -lhs f x = isNothing (fmap f x) - -rhs :: (a -> b) -> Maybe a -> Bool -rhs f Nothing = True -rhs f (Just _) = False - -inspect $ 'lhs === 'rhs - -main :: IO () -main = return () +{-# LANGUAGE TemplateHaskell #-} +{-# OPTIONS_GHC -g #-} +module DWARF where + +import Test.Inspection +import Data.Maybe + +lhs :: (a -> b) -> Maybe a -> Bool +lhs f x = isNothing (fmap f x) + +rhs :: (a -> b) -> Maybe a -> Bool +rhs f Nothing = True +rhs f (Just _) = False + +inspect $ 'lhs === 'rhs + +main :: IO () +main = return () diff --git a/examples/Dictionary.hs b/examples/Dictionary.hs --- a/examples/Dictionary.hs +++ b/examples/Dictionary.hs @@ -1,36 +1,36 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE TemplateHaskell #-} -module Dictionary (main) where - -import Test.Inspection -import Control.Monad.IO.Class (MonadIO (..)) -import Control.Monad (replicateM_) -import Data.Traversable (foldMapDefault) -import Data.Semigroup (Semigroup) - -putStrLn' :: MonadIO m => String -> m () -putStrLn' = liftIO . putStrLn - -action :: MonadIO m => m () -action = putStrLn' "foo" >> putStrLn' "bar" - -specialized :: IO () -specialized = action - -inspect $ hasNoTypeClasses 'specialized -inspect $ (hasNoTypeClasses 'action) { expectFail = True } - -inspect $ hasNoTypeClassesExcept 'action [''MonadIO, ''Monad, ''Applicative, ''Functor] - -listFoldMap :: Monoid m => (a -> m) -> [a] -> m -listFoldMap = foldMapDefault - -#if __GLASGOW_HASKELL__ >= 802 -inspect $ hasNoTypeClassesExcept 'listFoldMap [''Monoid, ''Semigroup] -#else -inspect $ (hasNoTypeClassesExcept 'listFoldMap [''Monoid, ''Semigroup]) { expectFail = True } -#endif - - -main :: IO () -main = return () +{-# LANGUAGE CPP #-} +{-# LANGUAGE TemplateHaskell #-} +module Dictionary where + +import Test.Inspection +import Control.Monad.IO.Class (MonadIO (..)) +import Control.Monad (replicateM_) +import Data.Traversable (foldMapDefault) +import Data.Semigroup (Semigroup) + +putStrLn' :: MonadIO m => String -> m () +putStrLn' = liftIO . putStrLn + +action :: MonadIO m => m () +action = putStrLn' "foo" >> putStrLn' "bar" + +specialized :: IO () +specialized = action + +inspect $ hasNoTypeClasses 'specialized +inspect $ (hasNoTypeClasses 'action) { expectFail = True } + +inspect $ hasNoTypeClassesExcept 'action [''MonadIO, ''Monad, ''Applicative, ''Functor] + +listFoldMap :: Monoid m => (a -> m) -> [a] -> m +listFoldMap = foldMapDefault + +#if __GLASGOW_HASKELL__ >= 802 +inspect $ hasNoTypeClassesExcept 'listFoldMap [''Monoid, ''Semigroup] +#else +inspect $ (hasNoTypeClassesExcept 'listFoldMap [''Monoid, ''Semigroup]) { expectFail = True } +#endif + + +main :: IO () +main = return () diff --git a/examples/DoesNotUse.hs b/examples/DoesNotUse.hs --- a/examples/DoesNotUse.hs +++ b/examples/DoesNotUse.hs @@ -1,19 +1,20 @@ -{-# LANGUAGE TemplateHaskell #-} -module DoesNotUse where - -import Test.Inspection -import Control.Exception.Base (patError) - -matches (Just _) = True -matches Nothing = False - -partial (Just _) = Left - - -inspect $ ('matches `doesNotUse` 'Just) { expectFail = True } -inspect $ 'matches `doesNotUse` 'patError -inspect $ ('partial `doesNotUse` 'patError) { expectFail = True } -inspect $ ('partial `doesNotUse` 'Left) { expectFail = True } - -main :: IO () -main = return () +{-# LANGUAGE TemplateHaskell #-} +{-# OPTIONS_GHC -Wno-incomplete-patterns #-} +module DoesNotUse where + +import Test.Inspection +import Control.Exception.Base (patError) + +matches (Just _) = True +matches Nothing = False + +partial (Just _) = Left + + +inspect $ ('matches `doesNotUse` 'Just) { expectFail = True } +inspect $ 'matches `doesNotUse` 'patError +inspect $ ('partial `doesNotUse` 'patError) { expectFail = True } +inspect $ ('partial `doesNotUse` 'Left) { expectFail = True } + +main :: IO () +main = return () diff --git a/examples/Fusion.hs b/examples/Fusion.hs --- a/examples/Fusion.hs +++ b/examples/Fusion.hs @@ -1,37 +1,37 @@ -{-# LANGUAGE TemplateHaskell, CPP #-} -{-# OPTIONS_GHC -dsuppress-all -funfolding-use-threshold=120 #-} -module Fusion (main) where - -import Test.Inspection -import Data.List (foldl', sort) - -sumUp1 :: Int -> Bool -sumUp1 n = sum [1..n] > 1000 - -inspect $ 'sumUp1 `hasNoType` ''[] -inspect $ ('sumUp1 `hasNoType` ''Int) { expectFail = True } -inspect $ mkObligation 'sumUp1 NoAllocation - --- This stopped working in GHC-9.0, because --- * the > 1000 comparison is floated into the recursive join point (ok) --- * `sumUp2` is compiled with a worker-wrapper split that does not happen for --- sumUp1 (hard to fix) --- so I am disabling this part of the test on GHC-9.0 - -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) - -inspect $ 'sumUp1 === 'sumUp2 - --- Example for a non-fusing funtion -sumUpSort :: Int -> Int -sumUpSort n = sum . sort $ [1..n] - -inspect $ ('sumUpSort `hasNoType` ''[]) { expectFail = True } - -main :: IO () -main = return () +{-# LANGUAGE TemplateHaskell, CPP #-} +{-# OPTIONS_GHC -dsuppress-all -funfolding-use-threshold=120 #-} +module Fusion where + +import Test.Inspection +import Data.List (foldl', sort) + +sumUp1 :: Int -> Bool +sumUp1 n = sum [1..n] > 1000 + +inspect $ 'sumUp1 `hasNoType` ''[] +inspect $ ('sumUp1 `hasNoType` ''Int) { expectFail = True } +inspect $ mkObligation 'sumUp1 NoAllocation + +-- This stopped working in GHC-9.0, because +-- * the > 1000 comparison is floated into the recursive join point (ok) +-- * `sumUp2` is compiled with a worker-wrapper split that does not happen for +-- sumUp1 (hard to fix) +-- so I am disabling this part of the test on GHC-9.0 + +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) + +inspect $ 'sumUp1 === 'sumUp2 + +-- Example for a non-fusing funtion +sumUpSort :: Int -> Int +sumUpSort n = sum . sort $ [1..n] + +inspect $ ('sumUpSort `hasNoType` ''[]) { expectFail = True } + +main :: IO () +main = return () diff --git a/examples/GenericLens.hs b/examples/GenericLens.hs --- a/examples/GenericLens.hs +++ b/examples/GenericLens.hs @@ -1,49 +1,49 @@ -{-# LANGUAGE RankNTypes, DeriveGeneric, TypeApplications, DataKinds, ExistentialQuantification, TemplateHaskell #-} -{-# OPTIONS_GHC -dsuppress-idinfo #-} -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 === 'fieldALensGeneric -inspect $ 'fieldALensManual === 'fieldALensGenericYoneda - +{-# LANGUAGE RankNTypes, DeriveGeneric, TypeApplications, DataKinds, ExistentialQuantification, TemplateHaskell #-} +{-# OPTIONS_GHC -dsuppress-idinfo #-} +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 === 'fieldALensGeneric +inspect $ 'fieldALensManual === 'fieldALensGenericYoneda + diff --git a/examples/Generics.hs b/examples/Generics.hs --- a/examples/Generics.hs +++ b/examples/Generics.hs @@ -1,29 +1,29 @@ -{-# LANGUAGE DeriveGeneric, TemplateHaskell #-} -module Generics (main) where - -import GHC.Generics -import Test.Inspection - -data Record = MkRecord - { fieldA :: Int - , fieldB :: Bool - } deriving Generic - - -myRecord :: Record -myRecord = MkRecord 1 True - -genericRep :: Rep Record x -genericRep = from myRecord - - -roundTripRep :: Record -roundTripRep = to $ from myRecord - -main :: IO () -main = return () - --- the check -inspect $ hasNoGenerics 'roundTripRep -inspect $ (hasNoGenerics 'genericRep) { expectFail = True } - +{-# LANGUAGE DeriveGeneric, TemplateHaskell #-} +module Generics where + +import GHC.Generics +import Test.Inspection + +data Record = MkRecord + { fieldA :: Int + , fieldB :: Bool + } deriving Generic + + +myRecord :: Record +myRecord = MkRecord 1 True + +genericRep :: Rep Record x +genericRep = from myRecord + + +roundTripRep :: Record +roundTripRep = to $ from myRecord + +main :: IO () +main = return () + +-- the check +inspect $ hasNoGenerics 'roundTripRep +inspect $ (hasNoGenerics 'genericRep) { expectFail = True } + diff --git a/examples/HPCs.hs b/examples/HPCs.hs --- a/examples/HPCs.hs +++ b/examples/HPCs.hs @@ -1,22 +1,22 @@ -{-# LANGUAGE TemplateHaskell #-} -{-# OPTIONS_GHC -O -fhpc -fplugin-opt=Test.Inspection.Plugin:quiet #-} -module HPCs (main) where - -import Test.Inspection - -main :: IO () -main = return () - -theTwo :: Int -theTwo = 2 - -anotherTwo :: Int -anotherTwo = 2 - -theOnePlusOne :: Int -theOnePlusOne = 1 + 1 - -inspect $ 'theTwo ==- 'theOnePlusOne -inspect $ 'theTwo ==- 'anotherTwo -inspect $ 'theTwo =/= 'theOnePlusOne -inspect $ 'theTwo =/= 'anotherTwo +{-# LANGUAGE TemplateHaskell #-} +{-# OPTIONS_GHC -O -fhpc -fplugin-opt=Test.Inspection.Plugin:quiet #-} +module HPCs where + +import Test.Inspection + +main :: IO () +main = return () + +theTwo :: Int +theTwo = 2 + +anotherTwo :: Int +anotherTwo = 2 + +theOnePlusOne :: Int +theOnePlusOne = 1 + 1 + +inspect $ 'theTwo ==- 'theOnePlusOne +inspect $ 'theTwo ==- 'anotherTwo +inspect $ 'theTwo =/= 'theOnePlusOne +inspect $ 'theTwo =/= 'anotherTwo diff --git a/examples/LetsTest.hs b/examples/LetsTest.hs --- a/examples/LetsTest.hs +++ b/examples/LetsTest.hs @@ -1,56 +1,56 @@ -{-# LANGUAGE TemplateHaskell #-} -{-# OPTIONS_GHC -dsuppress-all #-} -module Main (main) where - -import Test.Inspection -import Data.Char (toUpper) -import System.Exit - -lhs1, rhs1 :: Char -> Char -> String - -lhs1 x y = let x' = toUpper x - y' = toUpper y - in [x', x', y', y'] - -rhs1 x y = let y' = toUpper y - x' = toUpper x - in [x', x', y', y'] - --- recursive -lhs2, rhs2, rhs2b :: String -lhs2 = let zs = 'z' : xs - xs = 'x' : ys - ys = 'y' : xs - in zs - -rhs2 = let ys = 'y' : xs - xs = 'x' : ys - zs = 'z' : xs - in zs - -rhs2b = let ys = 'y' : xs - xs = 'x' : ys - zs = 'z' : ys - in zs - -printResult :: Result -> IO () -printResult (Success s) = putStrLn s -printResult (Failure s) = putStrLn s - -isSuccess :: Result -> Bool -isSuccess (Success _) = True -isSuccess (Failure _) = False - -results :: [Result] -results = - [ $(inspectTest $ 'lhs1 ==~ 'rhs1) - , $(inspectTest $ 'lhs2 ==- 'rhs2) -- here GHC orders let bindings by itself! - , $(inspectTest $ 'lhs2 =/~ 'rhs2b) - ] - -main :: IO () -main = do - mapM_ printResult results - if map isSuccess results == [True, True, False] - then exitSuccess - else exitFailure +{-# LANGUAGE TemplateHaskell #-} +{-# OPTIONS_GHC -dsuppress-all #-} +module Main where + +import Test.Inspection +import Data.Char (toUpper) +import System.Exit + +lhs1, rhs1 :: Char -> Char -> String + +lhs1 x y = let x' = toUpper x + y' = toUpper y + in [x', x', y', y'] + +rhs1 x y = let y' = toUpper y + x' = toUpper x + in [x', x', y', y'] + +-- recursive +lhs2, rhs2, rhs2b :: String +lhs2 = let zs = 'z' : xs + xs = 'x' : ys + ys = 'y' : xs + in zs + +rhs2 = let ys = 'y' : xs + xs = 'x' : ys + zs = 'z' : xs + in zs + +rhs2b = let ys = 'y' : xs + xs = 'x' : ys + zs = 'z' : ys + in zs + +printResult :: Result -> IO () +printResult (Success s) = putStrLn s +printResult (Failure s) = putStrLn s + +isSuccess :: Result -> Bool +isSuccess (Success _) = True +isSuccess (Failure _) = False + +results :: [Result] +results = + [ $(inspectTest $ 'lhs1 ==~ 'rhs1) + , $(inspectTest $ 'lhs2 ==- 'rhs2) -- here GHC orders let bindings by itself! + , $(inspectTest $ 'lhs2 =/~ 'rhs2b) + ] + +main :: IO () +main = do + mapM_ printResult results + if map isSuccess results == [True, True, False] + then exitSuccess + else exitFailure diff --git a/examples/MutualRecursion.hs b/examples/MutualRecursion.hs --- a/examples/MutualRecursion.hs +++ b/examples/MutualRecursion.hs @@ -1,873 +1,873 @@ -{-# LANGUAGE TemplateHaskell #-} -{-# OPTIONS_GHC -fplugin Test.Inspection.Plugin #-} -module MutualRecursion where - -import System.Exit -import Test.Inspection - -inf = go0 - where - go0 = 'a' : go1 - go1 = 'b' : go2 - go2 = 'c' : go0 -inf' = go0 - where - go1 = 'b' : go2 - go0 = 'a' : go1 - go2 = 'c' : go0 -inf2' = go0 - where - go1 = 'b' : go2 - go2 = 'c' : go0 - go0 = 'a' : go1 -inf3' = go0 - where - go0 = 'a' : go1 - go1 = 'b' : go2 - go2 = 'c' : go0 - -inspect $ 'inf === 'inf' -inspect $ 'inf === 'inf2' -inspect $ 'inf === 'inf3' - --- with local variable for let* --- NOINLINE to prevent CSE -infl x = go0 - where - go0 = x : go1 - go1 = 'b' : go2 - go2 = 'c' : go0 -{-# NOINLINE infl #-} -infl' x = go0 - where - go1 = 'c' : go2 - go0 = x : go1 - go2 = 'b' : go0 -{-# NOINLINE infl' #-} - --- See https://github.com/nomeata/inspection-testing/pull/88 --- and https://github.com/nomeata/inspection-testing/issues/82 --- Change to ===, this shouldn't panic. -inspect $ 'infl =/= 'infl' - -letrec = - let go0 = 'a' : go1 - go1 = 'b' : go2 - go2 = 'c' : go0 - in go0 -letrec' = - let go1 = 'b' : go2 - go0 = 'a' : go1 - go2 = 'c' : go0 - in go0 -letrec2' = - let go1 = 'b' : go2 - go2 = 'c' : go0 - go0 = 'a' : go1 - in go0 -letrec3' = - let go0 = 'a' : go1 - go1 = 'b' : go2 - go2 = 'c' : go0 - in go0 - -inspect $ 'letrec === 'letrec' -inspect $ 'letrec === 'letrec2' -inspect $ 'letrec === 'letrec3' - -something_else = - let go0 = 'a' : go1 - go1 = 'b' : go0 - go2 = 'c' : go0 - in go0 - -inspect $ 'letrec =/= 'something_else - - - --- | Test to make sure we don't have any aggressively worst-case behavior. -bigletrec = - let go0 = '\x0' : go1 - go1 = '\x1' : go2 - go2 = '\x2' : go3 - go3 = '\x3' : go4 - go4 = '\x4' : go5 - go5 = '\x5' : go6 - go6 = '\x6' : go7 - go7 = '\x7' : go8 - go8 = '\x8' : go9 - go9 = '\x9' : go10 - go10 = '\x10' : go11 - go11 = '\x11' : go12 - go12 = '\x12' : go13 - go13 = '\x13' : go14 - go14 = '\x14' : go15 - go15 = '\x15' : go16 - go16 = '\x16' : go17 - go17 = '\x17' : go18 - go18 = '\x18' : go19 - go19 = '\x19' : go20 - go20 = '\x20' : go21 - go21 = '\x21' : go22 - go22 = '\x22' : go23 - go23 = '\x23' : go24 - go24 = '\x24' : go25 - go25 = '\x25' : go26 - go26 = '\x26' : go27 - go27 = '\x27' : go28 - go28 = '\x28' : go29 - go29 = '\x29' : go30 - go30 = '\x30' : go31 - go31 = '\x31' : go32 - go32 = '\x32' : go33 - go33 = '\x33' : go34 - go34 = '\x34' : go35 - go35 = '\x35' : go36 - go36 = '\x36' : go37 - go37 = '\x37' : go38 - go38 = '\x38' : go39 - go39 = '\x39' : go40 - go40 = '\x40' : go41 - go41 = '\x41' : go42 - go42 = '\x42' : go43 - go43 = '\x43' : go44 - go44 = '\x44' : go45 - go45 = '\x45' : go46 - go46 = '\x46' : go47 - go47 = '\x47' : go48 - go48 = '\x48' : go49 - go49 = '\x49' : go50 - go50 = '\x50' : go51 - go51 = '\x51' : go52 - go52 = '\x52' : go53 - go53 = '\x53' : go54 - go54 = '\x54' : go55 - go55 = '\x55' : go56 - go56 = '\x56' : go57 - go57 = '\x57' : go58 - go58 = '\x58' : go59 - go59 = '\x59' : go60 - go60 = '\x60' : go61 - go61 = '\x61' : go62 - go62 = '\x62' : go63 - go63 = '\x63' : go64 - go64 = '\x64' : go65 - go65 = '\x65' : go66 - go66 = '\x66' : go67 - go67 = '\x67' : go68 - go68 = '\x68' : go69 - go69 = '\x69' : go70 - go70 = '\x70' : go71 - go71 = '\x71' : go72 - go72 = '\x72' : go73 - go73 = '\x73' : go74 - go74 = '\x74' : go75 - go75 = '\x75' : go76 - go76 = '\x76' : go77 - go77 = '\x77' : go78 - go78 = '\x78' : go79 - go79 = '\x79' : go80 - go80 = '\x80' : go81 - go81 = '\x81' : go82 - go82 = '\x82' : go83 - go83 = '\x83' : go84 - go84 = '\x84' : go85 - go85 = '\x85' : go86 - go86 = '\x86' : go87 - go87 = '\x87' : go88 - go88 = '\x88' : go89 - go89 = '\x89' : go90 - go90 = '\x90' : go91 - go91 = '\x91' : go92 - go92 = '\x92' : go93 - go93 = '\x93' : go94 - go94 = '\x94' : go95 - go95 = '\x95' : go96 - go96 = '\x96' : go97 - go97 = '\x97' : go98 - go98 = '\x98' : go99 - go99 = '\x99' : go100 - go100 = '\x100' : go101 - go101 = '\x101' : go102 - go102 = '\x102' : go103 - go103 = '\x103' : go104 - go104 = '\x104' : go105 - go105 = '\x105' : go106 - go106 = '\x106' : go107 - go107 = '\x107' : go108 - go108 = '\x108' : go109 - go109 = '\x109' : go110 - go110 = '\x110' : go111 - go111 = '\x111' : go112 - go112 = '\x112' : go113 - go113 = '\x113' : go114 - go114 = '\x114' : go115 - go115 = '\x115' : go116 - go116 = '\x116' : go117 - go117 = '\x117' : go118 - go118 = '\x118' : go119 - go119 = '\x119' : go120 - go120 = '\x120' : go121 - go121 = '\x121' : go122 - go122 = '\x122' : go123 - go123 = '\x123' : go124 - go124 = '\x124' : go125 - go125 = '\x125' : go126 - go126 = '\x126' : go127 - go127 = '\x127' : go128 - go128 = '\x128' : go129 - go129 = '\x129' : go130 - go130 = '\x130' : go131 - go131 = '\x131' : go132 - go132 = '\x132' : go133 - go133 = '\x133' : go134 - go134 = '\x134' : go135 - go135 = '\x135' : go136 - go136 = '\x136' : go137 - go137 = '\x137' : go138 - go138 = '\x138' : go139 - go139 = '\x139' : go140 - go140 = '\x140' : go141 - go141 = '\x141' : go142 - go142 = '\x142' : go143 - go143 = '\x143' : go144 - go144 = '\x144' : go145 - go145 = '\x145' : go146 - go146 = '\x146' : go147 - go147 = '\x147' : go148 - go148 = '\x148' : go149 - go149 = '\x149' : go150 - go150 = '\x150' : go151 - go151 = '\x151' : go152 - go152 = '\x152' : go153 - go153 = '\x153' : go154 - go154 = '\x154' : go155 - go155 = '\x155' : go156 - go156 = '\x156' : go157 - go157 = '\x157' : go158 - go158 = '\x158' : go159 - go159 = '\x159' : go160 - go160 = '\x160' : go161 - go161 = '\x161' : go162 - go162 = '\x162' : go163 - go163 = '\x163' : go164 - go164 = '\x164' : go165 - go165 = '\x165' : go166 - go166 = '\x166' : go167 - go167 = '\x167' : go168 - go168 = '\x168' : go169 - go169 = '\x169' : go170 - go170 = '\x170' : go171 - go171 = '\x171' : go172 - go172 = '\x172' : go173 - go173 = '\x173' : go174 - go174 = '\x174' : go175 - go175 = '\x175' : go176 - go176 = '\x176' : go177 - go177 = '\x177' : go178 - go178 = '\x178' : go179 - go179 = '\x179' : go180 - go180 = '\x180' : go181 - go181 = '\x181' : go182 - go182 = '\x182' : go183 - go183 = '\x183' : go184 - go184 = '\x184' : go185 - go185 = '\x185' : go186 - go186 = '\x186' : go187 - go187 = '\x187' : go188 - go188 = '\x188' : go189 - go189 = '\x189' : go190 - go190 = '\x190' : go191 - go191 = '\x191' : go192 - go192 = '\x192' : go193 - go193 = '\x193' : go194 - go194 = '\x194' : go195 - go195 = '\x195' : go196 - go196 = '\x196' : go197 - go197 = '\x197' : go198 - go198 = '\x198' : go199 - go199 = '\x199' : go200 - go200 = '\x200' : go201 - go201 = '\x201' : go202 - go202 = '\x202' : go203 - go203 = '\x203' : go204 - go204 = '\x204' : go205 - go205 = '\x205' : go206 - go206 = '\x206' : go207 - go207 = '\x207' : go208 - go208 = '\x208' : go209 - go209 = '\x209' : go210 - go210 = '\x210' : go211 - go211 = '\x211' : go212 - go212 = '\x212' : go213 - go213 = '\x213' : go214 - go214 = '\x214' : go215 - go215 = '\x215' : go216 - go216 = '\x216' : go217 - go217 = '\x217' : go218 - go218 = '\x218' : go219 - go219 = '\x219' : go220 - go220 = '\x220' : go221 - go221 = '\x221' : go222 - go222 = '\x222' : go223 - go223 = '\x223' : go224 - go224 = '\x224' : go225 - go225 = '\x225' : go226 - go226 = '\x226' : go227 - go227 = '\x227' : go228 - go228 = '\x228' : go229 - go229 = '\x229' : go230 - go230 = '\x230' : go231 - go231 = '\x231' : go232 - go232 = '\x232' : go233 - go233 = '\x233' : go234 - go234 = '\x234' : go235 - go235 = '\x235' : go236 - go236 = '\x236' : go237 - go237 = '\x237' : go238 - go238 = '\x238' : go239 - go239 = '\x239' : go240 - go240 = '\x240' : go241 - go241 = '\x241' : go242 - go242 = '\x242' : go243 - go243 = '\x243' : go244 - go244 = '\x244' : go245 - go245 = '\x245' : go246 - go246 = '\x246' : go247 - go247 = '\x247' : go248 - go248 = '\x248' : go249 - go249 = '\x249' : go250 - go250 = '\x250' : go251 - go251 = '\x251' : go252 - go252 = '\x252' : go253 - go253 = '\x253' : go254 - go254 = '\x254' : go255 - go255 = '\x255' : go256 - go256 = '\x256' : go0 - in go0 -bigletrec' = - let go0 = '\x0' : go1 - go1 = '\x1' : go2 - go2 = '\x2' : go3 - go3 = '\x3' : go4 - go4 = '\x4' : go5 - go5 = '\x5' : go6 - go6 = '\x6' : go7 - go7 = '\x7' : go8 - go8 = '\x8' : go9 - go9 = '\x9' : go10 - go10 = '\x10' : go11 - go11 = '\x11' : go12 - go12 = '\x12' : go13 - go13 = '\x13' : go14 - go14 = '\x14' : go15 - go15 = '\x15' : go16 - go16 = '\x16' : go17 - go17 = '\x17' : go18 - go18 = '\x18' : go19 - go19 = '\x19' : go20 - go20 = '\x20' : go21 - go21 = '\x21' : go22 - go22 = '\x22' : go23 - go23 = '\x23' : go24 - go24 = '\x24' : go25 - go25 = '\x25' : go26 - go26 = '\x26' : go27 - go27 = '\x27' : go28 - go28 = '\x28' : go29 - go29 = '\x29' : go30 - go30 = '\x30' : go31 - go31 = '\x31' : go32 - go32 = '\x32' : go33 - go33 = '\x33' : go34 - go34 = '\x34' : go35 - go35 = '\x35' : go36 - go36 = '\x36' : go37 - go37 = '\x37' : go38 - go38 = '\x38' : go39 - go39 = '\x39' : go40 - go40 = '\x40' : go41 - go41 = '\x41' : go42 - go42 = '\x42' : go43 - go43 = '\x43' : go44 - go44 = '\x44' : go45 - go45 = '\x45' : go46 - go46 = '\x46' : go47 - go47 = '\x47' : go48 - go48 = '\x48' : go49 - go49 = '\x49' : go50 - go50 = '\x50' : go51 - go51 = '\x51' : go52 - go52 = '\x52' : go53 - go53 = '\x53' : go54 - go54 = '\x54' : go55 - go55 = '\x55' : go56 - go56 = '\x56' : go57 - go57 = '\x57' : go58 - go58 = '\x58' : go59 - go59 = '\x59' : go60 - go60 = '\x60' : go61 - go61 = '\x61' : go62 - go62 = '\x62' : go63 - go63 = '\x63' : go64 - go64 = '\x64' : go65 - go65 = '\x65' : go66 - go66 = '\x66' : go67 - go67 = '\x67' : go68 - go68 = '\x68' : go69 - go69 = '\x69' : go70 - go70 = '\x70' : go71 - go71 = '\x71' : go72 - go72 = '\x72' : go73 - go73 = '\x73' : go74 - go74 = '\x74' : go75 - go75 = '\x75' : go76 - go76 = '\x76' : go77 - go77 = '\x77' : go78 - go78 = '\x78' : go79 - go79 = '\x79' : go80 - go80 = '\x80' : go81 - go81 = '\x81' : go82 - go82 = '\x82' : go83 - go83 = '\x83' : go84 - go84 = '\x84' : go85 - go85 = '\x85' : go86 - go86 = '\x86' : go87 - go87 = '\x87' : go88 - go88 = '\x88' : go89 - go89 = '\x89' : go90 - go90 = '\x90' : go91 - go91 = '\x91' : go92 - go92 = '\x92' : go93 - go93 = '\x93' : go94 - go94 = '\x94' : go95 - go95 = '\x95' : go96 - go96 = '\x96' : go97 - go97 = '\x97' : go98 - go98 = '\x98' : go99 - go99 = '\x99' : go100 - go100 = '\x100' : go101 - go101 = '\x101' : go102 - go102 = '\x102' : go103 - go103 = '\x103' : go104 - go104 = '\x104' : go105 - go105 = '\x105' : go106 - go106 = '\x106' : go107 - go107 = '\x107' : go108 - go108 = '\x108' : go109 - go109 = '\x109' : go110 - go110 = '\x110' : go111 - go111 = '\x111' : go112 - go112 = '\x112' : go113 - go113 = '\x113' : go114 - go114 = '\x114' : go115 - go115 = '\x115' : go116 - go116 = '\x116' : go117 - go117 = '\x117' : go118 - go118 = '\x118' : go119 - go119 = '\x119' : go120 - go120 = '\x120' : go121 - go121 = '\x121' : go122 - go122 = '\x122' : go123 - go123 = '\x123' : go124 - go124 = '\x124' : go125 - go125 = '\x125' : go126 - go126 = '\x126' : go127 - go127 = '\x127' : go128 - go128 = '\x128' : go129 - go129 = '\x129' : go130 - go130 = '\x130' : go131 - go131 = '\x131' : go132 - go132 = '\x132' : go133 - go133 = '\x133' : go134 - go134 = '\x134' : go135 - go135 = '\x135' : go136 - go136 = '\x136' : go137 - go137 = '\x137' : go138 - go138 = '\x138' : go139 - go139 = '\x139' : go140 - go140 = '\x140' : go141 - go141 = '\x141' : go142 - go142 = '\x142' : go143 - go143 = '\x143' : go144 - go144 = '\x144' : go145 - go145 = '\x145' : go146 - go146 = '\x146' : go147 - go147 = '\x147' : go148 - go148 = '\x148' : go149 - go149 = '\x149' : go150 - go150 = '\x150' : go151 - go151 = '\x151' : go152 - go152 = '\x152' : go153 - go153 = '\x153' : go154 - go154 = '\x154' : go155 - go155 = '\x155' : go156 - go156 = '\x156' : go157 - go157 = '\x157' : go158 - go158 = '\x158' : go159 - go159 = '\x159' : go160 - go160 = '\x160' : go161 - go161 = '\x161' : go162 - go162 = '\x162' : go163 - go163 = '\x163' : go164 - go164 = '\x164' : go165 - go165 = '\x165' : go166 - go166 = '\x166' : go167 - go167 = '\x167' : go168 - go168 = '\x168' : go169 - go169 = '\x169' : go170 - go170 = '\x170' : go171 - go171 = '\x171' : go172 - go172 = '\x172' : go173 - go173 = '\x173' : go174 - go174 = '\x174' : go175 - go175 = '\x175' : go176 - go176 = '\x176' : go177 - go177 = '\x177' : go178 - go178 = '\x178' : go179 - go179 = '\x179' : go180 - go180 = '\x180' : go181 - go181 = '\x181' : go182 - go182 = '\x182' : go183 - go183 = '\x183' : go184 - go184 = '\x184' : go185 - go185 = '\x185' : go186 - go186 = '\x186' : go187 - go187 = '\x187' : go188 - go188 = '\x188' : go189 - go189 = '\x189' : go190 - go190 = '\x190' : go191 - go191 = '\x191' : go192 - go192 = '\x192' : go193 - go193 = '\x193' : go194 - go194 = '\x194' : go195 - go195 = '\x195' : go196 - go196 = '\x196' : go197 - go197 = '\x197' : go198 - go198 = '\x198' : go199 - go199 = '\x199' : go200 - go200 = '\x200' : go201 - go201 = '\x201' : go202 - go202 = '\x202' : go203 - go203 = '\x203' : go204 - go204 = '\x204' : go205 - go205 = '\x205' : go206 - go206 = '\x206' : go207 - go207 = '\x207' : go208 - go208 = '\x208' : go209 - go209 = '\x209' : go210 - go210 = '\x210' : go211 - go211 = '\x211' : go212 - go212 = '\x212' : go213 - go213 = '\x213' : go214 - go214 = '\x214' : go215 - go215 = '\x215' : go216 - go216 = '\x216' : go217 - go217 = '\x217' : go218 - go218 = '\x218' : go219 - go219 = '\x219' : go220 - go220 = '\x220' : go221 - go221 = '\x221' : go222 - go222 = '\x222' : go223 - go223 = '\x223' : go224 - go224 = '\x224' : go225 - go225 = '\x225' : go226 - go226 = '\x226' : go227 - go227 = '\x227' : go228 - go228 = '\x228' : go229 - go229 = '\x229' : go230 - go230 = '\x230' : go231 - go231 = '\x231' : go232 - go232 = '\x232' : go233 - go233 = '\x233' : go234 - go234 = '\x234' : go235 - go235 = '\x235' : go236 - go236 = '\x236' : go237 - go237 = '\x237' : go238 - go238 = '\x238' : go239 - go239 = '\x239' : go240 - go240 = '\x240' : go241 - go241 = '\x241' : go242 - go242 = '\x242' : go243 - go243 = '\x243' : go244 - go244 = '\x244' : go245 - go245 = '\x245' : go246 - go246 = '\x246' : go247 - go247 = '\x247' : go248 - go248 = '\x248' : go249 - go249 = '\x249' : go250 - go250 = '\x250' : go251 - go251 = '\x251' : go252 - go252 = '\x252' : go253 - go253 = '\x253' : go254 - go254 = '\x254' : go255 - go255 = '\x255' : go256 - go256 = '\x256' : go0 - in go0 -badletrec' = - let go0 = 'a' : go1 - go1 = '\x1' : go2 - go2 = '\x2' : go3 - go3 = '\x3' : go4 - go4 = '\x4' : go5 - go5 = '\x5' : go6 - go6 = '\x6' : go7 - go7 = '\x7' : go8 - go8 = '\x8' : go9 - go9 = '\x9' : go10 - go10 = '\x10' : go11 - go11 = '\x11' : go12 - go12 = '\x12' : go13 - go13 = '\x13' : go14 - go14 = '\x14' : go15 - go15 = '\x15' : go16 - go16 = '\x16' : go17 - go17 = '\x17' : go18 - go18 = '\x18' : go19 - go19 = '\x19' : go20 - go20 = '\x20' : go21 - go21 = '\x21' : go22 - go22 = '\x22' : go23 - go23 = '\x23' : go24 - go24 = '\x24' : go25 - go25 = '\x25' : go26 - go26 = '\x26' : go27 - go27 = '\x27' : go28 - go28 = '\x28' : go29 - go29 = '\x29' : go30 - go30 = '\x30' : go31 - go31 = '\x31' : go32 - go32 = '\x32' : go33 - go33 = '\x33' : go34 - go34 = '\x34' : go35 - go35 = '\x35' : go36 - go36 = '\x36' : go37 - go37 = '\x37' : go38 - go38 = '\x38' : go39 - go39 = '\x39' : go40 - go40 = '\x40' : go41 - go41 = '\x41' : go42 - go42 = '\x42' : go43 - go43 = '\x43' : go44 - go44 = '\x44' : go45 - go45 = '\x45' : go46 - go46 = '\x46' : go47 - go47 = '\x47' : go48 - go48 = '\x48' : go49 - go49 = '\x49' : go50 - go50 = '\x50' : go51 - go51 = '\x51' : go52 - go52 = '\x52' : go53 - go53 = '\x53' : go54 - go54 = '\x54' : go55 - go55 = '\x55' : go56 - go56 = '\x56' : go57 - go57 = '\x57' : go58 - go58 = '\x58' : go59 - go59 = '\x59' : go60 - go60 = '\x60' : go61 - go61 = '\x61' : go62 - go62 = '\x62' : go63 - go63 = '\x63' : go64 - go64 = '\x64' : go65 - go65 = '\x65' : go66 - go66 = '\x66' : go67 - go67 = '\x67' : go68 - go68 = '\x68' : go69 - go69 = '\x69' : go70 - go70 = '\x70' : go71 - go71 = '\x71' : go72 - go72 = '\x72' : go73 - go73 = '\x73' : go74 - go74 = '\x74' : go75 - go75 = '\x75' : go76 - go76 = '\x76' : go77 - go77 = '\x77' : go78 - go78 = '\x78' : go79 - go79 = '\x79' : go80 - go80 = '\x80' : go81 - go81 = '\x81' : go82 - go82 = '\x82' : go83 - go83 = '\x83' : go84 - go84 = '\x84' : go85 - go85 = '\x85' : go86 - go86 = '\x86' : go87 - go87 = '\x87' : go88 - go88 = '\x88' : go89 - go89 = '\x89' : go90 - go90 = '\x90' : go91 - go91 = '\x91' : go92 - go92 = '\x92' : go93 - go93 = '\x93' : go94 - go94 = '\x94' : go95 - go95 = '\x95' : go96 - go96 = '\x96' : go97 - go97 = '\x97' : go98 - go98 = '\x98' : go99 - go99 = '\x99' : go100 - go100 = '\x100' : go101 - go101 = '\x101' : go102 - go102 = '\x102' : go103 - go103 = '\x103' : go104 - go104 = '\x104' : go105 - go105 = '\x105' : go106 - go106 = '\x106' : go107 - go107 = '\x107' : go108 - go108 = '\x108' : go109 - go109 = '\x109' : go110 - go110 = '\x110' : go111 - go111 = '\x111' : go112 - go112 = '\x112' : go113 - go113 = '\x113' : go114 - go114 = '\x114' : go115 - go115 = '\x115' : go116 - go116 = '\x116' : go117 - go117 = '\x117' : go118 - go118 = '\x118' : go119 - go119 = '\x119' : go120 - go120 = '\x120' : go121 - go121 = '\x121' : go122 - go122 = '\x122' : go123 - go123 = '\x123' : go124 - go124 = '\x124' : go125 - go125 = '\x125' : go126 - go126 = '\x126' : go127 - go127 = '\x127' : go128 - go128 = '\x128' : go129 - go129 = '\x129' : go130 - go130 = '\x130' : go131 - go131 = '\x131' : go132 - go132 = '\x132' : go133 - go133 = '\x133' : go134 - go134 = '\x134' : go135 - go135 = '\x135' : go136 - go136 = '\x136' : go137 - go137 = '\x137' : go138 - go138 = '\x138' : go139 - go139 = '\x139' : go140 - go140 = '\x140' : go141 - go141 = '\x141' : go142 - go142 = '\x142' : go143 - go143 = '\x143' : go144 - go144 = '\x144' : go145 - go145 = '\x145' : go146 - go146 = '\x146' : go147 - go147 = '\x147' : go148 - go148 = '\x148' : go149 - go149 = '\x149' : go150 - go150 = '\x150' : go151 - go151 = '\x151' : go152 - go152 = '\x152' : go153 - go153 = '\x153' : go154 - go154 = '\x154' : go155 - go155 = '\x155' : go156 - go156 = '\x156' : go157 - go157 = '\x157' : go158 - go158 = '\x158' : go159 - go159 = '\x159' : go160 - go160 = '\x160' : go161 - go161 = '\x161' : go162 - go162 = '\x162' : go163 - go163 = '\x163' : go164 - go164 = '\x164' : go165 - go165 = '\x165' : go166 - go166 = '\x166' : go167 - go167 = '\x167' : go168 - go168 = '\x168' : go169 - go169 = '\x169' : go170 - go170 = '\x170' : go171 - go171 = '\x171' : go172 - go172 = '\x172' : go173 - go173 = '\x173' : go174 - go174 = '\x174' : go175 - go175 = '\x175' : go176 - go176 = '\x176' : go177 - go177 = '\x177' : go178 - go178 = '\x178' : go179 - go179 = '\x179' : go180 - go180 = '\x180' : go181 - go181 = '\x181' : go182 - go182 = '\x182' : go183 - go183 = '\x183' : go184 - go184 = '\x184' : go185 - go185 = '\x185' : go186 - go186 = '\x186' : go187 - go187 = '\x187' : go188 - go188 = '\x188' : go189 - go189 = '\x189' : go190 - go190 = '\x190' : go191 - go191 = '\x191' : go192 - go192 = '\x192' : go193 - go193 = '\x193' : go194 - go194 = '\x194' : go195 - go195 = '\x195' : go196 - go196 = '\x196' : go197 - go197 = '\x197' : go198 - go198 = '\x198' : go199 - go199 = '\x199' : go200 - go200 = '\x200' : go201 - go201 = '\x201' : go202 - go202 = '\x202' : go203 - go203 = '\x203' : go204 - go204 = '\x204' : go205 - go205 = '\x205' : go206 - go206 = '\x206' : go207 - go207 = '\x207' : go208 - go208 = '\x208' : go209 - go209 = '\x209' : go210 - go210 = '\x210' : go211 - go211 = '\x211' : go212 - go212 = '\x212' : go213 - go213 = '\x213' : go214 - go214 = '\x214' : go215 - go215 = '\x215' : go216 - go216 = '\x216' : go217 - go217 = '\x217' : go218 - go218 = '\x218' : go219 - go219 = '\x219' : go220 - go220 = '\x220' : go221 - go221 = '\x221' : go222 - go222 = '\x222' : go223 - go223 = '\x223' : go224 - go224 = '\x224' : go225 - go225 = '\x225' : go226 - go226 = '\x226' : go227 - go227 = '\x227' : go228 - go228 = '\x228' : go229 - go229 = '\x229' : go230 - go230 = '\x230' : go231 - go231 = '\x231' : go232 - go232 = '\x232' : go233 - go233 = '\x233' : go234 - go234 = '\x234' : go235 - go235 = '\x235' : go236 - go236 = '\x236' : go237 - go237 = '\x237' : go238 - go238 = '\x238' : go239 - go239 = '\x239' : go240 - go240 = '\x240' : go241 - go241 = '\x241' : go242 - go242 = '\x242' : go243 - go243 = '\x243' : go244 - go244 = '\x244' : go245 - go245 = '\x245' : go246 - go246 = '\x246' : go247 - go247 = '\x247' : go248 - go248 = '\x248' : go249 - go249 = '\x249' : go250 - go250 = '\x250' : go251 - go251 = '\x251' : go252 - go252 = '\x252' : go253 - go253 = '\x253' : go254 - go254 = '\x254' : go255 - go255 = '\x255' : go256 - go256 = '\x256' : go0 - in go0 - -inspect $ 'bigletrec === 'bigletrec' -inspect $ 'bigletrec =/= 'badletrec' - - -main :: IO () -main = pure () - +{-# LANGUAGE TemplateHaskell #-} +{-# OPTIONS_GHC -fplugin Test.Inspection.Plugin #-} +module MutualRecursion where + +import System.Exit +import Test.Inspection + +inf = go0 + where + go0 = 'a' : go1 + go1 = 'b' : go2 + go2 = 'c' : go0 +inf' = go0 + where + go1 = 'b' : go2 + go0 = 'a' : go1 + go2 = 'c' : go0 +inf2' = go0 + where + go1 = 'b' : go2 + go2 = 'c' : go0 + go0 = 'a' : go1 +inf3' = go0 + where + go0 = 'a' : go1 + go1 = 'b' : go2 + go2 = 'c' : go0 + +inspect $ 'inf === 'inf' +inspect $ 'inf === 'inf2' +inspect $ 'inf === 'inf3' + +-- with local variable for let* +-- NOINLINE to prevent CSE +infl x = go0 + where + go0 = x : go1 + go1 = 'b' : go2 + go2 = 'c' : go0 +{-# NOINLINE infl #-} +infl' x = go0 + where + go1 = 'c' : go2 + go0 = x : go1 + go2 = 'b' : go0 +{-# NOINLINE infl' #-} + +-- See https://github.com/nomeata/inspection-testing/pull/88 +-- and https://github.com/nomeata/inspection-testing/issues/82 +-- Change to ===, this shouldn't panic. +inspect $ 'infl =/= 'infl' + +letrec = + let go0 = 'a' : go1 + go1 = 'b' : go2 + go2 = 'c' : go0 + in go0 +letrec' = + let go1 = 'b' : go2 + go0 = 'a' : go1 + go2 = 'c' : go0 + in go0 +letrec2' = + let go1 = 'b' : go2 + go2 = 'c' : go0 + go0 = 'a' : go1 + in go0 +letrec3' = + let go0 = 'a' : go1 + go1 = 'b' : go2 + go2 = 'c' : go0 + in go0 + +inspect $ 'letrec === 'letrec' +inspect $ 'letrec === 'letrec2' +inspect $ 'letrec === 'letrec3' + +something_else = + let go0 = 'a' : go1 + go1 = 'b' : go0 + go2 = 'c' : go0 + in go0 + +inspect $ 'letrec =/= 'something_else + + + +-- | Test to make sure we don't have any aggressively worst-case behavior. +bigletrec = + let go0 = '\x0' : go1 + go1 = '\x1' : go2 + go2 = '\x2' : go3 + go3 = '\x3' : go4 + go4 = '\x4' : go5 + go5 = '\x5' : go6 + go6 = '\x6' : go7 + go7 = '\x7' : go8 + go8 = '\x8' : go9 + go9 = '\x9' : go10 + go10 = '\x10' : go11 + go11 = '\x11' : go12 + go12 = '\x12' : go13 + go13 = '\x13' : go14 + go14 = '\x14' : go15 + go15 = '\x15' : go16 + go16 = '\x16' : go17 + go17 = '\x17' : go18 + go18 = '\x18' : go19 + go19 = '\x19' : go20 + go20 = '\x20' : go21 + go21 = '\x21' : go22 + go22 = '\x22' : go23 + go23 = '\x23' : go24 + go24 = '\x24' : go25 + go25 = '\x25' : go26 + go26 = '\x26' : go27 + go27 = '\x27' : go28 + go28 = '\x28' : go29 + go29 = '\x29' : go30 + go30 = '\x30' : go31 + go31 = '\x31' : go32 + go32 = '\x32' : go33 + go33 = '\x33' : go34 + go34 = '\x34' : go35 + go35 = '\x35' : go36 + go36 = '\x36' : go37 + go37 = '\x37' : go38 + go38 = '\x38' : go39 + go39 = '\x39' : go40 + go40 = '\x40' : go41 + go41 = '\x41' : go42 + go42 = '\x42' : go43 + go43 = '\x43' : go44 + go44 = '\x44' : go45 + go45 = '\x45' : go46 + go46 = '\x46' : go47 + go47 = '\x47' : go48 + go48 = '\x48' : go49 + go49 = '\x49' : go50 + go50 = '\x50' : go51 + go51 = '\x51' : go52 + go52 = '\x52' : go53 + go53 = '\x53' : go54 + go54 = '\x54' : go55 + go55 = '\x55' : go56 + go56 = '\x56' : go57 + go57 = '\x57' : go58 + go58 = '\x58' : go59 + go59 = '\x59' : go60 + go60 = '\x60' : go61 + go61 = '\x61' : go62 + go62 = '\x62' : go63 + go63 = '\x63' : go64 + go64 = '\x64' : go65 + go65 = '\x65' : go66 + go66 = '\x66' : go67 + go67 = '\x67' : go68 + go68 = '\x68' : go69 + go69 = '\x69' : go70 + go70 = '\x70' : go71 + go71 = '\x71' : go72 + go72 = '\x72' : go73 + go73 = '\x73' : go74 + go74 = '\x74' : go75 + go75 = '\x75' : go76 + go76 = '\x76' : go77 + go77 = '\x77' : go78 + go78 = '\x78' : go79 + go79 = '\x79' : go80 + go80 = '\x80' : go81 + go81 = '\x81' : go82 + go82 = '\x82' : go83 + go83 = '\x83' : go84 + go84 = '\x84' : go85 + go85 = '\x85' : go86 + go86 = '\x86' : go87 + go87 = '\x87' : go88 + go88 = '\x88' : go89 + go89 = '\x89' : go90 + go90 = '\x90' : go91 + go91 = '\x91' : go92 + go92 = '\x92' : go93 + go93 = '\x93' : go94 + go94 = '\x94' : go95 + go95 = '\x95' : go96 + go96 = '\x96' : go97 + go97 = '\x97' : go98 + go98 = '\x98' : go99 + go99 = '\x99' : go100 + go100 = '\x100' : go101 + go101 = '\x101' : go102 + go102 = '\x102' : go103 + go103 = '\x103' : go104 + go104 = '\x104' : go105 + go105 = '\x105' : go106 + go106 = '\x106' : go107 + go107 = '\x107' : go108 + go108 = '\x108' : go109 + go109 = '\x109' : go110 + go110 = '\x110' : go111 + go111 = '\x111' : go112 + go112 = '\x112' : go113 + go113 = '\x113' : go114 + go114 = '\x114' : go115 + go115 = '\x115' : go116 + go116 = '\x116' : go117 + go117 = '\x117' : go118 + go118 = '\x118' : go119 + go119 = '\x119' : go120 + go120 = '\x120' : go121 + go121 = '\x121' : go122 + go122 = '\x122' : go123 + go123 = '\x123' : go124 + go124 = '\x124' : go125 + go125 = '\x125' : go126 + go126 = '\x126' : go127 + go127 = '\x127' : go128 + go128 = '\x128' : go129 + go129 = '\x129' : go130 + go130 = '\x130' : go131 + go131 = '\x131' : go132 + go132 = '\x132' : go133 + go133 = '\x133' : go134 + go134 = '\x134' : go135 + go135 = '\x135' : go136 + go136 = '\x136' : go137 + go137 = '\x137' : go138 + go138 = '\x138' : go139 + go139 = '\x139' : go140 + go140 = '\x140' : go141 + go141 = '\x141' : go142 + go142 = '\x142' : go143 + go143 = '\x143' : go144 + go144 = '\x144' : go145 + go145 = '\x145' : go146 + go146 = '\x146' : go147 + go147 = '\x147' : go148 + go148 = '\x148' : go149 + go149 = '\x149' : go150 + go150 = '\x150' : go151 + go151 = '\x151' : go152 + go152 = '\x152' : go153 + go153 = '\x153' : go154 + go154 = '\x154' : go155 + go155 = '\x155' : go156 + go156 = '\x156' : go157 + go157 = '\x157' : go158 + go158 = '\x158' : go159 + go159 = '\x159' : go160 + go160 = '\x160' : go161 + go161 = '\x161' : go162 + go162 = '\x162' : go163 + go163 = '\x163' : go164 + go164 = '\x164' : go165 + go165 = '\x165' : go166 + go166 = '\x166' : go167 + go167 = '\x167' : go168 + go168 = '\x168' : go169 + go169 = '\x169' : go170 + go170 = '\x170' : go171 + go171 = '\x171' : go172 + go172 = '\x172' : go173 + go173 = '\x173' : go174 + go174 = '\x174' : go175 + go175 = '\x175' : go176 + go176 = '\x176' : go177 + go177 = '\x177' : go178 + go178 = '\x178' : go179 + go179 = '\x179' : go180 + go180 = '\x180' : go181 + go181 = '\x181' : go182 + go182 = '\x182' : go183 + go183 = '\x183' : go184 + go184 = '\x184' : go185 + go185 = '\x185' : go186 + go186 = '\x186' : go187 + go187 = '\x187' : go188 + go188 = '\x188' : go189 + go189 = '\x189' : go190 + go190 = '\x190' : go191 + go191 = '\x191' : go192 + go192 = '\x192' : go193 + go193 = '\x193' : go194 + go194 = '\x194' : go195 + go195 = '\x195' : go196 + go196 = '\x196' : go197 + go197 = '\x197' : go198 + go198 = '\x198' : go199 + go199 = '\x199' : go200 + go200 = '\x200' : go201 + go201 = '\x201' : go202 + go202 = '\x202' : go203 + go203 = '\x203' : go204 + go204 = '\x204' : go205 + go205 = '\x205' : go206 + go206 = '\x206' : go207 + go207 = '\x207' : go208 + go208 = '\x208' : go209 + go209 = '\x209' : go210 + go210 = '\x210' : go211 + go211 = '\x211' : go212 + go212 = '\x212' : go213 + go213 = '\x213' : go214 + go214 = '\x214' : go215 + go215 = '\x215' : go216 + go216 = '\x216' : go217 + go217 = '\x217' : go218 + go218 = '\x218' : go219 + go219 = '\x219' : go220 + go220 = '\x220' : go221 + go221 = '\x221' : go222 + go222 = '\x222' : go223 + go223 = '\x223' : go224 + go224 = '\x224' : go225 + go225 = '\x225' : go226 + go226 = '\x226' : go227 + go227 = '\x227' : go228 + go228 = '\x228' : go229 + go229 = '\x229' : go230 + go230 = '\x230' : go231 + go231 = '\x231' : go232 + go232 = '\x232' : go233 + go233 = '\x233' : go234 + go234 = '\x234' : go235 + go235 = '\x235' : go236 + go236 = '\x236' : go237 + go237 = '\x237' : go238 + go238 = '\x238' : go239 + go239 = '\x239' : go240 + go240 = '\x240' : go241 + go241 = '\x241' : go242 + go242 = '\x242' : go243 + go243 = '\x243' : go244 + go244 = '\x244' : go245 + go245 = '\x245' : go246 + go246 = '\x246' : go247 + go247 = '\x247' : go248 + go248 = '\x248' : go249 + go249 = '\x249' : go250 + go250 = '\x250' : go251 + go251 = '\x251' : go252 + go252 = '\x252' : go253 + go253 = '\x253' : go254 + go254 = '\x254' : go255 + go255 = '\x255' : go256 + go256 = '\x256' : go0 + in go0 +bigletrec' = + let go0 = '\x0' : go1 + go1 = '\x1' : go2 + go2 = '\x2' : go3 + go3 = '\x3' : go4 + go4 = '\x4' : go5 + go5 = '\x5' : go6 + go6 = '\x6' : go7 + go7 = '\x7' : go8 + go8 = '\x8' : go9 + go9 = '\x9' : go10 + go10 = '\x10' : go11 + go11 = '\x11' : go12 + go12 = '\x12' : go13 + go13 = '\x13' : go14 + go14 = '\x14' : go15 + go15 = '\x15' : go16 + go16 = '\x16' : go17 + go17 = '\x17' : go18 + go18 = '\x18' : go19 + go19 = '\x19' : go20 + go20 = '\x20' : go21 + go21 = '\x21' : go22 + go22 = '\x22' : go23 + go23 = '\x23' : go24 + go24 = '\x24' : go25 + go25 = '\x25' : go26 + go26 = '\x26' : go27 + go27 = '\x27' : go28 + go28 = '\x28' : go29 + go29 = '\x29' : go30 + go30 = '\x30' : go31 + go31 = '\x31' : go32 + go32 = '\x32' : go33 + go33 = '\x33' : go34 + go34 = '\x34' : go35 + go35 = '\x35' : go36 + go36 = '\x36' : go37 + go37 = '\x37' : go38 + go38 = '\x38' : go39 + go39 = '\x39' : go40 + go40 = '\x40' : go41 + go41 = '\x41' : go42 + go42 = '\x42' : go43 + go43 = '\x43' : go44 + go44 = '\x44' : go45 + go45 = '\x45' : go46 + go46 = '\x46' : go47 + go47 = '\x47' : go48 + go48 = '\x48' : go49 + go49 = '\x49' : go50 + go50 = '\x50' : go51 + go51 = '\x51' : go52 + go52 = '\x52' : go53 + go53 = '\x53' : go54 + go54 = '\x54' : go55 + go55 = '\x55' : go56 + go56 = '\x56' : go57 + go57 = '\x57' : go58 + go58 = '\x58' : go59 + go59 = '\x59' : go60 + go60 = '\x60' : go61 + go61 = '\x61' : go62 + go62 = '\x62' : go63 + go63 = '\x63' : go64 + go64 = '\x64' : go65 + go65 = '\x65' : go66 + go66 = '\x66' : go67 + go67 = '\x67' : go68 + go68 = '\x68' : go69 + go69 = '\x69' : go70 + go70 = '\x70' : go71 + go71 = '\x71' : go72 + go72 = '\x72' : go73 + go73 = '\x73' : go74 + go74 = '\x74' : go75 + go75 = '\x75' : go76 + go76 = '\x76' : go77 + go77 = '\x77' : go78 + go78 = '\x78' : go79 + go79 = '\x79' : go80 + go80 = '\x80' : go81 + go81 = '\x81' : go82 + go82 = '\x82' : go83 + go83 = '\x83' : go84 + go84 = '\x84' : go85 + go85 = '\x85' : go86 + go86 = '\x86' : go87 + go87 = '\x87' : go88 + go88 = '\x88' : go89 + go89 = '\x89' : go90 + go90 = '\x90' : go91 + go91 = '\x91' : go92 + go92 = '\x92' : go93 + go93 = '\x93' : go94 + go94 = '\x94' : go95 + go95 = '\x95' : go96 + go96 = '\x96' : go97 + go97 = '\x97' : go98 + go98 = '\x98' : go99 + go99 = '\x99' : go100 + go100 = '\x100' : go101 + go101 = '\x101' : go102 + go102 = '\x102' : go103 + go103 = '\x103' : go104 + go104 = '\x104' : go105 + go105 = '\x105' : go106 + go106 = '\x106' : go107 + go107 = '\x107' : go108 + go108 = '\x108' : go109 + go109 = '\x109' : go110 + go110 = '\x110' : go111 + go111 = '\x111' : go112 + go112 = '\x112' : go113 + go113 = '\x113' : go114 + go114 = '\x114' : go115 + go115 = '\x115' : go116 + go116 = '\x116' : go117 + go117 = '\x117' : go118 + go118 = '\x118' : go119 + go119 = '\x119' : go120 + go120 = '\x120' : go121 + go121 = '\x121' : go122 + go122 = '\x122' : go123 + go123 = '\x123' : go124 + go124 = '\x124' : go125 + go125 = '\x125' : go126 + go126 = '\x126' : go127 + go127 = '\x127' : go128 + go128 = '\x128' : go129 + go129 = '\x129' : go130 + go130 = '\x130' : go131 + go131 = '\x131' : go132 + go132 = '\x132' : go133 + go133 = '\x133' : go134 + go134 = '\x134' : go135 + go135 = '\x135' : go136 + go136 = '\x136' : go137 + go137 = '\x137' : go138 + go138 = '\x138' : go139 + go139 = '\x139' : go140 + go140 = '\x140' : go141 + go141 = '\x141' : go142 + go142 = '\x142' : go143 + go143 = '\x143' : go144 + go144 = '\x144' : go145 + go145 = '\x145' : go146 + go146 = '\x146' : go147 + go147 = '\x147' : go148 + go148 = '\x148' : go149 + go149 = '\x149' : go150 + go150 = '\x150' : go151 + go151 = '\x151' : go152 + go152 = '\x152' : go153 + go153 = '\x153' : go154 + go154 = '\x154' : go155 + go155 = '\x155' : go156 + go156 = '\x156' : go157 + go157 = '\x157' : go158 + go158 = '\x158' : go159 + go159 = '\x159' : go160 + go160 = '\x160' : go161 + go161 = '\x161' : go162 + go162 = '\x162' : go163 + go163 = '\x163' : go164 + go164 = '\x164' : go165 + go165 = '\x165' : go166 + go166 = '\x166' : go167 + go167 = '\x167' : go168 + go168 = '\x168' : go169 + go169 = '\x169' : go170 + go170 = '\x170' : go171 + go171 = '\x171' : go172 + go172 = '\x172' : go173 + go173 = '\x173' : go174 + go174 = '\x174' : go175 + go175 = '\x175' : go176 + go176 = '\x176' : go177 + go177 = '\x177' : go178 + go178 = '\x178' : go179 + go179 = '\x179' : go180 + go180 = '\x180' : go181 + go181 = '\x181' : go182 + go182 = '\x182' : go183 + go183 = '\x183' : go184 + go184 = '\x184' : go185 + go185 = '\x185' : go186 + go186 = '\x186' : go187 + go187 = '\x187' : go188 + go188 = '\x188' : go189 + go189 = '\x189' : go190 + go190 = '\x190' : go191 + go191 = '\x191' : go192 + go192 = '\x192' : go193 + go193 = '\x193' : go194 + go194 = '\x194' : go195 + go195 = '\x195' : go196 + go196 = '\x196' : go197 + go197 = '\x197' : go198 + go198 = '\x198' : go199 + go199 = '\x199' : go200 + go200 = '\x200' : go201 + go201 = '\x201' : go202 + go202 = '\x202' : go203 + go203 = '\x203' : go204 + go204 = '\x204' : go205 + go205 = '\x205' : go206 + go206 = '\x206' : go207 + go207 = '\x207' : go208 + go208 = '\x208' : go209 + go209 = '\x209' : go210 + go210 = '\x210' : go211 + go211 = '\x211' : go212 + go212 = '\x212' : go213 + go213 = '\x213' : go214 + go214 = '\x214' : go215 + go215 = '\x215' : go216 + go216 = '\x216' : go217 + go217 = '\x217' : go218 + go218 = '\x218' : go219 + go219 = '\x219' : go220 + go220 = '\x220' : go221 + go221 = '\x221' : go222 + go222 = '\x222' : go223 + go223 = '\x223' : go224 + go224 = '\x224' : go225 + go225 = '\x225' : go226 + go226 = '\x226' : go227 + go227 = '\x227' : go228 + go228 = '\x228' : go229 + go229 = '\x229' : go230 + go230 = '\x230' : go231 + go231 = '\x231' : go232 + go232 = '\x232' : go233 + go233 = '\x233' : go234 + go234 = '\x234' : go235 + go235 = '\x235' : go236 + go236 = '\x236' : go237 + go237 = '\x237' : go238 + go238 = '\x238' : go239 + go239 = '\x239' : go240 + go240 = '\x240' : go241 + go241 = '\x241' : go242 + go242 = '\x242' : go243 + go243 = '\x243' : go244 + go244 = '\x244' : go245 + go245 = '\x245' : go246 + go246 = '\x246' : go247 + go247 = '\x247' : go248 + go248 = '\x248' : go249 + go249 = '\x249' : go250 + go250 = '\x250' : go251 + go251 = '\x251' : go252 + go252 = '\x252' : go253 + go253 = '\x253' : go254 + go254 = '\x254' : go255 + go255 = '\x255' : go256 + go256 = '\x256' : go0 + in go0 +badletrec' = + let go0 = 'a' : go1 + go1 = '\x1' : go2 + go2 = '\x2' : go3 + go3 = '\x3' : go4 + go4 = '\x4' : go5 + go5 = '\x5' : go6 + go6 = '\x6' : go7 + go7 = '\x7' : go8 + go8 = '\x8' : go9 + go9 = '\x9' : go10 + go10 = '\x10' : go11 + go11 = '\x11' : go12 + go12 = '\x12' : go13 + go13 = '\x13' : go14 + go14 = '\x14' : go15 + go15 = '\x15' : go16 + go16 = '\x16' : go17 + go17 = '\x17' : go18 + go18 = '\x18' : go19 + go19 = '\x19' : go20 + go20 = '\x20' : go21 + go21 = '\x21' : go22 + go22 = '\x22' : go23 + go23 = '\x23' : go24 + go24 = '\x24' : go25 + go25 = '\x25' : go26 + go26 = '\x26' : go27 + go27 = '\x27' : go28 + go28 = '\x28' : go29 + go29 = '\x29' : go30 + go30 = '\x30' : go31 + go31 = '\x31' : go32 + go32 = '\x32' : go33 + go33 = '\x33' : go34 + go34 = '\x34' : go35 + go35 = '\x35' : go36 + go36 = '\x36' : go37 + go37 = '\x37' : go38 + go38 = '\x38' : go39 + go39 = '\x39' : go40 + go40 = '\x40' : go41 + go41 = '\x41' : go42 + go42 = '\x42' : go43 + go43 = '\x43' : go44 + go44 = '\x44' : go45 + go45 = '\x45' : go46 + go46 = '\x46' : go47 + go47 = '\x47' : go48 + go48 = '\x48' : go49 + go49 = '\x49' : go50 + go50 = '\x50' : go51 + go51 = '\x51' : go52 + go52 = '\x52' : go53 + go53 = '\x53' : go54 + go54 = '\x54' : go55 + go55 = '\x55' : go56 + go56 = '\x56' : go57 + go57 = '\x57' : go58 + go58 = '\x58' : go59 + go59 = '\x59' : go60 + go60 = '\x60' : go61 + go61 = '\x61' : go62 + go62 = '\x62' : go63 + go63 = '\x63' : go64 + go64 = '\x64' : go65 + go65 = '\x65' : go66 + go66 = '\x66' : go67 + go67 = '\x67' : go68 + go68 = '\x68' : go69 + go69 = '\x69' : go70 + go70 = '\x70' : go71 + go71 = '\x71' : go72 + go72 = '\x72' : go73 + go73 = '\x73' : go74 + go74 = '\x74' : go75 + go75 = '\x75' : go76 + go76 = '\x76' : go77 + go77 = '\x77' : go78 + go78 = '\x78' : go79 + go79 = '\x79' : go80 + go80 = '\x80' : go81 + go81 = '\x81' : go82 + go82 = '\x82' : go83 + go83 = '\x83' : go84 + go84 = '\x84' : go85 + go85 = '\x85' : go86 + go86 = '\x86' : go87 + go87 = '\x87' : go88 + go88 = '\x88' : go89 + go89 = '\x89' : go90 + go90 = '\x90' : go91 + go91 = '\x91' : go92 + go92 = '\x92' : go93 + go93 = '\x93' : go94 + go94 = '\x94' : go95 + go95 = '\x95' : go96 + go96 = '\x96' : go97 + go97 = '\x97' : go98 + go98 = '\x98' : go99 + go99 = '\x99' : go100 + go100 = '\x100' : go101 + go101 = '\x101' : go102 + go102 = '\x102' : go103 + go103 = '\x103' : go104 + go104 = '\x104' : go105 + go105 = '\x105' : go106 + go106 = '\x106' : go107 + go107 = '\x107' : go108 + go108 = '\x108' : go109 + go109 = '\x109' : go110 + go110 = '\x110' : go111 + go111 = '\x111' : go112 + go112 = '\x112' : go113 + go113 = '\x113' : go114 + go114 = '\x114' : go115 + go115 = '\x115' : go116 + go116 = '\x116' : go117 + go117 = '\x117' : go118 + go118 = '\x118' : go119 + go119 = '\x119' : go120 + go120 = '\x120' : go121 + go121 = '\x121' : go122 + go122 = '\x122' : go123 + go123 = '\x123' : go124 + go124 = '\x124' : go125 + go125 = '\x125' : go126 + go126 = '\x126' : go127 + go127 = '\x127' : go128 + go128 = '\x128' : go129 + go129 = '\x129' : go130 + go130 = '\x130' : go131 + go131 = '\x131' : go132 + go132 = '\x132' : go133 + go133 = '\x133' : go134 + go134 = '\x134' : go135 + go135 = '\x135' : go136 + go136 = '\x136' : go137 + go137 = '\x137' : go138 + go138 = '\x138' : go139 + go139 = '\x139' : go140 + go140 = '\x140' : go141 + go141 = '\x141' : go142 + go142 = '\x142' : go143 + go143 = '\x143' : go144 + go144 = '\x144' : go145 + go145 = '\x145' : go146 + go146 = '\x146' : go147 + go147 = '\x147' : go148 + go148 = '\x148' : go149 + go149 = '\x149' : go150 + go150 = '\x150' : go151 + go151 = '\x151' : go152 + go152 = '\x152' : go153 + go153 = '\x153' : go154 + go154 = '\x154' : go155 + go155 = '\x155' : go156 + go156 = '\x156' : go157 + go157 = '\x157' : go158 + go158 = '\x158' : go159 + go159 = '\x159' : go160 + go160 = '\x160' : go161 + go161 = '\x161' : go162 + go162 = '\x162' : go163 + go163 = '\x163' : go164 + go164 = '\x164' : go165 + go165 = '\x165' : go166 + go166 = '\x166' : go167 + go167 = '\x167' : go168 + go168 = '\x168' : go169 + go169 = '\x169' : go170 + go170 = '\x170' : go171 + go171 = '\x171' : go172 + go172 = '\x172' : go173 + go173 = '\x173' : go174 + go174 = '\x174' : go175 + go175 = '\x175' : go176 + go176 = '\x176' : go177 + go177 = '\x177' : go178 + go178 = '\x178' : go179 + go179 = '\x179' : go180 + go180 = '\x180' : go181 + go181 = '\x181' : go182 + go182 = '\x182' : go183 + go183 = '\x183' : go184 + go184 = '\x184' : go185 + go185 = '\x185' : go186 + go186 = '\x186' : go187 + go187 = '\x187' : go188 + go188 = '\x188' : go189 + go189 = '\x189' : go190 + go190 = '\x190' : go191 + go191 = '\x191' : go192 + go192 = '\x192' : go193 + go193 = '\x193' : go194 + go194 = '\x194' : go195 + go195 = '\x195' : go196 + go196 = '\x196' : go197 + go197 = '\x197' : go198 + go198 = '\x198' : go199 + go199 = '\x199' : go200 + go200 = '\x200' : go201 + go201 = '\x201' : go202 + go202 = '\x202' : go203 + go203 = '\x203' : go204 + go204 = '\x204' : go205 + go205 = '\x205' : go206 + go206 = '\x206' : go207 + go207 = '\x207' : go208 + go208 = '\x208' : go209 + go209 = '\x209' : go210 + go210 = '\x210' : go211 + go211 = '\x211' : go212 + go212 = '\x212' : go213 + go213 = '\x213' : go214 + go214 = '\x214' : go215 + go215 = '\x215' : go216 + go216 = '\x216' : go217 + go217 = '\x217' : go218 + go218 = '\x218' : go219 + go219 = '\x219' : go220 + go220 = '\x220' : go221 + go221 = '\x221' : go222 + go222 = '\x222' : go223 + go223 = '\x223' : go224 + go224 = '\x224' : go225 + go225 = '\x225' : go226 + go226 = '\x226' : go227 + go227 = '\x227' : go228 + go228 = '\x228' : go229 + go229 = '\x229' : go230 + go230 = '\x230' : go231 + go231 = '\x231' : go232 + go232 = '\x232' : go233 + go233 = '\x233' : go234 + go234 = '\x234' : go235 + go235 = '\x235' : go236 + go236 = '\x236' : go237 + go237 = '\x237' : go238 + go238 = '\x238' : go239 + go239 = '\x239' : go240 + go240 = '\x240' : go241 + go241 = '\x241' : go242 + go242 = '\x242' : go243 + go243 = '\x243' : go244 + go244 = '\x244' : go245 + go245 = '\x245' : go246 + go246 = '\x246' : go247 + go247 = '\x247' : go248 + go248 = '\x248' : go249 + go249 = '\x249' : go250 + go250 = '\x250' : go251 + go251 = '\x251' : go252 + go252 = '\x252' : go253 + go253 = '\x253' : go254 + go254 = '\x254' : go255 + go255 = '\x255' : go256 + go256 = '\x256' : go0 + in go0 + +inspect $ 'bigletrec === 'bigletrec' +inspect $ 'bigletrec =/= 'badletrec' + + +main :: IO () +main = pure () + diff --git a/examples/NS_NP.hs b/examples/NS_NP.hs --- a/examples/NS_NP.hs +++ b/examples/NS_NP.hs @@ -1,44 +1,44 @@ -{-# LANGUAGE GADTs, TypeFamilies, DataKinds, PolyKinds, TypeOperators #-} -{-# LANGUAGE TemplateHaskell #-} -{-# OPTIONS_GHC -O -fplugin-opt=Test.Inspection.Plugin:quiet -Wno-overlapping-patterns #-} -module NS_NP (main) where - -import Data.Kind -import Test.Inspection - -data NS (f :: k -> Type) (xs :: [k]) where - Z :: f x -> NS f (x : xs) - S :: !(NS f xs) -> NS f (x : xs) - -data NP (f :: k -> Type) (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 +{-# LANGUAGE GADTs, TypeFamilies, DataKinds, PolyKinds, TypeOperators #-} +{-# LANGUAGE TemplateHaskell #-} +{-# OPTIONS_GHC -O -fplugin-opt=Test.Inspection.Plugin:quiet -Wno-overlapping-patterns #-} +module NS_NP where + +import Data.Kind +import Test.Inspection + +data NS (f :: k -> Type) (xs :: [k]) where + Z :: f x -> NS f (x : xs) + S :: !(NS f xs) -> NS f (x : xs) + +data NP (f :: k -> Type) (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/Regression.hs b/examples/Regression.hs --- a/examples/Regression.hs +++ b/examples/Regression.hs @@ -1,17 +1,18 @@ -{-# LANGUAGE TemplateHaskell #-} - --- This is a kitchen sink test file for various regressions --- reported via GitHub - -import Test.Inspection - - --- https://github.com/nomeata/inspection-testing/issues/35 -empty1, empty2 :: [a] -empty1 = map id [] -empty2 = [] - -inspect $ 'empty1 === 'empty2 - -main :: IO () -main = return () +{-# LANGUAGE TemplateHaskell #-} +module Main where + +-- This is a kitchen sink test file for various regressions +-- reported via GitHub + +import Test.Inspection + + +-- https://github.com/nomeata/inspection-testing/issues/35 +empty1, empty2 :: [a] +empty1 = map id [] +empty2 = [] + +inspect $ 'empty1 === 'empty2 + +main :: IO () +main = return () diff --git a/examples/Simple.hs b/examples/Simple.hs --- a/examples/Simple.hs +++ b/examples/Simple.hs @@ -1,16 +1,16 @@ -{-# LANGUAGE TemplateHaskell #-} -module Simple (main) 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 () +{-# LANGUAGE TemplateHaskell #-} +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/SimpleTest.hs b/examples/SimpleTest.hs --- a/examples/SimpleTest.hs +++ b/examples/SimpleTest.hs @@ -1,36 +1,39 @@ -{-# LANGUAGE TemplateHaskell #-} -module Main (main) where - -import Test.Inspection -import Data.Maybe -import System.Exit - -lhs, rhs, something_else :: (a -> b) -> Maybe a -> Bool - -lhs f x = isNothing (fmap f x) - -rhs _ Nothing = True -rhs _ (Just _) = False - -something_else _ _ = False - -printResult :: Result -> IO () -printResult (Success s) = putStrLn s -printResult (Failure s) = putStrLn s - -isSuccess :: Result -> Bool -isSuccess (Success _) = True -isSuccess (Failure _) = False - -results :: [Result] -results = - [ $(inspectTest $ 'lhs === 'rhs) - , $(inspectTest $ 'lhs === 'something_else) - ] - -main :: IO () -main = do - mapM_ printResult results - if map isSuccess results == [True, False] - then exitSuccess - else exitFailure +{-# LANGUAGE TemplateHaskell #-} +module Main (main) where + +import Test.Inspection +import Data.Maybe +import System.Exit + +lhs, rhs, something_else :: (a -> b) -> Maybe a -> Bool + +lhs f x = isNothing (fmap f x) + +rhs _ Nothing = True +rhs _ (Just _) = False + +something_else _ _ = False + +printResult :: Result -> IO () +printResult (Success s) = putStrLn s +printResult (Failure s) = putStrLn s + +isSuccess :: Result -> Bool +isSuccess (Success _) = True +isSuccess (Failure _) = False + +results :: [Result] +results = + [ $(inspectTest $ 'lhs === 'rhs) + , $(inspectTest $ 'lhs === 'something_else) + ] + +main :: IO () +main = do + mapM_ printResult results + if map isSuccess results == [True, False] + then exitSuccess + else exitFailure + +_unused :: () +_unused = const () [ 'lhs, 'rhs, 'something_else ] diff --git a/examples/Text.hs b/examples/Text.hs --- a/examples/Text.hs +++ b/examples/Text.hs @@ -1,27 +1,27 @@ -{-# LANGUAGE TemplateHaskell #-} -module Text (main) 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 () +{-# LANGUAGE TemplateHaskell #-} +module Text (main) 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/examples/UnsafeCoerce.hs b/examples/UnsafeCoerce.hs --- a/examples/UnsafeCoerce.hs +++ b/examples/UnsafeCoerce.hs @@ -1,18 +1,18 @@ -{-# LANGUAGE TemplateHaskell #-} -module UnsafeCoerce (main) where - -import Test.Inspection -import Unsafe.Coerce -import GHC.Exts - -lhs :: Any -> Any -lhs a = unsafeCoerce $ unsafeCoerce a + (1 :: Int) - -rhs :: Int -> Int -rhs = (+ 1) - -inspect $ 'lhs =/= 'rhs -inspect $ 'lhs ==- 'rhs - -main :: IO () -main = return () +{-# LANGUAGE TemplateHaskell #-} +module UnsafeCoerce where + +import Test.Inspection +import Unsafe.Coerce +import GHC.Exts + +lhs :: Any -> Any +lhs a = unsafeCoerce $ unsafeCoerce a + (1 :: Int) + +rhs :: Int -> Int +rhs = (+ 1) + +inspect $ 'lhs =/= 'rhs +inspect $ 'lhs ==- 'rhs + +main :: IO () +main = return () diff --git a/examples/WorkerWrapper.hs b/examples/WorkerWrapper.hs --- a/examples/WorkerWrapper.hs +++ b/examples/WorkerWrapper.hs @@ -1,35 +1,35 @@ -{-# LANGUAGE TemplateHaskell #-} -module WorkerWrapper (main) where - -import Test.Inspection - --- In this module, we are interested in checking if the worker-wrapper transformation is firing. --- That transformation is described here: --- https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/demand#worker-wrapper-split --- In short, we don't want to be passing around the dictionary type below, but rather have GHC --- generate a helper function @$wdictFold :: (m -> m -> m) -> m -> [m] -> m@, as this saves us some --- wrapping and unwrapping work at each iteration. --- --- GHC still generates a wrapper at the @dictFold@ name. That is, a function that still consumes the --- @MonoidDict@ type, but unwraps it just once, before passing it off to @wdictFold@ to handle the --- recuresion. As @dictFold@ refers to this wrapper, we cannot check that the @MonoidDict@ type is --- unused in its definition. --- --- So what are we to do? As the generated wrapper should have an @INLINE@ pragma, once we pass it in --- the @MonoidDict@, we should be safely in worker-land, and not need to reference @MonoidDict@ --- again. Thus, we look at @appliedFold@, and assert that @MonoidDict@ never shows up -- as would be --- expected if worker-wrapper fired as hoped. -data MonoidDict a = MonoidDict { dictMappend :: a -> a -> a, dictMempty :: a } - -dictFold :: MonoidDict m -> [m] -> m -dictFold bm xs = case xs of - [] -> dictMempty bm - x:xs' -> dictMappend bm x $ dictFold bm xs' - -appliedFold :: [Int] -> Int -appliedFold = dictFold $ MonoidDict (+) 0 - -inspect $ 'appliedFold `doesNotUse` 'MonoidDict - -main :: IO () -main = return () +{-# LANGUAGE TemplateHaskell #-} +module WorkerWrapper where + +import Test.Inspection + +-- In this module, we are interested in checking if the worker-wrapper transformation is firing. +-- That transformation is described here: +-- https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/demand#worker-wrapper-split +-- In short, we don't want to be passing around the dictionary type below, but rather have GHC +-- generate a helper function @$wdictFold :: (m -> m -> m) -> m -> [m] -> m@, as this saves us some +-- wrapping and unwrapping work at each iteration. +-- +-- GHC still generates a wrapper at the @dictFold@ name. That is, a function that still consumes the +-- @MonoidDict@ type, but unwraps it just once, before passing it off to @wdictFold@ to handle the +-- recuresion. As @dictFold@ refers to this wrapper, we cannot check that the @MonoidDict@ type is +-- unused in its definition. +-- +-- So what are we to do? As the generated wrapper should have an @INLINE@ pragma, once we pass it in +-- the @MonoidDict@, we should be safely in worker-land, and not need to reference @MonoidDict@ +-- again. Thus, we look at @appliedFold@, and assert that @MonoidDict@ never shows up -- as would be +-- expected if worker-wrapper fired as hoped. +data MonoidDict a = MonoidDict { dictMappend :: a -> a -> a, dictMempty :: a } + +dictFold :: MonoidDict m -> [m] -> m +dictFold bm xs = case xs of + [] -> dictMempty bm + x:xs' -> dictMappend bm x $ dictFold bm xs' + +appliedFold :: [Int] -> Int +appliedFold = dictFold $ MonoidDict (+) 0 + +inspect $ 'appliedFold `doesNotUse` 'MonoidDict + +main :: IO () +main = return () diff --git a/inspection-testing.cabal b/inspection-testing.cabal --- a/inspection-testing.cabal +++ b/inspection-testing.cabal @@ -1,244 +1,243 @@ -name: inspection-testing -version: 0.6.2 -synopsis: GHC plugin to do inspection testing -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.4.*, GHC ==8.6.*, GHC ==8.8.*, GHC ==8.10.*, GHC ==9.0.*, GHC ==9.2.*, GHC ==9.4.*, GHC ==9.6.*, GHC ==9.8.*, GHC ==9.10.* - -source-repository head - type: git - location: git://github.com/nomeata/inspection-testing.git - -library - exposed-modules: Test.Inspection - Test.Inspection.Plugin - Test.Inspection.Core - hs-source-dirs: src - build-depends: base >=4.9 && <4.22 - build-depends: ghc >= 8.0.2 && <9.13 - build-depends: template-haskell - build-depends: containers - build-depends: transformers - build-depends: mtl - 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 - default-language: Haskell2010 - ghc-options: -main-is NS_NP - if impl(ghc < 8.4) - ghc-options: -fplugin=Test.Inspection.Plugin - -test-suite HPCs - type: exitcode-stdio-1.0 - hs-source-dirs: examples - main-is: HPCs.hs - build-depends: inspection-testing - build-depends: base - default-language: Haskell2010 - ghc-options: -main-is HPCs - if impl(ghc < 8.4) - ghc-options: -fplugin=Test.Inspection.Plugin - -test-suite simple - type: exitcode-stdio-1.0 - hs-source-dirs: examples - main-is: Simple.hs - build-depends: inspection-testing - build-depends: base - default-language: Haskell2010 - ghc-options: -main-is Simple - if impl(ghc < 8.4) - ghc-options: -fplugin=Test.Inspection.Plugin - -test-suite simple-test - type: exitcode-stdio-1.0 - hs-source-dirs: examples - main-is: SimpleTest.hs - build-depends: inspection-testing - build-depends: base - default-language: Haskell2010 - if impl(ghc < 8.4) - ghc-options: -fplugin=Test.Inspection.Plugin - -test-suite lets-test - type: exitcode-stdio-1.0 - hs-source-dirs: examples - main-is: LetsTest.hs - build-depends: inspection-testing - build-depends: base - default-language: Haskell2010 - if impl(ghc < 8.4) - ghc-options: -fplugin=Test.Inspection.Plugin - -test-suite doesnotuse - type: exitcode-stdio-1.0 - hs-source-dirs: examples - main-is: DoesNotUse.hs - build-depends: inspection-testing - build-depends: base - default-language: Haskell2010 - ghc-options: -main-is DoesNotUse - if impl(ghc < 8.4) - ghc-options: -fplugin=Test.Inspection.Plugin - -test-suite fusion - type: exitcode-stdio-1.0 - hs-source-dirs: examples - main-is: Fusion.hs - build-depends: inspection-testing - build-depends: base - default-language: Haskell2010 - ghc-options: -main-is Fusion - if impl(ghc < 8.4) - ghc-options: -fplugin=Test.Inspection.Plugin - -test-suite generics - type: exitcode-stdio-1.0 - hs-source-dirs: examples - main-is: Generics.hs - build-depends: inspection-testing - build-depends: base - default-language: Haskell2010 - ghc-options: -main-is Generics - if impl(ghc < 8.4) - ghc-options: -fplugin=Test.Inspection.Plugin - -test-suite dictionary - type: exitcode-stdio-1.0 - hs-source-dirs: examples - main-is: Dictionary.hs - build-depends: inspection-testing - build-depends: base - default-language: Haskell2010 - ghc-options: -main-is Dictionary - if impl(ghc < 8.4) - ghc-options: -fplugin=Test.Inspection.Plugin - -test-suite mutual-recursion - type: exitcode-stdio-1.0 - hs-source-dirs: examples - main-is: MutualRecursion.hs - build-depends: inspection-testing - build-depends: base - default-language: Haskell2010 - ghc-options: -main-is MutualRecursion - -test-suite regression - type: exitcode-stdio-1.0 - hs-source-dirs: examples - main-is: Regression.hs - build-depends: inspection-testing - build-depends: base - default-language: Haskell2010 - if impl(ghc < 8.4) - ghc-options: -fplugin=Test.Inspection.Plugin - -test-suite worker-wrapper - type: exitcode-stdio-1.0 - hs-source-dirs: examples - main-is: WorkerWrapper.hs - build-depends: inspection-testing - build-depends: base - default-language: Haskell2010 - ghc-options: -main-is WorkerWrapper - if impl(ghc < 8.4) - ghc-options: -fplugin=Test.Inspection.Plugin - -test-suite unsafe-coerce - type: exitcode-stdio-1.0 - hs-source-dirs: examples - main-is: UnsafeCoerce.hs - build-depends: inspection-testing - build-depends: base - default-language: Haskell2010 - ghc-options: -main-is UnsafeCoerce - if impl(ghc < 8.4) - ghc-options: -fplugin=Test.Inspection.Plugin - -flag more-tests - description: Run tests that pull in specific versions of other packages - default: False - -test-suite generic-lens - type: exitcode-stdio-1.0 - hs-source-dirs: examples - main-is: GenericLens.hs - if flag(more-tests) - build-depends: inspection-testing - build-depends: base - build-depends: generic-lens ==2.1.0.0 - else - buildable: False - default-language: Haskell2010 - ghc-options: -main-is GenericLens - if impl(ghc < 8.4) - ghc-options: -fplugin=Test.Inspection.Plugin - - -flag old-text-tests - description: Run tests that exhibits bug in old text package. Only works with older version of GHC. - default: False - -test-suite text - type: exitcode-stdio-1.0 - hs-source-dirs: examples - main-is: Text.hs - if flag(old-text-tests) - build-depends: inspection-testing - build-depends: base - build-depends: text ==1.2.2.2 - build-depends: bytestring - else - buildable: False - default-language: Haskell2010 - ghc-options: -main-is Text - if impl(ghc < 8.4) - ghc-options: -fplugin=Test.Inspection.Plugin - -test-suite dwarf - type: exitcode-stdio-1.0 - hs-source-dirs: examples - main-is: DWARF.hs - build-depends: inspection-testing - build-depends: base - default-language: Haskell2010 - ghc-options: -main-is DWARF - if impl(ghc < 8.4) - ghc-options: -fplugin=Test.Inspection.Plugin +name: inspection-testing +version: 0.6.3 +synopsis: GHC plugin to do inspection testing +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.4.*, GHC ==8.6.*, GHC ==8.8.*, GHC ==8.10.*, GHC ==9.0.*, GHC ==9.2.*, GHC ==9.4.*, GHC ==9.6.*, GHC ==9.8.*, GHC ==9.10.*, GHC==9.12.*, GHC==9.14.* + +source-repository head + type: git + location: https://github.com/nomeata/inspection-testing + +library + exposed-modules: Test.Inspection + Test.Inspection.Plugin + Test.Inspection.Core + hs-source-dirs: src + build-depends: base >=4.9 && <4.23 + build-depends: ghc >= 8.0.2 && <9.15 + build-depends: template-haskell + build-depends: containers + build-depends: transformers + 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 + default-language: Haskell2010 + ghc-options: -main-is NS_NP + if impl(ghc < 8.4) + ghc-options: -fplugin=Test.Inspection.Plugin + +test-suite HPCs + type: exitcode-stdio-1.0 + hs-source-dirs: examples + main-is: HPCs.hs + build-depends: inspection-testing + build-depends: base + default-language: Haskell2010 + ghc-options: -main-is HPCs + if impl(ghc < 8.4) + ghc-options: -fplugin=Test.Inspection.Plugin + +test-suite simple + type: exitcode-stdio-1.0 + hs-source-dirs: examples + main-is: Simple.hs + build-depends: inspection-testing + build-depends: base + default-language: Haskell2010 + ghc-options: -main-is Simple + if impl(ghc < 8.4) + ghc-options: -fplugin=Test.Inspection.Plugin + +test-suite simple-test + type: exitcode-stdio-1.0 + hs-source-dirs: examples + main-is: SimpleTest.hs + build-depends: inspection-testing + build-depends: base + default-language: Haskell2010 + if impl(ghc < 8.4) + ghc-options: -fplugin=Test.Inspection.Plugin + +test-suite lets-test + type: exitcode-stdio-1.0 + hs-source-dirs: examples + main-is: LetsTest.hs + build-depends: inspection-testing + build-depends: base + default-language: Haskell2010 + if impl(ghc < 8.4) + ghc-options: -fplugin=Test.Inspection.Plugin + +test-suite doesnotuse + type: exitcode-stdio-1.0 + hs-source-dirs: examples + main-is: DoesNotUse.hs + build-depends: inspection-testing + build-depends: base + default-language: Haskell2010 + ghc-options: -main-is DoesNotUse + if impl(ghc < 8.4) + ghc-options: -fplugin=Test.Inspection.Plugin + +test-suite fusion + type: exitcode-stdio-1.0 + hs-source-dirs: examples + main-is: Fusion.hs + build-depends: inspection-testing + build-depends: base + default-language: Haskell2010 + ghc-options: -main-is Fusion + if impl(ghc < 8.4) + ghc-options: -fplugin=Test.Inspection.Plugin + +test-suite generics + type: exitcode-stdio-1.0 + hs-source-dirs: examples + main-is: Generics.hs + build-depends: inspection-testing + build-depends: base + default-language: Haskell2010 + ghc-options: -main-is Generics + if impl(ghc < 8.4) + ghc-options: -fplugin=Test.Inspection.Plugin + +test-suite dictionary + type: exitcode-stdio-1.0 + hs-source-dirs: examples + main-is: Dictionary.hs + build-depends: inspection-testing + build-depends: base + default-language: Haskell2010 + ghc-options: -main-is Dictionary + if impl(ghc < 8.4) + ghc-options: -fplugin=Test.Inspection.Plugin + +test-suite mutual-recursion + type: exitcode-stdio-1.0 + hs-source-dirs: examples + main-is: MutualRecursion.hs + build-depends: inspection-testing + build-depends: base + default-language: Haskell2010 + ghc-options: -main-is MutualRecursion + +test-suite regression + type: exitcode-stdio-1.0 + hs-source-dirs: examples + main-is: Regression.hs + build-depends: inspection-testing + build-depends: base + default-language: Haskell2010 + if impl(ghc < 8.4) + ghc-options: -fplugin=Test.Inspection.Plugin + +test-suite worker-wrapper + type: exitcode-stdio-1.0 + hs-source-dirs: examples + main-is: WorkerWrapper.hs + build-depends: inspection-testing + build-depends: base + default-language: Haskell2010 + ghc-options: -main-is WorkerWrapper + if impl(ghc < 8.4) + ghc-options: -fplugin=Test.Inspection.Plugin + +test-suite unsafe-coerce + type: exitcode-stdio-1.0 + hs-source-dirs: examples + main-is: UnsafeCoerce.hs + build-depends: inspection-testing + build-depends: base + default-language: Haskell2010 + ghc-options: -main-is UnsafeCoerce + if impl(ghc < 8.4) + ghc-options: -fplugin=Test.Inspection.Plugin + +flag more-tests + description: Run tests that pull in specific versions of other packages + default: False + +test-suite generic-lens + type: exitcode-stdio-1.0 + hs-source-dirs: examples + main-is: GenericLens.hs + if flag(more-tests) + build-depends: inspection-testing + build-depends: base + build-depends: generic-lens ==2.1.0.0 + else + buildable: False + default-language: Haskell2010 + ghc-options: -main-is GenericLens + if impl(ghc < 8.4) + ghc-options: -fplugin=Test.Inspection.Plugin + + +flag old-text-tests + description: Run tests that exhibits bug in old text package. Only works with older version of GHC. + default: False + +test-suite text + type: exitcode-stdio-1.0 + hs-source-dirs: examples + main-is: Text.hs + if flag(old-text-tests) + build-depends: inspection-testing + build-depends: base + build-depends: text ==1.2.2.2 + build-depends: bytestring + else + buildable: False + default-language: Haskell2010 + ghc-options: -main-is Text + if impl(ghc < 8.4) + ghc-options: -fplugin=Test.Inspection.Plugin + +test-suite dwarf + type: exitcode-stdio-1.0 + hs-source-dirs: examples + main-is: DWARF.hs + build-depends: inspection-testing + build-depends: base + default-language: Haskell2010 + ghc-options: -main-is DWARF + if impl(ghc < 8.4) + ghc-options: -fplugin=Test.Inspection.Plugin diff --git a/src/Test/Inspection.hs b/src/Test/Inspection.hs --- a/src/Test/Inspection.hs +++ b/src/Test/Inspection.hs @@ -1,355 +1,355 @@ --- | --- 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 inspection testing. - -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE CPP #-} -module Test.Inspection ( - -- * Synopsis - -- $synopsis - - -- * Registering obligations - inspect, - inspectTest, - Result(..), - -- * Defining obligations - Obligation(..), mkObligation, Equivalence (..), Property(..), - -- * Convenience functions - -- $convenience - (===), (==-), (=/=), (=/-), (==~), (=/~), - hasNoType, hasNoGenerics, - hasNoTypeClasses, hasNoTypeClassesExcept, - doesNotUse, coreOf, -) where - -import Language.Haskell.TH -import Language.Haskell.TH.Syntax (Quasi(qNewName), liftData, addTopDecls) -#if MIN_VERSION_GLASGOW_HASKELL(8,4,0,0) -import Language.Haskell.TH.Syntax (addCorePlugin) -#endif -import Data.Data -import Data.Maybe -import GHC.Exts (lazy) -import GHC.Generics (V1(), U1(), M1(), K1(), (:+:), (:*:), (:.:), Rec1, Par1) - -{- $synopsis - -To use inspection testing, you need to - - 1. enable the @TemplateHaskell@ language extension - 2. declare your proof obligations using 'inspect' or 'inspectTest' - -An example module is - -@ -{-\# LANGUAGE TemplateHaskell \#-} -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 -@ - -On GHC < 8.4, you have to explicitly load the plugin: -@ -{-\# OPTIONS_GHC -fplugin=Test.Inspection.Plugin \#-} -@ --} - --- 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 --- mnemonic convenience functions like '(===)' or 'hasNoType'. --- --- The obligation needs to be passed to 'inspect' or 'inspectTest'. --- --- @since 0.1 -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 - -- @{-\# LANGUAGE 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? - -- (Only used by 'inspect', not by 'inspectTest') - , srcLoc :: Maybe Loc - -- ^ The source location where this obligation is defined. - -- This is filled in by 'inspect'. - , storeResult :: Maybe String - -- ^ If this is 'Nothing', then report errors during compilation. - -- Otherwise, update the top-level definition with this name. - -- - -- @since 0.2 - } - deriving Data - --- | Properties of the obligation target to be checked. --- --- @since 0.1 -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@. - -- - -- In general @f@ and @g@ need to be defined in this module, so that their - -- actual defintions can be inspected. - -- - -- The `Equivalence` indicates how strict to check for equality - = EqualTo Name Equivalence - - -- | Do none of these types appear anywhere in the definition of the function - -- (neither locally bound nor passed as arguments) - -- - -- @since 0.3 - | NoTypes [Name] - - -- | Does this function perform no heap allocations. - | NoAllocation - - -- | Does this value contain dictionaries (/except/ of the listed classes). - -- - -- @since 0.3 - | NoTypeClasses [Name] - - -- | Does not contain this value (in terms or patterns) - -- - -- @since 0.4.1 - | NoUseOf [Name] - - -- | Always satisfied, but dumps the value in non-quiet mode. - -- - -- @since 0.4.2 - | CoreOf - deriving Data - --- | Equivalence of terms. --- --- @since 0.5 -data Equivalence - = StrictEquiv -- ^ strict term equality - | IgnoreTypesAndTicksEquiv -- ^ ignore types and hpc ticks during the comparison - | UnorderedLetsEquiv -- ^ allow permuted let bindings, ignore types and hpc tick during comparison - deriving Data - --- | Creates an inspection obligation for the given function name --- with default values for the optional fields. --- --- @since 0.1 -mkObligation :: Name -> Property -> Obligation -mkObligation target prop = Obligation - { target = target - , property = prop - , testName = Nothing - , srcLoc = Nothing - , expectFail = False - , storeResult = Nothing - } - -{- $convenience - -These convenience functions create common test obligations directly. --} - --- | Declare two functions to be equal (see 'EqualTo') --- --- @since 0.1 -(===) :: Name -> Name -> Obligation -(===) = mkEquality False StrictEquiv -infix 9 === - --- | Declare two functions to be equal, but ignoring --- type lambdas, type arguments, type casts and hpc ticks (see 'EqualTo'). --- Note that @-fhpc@ can prevent some optimizations; build without for more reliable analysis. --- --- @since 0.1.1 -(==-) :: Name -> Name -> Obligation -(==-) = mkEquality False IgnoreTypesAndTicksEquiv -infix 9 ==- - --- | Declare two functions to be equal as @('==-')@ but also ignoring --- let bindings ordering (see 'EqualTo'). --- --- @since 0.5 -(==~) :: Name -> Name -> Obligation -(==~) = mkEquality False UnorderedLetsEquiv -infix 9 ==~ - --- | Declare two functions to be equal, but expect the test to fail (see 'EqualTo' and 'expectFail') --- (This is useful for documentation purposes, or as a TODO list.) --- --- @since 0.1 -(=/=) :: Name -> Name -> Obligation -(=/=) = mkEquality True StrictEquiv -infix 9 =/= - --- | Declare two functions to be equal up to types (see '(==-)'), --- but expect the test to fail (see 'expectFail'). --- --- @since 0.4.3.0 -(=/-) :: Name -> Name -> Obligation -(=/-) = mkEquality True IgnoreTypesAndTicksEquiv -infix 9 =/- - --- | Declare two functions to be equal up to let binding ordering (see '(==~)'), --- but expect the test to fail (see 'expectFail'). --- --- @since 0.5 -(=/~) :: Name -> Name -> Obligation -(=/~) = mkEquality True UnorderedLetsEquiv -infix 9 =/~ - -mkEquality :: Bool -> Equivalence -> Name -> Name -> Obligation -mkEquality expectFail ignore_types n1 n2 = - (mkObligation n1 (EqualTo n2 ignore_types)) - { expectFail = expectFail } - --- | Declare that in a function’s implementation, the given type does not occur. --- --- More precisely: No locally bound variable (let-bound, lambda-bound or --- pattern-bound) has a type that contains the given type constructor. --- --- @'inspect' $ fusedFunction ``hasNoType`` ''[]@ --- --- @since 0.1 -hasNoType :: Name -> Name -> Obligation -hasNoType n tn = mkObligation n (NoTypes [tn]) - --- | Declare that a function’s implementation does not contain any generic types. --- This is just 'hasNoType' applied to the usual type constructors used in --- "GHC.Generics". --- --- @inspect $ hasNoGenerics genericFunction@ --- --- @since 0.3 -hasNoGenerics :: Name -> Obligation -hasNoGenerics n = - mkObligation n - (NoTypes [ ''V1, ''U1, ''M1, ''K1, ''(:+:), ''(:*:), ''(:.:), ''Rec1 - , ''Par1 - ]) - --- | Declare that a function's implementation does not include dictionaries. --- --- More precisely: No locally bound variable (let-bound, lambda-bound or --- pattern-bound) has a type that contains a type that mentions a type class. --- --- @'inspect' $ 'hasNoTypeClasses' specializedFunction@ --- --- @since 0.3 -hasNoTypeClasses :: Name -> Obligation -hasNoTypeClasses n = hasNoTypeClassesExcept n [] - --- | A variant of 'hasNoTypeClasses', which white-lists some type-classes. --- --- @'inspect' $ fieldLens ``hasNoTypeClassesExcept`` [''Functor]@ --- --- @since 0.3 -hasNoTypeClassesExcept :: Name -> [Name] -> Obligation -hasNoTypeClassesExcept n tns = mkObligation n (NoTypeClasses tns) - --- | Declare that a function's implementation does not use the given --- variable (either in terms or -- if it is a constructor -- in patterns). --- --- @'inspect' $ foo ``doesNotUse`` 'error@ --- --- @since 0.4.1 -doesNotUse :: Name -> Name -> Obligation -doesNotUse n ns = mkObligation n (NoUseOf [ns]) - --- | Dump the Core of the value. --- --- @'inspect' $ 'coreOf' 'foo@ --- --- This is useful when you need to inspect some values manually. --- --- @since 0.4.2 -coreOf :: Name -> Obligation -coreOf n = mkObligation n CoreOf - --- The exported TH functions - -inspectCommon :: AnnTarget -> Obligation -> Q [Dec] -inspectCommon annTarget obl = do -#if MIN_VERSION_GLASGOW_HASKELL(8,4,0,0) - addCorePlugin "Test.Inspection.Plugin" -#endif - loc <- location - annExpr <- liftData (obl { srcLoc = Just $ fromMaybe loc $ srcLoc obl }) - pure [PragmaD (AnnP annTarget annExpr)] - --- | As seen in the example above, the entry point to inspection testing is the --- 'inspect' function, to which you pass an 'Obligation'. --- It will report test failures at compile time. --- --- @since 0.1 -inspect :: Obligation -> Q [Dec] -inspect = inspectCommon ModuleAnnotation - --- | The result of 'inspectTest', which has a more or less helpful text message --- --- @since 0.2 -data Result = Failure String | Success String - deriving Show - -didNotRunPluginError :: Result -didNotRunPluginError = lazy (error "Test.Inspection.Plugin did not run") -{-# NOINLINE didNotRunPluginError #-} - --- | This is a variant of 'inspect' that allows compilation to succeed in any case, --- and instead indicates the result as a value of type 'Result', --- which allows seamless integration into test frameworks. --- --- This variant ignores the 'expectFail' field of the obligation. Instead, --- it is expected that you use the corresponding functionality in your test --- framework (e.g. [@tasty-expected-failure@](https://hackage.haskell.org/package/tasty-expected-failure)) --- --- @since 0.2 -inspectTest :: Obligation -> Q Exp -inspectTest obl = do - nameS <- genName - name <- newUniqueName nameS - anns <- inspectCommon (ValueAnnotation name) obl - addTopDecls $ - [ SigD name (ConT ''Result) - , ValD (VarP name) (NormalB (VarE 'didNotRunPluginError)) [] - , PragmaD (InlineP name NoInline FunLike AllPhases) - ] ++ anns - return $ VarE name - where - genName = do - (r,c) <- loc_start <$> location - return $ "inspect_" ++ show r ++ "_" ++ show c - --- | Like newName, but even more unique (unique across different splices), --- and with unique @nameBase@s. Precondition: the string is a valid Haskell --- alphanumeric identifier (could be upper- or lower-case). -newUniqueName :: Quasi q => String -> q Name -newUniqueName str = do - n <- qNewName str - qNewName $ show n --- This is from https://ghc.haskell.org/trac/ghc/ticket/13054#comment:1 +-- | +-- 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 inspection testing. + +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE CPP #-} +module Test.Inspection ( + -- * Synopsis + -- $synopsis + + -- * Registering obligations + inspect, + inspectTest, + Result(..), + -- * Defining obligations + Obligation(..), mkObligation, Equivalence (..), Property(..), + -- * Convenience functions + -- $convenience + (===), (==-), (=/=), (=/-), (==~), (=/~), + hasNoType, hasNoGenerics, + hasNoTypeClasses, hasNoTypeClassesExcept, + doesNotUse, coreOf, +) where + +import Language.Haskell.TH +import Language.Haskell.TH.Syntax (Quasi(qNewName), liftData, addTopDecls) +#if MIN_VERSION_GLASGOW_HASKELL(8,4,0,0) +import Language.Haskell.TH.Syntax (addCorePlugin) +#endif +import Data.Data +import Data.Maybe +import GHC.Exts (lazy) +import GHC.Generics (V1(), U1(), M1(), K1(), (:+:), (:*:), (:.:), Rec1, Par1) + +{- $synopsis + +To use inspection testing, you need to + + 1. enable the @TemplateHaskell@ language extension + 2. declare your proof obligations using 'inspect' or 'inspectTest' + +An example module is + +@ +{-\# LANGUAGE TemplateHaskell \#-} +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 +@ + +On GHC < 8.4, you have to explicitly load the plugin: +@ +{-\# OPTIONS_GHC -fplugin=Test.Inspection.Plugin \#-} +@ +-} + +-- 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 +-- mnemonic convenience functions like '(===)' or 'hasNoType'. +-- +-- The obligation needs to be passed to 'inspect' or 'inspectTest'. +-- +-- @since 0.1 +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 + -- @{-\# LANGUAGE 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? + -- (Only used by 'inspect', not by 'inspectTest') + , srcLoc :: Maybe Loc + -- ^ The source location where this obligation is defined. + -- This is filled in by 'inspect'. + , storeResult :: Maybe String + -- ^ If this is 'Nothing', then report errors during compilation. + -- Otherwise, update the top-level definition with this name. + -- + -- @since 0.2 + } + deriving Data + +-- | Properties of the obligation target to be checked. +-- +-- @since 0.1 +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@. + -- + -- In general @f@ and @g@ need to be defined in this module, so that their + -- actual defintions can be inspected. + -- + -- The `Equivalence` indicates how strict to check for equality + = EqualTo Name Equivalence + + -- | Do none of these types appear anywhere in the definition of the function + -- (neither locally bound nor passed as arguments) + -- + -- @since 0.3 + | NoTypes [Name] + + -- | Does this function perform no heap allocations. + | NoAllocation + + -- | Does this value contain dictionaries (/except/ of the listed classes). + -- + -- @since 0.3 + | NoTypeClasses [Name] + + -- | Does not contain this value (in terms or patterns) + -- + -- @since 0.4.1 + | NoUseOf [Name] + + -- | Always satisfied, but dumps the value in non-quiet mode. + -- + -- @since 0.4.2 + | CoreOf + deriving Data + +-- | Equivalence of terms. +-- +-- @since 0.5 +data Equivalence + = StrictEquiv -- ^ strict term equality + | IgnoreTypesAndTicksEquiv -- ^ ignore types and hpc ticks during the comparison + | UnorderedLetsEquiv -- ^ allow permuted let bindings, ignore types and hpc tick during comparison + deriving Data + +-- | Creates an inspection obligation for the given function name +-- with default values for the optional fields. +-- +-- @since 0.1 +mkObligation :: Name -> Property -> Obligation +mkObligation target prop = Obligation + { target = target + , property = prop + , testName = Nothing + , srcLoc = Nothing + , expectFail = False + , storeResult = Nothing + } + +{- $convenience + +These convenience functions create common test obligations directly. +-} + +-- | Declare two functions to be equal (see 'EqualTo') +-- +-- @since 0.1 +(===) :: Name -> Name -> Obligation +(===) = mkEquality False StrictEquiv +infix 9 === + +-- | Declare two functions to be equal, but ignoring +-- type lambdas, type arguments, type casts and hpc ticks (see 'EqualTo'). +-- Note that @-fhpc@ can prevent some optimizations; build without for more reliable analysis. +-- +-- @since 0.1.1 +(==-) :: Name -> Name -> Obligation +(==-) = mkEquality False IgnoreTypesAndTicksEquiv +infix 9 ==- + +-- | Declare two functions to be equal as @('==-')@ but also ignoring +-- let bindings ordering (see 'EqualTo'). +-- +-- @since 0.5 +(==~) :: Name -> Name -> Obligation +(==~) = mkEquality False UnorderedLetsEquiv +infix 9 ==~ + +-- | Declare two functions to be equal, but expect the test to fail (see 'EqualTo' and 'expectFail') +-- (This is useful for documentation purposes, or as a TODO list.) +-- +-- @since 0.1 +(=/=) :: Name -> Name -> Obligation +(=/=) = mkEquality True StrictEquiv +infix 9 =/= + +-- | Declare two functions to be equal up to types (see '(==-)'), +-- but expect the test to fail (see 'expectFail'). +-- +-- @since 0.4.3.0 +(=/-) :: Name -> Name -> Obligation +(=/-) = mkEquality True IgnoreTypesAndTicksEquiv +infix 9 =/- + +-- | Declare two functions to be equal up to let binding ordering (see '(==~)'), +-- but expect the test to fail (see 'expectFail'). +-- +-- @since 0.5 +(=/~) :: Name -> Name -> Obligation +(=/~) = mkEquality True UnorderedLetsEquiv +infix 9 =/~ + +mkEquality :: Bool -> Equivalence -> Name -> Name -> Obligation +mkEquality expectFail ignore_types n1 n2 = + (mkObligation n1 (EqualTo n2 ignore_types)) + { expectFail = expectFail } + +-- | Declare that in a function’s implementation, the given type does not occur. +-- +-- More precisely: No locally bound variable (let-bound, lambda-bound or +-- pattern-bound) has a type that contains the given type constructor. +-- +-- @'inspect' $ fusedFunction ``hasNoType`` ''[]@ +-- +-- @since 0.1 +hasNoType :: Name -> Name -> Obligation +hasNoType n tn = mkObligation n (NoTypes [tn]) + +-- | Declare that a function’s implementation does not contain any generic types. +-- This is just 'hasNoType' applied to the usual type constructors used in +-- "GHC.Generics". +-- +-- @inspect $ hasNoGenerics genericFunction@ +-- +-- @since 0.3 +hasNoGenerics :: Name -> Obligation +hasNoGenerics n = + mkObligation n + (NoTypes [ ''V1, ''U1, ''M1, ''K1, ''(:+:), ''(:*:), ''(:.:), ''Rec1 + , ''Par1 + ]) + +-- | Declare that a function's implementation does not include dictionaries. +-- +-- More precisely: No locally bound variable (let-bound, lambda-bound or +-- pattern-bound) has a type that contains a type that mentions a type class. +-- +-- @'inspect' $ 'hasNoTypeClasses' specializedFunction@ +-- +-- @since 0.3 +hasNoTypeClasses :: Name -> Obligation +hasNoTypeClasses n = hasNoTypeClassesExcept n [] + +-- | A variant of 'hasNoTypeClasses', which white-lists some type-classes. +-- +-- @'inspect' $ fieldLens ``hasNoTypeClassesExcept`` [''Functor]@ +-- +-- @since 0.3 +hasNoTypeClassesExcept :: Name -> [Name] -> Obligation +hasNoTypeClassesExcept n tns = mkObligation n (NoTypeClasses tns) + +-- | Declare that a function's implementation does not use the given +-- variable (either in terms or -- if it is a constructor -- in patterns). +-- +-- @'inspect' $ foo ``doesNotUse`` 'error@ +-- +-- @since 0.4.1 +doesNotUse :: Name -> Name -> Obligation +doesNotUse n ns = mkObligation n (NoUseOf [ns]) + +-- | Dump the Core of the value. +-- +-- @'inspect' $ 'coreOf' 'foo@ +-- +-- This is useful when you need to inspect some values manually. +-- +-- @since 0.4.2 +coreOf :: Name -> Obligation +coreOf n = mkObligation n CoreOf + +-- The exported TH functions + +inspectCommon :: AnnTarget -> Obligation -> Q [Dec] +inspectCommon annTarget obl = do +#if MIN_VERSION_GLASGOW_HASKELL(8,4,0,0) + addCorePlugin "Test.Inspection.Plugin" +#endif + loc <- location + annExpr <- liftData (obl { srcLoc = Just $ fromMaybe loc $ srcLoc obl }) + pure [PragmaD (AnnP annTarget annExpr)] + +-- | As seen in the example above, the entry point to inspection testing is the +-- 'inspect' function, to which you pass an 'Obligation'. +-- It will report test failures at compile time. +-- +-- @since 0.1 +inspect :: Obligation -> Q [Dec] +inspect = inspectCommon ModuleAnnotation + +-- | The result of 'inspectTest', which has a more or less helpful text message +-- +-- @since 0.2 +data Result = Failure String | Success String + deriving Show + +didNotRunPluginError :: Result +didNotRunPluginError = lazy (error "Test.Inspection.Plugin did not run") +{-# NOINLINE didNotRunPluginError #-} + +-- | This is a variant of 'inspect' that allows compilation to succeed in any case, +-- and instead indicates the result as a value of type 'Result', +-- which allows seamless integration into test frameworks. +-- +-- This variant ignores the 'expectFail' field of the obligation. Instead, +-- it is expected that you use the corresponding functionality in your test +-- framework (e.g. [@tasty-expected-failure@](https://hackage.haskell.org/package/tasty-expected-failure)) +-- +-- @since 0.2 +inspectTest :: Obligation -> Q Exp +inspectTest obl = do + nameS <- genName + name <- newUniqueName nameS + anns <- inspectCommon (ValueAnnotation name) obl + addTopDecls $ + [ SigD name (ConT ''Result) + , ValD (VarP name) (NormalB (VarE 'didNotRunPluginError)) [] + , PragmaD (InlineP name NoInline FunLike AllPhases) + ] ++ anns + return $ VarE name + where + genName = do + (r,c) <- loc_start <$> location + return $ "inspect_" ++ show r ++ "_" ++ show c + +-- | Like newName, but even more unique (unique across different splices), +-- and with unique @nameBase@s. Precondition: the string is a valid Haskell +-- alphanumeric identifier (could be upper- or lower-case). +newUniqueName :: Quasi q => String -> q Name +newUniqueName str = do + n <- qNewName str + qNewName $ show n +-- This is from https://ghc.haskell.org/trac/ghc/ticket/13054#comment:1 diff --git a/src/Test/Inspection/Core.hs b/src/Test/Inspection/Core.hs --- a/src/Test/Inspection/Core.hs +++ b/src/Test/Inspection/Core.hs @@ -1,612 +1,612 @@ --- | This module implements some analyses of Core expressions necessary for --- "Test.Inspection". Normally, users of this package can ignore this module. -{-# LANGUAGE CPP, FlexibleContexts, PatternSynonyms, MultiWayIf, ViewPatterns #-} -module Test.Inspection.Core - ( slice - , pprSlice - , pprSliceDifference - , eqSlice - , eqSlice' - , freeOfType - , freeOfTerm - , doesNotAllocate - , doesNotContainTypeClasses - ) where - -#if MIN_VERSION_ghc(9,0,0) -import GHC.Builtin.Types (isCTupleTyConName) -import GHC.Core -import GHC.Core.Utils -import GHC.Core.TyCo.Rep -import GHC.Core.Type -import GHC.Types.Var as Var -import GHC.Types.Var.Set (mkVarSet) -import GHC.Types.Id -import GHC.Types.Name -import GHC.Types.Literal -import GHC.Types.Var.Env -import GHC.Types.Unique -import GHC.Utils.Outputable as Outputable -import GHC.Core.Ppr -import GHC.Core.Subst -import GHC.Core.Coercion -import GHC.Utils.Misc -import GHC.Core.DataCon -import GHC.Core.TyCon (TyCon, isClassTyCon) -#else -import TysWiredIn (isCTupleTyConName) -import CoreSyn -import CoreUtils -import CoreSubst -import TyCoRep -import Type -import Var -import VarSet (mkVarSet) -import Id -import Literal -import Name -import VarEnv -import Outputable -import PprCore -import Coercion -import Util -import DataCon -import Unique -import TyCon (TyCon, isClassTyCon) -#endif - -#if MIN_VERSION_ghc(9,2,0) -import GHC.Types.Tickish -#endif - -#if MIN_VERSION_ghc(9,6,0) -import GHC.Core.TyCo.Compare (eqTypeX) -#endif - -import qualified Data.Set as S -import Control.Monad (unless) -import Control.Monad.State.Strict (execState, modify', gets) -import Data.List (nub, intercalate) -import Data.Maybe (listToMaybe, fromJust) -import Data.Either (isRight) - -import Test.Inspection (Equivalence (..)) - --- Uncomment to enable debug traces --- #define DEBUG_TRACE - -#ifdef DEBUG_TRACE -import Debug.Trace - -tracePut :: Monad m => Int -> String -> String -> m () -tracePut lv name msg = traceM $ replicate lv ' ' ++ name ++ ": " ++ msg -#else -tracePut :: Monad m => Int -> String -> String -> m () -tracePut _ _ _ = return () -#endif - -#if !MIN_VERSION_ghc(9,2,0) -pattern Alt :: a -> b -> c -> (a, b, c) -pattern Alt a b c = (a, b, c) -{-# COMPLETE Alt #-} -#endif - - -type Slice = [(Var, CoreExpr)] - --- | Selects those bindings that define the given variable (with this variable first) -slice :: [(Var, CoreExpr)] -> Var -> Slice -slice binds v - | Just e <- lookup v binds - = (v,e) : [(v',e) | (v',e) <- binds, v' /= v, v' `S.member` used ] - | otherwise - = error "slice: cannot find given variable in bindings" - 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 e = fromJust $ lookup v binds - go e - | otherwise = return () - - go (Var v) = goV v - go (Lit _ ) = pure () - go (App e arg) | isTyCoArg arg = go e - go (App e arg) = go e >> go arg - 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 (Alt _ _ e) = go e - --- | Pretty-print a slice -pprSlice :: Slice -> SDoc -pprSlice slice = - withLessDetail $ pprCoreBindings [ NonRec v e | (v,e) <- slice ] - --- | Pretty-print two slices, after removing variables occurring in both -pprSliceDifference :: Slice -> Slice -> SDoc -pprSliceDifference slice1 slice2 - | [(v1,e1)] <- slice1' - , [(v2,e2)] <- slice2' - = pprSingletonSliceDifference (mkInScopeSet (mkVarSet (S.toList both))) v1 v2 e1 e2 - - | otherwise = - hang (text "LHS" Outputable.<> colon) 4 (pprSlice slice1') $$ - hang (text "RHS" Outputable.<> colon) 4 (pprSlice slice2') - where - both = S.intersection (S.fromList (map fst slice1)) (S.fromList (map fst slice2)) - slice1' = filter (\(v,_) -> v `S.notMember` both) slice1 - slice2' = filter (\(v,_) -> v `S.notMember` both) slice2 - -pprSingletonSliceDifference :: InScopeSet -> Var -> Var -> CoreExpr -> CoreExpr -> SDoc -pprSingletonSliceDifference iss v1 v2 e1 e2 = - ctxDoc $ - hang (text "LHS" Outputable.<> colon) 4 (hang (pprPrefixOcc v1) 2 (eqSign <+> pprCoreExpr e1')) $$ - hang (text "RHS" Outputable.<> colon) 4 (hang (pprPrefixOcc v2) 2 (eqSign <+> pprCoreExpr e2')) - where - hasContext = not (null ctxt) - - ctxDoc | hasContext = id - | otherwise = (hang (text "In") 4 (ppr $ mkContextExpr (reverse (map snd ctxt))) $$) - - eqSign | hasContext = text "= ..." - | otherwise = equals - - (e1', e2', ctxt) = go e1 e2 [] (mkRnEnv2 emptyInScopeSet) - - go :: CoreExpr -> CoreExpr -> [(Var, Var)] -> RnEnv2 -> (CoreExpr, CoreExpr, [(Var, Var)]) - go (Lam b1 t1) (Lam b2 t2) ctxt env - | eqTypeX env (varType b1) (varType b2) - = go t1 t2 ((b1,b2):ctxt) (rnBndr2 env b1 b2) - where - go x y ctxt _env = (rename iss ctxt x, y, ctxt) - - mkContextExpr :: [Var] -> CoreExpr - mkContextExpr [] = ellipsis - mkContextExpr (x:rest) = Lam x (mkContextExpr rest) - - ellipsis :: CoreExpr -#if MIN_VERSION_ghc(8,8,0) - ellipsis = Lit $ mkLitString "..." -#else - ellipsis = Lit $ mkMachString "..." -#endif - -withLessDetail :: SDoc -> SDoc -#if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0) && !MIN_VERSION_GLASGOW_HASKELL(9,0,0,0) -withLessDetail sdoc = sdocWithDynFlags $ \dflags -> - withPprStyle (defaultUserStyle dflags) sdoc -#else -withLessDetail sdoc = withPprStyle defaultUserStyle sdoc -#endif - --- | Equality name environment. --- This environment contains top-level and let-bound definitions --- (no lambda arguments). -data EqEnv = EqEnv !Int [(Var, (Int, CoreExpr))] [(Var, (Int, CoreExpr))] - --- | Lookup left and right variables in EqEnv. -lookupEqEnv :: Var -> Var -> EqEnv -> Maybe (Int, Int, CoreExpr, CoreExpr) -lookupEqEnv x y (EqEnv _ env1 env2) - | Just (i, e1) <- lookup x env1 - , Just (j, e2) <- lookup y env2 - = Just (i, j, e1, e2) - - | otherwise - = Nothing - -initialEqEnv :: [(Var, CoreExpr)] -> [(Var, CoreExpr)] -> EqEnv -initialEqEnv ls rs = EqEnv 1 - [ (x, (0, e1)) | (x, e1) <- ls ] - [ (y, (0, e2)) | (y, e2) <- rs ] - -bindEqEnv :: [(Var, CoreExpr)] -> [(Var, CoreExpr)] -> EqEnv -> EqEnv -bindEqEnv ls rs (EqEnv i env1 env2)= EqEnv (i + 1) - ([ (x, (i, e1)) | (x, e1) <- ls ] ++ env1) - ([ (y, (i, e2)) | (y, e2) <- rs ] ++ env2) - --- | This is a heuristic, which only works if both slices --- have auxiliary 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 :: Equivalence -> Slice -> Slice -> Bool -eqSlice eqv l r = isRight (eqSlice' eqv l r) - --- | Like 'eqSlice' but also returns an explanation of inequality. -eqSlice' :: Equivalence -> Slice -> Slice -> Either SDoc () -eqSlice' _ [] [] = Right () -eqSlice' _ ((v,_) : _) [] = Left $ ppr v -eqSlice' _ [] ((v,_) : _) = Left $ ppr v - -- Mostly defensive programming (slices should not be empty) -eqSlice' eqv slice1@((head1, def1) : _) slice2@((head2, def2) : _) = do - goStart head1 def1 head2 def2 - where - -- ignore types and hpc ticks - it :: Bool - it = case eqv of - StrictEquiv -> False - IgnoreTypesAndTicksEquiv -> True - UnorderedLetsEquiv -> True - - -- unordered lets - ul :: Bool - ul = case eqv of - StrictEquiv -> False - IgnoreTypesAndTicksEquiv -> False - UnorderedLetsEquiv -> True - - goStart :: Var -> CoreExpr -> Var -> CoreExpr -> Either SDoc () - goStart x e1 y e2 = do - tracePut 0 "TOP" (varToString x ++ " =?= " ++ varToString y) - if | Just x' <- essentiallyVar e1 - , Just e1' <- lookup x' slice1 - -> goStart x' e1' y e2 - - | Just y' <- essentiallyVar e2 - , Just e2' <- lookup y' slice2 - -> goStart x e1 y' e2' - - -- otherwise if neither x and y expressions are variables - -- 1. compare the expressions (already assuming that x and y are equal) - -- 2. comparison may create new obligations, loop. - | otherwise - -> do - let env = rnBndr2 (mkRnEnv2 emptyInScopeSet) x y - ee = initialEqEnv slice1 slice2 - go [] 0 env ee e1 e2 - - essentiallyVar :: CoreExpr -> Maybe Var - essentiallyVar (App e a) | it, isTyCoArg a = essentiallyVar e - essentiallyVar (Lam v e) | it, isTyCoVar v = essentiallyVar e - essentiallyVar (Cast e _) | it = essentiallyVar e -#if MIN_VERSION_ghc(9,0,0) - essentiallyVar (Case s b _ alts) | it, Just e <- isUnsafeEqualityCase s b alts = essentiallyVar e -#endif - essentiallyVar (Var v) = Just v - essentiallyVar (Tick HpcTick{} e) | it = essentiallyVar e - essentiallyVar (Tick SourceNote{} e) = essentiallyVar e - essentiallyVar _ = Nothing - - -- report inequality - inequality :: [SDoc] -> SDoc -> Either SDoc a - inequality [] err = Left err - inequality ctx err = Left $ err $$ hang (text "in") 2 (vcat ctx) - - go :: [SDoc] -> Int -> RnEnv2 -> EqEnv -> CoreExpr -> CoreExpr -> Either SDoc () - go ctx lv env ee (essentiallyVar -> Just v1) (essentiallyVar -> Just v2) = do - -- NOTE: The ordering of this checks is important. - -- - -- See example https://github.com/nomeata/inspection-testing/pull/89#issuecomment-2967774956 - -- GHC may use same name for local names in different bindings. - -- - -- Therefore we first check for already visited and lambda-bound variables. - -- (inRnEnvL/inRnEnvR checks are important so we don't confuse for unbound variables). - -- We need to this first to break loops of recursive definitions,. - -- - -- Then we test whether variables are top or local-let bound. - -- If so, we proceed to compare their definitions. - -- - -- Lastly we check whether variables are equal. - -- This case checks for any global names. - if - | inRnEnvL env v1 - , inRnEnvR env v2 - , rnOccL env v1 == rnOccR env v2 -> do - tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " IN ENV") - return () - - | Just (i, j, e1, e2) <- lookupEqEnv v1 v2 ee -> - -- we check that levels are the same - -- if they are not we fail immediately and not fall-back further. - if i == j - then do - tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " BOUND " ++ show i) - let ctx' = text "comparing definitions of" <+> ppr v1 <+> text "=?=" <+> ppr v2 : ctx - let env' = rnBndr2 env v1 v2 - go ctx' lv env' ee e1 e2 - else do - tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " BOUND IN DIFFERENT LETS " ++ show i ++ " /= " ++ show j) - inequality ctx $ hsep [ text "variables", ppr v1, text "and", ppr v2, text "are bound in different lets" ] - - | v1 == v2 -> do - tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " SAME") - return () - - | otherwise -> do - tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " NOT EQUAL") - inequality ctx $ hsep [ text "inequal variables", ppr v1, text "and", ppr v2 ] - - go ctx lv _ _ (Lit lit1) (Lit lit2) = do - tracePut lv "LIT" "???" -- no Show for Literal :( - unless (lit1 == lit2) $ inequality ctx $ sep [ text "inequal literals", ppr lit1, text "and", ppr lit2 ] - - go ctx _ env _ (Type t1) (Type t2) = - goTypes ctx env t1 t2 - - go ctx _ env _ (Coercion co1) (Coercion co2) = - goCoercions ctx env co1 co2 - - go ctx lv env ee (Cast e1 _) e2 | it = go ctx lv env ee e1 e2 - go ctx lv env ee e1 (Cast e2 _) | it = go ctx lv env ee e1 e2 -#if MIN_VERSION_ghc(9,0,0) - go ctx lv env ee (Case s b _ alts) e2 | it, Just e1 <- isUnsafeEqualityCase s b alts = go ctx lv env ee e1 e2 - go ctx lv env ee e1 (Case s b _ alts) | it, Just e2 <- isUnsafeEqualityCase s b alts = go ctx lv env ee e1 e2 -#endif - go ctx lv env ee (Cast e1 co1) (Cast e2 co2) = traceBlock lv "CAST" "" $ \lv -> do - goCoercions ctx env co1 co2 - go ctx lv env ee e1 e2 - - go ctx lv env ee (App e1 a) e2 | it, isTyCoArg a = go ctx lv env ee e1 e2 - go ctx lv env ee e1 (App e2 a) | it, isTyCoArg a = go ctx lv env ee e1 e2 - go ctx lv env ee (App f1 a1) (App f2 a2) = traceBlock lv "APP" "" $ \lv -> do - go ctx lv env ee f1 f2 - go ctx lv env ee a1 a2 - go ctx lv env ee (Tick HpcTick{} e1) e2 | it = go ctx lv env ee e1 e2 - go ctx lv env ee e1 (Tick HpcTick{} e2) | it = go ctx lv env ee e1 e2 - go ctx lv env ee (Tick SourceNote{} e1) e2 = go ctx lv env ee e1 e2 - go ctx lv env ee e1 (Tick SourceNote{} e2) = go ctx lv env ee e1 e2 - go ctx lv env ee (Tick n1 e1) (Tick n2 e2) = traceBlock lv "TICK" "" $ \lv -> do - unless (go_tick env n1 n2) $ inequality ctx $ text "inequal ticks" - go ctx lv env ee e1 e2 - - go ctx lv env ee (Lam b e1) e2 | it, isTyCoVar b = go ctx lv env ee e1 e2 - go ctx lv env ee e1 (Lam b e2) | it, isTyCoVar b = go ctx lv env ee e1 e2 - go ctx lv env ee (Lam b1 e1) (Lam b2 e2) = traceBlock lv "LAM" (varToString b1 ++ " ~ " ++ varToString b2) $ \lv -> do - unless it $ goTypes ctx env (varType b1) (varType b2) - go ctx lv (rnBndr2 env b1 b2) ee e1 e2 - - go ctx lv env ee e1@(Let _ _) e2@(Let _ _) - | ul - , (ps1, e1') <- peelLets e1 - , (ps2, e2') <- peelLets e2 - = traceBlock lv "LET" (showVars ps1 ++ " ~ " ++ showVars ps2) $ \lv -> do - let ctx' = text "let bindings:" <+> pprVars ps1 <+> pprVars ps2 : ctx - unless (equalLength ps1 ps2) $ inequality ctx $ text "different amount of bindings in let" - let ee' = bindEqEnv ps1 ps2 ee - go ctx' lv env ee' e1' e2' - - go ctx lv env ee (Let (NonRec v1 r1) e1) (Let (NonRec v2 r2) e2) - = do go ctx lv env ee r1 r2 -- No need to check binder types, since RHSs match - go ctx lv (rnBndr2 env v1 v2) ee e1 e2 - - go ctx lv env ee (Let (Rec ps1) e1) (Let (Rec ps2) e2) - = do - unless (equalLength ps1 ps2) $ inequality ctx $ text "different amount of bindings in recursive let" - sequence_ $ zipWith (go ctx lv env' ee) rs1 rs2 - go ctx lv env' ee e1 e2 - where - bs1, bs2 :: [CoreBndr] - rs1, rs2 :: [CoreExpr] - - (bs1,rs1) = unzip ps1 - (bs2,rs2) = unzip ps2 - env' = rnBndrs2 env bs1 bs2 - - go ctx lv env ee (Case e1 b1 t1 a1) (Case e2 b2 t2 a2) - | null a1 -- See Note [Empty case alternatives] in TrieMap - , null a2 - = do - go ctx lv env ee e1 e2 - unless it $ goTypes ctx env t1 t2 - - | otherwise - = traceBlock lv "CASE" "..." $ \lv -> do - unless (equalLength a1 a2) $ inequality ctx $ text "different amount of alternatives in case" - go ctx lv env ee e1 e2 - sequence_ $ zipWith (go_alt ctx lv (rnBndr2 env b1 b2) ee) a1 a2 - - go ctx lv _ _ e1 e2 = do - tracePut lv "FAIL" (conToString e1 ++ " =/= " ++ conToString e2) - inequality ctx $ sep [ text "inequal terms:", ppr e1, text "and", ppr e2] - - goCoercions ctx env t1 t2 - | eqCoercionX env t1 t2 = return () - | otherwise = inequality ctx $ sep [ text "inequal coercions:", ppr t1, text "and", ppr t2 ] - - goTypes ctx env t1 t2 - | eqTypeX env t1 t2 = return () - | otherwise = inequality ctx $ sep [ text "inequal types:", ppr t1, text "and", ppr t2 ] - - ----------- - go_alt :: [SDoc] -> Int -> RnEnv2 -> EqEnv -> CoreAlt -> CoreAlt -> Either SDoc () - go_alt ctx lv env ee (Alt c1 bs1 e1) (Alt c2 bs2 e2) - = traceBlock lv "ALT" "..." $ \lv -> do - unless (c1 == c2) $ inequality ctx $ sep [ text "inequal constructors:", ppr c1, text "and", ppr c2 ] - go ctx lv (rnBndrs2 env bs1 bs2) ee e1 e2 - - go_tick :: RnEnv2 -> CoreTickish -> CoreTickish -> Bool - go_tick env Breakpoint{ breakpointId = lid, breakpointFVs = lids } Breakpoint{ breakpointId = rid, breakpointFVs = rids } - = lid == rid && map (rnOccL env) lids == map (rnOccR env) rids - go_tick _ l r = l == r - - peelLets (Let (NonRec v r) e) = let (xs, e') = peelLets e in ((v,r):xs, e') - peelLets (Let (Rec bs) e) = let (xs, e') = peelLets e in (bs ++ xs, e') - peelLets e = ([], e) - -#if !MIN_VERSION_ghc(9,9,0) && MIN_VERSION_ghc(9,0,0) -isUnsafeEqualityCase :: CoreExpr -> Id -> [CoreAlt] -> Maybe CoreExpr -isUnsafeEqualityCase scrut _bndr [Alt _ _ rhs] - | isUnsafeEqualityProof scrut = Just rhs -isUnsafeEqualityCase _ _ _ = Nothing -#endif - -#if !MIN_VERSION_ghc(9,2,0) -type CoreTickish = Tickish Id -#endif - -traceBlock :: Monad m => Int -> String -> String -> (Int -> m ()) -> m () -traceBlock lv name msg action = do - tracePut lv name msg - action (lv + 1) - tracePut lv name $ msg ++ " OK" - -showVars :: [(Var, a)] -> String -showVars xs = intercalate ", " [ varToString x | (x, _) <- xs ] - -pprVars :: [(Var, a)] -> SDoc -pprVars = braces . hsep . map (ppr . fst) - -varToString :: Var -> String -varToString v = occNameString (occName (tyVarName v)) ++ "_" ++ show (getUnique v) --- using tyVarName as varName is ambiguous. - -conToString :: CoreExpr -> [Char] -conToString Var {} = "Var" -conToString Lit {} = "Lit" -conToString App {} = "App" -conToString Lam {} = "Lam" -conToString Let {} = "Let" -conToString Case {} = "Case" -conToString Cast {} = "Cast" -conToString Tick {} = "Tick" -conToString Type {} = "Type" -conToString Coercion {} = "Coercion" - --- | Returns @True@ if the given core expression mentions no type constructor --- anywhere that has the given name. -freeOfType :: Slice -> [Name] -> Maybe (Var, CoreExpr) -freeOfType slice tcNs = - fmap (\(a,b,_) -> (a,b)) - $ allTyCons (\tc -> getName tc `notElem` tcNs) slice - --- | Check if all type constructors in a slice satisfy the given predicate. --- Returns the binder, expression and failing constructors triple on failure. -allTyCons :: (TyCon -> Bool) -> Slice -> Maybe (Var, CoreExpr, [TyCon]) -allTyCons ignore slice = - listToMaybe - [(v, e, nub tcs) | (v, e) <- slice, let tcs = go e, not (null tcs)] - where - goV v = goT (varType v) - - go (Var v) = goV v - go (Lit _) = [] - go (App e a) = go e ++ go a - go (Lam b e) = goV b ++ go e - go (Let bind body) = concatMap goB (flattenBinds [bind]) ++ go body - go (Case s b _ alts) = go s ++ goV b ++ concatMap goA alts - go (Cast e _) = go e - go (Tick _ e) = go e - go (Type t) = (goT t) - go (Coercion _) = [] - - goB (b, e) = goV b ++ go e - - goA (Alt _ pats e) = concatMap goV pats ++ go e - - goT (TyVarTy _) = [] - goT (AppTy t1 t2) = goT t1 ++ goT t2 - goT (TyConApp tc ts) = [tc | not (ignore tc)] ++ concatMap goT ts - -- ↑ This is the crucial bit - goT (ForAllTy _ t) = goT t -#if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0) - goT (FunTy -#if MIN_VERSION_GLASGOW_HASKELL(9,0,0,0) - _ -#endif -# if MIN_VERSION_GLASGOW_HASKELL(8,9,0,0) - _ -# endif - t1 t2) = goT t1 ++ goT t2 -#endif - goT (LitTy _) = [] - goT (CastTy t _) = goT t - goT (CoercionTy _) = [] --- --- | Returns @True@ if the given core expression mentions no term variable --- anywhere that has the given name. -freeOfTerm :: Slice -> [Name] -> Maybe (Var, CoreExpr) -freeOfTerm slice needles = listToMaybe [ (v,e) | (v,e) <- slice, not (go e) ] - where - isNeedle n = n `elem` needles - - goV v | isNeedle (Var.varName v) = False - | Just dc <- isDataConId_maybe v - , isNeedle (dataConName dc) = False - | otherwise = True - - go (Var v) = goV v - go (Lit _ ) = True - go (App e a) = go e && go a - go (Lam _ e) = go e - go (Let bind body) = all goB (flattenBinds [bind]) && go body - go (Case s _ _ alts) = go s && all goA alts - go (Cast e _) = go e - go (Tick _ e) = go e - go (Type _) = True - go (Coercion _) = True - - goB (_, e) = go e - - goA (Alt ac _ e) = goAltCon ac && go e - - goAltCon (DataAlt dc) | isNeedle (dataConName dc) = False - goAltCon _ = 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 :: Slice -> 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 (Alt _ _ e) = go a e - -doesNotContainTypeClasses :: Slice -> [Name] -> Maybe (Var, CoreExpr, [TyCon]) -doesNotContainTypeClasses slice tcNs - = allTyCons (\tc -> not (isClassTyCon tc) || isCTupleTyConName (getName tc) || any (getName tc ==) tcNs) slice - -rename :: InScopeSet -> [(Var, Var)] -> CoreExpr -> CoreExpr -rename iss rn = substExpr' sub where - -- convert RnEnv2 to Subst - -- here we forget about tyvars and covars, but mostly this is good enough. - sub = mkOpenSubst iss [ (v1, if isTyVar v2 then Type (mkTyVarTy v2) else if isCoVar v2 then Coercion (mkCoVarCo v2) else Var v2 ) | (v1, v2) <- rn] - -#if MIN_VERSION_GLASGOW_HASKELL(9,0,0,0) - substExpr' = substExpr -#else - substExpr' = substExpr empty -#endif +-- | This module implements some analyses of Core expressions necessary for +-- "Test.Inspection". Normally, users of this package can ignore this module. +{-# LANGUAGE CPP, FlexibleContexts, PatternSynonyms, MultiWayIf, ViewPatterns #-} +module Test.Inspection.Core + ( slice + , pprSlice + , pprSliceDifference + , eqSlice + , eqSlice' + , freeOfType + , freeOfTerm + , doesNotAllocate + , doesNotContainTypeClasses + ) where + +#if MIN_VERSION_ghc(9,0,0) +import GHC.Builtin.Types (isCTupleTyConName) +import GHC.Core +import GHC.Core.Utils +import GHC.Core.TyCo.Rep +import GHC.Core.Type +import GHC.Types.Var as Var +import GHC.Types.Var.Set (mkVarSet) +import GHC.Types.Id +import GHC.Types.Name +import GHC.Types.Literal +import GHC.Types.Var.Env +import GHC.Types.Unique +import GHC.Utils.Outputable as Outputable +import GHC.Core.Ppr +import GHC.Core.Subst +import GHC.Core.Coercion +import GHC.Utils.Misc +import GHC.Core.DataCon +import GHC.Core.TyCon (TyCon, isClassTyCon) +#else +import TysWiredIn (isCTupleTyConName) +import CoreSyn +import CoreUtils +import CoreSubst +import TyCoRep +import Type +import Var +import VarSet (mkVarSet) +import Id +import Literal +import Name +import VarEnv +import Outputable +import PprCore +import Coercion +import Util +import DataCon +import Unique +import TyCon (TyCon, isClassTyCon) +#endif + +#if MIN_VERSION_ghc(9,2,0) +import GHC.Types.Tickish +#endif + +#if MIN_VERSION_ghc(9,6,0) +import GHC.Core.TyCo.Compare (eqTypeX) +#endif + +import qualified Data.Set as S +import Control.Monad (unless) +import Control.Monad.Trans.State.Strict (execState, modify', gets) +import Data.List (nub, intercalate) +import Data.Maybe (listToMaybe, fromJust) +import Data.Either (isRight) + +import Test.Inspection (Equivalence (..)) + +-- Uncomment to enable debug traces +-- #define DEBUG_TRACE + +#ifdef DEBUG_TRACE +import Debug.Trace + +tracePut :: Monad m => Int -> String -> String -> m () +tracePut lv name msg = traceM $ replicate lv ' ' ++ name ++ ": " ++ msg +#else +tracePut :: Monad m => Int -> String -> String -> m () +tracePut _ _ _ = return () +#endif + +#if !MIN_VERSION_ghc(9,2,0) +pattern Alt :: a -> b -> c -> (a, b, c) +pattern Alt a b c = (a, b, c) +{-# COMPLETE Alt #-} +#endif + + +type Slice = [(Var, CoreExpr)] + +-- | Selects those bindings that define the given variable (with this variable first) +slice :: [(Var, CoreExpr)] -> Var -> Slice +slice binds v + | Just e <- lookup v binds + = (v,e) : [(v',e) | (v',e) <- binds, v' /= v, v' `S.member` used ] + | otherwise + = error "slice: cannot find given variable in bindings" + 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 e = fromJust $ lookup v binds + go e + | otherwise = return () + + go (Var v) = goV v + go (Lit _ ) = pure () + go (App e arg) | isTyCoArg arg = go e + go (App e arg) = go e >> go arg + 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 (Alt _ _ e) = go e + +-- | Pretty-print a slice +pprSlice :: Slice -> SDoc +pprSlice slice = + withLessDetail $ pprCoreBindings [ NonRec v e | (v,e) <- slice ] + +-- | Pretty-print two slices, after removing variables occurring in both +pprSliceDifference :: Slice -> Slice -> SDoc +pprSliceDifference slice1 slice2 + | [(v1,e1)] <- slice1' + , [(v2,e2)] <- slice2' + = pprSingletonSliceDifference (mkInScopeSet (mkVarSet (S.toList both))) v1 v2 e1 e2 + + | otherwise = + hang (text "LHS" Outputable.<> colon) 4 (pprSlice slice1') $$ + hang (text "RHS" Outputable.<> colon) 4 (pprSlice slice2') + where + both = S.intersection (S.fromList (map fst slice1)) (S.fromList (map fst slice2)) + slice1' = filter (\(v,_) -> v `S.notMember` both) slice1 + slice2' = filter (\(v,_) -> v `S.notMember` both) slice2 + +pprSingletonSliceDifference :: InScopeSet -> Var -> Var -> CoreExpr -> CoreExpr -> SDoc +pprSingletonSliceDifference iss v1 v2 e1 e2 = + ctxDoc $ + hang (text "LHS" Outputable.<> colon) 4 (hang (pprPrefixOcc v1) 2 (eqSign <+> pprCoreExpr e1')) $$ + hang (text "RHS" Outputable.<> colon) 4 (hang (pprPrefixOcc v2) 2 (eqSign <+> pprCoreExpr e2')) + where + hasContext = not (null ctxt) + + ctxDoc | hasContext = id + | otherwise = (hang (text "In") 4 (ppr $ mkContextExpr (reverse (map snd ctxt))) $$) + + eqSign | hasContext = text "= ..." + | otherwise = equals + + (e1', e2', ctxt) = go e1 e2 [] (mkRnEnv2 emptyInScopeSet) + + go :: CoreExpr -> CoreExpr -> [(Var, Var)] -> RnEnv2 -> (CoreExpr, CoreExpr, [(Var, Var)]) + go (Lam b1 t1) (Lam b2 t2) ctxt env + | eqTypeX env (varType b1) (varType b2) + = go t1 t2 ((b1,b2):ctxt) (rnBndr2 env b1 b2) + where + go x y ctxt _env = (rename iss ctxt x, y, ctxt) + + mkContextExpr :: [Var] -> CoreExpr + mkContextExpr [] = ellipsis + mkContextExpr (x:rest) = Lam x (mkContextExpr rest) + + ellipsis :: CoreExpr +#if MIN_VERSION_ghc(8,8,0) + ellipsis = Lit $ mkLitString "..." +#else + ellipsis = Lit $ mkMachString "..." +#endif + +withLessDetail :: SDoc -> SDoc +#if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0) && !MIN_VERSION_GLASGOW_HASKELL(9,0,0,0) +withLessDetail sdoc = sdocWithDynFlags $ \dflags -> + withPprStyle (defaultUserStyle dflags) sdoc +#else +withLessDetail sdoc = withPprStyle defaultUserStyle sdoc +#endif + +-- | Equality name environment. +-- This environment contains top-level and let-bound definitions +-- (no lambda arguments). +data EqEnv = EqEnv !Int [(Var, (Int, CoreExpr))] [(Var, (Int, CoreExpr))] + +-- | Lookup left and right variables in EqEnv. +lookupEqEnv :: Var -> Var -> EqEnv -> Maybe (Int, Int, CoreExpr, CoreExpr) +lookupEqEnv x y (EqEnv _ env1 env2) + | Just (i, e1) <- lookup x env1 + , Just (j, e2) <- lookup y env2 + = Just (i, j, e1, e2) + + | otherwise + = Nothing + +initialEqEnv :: [(Var, CoreExpr)] -> [(Var, CoreExpr)] -> EqEnv +initialEqEnv ls rs = EqEnv 1 + [ (x, (0, e1)) | (x, e1) <- ls ] + [ (y, (0, e2)) | (y, e2) <- rs ] + +bindEqEnv :: [(Var, CoreExpr)] -> [(Var, CoreExpr)] -> EqEnv -> EqEnv +bindEqEnv ls rs (EqEnv i env1 env2)= EqEnv (i + 1) + ([ (x, (i, e1)) | (x, e1) <- ls ] ++ env1) + ([ (y, (i, e2)) | (y, e2) <- rs ] ++ env2) + +-- | This is a heuristic, which only works if both slices +-- have auxiliary 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 :: Equivalence -> Slice -> Slice -> Bool +eqSlice eqv l r = isRight (eqSlice' eqv l r) + +-- | Like 'eqSlice' but also returns an explanation of inequality. +eqSlice' :: Equivalence -> Slice -> Slice -> Either SDoc () +eqSlice' _ [] [] = Right () +eqSlice' _ ((v,_) : _) [] = Left $ ppr v +eqSlice' _ [] ((v,_) : _) = Left $ ppr v + -- Mostly defensive programming (slices should not be empty) +eqSlice' eqv slice1@((head1, def1) : _) slice2@((head2, def2) : _) = do + goStart head1 def1 head2 def2 + where + -- ignore types and hpc ticks + it :: Bool + it = case eqv of + StrictEquiv -> False + IgnoreTypesAndTicksEquiv -> True + UnorderedLetsEquiv -> True + + -- unordered lets + ul :: Bool + ul = case eqv of + StrictEquiv -> False + IgnoreTypesAndTicksEquiv -> False + UnorderedLetsEquiv -> True + + goStart :: Var -> CoreExpr -> Var -> CoreExpr -> Either SDoc () + goStart x e1 y e2 = do + tracePut 0 "TOP" (varToString x ++ " =?= " ++ varToString y) + if | Just x' <- essentiallyVar e1 + , Just e1' <- lookup x' slice1 + -> goStart x' e1' y e2 + + | Just y' <- essentiallyVar e2 + , Just e2' <- lookup y' slice2 + -> goStart x e1 y' e2' + + -- otherwise if neither x and y expressions are variables + -- 1. compare the expressions (already assuming that x and y are equal) + -- 2. comparison may create new obligations, loop. + | otherwise + -> do + let env = rnBndr2 (mkRnEnv2 emptyInScopeSet) x y + ee = initialEqEnv slice1 slice2 + go [] 0 env ee e1 e2 + + essentiallyVar :: CoreExpr -> Maybe Var + essentiallyVar (App e a) | it, isTyCoArg a = essentiallyVar e + essentiallyVar (Lam v e) | it, isTyCoVar v = essentiallyVar e + essentiallyVar (Cast e _) | it = essentiallyVar e +#if MIN_VERSION_ghc(9,0,0) + essentiallyVar (Case s b _ alts) | it, Just e <- isUnsafeEqualityCase s b alts = essentiallyVar e +#endif + essentiallyVar (Var v) = Just v + essentiallyVar (Tick HpcTick{} e) | it = essentiallyVar e + essentiallyVar (Tick SourceNote{} e) = essentiallyVar e + essentiallyVar _ = Nothing + + -- report inequality + inequality :: [SDoc] -> SDoc -> Either SDoc a + inequality [] err = Left err + inequality ctx err = Left $ err $$ hang (text "in") 2 (vcat ctx) + + go :: [SDoc] -> Int -> RnEnv2 -> EqEnv -> CoreExpr -> CoreExpr -> Either SDoc () + go ctx lv env ee (essentiallyVar -> Just v1) (essentiallyVar -> Just v2) = do + -- NOTE: The ordering of this checks is important. + -- + -- See example https://github.com/nomeata/inspection-testing/pull/89#issuecomment-2967774956 + -- GHC may use same name for local names in different bindings. + -- + -- Therefore we first check for already visited and lambda-bound variables. + -- (inRnEnvL/inRnEnvR checks are important so we don't confuse for unbound variables). + -- We need to this first to break loops of recursive definitions,. + -- + -- Then we test whether variables are top or local-let bound. + -- If so, we proceed to compare their definitions. + -- + -- Lastly we check whether variables are equal. + -- This case checks for any global names. + if + | inRnEnvL env v1 + , inRnEnvR env v2 + , rnOccL env v1 == rnOccR env v2 -> do + tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " IN ENV") + return () + + | Just (i, j, e1, e2) <- lookupEqEnv v1 v2 ee -> + -- we check that levels are the same + -- if they are not we fail immediately and not fall-back further. + if i == j + then do + tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " BOUND " ++ show i) + let ctx' = text "comparing definitions of" <+> ppr v1 <+> text "=?=" <+> ppr v2 : ctx + let env' = rnBndr2 env v1 v2 + go ctx' lv env' ee e1 e2 + else do + tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " BOUND IN DIFFERENT LETS " ++ show i ++ " /= " ++ show j) + inequality ctx $ hsep [ text "variables", ppr v1, text "and", ppr v2, text "are bound in different lets" ] + + | v1 == v2 -> do + tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " SAME") + return () + + | otherwise -> do + tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " NOT EQUAL") + inequality ctx $ hsep [ text "inequal variables", ppr v1, text "and", ppr v2 ] + + go ctx lv _ _ (Lit lit1) (Lit lit2) = do + tracePut lv "LIT" "???" -- no Show for Literal :( + unless (lit1 == lit2) $ inequality ctx $ sep [ text "inequal literals", ppr lit1, text "and", ppr lit2 ] + + go ctx _ env _ (Type t1) (Type t2) = + goTypes ctx env t1 t2 + + go ctx _ env _ (Coercion co1) (Coercion co2) = + goCoercions ctx env co1 co2 + + go ctx lv env ee (Cast e1 _) e2 | it = go ctx lv env ee e1 e2 + go ctx lv env ee e1 (Cast e2 _) | it = go ctx lv env ee e1 e2 +#if MIN_VERSION_ghc(9,0,0) + go ctx lv env ee (Case s b _ alts) e2 | it, Just e1 <- isUnsafeEqualityCase s b alts = go ctx lv env ee e1 e2 + go ctx lv env ee e1 (Case s b _ alts) | it, Just e2 <- isUnsafeEqualityCase s b alts = go ctx lv env ee e1 e2 +#endif + go ctx lv env ee (Cast e1 co1) (Cast e2 co2) = traceBlock lv "CAST" "" $ \lv -> do + goCoercions ctx env co1 co2 + go ctx lv env ee e1 e2 + + go ctx lv env ee (App e1 a) e2 | it, isTyCoArg a = go ctx lv env ee e1 e2 + go ctx lv env ee e1 (App e2 a) | it, isTyCoArg a = go ctx lv env ee e1 e2 + go ctx lv env ee (App f1 a1) (App f2 a2) = traceBlock lv "APP" "" $ \lv -> do + go ctx lv env ee f1 f2 + go ctx lv env ee a1 a2 + go ctx lv env ee (Tick HpcTick{} e1) e2 | it = go ctx lv env ee e1 e2 + go ctx lv env ee e1 (Tick HpcTick{} e2) | it = go ctx lv env ee e1 e2 + go ctx lv env ee (Tick SourceNote{} e1) e2 = go ctx lv env ee e1 e2 + go ctx lv env ee e1 (Tick SourceNote{} e2) = go ctx lv env ee e1 e2 + go ctx lv env ee (Tick n1 e1) (Tick n2 e2) = traceBlock lv "TICK" "" $ \lv -> do + unless (go_tick env n1 n2) $ inequality ctx $ text "inequal ticks" + go ctx lv env ee e1 e2 + + go ctx lv env ee (Lam b e1) e2 | it, isTyCoVar b = go ctx lv env ee e1 e2 + go ctx lv env ee e1 (Lam b e2) | it, isTyCoVar b = go ctx lv env ee e1 e2 + go ctx lv env ee (Lam b1 e1) (Lam b2 e2) = traceBlock lv "LAM" (varToString b1 ++ " ~ " ++ varToString b2) $ \lv -> do + unless it $ goTypes ctx env (varType b1) (varType b2) + go ctx lv (rnBndr2 env b1 b2) ee e1 e2 + + go ctx lv env ee e1@(Let _ _) e2@(Let _ _) + | ul + , (ps1, e1') <- peelLets e1 + , (ps2, e2') <- peelLets e2 + = traceBlock lv "LET" (showVars ps1 ++ " ~ " ++ showVars ps2) $ \lv -> do + let ctx' = text "let bindings:" <+> pprVars ps1 <+> pprVars ps2 : ctx + unless (equalLength ps1 ps2) $ inequality ctx $ text "different amount of bindings in let" + let ee' = bindEqEnv ps1 ps2 ee + go ctx' lv env ee' e1' e2' + + go ctx lv env ee (Let (NonRec v1 r1) e1) (Let (NonRec v2 r2) e2) + = do go ctx lv env ee r1 r2 -- No need to check binder types, since RHSs match + go ctx lv (rnBndr2 env v1 v2) ee e1 e2 + + go ctx lv env ee (Let (Rec ps1) e1) (Let (Rec ps2) e2) + = do + unless (equalLength ps1 ps2) $ inequality ctx $ text "different amount of bindings in recursive let" + sequence_ $ zipWith (go ctx lv env' ee) rs1 rs2 + go ctx lv env' ee e1 e2 + where + bs1, bs2 :: [CoreBndr] + rs1, rs2 :: [CoreExpr] + + (bs1,rs1) = unzip ps1 + (bs2,rs2) = unzip ps2 + env' = rnBndrs2 env bs1 bs2 + + go ctx lv env ee (Case e1 b1 t1 a1) (Case e2 b2 t2 a2) + | null a1 -- See Note [Empty case alternatives] in TrieMap + , null a2 + = do + go ctx lv env ee e1 e2 + unless it $ goTypes ctx env t1 t2 + + | otherwise + = traceBlock lv "CASE" "..." $ \lv -> do + unless (equalLength a1 a2) $ inequality ctx $ text "different amount of alternatives in case" + go ctx lv env ee e1 e2 + sequence_ $ zipWith (go_alt ctx lv (rnBndr2 env b1 b2) ee) a1 a2 + + go ctx lv _ _ e1 e2 = do + tracePut lv "FAIL" (conToString e1 ++ " =/= " ++ conToString e2) + inequality ctx $ sep [ text "inequal terms:", ppr e1, text "and", ppr e2] + + goCoercions ctx env t1 t2 + | eqCoercionX env t1 t2 = return () + | otherwise = inequality ctx $ sep [ text "inequal coercions:", ppr t1, text "and", ppr t2 ] + + goTypes ctx env t1 t2 + | eqTypeX env t1 t2 = return () + | otherwise = inequality ctx $ sep [ text "inequal types:", ppr t1, text "and", ppr t2 ] + + ----------- + go_alt :: [SDoc] -> Int -> RnEnv2 -> EqEnv -> CoreAlt -> CoreAlt -> Either SDoc () + go_alt ctx lv env ee (Alt c1 bs1 e1) (Alt c2 bs2 e2) + = traceBlock lv "ALT" "..." $ \lv -> do + unless (c1 == c2) $ inequality ctx $ sep [ text "inequal constructors:", ppr c1, text "and", ppr c2 ] + go ctx lv (rnBndrs2 env bs1 bs2) ee e1 e2 + + go_tick :: RnEnv2 -> CoreTickish -> CoreTickish -> Bool + go_tick env Breakpoint{ breakpointId = lid, breakpointFVs = lids } Breakpoint{ breakpointId = rid, breakpointFVs = rids } + = lid == rid && map (rnOccL env) lids == map (rnOccR env) rids + go_tick _ l r = l == r + + peelLets (Let (NonRec v r) e) = let (xs, e') = peelLets e in ((v,r):xs, e') + peelLets (Let (Rec bs) e) = let (xs, e') = peelLets e in (bs ++ xs, e') + peelLets e = ([], e) + +#if !MIN_VERSION_ghc(9,9,0) && MIN_VERSION_ghc(9,0,0) +isUnsafeEqualityCase :: CoreExpr -> Id -> [CoreAlt] -> Maybe CoreExpr +isUnsafeEqualityCase scrut _bndr [Alt _ _ rhs] + | isUnsafeEqualityProof scrut = Just rhs +isUnsafeEqualityCase _ _ _ = Nothing +#endif + +#if !MIN_VERSION_ghc(9,2,0) +type CoreTickish = Tickish Id +#endif + +traceBlock :: Monad m => Int -> String -> String -> (Int -> m ()) -> m () +traceBlock lv name msg action = do + tracePut lv name msg + action (lv + 1) + tracePut lv name $ msg ++ " OK" + +showVars :: [(Var, a)] -> String +showVars xs = intercalate ", " [ varToString x | (x, _) <- xs ] + +pprVars :: [(Var, a)] -> SDoc +pprVars = braces . hsep . map (ppr . fst) + +varToString :: Var -> String +varToString v = occNameString (occName (tyVarName v)) ++ "_" ++ show (getUnique v) +-- using tyVarName as varName is ambiguous. + +conToString :: CoreExpr -> [Char] +conToString Var {} = "Var" +conToString Lit {} = "Lit" +conToString App {} = "App" +conToString Lam {} = "Lam" +conToString Let {} = "Let" +conToString Case {} = "Case" +conToString Cast {} = "Cast" +conToString Tick {} = "Tick" +conToString Type {} = "Type" +conToString Coercion {} = "Coercion" + +-- | Returns @True@ if the given core expression mentions no type constructor +-- anywhere that has the given name. +freeOfType :: Slice -> [Name] -> Maybe (Var, CoreExpr) +freeOfType slice tcNs = + fmap (\(a,b,_) -> (a,b)) + $ allTyCons (\tc -> getName tc `notElem` tcNs) slice + +-- | Check if all type constructors in a slice satisfy the given predicate. +-- Returns the binder, expression and failing constructors triple on failure. +allTyCons :: (TyCon -> Bool) -> Slice -> Maybe (Var, CoreExpr, [TyCon]) +allTyCons ignore slice = + listToMaybe + [(v, e, nub tcs) | (v, e) <- slice, let tcs = go e, not (null tcs)] + where + goV v = goT (varType v) + + go (Var v) = goV v + go (Lit _) = [] + go (App e a) = go e ++ go a + go (Lam b e) = goV b ++ go e + go (Let bind body) = concatMap goB (flattenBinds [bind]) ++ go body + go (Case s b _ alts) = go s ++ goV b ++ concatMap goA alts + go (Cast e _) = go e + go (Tick _ e) = go e + go (Type t) = (goT t) + go (Coercion _) = [] + + goB (b, e) = goV b ++ go e + + goA (Alt _ pats e) = concatMap goV pats ++ go e + + goT (TyVarTy _) = [] + goT (AppTy t1 t2) = goT t1 ++ goT t2 + goT (TyConApp tc ts) = [tc | not (ignore tc)] ++ concatMap goT ts + -- ↑ This is the crucial bit + goT (ForAllTy _ t) = goT t +#if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0) + goT (FunTy +#if MIN_VERSION_GLASGOW_HASKELL(9,0,0,0) + _ +#endif +# if MIN_VERSION_GLASGOW_HASKELL(8,9,0,0) + _ +# endif + t1 t2) = goT t1 ++ goT t2 +#endif + goT (LitTy _) = [] + goT (CastTy t _) = goT t + goT (CoercionTy _) = [] +-- +-- | Returns @True@ if the given core expression mentions no term variable +-- anywhere that has the given name. +freeOfTerm :: Slice -> [Name] -> Maybe (Var, CoreExpr) +freeOfTerm slice needles = listToMaybe [ (v,e) | (v,e) <- slice, not (go e) ] + where + isNeedle n = n `elem` needles + + goV v | isNeedle (Var.varName v) = False + | Just dc <- isDataConId_maybe v + , isNeedle (dataConName dc) = False + | otherwise = True + + go (Var v) = goV v + go (Lit _ ) = True + go (App e a) = go e && go a + go (Lam _ e) = go e + go (Let bind body) = all goB (flattenBinds [bind]) && go body + go (Case s _ _ alts) = go s && all goA alts + go (Cast e _) = go e + go (Tick _ e) = go e + go (Type _) = True + go (Coercion _) = True + + goB (_, e) = go e + + goA (Alt ac _ e) = goAltCon ac && go e + + goAltCon (DataAlt dc) | isNeedle (dataConName dc) = False + goAltCon _ = 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 :: Slice -> 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 (Alt _ _ e) = go a e + +doesNotContainTypeClasses :: Slice -> [Name] -> Maybe (Var, CoreExpr, [TyCon]) +doesNotContainTypeClasses slice tcNs + = allTyCons (\tc -> not (isClassTyCon tc) || isCTupleTyConName (getName tc) || any (getName tc ==) tcNs) slice + +rename :: InScopeSet -> [(Var, Var)] -> CoreExpr -> CoreExpr +rename iss rn = substExpr' sub where + -- convert RnEnv2 to Subst + -- here we forget about tyvars and covars, but mostly this is good enough. + sub = mkOpenSubst iss [ (v1, if isTyVar v2 then Type (mkTyVarTy v2) else if isCoVar v2 then Coercion (mkCoVarCo v2) else Var v2 ) | (v1, v2) <- rn] + +#if MIN_VERSION_GLASGOW_HASKELL(9,0,0,0) + substExpr' = substExpr +#else + substExpr' = substExpr empty +#endif diff --git a/src/Test/Inspection/Plugin.hs b/src/Test/Inspection/Plugin.hs --- a/src/Test/Inspection/Plugin.hs +++ b/src/Test/Inspection/Plugin.hs @@ -1,376 +1,376 @@ --- | See "Test.Inspection". --- -{-# LANGUAGE CPP #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE MultiWayIf #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE LambdaCase #-} -module Test.Inspection.Plugin - ( plugin - , checkProperty - , CheckResult(..) - , prettyProperty - ) where - -import Control.Monad -import System.Exit -import Data.Either -import Data.Maybe -import Data.Bifunctor -import Data.List -import qualified Data.Map.Strict as M -import qualified Language.Haskell.TH.Syntax as TH - -#if MIN_VERSION_ghc(9,4,0) -import GHC.Types.Error -import GHC.Driver.Session -#endif - -#if MIN_VERSION_ghc(9,0,0) -import GHC.Plugins hiding (SrcLoc) -import GHC.Utils.Outputable as Outputable -#else -import GhcPlugins hiding (SrcLoc) -import Outputable -#endif - -#if MIN_VERSION_ghc(9,2,0) -import GHC.Types.TyThing -#endif - -import Test.Inspection (Obligation(..), Equivalence (..), Property(..), Result(..)) -import Test.Inspection.Core - --- | The plugin. It supports some options: --- --- * @-fplugin-opt=Test.Inspection.Plugin:keep-going@ to keep building despite failing obligations --- * @-fplugin-opt=Test.Inspection.Plugin:keep-going-O0@ to keep building despite failing obligations, when optimisations are off --- * @-fplugin-opt=Test.Inspection.Plugin:skip-O0@ to skip performing inspections when optimisations are off --- * @-fplugin-opt=Test.Inspection.Plugin:quiet@ to be silent if all obligations are fulfilled --- --- It makes sense to enable only one of @keep-going@, @keep-going-O0@ and --- @skip-O0@ at a time. @skip-O0@ is useful when working with GHCi, to suppress --- inspection failure messages and eliminate the overhead of inspection when --- loading. - - -plugin :: Plugin -plugin = defaultPlugin - { installCoreToDos = install -#if __GLASGOW_HASKELL__ >= 806 - , pluginRecompile = \_args -> pure NoForceRecompile -#endif - } - -data UponFailure = AbortCompilation | KeepGoingO0 | SkipO0 | KeepGoing deriving Eq - -data ReportingMode = Verbose | Quiet deriving Eq - -data ResultTarget = PrintAndAbort | StoreAt Name - -install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo] -install args passes = return $ passes ++ [pass] - where - pass = CoreDoPluginPass "Test.Inspection.Plugin" (proofPass upon_failure report) - upon_failure | "keep-going" `elem` args = KeepGoing - | "keep-going-O0" `elem` args = KeepGoingO0 - | "skip-O0" `elem` args = SkipO0 - | otherwise = AbortCompilation - report | "quiet" `elem` args = Quiet - | otherwise = Verbose - -extractObligations :: ModGuts -> (ModGuts, [(ResultTarget, Obligation)]) -extractObligations guts = (guts', obligations) - where - (anns_clean, obligations) = partitionMaybe findObligationAnn (mg_anns guts) - guts' = guts { mg_anns = anns_clean } - -findObligationAnn :: Annotation -> Maybe (ResultTarget, Obligation) -findObligationAnn (Annotation (ModuleTarget _) payload) - | Just obl <- fromSerialized deserializeWithData payload - = Just (PrintAndAbort, obl) -findObligationAnn (Annotation (NamedTarget n) payload) - | Just obl <- fromSerialized deserializeWithData payload - = Just (StoreAt n, obl) -findObligationAnn _ - = Nothing - -prettyObligation :: Module -> Obligation -> String -> String -prettyObligation mod (Obligation {..}) result = - maybe "" myPrettySrcLoc srcLoc ++ ": " ++ name ++ " " ++ result - where - name = case testName of - Just n -> n - Nothing -> prettyProperty (showTHName mod) target property - -prettyProperty :: (TH.Name -> String) -> TH.Name -> Property -> String -prettyProperty showName target = \case - EqualTo n2 eqv -> showName target ++ " " ++ showEquiv eqv ++ " " ++ showName n2 - NoTypes [t] -> showName target ++ " `hasNoType` " ++ showName t - NoTypes ts -> showName target ++ " mentions none of " ++ intercalate ", " (map showName ts) - NoAllocation -> showName target ++ " does not allocate" - NoTypeClasses [] -> showName target ++ " does not contain dictionary values" - NoTypeClasses ts -> showName target ++ " does not contain dictionary values except of " ++ intercalate ", " (map showName ts) - NoUseOf ns -> showName target ++ " uses none of " ++ intercalate ", " (map showName ns) - CoreOf -> showName target ++ " core dump" -- :) - where - showEquiv StrictEquiv = "===" - showEquiv IgnoreTypesAndTicksEquiv = "==-" - showEquiv UnorderedLetsEquiv = "==~" - --- | 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 - -data Stat = ExpSuccess | ExpFailure | UnexpSuccess | UnexpFailure | StoredResult - deriving (Enum, Eq, Ord, Bounded) -type Stats = M.Map Stat Int - -type Updates = [(Name, Result)] - -tick :: Stat -> Stats -tick s = M.singleton s 1 - -checkObligation :: ReportingMode -> ModGuts -> (ResultTarget, Obligation) -> CoreM (Updates, Stats) -checkObligation report guts (reportTarget, obl) = do - - res <- checkProperty guts (target obl) (property obl) - case reportTarget of - PrintAndAbort -> do - category <- case (res, expectFail obl) of - -- Property holds - (ResSuccess, False) -> do - unless (report == Quiet) $ - putMsgS $ prettyObligation (mg_module guts) obl expSuccess - return ExpSuccess - (ResSuccess, True) -> do - putMsgS $ prettyObligation (mg_module guts) obl unexpSuccess - return UnexpSuccess - -- Property holds, with extra message - (ResSuccessWithMessage reportDoc, False) -> do - unless (report == Quiet) $ do - putMsgS $ prettyObligation (mg_module guts) obl expSuccess - putMsg reportDoc - return ExpSuccess - (ResSuccessWithMessage reportDoc, True) -> do - putMsgS $ prettyObligation (mg_module guts) obl unexpSuccess - putMsg reportDoc - return UnexpSuccess - -- Property does not hold - (ResFailure reportDoc, False) -> do - putMsgS $ prettyObligation (mg_module guts) obl unexpFailure - putMsg $ reportDoc - return UnexpFailure - (ResFailure _, True) -> do - unless (report == Quiet) $ - putMsgS $ prettyObligation (mg_module guts) obl expFailure - return ExpFailure - return ([], tick category) - StoreAt name -> do - dflags <- getDynFlags - let result = case res of - ResSuccess -> Success $ showSDoc dflags $ - text (prettyObligation (mg_module guts) obl expSuccess) - ResSuccessWithMessage msg -> Success $ showSDoc dflags $ - text (prettyObligation (mg_module guts) obl expSuccess) $$ - msg - ResFailure reportMsg -> Failure $ showSDoc dflags $ - text (prettyObligation (mg_module guts) obl unexpFailure) $$ - reportMsg - pure ([(name, result)], tick StoredResult) - - where - expSuccess = "passed." - unexpSuccess = "passed unexpectedly!" - unexpFailure = "failed:" - expFailure = "failed expectedly." - - -data CheckResult - = ResSuccess - | ResSuccessWithMessage SDoc - | ResFailure SDoc - -lookupNameInGuts :: ModGuts -> Name -> Maybe (Var, CoreExpr) -lookupNameInGuts guts n = listToMaybe - [ (v,e) - | (v,e) <- flattenBinds (mg_binds guts) - , getName v == n - ] - -updateNameInGuts :: Name -> CoreExpr -> ModGuts -> ModGuts -updateNameInGuts n expr guts = - guts {mg_binds = map (updateNameInGut n expr) (mg_binds guts) } - -updateNameInGut :: Name -> CoreExpr -> CoreBind -> CoreBind -updateNameInGut n e (NonRec v _) | getName v == n = NonRec v e -updateNameInGut _ _ bind = bind - -checkProperty :: ModGuts -> TH.Name -> Property -> CoreM CheckResult -checkProperty guts thn1 (EqualTo thn2 ignore_types) = do - n1 <- fromTHName thn1 - n2 <- fromTHName thn2 - - let p1 = lookupNameInGuts guts n1 - let p2 = lookupNameInGuts guts n2 - - if | n1 == n2 - -> pure ResSuccess - -- Ok if one points to another - | Just (_, Var other) <- p1, getName other == n2 - -> pure ResSuccess - | Just (_, Var other) <- p2, getName other == n1 - -> pure ResSuccess - | Just (v1, _) <- p1 - , Just (v2, _) <- p2 - , let slice1 = slice binds v1 - , let slice2 = slice binds v2 - -> case eqSlice' ignore_types slice1 slice2 of - -- OK if they have the same expression - Right _ -> pure ResSuccess - -- Not ok if the expression differ - Left err -> pure . ResFailure $ err $$ pprSliceDifference slice1 slice2 - -- Not ok if both names are bound externally - | Nothing <- p1 - , Nothing <- p2 - -> pure . ResFailure $ ppr n1 <+> text " and " <+> ppr n2 <+> - text "are different external names" - | Nothing <- p1 - -> pure . ResFailure $ ppr n1 <+> text "is an external name" - | Nothing <- p2 - -> pure . ResFailure $ ppr n2 <+> text "is an external name" - where - binds = flattenBinds (mg_binds guts) - -checkProperty guts thn (NoUseOf thns) = do - n <- fromTHName thn - ns <- mapM fromTHName thns - case lookupNameInGuts guts n of - Nothing -> pure . ResFailure $ ppr n <+> text "is not a local name" - Just (v, _) -> case freeOfTerm (slice binds v) ns of - Just _ -> pure . ResFailure $ pprSlice (slice binds v) - Nothing -> pure ResSuccess - where binds = flattenBinds (mg_binds guts) - -checkProperty guts thn (NoTypes thts) = do - n <- fromTHName thn - ts <- mapM fromTHName thts - case lookupNameInGuts guts n of - Nothing -> pure . ResFailure $ ppr n <+> text "is not a local name" - Just (v, _) -> case freeOfType (slice binds v) ts of - Just _ -> pure . ResFailure $ pprSlice (slice binds v) - Nothing -> pure ResSuccess - where binds = flattenBinds (mg_binds guts) - -checkProperty guts thn NoAllocation = do - n <- fromTHName thn - case lookupNameInGuts guts n of - Nothing -> pure . ResFailure $ ppr n <+> text "is not a local name" - Just (v, _) -> case doesNotAllocate (slice binds v) of - Just (v',e') -> pure . ResFailure $ nest 4 (ppr v' <+> text "=" <+> ppr e') - Nothing -> pure ResSuccess - where binds = flattenBinds (mg_binds guts) - -checkProperty guts thn (NoTypeClasses thts) = do - n <- fromTHName thn - ts <- mapM fromTHName thts - case lookupNameInGuts guts n of - Nothing -> pure . ResFailure $ ppr n <+> text "is not a local name" - Just (v, _) -> case doesNotContainTypeClasses (slice binds v) ts of - Just (v',e',tc) -> pure . ResFailure - $ nest 4 $ vcat - [ text "Found type classes: " <+> ppr tc - , ppr v' <+> text "=" <+> ppr e' - ] - Nothing -> pure ResSuccess - where binds = flattenBinds (mg_binds guts) - -checkProperty guts thn CoreOf = do - n <- fromTHName thn - case lookupNameInGuts guts n of - Nothing -> pure . ResFailure $ ppr n <+> text "is not a local name" - Just (v, _) -> do - let s = slice binds v - pure $ ResSuccessWithMessage $ nest 4 $ pprSlice s - where binds = flattenBinds (mg_binds guts) - -fromTHName :: TH.Name -> CoreM Name -fromTHName thn = thNameToGhcName thn >>= \case - Nothing -> do - errorMsg $ text "Could not resolve TH name" <+> text (show thn) - liftIO $ exitFailure -- kill the compiler. Is there a nicer way? - Just n -> return n - -storeResults :: Updates -> ModGuts -> CoreM ModGuts -storeResults = flip (foldM (flip (uncurry go))) - where - go :: Name -> Result -> ModGuts -> CoreM ModGuts - go name res guts = do - e <- resultToExpr res - pure $ updateNameInGuts name e guts - -dcExpr :: TH.Name -> CoreM CoreExpr -dcExpr thn = do - name <- fromTHName thn - dc <- lookupDataCon name - pure $ Var (dataConWrapId dc) - -resultToExpr :: Result -> CoreM CoreExpr -resultToExpr (Success s) = App <$> dcExpr 'Success <*> mkStringExpr s -resultToExpr (Failure s) = App <$> dcExpr 'Failure <*> mkStringExpr s - -proofPass :: UponFailure -> ReportingMode -> ModGuts -> CoreM ModGuts -proofPass upon_failure report guts = do - case upon_failure of - SkipO0 -> pure guts - _ -> do - let (guts', obligations) = extractObligations guts - (toStore, stats) <- (concat `bimap` M.unionsWith (+)) . unzip <$> - mapM (checkObligation report guts') obligations - let n = sum stats :: Int - - guts'' <- storeResults toStore guts' - - let q :: Stat -> Int - q s = fromMaybe 0 $ M.lookup s stats - - let summary_message = nest 2 $ - vcat [ nest 2 (desc s) Outputable.<> colon <+> ppr (q s) - | s <- [minBound..maxBound], q s > 0 ] - - -- Only print a message if there are some compile-time results to report - unless (q StoredResult == n) $ do - if q ExpSuccess + q ExpFailure + q StoredResult == n - then unless (report == Quiet) $ - putMsg $ text "inspection testing successful" $$ summary_message - else do - errorMsg $ text "inspection testing unsuccessful" $$ summary_message - case upon_failure of - KeepGoing -> return () - _ -> liftIO $ exitFailure -- kill the compiler. Is there a nicer way? - - return guts'' - - -desc :: Stat -> SDoc -desc ExpSuccess = text " expected successes" -desc UnexpSuccess = text "unexpected successes" -desc ExpFailure = text " expected failures" -desc UnexpFailure = text " unexpected failures" -desc StoredResult = text " results stored" - -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) - ] +-- | See "Test.Inspection". +-- +{-# LANGUAGE CPP #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE LambdaCase #-} +module Test.Inspection.Plugin + ( plugin + , checkProperty + , CheckResult(..) + , prettyProperty + ) where + +import Control.Monad +import System.Exit +import Data.Either +import Data.Maybe +import Data.Bifunctor +import Data.List +import qualified Data.Map.Strict as M +import qualified Language.Haskell.TH.Syntax as TH + +#if MIN_VERSION_ghc(9,4,0) +import GHC.Types.Error +import GHC.Driver.Session +#endif + +#if MIN_VERSION_ghc(9,0,0) +import GHC.Plugins hiding (SrcLoc) +import GHC.Utils.Outputable as Outputable +#else +import GhcPlugins hiding (SrcLoc) +import Outputable +#endif + +#if MIN_VERSION_ghc(9,2,0) +import GHC.Types.TyThing +#endif + +import Test.Inspection (Obligation(..), Equivalence (..), Property(..), Result(..)) +import Test.Inspection.Core + +-- | The plugin. It supports some options: +-- +-- * @-fplugin-opt=Test.Inspection.Plugin:keep-going@ to keep building despite failing obligations +-- * @-fplugin-opt=Test.Inspection.Plugin:keep-going-O0@ to keep building despite failing obligations, when optimisations are off +-- * @-fplugin-opt=Test.Inspection.Plugin:skip-O0@ to skip performing inspections when optimisations are off +-- * @-fplugin-opt=Test.Inspection.Plugin:quiet@ to be silent if all obligations are fulfilled +-- +-- It makes sense to enable only one of @keep-going@, @keep-going-O0@ and +-- @skip-O0@ at a time. @skip-O0@ is useful when working with GHCi, to suppress +-- inspection failure messages and eliminate the overhead of inspection when +-- loading. + + +plugin :: Plugin +plugin = defaultPlugin + { installCoreToDos = install +#if __GLASGOW_HASKELL__ >= 806 + , pluginRecompile = \_args -> pure NoForceRecompile +#endif + } + +data UponFailure = AbortCompilation | KeepGoingO0 | SkipO0 | KeepGoing deriving Eq + +data ReportingMode = Verbose | Quiet deriving Eq + +data ResultTarget = PrintAndAbort | StoreAt Name + +install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo] +install args passes = return $ passes ++ [pass] + where + pass = CoreDoPluginPass "Test.Inspection.Plugin" (proofPass upon_failure report) + upon_failure | "keep-going" `elem` args = KeepGoing + | "keep-going-O0" `elem` args = KeepGoingO0 + | "skip-O0" `elem` args = SkipO0 + | otherwise = AbortCompilation + report | "quiet" `elem` args = Quiet + | otherwise = Verbose + +extractObligations :: ModGuts -> (ModGuts, [(ResultTarget, Obligation)]) +extractObligations guts = (guts', obligations) + where + (anns_clean, obligations) = partitionMaybe findObligationAnn (mg_anns guts) + guts' = guts { mg_anns = anns_clean } + +findObligationAnn :: Annotation -> Maybe (ResultTarget, Obligation) +findObligationAnn (Annotation (ModuleTarget _) payload) + | Just obl <- fromSerialized deserializeWithData payload + = Just (PrintAndAbort, obl) +findObligationAnn (Annotation (NamedTarget n) payload) + | Just obl <- fromSerialized deserializeWithData payload + = Just (StoreAt n, obl) +findObligationAnn _ + = Nothing + +prettyObligation :: Module -> Obligation -> String -> String +prettyObligation mod (Obligation {..}) result = + maybe "" myPrettySrcLoc srcLoc ++ ": " ++ name ++ " " ++ result + where + name = case testName of + Just n -> n + Nothing -> prettyProperty (showTHName mod) target property + +prettyProperty :: (TH.Name -> String) -> TH.Name -> Property -> String +prettyProperty showName target = \case + EqualTo n2 eqv -> showName target ++ " " ++ showEquiv eqv ++ " " ++ showName n2 + NoTypes [t] -> showName target ++ " `hasNoType` " ++ showName t + NoTypes ts -> showName target ++ " mentions none of " ++ intercalate ", " (map showName ts) + NoAllocation -> showName target ++ " does not allocate" + NoTypeClasses [] -> showName target ++ " does not contain dictionary values" + NoTypeClasses ts -> showName target ++ " does not contain dictionary values except of " ++ intercalate ", " (map showName ts) + NoUseOf ns -> showName target ++ " uses none of " ++ intercalate ", " (map showName ns) + CoreOf -> showName target ++ " core dump" -- :) + where + showEquiv StrictEquiv = "===" + showEquiv IgnoreTypesAndTicksEquiv = "==-" + showEquiv UnorderedLetsEquiv = "==~" + +-- | 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 + +data Stat = ExpSuccess | ExpFailure | UnexpSuccess | UnexpFailure | StoredResult + deriving (Enum, Eq, Ord, Bounded) +type Stats = M.Map Stat Int + +type Updates = [(Name, Result)] + +tick :: Stat -> Stats +tick s = M.singleton s 1 + +checkObligation :: ReportingMode -> ModGuts -> (ResultTarget, Obligation) -> CoreM (Updates, Stats) +checkObligation report guts (reportTarget, obl) = do + + res <- checkProperty guts (target obl) (property obl) + case reportTarget of + PrintAndAbort -> do + category <- case (res, expectFail obl) of + -- Property holds + (ResSuccess, False) -> do + unless (report == Quiet) $ + putMsgS $ prettyObligation (mg_module guts) obl expSuccess + return ExpSuccess + (ResSuccess, True) -> do + putMsgS $ prettyObligation (mg_module guts) obl unexpSuccess + return UnexpSuccess + -- Property holds, with extra message + (ResSuccessWithMessage reportDoc, False) -> do + unless (report == Quiet) $ do + putMsgS $ prettyObligation (mg_module guts) obl expSuccess + putMsg reportDoc + return ExpSuccess + (ResSuccessWithMessage reportDoc, True) -> do + putMsgS $ prettyObligation (mg_module guts) obl unexpSuccess + putMsg reportDoc + return UnexpSuccess + -- Property does not hold + (ResFailure reportDoc, False) -> do + putMsgS $ prettyObligation (mg_module guts) obl unexpFailure + putMsg $ reportDoc + return UnexpFailure + (ResFailure _, True) -> do + unless (report == Quiet) $ + putMsgS $ prettyObligation (mg_module guts) obl expFailure + return ExpFailure + return ([], tick category) + StoreAt name -> do + dflags <- getDynFlags + let result = case res of + ResSuccess -> Success $ showSDoc dflags $ + text (prettyObligation (mg_module guts) obl expSuccess) + ResSuccessWithMessage msg -> Success $ showSDoc dflags $ + text (prettyObligation (mg_module guts) obl expSuccess) $$ + msg + ResFailure reportMsg -> Failure $ showSDoc dflags $ + text (prettyObligation (mg_module guts) obl unexpFailure) $$ + reportMsg + pure ([(name, result)], tick StoredResult) + + where + expSuccess = "passed." + unexpSuccess = "passed unexpectedly!" + unexpFailure = "failed:" + expFailure = "failed expectedly." + + +data CheckResult + = ResSuccess + | ResSuccessWithMessage SDoc + | ResFailure SDoc + +lookupNameInGuts :: ModGuts -> Name -> Maybe (Var, CoreExpr) +lookupNameInGuts guts n = listToMaybe + [ (v,e) + | (v,e) <- flattenBinds (mg_binds guts) + , getName v == n + ] + +updateNameInGuts :: Name -> CoreExpr -> ModGuts -> ModGuts +updateNameInGuts n expr guts = + guts {mg_binds = map (updateNameInGut n expr) (mg_binds guts) } + +updateNameInGut :: Name -> CoreExpr -> CoreBind -> CoreBind +updateNameInGut n e (NonRec v _) | getName v == n = NonRec v e +updateNameInGut _ _ bind = bind + +checkProperty :: ModGuts -> TH.Name -> Property -> CoreM CheckResult +checkProperty guts thn1 (EqualTo thn2 ignore_types) = do + n1 <- fromTHName thn1 + n2 <- fromTHName thn2 + + let p1 = lookupNameInGuts guts n1 + let p2 = lookupNameInGuts guts n2 + + if | n1 == n2 + -> pure ResSuccess + -- Ok if one points to another + | Just (_, Var other) <- p1, getName other == n2 + -> pure ResSuccess + | Just (_, Var other) <- p2, getName other == n1 + -> pure ResSuccess + | Just (v1, _) <- p1 + , Just (v2, _) <- p2 + , let slice1 = slice binds v1 + , let slice2 = slice binds v2 + -> case eqSlice' ignore_types slice1 slice2 of + -- OK if they have the same expression + Right _ -> pure ResSuccess + -- Not ok if the expression differ + Left err -> pure . ResFailure $ err $$ pprSliceDifference slice1 slice2 + -- Not ok if both names are bound externally + | Nothing <- p1 + , Nothing <- p2 + -> pure . ResFailure $ ppr n1 <+> text " and " <+> ppr n2 <+> + text "are different external names" + | Nothing <- p1 + -> pure . ResFailure $ ppr n1 <+> text "is an external name" + | Nothing <- p2 + -> pure . ResFailure $ ppr n2 <+> text "is an external name" + where + binds = flattenBinds (mg_binds guts) + +checkProperty guts thn (NoUseOf thns) = do + n <- fromTHName thn + ns <- mapM fromTHName thns + case lookupNameInGuts guts n of + Nothing -> pure . ResFailure $ ppr n <+> text "is not a local name" + Just (v, _) -> case freeOfTerm (slice binds v) ns of + Just _ -> pure . ResFailure $ pprSlice (slice binds v) + Nothing -> pure ResSuccess + where binds = flattenBinds (mg_binds guts) + +checkProperty guts thn (NoTypes thts) = do + n <- fromTHName thn + ts <- mapM fromTHName thts + case lookupNameInGuts guts n of + Nothing -> pure . ResFailure $ ppr n <+> text "is not a local name" + Just (v, _) -> case freeOfType (slice binds v) ts of + Just _ -> pure . ResFailure $ pprSlice (slice binds v) + Nothing -> pure ResSuccess + where binds = flattenBinds (mg_binds guts) + +checkProperty guts thn NoAllocation = do + n <- fromTHName thn + case lookupNameInGuts guts n of + Nothing -> pure . ResFailure $ ppr n <+> text "is not a local name" + Just (v, _) -> case doesNotAllocate (slice binds v) of + Just (v',e') -> pure . ResFailure $ nest 4 (ppr v' <+> text "=" <+> ppr e') + Nothing -> pure ResSuccess + where binds = flattenBinds (mg_binds guts) + +checkProperty guts thn (NoTypeClasses thts) = do + n <- fromTHName thn + ts <- mapM fromTHName thts + case lookupNameInGuts guts n of + Nothing -> pure . ResFailure $ ppr n <+> text "is not a local name" + Just (v, _) -> case doesNotContainTypeClasses (slice binds v) ts of + Just (v',e',tc) -> pure . ResFailure + $ nest 4 $ vcat + [ text "Found type classes: " <+> ppr tc + , ppr v' <+> text "=" <+> ppr e' + ] + Nothing -> pure ResSuccess + where binds = flattenBinds (mg_binds guts) + +checkProperty guts thn CoreOf = do + n <- fromTHName thn + case lookupNameInGuts guts n of + Nothing -> pure . ResFailure $ ppr n <+> text "is not a local name" + Just (v, _) -> do + let s = slice binds v + pure $ ResSuccessWithMessage $ nest 4 $ pprSlice s + where binds = flattenBinds (mg_binds guts) + +fromTHName :: TH.Name -> CoreM Name +fromTHName thn = thNameToGhcName thn >>= \case + Nothing -> do + errorMsg $ text "Could not resolve TH name" <+> text (show thn) + liftIO $ exitFailure -- kill the compiler. Is there a nicer way? + Just n -> return n + +storeResults :: Updates -> ModGuts -> CoreM ModGuts +storeResults = flip (foldM (flip (uncurry go))) + where + go :: Name -> Result -> ModGuts -> CoreM ModGuts + go name res guts = do + e <- resultToExpr res + pure $ updateNameInGuts name e guts + +dcExpr :: TH.Name -> CoreM CoreExpr +dcExpr thn = do + name <- fromTHName thn + dc <- lookupDataCon name + pure $ Var (dataConWrapId dc) + +resultToExpr :: Result -> CoreM CoreExpr +resultToExpr (Success s) = App <$> dcExpr 'Success <*> mkStringExpr s +resultToExpr (Failure s) = App <$> dcExpr 'Failure <*> mkStringExpr s + +proofPass :: UponFailure -> ReportingMode -> ModGuts -> CoreM ModGuts +proofPass upon_failure report guts = do + case upon_failure of + SkipO0 -> pure guts + _ -> do + let (guts', obligations) = extractObligations guts + (toStore, stats) <- (concat `bimap` M.unionsWith (+)) . unzip <$> + mapM (checkObligation report guts') obligations + let n = sum stats :: Int + + guts'' <- storeResults toStore guts' + + let q :: Stat -> Int + q s = fromMaybe 0 $ M.lookup s stats + + let summary_message = nest 2 $ + vcat [ nest 2 (desc s) Outputable.<> colon <+> ppr (q s) + | s <- [minBound..maxBound], q s > 0 ] + + -- Only print a message if there are some compile-time results to report + unless (q StoredResult == n) $ do + if q ExpSuccess + q ExpFailure + q StoredResult == n + then unless (report == Quiet) $ + putMsg $ text "inspection testing successful" $$ summary_message + else do + errorMsg $ text "inspection testing unsuccessful" $$ summary_message + case upon_failure of + KeepGoing -> return () + _ -> liftIO $ exitFailure -- kill the compiler. Is there a nicer way? + + return guts'' + + +desc :: Stat -> SDoc +desc ExpSuccess = text " expected successes" +desc UnexpSuccess = text "unexpected successes" +desc ExpFailure = text " expected failures" +desc UnexpFailure = text " unexpected failures" +desc StoredResult = text " results stored" + +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) + ]