|
|
|---|
|
|
|
|---|
Rename the formal parameters of a defined function or lambda expression.
(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)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
The formals
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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))))