ghc-proofs (empty) → 0.1
raw patch · 9 files changed
+1479/−0 lines, 9 filesdep +basedep +ghcdep +ghc-proofssetup-changed
Dependencies added: base, ghc, ghc-proofs, transformers
Files
- ChangeLog.md +9/−0
- GHC/Proof.hs +98/−0
- GHC/Proof/Plugin.hs +178/−0
- LICENSE +20/−0
- README.md +246/−0
- Setup.hs +2/−0
- examples/HLint.hs +758/−0
- examples/Successors.hs +110/−0
- ghc-proofs.cabal +58/−0
+ ChangeLog.md view
@@ -0,0 +1,9 @@+# Revision history for ghc-proofs++## 0.1 -- 2017-08-26++* Initial release to hackage++## 0 -- 2017-02-06++* Development commences
+ GHC/Proof.hs view
@@ -0,0 +1,98 @@+-- |+-- Description : Let GHC prove program equations+-- Copyright : (c) Joachim Breitner, 2017+-- License : MIT+-- Maintainer : mail@joachim-breitner.de+-- Portability : GHC specifc+--+-- This module supports the accompanying GHC plugin "GHC.Proof.Plugin" and adds+-- to GHC the ability to verify simple program equations.+--+-- = Synopis+--+-- Consider this module:+--+-- > {-# OPTIONS_GHC -O -fplugin GHC.Proof.Plugin #-}+-- > module Simple where+-- >+-- > import GHC.Proof+-- > import Data.Maybe+-- >+-- > my_proof1 :: (a -> b) -> Maybe a -> Proof+-- > my_proof1 f x = isNothing (fmap f x)+-- > === isNothing x+-- >+-- > my_proof2 :: a -> Maybe a -> Proof+-- > my_proof2 d x = fromMaybe d x+-- > === maybe d id x+--+-- Compiling it will result in this output:+--+-- > $ ghc Simple.hs+-- > [1 of 1] Compiling Simple ( Simple.hs, Simple.o )+-- > GHC.Proof: Proving my_proof1 …+-- > GHC.Proof: Proving my_proof2 …+-- > GHC.Proof proved 2 equalities+--+-- = Usage+--+-- To use this plugin, you have to+--+-- * Make sure you load the plugin @GHC.Proof.Plugin@, either by passing+-- @-fplugin GHC.Proof.Plugin@ to GHC or, more conveniently, using the+-- @OPTIONS_GHC@ pragma as above.+--+-- * Import the @GHC.Proof@ module.+--+-- * Define proof obligations using the 'proof' function or, equilvalently, the+-- '===' operator. Type signatures are optional.+--+-- These proof obligation must occur direclty on the+-- right-hand side of a top-level definition, where all parameters (if any)+-- are plain variables. For example, this would (currently) not work:+--+-- > not_good (f,x) = isNothing (fmap f x) === isNothing x+--+-- If your module has an explicit export list, then these functions need to+-- be exported (otherwise the compiler deletes them too quickly).+--+-- * Compile. If all proof obligations can be proven, compilation continues as+-- usual; otherwise it aborts.+--+-- = What can I prove this way?+--+-- Who knows... but generally you can only expect interesting results when you+-- use functions that are either non-recursive, or have an extensive rewrite+-- rule setup (such as lists). See the @examples/@ directory for some examples+-- of what works.+module GHC.Proof where++-- | A dummy data type, to give 'proof' a nicely readable type signature.+data Proof = Proof++-- | Instructs the compiler to see if it can prove the two arguments to 'proof'+-- to be equivalent.+proof :: a -> a -> Proof+proof _ _ = Proof+{-# INLINE [0] proof #-}++-- | Infix operator for 'proof'.+(===) :: a -> a -> Proof+(===) = proof+infix 0 ===++-- | Instructs the compiler to try to prove the two arguments to 'proof'+-- to be equivalent, but do not abort if it fails.+--+-- This is useful to document equalities that you would like to be proven, but+-- where @ghc-proofs@ does not work well enough.+non_proof :: a -> a -> Proof+non_proof _ _ = Proof+{-# INLINE [0] non_proof #-}++-- | Infix operator for 'non_proof'.+(=/=) :: a -> a -> Proof+(=/=) = non_proof+infix 0 =/=++
+ GHC/Proof/Plugin.hs view
@@ -0,0 +1,178 @@+-- | See "GHC.Proof".+{-# LANGUAGE CPP #-}+module GHC.Proof.Plugin (plugin) where++import Data.Maybe+import Control.Monad+import System.Exit++import GhcPlugins+import Simplify+import CoreStats+import CoreMonad+import SimplMonad+import OccurAnal+import FamInstEnv+import SimplEnv+import CSE++-- import GHC.Proof++plugin :: Plugin+plugin = defaultPlugin { installCoreToDos = install }++install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]+install _ (simpl:xs) = return $ simpl: myOccurPass : pass : xs+ where pass = CoreDoPluginPass "GHC.Proof" proofPass+ myOccurPass = CoreDoPluginPass "GHC.Proof Occur" occurPass+++type Task = (SDoc, Bool, [CoreBndr], CoreExpr, CoreExpr)++findProofTasks :: ModGuts -> CoreM [Task]+findProofTasks guts = return $ mapMaybe findProofTask (mg_binds guts)+++findProofTask :: CoreBind -> Maybe Task+findProofTask (NonRec name e)+ | (bndrs, body) <- collectBinders e+ , (Var v `App` Type _ `App` e1 `App` e2) <- body+ , isProof (idName v)+ = Just (ppr name, True, bndrs, e1,e2)+findProofTask (NonRec name e)+ | (bndrs, body) <- collectBinders e+ , (Var v `App` Type _ `App` e1 `App` e2) <- body+ , isNonProof (idName v)+ = Just (ppr name, False, bndrs, e1,e2)+findProofTask _ = Nothing+++isProof :: Name -> Bool+isProof n =+ occNameString oN == "proof" &&+ moduleNameString (moduleName (nameModule n)) == "GHC.Proof"+ || occNameString oN == "===" &&+ moduleNameString (moduleName (nameModule n)) == "GHC.Proof"+ where oN = occName n++isNonProof :: Name -> Bool+isNonProof n =+ occNameString oN == "non_proof" &&+ moduleNameString (moduleName (nameModule n)) == "GHC.Proof"+ || occNameString oN == "=/=" &&+ moduleNameString (moduleName (nameModule n)) == "GHC.Proof"+ where oN = occName n+++proveTask :: ModGuts -> Task -> CoreM Bool+proveTask guts (name, really, bndrs, e1, e2) = do+ if really+ then putMsg (text "GHC.Proof: Proving" <+> name <+> text "…")+ else putMsg (text "GHC.Proof: Not proving" <+> name <+> text "…")++ se1 <- simplify guts bndrs e1+ se2 <- simplify guts bndrs e2+ let differences = diffExpr False (mkRnEnv2 emptyInScopeSet) se1 se2++ if really+ then+ if null differences+ then return True+ else do+ putMsg $+ text "Proof failed" $$+ nest 4 (hang (text "Simplified LHS" <> colon) 4 (ppr se1)) $$+ nest 4 (hang (text "Simplified RHS" <> colon) 4 (ppr se2))+ -- nest 4 (text "Differences:") $$+ -- nest 4 (itemize differences)+ return False+ else+ if null differences+ then do+ putMsg $ text "Proof succeeded unexpectedly"+ return False+ else do+ return True++itemize :: [SDoc] -> SDoc+itemize = vcat . map (char '•' <+>)++simplify :: ModGuts -> [Var] -> CoreExpr -> CoreM CoreExpr+simplify guts more_in_scope expr = do+ dflags <- getDynFlags++#if __GLASGOW_HASKELL__ >= 801+ let dflags' = dflags { ufUseThreshold = 1000, ufVeryAggressive = True } --yeeha!+#else+ let dflags' = dflags { ufUseThreshold = 1000 }+#endif+ us <- liftIO $ mkSplitUniqSupply 's'+ let sz = exprSize expr++ hpt_rule_base <- getRuleBase+ hsc_env <- getHscEnv+ eps <- liftIO $ hscEPS hsc_env+ let rule_base1 = unionRuleBase hpt_rule_base (eps_rule_base eps)+ rule_base2 = extendRuleBaseList rule_base1 (mg_rules guts)+ vis_orphs <- getVisibleOrphanMods+ let rule_env = RuleEnv rule_base2 vis_orphs+ let in_scope = bindersOfBinds (mg_binds guts) ++ more_in_scope++ (expr', _) <- liftIO $ initSmpl dflags' rule_env emptyFamInstEnvs us sz $ do+ return expr >>= simplExpr (simplEnv in_scope 4) . occurAnalyseExpr+ >>= simplExpr (simplEnv in_scope 4) . occurAnalyseExpr+ >>= simplExpr (simplEnv in_scope 3) . occurAnalyseExpr+ >>= simplExpr (simplEnv in_scope 3) . occurAnalyseExpr+ >>= simplExpr (simplEnv in_scope 2) . occurAnalyseExpr+ >>= simplExpr (simplEnv in_scope 2) . occurAnalyseExpr+ >>= simplExpr (simplEnv in_scope 2) . occurAnalyseExpr+ >>= simplExpr (simplEnv in_scope 1) . occurAnalyseExpr . cseOneExpr'+ >>= simplExpr (simplEnv in_scope 1) . occurAnalyseExpr . cseOneExpr'+ return expr'++#if __GLASGOW_HASKELL__ >= 801+cseOneExpr' = cseOneExpr+#else+cseOneExpr' = id+#endif++simplEnv :: [Var] -> Int -> SimplEnv+simplEnv vars p = env1+ where+ env1 = addNewInScopeIds env0 vars+ env0 = mkSimplEnv $ SimplMode { sm_names = ["GHC.Proof"]+ , sm_phase = Phase p+ , sm_rules = True+ , sm_inline = True+ , sm_eta_expand = True+ , sm_case_case = True }++proofPass :: ModGuts -> CoreM ModGuts+proofPass guts = do++ dflags <- getDynFlags+ when (optLevel dflags < 1) $+ warnMsg $ fsep $ map text $ words "GHC.Proof: Compilation without -O detected. Expect proofs to fail."+++ tasks <- findProofTasks guts+ ok <- and <$> mapM (proveTask guts) tasks+ if ok+ then do+ let n = length [ () | (_, True, _, _, _) <- tasks ]+ let m = length [ () | (_, False, _, _, _) <- tasks ]+ putMsg $ text "GHC.Proof proved" <+> ppr n <+> text "equalities"+ return guts+ else do+ errorMsg $ text "GHC.Proof could not prove all equalities"+ liftIO $ exitFailure -- kill the compiler. Is there a nicer way?++occurPass :: PluginPass+occurPass mg@(ModGuts { mg_module = this_mod+ , mg_rdr_env = rdr_env+ , mg_deps = deps+ , mg_binds = binds, mg_rules = rules+ , mg_fam_inst_env = fam_inst_env })+ = do let binds' = occurAnalysePgm this_mod (const True) rules [] emptyVarSet binds+ return mg+
+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2017 Joachim Breitner++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ README.md view
@@ -0,0 +1,246 @@+Prove program equations with GHC+================================++This GHC plugin allows you to embed code equation into your code, and have them+checked by GHC.++Synopsis+--------++See the `GHC.Proof` module for the documentation, but there really isn't much+more to it than:++```haskell+{-# OPTIONS_GHC -O -fplugin GHC.Proof.Plugin #-}+module Simple where++import GHC.Proof+import Data.Maybe++my_proof1 = (\f x -> isNothing (fmap f x))+ === (\f x -> isNothing x)+```++If you compile this, you will reassurringly read:++```+$ ghc Simple.hs+[1 of 1] Compiling Simple ( Simple.hs, Simple.o )+GHC.Proof: Proving my_proof1 …+GHC.Proof proved 1 equalities+```++See the [`examples/`](examples/) directory for more examples of working proofs+(with GHC HEAD).++If you have proof that GHC cannot prove, for example++```haskell+not_a_proof = (2+2::Int) === (5::Int)+```++then the compiler will tell you so, and abort the compilation:+```+$ ghc Simple.hs+[1 of 1] Compiling Simple ( Simple.hs, Simple.o )+GHC.Proof: Proving not_a_proof …+Proof failed+ Simplified LHS: GHC.Types.I# 4#+ Simplified RHS: GHC.Types.I# 5#+ Differences:+ • 4# /= 5#++Simple.hs: error: GHC.Proof could not prove all equalities+```++How does it work?+-----------------++GHC is a mighty optimizing compiler, and the centerpiece of optimizing, the+*simplifier* is capable of quite a bit of symbolic execution. We can use this+to prove program equalities, simply by taking two expressions, letting GHC+simplify them as far as possible. If the resulting expressions are the same,+then the original expressions are – as far as the compiler is concerned –+identicial.++The GHC simplifier works on the level of the intermediate language GHC Core,+and failed proofs will be reported as such.++The gory details are as follows: The simplifier is run 8 times, twice for each+of the simplifier phases 4, 3, 2 and 1. In between, the *occurrence analiser*+is run. Near the end, we also run *common-subexpression elimination*.++The simplifier is run with more aggressive flags. In particular, it is+instructed to inline functions aggressively and without worrying about code+size.+++Why is this so great?+---------------------++ * You can annotate your code with proofs, in the same file, in the same+ language, without extra tools (besides the plugin).+ * The proofs stay with the code and are run with every compilation.+ * The proof goes through when *the compiler* thinks the expressions are the+ same. There is no worry about whether an external proof tools captures the+ semantics of GHC’s Haskell precisely.+ * It suports, in principle, all of Haskell’s syntax, including a huge number+ of extensions.+ * It is super easy (if it works).+ * Using rewrite rules allows proofs with regard to some theory (e.g. with+ regard to equations about `foldr` and other list combinators), independent+ of whether these are proven.++Why is this not so great?+--------------------++ * It can only prove quite simple things right now.+ * Even for easy things, the proof might fail because GHC simply simplifies the+ expressions slightly different, and there is not always an easy way of+ fixing this.+ * The proofs depend on optimization flags.+ * There is no guarantee that the next GHC release will be able to prove the+ same things.+ * Failed proofs are reported in GHC Core instead of Haskell.+ * At least currently, it more or less requires GHC HEAD (it compiles with+ GHC-8.0, but it has less control over the simplifier and less proofs will go+ through.)++What can it prove?+------------------++Not everything. By far.++But some nice, practical results work, see for example the+[proofs of the `Applicative` and `Monad` laws for `Control.Applicative.Succs`](examples/Successors.hs).++Best results were observed with compositions of non-recursive+functions that handle non-recursive data or handle lists usind standard list+combinators.++The GHC simplifier generally refuses to inline recursive functions, so there is+not much we can do with these for now.++My proof is not found. What can I do?+-------------------------------------++The plugin searches for top-level bindings of the form+```haskell+somename = proof expression1 expression2+```+or+```haskell+somename = expression1 === expression2+```++GHC will drop them before the plugin sees them, though, if `somename` is not+exported, so make sure it is exported. If you really do not want to export it, then you can keep it alive using the trick of+```haskell+{-# RULES "keep somename alive" id somename = somename #-}+```++If it still does not work, check the output of `-dverbose-core2core` for why+your binding does not have the expected form. Maybe you can fix it somehow.++My proof does not go through. Can I fix that?+---------------------------------------------++Maybe. Here are some tricks that sometimes help:++ * Check if your functions are properly unfolded in the proof. Maybe an+ `INLINEABLE` pragma helps.++ * Use `{-# LANGUAGE BangPatterns #-}` and mark some arguments as strict:++ ```haskell+ my_proof2 = (\d !x -> fromMaybe d x)+ === (\d !x -> maybe d id x)+ ```++ GHC makes these functions strict by putting the body in a case. This has+ roughly the same effect as s *case split* in interactive theorem proving.++ * Allow GHC to assume one of your functions is strict:++ ```haskell+ str :: (a -> b) -> (a -> b)+ str f x = x `seq` f x++ monad_law_3 = (\ (x::Succs a) k h -> x >>= (\x -> k x >>= str h))+ === (\ (x::Succs a) k h -> (x >>= k) >>= str h)+ ```++ * Instead of using recursion, try to use combinators (e.g. `filter`, `map`, `++` etc.).++ * Add rewrite rules to tell GHC about some program equations that it should+ use while simplifying. This is in particular useful when working with list functions++ Here are some examples:+ ```haskell+ {-# RULES "mapFB/id" forall c . mapFB c (\x -> x) = c #-}+ {-# RULES "foldr/nil" forall k n . GHC.Base.foldr k n [] = n #-}+ {-# RULES "foldr/mapFB" forall c f g n1 n2 xs.+ GHC.Base.foldr (mapFB c f) n1 (GHC.Base.foldr (mapFB (:) g) n2 xs)+ = GHC.Base.foldr (mapFB c (f.g)) (GHC.Base.foldr (mapFB c f) n1 n2) xs+ #-}+ ```++ But note that these apply to your whole module, and are exported from it, so you+ should not attempt to add such a rule to the same module where you prove+ the rule. And if you don’t want these rules to be applied in normal code,+ put your proofs into a separate `Proof` module that is never imported.+++Shall I use this in production?+-------------------------------++You can try. It certainly does not hurt, and proofs that go through are fine.+It might not prove enough to be really useful.++What next?+----------++It remains to be seen how useful this approach really is, and what can be done+to make it more useful. So we need to start proving some things.++Here are some aspects that likely need to be improved:++ * The user should be put into control of some of the simplifier settings.+ Depending on the proof, one might want to go through more or less of the+ simplifier phases, or disable and enable certain rules.++ * Maybe a syntax that does not abuse term-level bindings can be introduced.+ Currently, though, this is not possible for a plugin.++ * If deemed useful, this functionaly maybe can become part of GHC, and the+ simplifier could get a few extra knobs to turn.++ * A custom function to compare expressions that relates more than just+ alpha-equivalence could expand the scope of this plugin.++ * The reporting of failed proofs can be improved.++ * Come up with a better story about recursive functions.++How else can I prove things about Haskell?+------------------------------------------++ * Wait for full dependent types in Haskell and express your equivalences as+ types.+ * Manually or mechanically (e.g. using [Haskabelle](https://isabelle.in.tum.de/haskabelle.html)) rewrite your code in a+ theorem prover such as [Isabelle](http://isabelle.in.tum.de/),+ [Agda](http://wiki.portal.chalmers.se/agda/pmwiki.php) or+ [Coq](https://coq.inria.fr/), and prove stuff there.+ * Write your code in these theorem provers in the first place and export them+ to Haskell.+ * You might be able to prove a few things using+ [Liquid Haskell](https://ucsd-progsys.github.io/liquidhaskell-blog/) or,+ actually quite similar to this, [HERMIT](http://ku-fpg.github.io/software/hermit/).+++Can I comment or help?+----------------------++Sure! We can use the GitHub issue tracker for discussions, and obviously+contributions are welcome.+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ examples/HLint.hs view
@@ -0,0 +1,758 @@+{-# LANGUAGE BangPatterns, ScopedTypeVariables, AllowAmbiguousTypes #-}+{-# OPTIONS_GHC -O -fplugin GHC.Proof.Plugin #-}++-- This modules explores which rules from hlint-1.9.41 we can prove with+-- the GHC.Proof plugin.+--+-- Those with === are proved. Those with =/= not yet.+module HLint where++import GHC.Proof++import Control.Arrow+import Control.Exception+import Control.Monad+import Control.Monad.Trans.State+import qualified Data.Foldable+import Data.Foldable(asum, sequenceA_, traverse_, for_)+import Data.Traversable(traverse, for)+import Control.Applicative+import Data.Function+import Data.Int+import Data.Char+import Data.List as Data.List+import Data.List as X+import Data.Maybe+import Data.Monoid+import System.IO+import Control.Concurrent.Chan+import System.Mem.Weak+import Control.Exception.Base+import System.Exit+import Data.Either+import Numeric++-- I/O++-- warn = putStrLn (show x) ==> print x+proof1 x = putStrLn (show x) === print x++-- warn = mapM_ putChar ==> putStr+proof2 = mapM_ putChar =/= putStr++-- warn = hGetChar stdin ==> getChar+proof3 = hGetChar stdin === getChar++-- warn = hGetLine stdin ==> getLine+proof4 = hGetLine stdin === getLine++-- warn = hGetContents stdin ==> getContents+proof5 = hGetContents stdin === getContents++-- warn = hPutChar stdout ==> putChar+proof6 = hPutChar stdout =/= putChar++-- warn = hPutStr stdout ==> putStr+proof7 = hPutStr stdout =/= putStr++-- warn = hPutStrLn stdout ==> putStrLn+proof8 = hPutStrLn stdout =/= putStrLn++-- warn = hPrint stdout ==> print+proof9 :: forall x. Show x => Proof+proof9 = (hPrint stdout :: x -> IO ()) === print++-- warn = hWaitForInput a 0 ==> hReady a+proof10 a = hWaitForInput a 0 === hReady a++-- warn = hPutStrLn a (show b) ==> hPrint a b+proof11 a b = hPutStrLn a (show b) === hPrint a b++-- warn = hIsEOF stdin ==> isEOF+proof12 = hIsEOF stdin === isEOF++-- -- EXIT++-- warn = exitWith ExitSuccess ==> exitSuccess+proof13 = exitWith ExitSuccess === exitSuccess++-- -- ORD++-- warn = not (a == b) ==> a /= b where note = "incorrect if either value is NaN"+proof14a a (b::Bool) = not (a == b) === (a /= b)+proof14b a (b::Int) = not (a == b) =/= (a /= b)+proof14c a b = not (a == b) =/= (a /= b)++-- warn = not (a /= b) ==> a == b where note = "incorrect if either value is NaN"+proof15 a (b::Bool) = not (a /= b) === (a == b)++-- warn = not (a > b) ==> a <= b where note = "incorrect if either value is NaN"+proof16 a (b::Bool) = not (a > b) === (a <= b)++-- warn = not (a >= b) ==> a < b where note = "incorrect if either value is NaN"+proof17 a (b::Bool) = not (a >= b) === (a < b)++-- warn = not (a < b) ==> a >= b where note = "incorrect if either value is NaN"+proof18 a (b::Bool) = not (a < b) === (a >= b)++-- warn = not (a <= b) ==> a > b where note = "incorrect if either value is NaN"+proof19 a (b::Bool) = not (a <= b) === (a > b)++-- warn = compare x y /= GT ==> x <= y+-- warn = compare x y == LT ==> x < y+-- warn = compare x y /= LT ==> x >= y+-- warn = compare x y == GT ==> x > y+-- warn = compare x y == EQ ==> x == y+-- warn = compare x y /= EQ ==> x /= y+-- --warning = x == a || x == b || x == c ==> x `elem` [a,b,c] where note = ValidInstance "Eq" x+-- --warning = x /= a && x /= b && x /= c ==> x `notElem` [a,b,c] where note = ValidInstance "Eq" x+-- --warn = compare (f x) (f y) ==> Data.Ord.comparing f x y -- not that great+-- --warn = on compare f ==> Data.Ord.comparing f -- not that great+-- warn = head (sort x) ==> minimum x+-- warn = last (sort x) ==> maximum x+-- warn = head (sortBy f x) ==> minimumBy f x+-- where _ = isCompare f+-- warn = last (sortBy f x) ==> maximumBy f x+-- where _ = isCompare f+-- warn "Avoid reverse" = reverse (sort x) ==> sortBy (flip compare) x+-- warn "Avoid reverse" = reverse (sortBy f x) ==> sortBy (flip f) x+-- where _ = isCompare f+-- hint = flip (g `on` h) ==> flip g `on` h+proof20 g h = flip (g `on` h) === (flip g `on` h)+++-- hint = (f `on` g) `on` h ==> f `on` (g . h)+proof21 f g h = ((f `on` g) `on` h) === (f `on` (g.h))++++-- -- READ/SHOW++-- warn = showsPrec 0 x "" ==> show x+-- warn = readsPrec 0 ==> reads+-- warn = showsPrec 0 ==> shows+-- hint = showIntAtBase 16 intToDigit ==> showHex+-- hint = showIntAtBase 8 intToDigit ==> showOct++-- -- LIST++-- warn = concat (map f x) ==> concatMap f x+proof22 f x = concat (map f x) =/= concatMap f x++-- warn = concat (fmap f x) ==> concatMap f x+proof23 :: forall f. (Functor f, Foldable f) => Proof+proof23 = (\ f x -> concat (fmap f x)) =/= (\ f (x:: f a) -> concatMap f x)++-- hint = concat [a, b] ==> a ++ b+proof24 a b = concat [a, b] === (a ++ b)++-- hint "Use map once" = map f (map g x) ==> map (f . g) x+proof25 f g x = map f (map g x) === map (f . g) x++-- hint "Fuse concatMap/map" = concatMap f (map g x) ==> concatMap (f . g) x+proof26 f g x = concatMap f (map g x) =/= concatMap (f . g) x++-- hint = x !! 0 ==> head x+proof27 x = x !! 0 =/= head x++-- warn = take n (repeat x) ==> replicate n x+-- where _ = noQuickCheck -- takes too long+proof28 n x = take n (repeat x) === replicate n x++-- warn = map f (replicate n x) ==> replicate n (f x)+-- where _ = noQuickCheck -- takes too long+proof29 f n x = map f (replicate n x) =/= replicate n (f x)++-- warn = map f (repeat x) ==> repeat (f x)+-- where _ = noQuickCheck -- takes forever+proof30 f x = map f (repeat x) =/= repeat (f x)+ -- ^ works if we simplify all the way to phase 0!++-- warn = cycle [x] ==> repeat x+-- where _ = noQuickCheck -- takes forever+proof31 x = cycle [x] =/= repeat x++-- warn = head (reverse x) ==> last x+-- warn = head (drop n x) ==> x !! n where _ = isNat n+-- warn = reverse (tail (reverse x)) ==> init x where note = IncreasesLaziness+-- warn "Avoid reverse" = reverse (reverse x) ==> x where note = IncreasesLaziness+-- -- warn = take (length x - 1) x ==> init x -- not true for x == []+-- warn = isPrefixOf (reverse x) (reverse y) ==> isSuffixOf x y++-- warn = foldr (++) [] ==> concat+proof32 x = foldr (++) [] x === concat x++-- warn = foldr (++) "" ==> concat+proof33 x = foldr (++) "" x === concat x++-- warn = foldl (++) [] ==> concat where note = IncreasesLaziness+-- warn = foldl (++) "" ==> concat where note = IncreasesLaziness+-- warn = foldl f (head x) (tail x) ==> foldl1 f x+-- warn = foldr f (last x) (init x) ==> foldr1 f x+-- warn = span (not . p) ==> break p+proof34 p = span (not . p) =/= break p++-- warn = break (not . p) ==> span p+proof35 p = break (not . p) =/= span p++-- warn = (takeWhile p x, dropWhile p x) ==> span p x+proof36 p x = (takeWhile p x, dropWhile p x) =/= span p x++-- warn = fst (span p x) ==> takeWhile p x+proof37 p x = fst (span p x) =/= takeWhile p x++-- warn = snd (span p x) ==> dropWhile p x+proof38 p x = snd (span p x) =/= dropWhile p x++-- warn = fst (break p x) ==> takeWhile (not . p) x+proof39 p x = fst (break p x) =/= takeWhile (not . p) x++-- warn = snd (break p x) ==> dropWhile (not . p) x+proof40 p x = snd (break p x) =/= dropWhile (not . p) x++-- warn = concatMap (++ "\n") ==> unlines+proof41 = concatMap (++ "\n") =/= unlines++-- warn = map id ==> id+proof42 = map id =/= id++-- warn = concatMap id ==> concat+proof43 x = concatMap id x === concat x++-- warn = or (map p x) ==> any p x+proof44 p x = or (map p x) =/= any p x++-- warn = and (map p x) ==> all p x+proof45 p x = and (map p x) =/= all p x++-- warn = zipWith (,) ==> zip+proof46 = zipWith (,) =/= zip++-- warn = zipWith3 (,,) ==> zip3+proof47 = zipWith3 (,,) =/= zip3++-- hint = length x == 0 ==> null x where note = IncreasesLaziness+-- hint = x == [] ==> null x+proof48 x = (x `seq` x == []) =/= null x++-- hint "Use null" = length x /= 0 ==> not (null x) where note = IncreasesLaziness+-- hint "Use :" = (\x -> [x]) ==> (:[])+proof49 x = (\x -> [x]) === (:[])++-- warn = map (uncurry f) (zip x y) ==> zipWith f x y+proof50 f x y = map (uncurry f) (zip x y) =/= zipWith f x y++-- hint = map f (zip x y) ==> zipWith (curry f) x y where _ = isVar f+proof51 f x y = map f (zip x y) =/= zipWith (curry f) x y++-- warn = not (elem x y) ==> notElem x y+proof52 x y = not (elem x y) === notElem x y++-- hint = foldr f z (map g x) ==> foldr (f . g) z x+proof53 f z g x = foldr f z (map g x) =/= foldr (f . g) z x++-- warn = x ++ concatMap (' ':) y ==> unwords (x:y)+proof54 x y = x ++ concatMap (' ':) y =/= unwords (x:y)++-- warn = intercalate " " ==> unwords+proof55 x = intercalate " " x =/= unwords x++-- hint = concat (intersperse x y) ==> intercalate x y where _ = notEq x " "+proof56 x y = concat (intersperse x y) =/= intercalate x y ++-- hint = concat (intersperse " " x) ==> unwords x+proof57 x = concat (intersperse " " x) =/= unwords x++-- warn "Use any" = null (filter f x) ==> not (any f x)+proof58 f x = null (filter f x) =/= not (any f x)++-- warn "Use any" = filter f x == [] ==> not (any f x)+-- warn = filter f x /= [] ==> any f x+-- warn = any id ==> or+proof60 x = any id x =/= or x+proof60list (x::[Bool]) = any id x === or x++-- warn = all id ==> and+proof61 x = all id x =/= and x+proof61list (x::[Bool]) = all id x === and x++-- warn = any ((==) a) ==> elem a where note = ValidInstance "Eq" a+proof62 a x = any ((==) a) x =/= elem a x+proof62list a (x::[a]) = any ((==) a) x =/= elem a x++-- warn = any (== a) ==> elem a+proof63 a x = any (== a) x =/= elem a x+proof63list a (x::[a]) = any (== a) x =/= elem a x++-- warn = any (a ==) ==> elem a where note = ValidInstance "Eq" a+proof64 a x = any (a ==) x =/= elem a x+proof64list a (x::[a]) = any (a ==) x =/= elem a x++-- warn = all ((/=) a) ==> notElem a where note = ValidInstance "Eq" a+-- warn = all (/= a) ==> notElem a where note = ValidInstance "Eq" a+-- warn = all (a /=) ==> notElem a where note = ValidInstance "Eq" a+-- warn = elem True ==> or+proof65 x = elem True x =/= or x+proof65list (x::[Bool]) = elem True x =/= or x++-- warn = notElem False ==> and+proof66 x = notElem False x =/= and x+proof66list (x::[Bool]) = notElem False x =/= and x++-- warn = findIndex ((==) a) ==> elemIndex a+-- warn = findIndex (a ==) ==> elemIndex a+-- warn = findIndex (== a) ==> elemIndex a+-- warn = findIndices ((==) a) ==> elemIndices a+-- warn = findIndices (a ==) ==> elemIndices a+-- warn = findIndices (== a) ==> elemIndices a+-- warn = lookup b (zip l [0..]) ==> elemIndex b l+proof67 b l = lookup b (zip l [0..]) =/= elemIndex b l++-- hint = elem x [y] ==> x == y where note = ValidInstance "Eq" a+proof68 x y = elem x [y] =/= x == y++-- hint = notElem x [y] ==> x /= y where note = ValidInstance "Eq" a+proof69 x y = notElem x [y] =/= x /= y++-- hint "Length always non-negative" = length x >= 0 ==> True+-- hint "Use null" = length x > 0 ==> not (null x) where note = IncreasesLaziness+-- hint "Use null" = length x >= 1 ==> not (null x) where note = IncreasesLaziness+-- warn "Take on a non-positive" = take i x ==> [] where _ = isNegZero i+-- warn "Drop on a non-positive" = drop i x ==> x where _ = isNegZero i+-- warn = last (scanl f z x) ==> foldl f z x+-- warn = head (scanr f z x) ==> foldr f z x+-- warn = iterate id ==> repeat+-- where _ = noQuickCheck -- takes forever+proof70 x = iterate id x =/= repeat x++-- warn = zipWith f (repeat x) ==> map (f x)+proof71 f x y = zipWith f (repeat x) y =/= map (f x) y++-- warn = zipWith f y (repeat z) ==> map (\x -> f x z) y+proof72 f y z = zipWith f y (repeat z) =/= map (\x -> f x z) y++-- -- BY++-- warn = deleteBy (==) ==> delete+proof73 x xs = deleteBy (==) x xs === delete x xs++-- warn = groupBy (==) ==> group+proof74 xs = groupBy (==) xs === group xs++-- warn = insertBy compare ==> insert+proof75 x xs = insertBy compare x xs === insert x xs++-- warn = intersectBy (==) ==> intersect+proof76 xs = intersectBy (==) xs === intersect xs++-- warn = maximumBy compare ==> maximum+proof77 xs = maximumBy compare xs =/= maximum xs+proof77list (xs::[a]) = maximumBy compare xs =/= maximum xs++-- warn = minimumBy compare ==> minimum+proof78 xs = minimumBy compare xs =/= minimum xs+proof78list (xs::[a]) = minimumBy compare xs =/= minimum xs++-- warn = nubBy (==) ==> nub+proof79 xs = nubBy (==) xs === nub xs++-- warn = sortBy compare ==> sort+proof80 xs = sortBy compare xs === sort xs++-- warn = unionBy (==) ==> union+proof81 xs = unionBy (==) xs === union xs++-- -- FOLDS++-- warn = foldr (>>) (return ()) ==> sequence_+-- where _ = noQuickCheck+-- warn = foldr (&&) True ==> and+-- warn = foldl (&&) True ==> and where note = IncreasesLaziness+-- warn = foldr1 (&&) ==> and where note = RemovesError "on []"; _ = noQuickCheck+-- warn = foldl1 (&&) ==> and where note = RemovesError "on []"+-- warn = foldr (||) False ==> or+-- warn = foldl (||) False ==> or where note = IncreasesLaziness+-- warn = foldr1 (||) ==> or where note = RemovesError "on []"+-- warn = foldl1 (||) ==> or where note = RemovesError "on []"+-- warn = foldl (+) 0 ==> sum+-- warn = foldr (+) 0 ==> sum+-- warn = foldl1 (+) ==> sum where note = RemovesError "on []"+-- warn = foldr1 (+) ==> sum where note = RemovesError "on []"+-- warn = foldl (*) 1 ==> product+-- warn = foldr (*) 1 ==> product+-- warn = foldl1 (*) ==> product where note = RemovesError "on []"+-- warn = foldr1 (*) ==> product where note = RemovesError "on []"+-- warn = foldl1 max ==> maximum+-- warn = foldr1 max ==> maximum+-- warn = foldl1 min ==> minimum+-- warn = foldr1 min ==> minimum+-- warn = foldr mplus mzero ==> msum+-- where _ = noQuickCheck++-- -- FUNCTION++-- warn = (\x -> x) ==> id+-- warn = (\x y -> x) ==> const+-- warn = (\(x,y) -> y) ==> snd+-- warn = (\(x,y) -> x) ==> fst+-- hint "Use curry" = (\x y -> f (x,y)) ==> curry f+-- hint "Use uncurry" = (\(x,y) -> f x y) ==> uncurry f where note = IncreasesLaziness+-- warn "Redundant $" = (($) . f) ==> f+-- warn "Redundant $" = (f $) ==> f+-- hint = (\x -> y) ==> const y where _ = isAtom y && not (isWildcard y)+-- -- isWildcard because some people like to put brackets round them even though they are atomic+-- warn "Redundant flip" = flip f x y ==> f y x where _ = isApp original+-- warn "Evaluate" = id x ==> x+-- where _ = not (isTypeApp x)+-- warn "Redundant id" = id . x ==> x+-- warn "Redundant id" = x . id ==> x++-- -- CHAR++-- warn = a >= 'a' && a <= 'z' ==> isAsciiLower a+-- warn = a >= 'A' && a <= 'Z' ==> isAsciiUpper a+-- warn = a >= '0' && a <= '9' ==> isDigit a+-- warn = a >= '0' && a <= '7' ==> isOctDigit a+-- warn = isLower a || isUpper a ==> isAlpha a+-- warn = isUpper a || isLower a ==> isAlpha a++-- -- BOOL++-- warn "Redundant ==" = x == True ==> x+-- hint "Redundant ==" = x == False ==> not x+-- warn "Redundant ==" = True == a ==> a+-- hint "Redundant ==" = False == a ==> not a+-- warn "Redundant /=" = a /= True ==> not a+-- hint "Redundant /=" = a /= False ==> a+-- warn "Redundant /=" = True /= a ==> not a+-- hint "Redundant /=" = False /= a ==> a+-- warn "Redundant if" = (if a then x else x) ==> x where note = IncreasesLaziness+-- warn "Redundant if" = (if a then True else False) ==> a+-- warn "Redundant if" = (if a then False else True) ==> not a+-- warn "Redundant if" = (if a then t else (if b then t else f)) ==> if a || b then t else f+-- warn "Redundant if" = (if a then (if b then t else f) else f) ==> if a && b then t else f+-- warn "Redundant if" = (if x then True else y) ==> x || y where _ = notEq y False+-- warn "Redundant if" = (if x then y else False) ==> x && y where _ = notEq y True+-- hint "Use if" = case a of {True -> t; False -> f} ==> if a then t else f+-- hint "Use if" = case a of {False -> f; True -> t} ==> if a then t else f+-- hint "Use if" = case a of {True -> t; _ -> f} ==> if a then t else f+-- hint "Use if" = case a of {False -> f; _ -> t} ==> if a then t else f+-- hint "Redundant if" = (if c then (True, x) else (False, x)) ==> (c, x) where note = IncreasesLaziness+-- hint "Redundant if" = (if c then (False, x) else (True, x)) ==> (not c, x) where note = IncreasesLaziness+-- hint = or [x, y] ==> x || y+-- hint = or [x, y, z] ==> x || y || z+-- hint = and [x, y] ==> x && y+-- hint = and [x, y, z] ==> x && y && z+-- warn "Redundant if" = (if x then False else y) ==> not x && y where _ = notEq y True+-- warn "Redundant if" = (if x then y else True) ==> not x || y where _ = notEq y False+-- warn "Redundant not" = not (not x) ==> x+-- -- warn "Too strict if" = (if c then f x else f y) ==> f (if c then x else y) where note = IncreasesLaziness+-- -- also breaks types, see #87++-- -- ARROW++-- warn = id *** g ==> second g+-- warn = f *** id ==> first f+-- warn = zip (map f x) (map g x) ==> map (f Control.Arrow.&&& g) x+-- hint = (\(x,y) -> (f x, g y)) ==> f Control.Arrow.*** g+-- hint = (\x -> (f x, g x)) ==> f Control.Arrow.&&& g+-- hint = (\(x,y) -> (f x,y)) ==> Control.Arrow.first f+-- hint = (\(x,y) -> (x,f y)) ==> Control.Arrow.second f+-- hint = (f (fst x), g (snd x)) ==> (f Control.Arrow.*** g) x+-- hint "Redundant pair" = (fst x, snd x) ==> x where note = DecreasesLaziness++-- -- FUNCTOR++-- warn "Functor law" = fmap f (fmap g x) ==> fmap (f . g) x where _ = noQuickCheck+-- warn "Functor law" = f <$> g <$> x ==> f . g <$> x where _ = noQuickCheck+-- warn "Functor law" = fmap id ==> id where _ = noQuickCheck+-- warn "Functor law" = id <$> x ==> x where _ = noQuickCheck+-- hint = fmap f $ x ==> f Control.Applicative.<$> x+-- where _ = (isApp x || isAtom x) && noQuickCheck++-- -- MONAD++-- warn "Monad law, left identity" = return a >>= f ==> f a where _ = noQuickCheck+-- warn "Monad law, left identity" = f =<< return a ==> f a where _ = noQuickCheck+-- warn "Monad law, right identity" = m >>= return ==> m where _ = noQuickCheck+-- warn "Monad law, right identity" = return =<< m ==> m where _ = noQuickCheck+-- warn = liftM ==> fmap+-- warn = liftA ==> fmap+-- hint = m >>= return . f ==> fmap f m where _ = noQuickCheck -- cannot be fmap, because is in Functor not Monad+-- hint = return . f =<< m ==> fmap f m where _ = noQuickCheck+-- warn = (if x then y else return ()) ==> Control.Monad.when x $ _noParen_ y where _ = not (isAtom y) && noQuickCheck+-- warn = (if x then y else return ()) ==> Control.Monad.when x y where _ = isAtom y && noQuickCheck+-- warn = (if x then return () else y) ==> Control.Monad.unless x $ _noParen_ y where _ = not (isAtom y) && noQuickCheck+-- warn = (if x then return () else y) ==> Control.Monad.unless x y where _ = isAtom y && noQuickCheck+-- warn = sequence (map f x) ==> mapM f x where _ = noQuickCheck+-- warn = sequence_ (map f x) ==> mapM_ f x where _ = noQuickCheck+-- hint = flip mapM ==> Control.Monad.forM where _ = noQuickCheck+-- hint = flip mapM_ ==> Control.Monad.forM_ where _ = noQuickCheck+-- hint = flip forM ==> mapM where _ = noQuickCheck+-- hint = flip forM_ ==> mapM_ where _ = noQuickCheck+-- warn = when (not x) ==> unless x where _ = noQuickCheck+-- warn = x >>= id ==> Control.Monad.join x where _ = noQuickCheck+-- warn = id =<< x ==> Control.Monad.join x where _ = noQuickCheck+-- hint = a >> return () ==> Control.Monad.void a+-- where _ = (isAtom a || isApp a) && noQuickCheck+-- warn = fmap (const ()) ==> Control.Monad.void where _ = noQuickCheck+-- warn = const () <$> x ==> Control.Monad.void x where _ = noQuickCheck+-- warn = flip (>=>) ==> (<=<) where _ = noQuickCheck+-- warn = flip (<=<) ==> (>=>) where _ = noQuickCheck+-- warn = flip (>>=) ==> (=<<) where _ = noQuickCheck+-- warn = flip (=<<) ==> (>>=) where _ = noQuickCheck+-- hint = (\x -> f x >>= g) ==> f Control.Monad.>=> g where _ = noQuickCheck+-- hint = (\x -> f =<< g x) ==> f Control.Monad.<=< g where _ = noQuickCheck+-- warn = a >> forever a ==> forever a where _ = noQuickCheck+-- hint = liftM2 id ==> ap where _ = noQuickCheck+-- warn = mapM (uncurry f) (zip l m) ==> zipWithM f l m where _ = noQuickCheck+-- warn = mapM_ (void . f) ==> mapM_ f+-- warn = mapM_ (void f) ==> mapM_ f+-- warn = forM_ x (void . f) ==> forM_ x f+-- warn = forM_ x (void f) ==> forM_ x f+-- warn = void (mapM f x) ==> mapM_ f x+-- warn = void (forM x f) ==> forM_ x f++-- -- STATE MONAD++-- warn = fst (runState x y) ==> evalState x y where _ = noQuickCheck+-- warn = snd (runState x y) ==> execState x y where _ = noQuickCheck++-- -- MONAD LIST++-- warn = fmap unzip (mapM f x) ==> Control.Monad.mapAndUnzipM f x where _ = noQuickCheck+-- warn = sequence (zipWith f x y) ==> Control.Monad.zipWithM f x y where _ = noQuickCheck+-- warn = sequence_ (zipWith f x y) ==> Control.Monad.zipWithM_ f x y where _ = noQuickCheck+-- warn = sequence (replicate n x) ==> Control.Monad.replicateM n x where _ = noQuickCheck+-- warn = sequence_ (replicate n x) ==> Control.Monad.replicateM_ n x where _ = noQuickCheck+-- warn = mapM f (replicate n x) ==> Control.Monad.replicateM n (f x) where _ = noQuickCheck+-- warn = mapM_ f (replicate n x) ==> Control.Monad.replicateM_ n (f x) where _ = noQuickCheck+-- warn = mapM f (map g x) ==> mapM (f . g) x where _ = noQuickCheck+-- warn = mapM_ f (map g x) ==> mapM_ (f . g) x where _ = noQuickCheck+-- warn = mapM id ==> sequence where _ = noQuickCheck+-- warn = mapM_ id ==> sequence_ where _ = noQuickCheck++-- -- APPLICATIVE / TRAVERSABLE++-- warn = flip traverse ==> for where _ = noQuickCheck+-- warn = flip for ==> traverse where _ = noQuickCheck+-- warn = flip traverse_ ==> for_ where _ = noQuickCheck+-- warn = flip for_ ==> traverse_ where _ = noQuickCheck+-- warn = foldr (*>) (pure ()) ==> sequenceA_ where _ = noQuickCheck+-- warn = foldr (<|>) empty ==> asum where _ = noQuickCheck+-- warn = liftA2 (flip ($)) ==> (<**>) where _ = noQuickCheck+-- warn = Just <$> a <|> pure Nothing ==> optional a where _ = noQuickCheck+++-- -- LIST COMP++-- hint "Use list comprehension" = (if b then [x] else []) ==> [x | b]+-- hint "Redundant list comprehension" = [x | x <- y] ==> y where _ = isVar x++-- -- SEQ++-- warn "Redundant seq" = x `seq` x ==> x+-- warn "Redundant seq" = join seq ==> id+-- warn "Redundant $!" = id $! x ==> x+-- warn "Redundant seq" = x `seq` y ==> y where _ = isWHNF x+-- warn "Redundant $!" = f $! x ==> f x where _ = isWHNF x+-- warn "Redundant evaluate" = evaluate x ==> return x where _ = isWHNF x++-- -- TUPLE++-- warn = fst (unzip x) ==> map fst x+-- warn = snd (unzip x) ==> map snd x++-- -- MAYBE++-- warn = maybe x id ==> Data.Maybe.fromMaybe x+-- warn = maybe False (const True) ==> Data.Maybe.isJust+-- warn = maybe True (const False) ==> Data.Maybe.isNothing+-- warn = not (isNothing x) ==> isJust x+-- warn = not (isJust x) ==> isNothing x+-- warn = maybe [] (:[]) ==> maybeToList+-- warn = catMaybes (map f x) ==> mapMaybe f x+-- hint = (case x of Nothing -> y; Just a -> a) ==> fromMaybe y x+-- warn = (if isNothing x then y else f (fromJust x)) ==> maybe y f x+-- warn = (if isJust x then f (fromJust x) else y) ==> maybe y f x+-- warn = maybe Nothing (Just . f) ==> fmap f+-- hint = map fromJust . filter isJust ==> Data.Maybe.catMaybes+-- warn = x == Nothing ==> isNothing x+-- warn = Nothing == x ==> isNothing x+-- warn = x /= Nothing ==> Data.Maybe.isJust x+-- warn = Nothing /= x ==> Data.Maybe.isJust x+-- warn = concatMap (maybeToList . f) ==> Data.Maybe.mapMaybe f+-- warn = concatMap maybeToList ==> catMaybes+-- warn = maybe n Just x ==> x Control.Applicative.<|> n+-- hint = (case x of Just a -> a; Nothing -> y) ==> fromMaybe y x+-- warn = (if isNothing x then y else fromJust x) ==> fromMaybe y x+-- warn = (if isJust x then fromJust x else y) ==> fromMaybe y x+-- warn = isJust x && (fromJust x == y) ==> x == Just y+-- warn = mapMaybe f (map g x) ==> mapMaybe (f . g) x+-- warn = fromMaybe a (fmap f x) ==> maybe a f x+-- warn = mapMaybe id ==> catMaybes+-- hint = [x | Just x <- a] ==> Data.Maybe.catMaybes a+-- hint = (case m of Nothing -> Nothing; Just x -> x) ==> Control.Monad.join m+-- hint = maybe Nothing id ==> join+-- hint "Too strict maybe" = maybe (f x) (f . g) ==> f . maybe x g where note = IncreasesLaziness++-- -- EITHER++-- warn = [a | Left a <- a] ==> lefts a+-- warn = [a | Right a <- a] ==> rights a+-- warn = either Left (Right . f) ==> fmap f++-- -- INFIX++-- hint "Use infix" = elem x y ==> x `elem` y where _ = not (isInfixApp original) && not (isParen result)+-- hint "Use infix" = notElem x y ==> x `notElem` y where _ = not (isInfixApp original) && not (isParen result)+-- hint "Use infix" = isInfixOf x y ==> x `isInfixOf` y where _ = not (isInfixApp original) && not (isParen result)+-- hint "Use infix" = isSuffixOf x y ==> x `isSuffixOf` y where _ = not (isInfixApp original) && not (isParen result)+-- hint "Use infix" = isPrefixOf x y ==> x `isPrefixOf` y where _ = not (isInfixApp original) && not (isParen result)+-- hint "Use infix" = union x y ==> x `union` y where _ = not (isInfixApp original) && not (isParen result)+-- hint "Use infix" = intersect x y ==> x `intersect` y where _ = not (isInfixApp original) && not (isParen result)++-- -- MATHS++-- warn "Redundant fromIntegral" = fromIntegral x ==> x where _ = isLitInt x+-- warn "Redundant fromInteger" = fromInteger x ==> x where _ = isLitInt x+-- hint = x + negate y ==> x - y+-- hint = 0 - x ==> negate x+-- warn "Redundant negate" = negate (negate x) ==> x+-- hint = log y / log x ==> logBase x y+-- hint = sin x / cos x ==> tan x+-- hint = n `rem` 2 == 0 ==> even n+-- hint = n `rem` 2 /= 0 ==> odd n+-- hint = not (even x) ==> odd x+-- hint = not (odd x) ==> even x+-- hint = x ** 0.5 ==> sqrt x+-- hint "Use 1" = x ^ 0 ==> 1+-- hint = round (x - 0.5) ==> floor x++-- -- CONCURRENT++-- hint = mapM_ (writeChan a) ==> writeList2Chan a++-- -- EXCEPTION++-- hint = flip Control.Exception.catch ==> handle+-- hint = flip handle ==> Control.Exception.catch+-- hint = flip (catchJust p) ==> handleJust p+-- hint = flip (handleJust p) ==> catchJust p+-- hint = Control.Exception.bracket b (const a) (const t) ==> Control.Exception.bracket_ b a t+-- hint = Control.Exception.bracket (openFile x y) hClose ==> withFile x y+-- hint = Control.Exception.bracket (openBinaryFile x y) hClose ==> withBinaryFile x y+-- hint = throw (ErrorCall a) ==> error a+-- warn = toException NonTermination ==> nonTermination+-- warn = toException NestedAtomically ==> nestedAtomically++-- -- STOREABLE/PTR++-- hint = castPtr nullPtr ==> nullPtr+-- hint = castPtr (castPtr x) ==> castPtr x+-- hint = plusPtr (castPtr x) ==> plusPtr x+-- hint = minusPtr (castPtr x) ==> minusPtr x+-- hint = minusPtr x (castPtr y) ==> minusPtr x y+-- hint = peekByteOff (castPtr x) ==> peekByteOff x+-- hint = pokeByteOff (castPtr x) ==> pokeByteOff x++-- -- WEAK POINTERS++-- warn = mkWeak a a b ==> mkWeakPtr a b+-- warn = mkWeak a (a, b) c ==> mkWeakPair a b c++-- -- FOLDABLE++-- warn "Use Foldable.forM_" = (case m of Nothing -> return (); Just x -> f x) ==> Data.Foldable.forM_ m f+-- where _ = noQuickCheck+-- warn "Use Foldable.forM_" = when (isJust m) (f (fromJust m)) ==> Data.Foldable.forM_ m f+-- where _ = noQuickCheck++-- -- EVALUATE++-- -- TODO: These should be moved in to HSE\Evaluate.hs and applied+-- -- through a special evaluate hint mechanism+-- warn "Evaluate" = True && x ==> x+-- warn "Evaluate" = False && x ==> False+-- warn "Evaluate" = True || x ==> True+-- warn "Evaluate" = False || x ==> x+-- warn "Evaluate" = not True ==> False+-- warn "Evaluate" = not False ==> True+-- warn "Evaluate" = Nothing >>= k ==> Nothing+-- warn "Evaluate" = k =<< Nothing ==> Nothing+-- warn "Evaluate" = either f g (Left x) ==> f x+-- warn "Evaluate" = either f g (Right y) ==> g y+-- warn "Evaluate" = fst (x,y) ==> x+-- warn "Evaluate" = snd (x,y) ==> y+-- warn "Evaluate" = f (fst p) (snd p) ==> uncurry f p+-- warn "Evaluate" = init [x] ==> []+-- warn "Evaluate" = null [] ==> True+-- warn "Evaluate" = length [] ==> 0+-- warn "Evaluate" = foldl f z [] ==> z+-- warn "Evaluate" = foldr f z [] ==> z+-- warn "Evaluate" = foldr1 f [x] ==> x+-- warn "Evaluate" = scanr f z [] ==> [z]+-- warn "Evaluate" = scanr1 f [] ==> []+-- warn "Evaluate" = scanr1 f [x] ==> [x]+-- warn "Evaluate" = take n [] ==> [] where note = IncreasesLaziness+-- warn "Evaluate" = drop n [] ==> [] where note = IncreasesLaziness+-- warn "Evaluate" = takeWhile p [] ==> []+-- warn "Evaluate" = dropWhile p [] ==> []+-- warn "Evaluate" = span p [] ==> ([],[])+-- warn "Evaluate" = lines "" ==> []+-- warn "Evaluate" = unwords [] ==> ""+-- warn "Evaluate" = x - 0 ==> x+-- warn "Evaluate" = x * 1 ==> x+-- warn "Evaluate" = x / 1 ==> x+-- warn "Evaluate" = concat [a] ==> a+-- warn "Evaluate" = concat [] ==> []+-- warn "Evaluate" = zip [] [] ==> []+-- warn "Evaluate" = const x y ==> x++-- -- FOLDABLE + TUPLES++-- warn "Using foldr on tuple" = foldr f z (x,b) ==> f b z+-- warn "Using foldr' on tuple" = foldr' f z (x,b) ==> f b z+-- warn "Using foldl on tuple" = foldl f z (x,b) ==> f z b+-- warn "Using foldl' on tuple" = foldl' f z (x,b) ==> f z b+-- warn "Using foldMap on tuple" = foldMap f (x,b) ==> f b+-- warn "Using foldr1 on tuple" = foldr1 f (x,b) ==> b+-- warn "Using foldl1 on tuple" = foldl1 f (x,b) ==> b+-- warn "Using elem on tuple" = elem e (x,b) ==> e == b+-- warn "Using fold on tuple" = fold (x,b) ==> b+-- warn "Using toList on tuple" = toList (x,b) ==> b+-- warn "Using maximum on tuple" = maximum (x,b) ==> b+-- warn "Using minimum on tuple" = minimum (x,b) ==> b+-- warn "Using sum on tuple" = sum (x,b) ==> b+-- warn "Using product on tuple" = product (x,b) ==> b+-- warn "Using concat on tuple" = concat (x,b) ==> b+-- warn "Using and on tuple" = and (x,b) ==> b+-- warn "Using or on tuple" = or (x,b) ==> b+-- warn "Using any on tuple" = any f (x,b) ==> f b+-- warn "Using all on tuple" = all f (x,b) ==> f b++-- warn "Using foldr on tuple" = foldr f z (x,y,b) ==> f b z+-- warn "Using foldr' on tuple" = foldr' f z (x,y,b) ==> f b z+-- warn "Using foldl on tuple" = foldl f z (x,y,b) ==> f z b+-- warn "Using foldl' on tuple" = foldl' f z (x,y,b) ==> f z b+-- warn "Using foldMap on tuple" = foldMap f (x,y,b) ==> f b+-- warn "Using foldr1 on tuple" = foldr1 f (x,y,b) ==> b+-- warn "Using foldl1 on tuple" = foldl1 f (x,y,b) ==> b+-- warn "Using elem on tuple" = elem e (x,y,b) ==> e == b+-- warn "Using fold on tuple" = fold (x,y,b) ==> b+-- warn "Using toList on tuple" = toList (x,y,b) ==> b+-- warn "Using maximum on tuple" = maximum (x,y,b) ==> b+-- warn "Using minimum on tuple" = minimum (x,y,b) ==> b+-- warn "Using sum on tuple" = sum (x,y,b) ==> b+-- warn "Using product on tuple" = product (x,y,b) ==> b+-- warn "Using concat on tuple" = concat (x,y,b) ==> b+-- warn "Using and on tuple" = and (x,y,b) ==> b+-- warn "Using or on tuple" = or (x,y,b) ==> b+-- warn "Using any on tuple" = any f (x,y,b) ==> f b+-- warn "Using all on tuple" = all f (x,y,b) ==> f b++-- warn "Using null on tuple" = null x ==> False where _ = isTuple x+-- warn "Using length on tuple" = length x ==> 1 where _ = isTuple x++-- To be able to use this as a test suite+main = putStrLn "I ran, ergo I compiled."
+ examples/Successors.hs view
@@ -0,0 +1,110 @@+{-+This example is based on Control.Applicative.Successors, and shows how some+algebraic laws of a simple data structure can be proven by GHC.+-}+{-# LANGUAGE BangPatterns, ScopedTypeVariables, TypeApplications#-}+{-# OPTIONS_GHC -O -fplugin GHC.Proof.Plugin #-}+module Successors where++import GHC.Proof+import GHC.Base (build, mapFB, foldr)+import Control.Monad (ap)++-- The original code++data Succs a = Succs a [a]++instance Functor Succs where+ fmap f (Succs o s) = Succs (f o) (map f s)++instance Applicative Succs where+ pure x = Succs x []+ Succs f fs <*> Succs x xs = Succs (f x) (map ($x) fs ++ map f xs)++instance Monad Succs where+ return = pure -- this is strangely necesary+ Succs x xs >>= f = Succs y (map (getCurrent . f) xs ++ ys)+ where Succs y ys = f x++-- Two simple accessor function. The docs come with three identities each+--+-- prop> getCurrent (pure x) == x+-- prop> getCurrent (f <*> x) == (getCurrent f) (getCurrent x)+-- prop> getCurrent (x >>= k) == getCurrent (k (getCurrent x))+getCurrent :: Succs t -> t+getCurrent (Succs x _) = x++-- prop> getSuccs (pure x) == []+-- prop> getSuccs (f <*> x) == map ($ getCurrent x) (getSuccs f) ++ map (getCurrent f) (getSuccs x)+-- prop> getSuccs (x >>= k) == map (getCurrent . k) (getSuccs x) ++ getSuccs (k (getCurrent x))+getSuccs :: Succs t -> [t]+getSuccs (Succs _ xs) = xs++-- These identities are easily proven by GHC,+-- at least if one helps by making some of the arguments as strict.++getCurrent_prop1 x = getCurrent (pure x)+ === x+getCurrent_prop2 f x = (x `seq` getCurrent (f <*> x))+ === (x `seq` getCurrent f (getCurrent x))+getCurrent_prop3 x k = getCurrent (x >>= k)+ === (x `seq` getCurrent (k (getCurrent x)))++getSuccs_prop1 x = getSuccs (pure x)+ === []+getSuccs_prop2 f x = (x `seq` getSuccs (f <*> x))+ === (x `seq` map ($ getCurrent x) (getSuccs f) ++ map (getCurrent f) (getSuccs x))+getSuccs_prop3 x k = getSuccs (x >>= k)+ === map (getCurrent . k) (getSuccs x) ++ getSuccs (k (getCurrent x))++-- And now to the actual laws++functor_law1 :: Succs a -> Proof+functor_law1 v = fmap id v+ === v++functor_law2 :: (a -> b) -> (b -> c) -> Succs a -> Proof+functor_law2 f g v = fmap g (fmap f v)+ === fmap (g . f) v++applicative_law1 :: Succs a -> Proof+applicative_law1 v = pure id <*> v+ === v++applicative_law2 :: Succs (b -> c) -> Succs (a -> b) -> Succs a -> Proof+applicative_law2 u v w = pure (.) <*> u <*> v <*> w+ === u <*> (v <*> w)++applicative_law3 :: forall a b. (a -> b) -> a -> Proof+applicative_law3 f x = pure f <*> (pure x :: Succs a)+ === pure (f x)++applicative_law4 :: Succs (a -> b) -> a -> Proof+applicative_law4 u y = u <*> pure y+ === pure ($ y) <*> u++monad_law1 :: a -> (a -> Succs b) -> Proof+monad_law1 a k = (k a `seq` return a >>= k)+ === k a++monad_law2 :: Succs a -> Proof+monad_law2 m = m >>= return+ === m++-- A little trick to say: Prove this only for strict f+str :: (a -> b) -> (a -> b)+str f x = x `seq` f x++monad_law3 :: Succs a -> (a -> Succs b) -> (b -> Succs c) -> Proof+monad_law3 m k h = m >>= (\x -> k x >>= str h)+ === (m >>= k) >>= str h++-- The law relating the monad and applicative instances++return_pure x = return @Succs x+ === pure @Succs x++ap_star f x = (x `seq` getCurrent f `seq` f <*> x)+ === (x `seq` getCurrent f `seq` f `ap` x)++main = putStrLn "I ran, ergo I compiled."
+ ghc-proofs.cabal view
@@ -0,0 +1,58 @@+name: ghc-proofs+version: 0.1+synopsis: GHC plugin to prove program equations by simplification+description: Often when writing Haskel code, one would like to prove things about the code.+ .+ A good example is writing an 'Applicative' or 'Monad'+ instance: there are equation that should hold, and+ checking them manually is tedious.+ .+ Wouldn’t it be nice if the compiler could check them for+ us? With this plugin, he can! (At least in certain simple+ cases – for everything else, you have to use a more+ dedicated solution.)+ .+ See the documentation in "GHC.Proof" or the project+ webpage for more examples and more information.++category: Compiler Plugin, Formal Methods+homepage: https://github.com/nomeata/ghc-proofs+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.2.1, GHC == 8.3++source-repository head+ type: git+ location: git://github.com/nomeata/ghc-proofs.git++library+ exposed-modules: GHC.Proof+ GHC.Proof.Plugin+ build-depends: base >=4.9 && <4.11+ build-depends: ghc >= 8.2 && <8.4+ default-language: Haskell2010++test-suite successors+ type: exitcode-stdio-1.0+ hs-source-dirs: examples+ main-is: Successors.hs+ build-depends: ghc-proofs+ build-depends: base >=4.9 && <4.11+ default-language: Haskell2010+ ghc-options: -main-is Successors++test-suite hlint+ type: exitcode-stdio-1.0+ hs-source-dirs: examples+ main-is: HLint.hs+ build-depends: ghc-proofs+ build-depends: base >=4.9 && <4.11+ build-depends: transformers+ default-language: Haskell2010+ ghc-options: -main-is HLint