Module Analysis

Fixpoint analyzer for call patterns

Author: Michael Hanus

Version: January 2012

Summary of exported operations:

analysisDir :: String   
createAnalysisDir :: String -> IO ()   
ndInfoFileName :: String -> String   
strictInfoFileName :: String -> String   
adomBottom :: ADom a -> a   
adomShow :: ADom a -> a -> String   
adomLeq :: ADom a -> a -> a -> Bool   
abstractCall :: ADom a -> (String,[Term]) -> (String,[a])   
matchCTerms :: [Term] -> [CTerm] -> Maybe [(Int,CTerm)]   
lessCSpecific :: CTerm -> CTerm -> Bool   
leqCTerm :: CTerm -> CTerm -> Bool   
showCTerm :: CTerm -> String   
concreteDom :: ADom CTerm   
matchDTerms :: [Term] -> [DTerm] -> Maybe [(Int,DTerm)]   
consDTerm :: Int -> String -> [DTerm] -> DTerm   
cutDTerm :: Int -> DTerm -> DTerm   
lessDSpecific :: DTerm -> DTerm -> Bool   
leqDTerm :: DTerm -> DTerm -> Bool   
applyPrimDTerm :: String -> [DTerm] -> Maybe DTerm   
showDTerm :: DTerm -> String   
depthDom :: Int -> ADom DTerm   
eqSemInt :: [SemEq a] -> [SemEq a] -> Bool   
insertSemEq :: (a -> a -> Bool) -> SemEq a -> [SemEq a] -> [SemEq a]   
lessSemEq :: (a -> a -> Bool) -> SemEq a -> SemEq a -> Bool   
updateSemEq :: (a -> a -> Bool) -> (SemEq a -> SemEq a -> Bool) -> SemEq a -> [SemEq a] -> [SemEq a]   
lessSpecificEqCallPattern :: (a -> a -> Bool) -> SemEq a -> SemEq a -> Bool   
lessSpecificEqResult :: (a -> a -> Bool) -> SemEq a -> SemEq a -> Bool   
transformInt :: ADom a -> (SemEq a -> [SemEq a] -> [SemEq a]) -> [Rule] -> [SemEq a] -> [SemEq a] -> [SemEq a]   
extendListMap :: (a -> [b]) -> [a] -> [[b]]   
runFixpoint :: ADom a -> (SemEq a -> [SemEq a] -> [SemEq a]) -> [Rule] -> [(String,[a])] -> Bool -> ([SemEq a] -> [SemEq a] -> Bool) -> IO [SemEq a]   
computeFixpoint :: Bool -> Int -> (a -> String) -> (a -> a -> Bool) -> (a -> a) -> a -> IO a   
showSemInt :: ADom a -> [SemEq a] -> String   
getMainCall :: [Rule] -> (String,[Term])   
genMainCalls :: ADom a -> [Rule] -> [(String,[a])]   
printProgram :: ADom a -> [Rule] -> [(String,[a])] -> IO ()   
fEqsOfWorkSem :: String -> RedBlackTree (String,[([a],a,[String])]) -> [([a],a,[String])]   
processWorkList :: ADom a -> (SemEq a -> SemEq a -> Bool) -> Bool -> [Rule] -> [(String,[a])] -> RedBlackTree (String,[([a],a,[String])]) -> IO [SemEq a]   
runFixpointWL :: ADom a -> (SemEq a -> SemEq a -> Bool) -> [Rule] -> [(String,[a])] -> Bool -> IO [SemEq a]   
printTiming :: [(ProcessInfo,Int)] -> [(ProcessInfo,Int)] -> IO ()   
main :: IO ()   
Main calls to the (abstract) interpreters:
mainCallError :: [String] -> a   
checkArgs :: (Int,Bool,Bool,Bool,String) -> [String] -> (Int,Bool,Bool,Bool,String)   
callPatternAnalysis :: Int -> Bool -> Bool -> String -> IO ()   
transformNondet :: Int -> Bool -> Bool -> String -> IO ()   
unApply :: [Rule] -> [Rule]   
transformRules :: [(String,Bool)] -> [(String,[Int])] -> [Rule] -> ([Rule],Int)   
transformExp :: [(String,Bool)] -> [(String,[Int])] -> Term -> (Term,Bool,Int)   
extractStrictness :: ADom a -> [SemEq a] -> [(String,[Int])]   
sortFuncInfos :: [(String,a)] -> [(String,a)]   
showStrictness :: [(String,[Int])] -> String   
prog2DirFile :: String -> String   
bench :: Int -> String -> IO ()   
runBench :: IO ()   

Exported datatypes:


ADom

Constructors:

  • ADom :: a -> (Int -> a) -> (String -> [a] -> a) -> ([Term] -> [a] -> Maybe (Sub a)) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> String) -> (String -> [a] -> Maybe a) -> ADom a

SemEq

Constructors:

  • Eq :: String -> [a] -> a -> SemEq a

SemInt

Type synonym: SemInt a = [SemEq a]


Sub

Type synonym: Sub a = [(Int,a)]


CTerm

Constructors:

  • CBot :: CTerm
  • CVar :: Int -> CTerm
  • CCons :: String -> [CTerm] -> CTerm

DTerm

Constructors:

  • DBot :: DTerm
  • DCons :: String -> [DTerm] -> DTerm
  • CutVar :: DTerm

WorkSemInt

Type synonym: WorkSemInt a = TableRBT String [([a],a,[String])]


Exported operations:

analysisDir :: String   

Further infos:
  • solution complete, i.e., able to compute all solutions

createAnalysisDir :: String -> IO ()   

ndInfoFileName :: String -> String   

strictInfoFileName :: String -> String   

adomBottom :: ADom a -> a   

Further infos:
  • solution complete, i.e., able to compute all solutions

adomShow :: ADom a -> a -> String   

Further infos:
  • solution complete, i.e., able to compute all solutions

adomLeq :: ADom a -> a -> a -> Bool   

Further infos:
  • solution complete, i.e., able to compute all solutions

abstractCall :: ADom a -> (String,[Term]) -> (String,[a])   

matchCTerms :: [Term] -> [CTerm] -> Maybe [(Int,CTerm)]   

lessCSpecific :: CTerm -> CTerm -> Bool   

leqCTerm :: CTerm -> CTerm -> Bool   

showCTerm :: CTerm -> String   

matchDTerms :: [Term] -> [DTerm] -> Maybe [(Int,DTerm)]   

consDTerm :: Int -> String -> [DTerm] -> DTerm   

cutDTerm :: Int -> DTerm -> DTerm   

lessDSpecific :: DTerm -> DTerm -> Bool   

leqDTerm :: DTerm -> DTerm -> Bool   

applyPrimDTerm :: String -> [DTerm] -> Maybe DTerm   

showDTerm :: DTerm -> String   

depthDom :: Int -> ADom DTerm   

eqSemInt :: [SemEq a] -> [SemEq a] -> Bool   

insertSemEq :: (a -> a -> Bool) -> SemEq a -> [SemEq a] -> [SemEq a]   

lessSemEq :: (a -> a -> Bool) -> SemEq a -> SemEq a -> Bool   

updateSemEq :: (a -> a -> Bool) -> (SemEq a -> SemEq a -> Bool) -> SemEq a -> [SemEq a] -> [SemEq a]   

lessSpecificEqCallPattern :: (a -> a -> Bool) -> SemEq a -> SemEq a -> Bool   

lessSpecificEqResult :: (a -> a -> Bool) -> SemEq a -> SemEq a -> Bool   

transformInt :: ADom a -> (SemEq a -> [SemEq a] -> [SemEq a]) -> [Rule] -> [SemEq a] -> [SemEq a] -> [SemEq a]   

extendListMap :: (a -> [b]) -> [a] -> [[b]]   

runFixpoint :: ADom a -> (SemEq a -> [SemEq a] -> [SemEq a]) -> [Rule] -> [(String,[a])] -> Bool -> ([SemEq a] -> [SemEq a] -> Bool) -> IO [SemEq a]   

computeFixpoint :: Bool -> Int -> (a -> String) -> (a -> a -> Bool) -> (a -> a) -> a -> IO a   

showSemInt :: ADom a -> [SemEq a] -> String   

getMainCall :: [Rule] -> (String,[Term])   

genMainCalls :: ADom a -> [Rule] -> [(String,[a])]   

printProgram :: ADom a -> [Rule] -> [(String,[a])] -> IO ()   

fEqsOfWorkSem :: String -> RedBlackTree (String,[([a],a,[String])]) -> [([a],a,[String])]   

processWorkList :: ADom a -> (SemEq a -> SemEq a -> Bool) -> Bool -> [Rule] -> [(String,[a])] -> RedBlackTree (String,[([a],a,[String])]) -> IO [SemEq a]   

runFixpointWL :: ADom a -> (SemEq a -> SemEq a -> Bool) -> [Rule] -> [(String,[a])] -> Bool -> IO [SemEq a]   

printTiming :: [(ProcessInfo,Int)] -> [(ProcessInfo,Int)] -> IO ()   

main :: IO ()   

Main calls to the (abstract) interpreters:

mainCallError :: [String] -> a   

checkArgs :: (Int,Bool,Bool,Bool,String) -> [String] -> (Int,Bool,Bool,Bool,String)   

callPatternAnalysis :: Int -> Bool -> Bool -> String -> IO ()   

transformNondet :: Int -> Bool -> Bool -> String -> IO ()   

unApply :: [Rule] -> [Rule]   

transformRules :: [(String,Bool)] -> [(String,[Int])] -> [Rule] -> ([Rule],Int)   

transformExp :: [(String,Bool)] -> [(String,[Int])] -> Term -> (Term,Bool,Int)   

extractStrictness :: ADom a -> [SemEq a] -> [(String,[Int])]   

sortFuncInfos :: [(String,a)] -> [(String,a)]   

showStrictness :: [(String,[Int])] -> String   

prog2DirFile :: String -> String   

Further infos:
  • solution complete, i.e., able to compute all solutions

bench :: Int -> String -> IO ()   

runBench :: IO ()