|
definition:
|
binding2SMT :: Bool -> VerifyInfo -> (Int,TAExpr) -> TransStateM Term
binding2SMT odemanded vi (oresvar,oexp) =
exp2smt odemanded (oresvar, simpExpr oexp)
where
exp2smt demanded (resvar,exp) = case exp of
AVar _ i -> return $ if resvar==i then tTrue
else tEquVar resvar (TSVar i)
ALit _ l -> return (tEquVar resvar (lit2SMT l))
AComb ty ct (qf,_) args ->
if qf == pre "?" && length args == 2
then exp2smt demanded (resvar, AOr ty (args!!0) (args!!1))
else do
(bs,nargs) <- normalizeArgs args
-- TODO: select from 'bindexps' only demanded argument positions
bindexps <- mapM (exp2smt (isPrimOp qf || optStrict (toolOpts vi))) bs
comb2smt qf ty ct nargs bs bindexps
ALet _ bs e -> do
addVarTypes (map fst bs)
bindexps <- mapM (exp2smt False) (map (\ ((i,_),ae) -> (i,ae)) bs)
bexp <- exp2smt demanded (resvar,e)
return (tConj (bindexps ++ [bexp]))
AOr _ e1 e2 -> do
bexp1 <- exp2smt demanded (resvar,e1)
bexp2 <- exp2smt demanded (resvar,e2)
return (tDisj [bexp1, bexp2])
ACase _ _ e brs -> do
freshvar <- getFreshVar
addVarTypes [(freshvar, annExpr e)]
argbexp <- exp2smt demanded (freshvar,e)
bbrs <- mapM branch2smt (map (\b -> (freshvar,b)) brs)
return (tConj [argbexp, tDisj bbrs])
ATyped _ e _ -> exp2smt demanded (resvar,e)
AFree _ _ _ -> error "Free variables not yet supported!"
where
comb2smt qf rtype ct nargs bs bindexps
| qf == pre "otherwise"
-- specific handling for the moment since the front end inserts it
-- as the last alternative of guarded rules...
= return (tEquVar resvar tTrue)
| ct == ConsCall -- translate data constructor
= return (tConj (bindexps ++
[tEquVar resvar
(TComb (cons2SMT (null nargs) False qf rtype)
(map arg2smt nargs))]))
| qf == pre "apply"
= -- cannot translate h.o. apply: ignore it
return tTrue
| isPrimOp qf
= return (tConj (bindexps ++
[tEquVar resvar (TComb (cons2SMT True False qf rtype)
(map arg2smt nargs))]))
| otherwise -- non-primitive operation: add contract only if demanded
= do let targs = zip (map fst bs) (map annExpr nargs)
precond <- preCondExpOf vi qf targs
postcond <- postCondExpOf vi qf (targs ++ [(resvar,rtype)])
return
(tConj (bindexps ++ if demanded then [precond,postcond] else []))
branch2smt (cvar, (ABranch p e)) = do
branchbexp <- exp2smt demanded (resvar,e)
addVarTypes patvars
return (tConj [ tEquVar cvar (pat2SMT p), branchbexp])
where
patvars = if isConsPattern p
then patArgs p
else []
arg2smt e = case e of AVar _ i -> TSVar i
ALit _ l -> lit2SMT l
_ -> error $ "Not normalized: " ++ show e
|
|
documentation:
|
Translates a binding between a variable (represented by its index
in the first component) and a FlatCurry expression (second component).
The FlatCurry expression is translated into an SMT formula so that
the binding is axiomiatized as an equation between the variable
and the translated expression.
The translated expression is normalized when necessary.
For this purpose, a "fresh variable index" is passed as a state.
Moreover, the returned state contains also the types of all fresh variables.
If the first argument is `False`, the expression is not strictly demanded,
i.e., possible contracts of it (if it is a function call) are ignored.
|