| 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. |
| 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 |