		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-var-renaming

Atj-rename-formal

Rename a formal parameters of a defined function or lambda expression.

Signature
(atj-rename-formal var indices curr-pkg vars-by-name) → (mv new-var new-indices)
Arguments: var — Guard (symbolp var).; indices — Guard (symbol-pos-alistp indices).; curr-pkg — Guard (stringp curr-pkg).; vars-by-name — Guard (string-symbollist-alistp vars-by-name).
Returns: new-var — Type (symbolp new-var).; new-indices — Type (symbol-pos-alistp new-indices), given (and (symbol-pos-alistp indices) (symbolp var)).

As explained in atj-rename-formals, the renaming of a variable is established when the variable is encountered as a formal parameter. This motivates the name of this function.

This function is called only on formal parameters marked as `new'. Formal parameters marked as `old' are just renamed according to the existing renaming map renaming-old.

Each ACL2 function is turned into a Java method, whose body is a shallowly embedded representation of the ACL2 function body. The ACL2 function body may reference the ACL2 function's parameter, as well as let-bound variables (via lambda expressions). Thus, the same variable symbol may in fact denote different variables in different parts of an ACL2 function body. Java does not allow different local variables with the same name in (nested scopes in) the same method, and so we need to map homonymous but different ACL2 variables in the same ACL2 function to differently named Java variables in the same Java method. We use numeric indices, one for each variable name, which is appended (as explained below) to the Java variable name to make it unique within the Java mehtod.

Another need for disambiguation arises because of package prefixes. An ACL2 variable is a symbol, which consists of a name and also a package name: two distinct variables may have the same name but different package names. However, when we append the package name and the name of the symbol, we have unique Java variable names.

We use atj-var-to-jvar to turn var into a new symbol whose name is a valid Java variable name. Then we ensure its uniqueness by retrieving and using the next index, from the parameter indices; more on this below. In general, as mentioned in atj-var-to-jvar, we append the index after the result of atj-var-to-jvar; but if the index is 0, we do not append it, to improve readability; in particular, if there is just one variable with a certain name, since we start with index 0, no index is ever added to the name. When this function is called, the indices alist always associates non-0 indices to the symbols whose names are in *atj-disallowed-jvar-names*: see *atj-init-indices*.

The name obtained by optionally appending the index may not be a valid Java identifier: this happens if it is a Java keyword or literal, or if it is empty. (This may actually happen only if no index is appended.) If this is the case, we add a single $ at the end, which makes the name valid and unambiguous.

The index to use for this variable is retrieved from the indices parameter, which is an alist that associates each variable to its next index to use. If a variable is not in the alist, it is as if it had index 0, and in that case no index is added, as explained above. The alist is updated by incrementing the next index to use for the variable, and returned along with the new variable.

The keys of the alist are not the original ACL2 variables, but the renamed variables resulting from atj-var-to-jvar. This gives us more flexibility, by obviating the requirement that atj-var-to-jvar be injective: if this function is not injective, then different ACL2 variables may become the same Java variable, and the next index must be the same for all of these variables, so that they can be properly disambiguated.

This pre-translation step is performed after the type annotation and new/old marking steps, but the caller of this function decomposes the marked annotated variable into its unmarked unannotated name, type, and marking, and only passes the unannotated name var to this function. The vars-by-name parameter of this function consists of variable names without annotations and markings.

Definitions and Theorems

Function: atj-rename-formal

(defun atj-rename-formal (var indices curr-pkg vars-by-name)
  (declare
       (xargs :guard (and (symbolp var)
                          (symbol-pos-alistp indices)
                          (stringp curr-pkg)
                          (string-symbollist-alistp vars-by-name))))
  (declare (xargs :guard (not (equal curr-pkg ""))))
  (let ((__function__ 'atj-rename-formal))
    (declare (ignorable __function__))
    (b* ((jvar (atj-var-to-jvar var curr-pkg vars-by-name))
         (jvar+index? (assoc-eq jvar indices))
         (index (if jvar+index? (cdr jvar+index?) 0))
         (indices (acons jvar (1+ index) indices))
         (jvar (atj-var-add-index jvar index)))
      (mv jvar indices))))

Theorem: symbolp-of-atj-rename-formal.new-var

(defthm symbolp-of-atj-rename-formal.new-var
  (b* (((mv ?new-var ?new-indices)
        (atj-rename-formal var indices curr-pkg vars-by-name)))
    (symbolp new-var))
  :rule-classes :rewrite)

Theorem: symbol-pos-alistp-of-atj-rename-formal.new-indices

(defthm symbol-pos-alistp-of-atj-rename-formal.new-indices
  (implies
       (and (symbol-pos-alistp indices)
            (symbolp var))
       (b* (((mv ?new-var ?new-indices)
             (atj-rename-formal var indices curr-pkg vars-by-name)))
         (symbol-pos-alistp new-indices)))
  :rule-classes :rewrite)