Atj-type-annotate-term
Add ATJ type annotations to ACL2 terms.
- Signature
(atj-type-annotate-term term required-types?
var-types mv-typess guards$ wrld)
→
(mv annotated-term resulting-types new-mv-typess)
- Arguments
- term — Guard (pseudo-termp term).
- required-types? — Guard (atj-type-listp required-types?).
- var-types — Guard (atj-symbol-type-alistp var-types).
- mv-typess — Guard (atj-type-list-listp mv-typess).
- guards$ — Guard (booleanp guards$).
- wrld — Guard (plist-worldp wrld).
- Returns
- annotated-term — Type (pseudo-termp annotated-term).
- resulting-types — Type (and (atj-type-listp resulting-types) (consp resulting-types)).
- new-mv-typess — Type (and (atj-type-list-listp new-mv-typess) (cons-listp new-mv-typess)).
The type annotation procedure involves inferring the types of terms,
and wrapping terms with type conversion functions
to match certain type requirements.
The var-types input assigns types to (at least)
all the free variables in the term that is being annotated.
At the top level (see atj-type-annotate-formals+body),
var-types is initialized with the formal parameters of a function
and with its corresponding input types.
When we encounter a lambda expression in a term,
var-types is updated with an alist that assigns
to the formal parameters of the lambda expression
the types inferred for the actual arguments of the lambda expression;
that is, unlike at the top level, at intermediate levels
variables receive the types inferred for their binding terms.
Here `updated' means that
the new alist is appended before the existing one:
recall that, due to the pre-translation step
that removes trivial lambda-bound variables,
lambda expressions may not be closed at this point;
thus, the appending achieves the desired ``overwriting''.
Even though variables can be annotated by multiple types in general
(see atj-type-annotate-var),
var-types assigns single types to variables.
The only variables annotated with lists of two or more types
are the mv vars that arise in the translation of mv-let
(see fty-check-mv-let-call).
These mv variables are treated specially
by the type annotation process,
without a need to add them to var-types.
The required-types? input specifies
the type(s) required for the term, if any.
This is nil if there are no requirements;
it is a singleton list if the term is single-valued;
it is a list of two or more types if the term is multi-valued.
At the top level (see atj-type-annotate-formals+body),
required-types? consists of the output type(s) of the function
(singleton if single-valued, of length two or more if multi-valued):
the body of the function must have the output type(s) of the function.
The recursive function atj-type-annotate-args,
which operates on the arguments of a function call,
does not take a list of required types as input.
The result of annotating a term is not only the annotated term,
but also the type(s) of the wrapped term.
This is always the same as the required types
when there are required types;
when there are no required types,
the resulting type(s) is/are the one(s) inferred for the term.
The type inferred for a variable is the one assigned by var-types.
(As already mentioned before,
the mv variables annotated with two or more types
are handled specially;
they are never passed to this function directly.)
We annotate the variable with its associated type;
note that the variable names in var-types
do not have type annotations.
We wrap the variable with a type conversion function
from the inferred type(s) to the required type(s) if supplied,
or to the inferred type(s) (i.e. no-op conversion) if not supplied.
The type inferred for a quoted constant
is determined by the value of the quoted constant.
We wrap the quoted constant with a type conversion function
as discussed above.
The non-strict function if is treated specially,
because eventually it is translated to a Java if,
which assigns either the `then' part or the `else' part
to a Java local variable.
The type of the Java local variable is
(the Java counterpart of) required-types? if supplied:
in this case, when required-types? is recursively passed
to the second and third argument of the if,
both terms will be wrapped so that they have the required type(s).
However, if required-types? is nil,
the recursive annotation of the `then' and `else' subterms
may produce different types,
and so in this case we re-wrap those terms
with the least upper bound of the two types.
The case of a term of the form (if a a b)
is treated a little differently,
but there is no substantial difference.
In the general case of (if a b c) with a different from b,
there is never any required type for the test a,
because in the Java code it is just used
to generate the test of the if;
ACL2 should ensure that the test of an if is single-valued,
but we defensively check for that.
In all cases, the if is wrapped with
the identify conversion function for the overall type(s),
for uniformity and to readily indicate the type
of the Java local variable to generate.
For a lambda expression
(other than the kind resulting from an mv-let,
whose treatment is described below),
the argument terms are annotated without required types.
The inferred types are then assigned to the formal parameters
when the body of the lambda expression is annotated.
We annotate all the formal parameters of the lambda expression;
but note that the new var-types has non-annotated variable names.
Note that the list of types returned by atj-type-annotate-args
has a different meaning from
the one returned by atj-type-annotate-term:
while the latter is a single or multiple type for a single term,
the latter consists of a single type for each argument
(more on this below).
For a named function call
other than mv
(whose treatment is described below)
and other than the array creation functions
in *atj-jprimarr-new-init-fns*
(whose treatment is also described below),
the function's types are obtained.
We first try annotating the argument terms without required types
(as done for a lambda expression as explained above),
thus inferring types for the arguments.
Then we look for the function types (of the named function)
whose input types are wider than or the same as
the inferred argument types.
If there are some, we select the one whose input types are the least
(this always exists because of the closure property
checked by atj-other-function-type;
see the documentation of that macro and supporting functions for details);
we then use the output type(s) of the selected function type
as the type(s) inferred for the function call,
and wrap it to adapt to the required type(s) for the function call if any.
The successful selection of such a function type means that,
in the generated Java code, an overloaded method will be called
based on the argument types inferred by the Java compiler.
If there are no function types satisfying the above condition,
we look at the primary function type (which always exists),
and its input types become the required ones for the argument terms,
while the output type(s) are used to infer the type(s) for the call,
which is then wrapped as needed to match the required type(s) if any.
If we encounter a call of mv,
which may be introduced by a previous pre-translation step,
we allow its arguments to have any types
and we regard the call as having the multiple type obtained
by putting the argument types into a list.
We also collect the required (if present) or inferred (otherwise) types
in a list without duplications that is threaded through these functions.
This list does not affect the type annotations,
but is used by the code generation functions
in order to determine which mv classes must be generated.
If we encounter a call of
an array creation function in *atj-jprimarr-new-init-fns*,
and if :guards is t,
we ensure that its (only) argument is a translated list call,
i.e. a (possibly empty) nest of conses
ending with a quoted nil.
If it is not, we stop with an error,
which is really a (deep) input validation error.
If it is a list call, we extract its element terms.
We type-annotate them, and we ensure that their result types
are consistent with the array's component type.
If they are not, it is a (deep) input validation error.
If everything checks, then we make the annotated arguments
directly arguments of the array creation function,
which therefore is now treated
as a function with a variable number of arguments.
Before attempting to process lambda expression or named function calls
as described above,
we first check whether the term is a translated mv-let.
For this to be the case,
not only fty-check-mv-let-call must succeed,
yielding variables var1, ..., varn
and subterms mv-term and body-term,
but also the term assigned to the mv variable
must have multiple types.
If the term is not a translated mv-let,
the term is processed as any other term.
If the term is a translated mv-let,
we annotate it by building a term of the form
([reqinf>reqinf]
((lambda ([types]mv)
([reqinf>reqinf]
((lambda ([type1]var1 ... [typen]varn)
([...>reqinf] body-term))
([AV>type1] (mv-nth ([AI>AI] '0)
([types>types] [types]mv)))
...
([AV>typen] (mv-nth ([AI>AI] 'n-1)
([types>types] [types]mv))))))
([types>types] mv-term)))
where types consists of type1, ..., typen,
and where reqinf is required-types? if non-nil
or otherwise the types inferred for body-term.
This term is systematically annotated in the same way as any other term,
so that subsequent pre-processing steps can treat all terms uniformly.
The [AV>typei] conversions
are consistent with the function type of mv-nth,
so that, as we are adding more direct support for mv in ATJ,
the code generation functions can still treat these newly annotated terms
as before, i.e. treating multiple values as lists.
The function atj-type-annotate-mv-let first checks whether the term
has the structure of a translated mv-let.
Then it annotates the term to which the mv variable is bound,
inferring a non-empty list of types (i.e. types above) for it:
if the list is a singleton,
the term is actually not a translated mv-let,
and the function returns a failure,
letting atj-type-annotate-term handle the term.
Otherwise, after checking that the number of types
is consistent with the number of variables
(this is never expected to fail),
we annotate the body term:
we pass the top-level required types (if any),
and we update var-types with the mv-let variables
associated to the types for the term to which mv is bound;
we do not need to update var-types with mv
because fty-check-mv-let-call ensures that
the variable mv does not occur free in the body term.
Note that, in general, some variables bound to mv-nth calls
may have been removed by a previous pre-translation step,
the one that removes unused variables (see fty-check-mv-let-call);
thus, in order to extend var-types,
we select the types for which there are actually variables.
In atj-type-annotate-args, we check that
the types inferred for each single argument are a singleton.
Except for the argument of ((lambda (mv) ...) mv-term)
in a translated mv-let,
in ACL2 all the arguments of function calls must be single-valued.
We do not expect this check to ever fail.
Note that an annotated term is still a regular term,
but it has a certain structure.
Theorem: return-type-of-atj-type-annotate-term.annotated-term
(defthm return-type-of-atj-type-annotate-term.annotated-term
(b* (((mv ?annotated-term
?resulting-types ?new-mv-typess)
(atj-type-annotate-term term required-types?
var-types mv-typess guards$ wrld)))
(pseudo-termp annotated-term))
:rule-classes :rewrite)
Theorem: return-type-of-atj-type-annotate-term.resulting-types
(defthm return-type-of-atj-type-annotate-term.resulting-types
(b* (((mv ?annotated-term
?resulting-types ?new-mv-typess)
(atj-type-annotate-term term required-types?
var-types mv-typess guards$ wrld)))
(and (atj-type-listp resulting-types)
(consp resulting-types)))
:rule-classes :rewrite)
Theorem: return-type-of-atj-type-annotate-term.new-mv-typess
(defthm return-type-of-atj-type-annotate-term.new-mv-typess
(b* (((mv ?annotated-term
?resulting-types ?new-mv-typess)
(atj-type-annotate-term term required-types?
var-types mv-typess guards$ wrld)))
(and (atj-type-list-listp new-mv-typess)
(cons-listp new-mv-typess)))
:rule-classes :rewrite)
Theorem: return-type-of-atj-type-annotate-mv-let.success
(defthm return-type-of-atj-type-annotate-mv-let.success
(b* (((mv ?success ?annotated-term
?resulting-types ?new-mv-typess)
(atj-type-annotate-mv-let term required-types?
var-types mv-typess guards$ wrld)))
(booleanp success))
:rule-classes :rewrite)
Theorem: return-type-of-atj-type-annotate-mv-let.annotated-term
(defthm return-type-of-atj-type-annotate-mv-let.annotated-term
(b* (((mv ?success ?annotated-term
?resulting-types ?new-mv-typess)
(atj-type-annotate-mv-let term required-types?
var-types mv-typess guards$ wrld)))
(pseudo-termp annotated-term))
:rule-classes :rewrite)
Theorem: return-type-of-atj-type-annotate-mv-let.resulting-types
(defthm return-type-of-atj-type-annotate-mv-let.resulting-types
(b* (((mv ?success ?annotated-term
?resulting-types ?new-mv-typess)
(atj-type-annotate-mv-let term required-types?
var-types mv-typess guards$ wrld)))
(and (atj-type-listp resulting-types)
(consp resulting-types)))
:rule-classes :rewrite)
Theorem: return-type-of-atj-type-annotate-mv-let.new-mv-typess
(defthm return-type-of-atj-type-annotate-mv-let.new-mv-typess
(b* (((mv ?success ?annotated-term
?resulting-types ?new-mv-typess)
(atj-type-annotate-mv-let term required-types?
var-types mv-typess guards$ wrld)))
(and (atj-type-list-listp new-mv-typess)
(cons-listp new-mv-typess)))
:rule-classes :rewrite)
Theorem: return-type-of-atj-type-annotate-args.annotated-args
(defthm return-type-of-atj-type-annotate-args.annotated-args
(b*
(((mv ?annotated-args
?resulting-types ?new-mv-typess)
(atj-type-annotate-args args var-types mv-typess guards$ wrld)))
(and (pseudo-term-listp annotated-args)
(equal (len annotated-args)
(len args))))
:rule-classes :rewrite)
Theorem: return-type-of-atj-type-annotate-args.resulting-types
(defthm return-type-of-atj-type-annotate-args.resulting-types
(b*
(((mv ?annotated-args
?resulting-types ?new-mv-typess)
(atj-type-annotate-args args var-types mv-typess guards$ wrld)))
(and (atj-type-listp resulting-types)
(equal (len resulting-types)
(len args))))
:rule-classes :rewrite)
Theorem: return-type-of-atj-type-annotate-args.new-mv-typess
(defthm return-type-of-atj-type-annotate-args.new-mv-typess
(b*
(((mv ?annotated-args
?resulting-types ?new-mv-typess)
(atj-type-annotate-args args var-types mv-typess guards$ wrld)))
(and (atj-type-list-listp new-mv-typess)
(cons-listp new-mv-typess)))
:rule-classes :rewrite)
Subtopics
- Atj-type-annotate-args
- Atj-type-annotate-mv-let