|
|
|---|
|
|
|
|---|
Check if two statements are related by variable renaming.
(statement-renamevar old new ren) → new-ren
In case of success, this function returns a renaming list updated according to the variables introduced in the statement.
Old and new statement must be of the same kind, and have constituents recursively related.
Variable declarations extend the renaming list with additional associations. All the other kinds of statements leave the renaming list unchanged.
We treat the initialization blocks of a loop specially, as usual (e.g. in the static safety checks and in dynamic execution): we extend the renaming list according to the statements in the initialization block, and then we process the rest of the statement with the updated renaming list. However, the renaming list after the loop is the same as the one before: a loop does not permanently introduce new variables.
The ACL2 function to check function definitions does not take a renaming list as argument, because a function definition has a fresh variable scope.