The definition of input/output types and operations to infer and manipulate such types.
Author: Michael Hanus
Version: December 2023
trivialInOutType
:: TermDomain a => Int -> InOutType a
The trivial InOutType
for a function of a given arity.
|
isAnyIOType
:: TermDomain a => InOutType a -> Bool
|
showIOT
:: TermDomain a => InOutType a -> String
|
inOutATypeFunc
:: TermDomain a => ((String,String) -> a) -> FuncDecl -> ((String,String),InOutType a)
Compute the in/out type for a function declaration w.r.t. |
ioVarType
:: TermDomain a => a -> [(InOutType a,[Int])]
An abstract type represented as an input/output type for a variable. |
showVarTypes
:: TermDomain a => [(Int,[(InOutType a,[Int])])] -> String
Shows a list of input/output variables types. |
showArgumentVars
:: [Int] -> String
Shows a list of argument variables in parentheses. |
addVarType2Map
:: TermDomain a => Int -> [(InOutType a,[Int])] -> [(Int,[(InOutType a,[Int])])] -> [(Int,[(InOutType a,[Int])])]
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])])]
Concatenates two VarTypesMap s.
|
setVarTypeInMap
:: TermDomain a => Int -> [(InOutType a,[Int])] -> [(Int,[(InOutType a,[Int])])] -> [(Int,[(InOutType a,[Int])])]
Replaces the variable types of a variable in a VarTypesMap .
|
bindVarInIOTypes
:: TermDomain a => Int -> a -> [(Int,[(InOutType a,[Int])])] -> [(Int,[(InOutType a,[Int])])]
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])])]
Simplify a set of input/output variable types by exploiting information about definitive abstract types (i.e., constructors). |
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
An input/output variable type (v,iot,vs)
consists of
v
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
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])]
The VarTypesMap
is a mapping from variables to their variable types.
Type synonym: VarTypesMap a = [(Int,VarTypes a)]
The trivial |
|
|
Compute the in/out type for a function declaration w.r.t. a given assignment of function names to result types. |
An abstract type represented as an input/output type for a variable.
|
Shows a list of input/output variables types. |
Shows a list of argument variables in parentheses. |
Adds variable types for a given variable to a |
Concatenates two |
Replaces the variable types of a variable in a |
Adds the binding of a variable to an abstract type (usually, the abstract representation of a constructor) to the variable type map. |
Simplify a set of input/output variable types by exploiting information about definitive abstract types (i.e., constructors). |