|
definition:
|
genTestFuncs :: Options -> (QName -> Bool) -> (QName -> Productivity) -> String
-> TestModule -> IO [CFuncDecl]
genTestFuncs opts terminating productivity mainmod tm =
fmap (filter (not . null . funcRules))
(mapM genTestFunc (propTests tm))
where
genTestFunc test = case test of
PropTest name t _ -> testFuncWithRules (propBody name t test)
IOTest name _ -> testFuncWithRules (ioTestBody name test)
EquivTest name f1 f2 t _ ->
-- if the test name has suffix "'TERMINATE" or the operations
-- to be tested are terminating, the test for terminating
-- operations is used:
if "'TERMINATE" `isSuffixOf` map toUpper (snd name) ||
(isTerminating f1 && isTerminating f2)
then do putStrLnIfDebug opts $
"Generating equivalence test for TERMINATING " ++
"operations for test: " ++ snd name
testFuncWithRules $ equivBodyTerm f1 f2 t test
else
-- if the test name has suffix "'PRODUCTIVE" or the
-- operations to be tested are productive,
-- the test for arbitrary operations is used
-- (which limits the size of computed
-- results but might find counter-examples later),
-- otherwise the test is omitted if we are in the "safe"
-- mode:
if "'PRODUCTIVE" `isSuffixOf` map toUpper (snd name) ||
optEquiv opts /= Safe ||
(isProductive f1 && isProductive f2)
then do putStrLnIfDebug opts $
"Generating equivalence test for PRODUCTIVE " ++
"operations for test: " ++ snd name
testFuncWithRules $ equivBodyAny f1 f2 t test
else testFuncWithRules []
where
testFuncWithRules rs =
return $ cfunc (mainmod, genTestName test) 0 Public
(emptyClassType (ioType (maybeType stringType))) rs
isTerminating f = terminating f || productivity f == Terminating
isProductive f = productivity f `notElem` [NoInfo, Looping]
msgOf test = string2ac $ genTestMsg (orgModuleName tm) test
testmname = testModuleName tm
easyCheckFuncName arity =
if arity>maxArity
then error $ "Properties with more than " ++ show maxArity ++
" parameters are currently not supported!"
else (easyCheckExecModule,"checkWithValues" ++ show arity)
-- Operation equivalence test for terminating operations:
equivBodyTerm f1 f2 texp test =
let xvars = map (\i -> (i,"x" ++ show i)) [1 .. arityOfType texp]
pxvars = map (\i -> (i,"px" ++ show i)) [1 .. arityOfType texp]
pvalOfFunc = ctype2typeop mainmod "pvalOf_" (resultType texp)
in propOrEquivBody
(map (\t -> ctype2BotType mainmod False t) (argTypes texp))
test
(cLambda (map CPVar pxvars)
(letExpr
(map (\ (x,px,te) -> CLocalPat (CPVar x)
(CSimpleRhs (applyE (ctype2typeop mainmod "from_P_" te)
[CVar px]) []))
(zip3 xvars pxvars (argTypes texp)))
(addPreCond (preConditions tm) [f1,f2] xvars
(applyF (easyCheckModule,"<~>")
[applyE pvalOfFunc [applyF f1 (map CVar xvars)],
applyE pvalOfFunc [applyF f2 (map CVar xvars)]]))))
-- Operation equivalence test for arbitrary operations:
equivBodyAny f1 f2 texp test =
let xvars = map (\i -> (i,"x" ++ show i)) [1 .. arityOfType texp]
pxvars = map (\i -> (i,"px" ++ show i)) [1 .. arityOfType texp]
pvar = (2,"p")
pvalOfFunc = ctype2typeop mainmod "peval_" (resultType texp)
in propOrEquivBody
(map (\t -> ctype2BotType mainmod False t) (argTypes texp) ++
[ctype2BotType mainmod True (resultType texp)])
test
(cLambda (map CPVar pxvars ++ [CPVar pvar])
(letExpr
(map (\ (x,px,te) -> CLocalPat (CPVar x)
(CSimpleRhs (applyE (ctype2typeop mainmod "from_P_" te)
[CVar px]) []))
(zip3 xvars pxvars (argTypes texp)))
(addPreCond (preConditions tm) [f1,f2] xvars
(applyF (easyCheckModule,"<~>")
[applyE pvalOfFunc [applyF f1 (map CVar xvars), CVar pvar],
applyE pvalOfFunc [applyF f2 (map CVar xvars), CVar pvar]]))))
propBody qname texp test =
propOrEquivBody (map (\t -> t) (argTypes texp))
test (CSymbol (testmname,snd qname))
propOrEquivBody argtypes test propexp =
[simpleRule [] $
CLetDecl [CLocalPat (CPVar msgvar) (CSimpleRhs (msgOf test) [])]
(applyF (easyCheckExecModule, "checkPropWithMsg")
[ CVar msgvar
, applyF (easyCheckFuncName (length argtypes)) $
[configOpWithMaxFail, CVar msgvar] ++
(map (\ t ->
applyF (easyCheckModule,"valuesOfSearchTree")
[if isPAKCS || useUserDefinedGen t || isFloatType t
then type2genop mainmod tm True t
else applyF (searchTreeModule,"someSearchTree")
[CTyped (constF (pre "unknown"))
(emptyClassType t)]])
argtypes) ++
[transFuncArgsInProp mainmod argtypes propexp]
])]
where
useUserDefinedGen texp = case texp of
CTVar _ -> error "No polymorphic generator!"
CFuncType _ _ -> True
CTApply _ _ -> maybe (error "No generator for type applications!")
(\ (qt,_) -> hasDefinedGen qt)
(tconsArgsOfType texp)
CTCons qt -> hasDefinedGen qt
where
hasDefinedGen (mn,tc) =
isJust (find (\qn -> "gen"++tc == snd qn) (generators tm)) ||
mn==mainmod && "_Constant" `isSuffixOf` tc
configOpWithMaxTest =
let n = optMaxTest opts
in if n==0 then stdConfigOp
else applyF (easyCheckExecModule,"setMaxTest")
[cInt n, stdConfigOp]
configOpWithMaxFail =
let n = optMaxFail opts
in if n==0 then configOpWithMaxTest
else applyF (easyCheckExecModule,"setMaxFail")
[cInt n, configOpWithMaxTest]
msgvar = (0,"msg")
stdConfigOp = constF (easyCheckConfig opts)
ioTestBody (_, name) test =
[simpleRule [] $ applyF (easyCheckExecModule,"checkPropIOWithMsg")
[stdConfigOp, msgOf test, CSymbol (testmname,name)]]
|