CurryInfo: contract-prover-4.0.0 / ContractProver.addPostConditionCheck

 
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

 argument 2

 deterministic operation

 
Adds a postcondition check to a program rule of a given operation.

 <FAILING>

 referentially transparent operation

 no fixity defined

 {(_,{AExternal}) |-> _ || ({(,)},{ARule}) |-> {AComb}}

 addPostConditionCheck

 no precedence defined

 _

 (String, String) -> FlatCurry.Annotated.Types.ARule FlatCurry.Types.TypeExpr
-> FlatCurry.Annotated.Types.AExpr FlatCurry.Types.TypeExpr

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term