Module Verify.CallTypes

The definition of call types and an operation to infer them.

Author: Michael Hanus

Version: January 2024

Summary of exported operations:

failCallType :: [[CallType]]  Deterministic 
The call type of an operation which has no non-failing arguments.
isFailCallType :: [[CallType]] -> Bool  Deterministic 
Is the call type a failure call type?
prettyCT :: CallType -> String  Deterministic 
prettyFunCallTypes :: [[CallType]] -> String  Deterministic 
prettyCallTypeArgs :: [CallType] -> String  Deterministic 
simpFuncCallType :: [((String,String),(Int,ConsType,[((String,String),Int)]))] -> [[CallType]] -> [[CallType]]  Deterministic 
Simplify call types by recursively transforming each complete list of constructors with AnyT arguments to AnyT.
joinCT :: CallType -> CallType -> CallType  Deterministic 
unionCT :: CallType -> CallType -> CallType  Deterministic 
unionCTs :: [[CallType]] -> [[CallType]] -> [[CallType]]  Deterministic 
Least-upper bound (union) on lists of argument call types.
addCTArgs :: [CallType] -> [[CallType]] -> [[CallType]]  Deterministic 
Adds a new list of argument types to a given list of alternative arg types
combineOneDiffCT :: [CallType] -> [CallType] -> [CallType]  Deterministic 
Combine to argument call types having exact one different argument.
insertCT :: ((String,String),[CallType]) -> [((String,String),[CallType])] -> [((String,String),[CallType])]  Deterministic 
numDiffs :: Eq a => [a] -> [a] -> Int  Deterministic 
Count the number of pairwise different elements in a list.
isTotalCallType :: [[CallType]] -> Bool  Deterministic 
addCons2CT :: (String,String) -> Int -> [Int] -> [CallType] -> [CallType]  Deterministic 
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  Deterministic 
testAddCons2CT1 :: [CallType]  Deterministic 
testAddCons2CT2 :: [CallType]  Deterministic 
initCallTypeState :: Options -> (String,String) -> [Int] -> CallTypeState  Deterministic 
callTypeFunc :: Options -> [((String,String),(Int,ConsType,[((String,String),Int)]))] -> FuncDecl -> ((String,String),[[CallType]])  Deterministic 
Computes the call type of a function where all constructors are provided as the second argument.
defaultCallTypes :: [((String,String),[[CallType]])]  Deterministic 
Some call types for predefined operations.
callTypeExternalFunc :: (String,String) -> Int -> ((String,String),[[CallType]])  Deterministic 
Computes the call type of an external (primitive) function.
addFreshVars :: [Int] -> CallTypeState -> CallTypeState  Deterministic 
callTypeExpr :: CallTypeState -> Expr -> [[CallType]]  Deterministic 
funcCallType2AType :: TermDomain a => [((String,String),(Int,ConsType,[((String,String),Int)]))] -> ((String,String),[[CallType]]) -> ((String,String),Maybe [a])  Deterministic 
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.
normalizeAType :: TermDomain a => [((String,String),(Int,ConsType,[((String,String),Int)]))] -> a -> a  Deterministic 
Normalize an abstract type by recursively replacing complete sets of constructors with anyType arguments by anyType.
isTotalACallType :: TermDomain a => Maybe [a] -> Bool  Deterministic 
failACallType :: TermDomain a => Maybe [a]  Deterministic 
The call type of an operation which has no non-failing arguments expressible by call types for the arguments.
isFailACallType :: TermDomain a => Maybe [a] -> Bool  Deterministic 
Is the call type a failure call type?
prettyFunCallAType :: TermDomain a => Maybe [a] -> String  Deterministic 
joinACallType :: TermDomain a => Maybe [a] -> Maybe [a] -> Maybe [a]  Deterministic 
Join two abstract call types.
subtypeOfRequiredCallType :: TermDomain a => [a] -> Maybe [a] -> Bool  Deterministic 
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  Deterministic 
specializeToRequiredType :: TermDomain a => [(Int,a)] -> Maybe [a] -> Maybe [(Int,a)]  Deterministic 
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.

Exported datatypes:


CallType

A call type is intended to specify the conditions on arguments so that a function call satisfying the call type is reducible (i.e., some rule matches).

A call type is either AnyT (any term matches) or a list of possible constructors with their argument call types. Note that literals l are represented as MCons [(("",l),[])]. This also implies that their siblings are unknown.

Constructors:


CallTypeState

The state passed to compute call types contains a mapping from variables (indices) to their positions and the call type of the current branch of the operation to be analyzed.

Constructors:


ACallType

Type synonym: ACallType a = Maybe [a]


Exported operations:

failCallType :: [[CallType]]  Deterministic 

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  Deterministic 

Is the call type a failure call type?

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

prettyCT :: CallType -> String  Deterministic 

prettyFunCallTypes :: [[CallType]] -> String  Deterministic 

prettyCallTypeArgs :: [CallType] -> String  Deterministic 

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

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

joinCT :: CallType -> CallType -> CallType  Deterministic 

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

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

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

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

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

Combine to argument call types having exact one different argument.

Further infos:
  • partially defined

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

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

Count the number of pairwise different elements in a list.

isTotalCallType :: [[CallType]] -> Bool  Deterministic 

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

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  Deterministic 

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

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

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]])]  Deterministic 

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]])  Deterministic 

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

Further infos:
  • partially defined

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

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,ConsType,[((String,String),Int)]))] -> a -> a  Deterministic 

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  Deterministic 

failACallType :: TermDomain a => Maybe [a]  Deterministic 

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  Deterministic 

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  Deterministic 

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

Join two abstract call types.

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

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  Deterministic 

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

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.