		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-var-reuse

Atj-vars-in-jexpr

Variables that will occur in the Java expression generated from an ACL2 term.

Signature
(atj-vars-in-jexpr term) → vars
Arguments: term — Guard (pseudo-termp term).
Returns: vars — Type (symbol-listp vars).

In the shallow embedding approach, each Java term is translated to a Java expression preceded by a Java block (which may be empty or not). The block is non-empty when the term involves lambda expressions, which become local variable assignments in Java, and if calls, which become if statements in Java. As detailed below, some of the variables in the ACL2 term will occur (as corresponding Java variables) in the Java expression; while others will only occur in the Java block. The ones that will occur in the Java expression are important for the correct marking of variables. This function returns the ACL2 variables in a term (as a set represented as a list without duplicates) that will occur in the Java expression generated from the term.

A quoted constant has no variables, and is always translated to a Java expression without variables. Thus, we return nil (i.e. the empty list of variables) in this case.

An ACL2 variable is translated to a corresponding variable in Java, and thus in this case we return the singleton list of the variable.

An if call is translated to a block with an if statement that performs all the evaluations of the test and branches, and the resulting Java expression is just a single fresh Java variable that has no counterpart in the ACL2 term. Thus, in this case we return nil (the empty list of variables).

A call of a named function different from if is translated to an expression that has subexpressions obtained by translating the arguments of the ACL2 function call. The expression is often a method call, with the subexpressions being its actual arguments, but it may also be an expression involving a Java operator (e.g. +) with the subexpressions as operands. Thus, in this case we return the union of the variables recursively computed for the argument terms.

A call of a lambda expression is translated to a Java block that assigns expressions to local variables that correspond to the formal parameters of the lambda expression, and to a Java expression obtained by translating the body of the lambda expression. Thus, in this case we return the variables recursively computed for the body of the lambda expression.

Theorem: return-type-of-atj-vars-in-jexpr.vars

(defthm return-type-of-atj-vars-in-jexpr.vars
  (b* ((?vars (atj-vars-in-jexpr term)))
    (symbol-listp vars))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-vars-in-jexpr-list.vars

(defthm return-type-of-atj-vars-in-jexpr-list.vars
  (b* ((?vars (atj-vars-in-jexpr-list terms)))
    (symbol-listp vars))
  :rule-classes :rewrite)

Subtopics

Atj-vars-in-jexpr-list