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