+ Most hints are perfect substitutions, and these are displayed without any notes. However, some hints change the semantics of your program - typically in irrelevant ways - but HLint shows a warning note. HLint does not warn when assuming typeclass laws (such as == being symmetric). Some notes you may see include: +
+
diff --git a/src/CmdLine.hs b/src/CmdLine.hs
--- a/src/CmdLine.hs
+++ b/src/CmdLine.hs
@@ -42,6 +42,7 @@
,cmdLanguage :: [Extension] -- ^ the extensions (may be prefixed by "No")
,cmdQuiet :: Bool -- ^ supress all console output
,cmdCross :: Bool -- ^ work between source files, applies to hints such as duplicate code between modules
+ ,cmdProof :: [FilePath] -- ^ a proof script to check against
}
@@ -63,6 +64,7 @@
| Encoding String
| FindHints FilePath
| Language String
+ | Proof FilePath
| Quiet
| Cross
| Ansi
@@ -87,6 +89,7 @@
,Option "d" ["datadir"] (ReqArg DataDir "dir") "Override the data directory"
,Option "p" ["path"] (ReqArg Path "dir") "Directory in which to search for files"
,Option "q" ["quiet"] (NoArg Quiet) "Supress most console output"
+ ,Option "" ["proof"] (ReqArg Proof "file") "Isabelle/HOLCF theory file"
,Option "" ["cpp-define"] (ReqArg Define "name[=value]") "CPP #define"
,Option "" ["cpp-include"] (ReqArg Include "dir") "CPP include path"
,Option "" ["cpp-simple"] (NoArg SimpleCpp) "Use a simple CPP (strip # lines)"
@@ -152,6 +155,7 @@
,cmdLanguage = languages
,cmdQuiet = Quiet `elem` opt
,cmdCross = Cross `elem` opt
+ ,cmdProof = [x | Proof x <- opt]
}
diff --git a/src/HLint.hs b/src/HLint.hs
--- a/src/HLint.hs
+++ b/src/HLint.hs
@@ -12,6 +12,7 @@
import Idea
import Apply
import Test
+import Proof
import Util
import Parallel
import HSE.All
@@ -49,6 +50,11 @@
let flags = parseFlags{cppFlags=cmdCpp, encoding=cmdEncoding, language=cmdLanguage}
if cmdTest then
test (\x -> hlint x >> return ()) cmdDataDir cmdGivenHints >> return []
+ else if notNull cmdProof then do
+ s <- readAllSettings cmd flags
+ let reps = if cmdReports == ["report.html"] then ["report.txt"] else cmdReports
+ mapM_ (proof reps s) cmdProof
+ return []
else if isNothing cmdFiles && notNull cmdFindHints then
mapM_ (\x -> putStrLn . fst =<< findSettings flags x) cmdFindHints >> return []
else if isNothing cmdFiles then
@@ -58,14 +64,18 @@
else
runHints cmd flags
-
-runHints :: Cmd -> ParseFlags -> IO [Suggestion]
-runHints Cmd{..} flags = do
- let outStrLn x = unless cmdQuiet $ putStrLn x
+readAllSettings :: Cmd -> ParseFlags -> IO [Setting]
+readAllSettings Cmd{..} flags = do
settings1 <- readSettings cmdDataDir cmdHintFiles cmdWithHints
settings2 <- concatMapM (fmap snd . findSettings flags) cmdFindHints
settings3 <- return [Classify Ignore x ("","") | x <- cmdIgnore]
- let settings = settings1 ++ settings2 ++ settings3
+ return $ settings1 ++ settings2 ++ settings3
+
+
+runHints :: Cmd -> ParseFlags -> IO [Suggestion]
+runHints cmd@Cmd{..} flags = do
+ let outStrLn x = unless cmdQuiet $ putStrLn x
+ settings <- readAllSettings cmd flags
let files = fromMaybe [] cmdFiles
ideas <- if cmdCross
diff --git a/src/HSE/Bracket.hs b/src/HSE/Bracket.hs
--- a/src/HSE/Bracket.hs
+++ b/src/HSE/Bracket.hs
@@ -45,6 +45,7 @@
| isAtom child = False
| InfixApp{} <- parent, App{} <- child = False
| isSection parent, App{} <- child = False
+ | Let{} <- parent, App{} <- child = False
| ListComp{} <- parent = False
| List{} <- parent = False
| Tuple{} <- parent = False
diff --git a/src/HSE/Evaluate.hs b/src/HSE/Evaluate.hs
--- a/src/HSE/Evaluate.hs
+++ b/src/HSE/Evaluate.hs
@@ -19,6 +19,8 @@
evaluate1 (App s len (List _ xs)) | len ~= "length" = Lit s $ Int s n (show n)
where n = fromIntegral $ length xs
evaluate1 (view -> App2 op (Lit _ x) (Lit _ y)) | op ~= "==" = toNamed $ show $ x =~= y
+evaluate1 (view -> App2 op (Lit _ (Int _ x _)) (Lit _ (Int _ y _)))
+ | op ~= ">=" = toNamed $ show $ x >= y
evaluate1 (view -> App2 op x y)
| op ~= "&&" && x ~= "True" = y
| op ~= "&&" && x ~= "False" = x
diff --git a/src/HSE/Util.hs b/src/HSE/Util.hs
--- a/src/HSE/Util.hs
+++ b/src/HSE/Util.hs
@@ -75,6 +75,7 @@
isList List{} = True; isList _ = False
isAnyApp x = isApp x || isInfixApp x
isParen Paren{} = True; isParen _ = False
+isIf If{} = True; isIf _ = False
isLambda Lambda{} = True; isLambda _ = False
isMDo MDo{} = True; isMDo _ = False
isBoxed Boxed{} = True; isBoxed _ = False
diff --git a/src/Hint/Duplicate.hs b/src/Hint/Duplicate.hs
--- a/src/Hint/Duplicate.hs
+++ b/src/Hint/Duplicate.hs
@@ -36,7 +36,7 @@
(if length xs >= 5 then Error else Warning)
"Reduce duplication" p1
(unlines $ map (prettyPrint . fmap (const p1)) xs)
- ("Combine with " ++ showSrcLoc p2) ""
+ ("Combine with " ++ showSrcLoc p2) []
| (p1,p2,xs) <- duplicateOrdered 3 $ map (map (toSrcLoc . ann &&& dropAnn)) ys]
diff --git a/src/Hint/Extensions.hs b/src/Hint/Extensions.hs
--- a/src/Hint/Extensions.hs
+++ b/src/Hint/Extensions.hs
@@ -63,8 +63,8 @@
-- RecordWildCards implies DisambiguateRecordFields, but most people probably don't want it
-warnings old new | RecordWildCards `elem` old && RecordWildCards `notElem` new = "you may need to add DisambiguateRecordFields"
-warnings _ _ = ""
+warnings old new | RecordWildCards `elem` old && RecordWildCards `notElem` new = [Note "you may need to add DisambiguateRecordFields"]
+warnings _ _ = []
used :: Extension -> Module_ -> Bool
diff --git a/src/Hint/Import.hs b/src/Hint/Import.hs
--- a/src/Hint/Import.hs
+++ b/src/Hint/Import.hs
@@ -56,7 +56,7 @@
wrap :: [ImportDecl S] -> [Idea]
-wrap o = [ rawIdea Error "Use fewer imports" (toSrcLoc $ ann $ head o) (f o) (f x) ""
+wrap o = [ rawIdea Error "Use fewer imports" (toSrcLoc $ ann $ head o) (f o) (f x) []
| Just x <- [simplify o]]
where f = unlines . map prettyPrint
@@ -124,7 +124,7 @@
= [rawIdea Warning "Use hierarchical imports" (toSrcLoc $ ann i) (ltrim $ prettyPrint i) (
unlines $ map (ltrim . prettyPrint)
[f "System.IO" Nothing, f "System.IO.Error" Nothing
- ,f "Control.Exception" $ Just $ ImportSpecList an False [IVar an $ toNamed x | x <- ["bracket","bracket_"]]]) ""]
+ ,f "Control.Exception" $ Just $ ImportSpecList an False [IVar an $ toNamed x | x <- ["bracket","bracket_"]]]) []]
where f a b = (desugarQual i){importModule=ModuleName an a, importSpecs=b}
hierarchy _ = []
@@ -141,7 +141,7 @@
[ rawIdea Warning "Use import/export shortcut" (toSrcLoc $ ann hd)
(unlines $ prettyPrint hd : map prettyPrint imps)
(unlines $ prettyPrint newhd : map prettyPrint newimps)
- ""
+ []
| Module l (Just hd) _ imp _ <- [x]
, let asNames = mapMaybe importAs imp
, let expNames = [x | EModuleContents _ x <- childrenBi hd]
diff --git a/src/Hint/Match.hs b/src/Hint/Match.hs
--- a/src/Hint/Match.hs
+++ b/src/Hint/Match.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE PatternGuards, ViewPatterns, RelaxedPolyRec #-}
+{-# LANGUAGE PatternGuards, ViewPatterns, RelaxedPolyRec, RecordWildCards #-}
{-
The matching does a fairly simple unification between the two terms, treating
@@ -83,8 +83,8 @@
, m <- matches, Just (y,notes) <- [matchIdea s decl m parent x2]]
-matchIdea :: Scope -> Decl_ -> Setting -> Maybe (Int, Exp_) -> Exp_ -> Maybe (Exp_,String)
-matchIdea s decl MatchExp{lhs=lhs,rhs=rhs,side=side,scope=scope,notes=notes} parent x = do
+matchIdea :: Scope -> Decl_ -> Setting -> Maybe (Int, Exp_) -> Exp_ -> Maybe (Exp_,[Note])
+matchIdea s decl MatchExp{..} parent x = do
let nm = nameMatch scope s
u <- unifyExp nm True lhs x
u <- check u
@@ -186,8 +186,18 @@
isType "Atom" x = isAtom x
isType "WHNF" x = isWHNF x
+ isType "Nat" (asInt -> Just x) | x >= 0 = True
+ isType "Pos" (asInt -> Just x) | x > 0 = True
+ isType "Neg" (asInt -> Just x) | x < 0 = True
+ isType "NegZero" (asInt -> Just x) | x <= 0 = True
isType ('L':'i':'t':typ@(_:_)) (Lit _ x) = head (words $ show x) == typ
isType typ x = head (words $ show x) == typ
+
+ asInt :: Exp_ -> Maybe Integer
+ asInt (Paren _ x) = asInt x
+ asInt (NegApp _ x) = fmap negate $ asInt x
+ asInt (Lit _ (Int _ x _)) = Just x
+ asInt _ = Nothing
list :: Exp_ -> [Exp_]
list (List _ xs) = xs
diff --git a/src/Hint/Pragma.hs b/src/Hint/Pragma.hs
--- a/src/Hint/Pragma.hs
+++ b/src/Hint/Pragma.hs
@@ -41,7 +41,7 @@
pragmaIdea :: [ModulePragma S] -> [ModulePragma S] -> Idea
-pragmaIdea xs ys = rawIdea Error "Use better pragmas" (toSrcLoc $ ann $ head xs) (f xs) (f ys) ""
+pragmaIdea xs ys = rawIdea Error "Use better pragmas" (toSrcLoc $ ann $ head xs) (f xs) (f ys) []
where f = unlines . map prettyPrint
diff --git a/src/Idea.hs b/src/Idea.hs
--- a/src/Idea.hs
+++ b/src/Idea.hs
@@ -1,6 +1,6 @@
{-# LANGUAGE RecordWildCards, NoMonomorphismRestriction #-}
-module Idea(module Idea, Severity(..)) where
+module Idea(module Idea, Note(..), showNotes, Severity(..)) where
import HSE.All
import Settings
@@ -10,7 +10,7 @@
data Idea
- = Idea {func :: FuncName, severity :: Severity, hint :: String, loc :: SrcLoc, from :: String, to :: String, note :: String}
+ = Idea {func :: FuncName, severity :: Severity, hint :: String, loc :: SrcLoc, from :: String, to :: String, note :: [Note]}
| ParseError {severity :: Severity, hint :: String, loc :: SrcLoc, msg :: String, from :: String}
deriving (Eq,Ord)
@@ -31,7 +31,7 @@
showEx tt Idea{..} = unlines $
[showSrcLoc loc ++ ": " ++ show severity ++ ": " ++ hint] ++
f "Found" from ++ f "Why not" to ++
- ["Note: " ++ note | note /= ""]
+ ["Note: " ++ n | let n = showNotes note, n /= ""]
where
f msg x | null xs = [msg ++ " remove it."]
| otherwise = (msg ++ ":") : map (" "++) xs
@@ -42,7 +42,7 @@
rawIdea = Idea ("","")
-idea severity hint from to = rawIdea severity hint (toSrcLoc $ ann from) (f from) (f to) ""
+idea severity hint from to = rawIdea severity hint (toSrcLoc $ ann from) (f from) (f to) []
where f = ltrim . prettyPrint
warn = idea Warning
err = idea Error
diff --git a/src/Proof.hs b/src/Proof.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof.hs
@@ -0,0 +1,179 @@
+{-# LANGUAGE RecordWildCards, PatternGuards #-}
+
+module Proof(proof) where
+
+import Control.Arrow
+import Control.Monad
+import Control.Monad.Trans.State
+import Data.Char
+import Data.List
+import Data.Maybe
+import Data.Function
+import System.FilePath
+import Settings
+import HSE.All
+
+
+data Theorem = Theorem
+ {original :: Maybe Setting
+ ,location :: String
+ ,lemma :: String
+ }
+
+instance Eq Theorem where
+ t1 == t2 = lemma t1 == lemma t2
+
+instance Show Theorem where
+ show Theorem{..} = location ++ ":\n" ++ maybe "" f original ++ lemma ++ "\n"
+ where f MatchExp{..} = "(* " ++ prettyPrint lhs ++ " ==> " ++ prettyPrint rhs ++ " *)\n"
+
+proof :: [FilePath] -> [Setting] -> FilePath -> IO ()
+proof reports hints thy = do
+ got <- fmap (isabelleTheorems (takeFileName thy)) $ readFile thy
+ let want = nub $ hintTheorems hints
+ let unused = got \\ want
+ let missing = want \\ got
+ let reasons = map (\x -> (fst $ head x, map snd x)) $ groupBy ((==) `on` fst) $
+ sortBy (compare `on` fst) $ map (classifyMissing &&& id) missing
+ let summary = table $ let (*) = (,) in
+ ["HLint hints" * want
+ ,"HOL proofs" * got
+ ,"Useful proofs" * (got `intersect` want)
+ ,"Unused proofs" * unused
+ ,"Unproved hints" * missing] ++
+ [(" " ++ name) * ps | (name,ps) <- reasons]
+ putStr $ unlines summary
+ forM_ reports $ \report -> do
+ let out = ("Unused proofs",unused) : map (first ("Unproved hints - " ++)) reasons
+ writeFile report $ unlines $ summary ++ "" : concat
+ [("== " ++ a ++ " ==") : "" : map show b | (a,b) <- out]
+ putStrLn $ "Report written to " ++ report
+ where
+ table xs = [a ++ replicate (n + 6 - length a - length bb) ' ' ++ bb | (a,b) <- xs, let bb = show $ length b]
+ where n = maximum $ map (length . fst) xs
+
+
+missingFuncs = let a*b = [(b,a) | b <- words b] in concat
+ ["IO" * "putChar putStr print putStrLn getLine getChar getContents hReady hPrint stdin"
+ ,"Exit" * "exitSuccess"
+ ,"Ord" * "(>) (<=) (>=) (<) compare minimum maximum sort sortBy"
+ ,"Show" * "show shows showIntAtBase"
+ ,"Read" * "reads read"
+ ,"String" * "lines unlines words unwords"
+ ,"Monad" * "mapM mapM_ sequence sequence_ msum mplus mzero liftM when unless return evaluate join void (>>=) (<=<) (>=>) forever ap"
+ ,"Functor" * "fmap"
+ ,"Numeric" * "(+) (*) fromInteger fromIntegral negate log (/) (-) (*) (^^) (^) subtract sqrt even odd"
+ ,"Char" * "isControl isPrint isUpper isLower isAlpha isDigit"
+ ,"Arrow" * "second first (***) (&&&)"
+ ,"Applicative+" * "traverse for traverse_ for_ pure (<|>) (<**>)"
+ ,"Exception" * "catch handle catchJust bracket error toException"
+ ,"WeakPtr" * "mkWeak"
+ ]
+
+
+-- | Guess why a theorem is missing
+classifyMissing :: Theorem -> String
+classifyMissing Theorem{original = Just MatchExp{..}}
+ | _:_ <- [v :: Exp_ | v@Case{} <- universeBi (lhs,rhs)] = "case"
+ | _:_ <- [v :: Exp_ | v@ListComp{} <- universeBi (lhs,rhs)] = "list-comp"
+ | v:_ <- mapMaybe (`lookup` missingFuncs) [prettyPrint (v :: Name SrcSpanInfo) | v <- universeBi (lhs,rhs)] = v
+classifyMissing _ = "?unknown"
+
+
+-- Extract theorems out of Isabelle code (HLint.thy)
+isabelleTheorems :: FilePath -> String -> [Theorem]
+isabelleTheorems file = find . lexer 1
+ where
+ find ((i,"lemma"):(_,'\"':lemma):rest) = Theorem Nothing (file ++ ":" ++ show i) lemma : find rest
+ find ((i,"lemma"):(_,name):(_,":"):(_,'\"':lemma):rest) = Theorem Nothing (file ++ ":" ++ show i) lemma : find rest
+ find ((i,"lemma"):(_,"assumes"):(_,'\"':assumes):(_,"shows"):(_,'\"':lemma):rest) =
+ Theorem Nothing (file ++ ":" ++ show i) (assumes ++ " \\
"
,code to
- ,if note /= "" then "Note: " ++ note ++ "" else ""
+ ,let n = showNotes note in if n /= "" then "Note: " ++ n ++ "" else ""
,""
,""]
diff --git a/src/Settings.hs b/src/Settings.hs
--- a/src/Settings.hs
+++ b/src/Settings.hs
@@ -1,7 +1,7 @@
{-# LANGUAGE PatternGuards, ViewPatterns #-}
module Settings(
- Severity(..), FuncName, Setting(..), isClassify, isMatchExp,
+ Severity(..), Note(..), showNotes, FuncName, Setting(..), isClassify, isMatchExp,
defaultHintName, isUnifyVar,
readSettings, readPragma, findSettings
) where
@@ -48,9 +48,31 @@
---------------------------------------------------------------------
-- TYPE
+data Note
+ = IncreasesLaziness
+ | DecreasesLaziness
+ | RemovesError String -- RemovesError "on []", RemovesError "when x is negative"
+ | ValidInstance String String -- ValidInstance "Eq" "x"
+ | Note String
+ deriving (Eq,Ord)
+
+instance Show Note where
+ show IncreasesLaziness = "increases laziness"
+ show DecreasesLaziness = "decreases laziness"
+ show (RemovesError x) = "removes error " ++ x
+ show (ValidInstance x y) = "requires a valid " ++ x ++ " instance for " ++ y
+ show (Note x) = x
+
+
+showNotes :: [Note] -> String
+showNotes = intercalate ", " . map show . filter use
+ where use ValidInstance{} = False -- Not important enough to tell an end user
+ use _ = True
+
+
data Setting
= Classify {severityS :: Severity, hintS :: String, funcS :: FuncName}
- | MatchExp {severityS :: Severity, hintS :: String, scope :: Scope, lhs :: Exp_, rhs :: Exp_, side :: Maybe Exp_, notes :: String}
+ | MatchExp {severityS :: Severity, hintS :: String, scope :: Scope, lhs :: Exp_, rhs :: Exp_, side :: Maybe Exp_, notes :: [Note]}
| Builtin String -- use a builtin hint set
| Infix Fixity
deriving Show
@@ -122,11 +144,25 @@
readPragma _ = Nothing
-readSide :: [Decl_] -> (Maybe Exp_, String)
-readSide = foldl f (Nothing,"")
- where f (Nothing,warn) (PatBind _ PWildCard{} Nothing (UnGuardedRhs _ side) Nothing) = (Just side, warn)
- f (side,"") (PatBind _ (fromNamed -> "note") Nothing (UnGuardedRhs _ (Lit _ (String _ warn _))) Nothing) = (side,warn)
+readSide :: [Decl_] -> (Maybe Exp_, [Note])
+readSide = foldl f (Nothing,[])
+ where f (Nothing,notes) (PatBind _ PWildCard{} Nothing (UnGuardedRhs _ side) Nothing) = (Just side, notes)
+ f (side,[]) (PatBind _ (fromNamed -> "note") Nothing (UnGuardedRhs _ note) Nothing) = (side,g note)
f _ x = errorOn x "bad side condition"
+
+ g (Lit _ (String _ x _)) = [Note x]
+ g (List _ xs) = concatMap g xs
+ g x = case fromApps x of
+ [con -> Just "IncreasesLaziness"] -> [IncreasesLaziness]
+ [con -> Just "DecreasesLaziness"] -> [DecreasesLaziness]
+ [con -> Just "RemovesError",str -> Just a] -> [RemovesError a]
+ [con -> Just "ValidInstance",str -> Just a,var -> Just b] -> [ValidInstance a b]
+ _ -> errorOn x "bad note"
+
+ con :: Exp_ -> Maybe String
+ con c@Con{} = Just $ prettyPrint c; con _ = Nothing
+ var c@Var{} = Just $ prettyPrint c; var _ = Nothing
+ str c = if isString c then Just $ fromString c else Nothing
-- Note: Foo may be ("","Foo") or ("Foo",""), return both
diff --git a/src/Test.hs b/src/Test.hs
--- a/src/Test.hs
+++ b/src/Test.hs
@@ -107,9 +107,14 @@
where
matches = filter isMatchExp hints
+ -- Hack around haskell98 not being compatible with base anymore
+ hackImport i@ImportDecl{importAs=Just a,importModule=b}
+ | prettyPrint b `elem` words "Maybe List Monad IO Char" = i{importAs=Just b,importModule=a}
+ hackImport i = i
+
contents =
["{-# LANGUAGE NoMonomorphismRestriction, ExtendedDefaultRules #-}"] ++
- concat (take 1 [map prettyPrint $ scopeImports $ scope x | x <- matches]) ++
+ concat [map (prettyPrint . hackImport) $ scopeImports $ scope x | x <- take 1 matches] ++
["main = return ()"
,"(==>) :: a -> a -> a; (==>) = undefined"
,"_noParen_ = id"