| definition: |
nonfailPreCondExpOf :: VerifyInfo -> QName -> TypeExpr -> [(Int,TypeExpr)]
-> TransStateM Term
nonfailPreCondExpOf ti qf ftype args =
if optContract (toolOpts ti)
then do
(fvars,nfcond) <- nonfailCondExpOf ti qf ftype args
precond <- preCondExpOf ti qf (args ++ fvars)
-- simplify term in order to check later for trivial precondition
return (simpTerm (tConj [nfcond,precond]))
else do
(_,rt) <- nonfailCondExpOf ti qf ftype args
return rt
|
| demand: |
argument 1 |
| deterministic: |
deterministic operation |
| documentation: |
-- Returns the conjunction of the non-failure condition and precondition -- (if the tool option `contract` is set) expression for a given operation -- and its arguments (which are assumed to be variable indices). -- Rename all local variables by adding the `freshvar` index to them. |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| name: |
nonfailPreCondExpOf |
| 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 ESMT.Term |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |