|
|
|---|
|
|
|
|---|
Pre-translation step performed by ATJ: marking of reusable lambda-bound variables.
Consider a function body of the form
(let ((x ...)) (let ((x ...)) (f x)))
The second
In contrast, consider a function body of the form
(let ((x ...)) (f (let ((x ...)) (f x)) (g x)))
Here, the second
When we translate ACL2 to Java,
let-bound variables become Java local variables.
In the first example above,
provided that the two
This pre-translation step analyzes terms to find out which lambda-bound (i.e. let-bound) variables can be reused and destructively updated. The lambda-bound variables are marked as either `new' or `old': the first marking means that the variable must be a new Java local variable that is declared and initilized; the second marking means that the variable can be an old Java local variable that is destructively assigned. These markings provide ``instructions'' to the ACL2-to-Java translation.
In the first example above the markings would be
(let (([n]x ...)) (let (([o]x ...)) (f [o]x)))
while in the second example above the markings would be
(let (([n]x ...)) (f (let (([n]x ...)) (f [n]x)) (g [n]x)))
Note that, as we mark the lambda-bound variables, we must mark in the same way the occurrences in the lambda bodies, to maintain the well-formedness of the ACL2 terms.
This pre-translation step must be performed after the type annotation step, so that types are kept into account: a variable can be reused only if it has the same type in both lambda formal parameters. Since the type annotation step adds types to variable names, by comparing names for equality we also compare their types for equality. If two variables have different types, they also have different names (since the name includes the type).
After this translation step, the variable renaming step takes care of renaming apart ACL2 variables with the same name that are both marked as `new'.