|
definition:
|
checkPredefinedOp :: TermDomain a => Expr -> VerifyStateM a (VarTypesMap a)
-> VerifyStateM a (VarTypesMap a)
checkPredefinedOp exp cont = case exp of
-- check integer division:
Comb FuncCall ap1 [Comb FuncCall ap2 [Comb FuncCall qf _, arg1], arg2]
| ap1 == apply && ap2 == apply && qf `elem` intDivOps
-> tryCheckNumValue (intValue arg2) qf arg1 arg2 fcInt
-- check float division:
Comb FuncCall qf [arg1, arg2]
| qf == pre "_impl#/#Prelude.Fractional#Prelude.Float#"
-> tryCheckNumValue (floatValue arg2) qf arg1 arg2 fcFloat
Comb FuncCall ap1 [Comb FuncCall ap2 [Comb FuncCall qf _, arg1], arg2]
| ap1 == apply && ap2 == apply && qf `elem` floatDivOps
-> tryCheckNumValue (floatValue arg2) qf arg1 arg2 fcFloat
-- check sqrt call:
Comb FuncCall ap1 [Comb FuncCall qf [], arg]
| ap1 == apply && qf == pre "_impl#sqrt#Prelude.Floating#Prelude.Float#"
-> maybe (verifyPredefinedOp qf [arg] fcFloat)
(\x -> do unless (x >= 0) $ addFailedFunc exp Nothing fcFalse
return [])
(floatValue arg)
_ -> cont
where
tryCheckNumValue mbx qf arg1 arg2 te =
maybe (verifyPredefinedOp qf [arg1,arg2] te)
(\z -> do if z == 0 then addFailedFunc exp Nothing fcFalse
else printIfVerb 4 nonZeroOkMsg
verifyExpr True arg1
return [])
mbx
verifyPredefinedOp qf args te =
maybe (do printIfVerb 0 $
"WARNING: non-fail condition of " ++ snd qf ++ " not found!"
cont)
(\nfc -> do vs <- mapM (verifyExpr True) args
mapM_ (\v -> setVarExpTypeOf v te) vs
verifyNonTrivFuncCall exp qf vs failACallType (Just nfc)
return [])
(lookupPredefinedNonFailCond qf)
intValue e = case e of
Lit (Intc i) -> Just i
Comb FuncCall ap [ Comb FuncCall fromint _ , nexp]
| ap == apply && fromint == pre "fromInt" -> intValue nexp
_ -> Nothing
floatValue e = case e of
Lit (Floatc f) -> Just f
Comb FuncCall ap [ Comb FuncCall fromfloat _ , nexp]
| ap == apply && fromfloat == pre "fromFloat" -> floatValue nexp
Comb FuncCall ap [(Comb FuncCall fromint _), nexp]
| ap == apply && fromint == pre "fromInt" -> fmap fromInt (intValue nexp)
Comb FuncCall negFloat [fexp]
| negFloat == pre "_impl#negate#Prelude.Num#Prelude.Float#"
-> fmap negate (floatValue fexp)
_ -> Nothing
apply = pre "apply"
nonZeroOkMsg = "Divion with non-zero constant is non-failing"
|
|
documentation:
|
-- Auxiliary operation to support specific handling of applying predefined
-- operations with specific non-fail conditions.
-- If the current expression (first argument) is not a specific
-- predefined operation, the computation will be continued by calling
-- the second argument (a continuation).
-- For instance, division operations require that the second argument is
-- non-zero. If this argument is a constant, it will be immediately checked,
-- otherwise a non-fail condition will be generated and checked.
-- Since such primitive operations can be invoked by FlatCurry expressions
-- with various structures (due to the numeric type classes),
-- these structures will be checked.
|
|
signature:
|
Analysis.TermDomain.TermDomain a => FlatCurry.Types.Expr
-> Control.Monad.Trans.State.StateT (VerifyState a) Prelude.IO [(Prelude.Int, [(Verify.IOTypes.InOutType a, [Prelude.Int])])]
-> Control.Monad.Trans.State.StateT (VerifyState a) Prelude.IO [(Prelude.Int, [(Verify.IOTypes.InOutType a, [Prelude.Int])])]
|