| definition: |
pred2SMT :: TAExpr -> TransStateM SMT.Term
pred2SMT exp = case exp of
AVar _ i -> return (tvar i)
ALit _ l -> return (lit2SMT l)
AComb _ ct (qf,ftype) args -> comb2bool qf ftype ct (length args) args
_ -> return (tcomb (show exp) []) -- TODO!
where
comb2bool qf ftype ct ar args
| qf == pre "[]" && ar == 0
= return (sortedConst "nil" (polytype2sort (annExpr exp)))
| qf == pre "not" && ar == 1
= do barg <- pred2SMT (head args)
return (tnot barg)
| qf == pre "null" && ar == 1
= do let arg = head args
barg <- pred2SMT arg
typeOfVar arg >>= return . (barg =%) . maybe (tcomb "nil" [])
(sortedConst "nil" . polytype2sort)
| qf == pre "apply"
= do -- cannot translate h.o. apply: replace it by new variable
fvar <- getFreshVar
addVarTypes [(fvar,annExpr exp)]
return (tvar fvar)
| qf == pre "/="
= do be <- comb2bool (pre "==") ftype ct ar args
return (tnot be)
| otherwise
= do bargs <- mapM pred2SMT args
return (SMT.TComb (cons2SMT (ct /= ConsCall || not (null bargs))
False qf ftype)
bargs)
typeOfVar e =
case e of
AVar _ i -> getVarTypes >>= return . lookup i . map (\(x,y,_) -> (x,y))
_ -> return $ Just $ annExpr e
|
| demand: |
argument 1 |
| deterministic: |
deterministic operation |
| documentation: |
--------------------------------------------------------------------------- -- Translates a Boolean FlatCurry expression into a Boolean formula. -- Calls to user-defined functions are replaced by the first argument -- (which might be true or false). |
| failfree: |
<FAILING> |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| iotype: |
{({AVar}) |-> _ || ({ALit}) |-> _ || ({AComb}) |-> _ || ({ALet}) |-> _ || ({AFree}) |-> _ || ({AOr}) |-> _ || ({ACase}) |-> _ || ({ATyped}) |-> _}
|
| name: |
pred2SMT |
| precedence: |
no precedence defined |
| result-values: |
_ |
| signature: |
FlatCurry.Annotated.Types.AExpr FlatCurry.Types.TypeExpr -> Control.Monad.Trans.State.StateT TransState.TransState (Control.Monad.Trans.State.StateT VerifierState.VState Prelude.IO) 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 |