CurryInfo: verify-non-fail-2.0.0 / Verify.WithSMT.fun2SMT
definition: 
|
fun2SMT :: FuncDecl -> Maybe ([Ident],FunSig,Term)
fun2SMT (Func qn _ _ texp rule) = do
let fsig = FunSig (transOpName qn)
(map type2sort (argTypes texp))
(type2sort (resultType texp))
srule <- rule2SMT rule
let tpars = union (typeParamsOfFunSig fsig) (typeParamsOfTerm srule)
return (tpars, fsig, srule)
where
rule2SMT (External s) = return $
tEqu (tComb (transOpName qn) []) (tComb ("External:" ++ s) [])
rule2SMT (Rule vs exp) = do
let isnd = ndExpr exp
lhs = tComb (transOpName qn) (map TSVar vs)
(rhs,varsorts) <- exp2SMTWithVars (maximum (0:vs))
(if isnd then Just lhs else Nothing)
(simpExpr exp)
return $
Forall (map (\ (v,t) -> SV v (type2sort t))
(funcType2TypedVars vs texp))
(Exists (map (\ (v,s) -> SV v s) varsorts)
(if isnd then rhs else tEqu lhs rhs))
|
|
demand:
|
argument 1 |
|
deterministic:
|
deterministic operation |
|
documentation:
|
------------------------------------------------------------------------ Translates a function declaration into a (possibly polymorphic) SMT function declaration. |
|
failfree:
|
<FAILING> |
|
indeterministic:
|
referentially transparent operation |
|
infix:
|
no fixity defined |
|
iotype:
|
{({Func}) |-> _}
|
|
name:
|
fun2SMT |
|
precedence:
|
no precedence defined |
|
result-values:
|
_ |
|
signature:
|
FlatCurry.Types.FuncDecl -> Prelude.Maybe ([String], Verify.ESMT.FunSig, Verify.ESMT.Term) |
|
solution-complete:
|
operation might suspend on free variables |
|
terminating:
|
possibly non-terminating |
|
totally-defined:
|
possibly non-reducible on same data term |