| definition: |
exp2SMT :: Maybe Term -> TAExpr -> Term
exp2SMT lhs exp = case exp of
AVar _ i -> makeRHS (TSVar i)
ALit _ l -> makeRHS (lit2SMT l)
AComb _ ct (qn,ftype) args ->
-- TODO: reason about condition `not (null args)`
makeRHS (TComb (cons2SMT (ct /= ConsCall || not (null args)) True qn ftype)
(map (exp2SMT Nothing) args))
ACase _ _ e brs -> let be = exp2SMT Nothing e
in branches2SMT be brs
ALet _ bs e -> Let (map (\ ((v,_),be) -> (v, exp2SMT Nothing be)) bs)
(exp2SMT lhs e)
ATyped _ e _ -> exp2SMT lhs e
AFree _ fvs e -> Forall (map (\ (v,t) -> SV v (polytype2psort t)) fvs)
(exp2SMT lhs e)
AOr _ e1 e2 -> tDisj [exp2SMT lhs e1, exp2SMT lhs e2]
where
makeRHS rhs = maybe rhs (\l -> tEqu l rhs) lhs
branches2SMT _ [] = error "branches2SMT: empty branch list"
branches2SMT be [ABranch p e] = branch2SMT be p e
branches2SMT be (ABranch p e : brs@(_:_)) =
tComb "ite" [patternTest p be, --tEqu be (pat2smt p),
branch2SMT be p e,
branches2SMT be brs]
branch2SMT _ (ALPattern _ _) e = exp2SMT lhs e
branch2SMT be (APattern _ (qf,_) ps) e = case ps of
[] -> exp2SMT lhs e
_ -> Let (map (\ (s,v) -> (v, tComb s [be]))
(zip (selectors qf) (map fst ps)))
(exp2SMT lhs e)
|
| demand: |
argument 2 |
| deterministic: |
deterministic operation |
| documentation: |
-- Translates a typed FlatCurry expression into an SMT expression. -- If the first argument is an SMT expression, an equation between -- this expression and the translated result expression is generated. -- This is useful to axiomatize non-deterministic operations. |
| failfree: |
(_, _) |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| iotype: |
{(_,{AVar}) |-> _ || (_,{ALit}) |-> _ || (_,{AComb}) |-> _ || (_,{ACase}) |-> _ || (_,{ALet}) |-> {Let} || (_,{ATyped}) |-> _ || (_,{AFree}) |-> {Forall} || (_,{AOr}) |-> _}
|
| name: |
exp2SMT |
| precedence: |
no precedence defined |
| result-values: |
_ |
| signature: |
Prelude.Maybe ESMT.Term -> FlatCurry.Annotated.Types.AExpr FlatCurry.Types.TypeExpr -> ESMT.Term |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |