|
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.
|
|
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
|