|
sourcecode:
|
------------------------------------------------------------------------
--- Groundness/non-determinism effect analysis based on the method
--- described in the [ICLP 2005 paper](https://doi.org/10.1007/11562931_21).
---
--- @author Michael Hanus
--- @version November 2024
------------------------------------------------------------------------
{-# OPTIONS_FRONTEND -Wno-incomplete-patterns #-}
module Analysis.Groundness
( Ground(..), showGround, groundAnalysis
, NDEffect(..), showNDEffect, ndEffectAnalysis
) where
import FlatCurry.Types
import Data.List
import RW.Base
import System.IO
import Analysis.Types
import Analysis.ProgInfo
------------------------------------------------------------------------
-- 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,...]).
data Ground = G | A | P [Int]
deriving (Show, Read, Eq)
-- Show groundness information as a string.
showGround :: AOutFormat -> Ground -> String
showGround ANote G = "G"
showGround AText G = "always ground result"
showGround ANote A = "A"
showGround AText A = "possibly non-ground result"
showGround ANote (P ps) = show ps
showGround AText (P ps) =
"ground if argument" ++
(if length ps == 1 then ' ' : show (head ps) ++ " is ground"
else "s " ++ show ps ++ " are ground")
-- 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.
groundAnalysis :: Analysis Ground
groundAnalysis = dependencyFuncAnalysis "Groundness" G groundFunc
groundFunc :: FuncDecl -> [(QName,Ground)] -> Ground
groundFunc (Func (m,f) _ _ _ rule) calledFuncs
| m==prelude && f `elem` preludeGroundFuncs = G
| m==prelude = maybe anaresult id (lookup f preludeFuncs)
| otherwise = anaresult
where
anaresult = groundFuncRule calledFuncs rule
preludeFuncs = [("cond",P [2]),("seq",P [2]),("ensureNotFree",P [1])]
preludeGroundFuncs =
["+","-","*","div","mod","divMod","quot","rem","quotRem","negateFloat",
"==","=:=","=:<=","compare","<",">","<=",">=","failed","error"]
groundFuncRule :: [(QName,Ground)] -> Rule -> Ground
groundFuncRule _ (External _) = A -- nothing known about other externals
groundFuncRule calledFuncs (Rule args rhs) =
absEvalExpr (zip args (map (\i->P [i]) [1..])) rhs
where
-- abstract evaluation of an expression w.r.t. groundness environment
absEvalExpr env (Var i) = maybe A -- occurs in case of recursive lets
id (lookup i env)
absEvalExpr _ (Lit _) = G
absEvalExpr env (Comb ct g es) =
if ct == FuncCall
then maybe (error $ "Abstract value of " ++ show g ++ " not found!")
(\gd -> let curargs = zip [1..] (map (absEvalExpr env) es)
in groundApply gd curargs)
(lookup g calledFuncs)
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) = lubG (absEvalExpr env e1) (absEvalExpr env e2)
absEvalExpr env (Typed e _) = absEvalExpr env e
absEvalExpr env (Case _ e bs) = foldr lubG G (map absEvalBranch bs)
where
gcase = absEvalExpr env e
absEvalBranch (Branch (LPattern _) be) = absEvalExpr env be
absEvalBranch (Branch (Pattern _ pargs) be) =
absEvalExpr (map (\pi -> (pi,gcase)) 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 groundness information for an application
groundApply :: Ground -> [(Int,Ground)] -> Ground
groundApply G _ = G
groundApply A _ = A
groundApply (P ps) gargs =
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]
deriving (Eq, Ord, Show, Read)
noEffect :: NDEffect
noEffect = NDEffect False False []
orEffect :: NDEffect
orEffect = NDEffect True False []
narrEffect :: NDEffect
narrEffect = NDEffect False True []
narrIfEffect :: [Int] -> NDEffect
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 :: [(Int,Ground)] -> NDEffect -> NDEffect
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 :: String
prelude = "Prelude"
------------------------------------------------------------------------------
-- ReadWrite instances:
instance ReadWrite Ground where
readRW _ ('0' : r0) = (G,r0)
readRW _ ('1' : r0) = (A,r0)
readRW strs ('2' : r0) = (P a',r1)
where
(a',r1) = readRW strs r0
showRW _ strs0 G = (strs0,showChar '0')
showRW _ strs0 A = (strs0,showChar '1')
showRW params strs0 (P a') = (strs1,showChar '2' . show1)
where
(strs1,show1) = showRW params strs0 a'
writeRW _ h G strs = hPutChar h '0' >> return strs
writeRW _ h A strs = hPutChar h '1' >> return strs
writeRW params h (P a') strs = hPutChar h '2' >> writeRW params h a' strs
typeOf _ = monoRWType "Ground"
instance ReadWrite NDEffect where
readRW strs r0 = (NDEffect a' b' c',r3)
where
(a',r1) = readRW strs r0
(b',r2) = readRW strs r1
(c',r3) = readRW strs r2
showRW params strs0 (NDEffect a' b' c') = (strs3,show1 . (show2 . show3))
where
(strs1,show1) = showRW params strs0 a'
(strs2,show2) = showRW params strs1 b'
(strs3,show3) = showRW params strs2 c'
writeRW params h (NDEffect a' b' c') strs =
(writeRW params h a' strs >>= writeRW params h b') >>= writeRW params h c'
typeOf _ = monoRWType "NDEffect"
------------------------------------------------------------------------------
|