| definition: |
daFuncRule :: [(QName,DemandedArgs)] -> Rule -> DemandedArgs
daFuncRule _ (External _) = [] -- nothing known about externals
daFuncRule calledFuncs (Rule args rhs) =
map fst
(filter ((==Bot) . snd)
(map (\botarg -> (botarg, absEvalExpr rhs [botarg]))
args))
where
-- abstract evaluation of an expression w.r.t. variables assumed to be Bot
absEvalExpr (Var i) bvs = if i `elem` bvs then Bot else Top
absEvalExpr (Lit _) _ = Top
absEvalExpr (Comb ct g es) bvs
| ct == FuncCall
= if g == (prelude,"failed")
then Bot -- Prelude.failed never returns a value
else maybe (error $ "Abstract value of " ++ show g ++ " not found!")
(\gdas -> let curargs = map (\(i,e) -> (i,absEvalExpr e bvs))
(zip [1..] es)
cdas = gdas \\
map fst (filter ((/=Bot) . snd) curargs)
in if null cdas then Top else Bot)
(lookup g calledFuncs)
| otherwise = Top
absEvalExpr (Free _ e) bvs = absEvalExpr e bvs
absEvalExpr (Let bs e) bvs = absEvalExpr e (absEvalBindings bs bvs)
absEvalExpr (Or e1 e2) bvs = lub (absEvalExpr e1 bvs) (absEvalExpr e2 bvs)
absEvalExpr (Case _ e bs) bvs =
if absEvalExpr e bvs == Bot
then Bot
else foldr lub Bot (map absEvalBranch bs)
where absEvalBranch (Branch _ be) = absEvalExpr be bvs
absEvalExpr (Typed e _) bvs = absEvalExpr e bvs
-- could be improved with local fixpoint computation
absEvalBindings [] bvs = bvs
absEvalBindings ((i,exp) : bs) bvs =
let ival = absEvalExpr exp bvs
in if ival==Bot
then absEvalBindings bs (i:bvs)
else absEvalBindings bs bvs
|
| demand: |
argument 2 |
| deterministic: |
deterministic operation |
| failfree: |
(_, _) |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| iotype: |
{(_,{External}) |-> {[]} || (_,{Rule}) |-> {:,[]}}
|
| name: |
daFuncRule |
| precedence: |
no precedence defined |
| result-values: |
{:,[]}
|
| signature: |
[((String, String), [Prelude.Int])] -> FlatCurry.Types.Rule -> [Prelude.Int] |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |