Renamings
Renamings of variables and functions.
See renaming-variables and renaming-functions.
The renaming information is captured as
a list of pairs of identifiers
((a1 . b1) (a2 . b2) ...)
such that a1, a2, etc. are all distinct
and that b1, b2, etc. are all distinct.
Technically, it is an alist with unique keys and unique values,
but we treat it as a list of pairs,
i.e. we do not use alist operations on it;
it is an injective alist, so its ``direction'' is unimportant.
Each pair (ai . bi) describes a renaming between
the variable ai in the old code
and the variable bi in the new code.
The keys are the variables or functions in scope in the old code;
the values are the variables or functions in scope in the new code.
These facts hold because of the way the list is threaded through,
in the ACL2 code that defines the renaming relation.
These facts are formally explicated and proved as part of the
proof of static safety preservation of variable and function renaming.
The relative ordering of the pairs in the renaming list is irrelevant.
Because of the way the list is constructed,
the pairs happen to be ordered in reverse chronological order,
i.e. the car is the most recent.
From a point of view,
it may be better to use a set of pairs (which is also an omap),
to make it more explicit that the order does not matter.
However, with lists we can more readily use
functions like no-duplicatesp-equal and theorems about them.
Subtopics
- Renaming
- Fixtype of renamings.
- Renaming-result
- Fixtype of errors and renamings.
- Renaming-old
- Set of old variables in a renaming.
- Renaming-new
- Set of new variables in a renaming.
- Renaming-pair-equality
- Theorem about pair equality in renamings.
