ghc-proofs 0.1 → 0.1.1

raw patch · 4 files changed

+13/−8 lines, 4 files

Files

• ChangeLog.md +4/−0
• GHC/Proof/Plugin.hs +2/−0
• examples/HLint.hs +6/−7
• ghc-proofs.cabal +1/−1

@@ -1,5 +1,9 @@ # Revision history for ghc-proofs +## 0.1.1  -- 2017-09-05++* Also run simplifier in stage 0+ ## 0.1  -- 2017-08-26  * Initial release to hackage

@@ -128,6 +128,8 @@                         >>= simplExpr (simplEnv in_scope 2) . occurAnalyseExpr                         >>= simplExpr (simplEnv in_scope 1) . occurAnalyseExpr . cseOneExpr'                         >>= simplExpr (simplEnv in_scope 1) . occurAnalyseExpr . cseOneExpr'+                        >>= simplExpr (simplEnv in_scope 0) . occurAnalyseExpr . cseOneExpr'+                        >>= simplExpr (simplEnv in_scope 0) . occurAnalyseExpr . cseOneExpr'     return expr'  #if  __GLASGOW_HASKELL__ >= 801

@@ -137,7 +137,7 @@ -- -- LIST  -- warn = concat (map f x) ==> concatMap f x-proof22 f x = 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@@ -150,7 +150,7 @@ 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+proof26 f g x = concatMap f (map g x) === concatMap (f . g) x  -- hint = x !! 0 ==> head x proof27 x = x !! 0 =/= head x@@ -165,8 +165,7 @@  -- 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!+proof30 f x = map f (repeat x) === repeat (f x)  -- warn = cycle [x] ==> repeat x --     where _ = noQuickCheck -- takes forever@@ -220,10 +219,10 @@ 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+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+proof45 p x = and (map p x) === all p x  -- warn = zipWith (,) ==> zip proof46 = zipWith (,) =/= zip@@ -249,7 +248,7 @@ 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+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)

@@ -1,5 +1,5 @@ name:                ghc-proofs-version:             0.1+version:             0.1.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.                      .