Module Verify.IOTypes

The definition of input/output types and operations to infer and manipulate such types.

Author: Michael Hanus

Version: December 2023

Summary of exported operations:

trivialInOutType :: TermDomain a => Int -> InOutType a  Deterministic 
The trivial InOutType for a function of a given arity.
isAnyIOType :: TermDomain a => InOutType a -> Bool  Deterministic 
showIOT :: TermDomain a => InOutType a -> String  Deterministic 
inOutATypeFunc :: TermDomain a => ((String,String) -> a) -> FuncDecl -> ((String,String),InOutType a)  Deterministic 
Compute the in/out type for a function declaration w.r.t.
ioVarType :: TermDomain a => a -> [(InOutType a,[Int])]  Deterministic 
An abstract type represented as an input/output type for a variable.
showVarTypes :: TermDomain a => [(Int,[(InOutType a,[Int])])] -> String  Deterministic 
Shows a list of input/output variables types.
showArgumentVars :: [Int] -> String  Deterministic 
Shows a list of argument variables in parentheses.
addVarType2Map :: TermDomain a => Int -> [(InOutType a,[Int])] -> [(Int,[(InOutType a,[Int])])] -> [(Int,[(InOutType a,[Int])])]  Deterministic 
Adds variable types for a given variable to a VarTypesMap.
concVarTypesMap :: TermDomain a => [(Int,[(InOutType a,[Int])])] -> [(Int,[(InOutType a,[Int])])] -> [(Int,[(InOutType a,[Int])])]  Deterministic 
Concatenates two VarTypesMaps.
setVarTypeInMap :: TermDomain a => Int -> [(InOutType a,[Int])] -> [(Int,[(InOutType a,[Int])])] -> [(Int,[(InOutType a,[Int])])]  Deterministic 
Replaces the variable types of a variable in a VarTypesMap.
bindVarInIOTypes :: TermDomain a => Int -> a -> [(Int,[(InOutType a,[Int])])] -> [(Int,[(InOutType a,[Int])])]  Deterministic 
Adds the binding of a variable to an abstract type (usually, the abstract representation of a constructor) to the variable type map.
simplifyVarTypes :: TermDomain a => [(Int,[(InOutType a,[Int])])] -> [(Int,[(InOutType a,[Int])])]  Deterministic 
Simplify a set of input/output variable types by exploiting information about definitive abstract types (i.e., constructors).

Exported datatypes:

InOutType

An InOutType is a disjunction, represented as a list, of input/output type pairs. It is parameterized over the abstract term domain.

Constructors:

  • IOT :: [([a],a)] -> InOutType a
VarTypes

An input/output variable type (v,iot,vs) consists of

  • a variable v
  • an input/output type iot specifying the result of v, i.e., either the input/output type of the function bound to v or simply {() |-> any} if the variable is unbound
  • the list vs of arguments of the function to which v is bound (which could be empty).

In order to combine all in/out variables types for a variable, we represent it by the variable and a disjunction of in/out types and their argument variables, represented as a list. This disjunction is defined by the following type:

Type synonym: VarTypes a = [(InOutType a,[Int])]

VarTypesMap

The VarTypesMap is a mapping from variables to their variable types.

Type synonym: VarTypesMap a = [(Int,VarTypes a)]

Exported operations:

trivialInOutType :: TermDomain a => Int -> InOutType a  Deterministic 

The trivial InOutType for a function of a given arity.

isAnyIOType :: TermDomain a => InOutType a -> Bool  Deterministic 

showIOT :: TermDomain a => InOutType a -> String  Deterministic 

inOutATypeFunc :: TermDomain a => ((String,String) -> a) -> FuncDecl -> ((String,String),InOutType a)  Deterministic 

Compute the in/out type for a function declaration w.r.t. a given assignment of function names to result types.

ioVarType :: TermDomain a => a -> [(InOutType a,[Int])]  Deterministic 

An abstract type represented as an input/output type for a variable.

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

showVarTypes :: TermDomain a => [(Int,[(InOutType a,[Int])])] -> String  Deterministic 

Shows a list of input/output variables types.

showArgumentVars :: [Int] -> String  Deterministic 

Shows a list of argument variables in parentheses.

addVarType2Map :: TermDomain a => Int -> [(InOutType a,[Int])] -> [(Int,[(InOutType a,[Int])])] -> [(Int,[(InOutType a,[Int])])]  Deterministic 

Adds variable types for a given variable to a VarTypesMap.

concVarTypesMap :: TermDomain a => [(Int,[(InOutType a,[Int])])] -> [(Int,[(InOutType a,[Int])])] -> [(Int,[(InOutType a,[Int])])]  Deterministic 

Concatenates two VarTypesMaps.

setVarTypeInMap :: TermDomain a => Int -> [(InOutType a,[Int])] -> [(Int,[(InOutType a,[Int])])] -> [(Int,[(InOutType a,[Int])])]  Deterministic 

Replaces the variable types of a variable in a VarTypesMap.

bindVarInIOTypes :: TermDomain a => Int -> a -> [(Int,[(InOutType a,[Int])])] -> [(Int,[(InOutType a,[Int])])]  Deterministic 

Adds the binding of a variable to an abstract type (usually, the abstract representation of a constructor) to the variable type map.

simplifyVarTypes :: TermDomain a => [(Int,[(InOutType a,[Int])])] -> [(Int,[(InOutType a,[Int])])]  Deterministic 

Simplify a set of input/output variable types by exploiting information about definitive abstract types (i.e., constructors).