Module Verify.CallTypes

failCallType :: [[CallType]]   

The call type of an operation which has no non-failing arguments.

Further infos:

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

isFailCallType :: [[CallType]] -> Bool   

Is the call type a failure call type?

Further infos:

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

prettyCT :: CallType -> String   

prettyFunCallTypes :: [[CallType]] -> String   

prettyCallTypeArgs :: [CallType] -> String   

simpFuncCallType :: [[((String,String),Int)]] -> [[CallType]] -> [[CallType]]   

Simplify call types by recursively transforming each complete list of constructors with AnyT arguments to AnyT.

joinCT :: CallType -> CallType -> CallType   

unionCT :: CallType -> CallType -> CallType   

unionCTs :: [[CallType]] -> [[CallType]] -> [[CallType]]   

Least-upper bound (union) on lists of argument call types.

addCTArgs :: [CallType] -> [[CallType]] -> [[CallType]]   

Adds a new list of argument types to a given list of alternative arg types

combineOneDiffCT :: [CallType] -> [CallType] -> [CallType]   

Combine to argument call types having exact one different argument.

insertCT :: ((String,String),[CallType]) -> [((String,String),[CallType])] -> [((String,String),[CallType])]   

numDiffs :: Eq a => [a] -> [a] -> Int   

Count the number of pairwise different elements in a list.

isTotalCallType :: [[CallType]] -> Bool   

addCons2CT :: (String,String) -> Int -> [Int] -> [CallType] -> [CallType]   

Adds a constructor with a given arity at a position to a given list of argument call types.

addConsInCT :: (String,String) -> Int -> [Int] -> CallType -> CallType   

testAddCons2CT1 :: [CallType]   

testAddCons2CT2 :: [CallType]   

initCallTypeState :: Options -> (String,String) -> [Int] -> CallTypeState   

callTypeFunc :: Options -> [[((String,String),Int)]] -> FuncDecl -> ((String,String),[[CallType]])   

Computes the call type of a function where all constructors are provided as the second argument. The computed call type for an n-ary function is a disjunction (represented as a list) of alternative call types where each element in the disjunction is list of n call types for each argument.

defaultCallTypes :: [((String,String),[[CallType]])]   

Some call types for predefined operations. The fail call types for arithmetic operations could be improved in the future by considering refined number types.

callTypeExternalFunc :: (String,String) -> Int -> ((String,String),[[CallType]])   

Computes the call type of an external (primitive) function. Currently, we assume that they are total functions.

addFreshVars :: [Int] -> CallTypeState -> CallTypeState   

callTypeExpr :: CallTypeState -> Expr -> [[CallType]]   

funcCallType2AType :: TermDomain a => [[((String,String),Int)]] -> ((String,String),[[CallType]]) -> ((String,String),Maybe [a])   

Transforms a call type for an operation, i.e., a disjunction of a list of alternative call types for the arguments, into an abstract call type. Since the abstract call type of an operation is a single list of abstract call types for the arguments so that a disjunction of argument lists cannot be expressed, the disjunctions are joined (i.e., intersected).

normalizeAType :: TermDomain a => [[((String,String),Int)]] -> a -> a   

Normalize an abstract type by recursively replacing complete sets of constructors with anyType arguments by anyType. Note that this works only for abstract values which are depth-bounded, i.e., not for regular types. Thus, this operation might be better moved into the implementation of a particular abstract domain.

isTotalACallType :: TermDomain a => Maybe [a] -> Bool   

failACallType :: TermDomain a => Maybe [a]   

The call type of an operation which has no non-failing arguments expressible by call types for the arguments.

Further infos:

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

isFailACallType :: TermDomain a => Maybe [a] -> Bool   

Is the call type a failure call type?

Further infos:

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

prettyFunCallAType :: TermDomain a => Maybe [a] -> String   

joinACallType :: TermDomain a => Maybe [a] -> Maybe [a] -> Maybe [a]   

Join two abstract call types.

subtypeOfRequiredCallType :: TermDomain a => [a] -> Maybe [a] -> Bool   

Is a list of abstract call types (first argument) a subtype of the call type of an operation (second argument)?

isSubtypeOf :: TermDomain a => a -> a -> Bool   

specializeToRequiredType :: TermDomain a => [(Int,a)] -> Maybe [a] -> Maybe [(Int,a)]   

Is it possible to specialize the abstract types of the given argument variables so that their type is a subtype of the function call type given in the second argument? If yes, the specialized argument variable types are returned.