| definition: |
fun2SMT :: TAFuncDecl -> ([SMT.Ident],FunSig,SMT.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) =
(tcomb (transOpName qn) []) =% (tcomb ("External:" ++ s) [])
rule2SMT (ARule _ vs exp) =
SMT.Forall (map (\ (v,t) -> SMT.SV (var2SMT v) (polytype2psort t)) vs)
(if ndExpr exp then exp2SMT (Just lhs) exp
else lhs =% (exp2SMT Nothing exp))
where
lhs = tcomb (transOpName qn) (map (tvar . 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, Language.SMTLIB.Types.Term) |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |