| 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)
(if ndExpr exp then exp2SMT (Just lhs) exp
else tEqu lhs (exp2SMT Nothing 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 |