Commit c35604ff authored by Michael Hanus 's avatar Michael Hanus

Loads only module-relevant proof files

parent c3aee946
......@@ -37,22 +37,23 @@ import qualified FlatCurry.Types as FC
import FlatCurry.Files
import qualified FlatCurry.Goodies as FCG
import CC.Config ( packagePath, packageVersion )
import CC.Config ( packagePath, packageVersion )
import CC.Options
import CheckDetUsage ( checkDetUse, containsDetOperations)
import CheckDetUsage ( checkDetUse, containsDetOperations)
import ContractUsage
import DefaultRuleUsage ( checkDefaultRules, containsDefaultRules )
import DefaultRuleUsage ( checkDefaultRules, containsDefaultRules )
import PropertyUsage
import SimplifyPostConds ( simplifyPostConditionsWithTheorems )
import TheoremUsage
import UsageCheck ( checkBlacklistUse, checkSetUse )
import SimplifyPostConds ( simplifyPostConditionsWithTheorems )
import TheoremUsage ( determinismTheoremFor, existsProofFor
, getModuleProofFiles, getTheoremFunctions )
import UsageCheck ( checkBlacklistUse, checkSetUse )
-- Banner of this tool:
ccBanner :: String
ccBanner = unlines [bannerLine,bannerText,bannerLine]
where
bannerText = "CurryCheck: a tool for testing Curry programs (Version " ++
packageVersion ++ " of 30/10/2018)"
packageVersion ++ " of 31/10/2018)"
bannerLine = take (length bannerText) (repeat '-')
-- Help text
......@@ -661,7 +662,9 @@ analyseCurryProg opts modname orgprog = do
maybe (error $ "Source file of module '"++modname++"' not found!") id
let srcdir = takeDirectory 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 $
unlines ("Proof files found:" : map ("- " ++) prooffiles)
progtxt <- readFile srcfilename
......
......@@ -26,7 +26,7 @@
module TheoremUsage
( determinismTheoremFor
, getProofFiles, existsProofFor, isProofFileName, isProofFileNameFor
, getModuleProofFiles, existsProofFor, isProofFileNameFor
, getTheoremFunctions
) where
......@@ -56,6 +56,13 @@ getProofFiles dir = do
files <- getDirectoryContents dir
return (filter isProofFileName files)
--- Get the names of all files in the directory (first argument) containing
--- proofs of theorems of the module (second argument).
getModuleProofFiles :: String -> String -> IO [String]
getModuleProofFiles dir mod = do
files <- getDirectoryContents dir
return (filter (isModuleProofFileName mod) files)
--- Does the list of file names (second argument) contain a proof of the
--- qualified theorem name given as the first argument?
existsProofFor :: QName -> [String] -> Bool
......@@ -66,6 +73,13 @@ existsProofFor qpropname filenames =
isProofFileName :: String -> Bool
isProofFileName fn = "proof" `isPrefixOf` (map toLower fn)
--- Is the second argument a file name with a proof of some theorem of a module
--- (first argument), i.e., start it with `proof` and the module name?
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`?
isProofFileNameFor :: QName -> String -> Bool
isProofFileNameFor (mn,prop) fname =
......@@ -84,9 +98,9 @@ deleteNonAlphanNum = filter isAlphaNum
--- A theorem is a property for which a proof file exists in the
--- directory provided as first argument.
getTheoremFunctions :: String -> CurryProg -> IO [CFuncDecl]
getTheoremFunctions proofdir (CurryProg _ _ _ functions _) = do
getTheoremFunctions proofdir (CurryProg mn _ _ functions _) = do
let propfuncs = filter isProperty functions -- all properties
prooffiles <- getProofFiles proofdir
prooffiles <- getModuleProofFiles proofdir mn
return $ filter (\fd -> existsProofFor (funcName fd) prooffiles)
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