Module CurryCheck

This is the implementation of the currycheck tool. It performs various checks on Curry programs:

  • Correct usage of set functions, non-strict unification, default rules, DET annotations, contracts
  • All EasyCheck tests are extracted and checked
  • For all functions declared as deterministic, determinism properties are generated and checked.
  • For functions with postconditions (f'post), checks for postconditions are generated (together with possible preconditions)
  • For functions with specification (f'spec), checks for satisfaction of these specifications are generated (together with possible preconditions).

Author: Michael Hanus, Jan-Patrick Baye

Version: February 2023

Summary of exported operations:

ccBanner :: String  Deterministic 
usageText :: String  Non-deterministic 
maxArity :: Int  Deterministic 
Maximal arity of check functions and tuples currently supported:
defTypeSuffix :: String  Deterministic 
postCondSuffix :: String  Deterministic 
satSpecSuffix :: String  Deterministic 
isDetSuffix :: String  Deterministic 
isIOTest :: Test -> Bool  Deterministic 
isUnitTest :: Test -> Bool  Deterministic 
isPropTest :: Test -> Bool  Deterministic 
isEquivTest :: Test -> Bool  Deterministic 
equivTestOps :: Test -> [(String,String)]  Deterministic 
testName :: Test -> (String,String)  Deterministic 
testLine :: Test -> Int  Deterministic 
genTestMsg :: String -> Test -> String  Deterministic 
showModuleLine :: String -> Int -> String  Deterministic 
genTestName :: Test -> String  Deterministic 
staticErrorTestMod :: String -> [String] -> TestModule  Deterministic 
testThisModule :: TestModule -> Bool  Deterministic 
userTestDataOfModule :: TestModule -> [((String,String),Bool)]  Deterministic 
equivPropTypes :: TestModule -> [(String,String)]  Deterministic 
genTestFuncs :: Options -> ((String,String) -> Bool) -> ((String,String) -> Productivity) -> String -> TestModule -> IO [CFuncDecl]  Deterministic 
easyCheckConfig :: Options -> (String,String)  Deterministic 
type2genop :: String -> TestModule -> Bool -> CTypeExpr -> CExpr  Deterministic 
isFloatType :: CTypeExpr -> Bool  Deterministic 
typename2genopname :: String -> [(String,String)] -> (String,String) -> (String,String)  Deterministic 
transQN :: String -> String  Deterministic 
transFuncArgsInProp :: String -> [CTypeExpr] -> CExpr -> CExpr  Deterministic 
makeAllPublic :: CurryProg -> CurryProg  Deterministic 
classifyTest :: Options -> CurryProg -> CFuncDecl -> Test  Non-deterministic 
transformTests :: Options -> [String] -> [CFuncDecl] -> CurryProg -> IO ([CFuncDecl],[CFuncDecl],[(String,String)],CurryProg)  Non-deterministic 
transformDetTests :: Options -> [String] -> CurryProg -> ([CFuncDecl],[CFuncDecl],CurryProg)  Deterministic 
preCondOperations :: [CFuncDecl] -> [(String,String)]  Deterministic 
funDeclsWith :: (String -> Bool) -> [CFuncDecl] -> [CFuncDecl]  Deterministic 
propResultType :: CTypeExpr -> CTypeExpr  Deterministic 
genPostCondTest :: [(String,String)] -> [(String,String)] -> [String] -> CFuncDecl -> [CFuncDecl]  Deterministic 
genSpecTest :: Options -> [(String,String)] -> [(String,String)] -> [String] -> CFuncDecl -> [CFuncDecl]  Deterministic 
genSpecGroundEquivTest :: [(String,String)] -> (String,String) -> CContext -> CTypeExpr -> CFuncDecl  Deterministic 
addPreCond :: [(String,String)] -> [(String,String)] -> [(Int,String)] -> CExpr -> CExpr  Deterministic 
revertDetOpTrans :: [(String,String)] -> CFuncDecl -> CFuncDecl  Deterministic 
genDetOpTests :: [String] -> [(String,String)] -> [CFuncDecl] -> [CFuncDecl]  Deterministic 
genDetProp :: [(String,String)] -> CFuncDecl -> CFuncDecl  Deterministic 
poly2default :: Options -> CFuncDecl -> [(Bool,CFuncDecl)]  Deterministic 
poly2defaultType :: Options -> CTypeExpr -> CTypeExpr  Deterministic 
defaultQualType :: CQualTypeExpr -> CQualTypeExpr  Deterministic 
addShowContext :: CContext -> CContext  Deterministic 
addEqShowContext :: (Int,String) -> CContext -> CContext  Deterministic 
orgTestName :: (String,String) -> (String,String)  Deterministic 
orgQName :: (String,String) -> (String,String)  Deterministic 
analyseModule :: Options -> String -> IO [TestModule]  Non-deterministic 
staticProgAnalysis :: Options -> String -> String -> CurryProg -> IO ([String],[((String,String),String)])  Non-deterministic 
analyseCurryProg :: Options -> String -> CurryProg -> IO [TestModule]  Non-deterministic 
generatorsOfProg :: CurryProg -> [(String,String)]  Deterministic 
genBottomType :: String -> TypeDecl -> CTypeDecl  Deterministic 
isPrimExtType :: (String,String) -> Bool  Deterministic 
defaultValueOfBasicExtType :: String -> CLiteral  Deterministic 
ctype2BotType :: String -> Bool -> CTypeExpr -> CTypeExpr  Deterministic 
t2bt :: String -> String  Deterministic 
genPeval :: String -> TypeDecl -> CFuncDecl  Deterministic 
genPValOf :: String -> TypeDecl -> CFuncDecl  Deterministic 
ftype2pvalOf :: String -> String -> [(Int,String)] -> TypeExpr -> CExpr  Deterministic 
ctype2typeop :: String -> String -> CTypeExpr -> CExpr  Deterministic 
genShowP :: String -> TypeDecl -> CInstanceDecl  Deterministic 
genFromP :: String -> TypeDecl -> CFuncDecl  Deterministic 
ftype2fromP :: String -> String -> [(Int,String)] -> TypeExpr -> CExpr  Deterministic 
ctypedecl2ftypedecl :: CTypeDecl -> TypeDecl  Deterministic 
genMainTestModule :: Options -> String -> [TestModule] -> IO [Test]  Non-deterministic 
genMainFunction :: Options -> String -> [CFuncDecl] -> CFuncDecl  Deterministic 
removeNonExecTests :: Options -> ((String,String) -> [String]) -> [TestModule] -> ([TestModule],[(String,String)])  Deterministic 
collectAllTestTypeDecls :: Options -> [Prog] -> [(TypeDecl,Bool)] -> [((String,String),Bool)] -> IO ([Prog],[(TypeDecl,Bool)])  Non-deterministic 
genTestDataGenerator :: String -> TypeDecl -> CFuncDecl  Deterministic 
genPartialPrimDataGenerator :: String -> (String,String) -> CFuncDecl  Deterministic 
cleanup :: Options -> String -> [TestModule] -> IO ()  Non-deterministic 
printTestStatistics :: Options -> [String] -> String -> Int -> [Test] -> IO ()  Deterministic 
main :: IO ()  Non-deterministic 
checkModules :: Options -> [String] -> IO ()  Non-deterministic 
showGeneratedModule :: Options -> String -> String -> IO ()  Deterministic 
renameProp2EasyCheck :: CurryProg -> CurryProg  Deterministic 
firstWord :: String -> String  Deterministic 
stripSuffix :: String -> String -> String  Deterministic 
modNameToId :: String -> String  Deterministic 
arityOfType :: CTypeExpr -> Int  Deterministic 
searchTreeModule :: String  Deterministic 
Name of the SearchTree module.
searchTreeTC :: (String,String)  Deterministic 
Name of SearchTree type constructor.
generatorModule :: String  Deterministic 
Name of the SearchTreeGenerator module.
choiceGen :: (String,String)  Deterministic 
writeCurryProgram :: Options -> String -> CurryProg -> String -> IO ()  Non-deterministic 
isPAKCS :: Bool  Deterministic 
containsPPOptionLine :: String -> Bool  Deterministic 
tconsOf :: CTypeExpr -> [(String,String)]  Deterministic 
unionOn :: Eq a => (b -> [a]) -> [b] -> [a]  Deterministic 
showCTypeExpr :: CTypeExpr -> String  Deterministic 
showCExpr :: CExpr -> String  Non-deterministic 
cLambda :: [CPattern] -> CExpr -> CExpr  Deterministic 

Exported datatypes:


Test

Constructors:


TestModule

Constructors:

  • TestModule :: String -> String -> [String] -> [Test] -> [QName] -> [QName] -> TestModule

    Fields:

    • orgModuleName :: String
    • testModuleName :: String
    • staticErrors :: [String]
    • propTests :: [Test]
    • generators :: [QName]
    • preConditions :: [QName]

Exported operations:

ccBanner :: String  Deterministic 

usageText :: String  Non-deterministic 

maxArity :: Int  Deterministic 

Maximal arity of check functions and tuples currently supported:

Further infos:
  • solution complete, i.e., able to compute all solutions

defTypeSuffix :: String  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

postCondSuffix :: String  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

satSpecSuffix :: String  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

isDetSuffix :: String  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

isIOTest :: Test -> Bool  Deterministic 

isUnitTest :: Test -> Bool  Deterministic 

isPropTest :: Test -> Bool  Deterministic 

isEquivTest :: Test -> Bool  Deterministic 

equivTestOps :: Test -> [(String,String)]  Deterministic 

testName :: Test -> (String,String)  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

testLine :: Test -> Int  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

genTestMsg :: String -> Test -> String  Deterministic 

showModuleLine :: String -> Int -> String  Deterministic 

genTestName :: Test -> String  Deterministic 

staticErrorTestMod :: String -> [String] -> TestModule  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

testThisModule :: TestModule -> Bool  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

userTestDataOfModule :: TestModule -> [((String,String),Bool)]  Deterministic 

equivPropTypes :: TestModule -> [(String,String)]  Deterministic 

genTestFuncs :: Options -> ((String,String) -> Bool) -> ((String,String) -> Productivity) -> String -> TestModule -> IO [CFuncDecl]  Deterministic 

easyCheckConfig :: Options -> (String,String)  Deterministic 

type2genop :: String -> TestModule -> Bool -> CTypeExpr -> CExpr  Deterministic 

isFloatType :: CTypeExpr -> Bool  Deterministic 

typename2genopname :: String -> [(String,String)] -> (String,String) -> (String,String)  Deterministic 

transQN :: String -> String  Deterministic 

transFuncArgsInProp :: String -> [CTypeExpr] -> CExpr -> CExpr  Deterministic 

transformTests :: Options -> [String] -> [CFuncDecl] -> CurryProg -> IO ([CFuncDecl],[CFuncDecl],[(String,String)],CurryProg)  Non-deterministic 

transformDetTests :: Options -> [String] -> CurryProg -> ([CFuncDecl],[CFuncDecl],CurryProg)  Deterministic 

preCondOperations :: [CFuncDecl] -> [(String,String)]  Deterministic 

funDeclsWith :: (String -> Bool) -> [CFuncDecl] -> [CFuncDecl]  Deterministic 

genPostCondTest :: [(String,String)] -> [(String,String)] -> [String] -> CFuncDecl -> [CFuncDecl]  Deterministic 

genSpecTest :: Options -> [(String,String)] -> [(String,String)] -> [String] -> CFuncDecl -> [CFuncDecl]  Deterministic 

genSpecGroundEquivTest :: [(String,String)] -> (String,String) -> CContext -> CTypeExpr -> CFuncDecl  Deterministic 

addPreCond :: [(String,String)] -> [(String,String)] -> [(Int,String)] -> CExpr -> CExpr  Deterministic 

revertDetOpTrans :: [(String,String)] -> CFuncDecl -> CFuncDecl  Deterministic 

genDetOpTests :: [String] -> [(String,String)] -> [CFuncDecl] -> [CFuncDecl]  Deterministic 

genDetProp :: [(String,String)] -> CFuncDecl -> CFuncDecl  Deterministic 

poly2default :: Options -> CFuncDecl -> [(Bool,CFuncDecl)]  Deterministic 

poly2defaultType :: Options -> CTypeExpr -> CTypeExpr  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

addEqShowContext :: (Int,String) -> CContext -> CContext  Deterministic 

orgTestName :: (String,String) -> (String,String)  Deterministic 

orgQName :: (String,String) -> (String,String)  Deterministic 

analyseModule :: Options -> String -> IO [TestModule]  Non-deterministic 

staticProgAnalysis :: Options -> String -> String -> CurryProg -> IO ([String],[((String,String),String)])  Non-deterministic 

analyseCurryProg :: Options -> String -> CurryProg -> IO [TestModule]  Non-deterministic 

generatorsOfProg :: CurryProg -> [(String,String)]  Deterministic 

genBottomType :: String -> TypeDecl -> CTypeDecl  Deterministic 

isPrimExtType :: (String,String) -> Bool  Deterministic 

ctype2BotType :: String -> Bool -> CTypeExpr -> CTypeExpr  Deterministic 

t2bt :: String -> String  Deterministic 

genPeval :: String -> TypeDecl -> CFuncDecl  Deterministic 

genPValOf :: String -> TypeDecl -> CFuncDecl  Deterministic 

ftype2pvalOf :: String -> String -> [(Int,String)] -> TypeExpr -> CExpr  Deterministic 

ctype2typeop :: String -> String -> CTypeExpr -> CExpr  Deterministic 

genShowP :: String -> TypeDecl -> CInstanceDecl  Deterministic 

genFromP :: String -> TypeDecl -> CFuncDecl  Deterministic 

ftype2fromP :: String -> String -> [(Int,String)] -> TypeExpr -> CExpr  Deterministic 

genMainTestModule :: Options -> String -> [TestModule] -> IO [Test]  Non-deterministic 

genMainFunction :: Options -> String -> [CFuncDecl] -> CFuncDecl  Deterministic 

removeNonExecTests :: Options -> ((String,String) -> [String]) -> [TestModule] -> ([TestModule],[(String,String)])  Deterministic 

collectAllTestTypeDecls :: Options -> [Prog] -> [(TypeDecl,Bool)] -> [((String,String),Bool)] -> IO ([Prog],[(TypeDecl,Bool)])  Non-deterministic 

genTestDataGenerator :: String -> TypeDecl -> CFuncDecl  Deterministic 

genPartialPrimDataGenerator :: String -> (String,String) -> CFuncDecl  Deterministic 

cleanup :: Options -> String -> [TestModule] -> IO ()  Non-deterministic 

printTestStatistics :: Options -> [String] -> String -> Int -> [Test] -> IO ()  Deterministic 

main :: IO ()  Non-deterministic 

checkModules :: Options -> [String] -> IO ()  Non-deterministic 

showGeneratedModule :: Options -> String -> String -> IO ()  Deterministic 

firstWord :: String -> String  Deterministic 

stripSuffix :: String -> String -> String  Deterministic 

modNameToId :: String -> String  Deterministic 

arityOfType :: CTypeExpr -> Int  Deterministic 

searchTreeModule :: String  Deterministic 

Name of the SearchTree module.

Further infos:
  • solution complete, i.e., able to compute all solutions

searchTreeTC :: (String,String)  Deterministic 

Name of SearchTree type constructor.

Further infos:
  • solution complete, i.e., able to compute all solutions

generatorModule :: String  Deterministic 

Name of the SearchTreeGenerator module.

Further infos:
  • solution complete, i.e., able to compute all solutions

choiceGen :: (String,String)  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

writeCurryProgram :: Options -> String -> CurryProg -> String -> IO ()  Non-deterministic 

isPAKCS :: Bool  Deterministic 

containsPPOptionLine :: String -> Bool  Deterministic 

tconsOf :: CTypeExpr -> [(String,String)]  Deterministic 

unionOn :: Eq a => (b -> [a]) -> [b] -> [a]  Deterministic 

showCTypeExpr :: CTypeExpr -> String  Deterministic 

showCExpr :: CExpr -> String  Non-deterministic 

cLambda :: [CPattern] -> CExpr -> CExpr  Deterministic