diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,9 @@ +# Revision history for ghc-proofs + +## 0.1 -- 2017-08-26 + +* Initial release to hackage + +## 0 -- 2017-02-06 + +* Development commences diff --git a/GHC/Proof.hs b/GHC/Proof.hs new file mode 100644 --- /dev/null +++ b/GHC/Proof.hs @@ -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 =/= + + diff --git a/GHC/Proof/Plugin.hs b/GHC/Proof/Plugin.hs new file mode 100644 --- /dev/null +++ b/GHC/Proof/Plugin.hs @@ -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 + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2017 Joachim Breitner + +Permission is hereby granted, free of charge, to any person obtaining +a copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be included +in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY +CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, +TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE +SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,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. + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/examples/HLint.hs b/examples/HLint.hs new file mode 100644 --- /dev/null +++ b/examples/HLint.hs @@ -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." diff --git a/examples/Successors.hs b/examples/Successors.hs new file mode 100644 --- /dev/null +++ b/examples/Successors.hs @@ -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." diff --git a/ghc-proofs.cabal b/ghc-proofs.cabal new file mode 100644 --- /dev/null +++ b/ghc-proofs.cabal @@ -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