|
definition:
|
transformTests :: Options -> [String] -> [CFuncDecl] -> CurryProg
-> IO ([CFuncDecl],[CFuncDecl],[QName],CurryProg)
transformTests opts prfnames theofuncs
prog@(CurryProg mname imps dfltdecl clsdecls instdecls
typeDecls functions opDecls) = do
simpfuncs <- simplifyPostConditionsWithTheorems (optVerb opts) theofuncs funcs
let preCondOps = preCondOperations simpfuncs
postCondOps = map ((\ (mn,fn) -> (mn, fromPostCondName fn)) . funcName)
(funDeclsWith isPostCondName simpfuncs)
specOps = map ((\ (mn,fn) -> (mn, fromSpecName fn)) . funcName)
(funDeclsWith isSpecName simpfuncs)
-- generate post condition tests:
postCondTests =
concatMap (genPostCondTest preCondOps postCondOps prfnames) funcs
-- generate specification tests:
specOpTests = concatMap (genSpecTest opts preCondOps specOps prfnames) funcs
grSpecOpTests = if optEquiv opts == Ground then specOpTests else []
(realtests,ignoredtests) = partition fst $
if not (optProp opts)
then []
else concatMap (poly2default opts) $
-- ignore already proved properties:
filter (\fd -> not (existsProofFor (orgQName (funcName fd))
prfnames))
usertests ++
(if optSpec opts then grSpecOpTests ++ postCondTests else [])
return (map snd realtests ++
(if optSpec opts && optEquiv opts /= Ground then specOpTests else []),
map snd ignoredtests,
preCondOps,
CurryProg mname
(nub (easyCheckModule:imps))
dfltdecl clsdecls instdecls
typeDecls
(simpfuncs ++ map snd (realtests ++ ignoredtests))
opDecls)
where
(rawusertests, funcs) = partition isProperty functions
usertests = if optEquiv opts == Ground
then map equivProp2Ground rawusertests
else rawusertests
-- transform an equivalence property (f1 <=> f2) into a property
-- testing ground equivalence, i.e., f1 x1...xn <~> f2 x1...xn
equivProp2Ground fdecl =
maybe fdecl
(\ _ -> case classifyTest opts prog fdecl of
EquivTest _ f1 f2 texp _ ->
let ar = arityOfType texp
cvars = map (\i -> (i,"x" ++ show i)) [1 .. ar]
in stFunc (funcName fdecl) ar Public (propResultType texp)
[simpleRule (map CPVar cvars)
(applyF (easyCheckModule,"<~>")
[applyF f1 (map CVar cvars),
applyF f2 (map CVar cvars)])]
_ -> error "transformTests: internal error"
)
(isEquivProperty fdecl)
|
|
documentation:
|
-- 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 tuple consisting of all actual tests,
-- all ignored tests, the name of all operations with defined preconditions
-- (needed to generate meaningful equivalence tests),
-- and the public version of the original module.
|
|
signature:
|
CC.Options.Options -> [String] -> [AbstractCurry.Types.CFuncDecl]
-> AbstractCurry.Types.CurryProg
-> Prelude.IO ([AbstractCurry.Types.CFuncDecl], [AbstractCurry.Types.CFuncDecl], [(String, String)], AbstractCurry.Types.CurryProg)
|