Module Analysis

Fixpoint analyzer for call patterns

Author: Michael Hanus

Version: February 2023

Summary of exported operations:

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

Exported datatypes:


ADom

Constructors:

  • ADom :: a -> (Int -> a) -> (String -> [a] -> a) -> ([Term] -> [a] -> Maybe (Sub a)) -> (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  Deterministic 

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

createAnalysisDir :: String -> IO ()  Deterministic 

ndInfoFileName :: String -> String  Deterministic 

strictInfoFileName :: String -> String  Deterministic 

adomBottom :: ADom a -> a  Deterministic 

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

adomShow :: ADom a -> a -> String  Deterministic 

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

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

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

lessCSpecific :: CTerm -> CTerm -> Bool  Deterministic 

showCTerm :: CTerm -> String  Deterministic 

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

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

cutDTerm :: Int -> DTerm -> DTerm  Deterministic 

lessDSpecific :: DTerm -> DTerm -> Bool  Deterministic 

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

showDTerm :: DTerm -> String  Deterministic 

depthDom :: Int -> ADom DTerm  Deterministic 

eqSemInt :: Eq a => [SemEq a] -> [SemEq a] -> Bool  Deterministic 

insertSemEq :: Ord a => SemEq a -> [SemEq a] -> [SemEq a]  Deterministic 

updateSemEq :: Ord a => (SemEq a -> SemEq a -> Bool) -> SemEq a -> [SemEq a] -> [SemEq a]  Deterministic 

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

lessSpecificEqResult :: Eq a => (a -> a -> Bool) -> SemEq a -> SemEq a -> Bool  Deterministic 

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

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

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

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

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

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

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

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

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

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

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

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

main :: IO ()  Non-deterministic 

Main calls to the (abstract) interpreters:

mainCallError :: [String] -> a  Deterministic 

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

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

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

unApply :: [Rule] -> [Rule]  Deterministic 

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

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

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

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

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

dataModule :: TypeDecl -> String  Deterministic 

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

prog2DirFile :: String -> String  Deterministic 

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

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

runBench :: IO ()  Non-deterministic