| definition: |
addPostConditionCheck :: QName -> TARule -> TAExpr
addPostConditionCheck _ (AExternal _ _) =
error $ "Trying to add postcondition to external function!"
addPostConditionCheck qf@(mn,fn) (ARule _ lhs rhs) =
AComb ty FuncCall
((mn, if showdictsexists then "checkPostCond" else "checkPostCondNoShow"),
showDictTypeOf ty ~> showDictTypeOf tt
~> ty ~> (ty ~> boolType) ~> stringType ~> tt ~> ty)
(-- add Show dictionary arguments of types ty and tt, if both exist:
(if showdictsexists then catMaybes showdicts else []) ++
[ rhs
, AComb boolType (FuncPartCall 1) (toPostCondQName qf, ty) args
, string2TAFCY fn
, tupleExpr args
])
where
args = map (\ (i,t) -> AVar t i) lhs
tt = tupleType (map annExpr args)
ty = annExpr (last args)
showdicts = [showDictOf ty, showDictOf tt]
showdictsexists = all isJust showdicts
|
| demand: |
argument 2 |
| deterministic: |
deterministic operation |
| documentation: |
-- Adds a postcondition check to a program rule of a given operation. |
| failfree: |
<FAILING> |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| iotype: |
{(_,{AExternal}) |-> _ || ({(,)},{ARule}) |-> {AComb}}
|
| name: |
addPostConditionCheck |
| precedence: |
no precedence defined |
| result-values: |
_ |
| signature: |
(String, String) -> FlatCurry.Annotated.Types.ARule FlatCurry.Types.TypeExpr -> FlatCurry.Annotated.Types.AExpr FlatCurry.Types.TypeExpr |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |