| definition: |
exp2SMT :: TAExpr -> Term
exp2SMT exp = case exp of
AVar _ i -> TSVar i
ALit _ l -> lit2SMT l
AComb _ ct (qn,ftype) args ->
-- TODO: reason about condition `not (null args)`
TComb (cons2SMT (ct /= ConsCall || not (null args)) True qn ftype)
(map exp2SMT args)
ACase _ _ e brs -> let be = exp2SMT e
in branches2SMT be brs
ALet _ bs e -> Let (map (\ ((v,_),be) -> (v, exp2SMT be)) bs)
(exp2SMT e)
ATyped _ e _ -> exp2SMT e
AFree _ fvs e -> Forall (map (\ (v,t) -> SV v (polytype2psort t)) fvs)
(exp2SMT e)
AOr _ e1 e2 -> tDisj [exp2SMT e1, exp2SMT e2]
where
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 e
branch2SMT be (APattern _ (qf,_) ps) e = case ps of
[] -> exp2SMT e
_ -> Let (map (\ (s,v) -> (v, tComb s [be]))
(zip (selectors qf) (map fst ps)))
(exp2SMT e)
|
| demand: |
argument 1 |
| deterministic: |
deterministic operation |
| documentation: |
-- Translates a typed FlatCurry expression into an SMT expression. |
| failfree: |
_ |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| iotype: |
{({AVar}) |-> {TSVar} || ({ALit}) |-> {TConst} || ({AComb}) |-> {TComb} || ({ACase}) |-> _ || ({ALet}) |-> {Let} || ({ATyped}) |-> _ || ({AFree}) |-> {Forall} || ({AOr}) |-> _}
|
| name: |
exp2SMT |
| precedence: |
no precedence defined |
| result-values: |
_ |
| signature: |
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 |