definition: 
|
exp2SMT :: Maybe Term -> Expr -> Maybe Term
exp2SMT lhs exp = case exp of
Var i -> Just $ makeRHS (TSVar i)
Lit l -> Just $ makeRHS (lit2SMT l)
Comb _ qf args -> mapM (exp2SMT Nothing) args >>= comb2SMT qf
Case _ e bs -> do t <- exp2SMT Nothing e
bts <- mapM branch2SMT bs
return $ makeRHS (Match t bts)
FC.Let bs e -> do tbs <- mapM (\(v,be) -> do t <- exp2SMT Nothing be
return (v,t))
bs
t <- exp2SMT lhs e
return $ tLet tbs t
Free _ _ -> Nothing --error "exp2SMT: Free"
Typed e te -> case e of
Comb _ qf args | all isTyped args
-> mapM (exp2SMT Nothing) args >>=
return . makeRHS .
TComb (As (transOpName qf)
(type2sort (foldr FuncType te (map exprType args))))
_ -> exp2SMT lhs e
Or e1 e2 -> do t1 <- exp2SMT lhs e1
t2 <- exp2SMT lhs e2
return $ tDisj [t1,t2]
where
comb2SMT qf targs
| qf `elem` map pre ["chr", "ord"] && length targs == 1
= return $ makeRHS (head targs) -- chars are integers --> no conversion
| otherwise
= return $ makeRHS (tComb (transOpName qf) targs)
makeRHS rhs = maybe rhs (\l -> tEqu l rhs) lhs
branch2SMT (Branch (LPattern _) _) = Nothing -- literal patterns not supported
branch2SMT (Branch (Pattern qf vs) e) = do
t <- exp2SMT lhs e
return (PComb (Id (transOpName qf)) vs, t)
|
|
demand:
|
argument 2
|
|
deterministic:
|
deterministic operation
|
|
documentation:
|
Translates a (Boolean) 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:
|
<FAILING>
|
|
indeterministic:
|
referentially transparent operation
|
|
infix:
|
no fixity defined
|
|
iotype:
|
{(_,{Var}) |-> _ || (_,{Lit}) |-> _ || (_,{Comb}) |-> _ || (_,{Case}) |-> _ || (_,{Let}) |-> _ || (_,{Free}) |-> {Nothing} || (_,{Typed}) |-> _ || (_,{Or}) |-> _}
|
|
name:
|
exp2SMT
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
_
|
|
signature:
|
Prelude.Maybe Verify.ESMT.Term -> FlatCurry.Types.Expr
-> Prelude.Maybe Verify.ESMT.Term
|
|
solution-complete:
|
operation might suspend on free variables
|
|
terminating:
|
possibly non-terminating
|
|
totally-defined:
|
possibly non-reducible on same data term
|