CurryInfo: currycheck-4.0.0 / CurryCheck.genPostCondTest

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) _ _ (CQualType clscon texp) _) =
 if qf `notElem` postops || existsProofFor (orgQName postname) prooffnames
   then []
   else
  [CFunc postname ar Public
    (CQualType clscon (propResultType texp))
    [simpleRule (map CPVar cvars) $
       addPreCond prefuns [qf] cvars 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)
  postprop = applyF (easyCheckModule,"always")
                    [applyF (mn,toPostCondName fn)
                            (map CVar cvars ++ [rcall])]

argument 4

deterministic operation

-- 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) 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))

referentially transparent operation

no fixity defined

genPostCondTest

no precedence defined

{:,[]}

[(String, String)] -> [(String, String)] -> [String]
-> AbstractCurry.Types.CFuncDecl -> [AbstractCurry.Types.CFuncDecl]

operation might suspend on free variables

possibly non-terminating

possibly non-reducible on same data term