Commit 02ca5686 authored by Michael Hanus 's avatar Michael Hanus

Loads only module-relevant proof files

parent 40441970
...@@ -39,24 +39,25 @@ import FlatCurry.Files ...@@ -39,24 +39,25 @@ import FlatCurry.Files
import qualified FlatCurry.Goodies as FCG import qualified FlatCurry.Goodies as FCG
import Text.Pretty ( pPrint ) import Text.Pretty ( pPrint )
import CC.AnalysisHelpers ( getTerminationInfos, getProductivityInfos import CC.AnalysisHelpers ( getTerminationInfos, getProductivityInfos
, getUnsafeModuleInfos, dropPublicSuffix ) , getUnsafeModuleInfos, dropPublicSuffix )
import CC.Config ( packagePath, packageVersion ) import CC.Config ( packagePath, packageVersion )
import CC.Options import CC.Options
import CheckDetUsage ( checkDetUse, containsDetOperations) import CheckDetUsage ( checkDetUse, containsDetOperations)
import ContractUsage import ContractUsage
import DefaultRuleUsage ( checkDefaultRules, containsDefaultRules ) import DefaultRuleUsage ( checkDefaultRules, containsDefaultRules )
import PropertyUsage import PropertyUsage
import SimplifyPostConds ( simplifyPostConditionsWithTheorems ) import SimplifyPostConds ( simplifyPostConditionsWithTheorems )
import TheoremUsage import TheoremUsage ( determinismTheoremFor, existsProofFor
import UsageCheck ( checkBlacklistUse, checkSetUse ) , getModuleProofFiles, getTheoremFunctions )
import UsageCheck ( checkBlacklistUse, checkSetUse )
-- Banner of this tool: -- Banner of this tool:
ccBanner :: String ccBanner :: String
ccBanner = unlines [bannerLine,bannerText,bannerLine] ccBanner = unlines [bannerLine,bannerText,bannerLine]
where where
bannerText = "CurryCheck: a tool for testing Curry programs (Version " ++ bannerText = "CurryCheck: a tool for testing Curry programs (Version " ++
packageVersion ++ " of 30/10/2018)" packageVersion ++ " of 31/10/2018)"
bannerLine = take (length bannerText) (repeat '-') bannerLine = take (length bannerText) (repeat '-')
-- Help text -- Help text
...@@ -870,7 +871,9 @@ analyseCurryProg opts modname orgprog = do ...@@ -870,7 +871,9 @@ analyseCurryProg opts modname orgprog = do
maybe (error $ "Source file of module '"++modname++"' not found!") id maybe (error $ "Source file of module '"++modname++"' not found!") id
let srcdir = takeDirectory srcfilename let srcdir = takeDirectory srcfilename
putStrLnIfDebug opts $ "Source file: " ++ srcfilename putStrLnIfDebug opts $ "Source file: " ++ srcfilename
prooffiles <- if optProof opts then getProofFiles srcdir else return [] prooffiles <- if optProof opts
then getModuleProofFiles srcdir modname
else return []
unless (null prooffiles) $ putStrIfDetails opts $ unless (null prooffiles) $ putStrIfDetails opts $
unlines ("Proof files found:" : map ("- " ++) prooffiles) unlines ("Proof files found:" : map ("- " ++) prooffiles)
progtxt <- readFile srcfilename progtxt <- readFile srcfilename
......
...@@ -26,7 +26,7 @@ ...@@ -26,7 +26,7 @@
module TheoremUsage module TheoremUsage
( determinismTheoremFor ( determinismTheoremFor
, getProofFiles, existsProofFor, isProofFileName, isProofFileNameFor , getModuleProofFiles, existsProofFor, isProofFileNameFor
, getTheoremFunctions , getTheoremFunctions
) where ) where
...@@ -50,11 +50,11 @@ determinismTheoremFor funcname = funcname ++ "isdeterministic" ...@@ -50,11 +50,11 @@ determinismTheoremFor funcname = funcname ++ "isdeterministic"
-- Operations for proof files: -- Operations for proof files:
--- Get the names of all files in the directory (first argument) containing --- Get the names of all files in the directory (first argument) containing
--- proofs of theorems. --- proofs of theorems of the module (second argument).
getProofFiles :: String -> IO [String] getModuleProofFiles :: String -> String -> IO [String]
getProofFiles dir = do getModuleProofFiles dir mod = do
files <- getDirectoryContents dir files <- getDirectoryContents dir
return (filter isProofFileName files) return (filter (isModuleProofFileName mod) files)
--- Does the list of file names (second argument) contain a proof of the --- Does the list of file names (second argument) contain a proof of the
--- qualified theorem name given as the first argument? --- qualified theorem name given as the first argument?
...@@ -62,9 +62,12 @@ existsProofFor :: QName -> [String] -> Bool ...@@ -62,9 +62,12 @@ existsProofFor :: QName -> [String] -> Bool
existsProofFor qpropname filenames = existsProofFor qpropname filenames =
any (isProofFileNameFor qpropname) filenames any (isProofFileNameFor qpropname) filenames
--- Is this a file name with a proof, i.e., start it with `proof`? --- Is the second argument a file name with a proof of some theorem of a module
isProofFileName :: String -> Bool --- (first argument), i.e., start it with `proof` and the module name?
isProofFileName fn = "proof" `isPrefixOf` (map toLower fn) isModuleProofFileName :: String -> String -> Bool
isModuleProofFileName mn fn =
deleteNonAlphanNum ("proof" ++ map toLower mn)
`isPrefixOf` deleteNonAlphanNum (map toLower fn)
--- Is this the file name of a proof of property `prop`? --- Is this the file name of a proof of property `prop`?
isProofFileNameFor :: QName -> String -> Bool isProofFileNameFor :: QName -> String -> Bool
...@@ -84,9 +87,9 @@ deleteNonAlphanNum = filter isAlphaNum ...@@ -84,9 +87,9 @@ deleteNonAlphanNum = filter isAlphaNum
--- A theorem is a property for which a proof file exists in the --- A theorem is a property for which a proof file exists in the
--- directory provided as first argument. --- directory provided as first argument.
getTheoremFunctions :: String -> CurryProg -> IO [CFuncDecl] getTheoremFunctions :: String -> CurryProg -> IO [CFuncDecl]
getTheoremFunctions proofdir (CurryProg _ _ _ _ _ _ functions _) = do getTheoremFunctions proofdir (CurryProg mn _ _ _ _ _ functions _) = do
let propfuncs = filter isProperty functions -- all properties let propfuncs = filter isProperty functions -- all properties
prooffiles <- getProofFiles proofdir prooffiles <- getModuleProofFiles proofdir mn
return $ filter (\fd -> existsProofFor (funcName fd) prooffiles) return $ filter (\fd -> existsProofFor (funcName fd) prooffiles)
propfuncs propfuncs
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment