diff --git a/src/CurryCheck.curry b/src/CurryCheck.curry index 6876eb1e2ecfb8d4705a6116bdac6e66a394a5c0..085deec880bb2c2bc60955f634cd7ca0c19e3b02 100644 --- a/src/CurryCheck.curry +++ b/src/CurryCheck.curry @@ -14,7 +14,7 @@ --- (together with possible preconditions). --- --- @author Michael Hanus, Jan-Patrick Baye ---- @version October 2018 +--- @version November 2018 ------------------------------------------------------------------------- import AnsiCodes @@ -53,7 +53,7 @@ ccBanner :: String ccBanner = unlines [bannerLine,bannerText,bannerLine] where bannerText = "CurryCheck: a tool for testing Curry programs (Version " ++ - packageVersion ++ " of 31/10/2018)" + packageVersion ++ " of 01/11/2018)" bannerLine = take (length bannerText) (repeat '-') -- Help text @@ -389,13 +389,15 @@ classifyTests opts prog = map makeProperty -- Extracts all tests from a given Curry module and transforms -- all polymorphic tests into tests on a base type. +-- The second argument contains the names of existing proof files. +-- It is used to ignore tests when the properties are already proved. -- The third argument contains the list of function representing -- proved properties. It is used to simplify post conditions to be tested. -- The result contains a triple consisting of all actual tests, -- all ignored tests, and the public version of the original module. -transformTests :: Options -> String -> [CFuncDecl] -> CurryProg +transformTests :: Options -> [String] -> [CFuncDecl] -> CurryProg -> IO ([CFuncDecl],[CFuncDecl],CurryProg) -transformTests opts srcdir theofuncs +transformTests opts prfnames theofuncs prog@(CurryProg mname imps typeDecls functions opDecls) = do simpfuncs <- simplifyPostConditionsWithTheorems (optVerb opts) theofuncs funcs let preCondOps = preCondOperations simpfuncs @@ -404,16 +406,18 @@ transformTests opts srcdir theofuncs specOps = map ((\ (mn,fn) -> (mn, fromSpecName fn)) . funcName) (funDeclsWith isSpecName simpfuncs) -- generate post condition tests: - postCondTests = concatMap (genPostCondTest preCondOps postCondOps) funcs + postCondTests = + concatMap (genPostCondTest preCondOps postCondOps prfnames) funcs -- generate specification tests: - specOpTests = concatMap (genSpecTest preCondOps specOps) funcs + specOpTests = concatMap (genSpecTest preCondOps specOps prfnames) funcs (realtests,ignoredtests) = partition fst $ if not (optProp opts) then [] else concatMap (poly2default opts) $ -- ignore already proved properties: - filter (\fd -> funcName fd `notElem` map funcName theofuncs) + filter (\fd -> not (existsProofFor (orgQName (funcName fd)) + prfnames)) usertests ++ (if optSpec opts then postCondTests ++ specOpTests else []) return (map snd realtests, @@ -480,22 +484,25 @@ propResultType te = case te of -- Transforms a function declaration into a post condition test if -- there is a post condition for this function (i.e., a relation named --- f'post). The post condition test is of the form --- fSatisfiesPostCondition x1...xn y = always (f'post x1...xn (f x1...xn)) -genPostCondTest :: [QName] -> [QName] -> CFuncDecl -> [CFuncDecl] -genPostCondTest prefuns postops (CmtFunc _ qf ar vis texp rules) = - genPostCondTest prefuns postops (CFunc qf ar vis texp rules) -genPostCondTest prefuns postops (CFunc qf@(mn,fn) _ _ texp _) = - if qf `notElem` postops then [] else - [CFunc (mn, fn ++ postCondSuffix) ar Public - (propResultType texp) - [simpleRule (map CPVar cvars) $ - if qf `elem` prefuns - then applyF (easyCheckModule,"==>") - [applyF (mn,toPreCondName fn) (map CVar cvars), postprop] - else postprop - ]] +-- f'post) and there is no proof file for this post condition. +-- The generated post condition test is of the form +-- fSatisfiesPostCondition x1...xn y = always (f'post x1...xn (f x1...xn)) +genPostCondTest :: [QName] -> [QName] -> [String] -> CFuncDecl -> [CFuncDecl] +genPostCondTest prefuns postops prooffnames (CmtFunc _ qf ar vis texp rules) = + genPostCondTest prefuns postops prooffnames (CFunc qf ar vis texp rules) +genPostCondTest prefuns postops prooffnames (CFunc qf@(mn,fn) _ _ texp _) = + if qf `notElem` postops || existsProofFor (orgQName postname) prooffnames + then [] + else + [CFunc postname ar Public (propResultType texp) + [simpleRule (map CPVar cvars) $ + if qf `elem` prefuns + then applyF (easyCheckModule,"==>") + [applyF (mn,toPreCondName fn) (map CVar cvars), postprop] + else postprop + ]] where + postname = (mn, fn ++ postCondSuffix) -- name of generated post cond. test ar = arityOfType texp cvars = map (\i -> (i,"x"++show i)) [1 .. ar] rcall = applyF qf (map CVar cvars) @@ -505,23 +512,26 @@ genPostCondTest prefuns postops (CFunc qf@(mn,fn) _ _ texp _) = -- Transforms a function declaration into a specification test if -- there is a specification for this function (i.e., an operation named --- f'spec). The specification test is of the form --- fSatisfiesSpecification x1...xn = --- f'pre x1...xn ==> (f x1...xn <~> f'spec x1...xn) -genSpecTest :: [QName] -> [QName] -> CFuncDecl -> [CFuncDecl] -genSpecTest prefuns specops (CmtFunc _ qf ar vis texp rules) = - genSpecTest prefuns specops (CFunc qf ar vis texp rules) -genSpecTest prefuns specops (CFunc qf@(mn,fn) _ _ texp _) = - if qf `notElem` specops then [] else - [CFunc (mn, fn ++ satSpecSuffix) ar Public - (propResultType texp) - [simpleRule (map CPVar cvars) $ - addPreCond (applyF (easyCheckModule,"<~>") - [applyF qf (map CVar cvars), - applyF (mn,toSpecName fn) (map CVar cvars)])]] +-- f'spec) and there is no proof file for the satisfaction of the specification. +-- The generated specification test is of the form +-- fSatisfiesSpecification x1...xn = +-- f'pre x1...xn ==> (f x1...xn <~> f'spec x1...xn) +genSpecTest :: [QName] -> [QName] -> [String] -> CFuncDecl -> [CFuncDecl] +genSpecTest prefuns specops prooffnames (CmtFunc _ qf ar vis texp rules) = + genSpecTest prefuns specops prooffnames (CFunc qf ar vis texp rules) +genSpecTest prefuns specops prooffnames (CFunc qf@(mn,fn) _ _ texp _) = + if qf `notElem` specops || existsProofFor (orgQName sptname) prooffnames + then [] + else + [CFunc sptname ar Public (propResultType texp) + [simpleRule (map CPVar cvars) $ + addPreCond (applyF (easyCheckModule,"<~>") + [applyF qf (map CVar cvars), + applyF (mn,toSpecName fn) (map CVar cvars)])]] where - cvars = map (\i -> (i,"x"++show i)) [1 .. ar] - ar = arityOfType texp + sptname = (mn, fn ++ satSpecSuffix) -- name of generated specification test + cvars = map (\i -> (i,"x"++show i)) [1 .. ar] + ar = arityOfType texp addPreCond exp = if qf `elem` prefuns then applyF (easyCheckModule,"==>") @@ -612,6 +622,20 @@ orgTestName (mn,tname) = orgTestName (mn, stripSuffix tname satSpecSuffix) | otherwise = (mn,tname) +-- Transforms a possibly changed qualified name, e.g., `("Mod_PUBLIC","f")` +-- or `("Mod_PUBLICDET","f")`, back to its original name by removing the +-- module suffix. +orgQName :: QName -> QName +orgQName (mn,fn) + | publicSuffix `isSuffixOf` mn + = (stripSuffix mn publicSuffix, fn) + | publicdetSuffix `isSuffixOf` mn + = (stripSuffix mn publicdetSuffix, fn) + | otherwise = (mn,fn) + where + publicSuffix = "_PUBLIC" + publicdetSuffix = "_PUBLICDET" + -- This function implements the first phase of CurryCheck: it analyses -- a module to be checked, i.e., it finds the tests, creates new tests -- (e.g., for polymorphic properties, deterministic functions, post @@ -680,7 +704,7 @@ analyseCurryProg opts modname orgprog = do | otherwise = mn theopubfuncs = map (updQNamesInCFuncDecl rnm2pub) theofuncs (rawTests,ignoredTests,pubmod) <- - transformTests opts srcdir theopubfuncs + transformTests opts prooffiles theopubfuncs . renameCurryModule pubmodname . makeAllPublic $ prog let (rawDetTests,ignoredDetTests,pubdetmod) = transformDetTests opts prooffiles diff --git a/src/TheoremUsage.curry b/src/TheoremUsage.curry index 2e2c35f91c194d5abd0673a65a6081c21d14b75c..d236676e274cdd83343887e5b8af0aed6c0f486f 100644 --- a/src/TheoremUsage.curry +++ b/src/TheoremUsage.curry @@ -49,13 +49,6 @@ determinismTheoremFor funcname = funcname ++ "isdeterministic" ------------------------------------------------------------------------ -- Operations for proof files: ---- Get the names of all files in the directory (first argument) containing ---- proofs of theorems. -getProofFiles :: String -> IO [String] -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] @@ -69,10 +62,6 @@ existsProofFor :: QName -> [String] -> Bool existsProofFor qpropname filenames = any (isProofFileNameFor qpropname) filenames ---- Is this a file name with a proof, i.e., start it with `proof`? -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