CurryInfo: contract-prover-4.0.0 / Curry2SMT.fun2SMT
definition: 
|
fun2SMT :: TAFuncDecl -> ([Ident],FunSig,Term)
fun2SMT (AFunc qn _ _ texp rule) =
let fsig = FunSig (transOpName qn)
(map polytype2psort (argTypes texp))
(polytype2psort (resultType texp))
srule = rule2SMT rule
tpars = union (typeParamsOfFunSig fsig) (typeParamsOfTerm srule)
in (tpars, fsig, srule)
where
rule2SMT (AExternal _ s) =
tEqu (tComb (transOpName qn) []) (tComb ("External:" ++ s) [])
rule2SMT (ARule _ vs exp) =
Forall (map (\ (v,t) -> SV v (polytype2psort t)) vs)
(tEqu lhs (exp2SMT exp))
where
lhs = tComb (transOpName qn) (map (TSVar . fst) vs)
|
|
demand:
|
argument 1 |
|
deterministic:
|
deterministic operation |
|
documentation:
|
Translate a function declaration into a (possibly polymorphic) SMT function declaration. |
|
failfree:
|
_ |
|
indeterministic:
|
referentially transparent operation |
|
infix:
|
no fixity defined |
|
iotype:
|
{({AFunc}) |-> {(,,)}}
|
|
name:
|
fun2SMT |
|
precedence:
|
no precedence defined |
|
result-values:
|
{(,,)}
|
|
signature:
|
FlatCurry.Annotated.Types.AFuncDecl FlatCurry.Types.TypeExpr -> ([String], ESMT.FunSig, ESMT.Term) |
|
solution-complete:
|
operation might suspend on free variables |
|
terminating:
|
possibly non-terminating |
|
totally-defined:
|
possibly non-reducible on same data term |