		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-var-renaming

Atj-rename-formals+body

Rename all the ACL2 variables to their Java names, in the formal parameters and body of an ACL2 function.

Signature
(atj-rename-formals+body formals body curr-pkg) → (mv new-formals new-body)
Arguments: formals — Guard (symbol-listp formals).; body — Guard (pseudo-termp body).; curr-pkg — Guard (stringp curr-pkg).
Returns: new-formals — Type (symbol-listp new-formals), given the guard.; new-body — Type (pseudo-termp new-body), given the guard.

We collect all the variables in the formals and body, remove their markings and annotations (recall that the type annotation and new/old marking pre-translation steps take place before this renaming step), and organize them by symbol name: the resulting alist is passed to the renaming functions.

Starting with the empty alist of indices and the empty renaming alists, we introduce renamed variables for the formal parameters, and we use the resulting renaming alists to process the body.

Definitions and Theorems

Function: atj-rename-formals+body

(defun atj-rename-formals+body (formals body curr-pkg)
  (declare (xargs :guard (and (symbol-listp formals)
                              (pseudo-termp body)
                              (stringp curr-pkg))))
  (declare (xargs :guard (not (equal curr-pkg ""))))
  (let ((__function__ 'atj-rename-formals+body))
    (declare (ignorable __function__))
    (b* ((vars (union-eq formals (all-free/bound-vars body)))
         ((mv vars &) (atj-unmark-vars vars))
         (vars (atj-type-unannotate-vars vars))
         (vars-by-name (organize-symbols-by-name vars))
         ((mv new-formals
              renaming-new renaming-old indices)
          (atj-rename-formals formals nil nil *atj-init-indices*
                              curr-pkg vars-by-name))
         ((mv new-body & &)
          (atj-rename-term body renaming-new renaming-old
                           indices curr-pkg vars-by-name)))
      (mv new-formals new-body))))

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

(defthm symbol-listp-of-atj-rename-formals+body.new-formals
  (implies (and (symbol-listp formals)
                (pseudo-termp body)
                (stringp curr-pkg)
                (not (equal curr-pkg '"")))
           (b* (((mv ?new-formals ?new-body)
                 (atj-rename-formals+body formals body curr-pkg)))
             (symbol-listp new-formals)))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atj-rename-formals+body.new-body

(defthm pseudo-termp-of-atj-rename-formals+body.new-body
  (implies (and (symbol-listp formals)
                (pseudo-termp body)
                (stringp curr-pkg)
                (not (equal curr-pkg '"")))
           (b* (((mv ?new-formals ?new-body)
                 (atj-rename-formals+body formals body curr-pkg)))
             (pseudo-termp new-body)))
  :rule-classes :rewrite)

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

(defthm len-of-atj-rename-formals+body.new-formals
  (b* (((mv ?new-formals ?new-body)
        (atj-rename-formals+body formals body curr-pkg)))
    (equal (len new-formals)
           (len formals))))