| definition: |
addPreCond :: [QName] -> [QName] -> [CVarIName] -> CExpr -> CExpr
addPreCond prefuns fs pvars propexp =
let preconds = concatMap precondCall fs
in if null preconds
then propexp
else applyF (easyCheckModule,"==>")
[foldr1 (\x y -> applyF (pre "&&") [x,y]) preconds, propexp]
where
precondCall qn@(mn,fn) =
if qn `elem` prefuns
then [applyF (mn, toPreCondName fn) (map CVar pvars)]
else []
|
| demand: |
no demanded arguments |
| deterministic: |
deterministic operation |
| documentation: |
-- Adds the preconditions of operations (second argument), if they are -- present in the list of functions with preconditions in the first argument, -- on the given variables to the property expression `propexp`. |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| name: |
addPreCond |
| precedence: |
no precedence defined |
| result-values: |
_ |
| signature: |
[(String, String)] -> [(String, String)] -> [(Prelude.Int, String)] -> AbstractCurry.Types.CExpr -> AbstractCurry.Types.CExpr |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |