Commit e1cbfea5 authored by Michael Hanus 's avatar Michael Hanus
Browse files

Non-determinism effect analysis added

parent 024b66ef
......@@ -45,19 +45,20 @@ import Groundness
--- together with an operation to show the analysis result as a string.
registeredAnalysis :: [RegisteredAnalysis]
registeredAnalysis =
[cassAnalysis "Overlapping rules" overlapAnalysis showOverlap
,cassAnalysis "Deterministic operations" nondetAnalysis showDet
,cassAnalysis "Right-linear operations" rlinAnalysis showRightLinear
,cassAnalysis "Solution completeness" solcompAnalysis showSolComplete
,cassAnalysis "Pattern completeness" patCompAnalysis showComplete
,cassAnalysis "Totally defined operations" totalAnalysis showTotally
,cassAnalysis "Indeterministic operations" indetAnalysis showIndet
,cassAnalysis "Demanded arguments" demandAnalysis showDemand
,cassAnalysis "Groundness" groundAnalysis showGround
,cassAnalysis "Higher-order datatypes" hiOrdType showOrder
,cassAnalysis "Higher-order constructors" hiOrdCons showOrder
,cassAnalysis "Higher-order functions" hiOrdFunc showOrder
,cassAnalysis "Sibling constructors" siblingCons showSibling
[cassAnalysis "Overlapping rules" overlapAnalysis showOverlap
,cassAnalysis "Deterministic operations" nondetAnalysis showDet
,cassAnalysis "Right-linear operations" rlinAnalysis showRightLinear
,cassAnalysis "Solution completeness" solcompAnalysis showSolComplete
,cassAnalysis "Pattern completeness" patCompAnalysis showComplete
,cassAnalysis "Totally defined operations" totalAnalysis showTotally
,cassAnalysis "Indeterministic operations" indetAnalysis showIndet
,cassAnalysis "Demanded arguments" demandAnalysis showDemand
,cassAnalysis "Groundness" groundAnalysis showGround
,cassAnalysis "Non-determinism effects" ndEffectAnalysis showNDEffect
,cassAnalysis "Higher-order datatypes" hiOrdType showOrder
,cassAnalysis "Higher-order constructors" hiOrdCons showOrder
,cassAnalysis "Higher-order functions" hiOrdFunc showOrder
,cassAnalysis "Sibling constructors" siblingCons showSibling
]
......
......@@ -45,6 +45,11 @@ cass: $(DEPS)
$(REPL) $(REPL_OPTS) :set path $(ANADIR) :l AnalysisServer :save :q
mv AnalysisServer $@
# load the analysis server program into the Curry system:
.PHONY: load
load: $(DEPS)
$(REPL) $(REPL_OPTS) :set path $(ANADIR) :l AnalysisServer
.PHONY: clean
clean: uninstall
$(CLEANCURRY) -r
......
------------------------------------------------------------------------
--- Groundness analysis based on the [Brassel/Hanus ICLP 2005]
--- Groundness/non-determinism effect analysis based on
--- [Brassel/Hanus'05](http://www.informatik.uni-kiel.de/~mh/papers/ICLP05.html).
---
--- @author Michael Hanus
--- @version May 2013
------------------------------------------------------------------------
module Groundness(Ground(..),showGround,groundAnalysis) where
module Groundness(Ground(..),showGround,groundAnalysis,
NDEffect(..),showNDEffect,ndEffectAnalysis) where
import FlatCurry
import List
import Analysis
import GenericProgInfo
------------------------------------------------------------------------
-- Analyze the groundness of functions.
------------------------------------------------------------------------
--- Type to represent groundness information.
--- Definitely ground (G), maybe non-ground (A), or maybe non-ground
--- if i-th argument is non-ground (P i).
--- if i-th argument is non-ground (P [...,i,...]).
data Ground = G | A | P [Int]
-- Show groundness information as a string.
......@@ -25,12 +35,13 @@ showGround AText (P ps) =
(if length ps == 1 then ' ' : show (head ps) ++ " is ground"
else "s " ++ show ps ++ " are ground")
lub :: Ground -> Ground -> Ground
lub G y = y
lub A _ = A
lub (P ps) G = P ps
lub (P _ ) A = A
lub (P ps) (P qs) = P (union ps qs)
-- Lowest upper bound on groundness information.
lubG :: Ground -> Ground -> Ground
lubG G y = y
lubG A _ = A
lubG (P ps) G = P ps
lubG (P _ ) A = A
lubG (P ps) (P qs) = P (mergeInts ps qs)
------------------------------------------------------------------------
-- Analyze the groundness information of functions.
......@@ -68,12 +79,12 @@ groundFuncRule calledFuncs (Rule args rhs) =
(\gd -> let curargs = zip [1..] (map (absEvalExpr env) es)
in groundApply gd curargs)
(lookup g calledFuncs)
else foldr lub G (map (absEvalExpr env) es)
else foldr lubG G (map (absEvalExpr env) es)
absEvalExpr env (Free vs e) = absEvalExpr (zip vs (repeat A) ++ env) e
absEvalExpr env (Let bs e) = absEvalExpr (absEvalBindings env bs) e
absEvalExpr env (Or e1 e2) = lub (absEvalExpr env e1) (absEvalExpr env e2)
absEvalExpr env (Or e1 e2) = lubG (absEvalExpr env e1) (absEvalExpr env e2)
absEvalExpr env (Typed e _) = absEvalExpr env e
absEvalExpr env (Case _ e bs) = foldr lub G (map absEvalBranch bs)
absEvalExpr env (Case _ e bs) = foldr lubG G (map absEvalBranch bs)
where
gcase = absEvalExpr env e
......@@ -91,7 +102,145 @@ groundApply :: Ground -> [(Int,Ground)] -> Ground
groundApply G _ = G
groundApply A _ = A
groundApply (P ps) gargs =
foldr lub G (map (\p -> maybe A id (lookup p gargs)) ps)
foldr lubG G (map (\p -> maybe A id (lookup p gargs)) ps)
-----------------------------------------------------------------------
-- Non-determinism effect analysis
-----------------------------------------------------------------------
--- Type to represent non-determinism effects.
--- A non-determinism effect can be due to an Or (first argument),
--- due to a narrowing step (second argument), or if i-th argument
--- is non-ground (if i is a member of the third argument).
data NDEffect = NDEffect Bool Bool [Int]
noEffect = NDEffect False False []
orEffect = NDEffect True False []
narrEffect = NDEffect False True []
narrIfEffect = NDEffect False False
-- Show non-determinitic effect information as a string.
showNDEffect :: AOutFormat -> NDEffect -> String
showNDEffect ANote (NDEffect ornd narr ifs) = intercalate " " $
(if ornd then ["choice"] else []) ++
(if narr then ["narr"] else []) ++
(if not (null ifs) then ["narrIf"++show ifs] else [])
showNDEffect AText (NDEffect ornd narr ifs) = intercalate " / " $
(if ornd then ["choice"] else []) ++
(if narr then ["possibly non-deterministic narrowing steps"] else []) ++
(if not (null ifs)
then ["non-deterministic narrowing if argument" ++
(if length ifs == 1 then ' ' : show (head ifs) ++ " is non-ground"
else "s " ++ show ifs ++ " are non-ground")]
else [])
-- Lowest upper bound on non-determinism effects.
lubE :: NDEffect -> NDEffect -> NDEffect
lubE (NDEffect ornd1 narr1 ifs1) (NDEffect ornd2 narr2 ifs2) =
NDEffect (ornd1 || ornd2) narr (if narr then [] else mergeInts ifs1 ifs2)
where
narr = narr1 || narr2
-- Lowest upper bound on groundness/non-determinism effects.
lubGE :: (Ground,NDEffect) -> (Ground,NDEffect) -> (Ground,NDEffect)
lubGE (g1,ne1) (g2,ne2) = (lubG g1 g2, lubE ne1 ne2)
------------------------------------------------------------------------
-- Analyze the non-determinism effect of functions.
ndEffectAnalysis :: Analysis NDEffect
ndEffectAnalysis =
combinedDependencyFuncAnalysis "NDEffect" groundAnalysis noEffect ndEffectFunc
ndEffectFunc :: ProgInfo Ground -> FuncDecl -> [(QName,NDEffect)] -> NDEffect
ndEffectFunc groundinfo (Func (m,f) _ _ _ rule) calledFuncs
| m==prelude = maybe anaresult id (lookup f preludeFuncs)
| otherwise = anaresult
where
anaresult = ndEffectFuncRule groundinfo calledFuncs rule
preludeFuncs = [("?",orEffect)]
ndEffectFuncRule :: ProgInfo Ground -> [(QName,NDEffect)] -> Rule -> NDEffect
ndEffectFuncRule _ _ (External _) = noEffect -- externals are deterministic
ndEffectFuncRule groundinfo calledFuncs (Rule args rhs) =
snd (absEvalExpr (zip args (map (\i->(P [i],noEffect)) [1..])) rhs)
where
-- abstract evaluation of an expression w.r.t. NDEffect environment
absEvalExpr env (Var i) = maybe (A,noEffect) id (lookup i env)
absEvalExpr _ (Lit _) = (G,noEffect)
absEvalExpr env (Comb ct g es) =
if ct == FuncCall
then maybe (error $ "Abstract value of " ++ show g ++ " not found!")
(\gnd -> let curargs = zip [1..] (map (absEvalExpr env) es) in
maybe (error $ "Ground value of " ++ show g ++ " not found!")
(\ggd -> ndEffectApply (ggd,gnd) curargs)
(lookupProgInfo g groundinfo))
(lookup g calledFuncs)
else foldr lubGE (G,noEffect) (map (absEvalExpr env) es)
absEvalExpr env (Free vs e) =
absEvalExpr (zip vs (repeat (A,noEffect)) ++ env) e
absEvalExpr env (Let bs e) = absEvalExpr (absEvalBindings env bs) e
absEvalExpr env (Or e1 e2) =
let (g1,nd1) = absEvalExpr env e1
(g2,nd2) = absEvalExpr env e2
in (lubG g1 g2, lubE orEffect (lubE nd1 nd2))
absEvalExpr env (Typed e _) = absEvalExpr env e
absEvalExpr env (Case ctype e bs) =
if ctype==Rigid {- not really for KiCS2 -} || gcase==G || length bs == 1
then (gbrs, lubE ndbrs ndcase)
else (gbrs, lubE (ground2nondet gcase) (lubE ndbrs ndcase))
where
(gcase,ndcase) = absEvalExpr env e
(gbrs,ndbrs) = foldr lubGE (G,noEffect) (map absEvalBranch bs)
ground2nondet G = noEffect
ground2nondet A = narrEffect
ground2nondet (P ps) = narrIfEffect ps
absEvalBranch (Branch (LPattern _) be) = absEvalExpr env be
absEvalBranch (Branch (Pattern _ pargs) be) =
absEvalExpr (map (\pi -> (pi,(gcase,noEffect))) pargs ++ env) be
-- could be improved for recursive lets with local fixpoint computation
absEvalBindings env [] = env
absEvalBindings env ((i,exp):bs) =
absEvalBindings ((i, absEvalExpr env exp) : env) bs
-- compute ground/nondet effect information for an application
ndEffectApply :: (Ground,NDEffect) -> [(Int,(Ground,NDEffect))]
-> (Ground,NDEffect)
ndEffectApply (fgd,fnd) argsgnd =
let (argsgd,argsnd) = unzip (map (\ (i,(gd,nd)) -> ((i,gd),nd)) argsgnd)
in (groundApply fgd argsgd,
foldr lubE (ndEffectReplace argsgd fnd) argsnd)
-- replace (narrIf i) by i-th ground value
ndEffectReplace argsgd (NDEffect ornd narrnd ifs) = replaceProjs [] ifs
where
-- replace i by i-th ground value
replaceProjs ps [] = NDEffect ornd narrnd ps
replaceProjs ps (i:is) =
maybe (error $ "Ground value of argument " ++ show i ++ " not found!")
(\g -> case g of G -> replaceProjs ps is
A -> NDEffect ornd True []
P ips -> replaceProjs (mergeInts ips ps) is)
(lookup i argsgd)
-----------------------------------------------------------------------
-- merge ascending lists of integers and remove duplicates
mergeInts :: [Int] -> [Int] -> [Int]
mergeInts [] ys = ys
mergeInts (x:xs) [] = x:xs
mergeInts (x:xs) (y:ys) | x==y = x : mergeInts xs ys
| x<y = x : mergeInts xs (y:ys)
| x>y = y : mergeInts (x:xs) ys
prelude = "Prelude"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment