Permalink
Browse files

Integreate new hlint recommendations

  • Loading branch information...
1 parent 36e352c commit df1e7e172a539270f4edc230eae9220da8466975 @LeventErkok committed Feb 14, 2013
View
@@ -77,9 +77,9 @@ extractMap isSat qinps _modelMap solverLines =
sortByNodeId = sortBy (compare `on` fst)
inps -- for "sat", display the prefix existentials. For completeness, we will drop
-- only the trailing foralls. Exception: Don't drop anything if it's all a sequence of foralls
- | isSat = if all (== ALL) (map fst qinps)
- then map snd qinps
- else map snd $ reverse $ dropWhile ((== ALL) . fst) $ reverse qinps
+ | isSat = map snd $ if all (== ALL) (map fst qinps)
+ then qinps
+ else reverse $ dropWhile ((== ALL) . fst) $ reverse qinps
-- for "proof", just display the prefix universals
| True = map snd $ takeWhile ((== ALL) . fst) qinps
-- CVC4 puts quotes around echo's, go figure. strip them here
@@ -329,9 +329,9 @@ compileToSMTLib smtLib2 isSat a = do
cvt = if smtLib2 then toSMTLib2 else toSMTLib1
(_, _, _, _, smtLibPgm) <- simulate cvt defaultSMTCfg isSat comments a
let out = show smtLibPgm
- if smtLib2 -- append check-sat in case of smtLib2
- then return $ out ++ "\n(check-sat)\n"
- else return $ out ++ "\n"
+ return $ out ++ if smtLib2 -- append check-sat in case of smtLib2
+ then "\n(check-sat)\n"
+ else "\n"
-- | Create both SMT-Lib1 and SMT-Lib2 benchmarks. The first argument is the basename of the file,
-- SMT-Lib1 version will be written with suffix ".smt1" and SMT-Lib2 version will be written with
View
@@ -93,9 +93,9 @@ extractMap isSat qinps _modelMap solverLines =
sortByNodeId = sortBy (compare `on` fst)
inps -- for "sat", display the prefix existentials. For completeness, we will drop
-- only the trailing foralls. Exception: Don't drop anything if it's all a sequence of foralls
- | isSat = if all (== ALL) (map fst qinps)
- then map snd qinps
- else map snd $ reverse $ dropWhile ((== ALL) . fst) $ reverse qinps
+ | isSat = map snd $ if all (== ALL) (map fst qinps)
+ then qinps
+ else reverse $ dropWhile ((== ALL) . fst) $ reverse qinps
-- for "proof", just display the prefix universals
| True = map snd $ takeWhile ((== ALL) . fst) qinps
squashReals :: [(Int, (String, CW))] -> [(Int, (String, CW))]
View
@@ -429,9 +429,9 @@ runSolver cfg execPath opts script
ex <- waitForProcess pid
-- if the status is unknown, prepare for the possibility of not having a model
-- TBD: This is rather crude and potentially Z3 specific
- if "unknown" `isPrefixOf` r && "error" `isInfixOf` (out ++ err)
- then return (ExitSuccess, r , "")
- else return (ex, r ++ "\n" ++ out, err)
+ return $ if "unknown" `isPrefixOf` r && "error" `isInfixOf` (out ++ err)
+ then (ExitSuccess, r , "")
+ else (ex, r ++ "\n" ++ out, err)
return (send, ask, cleanUp)
mapM_ send (lines (scriptBody script))
r <- ask $ satCmd cfg
View
@@ -4,7 +4,6 @@
# in the distribution for details.
SHELL := /usr/bin/env bash
TSTSRCS = $(shell find . -name '*.hs' -or -name '*.lhs' | grep -v SBVUnitTest/SBVUnitTest.hs | grep -v SBVUnitTest/SBVBasicTests.hs | grep -v buildUtils/simplify.hs)
-LINTSRCS = $(shell find . -name '*.hs' -or -name '*.lhs' | grep -v Paths_sbv.hs)
STAMPFILE = SBVUnitTest/SBVUnitTestBuildTime.hs
DEPSRCS = $(shell find . -name '*.hs' -or -name '*.lhs' -or -name '*.cabal' | grep -v Paths_sbv.hs | grep -v $(STAMPFILE))
CABAL = cabal
@@ -72,7 +71,7 @@ gold: install
hlint: install
@echo "Running HLint.."
- @hlint ${LINTSRCS} -q -rhlintReport.html -i "Use otherwise" -i "Parse error"
+ @hlint Data SBVUnitTest -q -rhlintReport.html -i "Use otherwise" -i "Parse error"
tags:
$(call mkTags)
@@ -77,8 +77,9 @@ decide shouldCreate (Counts c t e f) = do
when (e /= 0) $ putStrLn $ "*** " ++ show e ++ " (of " ++ show c ++ ") test cases in error."
when (f /= 0) $ putStrLn $ "*** " ++ show f ++ " (of " ++ show c ++ ") test cases failed."
if c == t && e == 0 && f == 0
- then do if shouldCreate
- then putStrLn $ "All " ++ show c ++ " test cases executed in gold-file generation mode."
- else putStrLn $ "All " ++ show c ++ " test cases successfully passed."
+ then do putStrLn $ "All " ++ show c ++ " test cases "
+ ++ (if shouldCreate
+ then " executed in gold-file generation mode."
+ else " successfully passed.")
exitSuccess
else exitWith $ ExitFailure 2
@@ -2,4 +2,4 @@
module SBVUnitTestBuildTime (buildTime) where
buildTime :: String
-buildTime = "Tue Jan 1 22:35:55 PST 2013"
+buildTime = "Wed Feb 13 21:18:38 PST 2013"

0 comments on commit df1e7e1

Please sign in to comment.