Atj-function-type
Fixtype of ATJ function types.
This is a product type introduced by fty::defprod.
Fields
- inputs — atj-type-list
- outputs — atj-type-list
- arrays — symbol-list
An ATJ function type consists of
(zero or more) types for the arguments (i.e. inputs)
and (one or more) types for the results (i.e. outputs).
This is like an arrow type in higher-order languages.
We also augment the output types with array names.
These are represented via a list of symbols,
whose length must match the length of the output type list
(this length constraint is not explicitly captured in this fixtype,
but it is an expected invariant).
The nil symbol may be used in any position of the array name list,
meaning that there is no array name for the corresponding output type.
A non-nil symbol may be used only in a position
whose corresponding output type is a :jprimarr type.
In this case the symbol must match a formal parameter of the function
that has the same array type as input type.
The non-nil symbols must be all distinct.
The purpose of these array names is to support
the analysis of single-threaded use of Java primitive arrays
described at atj-pre-translation-array-analysis.
The idea is that if a function takes an array as input
(i.e. that input type is a :jprimarr type)
and if the function may modify that array (directly or indirectly),
then the possibly modified array must be returned as a result:
an explicit non-nil array name assigned to a result
specifies which result that is, and simplifies the analysis.
If instead a function does not modify an input array,
no result with the same name as the input needs to exist.
Results of non-array types use nil as array (non-)name.
If a function creates an array (directly or indirectly) and returns it,
then nil is used for that result,
i.e. the array has no name because it does not modify any input array
(and thus there is no input name to match);
it represents a newly created array.
Subtopics
- Atj-function-type-fix
- Fixing function for atj-function-type structures.
- Atj-function-type-equiv
- Basic equivalence relation for atj-function-type structures.
- Make-atj-function-type
- Basic constructor macro for atj-function-type structures.
- Atj-function-type->outputs
- Get the outputs field from a atj-function-type.
- Atj-function-type->inputs
- Get the inputs field from a atj-function-type.
- Atj-function-type->arrays
- Get the arrays field from a atj-function-type.
- Change-atj-function-type
- Modifying constructor for atj-function-type structures.
- Atj-function-type-p
- Recognizer for atj-function-type structures.
