		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-var-renaming

Atj-rename-formals

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

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

As explained in atj-rename-formal, the shallowly embedded ACL2 variables are made unique via indices. There is an independent index for each ACL2 variable, so we use an alist from symbols to natural numbers to keep track of these indices. This alist is threaded through the functions that rename all the variables in ACL2 terms. This pre-translation step happens after the type annotation and new/old marking step, but the variables in this alist are without annotations and markings, because annotations and markings are discarded when generating Java variables, and thus two ACL2 variables that only differ in annotations or markings must be renamed apart and must share the same index in the alist.

In ACL2, a variable is ``introduced'' as a formal parameter of a function or lambda expression, and then referenced in the body of the function or lambda expression. The choice and use of the index must be done at this introduction time, and not at every reference to the variable after its introduction. Thus, when we encounter the formals of a function or lambda expression, we generate the Java variable names for these ACL2 variables, using the current indices, and update and return the indices. This is the case only if the formal parameter is marked as `new'; if instead it is marked as `old', we look it up in a renaming map, which is an alist from the old variable names to the new variable names, i.e. it expresses the current renaming of variables. There are actually two renaming alists: one for the variables marked as `new', and one for the variables marked as `old': see atj-rename-term for more information. This function takes both renaming maps, and augments both of them with the renamings for the formal parameters that are marked as `new'. The variables in the renaming maps are all type-annotated, for faster lookup when renaming variables in terms. The variables in the renaming maps are not marked as `new' or `old'; as mentioned above, we have two separate maps for new and old variables.

Each ACL2 formal parameter in the input list is processed differently based on whether it is marked `new' or `old'. If it is marked `old', it is simply renamed according to the renaming-old alist, which must include an entry for the variable. When it is marked as `new', it is unmarked and unannotated and passed to atj-rename-formal, which uses and updates the index associated to the variable.

The formals formals being renamed are annotated, because this pre-translation step happens after the type annotation step. Thus, the type annotations are removed prior to the renaming and added back after the renaming.

Definitions and Theorems

Function: atj-rename-formals

(defun atj-rename-formals (formals renaming-new renaming-old
                                   indices curr-pkg vars-by-name)
 (declare
      (xargs :guard (and (symbol-listp formals)
                         (symbol-symbol-alistp renaming-new)
                         (symbol-symbol-alistp renaming-old)
                         (symbol-pos-alistp indices)
                         (stringp curr-pkg)
                         (string-symbollist-alistp vars-by-name))))
 (declare (xargs :guard (not (equal curr-pkg ""))))
 (let ((__function__ 'atj-rename-formals))
   (declare (ignorable __function__))
   (b* (((when (endp formals))
         (mv nil renaming-new renaming-old indices))
        (formal (car formals))
        ((mv uformal new?)
         (atj-unmark-var formal))
        ((when (not new?))
         (b* ((renaming-pair (assoc-eq uformal renaming-old))
              ((unless (consp renaming-pair))
               (raise "Internal error: ~x0 has no renaming."
                      formal)
               (mv (true-list-fix formals)
                   renaming-new renaming-old indices))
              (new-uformal (cdr renaming-pair))
              (new-formal (atj-mark-var-old new-uformal))
              ((mv new-formals
                   renaming-new renaming-old indices)
               (atj-rename-formals (cdr formals)
                                   renaming-new renaming-old
                                   indices curr-pkg vars-by-name)))
           (mv (cons new-formal new-formals)
               renaming-new renaming-old indices)))
        ((mv uuformal types)
         (atj-type-unannotate-var uformal))
        ((mv new-uuformal indices)
         (atj-rename-formal uuformal indices curr-pkg vars-by-name))
        (new-uformal (atj-type-annotate-var new-uuformal types))
        (renaming-new (acons uformal new-uformal renaming-new))
        (renaming-old (acons uformal new-uformal renaming-old))
        (new-formal (atj-mark-var-new new-uformal))
        ((mv new-formals
             renaming-new renaming-old indices)
         (atj-rename-formals (cdr formals)
                             renaming-new renaming-old
                             indices curr-pkg vars-by-name)))
     (mv (cons new-formal new-formals)
         renaming-new renaming-old indices))))

Theorem: symbol-listp-of-atj-rename-formals.new-formals

(defthm symbol-listp-of-atj-rename-formals.new-formals
  (implies
       (and (symbol-listp formals)
            (symbol-symbol-alistp renaming-new))
       (b* (((mv ?new-formals ?new-renaming-new
                 ?new-renaming-old ?new-indices)
             (atj-rename-formals formals renaming-new renaming-old
                                 indices curr-pkg vars-by-name)))
         (symbol-listp new-formals)))
  :rule-classes :rewrite)

Theorem: symbol-symbol-alistp-of-atj-rename-formals.new-renaming-new

(defthm symbol-symbol-alistp-of-atj-rename-formals.new-renaming-new
  (implies
       (and (symbol-listp formals)
            (symbol-symbol-alistp renaming-new))
       (b* (((mv ?new-formals ?new-renaming-new
                 ?new-renaming-old ?new-indices)
             (atj-rename-formals formals renaming-new renaming-old
                                 indices curr-pkg vars-by-name)))
         (symbol-symbol-alistp new-renaming-new)))
  :rule-classes :rewrite)

Theorem: symbol-symbol-alistp-of-atj-rename-formals.new-renaming-old

(defthm symbol-symbol-alistp-of-atj-rename-formals.new-renaming-old
  (implies
       (and (symbol-listp formals)
            (symbol-symbol-alistp renaming-old))
       (b* (((mv ?new-formals ?new-renaming-new
                 ?new-renaming-old ?new-indices)
             (atj-rename-formals formals renaming-new renaming-old
                                 indices curr-pkg vars-by-name)))
         (symbol-symbol-alistp new-renaming-old)))
  :rule-classes :rewrite)

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

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

Theorem: true-listp-of-atj-rename-formals.new-formals

(defthm true-listp-of-atj-rename-formals.new-formals
  (b* (((mv ?new-formals ?new-renaming-new
            ?new-renaming-old ?new-indices)
        (atj-rename-formals formals renaming-new renaming-old
                            indices curr-pkg vars-by-name)))
    (true-listp new-formals))
  :rule-classes :type-prescription)

Theorem: len-of-atj-rename-formals.new-formals

(defthm len-of-atj-rename-formals.new-formals
  (b* (((mv ?new-formals ?new-renaming-new
            ?new-renaming-old ?new-indices)
        (atj-rename-formals formals renaming-new renaming-old
                            indices curr-pkg vars-by-name)))
    (equal (len new-formals)
           (len formals))))