CurryInfo: contract-prover-4.0.0 / ContractProver.addPreConditions

 
addPreConditions :: Options -> TAProg -> IORef VState -> IO TAProg
addPreConditions _ prog vstref = do
  newfuns  <- mapM addPreCondition (progFuncs prog)
  return (updProgFuncs (const (concat newfuns)) prog)
 where
  addPreCondition fdecl@(AFunc qf ar vis fty rule) = do
    ti <- readVerifyInfoRef vstref
    return $
      if toPreCondQName qf `elem` map funcName (preConds ti)
        then let newrule = checkPreCondRule qf rule
             in [updFuncRule (const newrule) fdecl,
                 AFunc (toNoCheckQName qf) ar vis fty rule]
        else [fdecl]

  checkPreCondRule :: QName -> TARule -> TARule
  checkPreCondRule qn (ARule rty rargs _) =
    ARule rty rargs (addPreConditionCheck rty FuncCall qn rty
                       (map (\ (v,t) -> AVar t v) rargs))
  checkPreCondRule qn (AExternal _ _) = error $
    "addPreConditions: cannot add precondition to external operation '" ++
    snd qn ++ "'!"

 no demanded arguments

 deterministic operation

 
---------------------------------------------------------------------------
Add (non-trivial) preconditions:
If an operation `f` has some precondition `f'pre`,
replace the rule `f xs = rhs` by the following rules:

    f xs = checkPreCond (f'NOCHECK xs) (f'pre xs) "f" xs
    f'NOCHECK xs = rhs

 <FAILING>

 referentially transparent operation

 no fixity defined

 {(_,_,_) |-> _}

 addPreConditions

 no precedence defined

 _

 ToolOptions.Options -> FlatCurry.Annotated.Types.AProg FlatCurry.Types.TypeExpr
-> Data.IORef.IORef VerifierState.VState
-> Prelude.IO (FlatCurry.Annotated.Types.AProg FlatCurry.Types.TypeExpr)

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term