|
definition:
|
optPreConditionInRule :: Options -> VerifyInfo -> QName -> TARule
-> IORef VState -> IO TARule
optPreConditionInRule _ _ _ rl@(AExternal _ _) _ = return rl
optPreConditionInRule opts ti qn@(_,fn) (ARule rty rargs rhs) vstref = do
let targs = zip [1..] (map snd rargs)
st = makeTransState (maximum (0 : map fst rargs ++ allVars rhs) + 1) rargs
(flip evalStateT) st $ do
-- compute precondition of operation:
precondformula <- preCondExpOf ti qn targs
setAssertion precondformula
newrhs <- optPreCondInExp rhs
return (ARule rty rargs newrhs)
where
optPreCondInExp exp = case exp of
AComb ty ct (qf,tys) args ->
if qf == ("Prelude","?") && length args == 2
then optPreCondInExp (AOr ty (args!!0) (args!!1))
else do
precond <- getAssertion
nargs <- mapM optPreCondInExp args
if toPreCondQName qf `elem` map funcName (preConds ti)
then do
lift $ printWhenIntermediate opts $ "Checking call to " ++ snd qf
(bs,_) <- normalizeArgs nargs
bindexps <- mapM (binding2SMT True ti) bs
precondcall <- preCondExpOf ti qf
(zip (map fst bs) (map annExpr args))
-- TODO: select from 'bindexps' only demanded argument positions
let title = "SMT script to verify precondition of '" ++ snd qf ++
"' in function '" ++ fn ++ "'"
vartypes <- getVarTypes
pcproof <- lift $
checkImplication opts vstref title vartypes
precond (tConj bindexps) precondcall
let pcvalid = isJust pcproof
lift $ modifyIORef vstref
(addPreCondToStats (snd qf ++ "("++fn++")") pcvalid)
if pcvalid
then do
lift $ printWhenStatus opts $
fn ++ ": PRECONDITION OF '" ++ snd qf ++ "': VERIFIED"
return $ AComb ty ct (toNoCheckQName qf, tys) nargs
else do
lift $ printWhenStatus opts $
fn ++ ": PRECOND CHECK ADDED TO '" ++ snd qf ++ "'"
return $ AComb ty ct (qf,tys) nargs
else return $ AComb ty ct (qf,tys) nargs
ACase ty ct e brs -> do
ne <- optPreCondInExp e
freshvar <- getFreshVar
be <- binding2SMT True ti (freshvar,ne)
addToAssertion be
addVarTypes [ (freshvar, annExpr ne) ]
nbrs <- mapM (optPreCondInBranch freshvar) brs
return $ ACase ty ct ne nbrs
AOr ty e1 e2 -> do
ne1 <- optPreCondInExp e1
ne2 <- optPreCondInExp e2
return $ AOr ty ne1 ne2
ALet ty bs e -> do
nes <- mapM optPreCondInExp (map snd bs)
ne <- optPreCondInExp e
return $ ALet ty (zip (map fst bs) nes) ne
AFree ty fvs e -> do
ne <- optPreCondInExp e
return $ AFree ty fvs ne
ATyped ty e et -> do
ne <- optPreCondInExp e
return $ ATyped ty ne et
_ -> return exp
optPreCondInBranch dvar branch = do
ABranch p e <- renamePatternVars branch
addToAssertion (tEquVar dvar (pat2SMT p))
ne <- optPreCondInExp e
return (ABranch p ne)
|
|
iotype:
|
{(_,_,_,{AExternal},_) |-> _ || (_,_,{(,)},{ARule},_) |-> _}
|