| definition: |
nonfailCondExpOf :: VerifyInfo -> QName -> TypeExpr -> [(Int,TypeExpr)]
-> TransStateM ([(Int,TypeExpr)], Term)
nonfailCondExpOf ti qf ftype args =
maybe
(predefs qf)
(\fd -> let moreargs = funcArity fd - length args in
if moreargs > 0
then do
-- eta-expand function call with fresh variables so that one
-- can check non-fail conditions with a greater arity:
let etatypes = argTypes (dropArgTypes (length args) ftype)
fvars <- getFreshVarsForTypes (take moreargs etatypes)
rt <- applyFunc fd (args ++ fvars) >>= pred2SMT
return (fvars,rt)
else if moreargs < 0
then error $ "Operation '" ++ snd qf ++
"': nonfail condition has too few arguments!"
else do rt <- applyFunc fd args >>= pred2SMT
return ([],rt) )
(find (\fd -> decodeContractQName (funcName fd) == toNonFailQName qf)
(nfConds ti))
where
predefs qn | qn `elem` [pre "failed", pre "=:="] ||
(qn == pre "error" && optError (toolOpts ti))
= return ([], tFalse)
| otherwise
= return ([], tTrue)
|
| demand: |
no demanded arguments |
| deterministic: |
deterministic operation |
| documentation: |
-- Returns the non-failure condition expression for a given operation -- and its arguments (which are assumed to be variable indices). -- All local variables are renamed by adding the `freshvar` index to them. -- If the non-failure condition requires more arguments (due to a -- higher-order call), fresh arguments are added which are also returned. |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| name: |
nonfailCondExpOf |
| precedence: |
no precedence defined |
| result-values: |
_ |
| signature: |
VerifierState.VerifyInfo -> (String, String) -> FlatCurry.Types.TypeExpr -> [(Prelude.Int, FlatCurry.Types.TypeExpr)] -> Control.Monad.Trans.State.StateT TransState Prelude.IO ([(Prelude.Int, FlatCurry.Types.TypeExpr)], ESMT.Term) |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |